--- a/paper/chapter4.tex	Thu Feb 14 05:30:52 2008 +0900
+++ b/paper/chapter4.tex	Thu Feb 14 15:43:13 2008 +0900
@@ -1,30 +1,75 @@
-\chapter{評価および考察}
+\chapter{評価}
 \label{chapter4}
+
+実装したDining Philosophers Problemのタブロー展開および、
+線形時相論理による検証を組み込んだタブロー展開の評価を行う。
+
+また、検証を組み込んだタブロー展開においては他の検証ツールとの比較を行う。
+
+\section{実行環境と評価方法}
+実行環境として表\ref{tab:machine_spec}を用いた。
+
 %評価に使用したマシンのスペック
+\begin{table}
+    \centering
+    \begin{tabular}{|c|l|} \hline
+	OS & FedoraCore6 \\ \hline
+	CPU & Intel(R) Pentium4 2.8GHz \\ \hline
+	MEMORY & 1GB \\ \hline
+    \end{tabular}
+    \caption{評価に使用したマシンのスペック}
+    \label{tab:machine_spec}
+\end{table}
+
+
+評価の方法については、実行時間を計測することで行う。
+実行時間の計測は、Unixのtimeコマンドを用いて行う。
+timeコマンドは実行に要する経過時間などを計測するためのコマンドである。
+正確な結果を得るため、timeコマンドで5回計測し、その平均値を取る。
 
 \section{Dining Philosophers Problemのタブロー展開}
 CbCで実装したDining Philosophers Problemに対してタブロー展開を適用した。
-プロセス(哲学者)が5〜7人の場合の結果は表\ref{tab:dpp_tableau}のようになった。
+プロセス(哲学者)が3〜7個の場合の結果は表\ref{tab:dpp_tableau}のようになった。
 
 \begin{table}
     \centering
     \begin{tabular}{|r|r|r|} \hline
-	プロセス数 & 状態数 & 時間(秒) \\ \hline
-	5 & 38,984 & 0.76 \\ \hline
-	6 & 159,299 & 4.21 \\ \hline
-	7 & 845,529 & 31.01 \\ \hline
+	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
+	3 & 1,340 & 0.02 \\ \hline
+	4 & 6,115 & 0.10 \\ \hline
+	5 & 38,984 & 0.82 \\ \hline
+	6 & 159,299 & 4.38 \\ \hline
+	7 & 845,529 & 31.03 \\ \hline
 	8 & 3915,727 & 202.48 \\ \hline
     \end{tabular}
     \caption{Dining Philosophers Problemのタブロー展開結果}
     \label{tab:dpp_tableau}
 \end{table}
 
+表\ref{tab:dpp_tableau}を見ると、プロセス数に対して状態数が
+指数オーダーで増加していることがわかる。
+また、実行時間も同様に増加している。
+
+しかし、プロセス数が5個と6個の場合の実行時間がそれぞれ0.82秒、4.38秒と速く、
+実用レベルであると言える。
 
 \section{線形時相論理を用いた検証}
 Dining Philosophers Problemのデッドロックを検知するためのコードセグメントを組み込んで
-タブロー展開を行った。
+タブロー展開を行う。
+また、他の検証ツールとの比較を行う。
+\\
+
+プロセスが5〜６個の場合の結果は表\ref{tab:ltl_tableau}
 
-\section{他の検証ツールとの比較}
-SPINはモデル検査ツールであるため、検証対象をモデル化しそれをPROMELAで記述する必要がある。
+\begin{table}
+    \centering
+    \begin{tabular}{|r|r|r|} \hline
+	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
+	5 & 38,984 & 0.83 \\ \hline
+	6 & 159,299 & 4.41 \\ \hline
+    \end{tabular}
+    \caption{Dining Philosophers Problemにデッドロック検知を組み込んだ実行結果}
+    \label{tab:ltl_tableau}
+\end{table}
 
-CbCでの検証は、実際に動作するプログラムに対して行うことができる。
+