Mercurial > hg > Members > kono > Proof > automaton
view automaton-in-agda/src/temporal-logic.agda @ 327:4aa0ebd75673
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 21 Jan 2022 12:31:34 +0900 (2022-01-21) |
parents | automaton-in-agda/src/omega-automaton.agda@a3fb231feeb9 |
children | cd73fe566291 |
line wrap: on
line source
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