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 

ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → ( ℕ → Σ )  → Q
ω-run Ω zero s = astart Ω
ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n )

record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
    field
        from : ℕ
        stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω n S ) ≡ true

open Buchi
       
    
record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
    field
        next     : (n : ℕ ) → ℕ 
        infinite : (n : ℕ ) →  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 true-seq 
lemma1 = record {
        from = zero
      ; stay = lem1
   } where
      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 n true-seq ) ≡ true
      lem1 zero ()
      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 n 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 )
  }  

flip-dec : (n : ℕ ) →  Dec (  flip-seq n   ≡ true )
flip-dec n with flip-seq n
flip-dec n | false = no  λ () 
flip-dec n | true = yes refl

flip-dec1 : (n : ℕ ) → flip-seq (suc n)  ≡ negate ( flip-seq n )
flip-dec1 n = let open ≡-Reasoning in
          flip-seq (suc n )
       ≡⟨⟩
          negate ( flip-seq n )
       ∎

flip-dec2 : (n : ℕ ) → ¬ flip-seq (suc n)  ≡  flip-seq n 
flip-dec2 n neq with  flip-seq n
flip-dec2 n () | false 
flip-dec2 n () | true 


record flipProperty : Set where
    field
       flipP : (n : ℕ) →  ω-run ωa2 (suc (suc n)) flip-seq  ≡ ω-run ωa2 n flip-seq

lemma2 : Muller ωa2 flip-seq 
lemma2 = record {
          next = next
       ;  infinite = infinite
   }  where
     next : ℕ → ℕ
     next n with ω-run ωa2 n flip-seq | flip-seq n
     next n | ts | true = 2
     next n | ts | false = 1
     next n | ts* | true = 2
     next n | ts* | false = 1
     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
     infinite' = {!!}
     infinite : (n : ℕ) → aend ωa2 (ω-run ωa2 (n + (next n)) flip-seq) ≡ true
     infinite = {!!}

lemma3 : Buchi ωa1 false-seq  →  ⊥
lemma3 = {!!}

lemma4 : Muller ωa1 flip-seq  →  ⊥
lemma4 = {!!}