Mercurial > hg > Members > kono > Proof > automaton

comparison agda/omega-automaton.agda @ 164:bee86ee07fff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 12 Mar 2021 21:45:53 +0900
parents b3f05cd08d24
children
comparison
equal deleted inserted replaced
163:26407ce19d66 164:bee86ee07fff
12 open import logic 12 open import logic
13 open import automaton 13 open import automaton
14 14
15 open Automaton 15 open Automaton
16 16
17 ω-run : { Q Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q ) → ℕ → ( ℕ → Σ ) → Q 17 ω-run : { Q Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q ) → ℕ → ( ℕ → Σ ) → Q
18 ω-run Ω x zero s = x 18 ω-run Ω x zero s = x
19 ω-run Ω x (suc n) s = δ Ω (ω-run Ω ? n s) ( s n ) 19 ω-run Ω x (suc n) s = δ Ω (ω-run Ω x n s) ( s n )
20 20
21 --
22 -- accept as Buchi automaton
23 --
21 record Buchi { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where 24 record Buchi { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
22 field 25 field
23 from : ℕ 26 from : ℕ
24 stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω ? n S ) ≡ true 27 stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x n S ) ≡ true
25 28
26 open Buchi 29 open Buchi
27 30
31 -- after sometimes, always p
32 --
33 -- not p
34 -- ------------>
35 -- <> [] p * <> [] p
36 -- <-----------
37 -- p
38
28 39
40 --
41 -- accept as Muller automaton
42 --
29 record Muller { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where 43 record Muller { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
30 field 44 field
31 next : (n : ℕ ) → ℕ 45 next : (n : ℕ ) → ℕ
32 infinite : (n : ℕ ) → aend Ω ( ω-run Ω ? (n + (next n)) S ) ≡ true 46 infinite : (x : Q) → (n : ℕ ) → aend Ω ( ω-run Ω x (n + (next n)) S ) ≡ true
33 47
48 -- always sometimes p
49 --
34 -- not p 50 -- not p
35 -- ------------> 51 -- ------------>
36 -- [] <> p * [] <> p 52 -- [] <> p * [] <> p
37 -- <----------- 53 -- <-----------
38 -- p 54 -- p
65 81
66 flip-seq : ℕ → Bool 82 flip-seq : ℕ → Bool
67 flip-seq zero = false 83 flip-seq zero = false
68 flip-seq (suc n) = not ( flip-seq n ) 84 flip-seq (suc n) = not ( flip-seq n )
69 85
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
70 lemma1 : Buchi ωa1 true-seq 95 lemma1 : Buchi ωa1 true-seq
71 lemma1 = record { 96 lemma1 = record {
72 from = zero 97 from = zero
73 ; stay = lem1 98 ; stay = {!!}
74 } where 99 } where
75 lem1 : ( n : ℕ ) → n > zero → aend ωa1 (ω-run ωa1 ? n true-seq ) ≡ true 100 lem1 : ( n : ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} n true-seq ) ≡ true
76 lem1 zero () 101 lem1 zero ()
77 lem1 (suc n) (s≤s z≤n) with ω-run ωa1 ? n true-seq 102 lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} n true-seq
78 lem1 (suc n) (s≤s z≤n) | ts* = ? 103 lem1 (suc n) (s≤s z≤n) | ts* = {!!}
79 lem1 (suc n) (s≤s z≤n) | ts = ? 104 lem1 (suc n) (s≤s z≤n) | ts = {!!}
80 105
81 ωa2 : Automaton States3 Bool 106 ωa2 : Automaton States3 Bool
82 ωa2 = record { 107 ωa2 = record {
83 δ = transition3 108 δ = transition3
84 ; aend = λ x → not ( mark1 x ) 109 ; aend = λ x → not ( mark1 x )
95 ≡⟨⟩ 120 ≡⟨⟩
96 ( not ( flip-seq n ) ) 121 ( not ( flip-seq n ) )
97 ∎ 122 ∎
98 123
99 flip-dec2 : (n : ℕ ) → not flip-seq (suc n) ≡ flip-seq n 124 flip-dec2 : (n : ℕ ) → not flip-seq (suc n) ≡ flip-seq n
100 flip-dec2 n = ? 125 flip-dec2 n = {!!}
101 126
102 127
103 record flipProperty : Set where 128 record flipProperty : Set where
104 field 129 field
105 flipP : (n : ℕ) → ω-run ωa2 ? flip-seq ≡ ω-run ωa2 n flip-seq 130 flipP : (n : ℕ) → ω-run ωa2 {!!} {!!} ≡ ω-run ωa2 {!!} {!!}
106 131
107 lemma2 : Muller ωa2 flip-seq 132 lemma2 : Muller ωa2 flip-seq
108 lemma2 = record { 133 lemma2 = record {
109 next = next 134 next = next
110 ; infinite = infinite 135 ; infinite = {!!}
111 } where 136 } where
112 next : ℕ → ℕ 137 next : ℕ → ℕ
113 next n with ω-run ωa2 n flip-seq | flip-seq n 138 next = {!!}
114 next n | ts | true = 2 139 infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 {!!} ≡ true → aend ωa2 {!!} ≡ true
115 next n | ts | false = 1
116 next n | ts* | true = 2
117 next n | ts* | false = 1
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' = {!!} 140 infinite' = {!!}
120 infinite : (n : ℕ) → aend ωa2 (ω-run ωa2 (n + (next n)) flip-seq) ≡ true 141 infinite : (n : ℕ) → aend ωa2 {!!} ≡ true
121 infinite = {!!} 142 infinite = {!!}
122 143
123 lemma3 : Buchi ωa1 false-seq → ⊥ 144 lemma3 : Buchi ωa1 false-seq → ⊥
124 lemma3 = {!!} 145 lemma3 = {!!}
125 146