--- a/ModelChecking.agda	Tue Dec 07 18:28:06 2021 +0900
+++ b/ModelChecking.agda	Tue Apr 19 19:39:29 2022 +0900
@@ -59,23 +59,45 @@
 record Process : Set  where
    field
       phil : Phils
-      next : Code 
+      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 = C_putdown_lfork } )
+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 = {!!}
+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 = {!!}
+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
 
 
 
-