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 

data Code : Set  where
   C_set : Code
   C_putdown_rfork : Code 
   C_putdown_lfork : Code 
   C_thinking : Code 
   C_pickup_rfork : Code 
   C_pickup_lfork : Code 
   C_eating : Code 

record Process : Set  where
   field
      phil : Phils
      next_code : Code 

putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )

putdown_lfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
putdown_lfork_stub p next = putdown_lfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )

code_table :  {n : Level} {t : Set n} → Code → Process → ( Process → t) → t
code_table C_set  = {!!}
code_table C_putdown_rfork = putdown_rfork_stub
code_table C_putdown_lfork = putdown_lfork_stub
code_table C_thinking = {!!}
code_table C_pickup_rfork = {!!}
code_table C_pickup_lfork = {!!}
code_table C_eating = {!!}

open Process

step : {n : Level} {t : Set n} → List Process → (List Process → t) → t
step {n} {t} [] next0 = next0 []
step {n} {t} (p ∷ ps) next0 = code_table (next_code p) p ( λ np → next0 (ps ++ ( np ∷ [] ) )) 

test : List Process
test = step ( record { phil = record { pid = 1 ; left = record { value = 1 }  ; right = record { value = 1 }  } ; next_code = C_putdown_rfork } ∷ [] ) ( λ ps → ps )

test1 : List Process
test1 = step ( record { phil = record { pid = 1 ; left = record { value = 1 }  ; right = record { value = 1 }  } ; next_code = C_putdown_rfork } ∷ [] )
  $ λ ps → step ps $ λ ps → ps

-- loop exexution

-- concurrnt execution

-- state db ( binary tree of processes )

-- depth first ececution

-- verify temporal logic poroerries