|
21
|
1 module omega-automaton where
|
|
|
2
|
|
|
3 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
4 open import Data.Nat
|
|
|
5 open import Data.List
|
|
|
6 open import Data.Maybe
|
|
139
|
7 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate )
|
|
21
|
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
141
|
9 open import Relation.Nullary -- using (not_; Dec; yes; no)
|
|
21
|
10 open import Data.Empty
|
|
|
11
|
|
139
|
12 open import logic
|
|
21
|
13 open import automaton
|
|
|
14
|
|
|
15 open Automaton
|
|
|
16
|
|
164
|
17 ω-run : { Q Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q ) → ℕ → ( ℕ → Σ ) → Q
|
|
139
|
18 ω-run Ω x zero s = x
|
|
164
|
19 ω-run Ω x (suc n) s = δ Ω (ω-run Ω x n s) ( s n )
|
|
21
|
20
|
|
164
|
21 --
|
|
|
22 -- accept as Buchi automaton
|
|
|
23 --
|
|
22
|
24 record Buchi { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
|
|
21
|
25 field
|
|
|
26 from : ℕ
|
|
164
|
27 stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x n S ) ≡ true
|
|
21
|
28
|
|
|
29 open Buchi
|
|
164
|
30
|
|
|
31 -- after sometimes, always p
|
|
|
32 --
|
|
|
33 -- not p
|
|
|
34 -- ------------>
|
|
|
35 -- <> [] p * <> [] p
|
|
|
36 -- <-----------
|
|
|
37 -- p
|
|
|
38
|
|
21
|
39
|
|
164
|
40 --
|
|
|
41 -- accept as Muller automaton
|
|
|
42 --
|
|
22
|
43 record Muller { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
|
|
21
|
44 field
|
|
22
|
45 next : (n : ℕ ) → ℕ
|
|
164
|
46 infinite : (x : Q) → (n : ℕ ) → aend Ω ( ω-run Ω x (n + (next n)) S ) ≡ true
|
|
21
|
47
|
|
164
|
48 -- always sometimes p
|
|
|
49 --
|
|
139
|
50 -- not p
|
|
21
|
51 -- ------------>
|
|
|
52 -- [] <> p * [] <> p
|
|
|
53 -- <-----------
|
|
|
54 -- p
|
|
|
55
|
|
|
56 data States3 : Set where
|
|
|
57 ts* : States3
|
|
|
58 ts : States3
|
|
|
59
|
|
|
60 transition3 : States3 → Bool → States3
|
|
|
61 transition3 ts* true = ts*
|
|
|
62 transition3 ts* false = ts
|
|
|
63 transition3 ts true = ts*
|
|
|
64 transition3 ts false = ts
|
|
|
65
|
|
|
66 mark1 : States3 → Bool
|
|
|
67 mark1 ts* = true
|
|
|
68 mark1 ts = false
|
|
|
69
|
|
|
70 ωa1 : Automaton States3 Bool
|
|
|
71 ωa1 = record {
|
|
|
72 δ = transition3
|
|
|
73 ; aend = mark1
|
|
|
74 }
|
|
|
75
|
|
|
76 true-seq : ℕ → Bool
|
|
|
77 true-seq _ = true
|
|
|
78
|
|
|
79 false-seq : ℕ → Bool
|
|
|
80 false-seq _ = false
|
|
|
81
|
|
|
82 flip-seq : ℕ → Bool
|
|
|
83 flip-seq zero = false
|
|
139
|
84 flip-seq (suc n) = not ( flip-seq n )
|
|
21
|
85
|
|
164
|
86 lemma0 : Muller ωa1 flip-seq
|
|
|
87 lemma0 = record {
|
|
|
88 next = λ n → suc (suc n)
|
|
|
89 ; infinite = lemma01
|
|
|
90 } where
|
|
|
91 lemma01 : (x : States3) (n : ℕ) →
|
|
|
92 aend ωa1 (ω-run ωa1 x (n + suc (suc n)) flip-seq) ≡ true
|
|
|
93 lemma01 = {!!}
|
|
|
94
|
|
22
|
95 lemma1 : Buchi ωa1 true-seq
|
|
21
|
96 lemma1 = record {
|
|
|
97 from = zero
|
|
164
|
98 ; stay = {!!}
|
|
21
|
99 } where
|
|
164
|
100 lem1 : ( n : ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} n true-seq ) ≡ true
|
|
21
|
101 lem1 zero ()
|
|
164
|
102 lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} n true-seq
|
|
|
103 lem1 (suc n) (s≤s z≤n) | ts* = {!!}
|
|
|
104 lem1 (suc n) (s≤s z≤n) | ts = {!!}
|
|
21
|
105
|
|
|
106 ωa2 : Automaton States3 Bool
|
|
|
107 ωa2 = record {
|
|
|
108 δ = transition3
|
|
139
|
109 ; aend = λ x → not ( mark1 x )
|
|
21
|
110 }
|
|
|
111
|
|
22
|
112 flip-dec : (n : ℕ ) → Dec ( flip-seq n ≡ true )
|
|
|
113 flip-dec n with flip-seq n
|
|
|
114 flip-dec n | false = no λ ()
|
|
|
115 flip-dec n | true = yes refl
|
|
|
116
|
|
139
|
117 flip-dec1 : (n : ℕ ) → flip-seq (suc n) ≡ ( not ( flip-seq n ) )
|
|
22
|
118 flip-dec1 n = let open ≡-Reasoning in
|
|
|
119 flip-seq (suc n )
|
|
|
120 ≡⟨⟩
|
|
139
|
121 ( not ( flip-seq n ) )
|
|
22
|
122 ∎
|
|
|
123
|
|
139
|
124 flip-dec2 : (n : ℕ ) → not flip-seq (suc n) ≡ flip-seq n
|
|
164
|
125 flip-dec2 n = {!!}
|
|
22
|
126
|
|
23
|
127
|
|
|
128 record flipProperty : Set where
|
|
|
129 field
|
|
164
|
130 flipP : (n : ℕ) → ω-run ωa2 {!!} {!!} ≡ ω-run ωa2 {!!} {!!}
|
|
23
|
131
|
|
22
|
132 lemma2 : Muller ωa2 flip-seq
|
|
21
|
133 lemma2 = record {
|
|
22
|
134 next = next
|
|
164
|
135 ; infinite = {!!}
|
|
21
|
136 } where
|
|
22
|
137 next : ℕ → ℕ
|
|
164
|
138 next = {!!}
|
|
|
139 infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 {!!} ≡ true → aend ωa2 {!!} ≡ true
|
|
24
|
140 infinite' = {!!}
|
|
164
|
141 infinite : (n : ℕ) → aend ωa2 {!!} ≡ true
|
|
24
|
142 infinite = {!!}
|
|
21
|
143
|
|
22
|
144 lemma3 : Buchi ωa1 false-seq → ⊥
|
|
21
|
145 lemma3 = {!!}
|
|
|
146
|
|
22
|
147 lemma4 : Muller ωa1 flip-seq → ⊥
|
|
21
|
148 lemma4 = {!!}
|
|
|
149
|
|
|
150
|
|
|
151
|
|
|
152
|
|
|
153
|
|
|
154
|
|
|
155
|
