Mercurial > hg > Papers > 2008 > atsuki-master
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ˡˤ֤ΰ̤μ롣