--- a/Paper/master_paper.out	Fri Jan 20 13:40:03 2023 +0900
+++ b/Paper/master_paper.out	Fri Jan 20 15:20:31 2023 +0900
@@ -26,9 +26,12 @@
 \BOOKMARK [1][]{section.6.3}{\376\377\0006\000.\0003\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}% 25
 \BOOKMARK [1][]{section.6.4}{\376\377\0006\000.\0004\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}% 26
 \BOOKMARK [2][]{subsection.6.4.1}{\376\377\0006\000.\0004\000.\0001\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}{section.6.4}% 27
-\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\116\312\137\214\060\156\134\125\147\033}{}% 28
-\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 29
-\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 30
-\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 31
-\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}{}% 32
-\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}% 33
+\BOOKMARK [2][]{subsection.6.4.2}{\376\377\0006\000.\0004\000.\0002\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}{section.6.4}% 28
+\BOOKMARK [2][]{subsection.6.4.3}{\376\377\0006\000.\0004\000.\0003\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}{section.6.4}% 29
+\BOOKMARK [2][]{subsection.6.4.4}{\376\377\0006\000.\0004\000.\0004\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}{section.6.4}% 30
+\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\116\312\137\214\060\156\134\125\147\033}{}% 31
+\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 32
+\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 33
+\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 34
+\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}{}% 35
+\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}% 36

Binary file Paper/master_paper.pdf has changed

--- a/Paper/tex/dpp_impl.tex	Fri Jan 20 13:40:03 2023 +0900
+++ b/Paper/tex/dpp_impl.tex	Fri Jan 20 15:20:31 2023 +0900
@@ -100,3 +100,82 @@
 
 思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている．
 
+\subsection{Gears Agda によるDPPの検証}
+
+これまでの実装は一般的なDPPの実装であったため、
+Code / Data Gear の実装であった。
+ここからは、モデル検査を行うため、Meta Data Gear の定義をし、
+それの操作を行う Meta Code Gear の実装を行っていく。
+
+以下がMeta Code Gear の定義になる
+
+% ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける
+
+この Meta Data Gear の説明をすると、
+
+metadataは状態の分岐数を持っておくnum-brunchがある。
+
+MetaEnv はもとの DataGear を保持するDG(Data Gearの省略)
+meta に 前述したmetadataを持っており、
+他には、deadlockしているかのフラグである deadlock 、
+最後の2つは後述する際に必要になる。
+そのstate が step 実行済みなのかのフラグであるis-step、
+そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている。
+
+MetaEnv2 は1つのstate である MetaEnv の Listを meta で持てる。
+加えて今まで実行していた Data Gear  を DG で持てる。
+
+deadlockの検出方法として、状態の分岐数を保存するnum-brunchをmetadataに持つようにした。
+
+そしてnum-brunchの値が1であるということは、それ以上の状態に移動することができないとして、この状態をdead lockであると定義した。
+
+以下のソースコードがdead-lockを検知する関数となる
+
+複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て
+deadlockのフラグを立ち上げている。
+
+% judge-dead-lock-pのソースコードを貼り付ける
+
+ここから前述した通り、State Listを作成する。
+
+そのまま実行するだけでは無限に実行されるのみで停止しないと思われる。
+しかし、分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる。
+存在していた場合はそれを追加せず、存在しなかった場合にのみ State を追加する。
+
+Agdaには2つの record が等しい場合の分岐など存在しないため、
+以下のソースコードのようにrecordの中身を一つづつ一致しているか確認する。
+
+これで、
+まだ分岐を見ていない1つのStateの分岐を確かめる。
+発生した分岐を step 実行させる。
+step実行して作成された state が State Listに存在していないかを確かめる。
+これを繰り返すことで State Listを作る。
+State List に存在している全ての state の分岐を見たということは、
+出現するStateを全て網羅することができたと言える。
+
+あとは State List を dead lock の検査を行う Meta Code Gear に与えるとどの state が dead lockしているかを検証することができる
+
+\subsection{Gears Agda による live lockの検証方法について}
+live lockとは、状態が変動しているが、その状態はループしており、実行が進んでいないことを指す。
+
+DPPにて例を上げると、(上の哲学者のフローだと) dead lock が発生するため、フローを変更したとする。それは以下のような動作を追加する。
+「右手にフォークを持っているが、左手のフォークがすでに取られている場合に右手のフォークを即座に置いて固定時間待つ」
+とする。これで解決すると思われるが、全員が同時に食事をしようとした場合、右手のフォークを取ったり置いたりを永遠に繰り返すことになる。
+これを live lock という
+
+つまり、この状態を検知するなら、そのstateが持っているhistoryまで考慮する必要がある。つまり、今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い。
+
+history がloopしていた際に、誰もeathingしていない場合を live lock していると定義する。
+
+今回のはDPPであるためEatingが挙げられているが、他の実装であれば、どのコマンドが実行されるのが正常な動きなのかを決める。それがloop中に存在いしているかを見れば live lock を検知できる。
+
+
+\subsection{Gears Agda でのモデル検査の評価}
+
+SPINで行ったDPPのモデル検査に比べると、Gears Agdaの方が制約が多いため難解に思える。しかし、Gears Agda ではプログラムの実装も含んでいる。
+
+さらに、Gears Agda での実装をしたあとのモデル検査を行う際の Meta Code Gear の流れは変化しないため、比較的容易であると言える。
+
+加えて、Gears Agda は CbC へコンパイルされ、高速に実行されることを踏まえると、いかに Gears Agda が検証に向いたプログラムであるか理解できる。
+
+% この評価の話はまとめでしたほうがいいかもね？