|
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
|
|
|
68 code_table C_set = ?
|
|
|
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
|
