\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 で検出したい．

\section{SPINによるモデル検査}% 内容にそぐわない場合は使わない

SPIN(Simple Promela INterpreter) とは一般的にモデル検査に使用されるツールである。Promera(Process Meta Language) によって記述されたコードを元にプログラムが取る状態を網羅し、モデル検査を行うことができる。

今回 Gears Agda でのモデル検査と比較するために、SPINでのDPPプログラムのモデル検査に必要なコードの一部を\coderef{spin-dpp}に載せる。

\lstinputlisting[caption= SPINにてDPPをモデル検査する際のコードの一部 , label=code:spin-dpp]{src/dpp-verif/spin.pml}

コードを簡単に説明する。哲学者がThinkの状態から食事をしようとしだした際の状態の変化が4行目と5行目になっている。
forkの状態を配列で管理している。0 である状態が誰もそのforkを持っていない状態である。ここでは、5人目の人が右手にあるフォークを取ろうとした際に配列の最初を取ることが5行目に記述されている。

左手のフォークを取る動作も同じように記述する。
SPINではこのコードを元にプログラムが取りうる状態全てを網羅し、モデル検査を行うことができる。

\figref{DPP-model}はこのPromelaから作成された状態遷移図になる。
SPINではコードからプログラムの状態遷移図を出力することができる他、プログラムのstep実行など幅広くモデル検査を行うことができる。

\begin{figure}[htpb]
    \begin{center}
     \scalebox{0.6}{\includegraphics{fig/dpp-model.pdf}}
    \end{center}
    \caption{SPINにて作成した状態遷移図}
    \label{fig:DPP-model}
\end{figure}