--- a/ModelChecking.agda	Mon May 16 09:27:13 2022 +0900
+++ b/ModelChecking.agda	Mon May 16 10:48:49 2022 +0900
@@ -215,24 +215,24 @@
     a : ℕ → AtomicNat
     a ptr = record { ptr = ptr ; value = 0 }
 
-test21 : ℕ ∧ (bt (Data))
+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 → ⟪ n , Context.memory c  ⟫  where
-    a : ℕ → AtomicNat
-    a ptr = record { ptr = ptr ; value = 0 }
-    b : Maybe (List (bt Data)) → Maybe (bt Data)
-    b (just x) = head x
-    b nothing = nothing
-    d : bt Data → Maybe Data
-    d leaf = nothing
-    d (node key value t t₁) = just value
+ $ λ c n → insertTree ( Context.memory c)  2 (D_AtomicNat record { ptr = 2 ; value = 0 }) $ λ t → t   
 
-test211 : test21 ≡ ⟪ 2 , node 1 (D_AtomicNat record { ptr = 1 ; value = 0 }) leaf leaf  ⟫
-test211 = refl
-
+-- 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 
+     $ λ t → t 
+
+open _∧_
+
+test213 : bt Data
+test213 = insertTree (test20)  2 (D_AtomicNat record { ptr = 2 ; value = 0 }) $ λ t → t
 
 test2 : List Context 
 test2 = init-AtomicNat1 init-context $  λ c left → alloc-data c