--- a/Paper/tex/dpp_impl.tex	Sat Jan 21 20:47:38 2023 +0900
+++ b/Paper/tex/dpp_impl.tex	Sun Jan 22 21:20:59 2023 +0900
@@ -1,39 +1,4 @@
-\section{Dining Philosophers Problem}
-今回はモデル検査を行う対象として Dining Philosophers Problem （以下DPP）
-を用いることとした．
-DPP とは資源共有問題であり，モデル検査をする際に挙げられる代表的な問題
-である．
-
-DPPのストーリーを図 \ref{fig:DPP} に示している． 
-
-\begin{figure}[htpb]
-    \begin{center}
-     \scalebox{0.5}{\includegraphics{fig/Dining.pdf}}
-    \end{center}
-    \caption{メタ計算を可視化した CodeGear と DataGear}
-    \label{fig:DPP}
-\end{figure}   
-
-したがって，哲学者は以下のようなフローを独立して並列に繰り返し実行することとなる．
-
-\begin{enumerate}
-    \item しばらくの間思考を行う
-    \item 食事をするために右のフォークを取る
-    \item 右のフォークを取ったら，次は左のフォークを取る
-    \item 両方のフォークを取ったら，しばらく食事をする
-    \item 思考に戻るために左手に持っているフォークをテーブルに置く
-    \item 左手のフォークを置いたあとは右のフォークをテーブルに置く
-\end{enumerate}
-
-この際，すべての哲学者が同時に右のフォークを取った場合のことを考える．
-すべての哲学者はフォークを持っている．次に哲学者は左のフォークを取ろうと
-する．しかしフォークは哲学者の人数と同じ数だけ存在しているため，
-テーブルの上にフォークはすでにひとつも存在しない．
-すべての哲学者は左のフォークを取ろうとするが
-誰も右のフォークを置くことがないため，すべての哲学者の動作がこの状態で止まる．（dead lock）
-これが起こることを Gears Agda で検出したい．
-
-\subsection{Gears Agda によるDPPの実装}
+\section{Gears Agda によるDPPの実装}
 
 DPP の記述の主要部分を示し，説明する．
 
@@ -100,7 +65,7 @@
 
 思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている．
 
-\subsection{Gears Agda によるDPPの検証}
+\section{Gears Agda によるDPPの検証}
 
 これまでの実装は一般的なDPPの実装であったため、
 Code / Data Gear の実装であった。
@@ -171,7 +136,7 @@
 
 あとは State List を dead lock の検査を行う Meta Code Gear に与えるとどの state が dead lockしているかを検証することができる
 
-\subsection{Gears Agda による live lockの検証方法について}
+\section{Gears Agda による live lockの検証方法について}
 live lockとは、状態が変動しているが、その状態はループしており、実行が進んでいないことを指す。
 
 DPPにて例を上げると、(上の哲学者のフローだと) dead lock が発生するため、フローを変更したとする。それは以下のような動作を追加する。
@@ -186,7 +151,7 @@
 今回のはDPPであるためEatingが挙げられているが、他の実装であれば、どのコマンドが実行されるのが正常な動きなのかを決める。それがloop中に存在いしているかを見れば live lock を検知できる。
 
 
-\subsection{Gears Agda でのモデル検査の評価}
+\section{Gears Agda でのモデル検査の評価}
 
 SPINで行ったDPPのモデル検査に比べると、Gears Agdaの方が制約が多いため難解に思える。しかし、Gears Agda ではプログラムの実装も含んでいる。