# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1642735894 -32400
# Node ID 4aa0ebd756730e7414af2243922dafe909bb3b0b
# Parent  a3fb231feeb9beeaa51298ca672c2c664938a351
...

diff -r a3fb231feeb9 -r 4aa0ebd75673 automaton-in-agda/src/omega-automaton.agda
--- a/automaton-in-agda/src/omega-automaton.agda	Fri Jan 21 10:45:42 2022 +0900
+++ b/automaton-in-agda/src/omega-automaton.agda	Fri Jan 21 12:31:34 2022 +0900
@@ -184,47 +184,3 @@
 lemma4 = {!!}
 
 
-data LTTL ( V : Set )  : Set where
-    s :  V → LTTL V
-    ○ :  LTTL V → LTTL V
-    □ :  LTTL V → LTTL V
-    ⋄ :  LTTL V → LTTL V
-    _U_  :  LTTL V → LTTL  V → LTTL  V
-    t-not :  LTTL V → LTTL  V
-    _t\/_ :  LTTL V → LTTL  V → LTTL  V
-    _t/\_ :  LTTL V → LTTL  V → LTTL  V
-
-{-# TERMINATING #-}
-M1 : { V : Set } → (ℕ → V → Bool) → ℕ →  LTTL V  → Set
-M1 σ i (s x) = σ i x ≡ true
-M1 σ i (○ x) = M1 σ (suc i) x  
-M1 σ i (□ p) = (j : ℕ) → i ≤ j → M1  σ j p
-M1 σ i (⋄ p) = ¬ ( M1 σ i (t-not p) )
-M1 σ i (p U q) = ¬ ( ( j : ℕ) → i ≤ j → ¬ (M1 σ j q ∧ (( k : ℕ) → i ≤ k → k < j → M1 σ j p )) )
-M1 σ i (t-not p) = ¬ ( M1 σ i p )
-M1 σ i (p t\/ p₁) = M1 σ i p ∧ M1 σ i p₁ 
-M1 σ i (p t/\ p₁) = M1 σ i p ∨ M1 σ i p₁ 
-
-data LITL ( V : Set )  : Set where
-    iv :  V → LITL V
-    i○ :  LITL V → LITL V
-    _&_  :  LITL V → LITL  V → LITL  V
-    i-not :  LITL V → LITL  V
-    _i\/_ :  LITL V → LITL  V → LITL  V
-    _i/\_ :  LITL V → LITL  V → LITL  V
-
-open import Relation.Binary.Definitions
-open import Data.Unit using ( tt ; ⊤ )
-
-{-# TERMINATING #-}
-MI : { V : Set } → (ℕ → V → Bool) → (i j : ℕ) → i ≤ j  →  LITL V  → Set
-MI σ i j lt (iv x) = σ i x ≡ true
-MI σ i j lt (i○ x) with <-cmp i j
-... | tri< a ¬b ¬c = MI σ (suc i) j {!!} x
-... | tri≈ ¬a b ¬c = ⊤
-... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c)
-MI σ i j lt (p & q) = ¬ ( ( k : ℕ) → (i<k : i ≤ k) → (k<j : k ≤ j) → ¬ ( MI σ i k i<k p ∧ MI σ k j k<j p))
-MI σ i j lt (i-not p) = ¬ ( MI σ i j lt p )
-MI σ i j lt (p i\/ p₁) = MI σ i j lt p ∧ MI σ i j lt p₁ 
-MI σ i j lt (p i/\ p₁) = MI σ i j lt p ∨ MI σ i j lt p₁ 
-
diff -r a3fb231feeb9 -r 4aa0ebd75673 automaton-in-agda/src/temporal-logic.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton-in-agda/src/temporal-logic.agda	Fri Jan 21 12:31:34 2022 +0900
@@ -0,0 +1,102 @@
+module temporal-logic  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 (not_; Dec; yes; no)
+open import Data.Empty
+
+open import logic
+open import automaton
+
+open Automaton 
+
+
+open import nat
+open import Data.Nat.Properties
+
+data LTTL ( V : Set )  : Set where
+    s :  V → LTTL V
+    ○ :  LTTL V → LTTL V
+    □ :  LTTL V → LTTL V
+    ⋄ :  LTTL V → LTTL V
+    _U_  :  LTTL V → LTTL  V → LTTL  V
+    t-not :  LTTL V → LTTL  V
+    _t\/_ :  LTTL V → LTTL  V → LTTL  V
+    _t/\_ :  LTTL V → LTTL  V → LTTL  V
+
+{-# TERMINATING #-}
+M1 : { V : Set } → (ℕ → V → Bool) → ℕ →  LTTL V  → Set
+M1 σ i (s x) = σ i x ≡ true
+M1 σ i (○ x) = M1 σ (suc i) x  
+M1 σ i (□ p) = (j : ℕ) → i ≤ j → M1  σ j p
+M1 σ i (⋄ p) = ¬ ( M1 σ i (t-not p) )
+M1 σ i (p U q) = ¬ ( ( j : ℕ) → i ≤ j → ¬ (M1 σ j q ∧ (( k : ℕ) → i ≤ k → k < j → M1 σ j p )) )
+M1 σ i (t-not p) = ¬ ( M1 σ i p )
+M1 σ i (p t\/ p₁) = M1 σ i p ∧ M1 σ i p₁ 
+M1 σ i (p t/\ p₁) = M1 σ i p ∨ M1 σ i p₁ 
+
+data LITL ( V : Set )  : Set where
+    iv :  V → LITL V
+    i○ :  LITL V → LITL V
+    _&_  :  LITL V → LITL  V → LITL  V
+    i-not :  LITL V → LITL  V
+    _i\/_ :  LITL V → LITL  V → LITL  V
+    _i/\_ :  LITL V → LITL  V → LITL  V
+
+open import Relation.Binary.Definitions
+open import Data.Unit using ( tt ; ⊤ )
+
+{-# TERMINATING #-}
+MI : { V : Set } → (ℕ → V → Bool) → (i j : ℕ) → i ≤ j  →  LITL V  → Set
+MI σ i j lt (iv x) = σ i x ≡ true
+MI σ i j lt (i○ x) with <-cmp i j
+... | tri< a ¬b ¬c = MI σ (suc i) j {!!} x
+... | tri≈ ¬a b ¬c = ⊤
+... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c)
+MI σ i j lt (p & q) = ¬ ( ( k : ℕ) → (i<k : i ≤ k) → (k<j : k ≤ j) → ¬ ( MI σ i k i<k p ∧ MI σ k j k<j p))
+MI σ i j lt (i-not p) = ¬ ( MI σ i j lt p )
+MI σ i j lt (p i\/ p₁) = MI σ i j lt p ∧ MI σ i j lt p₁ 
+MI σ i j lt (p i/\ p₁) = MI σ i j lt p ∨ MI σ i j lt p₁ 
+
+data QBool ( V : Set )  : Set where
+    qb :  Bool → QBool V
+    qv :  V → QBool V
+    exists :  V → QBool V → QBool V
+    b-not :  QBool V → QBool  V
+    _b\/_ :  QBool V → QBool  V → QBool  V
+    _b/\_ :  QBool V → QBool  V → QBool  V
+
+{-# TERMINATING #-}
+SQ1 : { V : Set } → ((x y : V) → Dec ( x ≡ y))   → QBool V → V  → Bool → QBool V
+SQ1 {V} dec (qb x) v t = qb x
+SQ1 {V} dec (qv x) v t with dec x v
+... | yes _ = qb t
+... | no _ = qv x
+SQ1 {V} dec (exists x p) v t = SQ1 dec (SQ1 dec p x true) v t b\/  SQ1 dec (SQ1 dec p x false) v t
+SQ1 {V} dec (b-not p) v t = b-not (SQ1 dec p v t )
+SQ1 {V} dec (p b\/ p₁) v t =  SQ1 dec p v t b\/  SQ1 dec p₁ v t
+SQ1 {V} dec (p b/\ p₁) v t = SQ1 dec p v t b/\  SQ1 dec p₁ v t
+
+{-# TERMINATING #-}
+MQ : { V : Set } → (V → Bool) → ((x y : V) → Dec ( x ≡ y))   → QBool V → Bool
+MQ {V} val dec (qb x) = x
+MQ {V} val dec (qv x) = val x
+MQ {V} val dec (exists x p) =  MQ val dec ( SQ1 dec p x true b\/ SQ1 dec p x false )
+MQ {V} val dec (b-not p) = not ( MQ val dec p )
+MQ {V} val dec (p b\/ p₁) = MQ val dec p \/ MQ val dec p₁ 
+MQ {V} val dec (p b/\ p₁) = MQ val dec p /\ MQ val dec p₁ 
+
+data QPTL ( V : Set )  : Set where
+    qs :  V → QPTL V
+    q○ :  QPTL V → QPTL V
+    q□ :  QPTL V → QPTL V
+    q⋄ :  QPTL V → QPTL V
+    q-exists :  V → QPTL V → QPTL V
+    q-not :  QPTL V → QPTL  V
+    _q\/_ :  QPTL V → QPTL  V → QPTL  V
+    _q/\_ :  QPTL V → QPTL  V → QPTL  V
+