Mercurial > hg > Papers > 2023 > soto-master

changeset 13:62d87fdd7775

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add intro
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Tue, 31 Jan 2023 16:31:53 +0900
parents 3aa9d35e93bf
children f52e5fd41f58
files DPP/ModelChecking.agda Paper/master_paper.out Paper/master_paper.pdf Paper/master_paper.tex Paper/tex/abst.tex Paper/tex/intro.tex
diffstat 6 files changed, 52 insertions(+), 135 deletions(-) [+]
line wrap: on
line diff
--- a/DPP/ModelChecking.agda	Sun Jan 29 15:21:21 2023 +0900
+++ b/DPP/ModelChecking.agda	Tue Jan 31 16:31:53 2023 +0900
@@ -136,22 +136,8 @@
       set-state redu origin (false ∷ ss) f b env envl exit | p ∷ ps | C_eating = set-state redu origin ss (f ++ (p ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む
       set-state redu origin (true  ∷ ss) f b env envl exit | p ∷ ps | C_thinking = set-state redu origin ss (f ++ (record p{next-code = C_pickup_rfork} ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む
       set-state redu origin (false ∷ ss) f b env envl exit | p ∷ ps | C_thinking = set-state redu origin ss (f ++ (p ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む
-      set-state redu origin st@(s ∷ ss)     f b env envl exit | p ∷ ps | _ = set-state redu origin st (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
+      set-state redu origin (s ∷ ss)     f b env envl exit | p ∷ ps | _ = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
 
--- eatingも探索範囲に含める
-brute-force-search-1 : {n : Level} {t : Set n} → Env → (exit : List Bool → t) → t
-brute-force-search-1 env exit = make-state-list 1 [] (ph env) env (env ∷ []) exit where
-  make-state-list : {n : Level} {t : Set n} → ℕ → List Bool → List Phi → Env → (List Env) → (exit : List Bool → t) → t
-  make-state-list redu state (x ∷ pl) env envl exit with next-code x
-  ... | C_thinking = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit
-  ... | C_eating = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit
-  ... | _ = make-state-list redu state pl env envl exit
-  make-state-list redu state [] env envl exit = bit-force-search redu [] state env envl exit where
-    bit-force-search : {n : Level} {t : Set n} → ℕ → (f b : List Bool )→ Env → (List Env) → (exit : List Bool → t) → t
-    bit-force-search zero f l env envl exit = exit []
-    bit-force-search (suc redu) f [] env envl exit = exit []
-    bit-force-search (suc redu) f (true ∷ bs) env envl exit = bit-force-search (suc redu) (f ++ (false ∷ [])) bs env envl exit 
-    bit-force-search (suc redu) f (false ∷ bs) env envl exit = exit (f ++ (true ∷ bs)) 
 
 test-search : List Env
 test-search = init-table 3 (λ e0 → brute-force-search e0 (λ e1 → e1))
@@ -295,7 +281,6 @@
     metal :  List MetaEnv -- 結局探索して1ステップ実行(インターリーディング)するからMetaEnvのList Envがちょうどよい
 open MetaEnv2
 
--- this one need
 branch-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t
 branch-deadlock-check metaenv exit = search-brute-force-envll-p [] metaenv exit where
   search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
@@ -305,8 +290,7 @@
   ... | (env ∷ envs) = brute-force-search env (λ e0 → make-brute-force-envl (length e0)  [] metaenv e0 (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit))  where
     make-brute-force-envl : {n : Level} {t : Set n} → ℕ → List MetaEnv → MetaEnv → (state : List Env) → (exit : List MetaEnv → t) → t
     make-brute-force-envl len res xs [] exit = exit res
-    make-brute-force-envl len res xs (x ∷ state) exit =  brute-force-search env (λ e0 → search-brute-force-envll-p (f ++ ( record metaenv{meta = record (meta metaenv){num-branch = (length e0)} } ∷ [])) bs exit )
-    -- make-brute-force-envl len (res ++ (record xs{DG = (x ∷ DG xs); meta = record (meta xs){num-branch = len}} ∷ [])) xs state exit
+    make-brute-force-envl len res xs (x ∷ state) exit = make-brute-force-envl len (res ++ (record xs{DG = (x ∷ DG xs); meta = record (meta xs){num-branch = len}} ∷ [])) xs state exit
 
 data _===_ {n} {A : Set n} :  List A -> List A -> Set n where
           reflection  : {x : List A} -> x === x
@@ -321,7 +305,6 @@
 testhoge _ _ = {!!}
 -}
 
--- this need
 step-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t
 step-deadlock-check metaenvl exit = deadlock-check-p [] metaenvl exit where
   deadlock-check-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
@@ -373,45 +356,6 @@
   ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
   ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit
 
-waitlist-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
-waitlist-deadlock-metaenv meta2 exit = deadlock-check-p [] (metal meta2) (λ e → exit record meta2{metal = e}) where
-  deadlock-check-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
-  deadlock-check-p f [] exit = exit f
-  deadlock-check-p f b@(metaenv ∷ bs) exit with DG metaenv
-  ... | [] = deadlock-check-p f bs exit
-  ... | p0 ∷ envs = step-c p0 (λ e0 → check-wait-process [] (ph p0) e0 ( λ e → deadlock-check-p (f ++ (record metaenv{meta = record (meta metaenv){wait-list = e } } ∷ [])) bs exit) ) where
-    check-wait-process : {n : Level} {t : Set n} → List ℕ → List Phi → (p1 : Env) → (exit : List ℕ → t) → t
-    check-wait-process waitl [] p1 exit = exit waitl
-    check-wait-process waitl (p ∷ ps) p1 exit = hoge11 p (ph p1)  (λ e → check-wait-process (waitl ++ e) ps p1 exit) where
-      hoge11 : {n : Level} {t : Set n} → Phi → List Phi → (exit : List ℕ → t) → t
-      hoge11 p [] exit = exit []
-      hoge11 p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp)
-      hoge11 p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 p p1s exit
-      hoge11 p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 p p1s exit
-      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p)
-      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp)
-      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (pid p ∷ [])
-      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (pid p ∷ [])
-      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (pid p ∷ [])
-      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (pid p ∷ [])
-      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (pid p ∷ [])
-      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (pid p ∷ [])
-      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit []
-
-check-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
-check-deadlock-metaenv meta2 exit = search-brute-force-envll-p [] (metal meta2) (λ e → exit record meta2{metal = e}) where
-  search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
-  search-brute-force-envll-p f [] exit = exit f
-  search-brute-force-envll-p f b@(metaenv ∷ bs) exit with DG metaenv
-  ... | [] = search-brute-force-envll-p f bs exit
-  ... | (env ∷ envs) =  brute-force-search env (λ e0 → search-brute-force-envll-p (f ++ ( record metaenv{meta = record (meta metaenv){num-branch = (length e0)} } ∷ [])) bs exit )
-  {-
-  -- brute-force-search env (λ e0 → make-brute-force-envl (length e0)  [] metaenv e0 (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit))  where
-    make-brute-force-envl : {n : Level} {t : Set n} → ℕ → List MetaEnv → MetaEnv → (state : List Env) → (exit : List MetaEnv → t) → t
-    make-brute-force-envl len res xs [] exit = exit res
-    make-brute-force-envl len res xs (x ∷ state) exit = make-brute-force-envl len (res ++ (record xs{DG = (x ∷ DG xs); meta = record (meta xs){num-branch = len}} ∷ [])) xs state exit
--}
-
 judge-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
 judge-deadlock-metaenv meta2 exit = judge-deadlock-p [] (metal meta2) (λ e → exit record meta2{metal = e} ) where
   judge-deadlock-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
@@ -424,7 +368,7 @@
   ... | p ∷ ps with <-cmp (length (wait-list (meta metaenv))) (length (ph p))
   ... | tri< a ¬b ¬c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
   ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
-  ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = false} ∷ []) ) bs exit
+  ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit
 
 {-
 test-env-deadlock : {n : Level} {t : Set n} → (a b : Env)→ (exit : List MetaEnv → t) → t
@@ -468,14 +412,14 @@
   make-brute-force-envl res (addenv ∷ statel) meta exit = make-brute-force-envl (res ++ ( record meta{DG = addenv ∷ (DG meta); is-done = false; is-step = false} ∷ [])) statel meta exit
 
 
-step-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
-step-meta2 meta2 exit = step-brute-force-p1 [] (metal meta2) (λ envll → exit record meta2{metal = envll}) where
+step-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (next exit : MetaEnv2 → t) → t
+step-meta2 meta2 next1 exit = step-brute-force-p1 [] (metal meta2) (λ envll → next1 record meta2{metal = envll}) (λ e → exit meta2) where
   step-brute-force-p-p : {n : Level} {t : Set n} → (envl : (List Env)) → (exit : (List Env) → t) → t
-  step-brute-force-p1 : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
-  step-brute-force-p1 f [] exit = exit f
-  step-brute-force-p1 f (metaenv ∷ metaenvl) exit with is-step metaenv
-  ... | true =  step-brute-force-p1 (f ++ (metaenv ∷ [])) metaenvl exit
-  ... | false = step-brute-force-p-p (DG metaenv) (λ e0 → step-brute-force-p1 (f ++ (record metaenv{DG = e0; is-step = true} ∷ [])) metaenvl exit)
+  step-brute-force-p1 : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (next exit : List (MetaEnv) → t) → t
+  step-brute-force-p1 f [] next1 exit = next1 f
+  step-brute-force-p1 f (metaenv ∷ metaenvl) next1 exit with is-step metaenv
+  ... | true =  step-brute-force-p1 (f ++ (metaenv ∷ [])) metaenvl next1 exit
+  ... | false = step-brute-force-p-p (DG metaenv) (λ e0 → step-brute-force-p1 (f ++ (record metaenv{DG = e0; is-step = true} ∷ [])) metaenvl next1 exit)
   step-brute-force-p-p [] exit = exit []
   step-brute-force-p-p (x ∷ bs) exit = step-c x (λ e0 → exit (e0 ∷ bs))
 
@@ -513,7 +457,7 @@
   ... | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit)
   check-same-env-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → MetaEnv2 → (exit : MetaEnv2 → t) → t
   check-same-env-p [] [] metae2 exit = exit metae2
-  check-same-env-p f@(x ∷ fs) [] metae2 exit = step-meta2 record metae2{metal = f} (λ me2 → branch-search-meta2 me2 (λ me3 → check-same-env me3 exit) exit )
+  check-same-env-p f@(x ∷ fs) [] metae2 exit = step-meta2 record metae2{metal = f} (λ me2 → branch-search-meta2 me2 (λ me3 → check-same-env me3 exit) exit ) exit 
   check-same-env-p [] bl@(b ∷ bs) metae2 exit with DG b
   ... | [] =  check-same-env-p [] bs metae2 exit
   ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p ([] ++ lme) bl metae2 exit)
@@ -600,20 +544,19 @@
                  ; next-code = C_thinking
                  }  ∷ []
   })
-
 test-env1 : Env
 test-env1 = (record {
-  table = 1 ∷ 0 ∷ 0 ∷ []
+  table = 0 ∷ 0 ∷ 0 ∷ []
   ; ph = record
            { pid = 1
            ; left-hand = false
-           ; right-hand = true
-           ; next-code = C_pickup_lfork
+           ; right-hand = false
+           ; next-code = C_pickup_rfork
            } ∷ record
                  { pid = 2
                  ; left-hand = false
                  ; right-hand = false
-                 ; next-code = C_thinking
+                 ; next-code = C_pickup_rfork
            } ∷ record
                  { pid = 3
                  ; left-hand = false
@@ -626,7 +569,8 @@
 test-metaenv = record
                  { DG = test-env1 ∷ test-env ∷ []
                  ; meta = record { num-branch = zero ; wait-list = [] }
-                 ; deadlock = true ; is-done = false ; is-step = false
+                 ; deadlock = true ; is-done = false ; is-step = true
+
                  }
 
 test-metaenv1 : MetaEnv
@@ -671,7 +615,7 @@
   ... | [] = exit origin
   ... | env1 ∷ envl with DG x
   ... | [] = loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit
-  ... | env2 ∷ history = eq-env origin (ph env1) (ph env2) (λ exit-e → exit record origin{metal = f ++ (record x{is-done = boolor (is-done me) (is-done x) } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit )
+  ... | env2 ∷ history = eq-env origin (ph env1) (ph env2) (λ exit-e → exit record origin{metal = f ++ (record x{is-done = boolor (is-done me) (is-done x); is-step = true } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit )
 
   eq-env origin [] [] exit loop = exit origin -- true
   eq-env origin [] (x ∷ pl2) exit loop = loop false
@@ -771,7 +715,7 @@
                  ; left-hand = false
                  ; right-hand = false
                  ; next-code = C_pickup_rfork
-                 }  ∷ [] } ∷ []) ∷ [] ; metal = [] }) (λ me0 → check-same-env-test me0 (λ me1 → step-meta2 me1 (λ me2 → branch-search-meta2 me2 ( λ me3 → testhoge me3 me2  (λ me4 → check-same-env-test me4 (λ me5 → me5)))  (λ e → e) ) ))  (λ e → e)
+                 }  ∷ [] } ∷ []) ∷ [] ; metal = [] }) (λ me0 → check-same-env-test me0 (λ me1 → step-meta2 me1 (λ me2 → branch-search-meta2 me2 ( λ me3 → testhoge me3 me2  (λ me4 → check-same-env-test me4 (λ me5 → me5)))  (λ e → e) ) (λ e → e) ))  (λ e → e)
 
 
 test-dead-lock-meta21 : MetaEnv2
@@ -790,22 +734,18 @@
                  ; left-hand = false
                  ; right-hand = false
                  ; next-code = C_pickup_rfork
-                 }  ∷ [] } ∷ []) ∷ [] ; metal = [] }) (λ me0 → check-same-env-test me0 (λ me1 → step-meta2 me1 (λ me2 → branch-search-meta2 me2 ( λ me3 → testhoge me3 me2  (λ me4 → check-same-env-test me4 (λ me5 → me5)))  (λ e → e) )  ))  (λ e → e)
+                 }  ∷ [] } ∷ []) ∷ [] ; metal = [] }) (λ me0 → check-same-env-test me0 (λ me1 → step-meta2 me1 (λ me2 → branch-search-meta2 me2 ( λ me3 → testhoge me3 me2  (λ me4 → check-same-env-test me4 (λ me5 → me5)))  (λ e → e) ) (λ e → e) ))  (λ e → e)
 
 
-check-and-judge-deadlock : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
-check-and-judge-deadlock meta2 exit = check-deadlock-metaenv meta2 (λ e0 → waitlist-deadlock-metaenv e0 (λ e → judge-deadlock-metaenv e exit ) )
-
 test-dead-lock-meta22 : ℕ → MetaEnv2 → MetaEnv2
-test-dead-lock-meta22 zero metaenv2 = check-and-judge-deadlock metaenv2 (λ e → e)
-test-dead-lock-meta22 (suc n) metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-meta22 n me4) ) )  (λ e5 → e5)
+test-dead-lock-meta22 zero metaenv2 = metaenv2
+test-dead-lock-meta22 (suc n) metaenv2 = branch-search-meta2 metaenv2 (λ me1 → testhoge me1 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 me2 (λ me4 → test-dead-lock-meta22 n me4) ) (λ e → e)) )  (λ e → e)
 
 {-# TERMINATING #-}
 test-dead-lock-loop : MetaEnv2 → MetaEnv2
-test-dead-lock-loop metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-loop me4) ) ) (λ e → e)
+test-dead-lock-loop metaenv2 = branch-search-meta2 metaenv2 (λ me1 → testhoge me1 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 me2 (λ me4 → test-dead-lock-loop me4) ) (λ e → e)) )  (λ e → e)
 
-test-dead-lock-loop2 : MetaEnv2 → MetaEnv2
-test-dead-lock-loop2 metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-loop me4) ) ) (λ e → check-and-judge-deadlock e (λ e1 → e1) )
+-- test-dead-lock-loop test-metaenv3
 
 test-step-c2 : List (List Env)
 test-step-c2 = init-brute-force (record {
--- a/Paper/master_paper.out	Sun Jan 29 15:21:21 2023 +0900
+++ b/Paper/master_paper.out	Tue Jan 31 16:31:53 2023 +0900
@@ -1,6 +1,6 @@
 %このファイルは日本語文字を含みます.
 \BOOKMARK [0][]{chapter*.3}{\376\377\170\024\172\166\225\242\220\043\212\326\145\207\151\155\176\076}{}% 1
-\BOOKMARK [0][]{chapter.1}{\376\377\173\054\0001\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\137\142\137\017\142\113\154\325}{}% 2
+\BOOKMARK [0][]{chapter.1}{\376\377\173\054\0001\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\060\327\060\355\060\260\060\351\060\340\060\156\151\034\212\074}{}% 2
 \BOOKMARK [0][]{chapter.2}{\376\377\173\054\0002\172\340\000\040\000C\000o\000n\000t\000i\000n\000u\000a\000t\000i\000o\000n\000\040\000b\000a\000s\000e\000d\000\040\000C}{}% 3
 \BOOKMARK [1][]{section.2.1}{\376\377\0002\000.\0001\000\040\000C\000o\000d\000e\000\040\000G\000e\000a\000r\000\040\000/\000\040\000D\000a\000t\000a\000\040\000G\000e\000a\000r}{chapter.2}% 4
 \BOOKMARK [1][]{section.2.2}{\376\377\0002\000.\0002\000\040\000C\000b\000C\000\040\060\150\000\040\000C\212\000\212\236\060\156\220\125\060\104}{chapter.2}% 5
@@ -24,15 +24,10 @@
 \BOOKMARK [1][]{section.6.1}{\376\377\0006\000.\0001\000\040\060\342\060\307\060\353\151\034\147\373\060\150\060\157}{chapter.6}% 23
 \BOOKMARK [1][]{section.6.2}{\376\377\0006\000.\0002\000\040\000D\000i\000n\000i\000n\000g\000\040\000P\000h\000i\000l\000o\000s\000o\000p\000h\000e\000r\000s\000\040\000P\000r\000o\000b\000l\000e\000m}{chapter.6}% 24
 \BOOKMARK [1][]{section.6.3}{\376\377\0006\000.\0003\000\040\000S\000P\000I\000N\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{chapter.6}% 25
-\BOOKMARK [1][]{section.6.4}{\376\377\0006\000.\0004\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373\060\156\155\101\060\214}{chapter.6}% 26
-\BOOKMARK [1][]{section.6.5}{\376\377\0006\000.\0005\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\133\237\210\305}{chapter.6}% 27
-\BOOKMARK [1][]{section.6.6}{\376\377\0006\000.\0006\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\151\034\212\074}{chapter.6}% 28
-\BOOKMARK [1][]{section.6.7}{\376\377\0006\000.\0007\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000\040\000l\000i\000v\000e\000\040\000l\000o\000c\000k\060\156\151\034\212\074\145\271\154\325\060\153\060\144\060\104\060\146}{chapter.6}% 29
-\BOOKMARK [1][]{section.6.8}{\376\377\0006\000.\0008\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\060\342\060\307\060\353\151\034\147\373\060\156\212\125\117\241}{chapter.6}% 30
-\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\060\176\060\150\060\201\060\150\116\312\137\214\060\156\134\125\147\033}{}% 31
-\BOOKMARK [1][]{section.7.1}{\376\377\0007\000.\0001\000\040\116\312\137\214\060\156\212\262\230\114}{chapter.7}% 32
-\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 33
-\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 34
-\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 35
-\BOOKMARK [0][]{appendix.A}{\376\377\116\330\000\040\223\062\000A\000\040\000\040\170\024\172\166\117\032\151\155\176\076}{}% 36
-\BOOKMARK [1][]{section.A.1}{\376\377\000A\000-\0001\000\040\170\024\172\166\117\032\166\172\210\150\214\307\145\231}{appendix.A}% 37
+\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\060\176\060\150\060\201\060\150\116\312\137\214\060\156\134\125\147\033}{}% 26
+\BOOKMARK [1][]{section.7.1}{\376\377\0007\000.\0001\000\040\116\312\137\214\060\156\212\262\230\114}{chapter.7}% 27
+\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 28
+\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 29
+\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 30
+\BOOKMARK [0][]{appendix.A}{\376\377\116\330\000\040\223\062\000A\000\040\000\040\170\024\172\166\117\032\151\155\176\076}{}% 31
+\BOOKMARK [1][]{section.A.1}{\376\377\000A\000-\0001\000\040\170\024\172\166\117\032\166\172\210\150\214\307\145\231}{appendix.A}% 32
Binary file Paper/master_paper.pdf has changed
--- a/Paper/master_paper.tex	Sun Jan 29 15:21:21 2023 +0900
+++ b/Paper/master_paper.tex	Tue Jan 31 16:31:53 2023 +0900
@@ -129,7 +129,7 @@
 \input{tex/tree_desc.tex}% Gears Agda における木構造の設計
 
 \input{tex/spin_dpp.tex}% Gears Agda の記法　loopのやつやる
-\input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
+% \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
 
 \chapter{まとめと今後の展望}
 本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた。そこで、定理証明については Invariant を用いて定理証明を行った。モデル検査については Gears Agda にて dead lock を検知できるようになった。
--- a/Paper/tex/abst.tex	Sun Jan 29 15:21:21 2023 +0900
+++ b/Paper/tex/abst.tex	Tue Jan 31 16:31:53 2023 +0900
@@ -12,28 +12,18 @@
 そのため，他のプログラミング言語と比べて検証に適しているGears Agdaを使用する．
 Gears Agdaとは当研究室で開発している Continuation based C (CbC) の概念を
 取り入れた記法で記述された Agdaのことである．
-通常のプログラミング言語では関数を実行する際にメインルーチンからサブルーチンに遷移する．
-この際メインルーチンで使用していた変数などの環境はスタックされ，サブルーチンが終了し，
-メインルーチンに戻る際にスタックしていた環境に戻す流れとなる．
-CbCの場合はサブルーチンコールの際にアセンブラでいう jmp命令 により関数遷移を行うことができ，
-環境をスタックに保持しない．
-したがって関数の実行では暗黙な環境が存在せず，関数は受け取った引数のみを使用する．
-この関数の単位を Code Gear と呼び，Code Gearの引数を Data Gear と呼んでいる．
 
 定理証明によるプログラムの検証は一般的に難易度が高いが，
-これにより検証を Code Gear 単位に分割することができ，比較的容易に検証を行えるようになっている．\cite{ryokka-sigos}
+Gears Agda では検証をプログラム単位に分割することができ，比較的容易に検証を行えるようになっている．\cite{ryokka-sigos}
 
-しかし，定理証明では並行処理の検証は困難である。加えて、往々にして定理証明による検証自体が複雑である．
+先行研究では implies を用いて Hoare Logic での定理証明を行っていた。
+しかしそれでは記述が長く、かつ複雑になってしまっていた。
+そこで今回は Invariant というプログラムの不変条件を新たに取り入れた。これを検証しながら実行を行うことで、Hoare Logic を用いた定理証明を比較的簡単に行えるようになった。
+
+また，定理証明では並行処理の検証は困難である。
 そのため，もう一つの代表的な検証手法であるモデル検査を Gears Agda にて行えるようにした．
-CbCの継続の概念はモデル検査とも相性がよい．
-CbCが末尾関数呼び出しであるため Code Gear をそのまま
-モデルの edge として定義することができるためである．
- 
-定理証明支援機である Agda でモデル検査をするのは実行時間が掛かる点が困難である．
-しかし，Gears Agda で 書いたプログラムをCbCに変換する事ができれば，
-高速かつ Gears Agda で証明されたモデル検査器を動作させることができる．
 
-これらのことから，本紙では Gears Agda の定理証明とモデル検査での検証手法について述べる
+これらのことから，本論文では Gears Agda の定理証明とモデル検査での検証手法について述べる
 
 \chapter*{Abstract}
 We are developing Gears OS, a scalable and reliable OS, using the Continuation based C (CbC) language.
--- a/Paper/tex/intro.tex	Sun Jan 29 15:21:21 2023 +0900
+++ b/Paper/tex/intro.tex	Tue Jan 31 16:31:53 2023 +0900
@@ -1,37 +1,29 @@
-\chapter{Gears Agda での形式手法}
+\chapter{Gears Agda でのプログラムの検証}
 
-開発手法の一つとして，形式手法というものがある．
-形式手法とはプログラムの仕様を形式化，つまり数学的な記述を行い，
-書いたプログラムがそれを満たしているか検証を行う手法である．
-代表的な形式の検証手法として，定理証明やモデル検査が挙げられる．
+OSやアプリケーションの信頼性の向上は重要である
+信頼性を向上するための手段として、プログラムを検証する事が挙げられる。
 
-形式手法で開発したプログラムは数学的に正しいことが証明されている，
-そのため高い安全性が必要とされる鉄道や電力などのインフラ分野に使用されている．
-しかし、一見完璧な手法であるように思えるが欠点として，膨大なコストを要する．
-シンプルな実装であれば仕様の形式化が容易に行えるが，そうであれば形式手法を使用せずとも良いとなる．
 
+しかし、検証には仕様の形式化とその検証には膨大なコストを要する．
 そのため，他のプログラミング言語と比べて検証に適しているGears Agdaを使用する．
 Gears Agdaとは当研究室で開発している Continuation based C (CbC) の概念を
 取り入れた記法で記述された Agdaのことである．
+
 通常のプログラミング言語では関数を実行する際にメインルーチンからサブルーチンに遷移する．
 この際メインルーチンで使用していた変数などの環境はスタックされ，サブルーチンが終了し，
 メインルーチンに戻る際にスタックしていた環境に戻す流れとなる．
-CbCの場合はサブルーチンコールの際にアセンブラでいう jmp命令 により関数遷移を行うことができ，
-環境をスタックに保持しない．
+CbCの場合はサブルーチンコールの際にアセンブラでいう jmp命令 により関数遷移を行うことができ，環境をスタックに保持しない．
 したがって関数の実行では暗黙な環境が存在せず，関数は受け取った引数のみを使用する．
 この関数の単位を Code Gear と呼び，Code Gearの引数を Data Gear と呼んでいる．
 
-定理証明によるプログラムの検証は一般的に難易度が高いが，
-これにより検証を Code Gear 単位に分割することができ，比較的容易に検証を行えるようになっている．\cite{ryokka-sigos}
+これにより検証を Code Gear 単位に分割することができ，比較的容易に検証を行えるようになっている．
 
-しかし，定理証明では並行処理の検証は困難である。加えて、往々にして定理証明による検証自体が複雑である．
-そのため，もう一つの代表的な検証手法であるモデル検査を Gears Agda にて行えるようにした．
+先行研究では、Gears Agda での並列実行の検証について課題が残っていた。
+並列実行の検証を定理証明で行うには、考慮する状態の数が膨大になり困難である。
+そのため、Gears Agda でモデル検査を行うことでこの課題に対応する。
+
 CbCの継続の概念はモデル検査とも相性がよい．
 CbCが末尾関数呼び出しであるため Code Gear をそのまま
 モデルの edge として定義することができるためである．
 
-定理証明支援機である Agda でモデル検査をするのは実行時間が掛かる点が困難である．
-しかし，Gears Agda で 書いたプログラムをCbCに変換する事ができれば，
-高速かつ Gears Agda で証明されたモデル検査器を動作させることができる．
-
-これらのことから，本紙では Gears Agda の定理証明とモデル検査での検証手法について述べる
+これらのことから、本論文では、Gears Agda での定理証明とモデル検査について述べる