--- a/Paper/tex/dpp_impl.tex	Fri Jan 20 15:20:31 2023 +0900
+++ b/Paper/tex/dpp_impl.tex	Sat Jan 21 17:57:20 2023 +0900
@@ -107,14 +107,13 @@
 ここからは、モデル検査を行うため、Meta Data Gear の定義をし、
 それの操作を行う Meta Code Gear の実装を行っていく。
 
-以下がMeta Code Gear の定義になる
+以下\coderef{dpp-mdg}がMeta Code Gear の定義になる
 
 % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける
+\lstinputlisting[caption=Gears Agdaでの DPP モデル検査を行うための Meta Data Gear の定義, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced}
 
 この Meta Data Gear の説明をすると、
-
 metadataは状態の分岐数を持っておくnum-brunchがある。
-
 MetaEnv はもとの DataGear を保持するDG(Data Gearの省略)
 meta に 前述したmetadataを持っており、
 他には、deadlockしているかのフラグである deadlock 、
@@ -129,12 +128,14 @@
 
 そしてnum-brunchの値が1であるということは、それ以上の状態に移動することができないとして、この状態をdead lockであると定義した。
 
-以下のソースコードがdead-lockを検知する関数となる
+以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる
 
 複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て
 deadlockのフラグを立ち上げている。
 
 % judge-dead-lock-pのソースコードを貼り付ける
+\lstinputlisting[caption=DPP での dead lock を検知する Meta Code Gear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced}
+% こいつはmetaEnv2を受け取れるように変えないと行けない
 
 ここから前述した通り、State Listを作成する。
 
@@ -143,10 +144,24 @@
 存在していた場合はそれを追加せず、存在しなかった場合にのみ State を追加する。
 
 Agdaには2つの record が等しい場合の分岐など存在しないため、
-以下のソースコードのようにrecordの中身を一つづつ一致しているか確認する。
+\coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つづつ一致しているか確認する。
+こちらはそのまま掲載すると長いので、実際のコードに手を加えて省略している。実際のコードは付録にて参照できる。
+
+\lstinputlisting[caption=重複しているstateを除外する Meta Code Gear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced}
+% 手を加えているので詳細は付録を参照するように促す
+
+MetaEnv2 を受け取ってその中身の state を比較するが、そこまで展開する必要がある。
+ loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている。
 
-これで、
-まだ分岐を見ていない1つのStateの分岐を確かめる。
+更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し、次のstateの一致を探索するように記述されている。
+
+実際にstateの一致を見ているのは22行目のeq-env関数で、一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている
+
+State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている。
+その値が一致している場合には別の値を見て、一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。
+他の値である、lhandやrhandなども同じように記述している。
+
+これらにて、まだ分岐を見ていない1つのStateの分岐を確かめる。
 発生した分岐を step 実行させる。
 step実行して作成された state が State Listに存在していないかを確かめる。
 これを繰り返すことで State Listを作る。