--- a/paper/chapter4.tex	Thu Feb 14 15:43:13 2008 +0900
+++ b/paper/chapter4.tex	Thu Feb 14 22:10:16 2008 +0900
@@ -59,7 +59,7 @@
 また、他の検証ツールとの比較を行う。
 \\
 
-プロセスが5〜６個の場合の結果は表\ref{tab:ltl_tableau}
+プロセスが5〜６個の場合の結果は表\ref{tab:ltl_tableau}のようになった。
 
 \begin{table}
     \centering
@@ -72,4 +72,121 @@
     \label{tab:ltl_tableau}
 \end{table}
 
+検証用のコードセグメントを組み込んでのタブロー展開は、
+組み込む前のものと比べて実行時間はあまり変わっていない。
 
+また、プロセスが5個の場合の実行結果は以下のようになっている。
+
+\begin{center}
+\begin{itembox}[l]{プロセスが5個の場合の実行結果}
+\begin{verbatim}
+	省略
+found 38984
+no more branch 38984
+All done count 38984
+	memory_header 117030
+	memcmp_count 2383597
+	memory_body 1120
+	restore_count 467820
+	restore_size 6237600
+	range_count 15
+	range_size 200
+[]~p is not valid.
+\end{verbatim}
+\end{itembox}
+\end{center}
+
+この実行結果より、プロセスが5個の場合の状態数が38,984個であることがわかる。
+また、\verb|[]~p is not valid.|という結果からデッドロックが検知されたことがわかる。
+これは、命題pを「デッドロックが起きる」と定義し、
+\verb|[]~p|つまり決してpが起きないことを検査した結果、
+pが起きてしまったことを表している。
+
+\subsection{SPINによるDining Philosophers Problemの検証}
+SPINでDining Philosophers Problemの検証を行う。
+
+まず、Dining Philosophers Problemをモデル化したプログラムをPROMELAで記述する。
+そして、それからSPINによって検証器であるpan.cを生成しそれをコンパイル、実行する。
+
+ソースコード\ref{src:dpp.prm}にPROMELAによるDining Philosophers Problemのモデルの
+記述を示す。
+
+\lstinputlisting[caption=PROMELAによるDining Philosophers Problemの記述,label=src:dpp.prm]{src/dpp.prm}
+
+
+プロセスが5〜6個の場合の結果は表\ref{tab:spin_dpp}のようになった。
+
+\begin{table}
+    \centering
+    \begin{tabular}{|r|r|r|} \hline
+	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
+	5 & 94 & 0.008 \\ \hline
+	6 & 212 & 0.01 \\ \hline
+    \end{tabular}
+    \caption{SPINによるDining Philosophers Problemの検証結果}
+    \label{tab:spin_dpp}
+\end{table}
+
+CbCでの検証と比べて、状態数が少ない。
+そのため、実行にかかる時間も高速であった。
+これは、PROMELAでのDining Philosophers Problemを抽象化して記述しているため
+状態数が少ない。
+
+CbCの場合は、実際に実行可能なプログラムを逐次実行していくことで状態を変化
+させているため、モデル化した記述よりも状態数が多くなっていると考えられる。
+
+また、プロセスが5個の場合のSPINで生成された検証器の実行結果は以下のようになった。
+
+\begin{center}
+\begin{itembox}[l]{SPINのプロセスが5個の場合の実行結果}
+\begin{verbatim}
+pan: assertion violated 0 (at depth 44)
+(Spin Version 4.2.5 -- 2 April 2005)
+        + Partial Order Reduction
+
+Full statespace search for:
+	never claim             - (none specified)
+	assertion violations    +
+	acceptance   cycles     - (not selected)
+	invalid end states      +
+
+State-vector 44 byte, depth reached 44, errors: 1
+	46 states, stored
+	16 states, matched
+	62 transitions (= stored+matched)
+	  0 atomic steps
+hash conflicts: 0 (resolved)
+
+2.622   memory usage (Mbyte)
+\end{verbatim}
+\end{itembox}
+\end{center}
+
+\verb|assertion violated 0 (at depth 56)|がデッドロック検知を報告している部分である。
+\verb|212 states, stored|が生成されたユニークな状態の数である。
+
+\subsection{Java PathFinderによるDining Philosophers Problemの検証}
+JPFには、例題としてDiningPhil.javaが用意されているのでこれを用いる。
+
+使い方としては、\verb|javac|によりJavaのバイトコードを生成して、
+それを\verb|jpf|で実行するだけである。
+
+JPFの実行結果は、状態数が出ないため実行時間のみ比較する。
+表\ref{tab:jpf_dpp}に実行結果を示す。
+
+\begin{table}
+    \centering
+    \begin{tabular}{|r|r|} \hline
+	プロセス数 & 実行時間(秒) \\ \hline
+	5 & 3.98 \\ \hline
+	6 & 7.33 \\ \hline
+    \end{tabular}
+    \caption{JPFによるDining Philosophers Problemの検証結果}
+    \label{tab:jpf_dpp}
+\end{table}
+
+JPFもCbCと同様に実際に実行可能なバイトコードに対して検証が可能である。
+プロセス数に対する実行時間を比較するとCbCの方が速い。
+
+
+%%%end%%%

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/dpp.prm	Thu Feb 14 22:10:16 2008 +0900
@@ -0,0 +1,28 @@
+#define N 5
+
+byte fork[N];
+
+proctype philosopher(byte num)
+{
+    do
+    ::  atomic { fork[num] == 0 -> fork[num] = 1 };
+	atomic { fork[(num+1)%N] == 0 -> fork[(num+1)%N] = 1 };
+	atomic { fork[(num+1)%N] = 0; fork[num] = 0 };
+    od
+}
+
+proctype watchdog()
+{
+    do :: timeout -> assert(0) od
+}
+
+init
+{
+    fork[0] = 0; fork[1] = 0; fork[2] = 0; fork[3] = 0; fork[4] = 0;
+    run philosopher(0);
+    run philosopher(1);
+    run philosopher(2);
+    run philosopher(3);
+    run philosopher(4);
+    run watchdog()
+}