changeset 10:a4babe6179a7

*** empty log message ***
author atsuki
date Fri, 15 Feb 2008 19:00:41 +0900
parents c2a35ce4546e
children fd717f2d19ab
files paper/bibliography.tex paper/chapter4.tex paper/chapter5.tex
diffstat 3 files changed, 49 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/paper/bibliography.tex	Fri Feb 15 17:17:15 2008 +0900
+++ b/paper/bibliography.tex	Fri Feb 15 19:00:41 2008 +0900
@@ -1,4 +1,19 @@
 \begin{thebibliography}{99}
+    \bibitem{bib:jssst2006}
+	下地篤樹, 河野真治. ``タブロー法を用いたContinuation based Cプログラムの検証''.
+	日本ソフトウェア科学会第23回大会, 2006.
+    \bibitem{bib:sigos2007}
+	下地篤樹, 河野真治. ``線形時相論理によるContinuation based Cプログラムの検証''.
+	情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), April, 2007.
+    \bibitem{bib:jssst2000kono}
+	河野真治. ``継続を持つCの下位言語によるシステム記述''.
+	日本ソフトウェア科学会第17回大会, 2000.
+    \bibitem{bib:sigos2000shimabukuro}
+	島袋仁, 河野真治. ``C with Continuationと、そのPlayStationへの応用''.
+	情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), May, 2000.
+    \bibitem{bib:jssst2001higa}
+	比嘉薫, 河野真治. ``タブロー法の負荷分散について''.
+	日本ソフトウェア科学会第18回大会論文集, Sep, 2001.
     \bibitem{bib:spin}
 	``Spin - Formal Verification''.
 	http://spinroot.com/spin/whatispin.html
--- a/paper/chapter4.tex	Fri Feb 15 17:17:15 2008 +0900
+++ b/paper/chapter4.tex	Fri Feb 15 19:00:41 2008 +0900
@@ -29,18 +29,18 @@
 
 \section{Dining Philosophers ProblemΥ֥Ÿ}
 CbCǼDining Philosophers ProblemФƥ֥ŸŬѤ
-ץ(ůؼ)37Ĥξη̤ɽ\ref{tab:dpp_tableau}Τ褦ˤʤä
+ץ(ůؼ)37Ĥξη¬̤ɽ\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
+	3 & 1,340 & 0.01 \\ \hline
+	4 & 6,115 & 0.08 \\ \hline
+	5 & 38,984 & 0.66 \\ \hline
+	6 & 159,299 & 3.79 \\ \hline
+	7 & 845,529 & 28.59 \\ \hline
+	8 & 3915,727 & 199.80 \\ \hline
     \end{tabular}
     \caption{Dining Philosophers ProblemΥ֥Ÿ}
     \label{tab:dpp_tableau}
@@ -50,7 +50,7 @@
 ؿäƤ뤳Ȥ狼롣
 ޤ¹Ի֤ƱͤäƤ롣
 
-ץ5Ĥ6Ĥξμ¹Ի֤줾0.82á4.38ä®
+ץ5Ĥ6Ĥξμ¹Ի֤줾0.66á3.79ä®
 ѥ٥Ǥȸ롣
 
 \section{Ѥ}
@@ -59,14 +59,14 @@
 ޤ¾θڥġȤӤԤ
 \\
 
-ץ5Ĥξη̤ɽ\ref{tab:ltl_tableau}Τ褦ˤʤä
+ץ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
+	5 & 38,984 & 0.68 \\ \hline
+	6 & 159,299 & 3.90 \\ \hline
     \end{tabular}
     \caption{Dining Philosophers Problem˥ǥåɥåΤȤ߹¹Է}
     \label{tab:ltl_tableau}
@@ -80,7 +80,6 @@
 \begin{center}
 \begin{itembox}[l]{ץ5Ĥξμ¹Է}
 \begin{verbatim}
-	ά
 found 38984
 no more branch 38984
 All done count 38984
@@ -106,15 +105,17 @@
 SPINDining Philosophers ProblemθڤԤ
 
 ޤDining Philosophers Problemǥ벽ץPROMELAǵҤ롣
-ơ줫SPINˤäƸڴǤpan.c򥳥ѥ롢¹Ԥ롣
+ơSPINˤäƸڴǤpan.c򥳥ѥ롢¹Ԥ롣
 
 \ref{src:dpp.prm}PROMELAˤDining Philosophers ProblemΥǥ
 Ҥ򼨤
 
 \lstinputlisting[caption=PROMELAˤDining Philosophers Problemε,label=src:dpp.prm]{src/dpp.prm}
 
+\ref{src:dpp.prm}SPINˤpan.cʤɤΥե뤬롣
+gccǥѥ뤹뤳Ȥǡ¹ԥե뤬롣
 
-ץ56Ĥξη̤ɽ\ref{tab:spin_dpp}Τ褦ˤʤä
+ץ56Ĥξη¬̤ɽ\ref{tab:spin_dpp}Τ褦ˤʤä
 
 \begin{table}
     \centering
@@ -129,8 +130,8 @@
 
 CbCǤθڤ٤ơֿʤ
 Τᡢ¹Ԥˤ֤®Ǥä
-ϡPROMELAǤDining Philosophers ProblemݲƵҤƤ뤿
-ֿʤ
+ֿʤͳȤơPROMELAǤDining Philosophers Problem
+ݲƵҤ뤿ȹͤ롣
 
 CbCξϡºݤ˼¹Բǽʥץ༡¹ԤƤȤǾ֤Ѳ
 Ƥ뤿ᡢǥ벽Ҥֿ¿ʤäƤȹͤ롣
@@ -171,8 +172,8 @@
 ȤȤƤϡ\verb|javac|ˤJavaΥХȥɤơ
 \verb|jpf|Ǽ¹ԤǤ롣
 
-JPFμ¹Է̤ϡֿФʤ¹Ի֤ΤӤ롣
-ɽ\ref{tab:jpf_dpp}˼¹Է̤򼨤
+JPFμ¹Է̤ϡֿϤʤ¹Ի֤ΤӤ롣
+ɽ\ref{tab:jpf_dpp}˷¬̤򼨤
 
 \begin{table}
     \centering
@@ -186,7 +187,7 @@
 \end{table}
 
 JPFCbCƱͤ˼ºݤ˼¹ԲǽʥХȥɤФƸڤǽǤ롣
-ץФ¹Ի֤ӤCbC®
+ץФ¹Ի֤ӤCbC®Ȥ狼롣
 
 
 %%%end%%%
--- a/paper/chapter5.tex	Fri Feb 15 17:17:15 2008 +0900
+++ b/paper/chapter5.tex	Fri Feb 15 19:00:41 2008 +0900
@@ -1,18 +1,25 @@
 \chapter{}
 \label{chapter5}
-ܹƤǤϡContinuation based CץФ븡ڼˡƤ
+ܹƤǤϡContinuation based Cˤ
+μФ븡ڼˡƤ
 
-ޤڤоݤȤץ򤷡
-ȤDining Philosophers ProblemѤ
-
-ץ򥷥ߥ졼󤹤뤿˥塼Ȥ߹
+\ref{chapter3}ϤǤϡڤоݤȤץ򤷡
+ȤDining Philosophers ProblemѤ
 
 ڤȤơץ֤Ūõ뤿
-֥Ÿ
+֥Ÿ
 
 ֥Ÿݤ˸ѤΥɥȤȤ߹ळȤ
 Dining Philosophers ProblemΥǥåɥåΤǤ褦ˤ
 
+\ref{chapter4}Ǥϡ֥Ÿ
+˸ѥɥȤȤ߹Τ줾μˤơ
 ץФֿȸڤˤ֤ɾӹͻԤä
 
-¾θڥġȤӤԤä
+ץ5Ĥξμ¹Ի֤0.68äȹ®Ǥꡢѥ٥Ǥ뤳Ȥ
+
+ޤ¾θڥġǤSPINJava PathFinderȤӤԤͻ
+\\
+
+βȤơõ֤򰵽̤뤿ˡ
+LZWˡˤ֤ΰ̤μ롣