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