\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に対してタブロー展開を適用した。
プロセス(哲学者)が3〜7個の場合の結果は表\ref{tab:dpp_tableau}のようになった。

\begin{table}
    \centering
    \begin{tabular}{|r|r|r|} \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}

\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}