--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ModelChecking.agda	Sun Nov 14 14:55:22 2021 +0900
@@ -0,0 +1,49 @@
+module ModelChecking where
+
+open import Level renaming (zero to Z ; suc to succ)
+
+open import Data.Nat hiding (compare)
+open import Data.Nat.Properties as NatProp
+open import Data.Maybe
+-- open import Data.Maybe.Properties
+open import Data.Empty
+open import Data.List
+open import Data.Product
+open import Function as F hiding (const)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+open import logic
+open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
+open import Relation.Binary.Definitions
+
+record AtomicNat : Set where
+   field
+      value : ℕ
+
+set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t
+set a v next = next record { value = v }
+
+record Phils  : Set  where
+   field 
+      pid : ℕ
+      left right : AtomicNat
+
+putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
+putdown_rfork p next = set (Phils.right p) 0 ( λ f → next record p { right = f } )
+
+putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
+putdown_lfork p next = set (Phils.left p) 0 ( λ f → next record p { left = f } )
+
+thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
+thinking p next = next p 
+
+pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
+pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → next record p { right = f } )
+
+pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
+pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } )
+
+eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
+eating p next = next  p 
+