\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の実装}

DPP の記述の主要部分を示し，説明する．

\lstinputlisting[caption= Gears Agdaでの DPP の 哲学者の状態 , label=agda-dpp-state, lastline=7]{src/agda-dpp-impl.agda.replaced}

\lstinputlisting[caption= Gears Agdaでの DPP の プロセス , label=agda-dpp-process, firstline=9, lastline=16]{src/agda-dpp-impl.agda.replaced}

\lstinputlisting[caption= Gears Agdaでの DPP の Data Gear , label=agda-dpp-dg, firstline=17, lastline=21]{src/agda-dpp-impl.agda.replaced}

Code \ref{agda-dpp-state}は
前述した哲学者の状態を書き記して，哲学者が今行おうとしている動作を網羅している．

Code \ref{agda-dpp-process}は
哲学者一人ずつの環境を持っている．
pid はその哲学者がどこに座っているかの識別子で，
right / left hand はフォークを手に持っているかを格納している．
next-code は次に行う動作を格納している．

Code \ref{agda-dpp-dg} が Data Gear になる．
phは前もって定義した一人の哲学者のプロセスの List になる．
List になっている理由は，哲学者が複数人いるためである．
そのため実行時にListから一人ずつ取り出して実行をしていく．

tableはテーブルに置いてあるフォークの状態のことで，
pid が1の人の右側にあるフォークが List の最初にあり，
pid が1の人の左側にあるフォーク，すなわち pid が2の人の右側にあるフォークが
その次の List に格納されていくようになっている．
また，自然数の List になっているが，
その場所のフォークがテーブルの上にある場合は自然数の0が，
誰かが所持している場合はその人の pid が格納されるようになっている．

\lstinputlisting[caption= Gears Agdaでの DPP の Data Gear のinit, label=agda-dpp-init, firstline=23, lastline=30]{src/agda-dpp-impl.agda.replaced}

Code \ref{agda-dpp-init}が入力から Data Gear を作成する Code Gear になる．
ここでは哲学者の人数を自然数で受け取り，人数分の List Phi と table を一つづつ作成し env を作成している．
また，最初の哲学者の状態は思考することであるため，next-code には C\_thinking を格納している．

\lstinputlisting[caption= Gears Agdaでの DPP の step 実行, label=agda-dpp-step, firstline=31, lastline=37]{src/agda-dpp-impl.agda.replaced}

Agda では並列実行を行うことができない．そのため step 単位の実行を一つづつ行うことで
並列実行をしていることとする．

この際に Env にある List Phi の中身を展開しながら一つづつ行動を処理していく．

\lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced}

Code \ref{agda-dpp-lfork}が step 実行をした際に哲学者が左側のフォークを取る記述になる．

左側のフォークを取る際には table の index は pid の次の値になっている．
図 \ref{fig:DPP} を見ると直感的に理解ができる．

最後の哲学者は一番最初のフォークを参照する必要がある．
フォークの状態を確認し，値が0である場合はフォークがテーブルの上にあるので
それを自分の pid に書き換え left-hand を true に書き換えてフォークを手に持つ
フォークの状態が0以外，すなわち他の哲学者がその場所のフォークを取得している場合は
状態を変化させずに処理を続ける．
このように左のフォークを取る記述をした．

右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る．
比較するべき table の List と哲学者のListは一致しているため，put\_lfork のように最後の哲学者が
最初のフォークを参照することもない．

似たような形で哲学者がフォークを置く putdown-l/rfork を実装した．

思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている．