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 : ℕ ) → ℕ 
        large    : (n : ℕ ) →  next n > n
        infinite : (n : ℕ ) →  aend Ω ( ω-run Ω (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 

lemma2 : Muller ωa2 flip-seq 
lemma2 = record {
          next = next
       ;  large = large
       ;  infinite = infinite
   }  where
     next : ℕ → ℕ
     next 0 = 1
     next 1 = 3
     next (suc (suc n))  = suc (suc (next n ))
     large :  (n : ℕ) → next n > n
     large 0 =  s≤s ( z≤n )
     large 1 =  s≤s  ( s≤s ( z≤n ) )
     large (suc (suc n))  = s≤s ( s≤s (large n))
     lem2 :  (n : ℕ) →  ω-run ωa2 (suc (suc n)) flip-seq  ≡ ω-run ωa2 n flip-seq
     lem2 zero = refl
     lem2 (suc n) = {!!}
     infinite : (n : ℕ) → aend ωa2 (ω-run ωa2 (next n) flip-seq) ≡ true
     infinite 0 = refl
     infinite 1 = refl
     infinite (suc (suc n)) = let open ≡-Reasoning in
          aend ωa2 (ω-run ωa2 (next (suc (suc n))) flip-seq)
       ≡⟨⟩
          aend ωa2 (ω-run ωa2 (suc (suc (next n))) flip-seq)
       ≡⟨ cong ( λ x -> aend  ωa2 x ) (lem2 (next n) ) ⟩
          aend ωa2 (ω-run ωa2 (next n) flip-seq)
       ≡⟨ infinite n ⟩
          true
       ∎ 

   

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

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