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.Tree.Binary
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
      anid : ℕ
      value : ℕ

--
-- single process implemenation
--

set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t
set a v next = next record a { value = v }

record Phils  : Set  where
   field 
      pid : ℕ
      left right : AtomicNat

pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t

pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → pickup_lfork record p { right = f } next )
pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → eating record p { left = f } next )
eating p next = putdown_rfork p next
putdown_rfork p next = set (Phils.right p) 0 ( λ f → putdown_lfork record p { right = f } next )
putdown_lfork p next = set (Phils.left p) 0 ( λ f → thinking record p { left = f } next )
thinking p next = next p

run : Phils
run = pickup_rfork record { pid = 1 ; left = record { anid = 1 ; value = 0 } ; right = record { anid = 2 ; value = 0 } } $ λ p → p

--
-- goto version
--

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 

--
-- all possible arguments in APIs
--
record AtomicNatAPI : Set where
   field
      next : Code
      value : ℕ
      old : ℕ
      impl : AtomicNat

record PhilsAPI : Set  where
   field 
      next : Code
      impl : Phils

data Data : Set where
   D_Phils : ℕ → Phils → Data
   D_AtomicNat : ℕ → AtomicNat → Data

record Context  : Set  where
   field
      next :      Code 
      fail :      Code
      phil :      PhilsAPI
      atomicNat : AtomicNatAPI
      memory :    Tree Data Data
      error :     Data
      fail_next :      Code

g_set : {n : Level} {t : Set n} → Context  → AtomicNat → ( Code → Context → t ) → t
g_set {_} {t} c a next = f a ( AtomicNatAPI.value api   )
         $ λ a → next ( AtomicNatAPI.next api  ) record c { atomicNat = record api   { impl = a } }   where
    api : AtomicNatAPI
    api = Context.atomicNat c
    f : AtomicNat → ℕ  → ( AtomicNat → t ) → t
    f a n next = next record a { value = n }

g_cas : {n : Level} {t : Set n} → Context  → AtomicNat → ( Code → Context → t ) → t
g_cas {n} {t} c a next = f a ( AtomicNatAPI.old api   )( AtomicNat.value a ) ( AtomicNatAPI.value api   )
         $ λ a → next ( AtomicNatAPI.next api  ) record c { atomicNat = record api   { impl = a } }   where
    api : AtomicNatAPI
    api = Context.atomicNat c
    f : AtomicNat → (old now new : ℕ ) → ( AtomicNat → t ) → t
    f a old now new next1 with <-cmp old now 
    ... | tri≈ ¬a b ¬c = next1 record a { value = new }
    ... | tri< a₁ ¬b ¬c = next ( Context.fail c) c
    ... | tri> ¬a ¬b _ = next ( Context.fail c) c

g_putdown_rfork : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_putdown_rfork c p next = next C_set record c { 
    atomicNat = {!!} }

g_putdown_lfork : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_putdown_lfork c p next = next C_set record c { 
    atomicNat = {!!} }

g_thinking : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_thinking c p next = next C_pickup_rfork c  

g_pickup_rfork : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_pickup_rfork c p next = next C_set record c {
    atomicNat = {!!} }

g_pickup_lfork : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_pickup_lfork c p next = next C_set record c {
    atomicNat = {!!} }

g_eating : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
g_eating c p next =  next C_putdown_rfork c 

set_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
set_stub p next = set {!!} {!!} ( λ ph → next {!!} )

putdown_rfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
putdown_rfork_stub p next = {!!} -- g_putdown_rfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )

putdown_lfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
putdown_lfork_stub p next = {!!} -- g_putdown_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_thinking } )

thinking_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
thinking_stub p next = {!!} -- g_thinking ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_pickup_rfork } )

pickup_rfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
pickup_rfork_stub p next = {!!} -- g_pickup_rfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_pickup_lfork } )

pickup_lfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
pickup_lfork_stub p next = {!!} -- g_pickup_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_eating } )

eating_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
eating_stub p next = {!!} -- g_pickup_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_rfork } )

code_table :  {n : Level} {t : Set n} → Code → Context → ( Context → t) → t
code_table C_set  = set_stub
code_table C_putdown_rfork = putdown_rfork_stub
code_table C_putdown_lfork = putdown_lfork_stub
code_table C_thinking = thinking_stub
code_table C_pickup_rfork = pickup_rfork_stub
code_table C_pickup_lfork = pickup_lfork_stub
code_table C_eating = eating_stub

open Context

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

test : List Context
test = step {!!} ( λ ps → ps )

test1 : List Context
test1 = step {!!}
  $ λ ps → step ps $ λ ps → ps

-- loop exexution

-- concurrnt execution

-- state db ( binary tree of processes )

-- depth first ececution

-- verify temporal logic poroerries