Mercurial > hg > Papers > 2023 > soto-master

changeset 23:016e82a71407

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add slide
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Tue, 07 Feb 2023 02:27:53 +0900
parents b37e4cd69468
children 988528add93f
files DPP/ModelChecking.agda Paper/src/dpp-verif/ModelChecking.agda slide/memo.md slide/slide.md slide/slide.pdf
diffstat 5 files changed, 312 insertions(+), 68 deletions(-) [+]
line wrap: on
line diff
--- a/DPP/ModelChecking.agda	Sun Feb 05 16:35:38 2023 +0900
+++ b/DPP/ModelChecking.agda	Tue Feb 07 02:27:53 2023 +0900
@@ -111,7 +111,7 @@
   init-table-loop zero ind env exit = exit env
   init-table-loop (suc redu) ind env exit = init-table-loop redu (suc ind) record env{
     table = 0 ∷ (table env)
-    ; ph = record {pid = redu ; left-hand = false ; right-hand = false ; next-code = C_thinking } ∷ (ph env) } exit
+    ; ph = record {pid = suc(redu) ; left-hand = false ; right-hand = false ; next-code = C_thinking } ∷ (ph env) } exit
 
 -- eatingも探索範囲に含める
 brute-force-search : {n : Level} {t : Set n} → Env → (exit : List Env → t) → t
@@ -295,6 +295,17 @@
     metal :  List MetaEnv -- 結局探索して1ステップ実行(インターリーディング)するからMetaEnvのList Envがちょうどよい
 open MetaEnv2
 
+
+init-metaenv2  : {n : Level} {t : Set n} → ℕ → (exit : MetaEnv2 → t) → t
+init-metaenv2 n exit = init-table n (λ e → exit (record { DG = (e ∷ []) ∷ [] ; metal = record
+                                                                                           { DG = e ∷ []
+                                                                                           ; meta = record { num-branch = 0 ; wait-list = [] }
+                                                                                           ; deadlock = true
+                                                                                           ; is-done = false
+                                                                                           ; is-step = true
+                                                                                           } ∷ [] }))
+
+
 -- 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
@@ -646,8 +657,8 @@
 test-envl : List Env
 test-envl = test-env1 ∷ test-env1 ∷ []
 
-testhoge : {n : Level} {t : Set n} → (env1 env2 : MetaEnv2) → (exit : MetaEnv2 → t) → t
-testhoge env1 env2 exit = loop-target-metaenv (metal env1) env2 exit where
+exclude-same-env : {n : Level} {t : Set n} → (env1 env2 : MetaEnv2) → (exit : MetaEnv2 → t) → t
+exclude-same-env env1 env2 exit = loop-target-metaenv (metal env1) env2 exit where
   eq-pid : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t) → (loop : Bool → t)  → t
   eq-lhand : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t)  → t
   eq-rhand : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t)  → t
@@ -771,7 +782,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 → exclude-same-env me3 me2  (λ me4 → check-same-env-test me4 (λ me5 → me5)))  (λ e → e) ) ))  (λ e → e)
 
 
 test-dead-lock-meta21 : MetaEnv2
@@ -790,7 +801,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 → exclude-same-env me3 me2  (λ me4 → check-same-env-test me4 (λ me5 → me5)))  (λ e → e) )  ))  (λ e → e)
 
 
 check-and-judge-deadlock : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
@@ -798,15 +809,18 @@
 
 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 (suc n) metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → exclude-same-env me3 metaenv2 (λ me4 → test-dead-lock-meta22 n me4) ) )  (λ e5 → e5)
 
 {-# 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 (λ me2 → step-meta2 me2 (λ me3 → exclude-same-env me3 metaenv2 (λ me4 → test-dead-lock-loop me4) ) ) (λ e → e)
 
 {-# TERMINATING #-}
 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-loop2 metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → exclude-same-env me3 metaenv2 (λ me4 → test-dead-lock-loop2 me4) ) ) (λ e → check-and-judge-deadlock e (λ e1 → e1) )
+
+test-dead-lock-loop3 : ℕ → MetaEnv2
+test-dead-lock-loop3 n = init-metaenv2 n (λ metaenv2 →  test-dead-lock-loop2 metaenv2)
 
 test-step-c2 : List (List Env)
 test-step-c2 = init-brute-force (record {table = 0 ∷ 0 ∷ 0 ∷ []
--- a/Paper/src/dpp-verif/ModelChecking.agda	Sun Feb 05 16:35:38 2023 +0900
+++ b/Paper/src/dpp-verif/ModelChecking.agda	Tue Feb 07 02:27:53 2023 +0900
@@ -805,7 +805,7 @@
 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-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-loop2 metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-loop2 me4) ) ) (λ e → check-and-judge-deadlock e (λ e1 → e1) )
 
 test-step-c2 : List (List Env)
 test-step-c2 = init-brute-force (record {
--- a/slide/memo.md	Sun Feb 05 16:35:38 2023 +0900
+++ b/slide/memo.md	Tue Feb 07 02:27:53 2023 +0900
@@ -1,5 +1,96 @@
-# 
-
 # 目的
 
+そのまま読むかな
 
+# agdaの基本
+たぶんここの説明全部実際のコードでやったほうがいいらしい
+
+# record
+論文にもかいてあるし三段論法を
+取り扱ったほうが見る人も面白いのでは
+
+# CbC
+goto文のやつは消すかな
+
+# normal levelとmetalevel
+ポインタの操作は含まれない
+
+上の方は normal level の実装
+
+下の方が meta level の計算を可視化したもの
+
+例えば、変数がメモリのある番地に存在していれば、
+Meta Data Gear がその番地を持っている。
+(なので Data Gear に wrap されているというイメージ)
+
+Meta Code Gear がそのメモリから取り出して、
+
+普通の Code Gear が実行をするという流れ、
+
+後ろのほうでまた新しく保存したいデータがあれば
+Meta Code Gear が保存して、
+
+最後の Meta Data Gear が新しいデータのメモリ番地を
+持っているという流れになります。
+
+プログラムをする際は上のようにシンプルな実装をするが、
+実際には内部でメタ計算が走っているのが理想ですね
+
+Gears Agda 
+
+# Gears Agda
+
+この矢印tが Gears Agda のミソで、
+
+この定義を見ると、While loop はEnvとCode を受け取ってtを返します。
+
+この While loop を code Gear に
+見立てるなら、次に遷移する関数を指定する必要があります
+
+それがCodeになります。
+なので、Gears Agda では次に受け取る関数を受け取る用にしていて、それがnextになります。
+
+このようにして、CbC の継続という概念を
+矢印tで表現しています。
+
+(CbCのCodeGear はDataGearをうけとってそれを元に実行することはnextがEnvを受け取って実行すること)
+
+(CodeGear の実行終了時に、次の CodeGearに
+DataGearを与えることもnextにEnvを与えていることからわかると思います)
+
+
+<!-- 実行の文を持ってくるんだっけな -->
+
+- with 文
+with文で展開してパターンマッチすることもできる。
+ここでは less than がそれにあたる
+0とvarnを比較して
+false だった場合、trueだった場合をcase文のように
+書ける
+
+- `{-# TERMINATING #-}`
+Agdaが停止性を理解できない場合に、このようにアノテーションすることで停止することを示せます
+
+# loopの接続
+
+reduceがあるため、Agdaは
+
+で、前回のものは最初から構造体（record）に値が格納されている状態から始まっていたので
+proofGearsTermS では、入力が自然数で、recordの定義から検証を行っている
+
+そしてそれを行っているのが最初の関数であるwhileTest'で
+ここでvarnが入力c10と一致し、variが0であることを証明している
+
+次の関数であるversionでは、whileTest'のrecord定義時のConditionから
+
+loop時のconditionを生成しています
+
+- これで Gears Agda にて While Loop を Hoare Logic を使って検証することができた。
+
+# テストと定理証明の違い
+
+# 定理証明とモデル検査の違い
+
+# DPPの実装
+pidは哲学者をindexで管理するために必要
+どの哲学者がどのフォークを取るのか決まっているため
--- a/slide/slide.md	Sun Feb 05 16:35:38 2023 +0900
+++ b/slide/slide.md	Tue Feb 07 02:27:53 2023 +0900
@@ -46,6 +46,7 @@
      text-align: center;
   }
 
+math: mathjax
 ---
 <!-- headingDivider: 1 -->
 
@@ -68,14 +69,6 @@
   - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
 - 本研究では Gears Agda にて定理証明を用いた検証と、モデル検査による検証をする
 
-# CbC について
-- CbCとは当研究室で開発しているC言語の下位言語
-    - 継続呼び出しは引数付き goto 文で表現される
-      - 関数呼び出し時のスタックの操作を行わずjmp命令で次の処理に移動する
-    - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
-- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う
-
-
 # Agda の基本 
 - Agdaとは定理証明支援器であり、関数型言語
 - Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する
@@ -85,7 +78,7 @@
   - 関数名を定義した行よりも後ろの行で実装する
   - = の前で受け取る引数を記述、= の後ろで実装を記述する
 
-
+<!--
 ```
 sample : (A : Set ) → (B : Set ) → Set
 sample a b = b
@@ -110,8 +103,45 @@
 ```
 (env : Env) → varn env
 ```
+-->
+
+# Agda の基本 record
+オブジェクトあるいは構造体
+2つのものが同時に存在すること
+```
+record _∧_ (A B : Set) : Set where
+  field
+    p1 : A
+    p2 : B
+```
+３段論法を示すこともできる
+```
+syllogism : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
+syllogism x a = _∧_.p2 x (_∧_.p1 x a)
+```
+
+# CbC について
+- CbCとは当研究室で開発しているC言語の下位言語
+    - 関数呼び出し時にスタックの操作を行わずjmp命令で次の処理に移動する
+    - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
+- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う
+
+# Normal level と Meta Level を用いた信頼性の向上
+プログラムを記述する際に、メモリ管理、スレッド管理、資源管理などのプログラムの本筋とは別に実装が必要な場合がある。これらの計算をメタ計算と呼ぶ。
+CbC では メタ計算を分離して考える。メタ計算以外を Normal levelとしている。
+- Normal Level の計算
+  - 軽量継続
+  - Code Gear 単位で関数型プログラミングとなる
+  - atomic(Code Gear 自体の実行は割り込まれない)
+- Meta Level の計算
+  - メモリやCPUなどの資源管理、ポインタ操作
+  - Contextによる並列実行。monadに相当するData構造
+  - Hoare Condition と証明
 
 
+# Normal level と Meta Level の対応
+![height:400px](meta-cg-dg.jpg)
+Gears Agdaでは 検証を Meta計算として取り扱う
 
 # Gears Agda の記法
 <!-- Gears Agdaの説明が必要かも -->
@@ -123,7 +153,8 @@
 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
 whileLoop env next with lt 0 (varn env)
 whileLoop env next | false = next env
-whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+whileLoop env next | true = whileLoop 
+  (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 ```
 - tを返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
 - tail call により light weight continuation を定義している
@@ -143,28 +174,20 @@
 - Code Gear 単位で並列実行
 
 
-# Normal level と Meta Level を用いた信頼性の向上
-Normal Level 
-- 軽量継続
-- Code Gear 単位で関数型プログラミングとなる
-- atomic(Code Gear 自体の実行は割り込まれない)
-- ポインタの操作は含まれない
-
-Meta Level 
-- メモリやCPUなどの資源管理, ポインタ操作
-- Hoare Condition と証明
-- Contextによる並列実行
-- monadに相当するData構造
-
-# Normal level と Meta Level の対応
-![height:400px](meta-cg-dg.jpg)
 
 # Gears Agda と Hoare Logic
 <!-- class: slide -->
-C.A.R Hoare, R.W Floyd が考案
-- Pre Condition → Command → Post Condition
+- C.A.R Hoare, R.W Floyd が考案
+- 「プログラムの事前条件(P)が成立しているとき、コマンド(C)を実行して停止すると事後条件(Q)が成り立つ」というもの
+$$ \{P\} C \{Q\} $$
+- 事前条件を Code Gear に入れる前の Meta Gear で検証する。これを Pre Condition とする 
+- Command は Code Gear そのもの
+- 事後条件を Code Gear のあとの Meta Gear で検証する。これを Post Condition とした
+- 今回は、例として While loop の Hoare Logic を用いた検証を行う
 
+<!--
 Gears Agda による Command の例
+
 ```
 {-# TERMINATING #-}
 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
@@ -172,10 +195,45 @@
 whileLoop env next | false = next env
 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 ```
-- `{-# TERMINATING #-}`
-- with 文
+-->
+
+# Gears Agda での while loopの実装
+While Loopの実装は主に以下のDataGearとCodeGearで行った
+```
+record Env  : Set where
+  field
+    varn : ℕ -- これからループする回数
+    vari : ℕ -- 今までループした回数
+open Env
+```
+
+```
+{-# TERMINATING #-}
+whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true =
+    whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+```
+
+# While loopでのInvariantの定義
+
+不変条件としてInvariantを定義した。これを実行しながら証明することでHoare Logic での検証ができる
+```
+-- 初期値として、ループする前はループした回数は0であり
+-- かつループする回数とループする回数は等しい
+((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+```
+```
+-- ループする回数とループした回数を足すと入力したループして欲しい回数と等しい
+(varn env) + (vari env) ≡ c10)
+```
+```
+vari e1 ≡ c10 -- ループした回数は入力したループして欲しい回数と等しい
+```
 
 # Gears Agda の Pre Condition / Post Condition
+ループ実行中の命題は以下のようになる。
 ```
 whileLoopSeg : {l : Level} {t : Set l} → {c10 :  N } → (env : Env) → (varn env + vari env ≡ c10)
    → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) 
@@ -189,7 +247,7 @@
 これは命題なので証明を与えて Pre Condition から Post Condition を導出する必要がある。証明は値として次の CodeGear に渡される
 
 # Loop の接続
-分割したloopを接続するMeta Code Gearを作成する
+loop中のMeta Gearを作成する
 ```
 TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) 
   → {Invraiant : Index → Set } → ( reduce : Index → N) 
@@ -200,7 +258,9 @@
 - IndexはLoop変数
 - Invariantはloop変数の不変条件
 - loopに接続するCode Gearを与える
+  - つまりloopを抜ける際の Code Gear。ここでは next がそれにあたる
 - reduceは停止性を保証する減少列
+  - この減少列のおかげで`{-# TERMINATING #-}`が外せる
 
 これを証明することで検証ができる
 
@@ -218,24 +278,32 @@
     (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 
 ```
 - conversion1はPre Condition をPost Conditionに変換する
-- ⊤
+- ⊤は正しいことを示す論理記号
+
 
-# test との違い
-- test では実数を与えた際の出力が仕様に沿ったものであるかを検証する
-    - コーナーケースを人力で完全に考慮し、testする必要がある
-- 今回の定理証明を用いた証明では実数を必要としない
+# 定理証明とtest との違い
+- test では実値を与えた際の出力が仕様に沿ったものであるかを検証する
+    - コーナーケースを人力で完全に考慮するのは難しい
+- 今回の定理証明を用いた証明では実値を必要としない
     - そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる
 
 # モデル検査と定理証明の違い
 - モデル検査では全ての状態を網羅し、それが仕様を満たしているか検証する
 - 無限にある状態を検証することはできないため、定理証明と比べると完全な検証にならないこともある
-- 定理証明に比べて実装コストが低い<!-- 計算コストは高い -->
+- 定理証明に比べてモデル検査の実装コストは低い
+  - 定理証明の証明は難しい
+  - その代わりモデル検査は計算コストは高い
+- 定理証明では並列実行の検証をするには、状態を全探索しそれらを定理証明することになる
+
+# Gears Agda による モデル検査
+- 定理証明で並列実行の検証をするのは難しいので、モデル検査で検証を行う。
+- 今回は Gears Agda にてモデル検査をすることで、並列実行の検証を行う
+- 題材として、 Dining Philosophers Problem のモデル検査にてdead lockを検知する
 
 # Dining Philosophers Problem
-
 ||哲学者の遷移|
 |---|---|
-|![height:450px](DPP.jpg)|1. 哲学者は思考をしている  <br> 2. 食事をするために右のフォークを取る <br> 3. 次に左のフォークを取る <br> 4. 両方のフォークが取れたら食事をする <br> 5. 思考に戻るために左のフォークを置く <br> 6. 次に右のフォークを置く |
+|![height:450px](DPP.jpg)|制約 <br> - 哲学者と同じ数のフォークが存在する <br> - 両手にフォークを持つと食事できる <br> 哲学者のフロー <br> 1. 哲学者は思考をしている  <br> 2. 食事をするために右のフォークを取る <br> 3. 次に左のフォークを取る <br> 4. 両方のフォークが取れたら食事をする <br> 5. 思考に戻るために左のフォークを置く <br> 6. 次に右のフォークを置く |
 
 # Dining Philosophers Problem の実装
 - DPPはマルチプロセスの同期問題である
@@ -273,7 +341,7 @@
    C_eating : Code
 ```
 
-```
+``` 
 code_table : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t
 code_table C_putdown_rfork = putdown-rfork-c
 code_table C_putdown_lfork = putdown-lfork-c
@@ -302,29 +370,100 @@
 # モデル検査でのデッドロック検知
 - 今回Gears Agdaでのデッドロックの定義として、以下2つを設定した
   - その状態から分岐が作れない
-  - 実行時に状態が一切変化しない
-- これでプログラムが dead Lock しているのか検知するところまではできた
+    - ThinkingやEathingのときに乱数が出るので、その際に分岐するようにしている。それがないということ
+  - step実行時に状態が一切変化しない
+- Gears Agda にて出現する状態を全て網羅する
+  - step 実行を無限に続ける
+  - 一度分岐を確認した状態に対しては flag を立てる
+  - 全ての状態の分岐を確認したら停止し、これを State List とした
+- これで全ての状態に対して dead Lock しているのか検証する
+
+# モデル検査での Meta Data Gear
+以下の Meta Data Gear を定義した
+```
+record metadata : Set where
+  field
+    num-branch : ℕ -- その状態から発生する分岐の数
+    wait-list : List ℕ -- step実行で変化がなかったプロセス
+open metadata
+```
+```
+record MetaEnv : Set where
+  field
+    DG : List Env -- historyを持つためListにしている
+    meta : metadata
+    deadlock : Bool
+    is-done : Bool
+    is-step : Bool
+open MetaEnv
+```
+
+# モデル検査での Meta Data Gear
+```
+record MetaEnv2 : Set where
+  field
+    DG : List (List Env) -- HistoryをもったEnv(状態)を配列として複数持っている。
+    metal :  List MetaEnv
+open MetaEnv2
+```
 
 # モデル検査でのデッドロック検知
-網羅には以下の Meta CodeGear を実装した(一部抜粋)
+網羅には以下の Meta CodeGear を実装した
+```
+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 )
+```
+step実行しても状態が変更しない Meta Code Gear も同じように実装している。
+これで meta データ を定義できるようになった。
+
+
+# モデル検査でのデッドロックの検知
+metaデータから deadlock を検出する Meta Code Gear にて 、モデル検査を Gears Agda にて行えるようになった。
+
 ```
-brute-force-search : {n : Level} {t : Set n} 
-  → Env → (exit : List Env → t) → t
-brute-force-search 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 Env → 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
+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
+  judge-deadlock-p f [] exit = exit f
+  judge-deadlock-p f (metaenv ∷ bs) exit with num-branch (meta metaenv)
+  ... | suc (suc branchnum) = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
+  ... | zero = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
+  ... | suc zero with (DG metaenv )
+  ... | [] = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
+  ... | 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 = true} ∷ []) ) bs exit
 ```
 
+# Gears Agda でのモデル検査の実行
+以下の関数にてモデル検査を行うことができる
+```
+{-# TERMINATING #-}
+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-loop2 me4) ) ) 
+(λ e → check-and-judge-deadlock e (λ e1 → e1) )
+```
+<!-- initから投げるまでにした方がいいかもしれないな -->
+
+- Code Gear を繋げたものでは、Agdaは停止性を理解できないので、`{-# TERMINATING #-}`を使用してちゃんと止まることを記述している。
+  - 今回の DPP の状態は有限であることが予めわかっていたから可能だった
+  - 状態爆発が起こったり無限にある場合は、範囲を制限してモデル検査する方法が用いられる (bounded model checking)
+
 # 今後の研究方針
 - モデル検査
     - 有向グラフからなる有限オートマトンの遷移を全自動探索する
Binary file slide/slide.pdf has changed