Mercurial > hg > Gears > GearsAgda
annotate ModelChecking.agda @ 664:1f702351fd1f
findP done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Nov 2021 08:24:21 +0900 |
| parents | e30dcd03c07f |
| children | 4761b08c4bd6 |
| rev | line source |
|---|---|
| 635 | 1 module ModelChecking where |
| 2 | |
| 3 open import Level renaming (zero to Z ; suc to succ) | |
| 4 | |
| 5 open import Data.Nat hiding (compare) | |
| 6 open import Data.Nat.Properties as NatProp | |
| 7 open import Data.Maybe | |
| 8 -- open import Data.Maybe.Properties | |
| 9 open import Data.Empty | |
| 10 open import Data.List | |
| 11 open import Data.Product | |
| 12 open import Function as F hiding (const) | |
| 13 open import Relation.Binary | |
| 14 open import Relation.Binary.PropositionalEquality | |
| 15 open import Relation.Nullary | |
| 16 open import logic | |
| 17 open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) | |
| 18 open import Relation.Binary.Definitions | |
| 19 | |
| 20 record AtomicNat : Set where | |
| 21 field | |
| 22 value : ℕ | |
| 23 | |
| 24 set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t | |
| 25 set a v next = next record { value = v } | |
| 26 | |
| 27 record Phils : Set where | |
| 28 field | |
| 29 pid : ℕ | |
| 30 left right : AtomicNat | |
| 31 | |
| 32 putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 33 putdown_rfork p next = set (Phils.right p) 0 ( λ f → next record p { right = f } ) | |
| 34 | |
| 35 putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 36 putdown_lfork p next = set (Phils.left p) 0 ( λ f → next record p { left = f } ) | |
| 37 | |
| 38 thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 39 thinking p next = next p | |
| 40 | |
| 41 pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 42 pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → next record p { right = f } ) | |
| 43 | |
| 44 pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 45 pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } ) | |
| 46 | |
| 47 eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 48 eating p next = next p | |
| 49 | |
| 636 | 50 data Code : Set where |
| 51 C_set : Code | |
| 52 C_putdown_rfork : Code | |
| 53 C_putdown_lfork : Code | |
| 54 C_thinking : Code | |
| 55 C_pickup_rfork : Code | |
| 56 C_pickup_lfork : Code | |
| 57 C_eating : Code | |
| 58 | |
| 59 record Process : Set where | |
| 60 field | |
| 61 phil : Phils | |
| 62 next : Code | |
| 63 | |
| 64 putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t | |
| 65 putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next = C_putdown_lfork } ) | |
| 66 | |
| 67 code_table : {n : Level} {t : Set n} → Code → Process → ( Process → t) → t | |
|
637
e30dcd03c07f
stack invariant in findP
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
636
diff
changeset
|
68 code_table C_set = {!!} |
| 636 | 69 code_table C_putdown_rfork = putdown_rfork_stub |
| 70 code_table C_putdown_lfork = {!!} | |
| 71 code_table C_thinking = {!!} | |
| 72 code_table C_pickup_rfork = {!!} | |
| 73 code_table C_pickup_lfork = {!!} | |
| 74 code_table C_eating = {!!} | |
| 75 | |
| 76 step : {n : Level} {t : Set n} → List Process → (List Process → t) → t | |
| 77 step = {!!} | |
| 78 | |
| 79 | |
| 80 | |
| 81 |