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