|
327
|
1 module temporal-logic where
|
|
21
|
2
|
|
|
3 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
4 open import Data.Nat
|
|
|
5 open import Data.List
|
|
|
6 open import Data.Maybe
|
|
139
|
7 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate )
|
|
21
|
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
141
|
9 open import Relation.Nullary -- using (not_; Dec; yes; no)
|
|
21
|
10 open import Data.Empty
|
|
|
11
|
|
139
|
12 open import logic
|
|
21
|
13 open import automaton
|
|
|
14
|
|
|
15 open Automaton
|
|
|
16
|
|
|
17
|
|
326
|
18 open import nat
|
|
|
19 open import Data.Nat.Properties
|
|
|
20
|
|
|
21 data LTTL ( V : Set ) : Set where
|
|
|
22 s : V → LTTL V
|
|
|
23 ○ : LTTL V → LTTL V
|
|
|
24 □ : LTTL V → LTTL V
|
|
|
25 ⋄ : LTTL V → LTTL V
|
|
|
26 _U_ : LTTL V → LTTL V → LTTL V
|
|
|
27 t-not : LTTL V → LTTL V
|
|
|
28 _t\/_ : LTTL V → LTTL V → LTTL V
|
|
|
29 _t/\_ : LTTL V → LTTL V → LTTL V
|
|
21
|
30
|
|
326
|
31 {-# TERMINATING #-}
|
|
|
32 M1 : { V : Set } → (ℕ → V → Bool) → ℕ → LTTL V → Set
|
|
|
33 M1 σ i (s x) = σ i x ≡ true
|
|
|
34 M1 σ i (○ x) = M1 σ (suc i) x
|
|
|
35 M1 σ i (□ p) = (j : ℕ) → i ≤ j → M1 σ j p
|
|
328
|
36 M1 σ i (⋄ p) = ¬ ( M1 σ i (□ (t-not p) ))
|
|
326
|
37 M1 σ i (p U q) = ¬ ( ( j : ℕ) → i ≤ j → ¬ (M1 σ j q ∧ (( k : ℕ) → i ≤ k → k < j → M1 σ j p )) )
|
|
|
38 M1 σ i (t-not p) = ¬ ( M1 σ i p )
|
|
|
39 M1 σ i (p t\/ p₁) = M1 σ i p ∧ M1 σ i p₁
|
|
|
40 M1 σ i (p t/\ p₁) = M1 σ i p ∨ M1 σ i p₁
|
|
21
|
41
|
|
326
|
42 data LITL ( V : Set ) : Set where
|
|
|
43 iv : V → LITL V
|
|
|
44 i○ : LITL V → LITL V
|
|
|
45 _&_ : LITL V → LITL V → LITL V
|
|
|
46 i-not : LITL V → LITL V
|
|
|
47 _i\/_ : LITL V → LITL V → LITL V
|
|
|
48 _i/\_ : LITL V → LITL V → LITL V
|
|
21
|
49
|
|
326
|
50 open import Relation.Binary.Definitions
|
|
|
51 open import Data.Unit using ( tt ; ⊤ )
|
|
21
|
52
|
|
326
|
53 {-# TERMINATING #-}
|
|
|
54 MI : { V : Set } → (ℕ → V → Bool) → (i j : ℕ) → i ≤ j → LITL V → Set
|
|
|
55 MI σ i j lt (iv x) = σ i x ≡ true
|
|
|
56 MI σ i j lt (i○ x) with <-cmp i j
|
|
328
|
57 ... | tri< a ¬b ¬c = MI σ (suc i) j a x
|
|
326
|
58 ... | tri≈ ¬a b ¬c = ⊤
|
|
|
59 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c)
|
|
|
60 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))
|
|
|
61 MI σ i j lt (i-not p) = ¬ ( MI σ i j lt p )
|
|
|
62 MI σ i j lt (p i\/ p₁) = MI σ i j lt p ∧ MI σ i j lt p₁
|
|
|
63 MI σ i j lt (p i/\ p₁) = MI σ i j lt p ∨ MI σ i j lt p₁
|
|
|
64
|
|
327
|
65 data QBool ( V : Set ) : Set where
|
|
|
66 qb : Bool → QBool V
|
|
|
67 qv : V → QBool V
|
|
|
68 exists : V → QBool V → QBool V
|
|
|
69 b-not : QBool V → QBool V
|
|
|
70 _b\/_ : QBool V → QBool V → QBool V
|
|
|
71 _b/\_ : QBool V → QBool V → QBool V
|
|
|
72
|
|
|
73 {-# TERMINATING #-}
|
|
|
74 SQ1 : { V : Set } → ((x y : V) → Dec ( x ≡ y)) → QBool V → V → Bool → QBool V
|
|
|
75 SQ1 {V} dec (qb x) v t = qb x
|
|
|
76 SQ1 {V} dec (qv x) v t with dec x v
|
|
|
77 ... | yes _ = qb t
|
|
|
78 ... | no _ = qv x
|
|
|
79 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
|
|
|
80 SQ1 {V} dec (b-not p) v t = b-not (SQ1 dec p v t )
|
|
|
81 SQ1 {V} dec (p b\/ p₁) v t = SQ1 dec p v t b\/ SQ1 dec p₁ v t
|
|
|
82 SQ1 {V} dec (p b/\ p₁) v t = SQ1 dec p v t b/\ SQ1 dec p₁ v t
|
|
|
83
|
|
|
84 {-# TERMINATING #-}
|
|
|
85 MQ : { V : Set } → (V → Bool) → ((x y : V) → Dec ( x ≡ y)) → QBool V → Bool
|
|
|
86 MQ {V} val dec (qb x) = x
|
|
|
87 MQ {V} val dec (qv x) = val x
|
|
|
88 MQ {V} val dec (exists x p) = MQ val dec ( SQ1 dec p x true b\/ SQ1 dec p x false )
|
|
|
89 MQ {V} val dec (b-not p) = not ( MQ val dec p )
|
|
|
90 MQ {V} val dec (p b\/ p₁) = MQ val dec p \/ MQ val dec p₁
|
|
|
91 MQ {V} val dec (p b/\ p₁) = MQ val dec p /\ MQ val dec p₁
|
|
|
92
|
|
|
93 data QPTL ( V : Set ) : Set where
|
|
328
|
94 qt : Bool → QPTL V
|
|
327
|
95 qs : V → QPTL V
|
|
|
96 q○ : QPTL V → QPTL V
|
|
|
97 q□ : QPTL V → QPTL V
|
|
|
98 q⋄ : QPTL V → QPTL V
|
|
|
99 q-exists : V → QPTL V → QPTL V
|
|
|
100 q-not : QPTL V → QPTL V
|
|
|
101 _q\/_ : QPTL V → QPTL V → QPTL V
|
|
|
102 _q/\_ : QPTL V → QPTL V → QPTL V
|
|
|
103
|
|
330
|
104 --
|
|
|
105 -- ∃ p ( <> p → ? )
|
|
|
106 --
|
|
|
107
|
|
|
108
|
|
328
|
109 {-# TERMINATING #-}
|
|
|
110 SQP1 : { V : Set } → ((x y : V) → Dec ( x ≡ y)) → QPTL V → V → Bool → QPTL V
|
|
|
111 SQP1 {V} dec (qt x) v t = qt x
|
|
|
112 SQP1 {V} dec (qs x) v t with dec x v
|
|
|
113 ... | yes _ = qt t
|
|
|
114 ... | no _ = qs x
|
|
|
115 SQP1 {V} dec (q-exists x p) v t = SQP1 dec (SQP1 dec p x true) v t q\/ SQP1 dec (SQP1 dec p x false) v t
|
|
|
116 SQP1 {V} dec (q○ p) v t = q○ p
|
|
|
117 SQP1 {V} dec (q□ p) v t = SQP1 {V} dec p v t q/\ q□ p
|
|
|
118 SQP1 {V} dec (q⋄ p) v t = q-not ( SQP1 dec (q□ (q-not p)) v t)
|
|
|
119 SQP1 {V} dec (q-not p) v t = q-not ( SQP1 dec p v t )
|
|
|
120 SQP1 {V} dec (p q\/ p₁) v t = SQP1 {V} dec p v t q\/ SQP1 {V} dec p₁ v t
|
|
|
121 SQP1 {V} dec (p q/\ p₁) v t = SQP1 {V} dec p v t q/\ SQP1 {V} dec p₁ v t
|
|
|
122
|
|
|
123 {-# TERMINATING #-}
|
|
|
124 MQPTL : { V : Set } → (ℕ → V → Bool) → ℕ → ((x y : V) → Dec ( x ≡ y)) → QPTL V → Set
|
|
|
125 MQPTL σ i dec (qt x) = x ≡ true
|
|
|
126 MQPTL σ i dec (qs x) = σ i x ≡ true
|
|
|
127 MQPTL σ i dec (q○ x) = MQPTL σ (suc i) dec x
|
|
|
128 MQPTL σ i dec (q□ p) = (j : ℕ) → i ≤ j → MQPTL σ j dec p
|
|
|
129 MQPTL σ i dec (q⋄ p) = ¬ ( MQPTL σ i dec (q□ (q-not p) ))
|
|
|
130 MQPTL σ i dec (q-not p) = ¬ ( MQPTL σ i dec p )
|
|
|
131 MQPTL σ i dec (q-exists x p) = MQPTL σ i dec ( SQP1 dec p x true q\/ (SQP1 dec p x false))
|
|
|
132 MQPTL σ i dec (p q\/ p₁) = MQPTL σ i dec p ∧ MQPTL σ i dec p₁
|
|
|
133 MQPTL σ i dec (p q/\ p₁) = MQPTL σ i dec p ∨ MQPTL σ i dec p₁
|
|
|
134
|
