|
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
|
