# HG changeset patch # User atsuki # Date 1203636895 -32400 # Node ID 8dc58ffa1d7934a63c8d4bc12c59aed46241c422 # Parent c1ef5abc2bb751bc731ca39dddb5255185328c33 *** empty log message *** diff -r c1ef5abc2bb7 -r 8dc58ffa1d79 paper/Makefile --- a/paper/Makefile Fri Feb 22 08:28:02 2008 +0900 +++ b/paper/Makefile Fri Feb 22 08:34:55 2008 +0900 @@ -1,5 +1,5 @@ MAKE=make -f Makefile -LATEX=platex-euc +LATEX=platex BIBTEX=jbibtex MENDEX=mendex DVIPS=pdvips diff -r c1ef5abc2bb7 -r 8dc58ffa1d79 paper/chapter4.tex --- a/paper/chapter4.tex Fri Feb 22 08:28:02 2008 +0900 +++ b/paper/chapter4.tex Fri Feb 22 08:34:55 2008 +0900 @@ -201,12 +201,12 @@ \begin{center} \caption{JPFによるDining Philosophers Problemの検証の計測結果} \label{tab:jpf_dpp} - \begin{tabular}{|r|r|} \hline - プロセス数 & 実行時間(秒) \\ \hline - 5 & 3.98 \\ \hline - 6 & 7.33 \\ \hline - 7 & 26.29 \\ \hline - 8 & 123.16 \\ \hline + \begin{tabular}{|r|r|r|} \hline + プロセス数 & 状態数 & 実行時間(秒) \\ \hline + 5 & 不明 & 3.98 \\ \hline + 6 & 不明 & 7.33 \\ \hline + 7 & 不明 & 26.29 \\ \hline + 8 & 不明 & 123.16 \\ \hline \end{tabular} \end{center} \end{table} diff -r c1ef5abc2bb7 -r 8dc58ffa1d79 paper/chapter5.tex --- a/paper/chapter5.tex Fri Feb 22 08:28:02 2008 +0900 +++ b/paper/chapter5.tex Fri Feb 22 08:34:55 2008 +0900 @@ -1,6 +1,7 @@ \chapter{結論} \label{chapter5} -本稿では、Continuation based C言語による実装と + + 本稿では、Continuation based C言語による実装と その実装に対する検証手法を提案した。 第\ref{chapter3}章では、検証の対象として並列プログラムを選択し、 @@ -16,9 +17,6 @@ それに検証用コードセグメントを組み込んだ場合のそれぞれの実装において、 プロセス数に対する状態数と検証にかかる時間の評価および考察を行った。 -プロセス数が5個の場合の実行時間が0.68秒と高速であり、 -実用レベルに達しているといえる。 - また、他のモデル検査ツールであるSPINとJava PathFinderとの比較を行い、考察した。 \\ diff -r c1ef5abc2bb7 -r 8dc58ffa1d79 paper/thanx.tex --- a/paper/thanx.tex Fri Feb 22 08:28:02 2008 +0900 +++ b/paper/thanx.tex Fri Feb 22 08:34:55 2008 +0900 @@ -1,7 +1,7 @@ \chapter*{謝辞} \addcontentsline{toc}{chapter}{謝辞} -本研究を行うにあたって、ご多忙にも関わらず日頃より多くのご助言、ご指導を + 本研究を行うにあたって、ご多忙にも関わらず日頃より多くのご助言、ご指導を 頂きました河野真治准教授に心より感謝いたします。 また、本研究に大変貴重なご意見を下さった、和田知久教授、遠藤聡志教授、