Mercurial > hg > Gears > GearsAgda
annotate ModelChecking.agda @ 953:24255e0dd027
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 13 Sep 2024 13:25:17 +0900 |
| parents | 057d3309ed9d |
| children |
| rev | line source |
|---|---|
| 949 | 1 -- {-# OPTIONS --cubical-compatible --allow-unsolved-metas #-} |
| 2 {-# OPTIONS --cubical-compatible --safe #-} | |
| 635 | 3 module ModelChecking where |
| 4 | |
| 5 open import Level renaming (zero to Z ; suc to succ) | |
| 6 | |
| 7 open import Data.Nat hiding (compare) | |
| 8 open import Data.Nat.Properties as NatProp | |
| 9 open import Data.Maybe | |
| 10 -- open import Data.Maybe.Properties | |
| 11 open import Data.Empty | |
| 12 open import Data.List | |
| 710 | 13 -- open import Data.Tree.Binary |
| 14 -- open import Data.Product | |
| 635 | 15 open import Function as F hiding (const) |
| 16 open import Relation.Binary | |
| 17 open import Relation.Binary.PropositionalEquality | |
| 18 open import Relation.Nullary | |
| 19 open import logic | |
| 933 | 20 open import Data.Unit hiding ( _≟_ ) -- ; _≤?_ ; _≤_) |
| 635 | 21 open import Relation.Binary.Definitions |
| 22 | |
| 23 record AtomicNat : Set where | |
| 24 field | |
| 714 | 25 ptr : ℕ -- memory pointer ( unique id of DataGear ) |
| 635 | 26 value : ℕ |
| 27 | |
| 713 | 28 init-AtomicNat : AtomicNat |
| 714 | 29 init-AtomicNat = record { ptr = 0 ; value = 0 } |
| 713 | 30 |
| 709 | 31 -- |
| 32 -- single process implemenation | |
| 33 -- | |
| 34 | |
| 710 | 35 f_set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t |
| 36 f_set a v next = next record a { value = v } | |
| 635 | 37 |
| 709 | 38 -- |
| 711 | 39 -- Coda Gear |
| 709 | 40 -- |
| 635 | 41 |
| 636 | 42 data Code : Set where |
| 949 | 43 CC_nop : Code |
| 636 | 44 |
| 709 | 45 -- |
| 713 | 46 -- all possible arguments in -APIs |
| 709 | 47 -- |
| 713 | 48 record AtomicNat-API : Set where |
| 636 | 49 field |
| 709 | 50 next : Code |
| 711 | 51 fail : Code |
| 709 | 52 value : ℕ |
| 53 impl : AtomicNat | |
| 54 | |
| 713 | 55 data Error : Set where |
| 56 E_panic : Error | |
| 57 E_cas_fail : Error | |
| 58 | |
| 711 | 59 -- |
| 60 -- Data Gear | |
| 61 -- | |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
62 -- waiting / pointer / available |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
63 -- |
| 949 | 64 |
| 709 | 65 data Data : Set where |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
66 -- D_AtomicNat : AtomicNat → ℕ → Data |
| 949 | 67 CD_AtomicNat : AtomicNat → Data |
| 710 | 68 |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
69 -- data API : Set where |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
70 -- A_AtomicNat : AtomicNat-API → API |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
71 -- A_Phil : Phil-API → API |
| 710 | 72 |
| 709 | 73 |
| 74 record Context : Set where | |
| 75 field | |
| 76 next : Code | |
| 77 fail : Code | |
| 711 | 78 |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
79 -- -API list (frame in Gears Agda ) --- a Data of API |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
80 -- api : List API |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
81 -- c_Phil-API : Maybe Phil-API |
| 949 | 82 -- c_Phil-API : ? |
| 83 -- c_AtomicNat-API : AtomicNat-API | |
| 711 | 84 |
| 710 | 85 mbase : ℕ |
| 949 | 86 -- memory : ? |
| 709 | 87 error : Data |
| 88 fail_next : Code | |
| 89 | |
| 710 | 90 -- |
| 91 -- second level stub | |
| 92 -- | |
| 712 | 93 AtomicInt_cas_stub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t |
| 949 | 94 AtomicInt_cas_stub {_} {t} c next = ? |
| 709 | 95 |
| 96 | |
| 711 | 97 code_table : {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t |
| 949 | 98 code_table = ? |
| 636 | 99 |
| 709 | 100 step : {n : Level} {t : Set n} → List Context → (List Context → t) → t |
| 708 | 101 step {n} {t} [] next0 = next0 [] |
| 716 | 102 step {n} {t} (p ∷ ps) next0 = code_table (Context.next p) p ( λ code np → next0 (update-context ps np ++ ( record np { next = code } ∷ [] ))) where |
| 103 update-context : List Context → Context → List Context | |
| 104 update-context [] _ = [] | |
| 949 | 105 update-context (c1 ∷ t) np = ? -- record c1 { memory = Context.memory np ; mbase = Context.mbase np } ∷ t |
| 708 | 106 |
| 713 | 107 init-context : Context |
| 108 init-context = record { | |
| 949 | 109 next = CC_nop |
| 110 ; fail = CC_nop | |
| 111 -- ; c_Phil-API = ? | |
| 112 -- ; c_AtomicNat-API = record { next = CC_nop ; fail = CC_nop ; value = 0 ; impl = init-AtomicNat } | |
| 713 | 113 ; mbase = 0 |
| 949 | 114 -- ; memory = ? |
| 115 ; error = ? | |
| 116 ; fail_next = CC_nop | |
| 713 | 117 } |
| 118 | |
| 718 | 119 alloc-data : {n : Level} {t : Set n} → ( c : Context ) → ( Context → ℕ → t ) → t |
| 120 alloc-data {n} {t} c next = next record c { mbase = suc ( Context.mbase c ) } mnext where | |
| 121 mnext = suc ( Context.mbase c ) | |
| 122 | |
| 123 new-data : {n : Level} {t : Set n} → ( c : Context ) → (ℕ → Data ) → ( Context → ℕ → t ) → t | |
| 949 | 124 new-data c x next = alloc-data c $ λ c1 n → ? -- insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n ) |
| 718 | 125 |
|
720
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
126 init-AtomicNat0 : {n : Level} {t : Set n} → Context → ( Context → ℕ → t ) → t |
| 949 | 127 init-AtomicNat0 c1 next = ? |
| 128 | |
| 129 add< : { i : ℕ } (j : ℕ ) → i < suc i + j | |
| 130 add< {i} j = begin | |
| 131 suc i ≤⟨ m≤m+n (suc i) j ⟩ | |
| 132 suc i + j ∎ where open ≤-Reasoning | |
| 133 | |
| 134 nat-<> : { x y : ℕ } → x < y → y < x → ⊥ | |
| 135 nat-<> {x} {y} x<y y<x with <-cmp x y | |
| 136 ... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x ) | |
| 137 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x ) | |
| 138 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<y ) | |
|
720
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
139 |
| 949 | 140 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ |
| 141 nat-≤> {x} {y} x≤y y<x with <-cmp x y | |
| 142 ... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x ) | |
| 143 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x ) | |
| 144 ... | tri> ¬a ¬b c = ? | |
|
720
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
145 |
| 949 | 146 |
| 147 nat-<≡ : { x : ℕ } → x < x → ⊥ | |
| 148 nat-<≡ {x} x<x with <-cmp x x | |
| 149 ... | tri< a ¬b ¬c = ⊥-elim ( ¬c x<x ) | |
| 150 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c x<x ) | |
| 151 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<x ) | |
| 718 | 152 |
| 949 | 153 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ |
| 154 nat-≡< refl lt = nat-<≡ lt | |
| 155 | |
| 156 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ | |
| 157 lemma3 refl () | |
| 158 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ | |
| 159 lemma5 {i} {j} i<1 j<i with <-cmp j i | |
| 160 ... | tri< a ¬b ¬c = ⊥-elim ( ¬c ? ) | |
| 161 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a j<i ) | |
| 162 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a j<i ) | |
| 718 | 163 |
| 949 | 164 ¬x<x : {x : ℕ} → ¬ (x < x) |
| 165 ¬x<x x<x = ? | |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
166 |
| 949 | 167 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) |
| 168 → (r : Index) → (p : Invraiant r) | |
| 169 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t | |
| 170 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) | |
| 171 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) | |
| 172 ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where | |
| 173 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t | |
| 174 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) | |
| 175 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) | |
| 176 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt | |
| 177 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) | |
| 178 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) | |
| 708 | 179 |
| 180 -- loop exexution | |
| 181 | |
| 182 -- concurrnt execution | |
| 183 | |
| 184 -- state db ( binary tree of processes ) | |
| 185 | |
| 722 | 186 -- depth first execution |
| 708 | 187 |
| 188 -- verify temporal logic poroerries | |
| 636 | 189 |
| 190 | |
| 191 |