--- a/ModelChecking.agda	Mon May 16 17:55:19 2022 +0900
+++ b/ModelChecking.agda	Sun May 22 19:07:20 2022 +0900
@@ -94,6 +94,8 @@
 --
 -- Data Gear
 --
+--      waiting / pointer / available
+--
 data Data : Set where
    -- D_AtomicNat :  AtomicNat → ℕ → Data
    D_AtomicNat :  AtomicNat → Data
@@ -140,12 +142,11 @@
     ... | tri> ¬a ¬b _  = next (AtomicNat-API.fail api) c
     f_cas a bt    = next ( Context.fail c ) c       -- type error / panic
 
-
+-- putdown_rfork : Phil → (? → t) → t
+-- putdown_rfork p next = goto p->lfork->cas( 0 , putdown_lfork, putdown_lfork ) , next
 
--- putdown_rfork p next = f_set (Phil.right p) 0 ( λ f → putdown_lfork record p { right = f } next )
---               goto p->cas( 0 , putdown_lfork )
 Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
-Phil_putdown_rfork_sub c next = next C_cas_int record c { 
+Phil_putdown_rfork_sub c next = next C_cas_int record c {
     c_AtomicNat-API = record { impl = Phil.right phil ; value =  0 ; fail = C_putdown_lfork ; next = C_putdown_lfork } }  where
     phil : Phil
     phil = Phil-API.impl ( Context.c_Phil-API c )
@@ -228,89 +229,31 @@
     a : ℕ → AtomicNat
     a ptr = record { ptr = ptr ; value = 0 }
 
-init-Phil-1 : (ps : List Context) → (left right : AtomicNat ) → List Context
-init-Phil-1 ps left right = new-data (c1 ps) ( λ ptr → D_Phil (p ptr) )  $ λ c ptr → record c { c_Phil-API = record { next = C_thinking ; impl = p ptr }} ∷ ps where
-    p : ℕ → Phil
-    p ptr = record  init-Phil { ptr = ptr ; left = left ; right = right }  
-    c1 :  List Context → Context
-    c1 [] =  init-context
-    c1 (c2 ∷ ct) =  c2
-
-test-j0 : {n : Level} {t : Set n} → Context → (Context → AtomicNat → t) → t
-test-j0 c next = init-AtomicNat1 c next
-
-test-j2 : AtomicNat  
-test-j2 = test-j0 init-context (λ c f → f )
-
-test-i1 : Context → Context 
-test-i1 c = init-AtomicNat1 c $ λ c f → c
-
-test-i0 : Context
-test-i0 = test-i1 init-context
-
-test-i2 : Context
-test-i2 = test-i1 test-i0
-
-test20 : bt (Data)
-test20 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
- $ λ c n → Context.memory c
-
--- infinite loop
-test21 : bt (Data)
-test21 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
- $ λ c n → insertTree ( Context.memory c)  2 (D_AtomicNat record { ptr = 2 ; value = 0 }) $ λ t → t   
-
--- Ok
-test212  : bt Data
-test212 = insertTree   (node 1 (D_AtomicNat record { ptr = 1 ; value = 0 }) leaf leaf  ) 2 (D_AtomicNat record { ptr = 2 ; value = 0 })
-     $ λ t → t 
-
-open _∧_
-
-test213 : bt Data
-test213 = insertTree (test20)  2 (D_AtomicNat record { ptr = 2 ; value = 0 }) $ λ t → t
+init-Phil-1 : (c1 : Context) → Context
+init-Phil-1 c1 = record c1 { memory = mem2 $ mem1 $ mem ; mbase = n + 3 } where
+   n : ℕ
+   n = Context.mbase c1
+   left  = record { ptr = suc n ; value = 0}
+   right = record { ptr = suc (suc n) ; value = 0}
+   mem : bt Data
+   mem = insertTree ( Context.memory c1) (suc n) (D_AtomicNat left)
+      $ λ t →  t
+   mem1 : bt Data → bt Data
+   mem1 t = insertTree t (suc (suc n)) (D_AtomicNat right )
+      $ λ t →  t
+   mem2 : bt Data → bt Data
+   mem2 t = insertTree t (n + 3) (D_Phil record { ptr = n + 3 ; left = left ; right = right })  
+      $ λ t →  t
+     
+test-i0 : bt Data
+test-i0 =  Context.memory (init-Phil-1 init-context)
 
-test2 : List Context 
-test2 = init-AtomicNat1 init-context $  λ c left → alloc-data c
- $ λ c n → insertTree (Context.memory c) n  (D_AtomicNat (a n))
- $ λ bt → record c { memory = bt } ∷ [] where
-    a : ℕ → AtomicNat
-    a ptr = record { ptr = ptr ; value = 0 }
-
-test-newdata : bt Data
-test-newdata = new-data  init-context ( λ ptr → D_AtomicNat (a ptr) ) $ λ c n → Context.memory c where
-    a : ℕ → AtomicNat
-    a ptr = record { ptr = ptr ; value = 0 }
-
-test0 : List Context 
-test0 = init-AtomicNat1 init-context $ λ c left → c ∷ []
+make-phil : ℕ → Context
+make-phil zero = init-context
+make-phil (suc n) = init-Phil-1 ( make-phil n )
 
-test01 : bt Data 
-test01  = alloc-data init-context  $ λ c1 n → insertTree (Context.memory c1) n (D_AtomicNat (a n)) ( λ bt → next1 bt record c1 { memory = bt } n ) where
-    a : ℕ → AtomicNat
-    a ptr = record { ptr = ptr ; value = 0 }
-    next1 :  bt Data → Context  → ℕ → bt Data
-    next1 t c1 n = t
-
-test01-tree : bt Data
-test01-tree = node 1 (D_AtomicNat record { ptr = 1 ; value = 0 } ) leaf leaf
-
-test01-assert : test01-tree ≡ test01
-test01-assert = refl
-
-tail1 :  Maybe (List (bt Data)) →  Maybe (List (bt Data)) 
-tail1 (just x) = tail x
-tail1 nothing = nothing
-
-test22 : Context 
-test22 = init-AtomicNat1 init-context $ λ c left → init-AtomicNat1 c $ λ c1 right → c1
-
-test : List Context 
-test = init-AtomicNat1 init-context $ λ c left → init-AtomicNat1 c $ λ c1 right → init-Phil-1 (c1 ∷ []) left right
-
-test1 : List Context 
-test1 = init-AtomicNat1 init-context $ λ c left → init-AtomicNat1 c $ λ c1 right → step (init-Phil-1 (c1 ∷ []) left right) (λ ps → ps )
-
+test-i5 : bt Data
+test-i5 =  Context.memory (make-phil 5)
 
 -- loop exexution