# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651921267 -32400
# Node ID 8f8f136f21622975bd46173966660514cc445b7d
# Parent  75da5f6de47ede65492e730faf98d2dccb09c198
insertTree have some bug

diff -r 75da5f6de47e -r 8f8f136f2162 ModelChecking.agda
--- a/ModelChecking.agda	Fri May 06 10:11:31 2022 +0900
+++ b/ModelChecking.agda	Sat May 07 20:01:07 2022 +0900
@@ -97,12 +97,14 @@
 -- Data Gear
 --
 data Data : Set where
+   -- D_AtomicNat :  AtomicNat → ℕ → Data
    D_AtomicNat :  AtomicNat → Data
    D_Phil :      Phil → Data
    D_Error :      Error → Data
 
-   -- A_AtomicNat :  AtomicNat-API → Data
-   -- A_Phil :      Phil-API → Data
+-- data API : Set where
+--    A_AtomicNat :  AtomicNat-API → API
+--    A_Phil :      Phil-API → API
 
 open import hoareBinaryTree
 
@@ -111,7 +113,9 @@
       next :      Code 
       fail :      Code
 
-      --  -API list (frame in Gears Agda )
+      --  -API list (frame in Gears Agda )  --- a Data of API
+      -- api : List API
+      -- c_Phil-API :     Maybe Phil-API
       c_Phil-API :     Phil-API
       c_AtomicNat-API : AtomicNat-API
 
@@ -140,7 +144,7 @@
     f_cas : AtomicNat → (old : ℕ ) → Data  → bt Data  → t
     f_cas a old (D_AtomicNat now) bt with <-cmp old ( AtomicNat.value now )
     ... | tri≈ ¬a b ¬c  = next (AtomicNat-API.fail api) ( record c { memory = bt ; c_AtomicNat-API = record api { impl = a } }  ) -- update memory
-    ... | tri< a₁ ¬b ¬c = next (AtomicNat-API.fail api) c
+    ... | tri< a₁ ¬b ¬c = next (AtomicNat-API.fail api) c   --- cleaer API
     ... | tri> ¬a ¬b _  = next (AtomicNat-API.fail api) c
     f_cas a old _ bt    = next ( Context.fail c ) c       -- type error
 
@@ -211,17 +215,39 @@
     c1 [] =  init-context
     c1 (c2 ∷ ct) =  c2
 
-init-AtomicNat-n :  {n : Level} {t : Set n} → Context  → ( Context →  AtomicNat → t ) → t
-init-AtomicNat-n c1  next = new-data c1  ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 (a ptr) where
+init-AtomicNat1 :  {n : Level} {t : Set n} → Context  → ( Context →  AtomicNat → t ) → t
+init-AtomicNat1 c1  next = new-data c1  ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 (a ptr) 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 }
 
-test : List Context 
-test = init-AtomicNat-n init-context $ λ c left → init-AtomicNat-n c $ λ c1 right → step (init-Phil-1 (c1 ∷ []) left right) (λ ps → ps )
+test0 : List Context 
+test0 = init-AtomicNat1 init-context $ λ c left → c ∷ []
+
+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 }
 
--- test1 : List Context
--- test1 = step {!!}
---   $ λ ps → step ps $ λ ps → ps
+test21 : List (bt Data )
+test21 = init-AtomicNat1 init-context $  λ c left → alloc-data c
+ $ λ c n → find-loop n (Context.memory c) ( (Context.memory c) ∷ [] ) $ λ t st → st where
+    a : ℕ → AtomicNat
+    a ptr = record { ptr = ptr ; value = 0 }
+
+
+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 )
+
 
 -- loop exexution