Mercurial > hg > Papers > 2022 > soto-sigos

changeset 3:952d4dbb7c6a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
WIP 仮完成
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 05 May 2022 03:30:26 +0900
parents f9794e92f964
children 7434c0aa1859
files Paper/fig/Dining.pdf Paper/fig/cbc_codegear.pdf Paper/soto-sigos.aux Paper/soto-sigos.dvi Paper/soto-sigos.fdb_latexmk Paper/soto-sigos.fls Paper/soto-sigos.log Paper/soto-sigos.pdf Paper/soto-sigos.synctex.gz Paper/soto-sigos.tex Paper/tex/cbc.tex Paper/tex/cbc_agda.tex Paper/tex/dpp_impl.tex
diffstat 13 files changed, 139 insertions(+), 117 deletions(-) [+]
line wrap: on
line diff
Binary file Paper/fig/Dining.pdf has changed
Binary file Paper/fig/cbc_codegear.pdf has changed
--- a/Paper/soto-sigos.aux	Thu May 05 00:32:42 2022 +0900
+++ b/Paper/soto-sigos.aux	Thu May 05 03:30:26 2022 +0900
@@ -18,11 +18,13 @@
 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}{agda による Meta Gears}}{3}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {section}{\numberline {4}\hskip 1zw{モデル検査}}{3}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {section}{\numberline {5}\hskip 1zw{Dining Philosophers Problem}}{3}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}{Gears Agda によるDPPの実装}}{3}{}\protected@file@percent }
-\newlabel{agda-dpp-state}{{5}{3}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}{\ignorespaces Gears Agdaでの DPP の 哲学者の状態}}{3}{}\protected@file@percent }
-\newlabel{agda-dpp-process}{{6}{3}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {6}{\ignorespaces Gears Agdaでの DPP の プロセス}}{3}{}\protected@file@percent }
+\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces メタ計算を可視化した CodeGear と DataGear\relax }}{3}{}\protected@file@percent }
+\newlabel{fig:DPP}{{2}{3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}{Gears Agda によるDPPの実装}}{4}{}\protected@file@percent }
+\newlabel{agda-dpp-state}{{5}{4}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}{\ignorespaces Gears Agdaでの DPP の 哲学者の状態}}{4}{}\protected@file@percent }
+\newlabel{agda-dpp-process}{{6}{4}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {6}{\ignorespaces Gears Agdaでの DPP の プロセス}}{4}{}\protected@file@percent }
 \newlabel{agda-dpp-dg}{{7}{4}}
 \@writefile{lol}{\contentsline {lstlisting}{\numberline {7}{\ignorespaces Gears Agdaでの DPP の Data Gear}}{4}{}\protected@file@percent }
 \newlabel{agda-dpp-init}{{8}{4}}
@@ -30,13 +32,16 @@
 \newlabel{agda-dpp-step}{{9}{4}}
 \@writefile{lol}{\contentsline {lstlisting}{\numberline {9}{\ignorespaces Gears Agdaでの DPP の step 実行}}{4}{}\protected@file@percent }
 \newlabel{agda-dpp-lfork}{{10}{4}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {10}{\ignorespaces Gears Agdaでの DPP の 左のフォークを取るコード}}{4}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPPのモデル検査}}{4}{}\protected@file@percent }
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {10}{\ignorespaces Gears Agdaでの DPP の左のフォークを取る記述}}{4}{}\protected@file@percent }
 \citation{*}
 \bibstyle{ipsjsort}
 \bibdata{reference}
 \bibcite{agda-wiki}{1}
 \bibcite{agda-alpa}{2}
+\@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPPのモデル検査}}{5}{}\protected@file@percent }
+\newlabel{agda-dpp-bruteforce}{{11}{5}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {11}{\ignorespaces Gears Agdaでの DPP の場合を網羅するコード}}{5}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent }
 \bibcite{ats2}{3}
 \bibcite{cbc-gcc}{4}
 \bibcite{cbc-llvm}{5}
@@ -47,9 +52,6 @@
 \bibcite{rust}{10}
 \bibcite{coq-old}{11}
 \bibcite{agda-documentation}{12}
-\newlabel{agda-dpp-bruteforce}{{11}{5}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {11}{\ignorespaces Gears Agdaでの DPP の 左のフォークを取るコード}}{5}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent }
 \bibcite{cr-ryukyu}{13}
 \bibcite{10.1145/363235.363259}{14}
 \bibcite{kaito-lola}{15}
Binary file Paper/soto-sigos.dvi has changed
--- a/Paper/soto-sigos.fdb_latexmk	Thu May 05 00:32:42 2022 +0900
+++ b/Paper/soto-sigos.fdb_latexmk	Thu May 05 03:30:26 2022 +0900
@@ -1,17 +1,17 @@
 # Fdb version 3
-["bibtex soto-sigos"] 1651673321 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1651673322
+["bibtex soto-sigos"] 1651688945 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1651688946
   "./ipsjsort.bst" 1541385384 25930 d27669b348c8e9a5c1cc93168b2b5e89 ""
   "reference.bib" 1650721531 8174 141307c3535f6e6da421a5ffb91d3db0 ""
-  "soto-sigos.aux" 1651673322 4295 aab7a2e823658120e46d12dc2df2eb9c "latex"
+  "soto-sigos.aux" 1651688946 4473 72b17962261903c19be0d13abefbd397 "latex"
   (generated)
   "soto-sigos.bbl"
   "soto-sigos.blg"
-["dvipdf"] 1651673322 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1651673322
-  "soto-sigos.dvi" 1651673322 65688 e5ddc4db2906e7f1634a64560623fb9b "latex"
+["dvipdf"] 1651688946 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1651688946
+  "soto-sigos.dvi" 1651688946 66764 a04c3839e858c08442a39bf3db610eca "latex"
   (generated)
   "soto-sigos.pdf"
-["latex"] 1651673321 "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" "soto-sigos.dvi" "soto-sigos" 1651673322
-  "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" 1651673320 4629 dbd88eb23bf5ed403bba3199bc43593f ""
+["latex"] 1651688945 "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" "soto-sigos.dvi" "soto-sigos" 1651688946
+  "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" 1651688878 5261 a6bc4ac07bdab035bc9778a1f8fa9812 ""
   "/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1647844622 3524 cb3e574dea2d1052e39280babc910dc8 ""
   "/usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1647844622 2124 2601a75482e9426d33db523edf23570a ""
   "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm0700.tfm" 1647844622 3584 cf973739aac7ab6247f9150296af7954 ""
@@ -131,19 +131,19 @@
   "/usr/share/texmf-dist/tex/platex/japanese-otf/otf.sty" 1647806829 23780 6dcbea98f42a2e1905e36acdd2df6006 ""
   "/usr/share/texmf-dist/web2c/texmf.cnf" 1647844622 39911 2da6c67557ec033436fe5418a70a8a61 ""
   "/var/lib/texmf/web2c/eptex/platex.fmt" 1650708372 2834363 869774857659f265ab483b1aeb8f0c7c ""
-  "fig/meta-cg-dg.pdf" 1650721531 14360 a49f27d9f258ff5d68c6c4e908f67476 ""
-  "fig/meta-cg-dg.xbb" 1650721531 212 38813b94d19b91938f022ae3152b7ed7 ""
+  "fig/Dining.pdf" 1651685530 126415 635fdfd0d90894b78e5da1c3af0ef19f ""
+  "fig/cbc_codegear.pdf" 1651684831 30110 abae9d544b613e6b77036cde8327a20f ""
   "ipsj.cls" 1650809266 142123 ecf81ecc4679baed6ac44a1571336871 ""
   "ipsjtech.sty" 1541385384 6572 e6269869e3c126f2d200f352d590509a ""
-  "soto-sigos.aux" 1651673322 4295 aab7a2e823658120e46d12dc2df2eb9c "latex"
-  "soto-sigos.bbl" 1651673321 5285 fc93245f635fcc8bdb721d450a7e0e37 "bibtex soto-sigos"
-  "soto-sigos.tex" 1651673320 4629 dbd88eb23bf5ed403bba3199bc43593f ""
+  "soto-sigos.aux" 1651688946 4473 72b17962261903c19be0d13abefbd397 "latex"
+  "soto-sigos.bbl" 1651688945 5285 fc93245f635fcc8bdb721d450a7e0e37 "bibtex soto-sigos"
+  "soto-sigos.tex" 1651688878 5261 a6bc4ac07bdab035bc9778a1f8fa9812 ""
   "src/agda-dpp-impl.agda.replaced" 1651667549 2824 60454fbbf20d18849d1886385e94384b ""
   "src/agda-dpp-modelcheck.agda.replaced" 1651672378 3179 60cc940175e150991d362fe173027e9b ""
   "src/agda/cbc-agda.agda.replaced" 1651647471 1143 ab39102eb0f69d3b9f8e4e985a7c1e37 ""
-  "tex/cbc.tex" 1651644049 2219 f03feb68b5ce1a7b91d393a89cfeb34e ""
-  "tex/cbc_agda.tex" 1651652099 4661 0b5344e541f9fd9f293bced30f494ecd ""
-  "tex/dpp_impl.tex" 1651668498 6128 590795d2699a6da79652be11e27f0047 ""
+  "tex/cbc.tex" 1651688590 2216 c194a2cd2075b1e26ac8b51a728306a4 ""
+  "tex/cbc_agda.tex" 1651688631 4606 2279e1583a4c51075974ecc2bf95a7d7 ""
+  "tex/dpp_impl.tex" 1651688944 6361 19e932852f3f0ef1508bfd8f6a9481d8 ""
   "tex/intro.tex" 1651570383 3454 c2cd2b67fe52c3a93b6c540ef98ec175 ""
   (generated)
   "soto-sigos.aux"
--- a/Paper/soto-sigos.fls	Thu May 05 00:32:42 2022 +0900
+++ b/Paper/soto-sigos.fls	Thu May 05 03:30:26 2022 +0900
@@ -555,10 +555,10 @@
 INPUT /usr/share/texmf-dist/fonts/tfm/public/japanese-otf/nmlminr-h.tfm
 INPUT /usr/share/texmf-dist/fonts/tfm/public/lm/ec-lmr9.tfm
 OUTPUT soto-sigos.dvi
-INPUT ./fig/meta-cg-dg.pdf
-INPUT ./fig/meta-cg-dg.pdf
-INPUT fig/meta-cg-dg.pdf
-INPUT fig/meta-cg-dg.xbb
+INPUT ./fig/cbc_codegear.pdf
+INPUT ./fig/cbc_codegear.pdf
+INPUT fig/cbc_codegear.pdf
+INPUT extractbb -B cropbox -O fig/cbc_codegear.pdf
 INPUT ./tex/cbc_agda.tex
 INPUT tex/cbc_agda.tex
 INPUT ./tex/cbc_agda.tex
@@ -601,6 +601,10 @@
 INPUT tex/dpp_impl.tex
 INPUT ./tex/dpp_impl.tex
 INPUT tex/dpp_impl.tex
+INPUT ./fig/Dining.pdf
+INPUT ./fig/Dining.pdf
+INPUT fig/Dining.pdf
+INPUT extractbb -B cropbox -O fig/Dining.pdf
 INPUT ./src/agda-dpp-impl.agda.replaced
 INPUT src/agda-dpp-impl.agda.replaced
 INPUT ./src/agda-dpp-impl.agda.replaced
--- a/Paper/soto-sigos.log	Thu May 05 00:32:42 2022 +0900
+++ b/Paper/soto-sigos.log	Thu May 05 03:30:26 2022 +0900
@@ -1,4 +1,4 @@
-This is e-pTeX, Version 3.141592653-p3.9.0-210218-2.6 (utf8.euc) (TeX Live 2021/Arch Linux) (preloaded format=platex 2022.4.23)  4 MAY 2022 23:08
+This is e-pTeX, Version 3.141592653-p3.9.0-210218-2.6 (utf8.euc) (TeX Live 2021/Arch Linux) (preloaded format=platex 2022.4.23)  5 MAY 2022 03:29
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -3273,10 +3273,10 @@
 Package caption Info: listings package is loaded.
 )
 LaTeX Font Info:    Font shape `JT1/hmc/m/n' will be
-(Font)              scaled to size 9.24725pt on input line 51.
+(Font)              scaled to size 9.24725pt on input line 54.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 9.24725pt on input line 51.
-LaTeX Font Info:    Trying to load font information for T1+lmr on input line 51.
+(Font)              scaled to size 9.24725pt on input line 54.
+LaTeX Font Info:    Trying to load font information for T1+lmr on input line 54.
  (/usr/share/texmf-dist/tex/latex/lm/t1lmr.fd
 File: t1lmr.fd 2015/05/01 v1.6.1 Font defs for Latin Modern
 ) (/usr/share/texmf-dist/tex/latex/l3backend/l3backend-dvips.def
@@ -3291,104 +3291,104 @@
 ) (./soto-sigos.aux)
 \openout1 = `soto-sigos.aux'.
 
-LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 51.
-LaTeX Font Info:    ... okay on input line 51.
-LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 51.
-LaTeX Font Info:    ... okay on input line 51.
-LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 51.
-LaTeX Font Info:    ... okay on input line 51.
-LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 51.
-LaTeX Font Info:    ... okay on input line 51.
-LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 51.
-LaTeX Font Info:    ... okay on input line 51.
-LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 51.
-LaTeX Font Info:    ... okay on input line 51.
-LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 51.
-LaTeX Font Info:    ... okay on input line 51.
-LaTeX Font Info:    Checking defaults for JY1/mc/m/n on input line 51.
-LaTeX Font Info:    ... okay on input line 51.
-LaTeX Font Info:    Checking defaults for JT1/mc/m/n on input line 51.
-LaTeX Font Info:    ... okay on input line 51.
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 54.
+LaTeX Font Info:    ... okay on input line 54.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 54.
+LaTeX Font Info:    ... okay on input line 54.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 54.
+LaTeX Font Info:    ... okay on input line 54.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 54.
+LaTeX Font Info:    ... okay on input line 54.
+LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 54.
+LaTeX Font Info:    ... okay on input line 54.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 54.
+LaTeX Font Info:    ... okay on input line 54.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 54.
+LaTeX Font Info:    ... okay on input line 54.
+LaTeX Font Info:    Checking defaults for JY1/mc/m/n on input line 54.
+LaTeX Font Info:    ... okay on input line 54.
+LaTeX Font Info:    Checking defaults for JT1/mc/m/n on input line 54.
+LaTeX Font Info:    ... okay on input line 54.
 \c@lstlisting=\count303
 Package caption Info: Begin \AtBeginDocument code.
 Package caption Info: End \AtBeginDocument code.
 LaTeX Font Info:    Font shape `JT1/hmc/m/n' will be
-(Font)              scaled to size 8.53593pt on input line 64.
+(Font)              scaled to size 8.53593pt on input line 67.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 8.53593pt on input line 64.
+(Font)              scaled to size 8.53593pt on input line 67.
 LaTeX Font Info:    Font shape `JT1/hmc/bx/n' will be
-(Font)              scaled to size 8.53593pt on input line 64.
+(Font)              scaled to size 8.53593pt on input line 67.
 LaTeX Font Info:    Font shape `JY1/hmc/bx/n' will be
-(Font)              scaled to size 8.53593pt on input line 64.
+(Font)              scaled to size 8.53593pt on input line 67.
 LaTeX Font Info:    Font shape `JT1/gt/bx/n' in size <19.2207> not available
-(Font)              Font shape `JT1/gt/m/n' tried instead on input line 72.
+(Font)              Font shape `JT1/gt/m/n' tried instead on input line 75.
 LaTeX Font Info:    Font shape `JY1/gt/bx/n' in size <19.2207> not available
-(Font)              Font shape `JY1/gt/m/n' tried instead on input line 72.
-LaTeX Font Info:    Calculating math sizes for size <9.61035> on input line 72.
-LaTeX Font Info:    Trying to load font information for OT1+lmr on input line 72.
+(Font)              Font shape `JY1/gt/m/n' tried instead on input line 75.
+LaTeX Font Info:    Calculating math sizes for size <9.61035> on input line 75.
+LaTeX Font Info:    Trying to load font information for OT1+lmr on input line 75.
  (/usr/share/texmf-dist/tex/latex/lm/ot1lmr.fd
 File: ot1lmr.fd 2015/05/01 v1.6.1 Font defs for Latin Modern
 )
-LaTeX Font Info:    Trying to load font information for OML+lmm on input line 72.
+LaTeX Font Info:    Trying to load font information for OML+lmm on input line 75.
  (/usr/share/texmf-dist/tex/latex/lm/omllmm.fd
 File: omllmm.fd 2015/05/01 v1.6.1 Font defs for Latin Modern
 )
-LaTeX Font Info:    Trying to load font information for OMS+lmsy on input line 72.
+LaTeX Font Info:    Trying to load font information for OMS+lmsy on input line 75.
  (/usr/share/texmf-dist/tex/latex/lm/omslmsy.fd
 File: omslmsy.fd 2015/05/01 v1.6.1 Font defs for Latin Modern
 )
-LaTeX Font Info:    Trying to load font information for OMX+lmex on input line 72.
+LaTeX Font Info:    Trying to load font information for OMX+lmex on input line 75.
  (/usr/share/texmf-dist/tex/latex/lm/omxlmex.fd
 File: omxlmex.fd 2015/05/01 v1.6.1 Font defs for Latin Modern
 )
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <9.61035> on input line 72.
+(Font)              <9.61035> on input line 75.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <6.7272> on input line 72.
+(Font)              <6.7272> on input line 75.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <4.80518> on input line 72.
+(Font)              <4.80518> on input line 75.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 6.47304pt on input line 72.
+(Font)              scaled to size 6.47304pt on input line 75.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 4.62363pt on input line 72.
+(Font)              scaled to size 4.62363pt on input line 75.
 LaTeX Font Info:    Font shape `JT1/hmc/m/n' will be
-(Font)              scaled to size 11.38124pt on input line 72.
+(Font)              scaled to size 11.38124pt on input line 75.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 11.38124pt on input line 72.
-LaTeX Font Info:    Calculating math sizes for size <11.82813> on input line 72.
+(Font)              scaled to size 11.38124pt on input line 75.
+LaTeX Font Info:    Calculating math sizes for size <11.82813> on input line 75.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <11.82813> on input line 72.
+(Font)              <11.82813> on input line 75.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <8.27965> on input line 72.
+(Font)              <8.27965> on input line 75.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <5.91406> on input line 72.
+(Font)              <5.91406> on input line 75.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 7.96683pt on input line 72.
+(Font)              scaled to size 7.96683pt on input line 75.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 5.69061pt on input line 72.
+(Font)              scaled to size 5.69061pt on input line 75.
 LaTeX Font Info:    Font shape `JT1/hmc/m/n' will be
-(Font)              scaled to size 7.96683pt on input line 72.
+(Font)              scaled to size 7.96683pt on input line 75.
 LaTeX Font Info:    Font shape `JT1/hmc/m/n' will be
-(Font)              scaled to size 7.11327pt on input line 72.
+(Font)              scaled to size 7.11327pt on input line 75.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 7.11327pt on input line 72.
+(Font)              scaled to size 7.11327pt on input line 75.
 LaTeX Font Info:    Font shape `JT1/hmc/m/n' will be
-(Font)              scaled to size 7.8246pt on input line 72.
+(Font)              scaled to size 7.8246pt on input line 75.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 7.8246pt on input line 72.
-LaTeX Font Info:    Calculating math sizes for size <8.13184> on input line 72.
+(Font)              scaled to size 7.8246pt on input line 75.
+LaTeX Font Info:    Calculating math sizes for size <8.13184> on input line 75.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <8.13184> on input line 72.
+(Font)              <8.13184> on input line 75.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <5.69225> on input line 72.
+(Font)              <5.69225> on input line 75.
 LaTeX Font Info:    External font `lmex10' loaded for size
-(Font)              <4.06592> on input line 72.
+(Font)              <4.06592> on input line 75.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 5.47719pt on input line 72.
+(Font)              scaled to size 5.47719pt on input line 75.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
-(Font)              scaled to size 3.9123pt on input line 72.
+(Font)              scaled to size 3.9123pt on input line 75.
 LaTeX Font Info:    Font shape `JT1/hmc/m/n' will be
-(Font)              scaled to size 5.47719pt on input line 72.
+(Font)              scaled to size 5.47719pt on input line 75.
  (./tex/intro.tex
 LaTeX Font Info:    Font shape `JT1/hmc/bx/n' will be
 (Font)              scaled to size 11.38124pt on input line 1.
@@ -3427,10 +3427,10 @@
 
 
 ]
-File: fig/meta-cg-dg.pdf Graphic file (type pdf)
-<fig/meta-cg-dg.pdf>
+File: fig/cbc_codegear.pdf Graphic file (type pdf)
+<fig/cbc_codegear.pdf>
 ) (./tex/cbc_agda.tex
-LaTeX Font Info:    Trying to load font information for T1+lmtt on input line 9.
+LaTeX Font Info:    Trying to load font information for T1+lmtt on input line 8.
  (/usr/share/texmf-dist/tex/latex/lm/t1lmtt.fd
 File: t1lmtt.fd 2015/05/01 v1.6.1 Font defs for Latin Modern
 ) (./src/agda/cbc-agda.agda.replaced
@@ -3443,12 +3443,15 @@
 consecutive:
 ) [2]
 LaTeX Font Info:    Font shape `JT1/hmc/bx/n' will be
-(Font)              scaled to size 9.24725pt on input line 62.
+(Font)              scaled to size 9.24725pt on input line 61.
 LaTeX Font Info:    Font shape `JY1/hmc/bx/n' will be
-(Font)              scaled to size 9.24725pt on input line 62.
-) (./tex/dpp_impl.tex (./src/agda-dpp-impl.agda.replaced) (./src/agda-dpp-impl.agda.replaced
+(Font)              scaled to size 9.24725pt on input line 61.
+) (./tex/dpp_impl.tex
+File: fig/Dining.pdf Graphic file (type pdf)
+<fig/Dining.pdf>
+ [3] (./src/agda-dpp-impl.agda.replaced) (./src/agda-dpp-impl.agda.replaced
 consecutive:
-[3]) (./src/agda-dpp-impl.agda.replaced
+) (./src/agda-dpp-impl.agda.replaced
 consecutive:
 ) (./src/agda-dpp-impl.agda.replaced
 consecutive:
@@ -3458,7 +3461,7 @@
 consecutive:
 ) (./src/agda-dpp-impl.agda.replaced
 consecutive:
-)) [4] (./src/agda-dpp-modelcheck.agda.replaced) (./soto-sigos.bbl
+[4])) (./src/agda-dpp-modelcheck.agda.replaced) (./soto-sigos.bbl
 LaTeX Font Info:    Calculating math sizes for size <8.8711> on input line 1.
 LaTeX Font Info:    External font `lmex10' loaded for size
 (Font)              <8.8711> on input line 1.
@@ -3470,7 +3473,7 @@
 (Font)              scaled to size 5.97511pt on input line 1.
 LaTeX Font Info:    Font shape `JY1/hmc/m/n' will be
 (Font)              scaled to size 4.26796pt on input line 1.
-
+ [5]
 Underfull \hbox (badness 10000) in paragraph at lines 12--14
 []\T1/lmr/m/n/8.8711 : ATS-PL-SYS, $\T1/lmtt/m/n/8.8711 http : / / www . ats-[]lang . org/$\T1/lmr/m/n/8.8711 .
  []
@@ -3540,7 +3543,7 @@
 \T1/lmtt/m/n/8.8711 io / en / latest/$\T1/lmr/m/n/8.8711 .  plus.33emminus.07emAccessed:
  []
 
-[5]
+
 Underfull \hbox (badness 4353) in paragraph at lines 56--59
 []\T1/lmr/m/n/8.8711 : whileTest-Prim.agda - \JY1/hmc/m/n/8.8711 並列信頼研 \T1/lmr/m/n/8.8711 mer-cu-rial
  []
@@ -3588,20 +3591,18 @@
 \JY1/hmc/m/n/8.8711 報処理学会論文誌プログラミング （\T1/lmr/m/n/8.8711 PRO\JY1/hmc/m/n/8.8711 ） ，
  []
 
-) [6
-
-] (./soto-sigos.aux)
+) [6] (./soto-sigos.aux)
 
 LaTeX Font Warning: Some font shapes were not available, defaults substituted.
 
  ) 
 Here is how much of TeX's memory you used:
- 10939 strings out of 478739
- 166639 string characters out of 5863952
- 1333538 words of memory out of 5000000
- 29179 multiletter control sequences out of 15000+600000
+ 10946 strings out of 478739
+ 166780 string characters out of 5863952
+ 1450538 words of memory out of 5000000
+ 29184 multiletter control sequences out of 15000+600000
  583961 words of font info for 188 fonts, out of 8000000 for 9000
  929 hyphenation exceptions out of 8191
- 55i,11n,63p,487b,1974s stack positions out of 5000i,500n,10000p,200000b,80000s
-
-Output written on soto-sigos.dvi (6 pages, 65688 bytes).
+ 55i,10n,63p,483b,1976s stack positions out of 5000i,500n,10000p,200000b,80000s
+
+Output written on soto-sigos.dvi (6 pages, 66764 bytes).
Binary file Paper/soto-sigos.pdf has changed
Binary file Paper/soto-sigos.synctex.gz has changed
--- a/Paper/soto-sigos.tex	Thu May 05 00:32:42 2022 +0900
+++ b/Paper/soto-sigos.tex	Thu May 05 03:30:26 2022 +0900
@@ -48,6 +48,9 @@
 \newcommand\newblock{\hskip .11em\@plus.33em\@minus.07em}
 \captionsetup[lstlisting]{font={small, tt}}
 
+\renewcommand{\lstlistingname}{Code}
+
+
 \begin{document}
 
 % Title,  Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -78,7 +81,16 @@
 \input{tex/cbc_agda.tex}% Gears Agda の記法　loopのやつやる
 
 \section{モデル検査}
-モデル検査の説明をする。
+モデル検査とは、検証手法の一つである。
+他の検証手法として代表的なものとして、定理証明が挙げられる
+
+モデル検査はプログラムが入力に対して仕様を満たした動作を
+行うことを網羅的に検証することを指す。
+
+モデル検査と定理証明を比較した際に、モデル検査は入力が無限になる
+状態爆発が起こり得るという問題がある。
+定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
+できるが、専門的な知識が多く難易度が高いという欠点がある。
 
 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
 
@@ -91,7 +103,7 @@
 を定義した。
 
 
-\lstinputlisting[caption= Gears Agdaでの DPP の 左のフォークを取るコード, label=agda-dpp-bruteforce]{src/agda-dpp-modelcheck.agda.replaced}
+\lstinputlisting[caption= Gears Agdaでの DPP の場合を網羅するコード, label=agda-dpp-bruteforce]{src/agda-dpp-modelcheck.agda.replaced}
 
 内部で行っていることとして、その Code Gear 内に存在している next-code が thinking もしくは eatingである場合に
 そのプロセスのnext-codeをそのままにするか、それぞれ pickup-rfork か putdown-lfork にする。
--- a/Paper/tex/cbc.tex	Thu May 05 00:32:42 2022 +0900
+++ b/Paper/tex/cbc.tex	Thu May 05 03:30:26 2022 +0900
@@ -22,8 +22,6 @@
 さらに Code Gear 単位で処理が完結していることから、
 検証に適したプログラミング言語であると言える。
 
----
-
 また、プログラムを記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、資源管理等を記述しなければならない処理が存在する。
 これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。
 
@@ -35,7 +33,7 @@
 
 \begin{figure}[htpb]
  \begin{center}
-  \scalebox{0.35}{\includegraphics{fig/meta-cg-dg.pdf}}
+  \scalebox{0.35}{\includegraphics{fig/cbc_codegear.pdf}}
  \end{center}
  \caption{メタ計算を可視化した CodeGear と DataGear}
  \label{fig:meta-cgdg}
--- a/Paper/tex/cbc_agda.tex	Thu May 05 00:32:42 2022 +0900
+++ b/Paper/tex/cbc_agda.tex	Thu May 05 03:30:26 2022 +0900
@@ -2,9 +2,8 @@
 CbC の継続の概念を取り入れた Agda の記法を説明する。
 Agdaでは関数の再帰呼び出しが可能であるが、CbCでは値が 帰って来ない。そのためAgda
 で実装を行う際には再帰呼び出しを行わないようにする。
-code \ref{agda-dg}が例となるコードである。
 
-以下が Gears Agda の記述方法を足し算を行うプログラムを用いて説明する。
+以下で Gears Agda の記述方法を足し算を行うプログラムを用いて説明する。
 
 \lstinputlisting[caption= Agdaでの Data Gear の定義, label=agda-dg, firstline=6, lastline=11]{src/agda/cbc-agda.agda.replaced}
 
--- a/Paper/tex/dpp_impl.tex	Thu May 05 00:32:42 2022 +0900
+++ b/Paper/tex/dpp_impl.tex	Thu May 05 03:30:26 2022 +0900
@@ -4,12 +4,18 @@
 DPPとは資源共有問題であり、モデル検査をする際に挙げられる代表的な問題
 である。
 
-画像を貼る
+\begin{figure}[htpb]
+    \begin{center}
+     \scalebox{0.5}{\includegraphics{fig/Dining.pdf}}
+    \end{center}
+    \caption{メタ計算を可視化した CodeGear と DataGear}
+    \label{fig:DPP}
+\end{figure}   
 
 問題のストーリーをまとめると以下のようになる。
 
 \begin{itemize}
-    \item 哲学者がN人円卓についている
+    \item 哲学者がN人円卓についている(Nは2以上の自然数)
     \item 哲学者の目の前には食べ物が用意されている
     \item 哲学者の人数と同じだけのフォークがそれぞれ哲学者の間に置かれている
     \item 哲学者はしばらく思考したのち、しばらく食事する動作を繰り返しおこなう
@@ -20,7 +26,7 @@
     \item 哲学者はこの食事と思考を繰り返し行う。哲学者同士が会話することはない
 \end{itemize}
     
-つまり、以下のようなフローを独立して並列に実行することとなる
+つまり、哲学者は以下のようなフローを独立して並列に実行することとなる。
 
 \begin{enumerate}
     \item しばらくの間思考を行う
@@ -85,7 +91,7 @@
 
 この際に Env にある List Phi の中身を展開しながら一つづつ行動を処理していく。
 
-\lstinputlisting[caption= Gears Agdaでの DPP の 左のフォークを取るコード, label=agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced}
+\lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced}
 
 Code \ref{agda-dpp-lfork}がstep実行をした際に哲学者が左側のフォークを取る記述になる。