Mercurial > hg > Members > Moririn

changeset 718:93ec11846a27

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 16 May 2022 09:27:13 +0900
parents 52938e8a54a2
children 3e93bcfc879e
files ModelChecking.agda hoareBinaryTree.agda
diffstat 2 files changed, 58 insertions(+), 63 deletions(-) [+]
line wrap: on
line diff
--- a/ModelChecking.agda	Wed May 11 09:56:11 2022 +0900
+++ b/ModelChecking.agda	Mon May 16 09:27:13 2022 +0900
@@ -122,13 +122,6 @@
       error :     Data
       fail_next :      Code
 
-alloc-data : {n : Level} {t : Set n} → ( c : Context ) → ( Context → ℕ → t ) → t
-alloc-data {n} {t} c next = next record c { mbase = mnext } mnext  where
-     mnext = suc ( Context.mbase c )
-
-new-data : {n : Level} {t : Set n} → ( c : Context ) → (ℕ → Data ) → ( Context → ℕ → t ) → t
-new-data  c x next  = alloc-data c $ λ c1 n → insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n )
-
 --
 -- second level stub
 --
@@ -191,8 +184,6 @@
 code_table C_pickup_lfork = Phil_pickup_rfork_sub
 code_table C_eating = Phil_eating_sub
 
-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 (Context.next p) p ( λ code np → next0 (update-context ps np ++ ( record np { next = code } ∷ [] )))  where
@@ -212,6 +203,44 @@
     ; fail_next = C_nop
   }
 
+alloc-data : {n : Level} {t : Set n} → ( c : Context ) → ( Context → ℕ → t ) → t
+alloc-data {n} {t} c next = next record c { mbase =  suc ( Context.mbase c ) } mnext  where
+     mnext = suc ( Context.mbase c )
+
+new-data : {n : Level} {t : Set n} → ( c : Context ) → (ℕ → Data ) → ( Context → ℕ → t ) → t
+new-data  c x next  = alloc-data c $ λ c1 n → insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n )
+
+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 }
+
+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
+
+test211 : test21 ≡ ⟪ 2 , node 1 (D_AtomicNat record { ptr = 1 ; value = 0 }) leaf leaf  ⟫
+test211 = refl
+
+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 
+
+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 }
+
 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
@@ -220,11 +249,6 @@
     c1 [] =  init-context
     c1 (c2 ∷ ct) =  c2
 
-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
@@ -250,36 +274,8 @@
 tail1 (just x) = tail x
 tail1 nothing = nothing
 
-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 }
-
-test21 : ℕ ∧ (List (bt Data))
-test21 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
- $ λ c n → find-loop n (Context.memory c) (Context.memory c ∷ [])   $ λ t st → ⟪ n , st  ⟫  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
-
-test22 : ℕ ∧ (Maybe (List (bt Data)))
-test22 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
- $ λ c n → find n (Context.memory c) (Context.memory c ∷ []) (λ t st → find n t st (λ t st → ⟪ 1 , tail st ⟫) (λ t st → ⟪ 2 , just st ⟫))  $ λ t st → ⟪ 0 , tail st ⟫  where
-    a : ℕ → AtomicNat
-    a ptr = record { ptr = ptr ; value = 0 }
-
-test23 : ℕ ∧ (Maybe ((bt Data)))
-test23 = find n test01-tree (test01-tree ∷ []) (λ t st → find n t st (λ t st → ⟪ 1 , b (tail st) ⟫) (λ t st → ⟪ 2 , b ((just st)) ⟫))  $ λ t st → ⟪ 0 , b (tail st) ⟫  where
-    n = 2
-    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
+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
--- a/hoareBinaryTree.agda	Wed May 11 09:56:11 2022 +0900
+++ b/hoareBinaryTree.agda	Mon May 16 09:27:13 2022 +0900
@@ -56,7 +56,6 @@
 find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
            → (next : (tree1 : bt A) → (stack : List (bt A)) → t)
            → (exit : (tree1 : bt A) → (stack : List (bt A)) → t) → t
-find key _ (leaf ∷ st) _ exit = exit leaf []
 find key leaf st _ exit = exit leaf st 
 find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
 find key n st _ exit | tri≈ ¬a refl ¬c = exit n st 
@@ -97,8 +96,8 @@
 
 insertTest1 = insertTree leaf 1 1 (λ x → x )
 insertTest2 = insertTree insertTest1 2 1 (λ x → x )
-insertTest3 = insertTree insertTest2 3 2 (λ x → x )
-insertTest4 = insertTree insertTest3 2 2 (λ x → x ) -- this is wrong
+insertTest3 = insertTree insertTest2 3 3 (λ x → x )
+insertTest4 = insertTree insertTest3 1 4 (λ x → x ) -- this is wrong
 
 updateTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (empty : bt A → t ) → (next : A → bt A  → t ) → t
 updateTree {_} {_} {A} {t} tree key value empty next = find-loop key tree ( tree ∷ [] )
@@ -260,22 +259,22 @@
 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁
 
 
-record FindCond {n  : Level} {A : Set n} (C : ℕ → bt A → Set n)   : Set (Level.suc n) where
-   field
-      c1 : {key key₁ : ℕ}  {v1 : A } { tree tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key < key₁  → C key tree
-      c2 : {key key₁ : ℕ}  {v1 : A } { tree tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key > key₁  → C key tree₁
-
-
-findP0 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
-           →  {C : ℕ → bt A → Set n} → C key tree → FindCond C
-           → (next : (tree1 : bt A) → (stack : List (bt A)) → C key tree1 → bt-depth tree1 < bt-depth tree   → t )
-           → (exit : (tree1 : bt A) → (stack : List (bt A)) → C key tree1 
-                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
-findP0 key leaf st Pre _ _ exit = exit leaf st Pre (case1 refl)
-findP0 key (node key₁ v1 tree tree₁) st Pre _ next exit with <-cmp key key₁
-findP0 key n st Pre e _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
-findP0 {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre e next _ | tri< a ¬b ¬c = next tree (tree ∷ st) (FindCond.c1 e Pre a) depth-1< 
-findP0 key n@(node key₁ v1 tree tree₁) st Pre e next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) (FindCond.c2 e Pre c) depth-2<
+-- record FindCond {n  : Level} {A : Set n} (C : ℕ → bt A → Set n)   : Set (Level.suc n) where
+--    field
+--       c1 : {key key₁ : ℕ}  {v1 : A } { tree tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key < key₁  → C key tree
+--       c2 : {key key₁ : ℕ}  {v1 : A } { tree tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key > key₁  → C key tree₁
+-- 
+-- 
+-- findP0 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
+--            →  {C : ℕ → bt A → Set n} → C key tree → FindCond C
+--            → (next : (tree1 : bt A) → (stack : List (bt A)) → C key tree1 → bt-depth tree1 < bt-depth tree   → t )
+--            → (exit : (tree1 : bt A) → (stack : List (bt A)) → C key tree1 
+--                  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
+-- findP0 key leaf st Pre _ _ exit = exit leaf st Pre (case1 refl)
+-- findP0 key (node key₁ v1 tree tree₁) st Pre _ next exit with <-cmp key key₁
+-- findP0 key n st Pre e _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
+-- findP0 {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre e next _ | tri< a ¬b ¬c = next tree (tree ∷ st) (FindCond.c1 e Pre a) depth-1< 
+-- findP0 key n@(node key₁ v1 tree tree₁) st Pre e next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) (FindCond.c2 e Pre c) depth-2<
 
 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
            →  treeInvariant tree ∧ stackInvariant key tree tree0 stack