--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/omega-automaton.agda	Thu Aug 30 17:31:57 2018 +0900
@@ -0,0 +1,120 @@
+module omega-automaton where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+open import Data.List
+open import Data.Maybe
+open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.Empty
+
+open import automaton
+
+open Automaton 
+
+record Seq ( Σ : Set  )
+       : Set  where
+    field
+        value :  ℕ → Σ
+
+open Seq
+
+ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → Seq Σ  → Q
+ω-run Ω zero s = astart Ω
+ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( value s n )
+
+record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : Seq  Σ ) : Set where
+    field
+        from : ℕ
+        stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω n S ) ≡ true
+
+open Buchi
+       
+    
+record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : Seq  Σ ) : Set where
+    field
+        first : ℕ 
+        first-hit : aend Ω ( ω-run Ω first S ) ≡ true
+        next : (n : ℕ ) →  ℕ 
+        next-hit : {n : ℕ } → aend Ω ( ω-run Ω n S ) ≡ true → aend Ω ( ω-run Ω (n + next n) S ) ≡ true
+
+--                       ¬ p
+--                   ------------>
+--        [] <> p *                 [] <> p 
+--                   <-----------
+--                       p
+
+data  States3   : Set  where
+   ts* : States3
+   ts  : States3
+
+transition3 : States3  → Bool  → States3
+transition3 ts* true  = ts*
+transition3 ts* false  = ts
+transition3 ts true  = ts*
+transition3 ts false  = ts
+
+mark1 :  States3  → Bool
+mark1 ts* = true
+mark1 ts = false
+
+ωa1 : Automaton States3 Bool
+ωa1 = record {
+        δ = transition3
+     ;  astart = ts*
+     ;  aend = mark1
+  }  
+
+true-seq :  ℕ → Bool
+true-seq _ = true
+
+false-seq :  ℕ → Bool
+false-seq _ = false
+
+flip-seq :  ℕ → Bool
+flip-seq zero = false
+flip-seq (suc n) = negate ( flip-seq n )
+
+lemma1 : Buchi ωa1 ( record { value = true-seq } )
+lemma1 = record {
+        from = zero
+      ; stay = lem1
+   } where
+      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 n (record { value = true-seq })) ≡ true
+      lem1 zero ()
+      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 n (record { value = true-seq })
+      lem1 (suc n) (s≤s z≤n) | ts* = refl
+      lem1 (suc n) (s≤s z≤n) | ts = refl
+
+ωa2 : Automaton States3 Bool
+ωa2 = record {
+        δ = transition3
+     ;  astart = ts*
+     ;  aend = λ x → negate ( mark1 x )
+  }  
+
+lemma2 : Muller ωa2 ( record { value = flip-seq } )
+lemma2 = record {
+        first = 1
+     ;  first-hit =  refl
+     ;  next = λ x → 2
+     ;  next-hit = {!!}
+   }  where
+    lemma : {n : ℕ} → aend ωa2 (ω-run ωa2 n (record { value = false-seq })) ≡ true
+      → aend ωa2 (ω-run ωa2 (n + 2) (record { value = false-seq })) ≡ true
+    lemma {n} prev = {!!}
+   
+
+lemma3 : Buchi ωa1 ( record { value = false-seq } ) →  ⊥
+lemma3 = {!!}
+
+lemma4 : Muller ωa1 ( record { value = flip-seq } ) →  ⊥
+lemma4 = {!!}
+
+
+
+
+
+
+