Mercurial > hg > Papers > 2022 > soto-sigos
changeset 7:6a61c1eb0205
これを提出した
line wrap: on
line diff
--- a/DPP/ModelChecking.agda Thu May 05 22:32:45 2022 +0900 +++ b/DPP/ModelChecking.agda Thu May 12 15:44:39 2022 +0900 @@ -136,7 +136,7 @@ set-state redu origin (false ∷ ss) f b env envl exit | p ∷ ps | C_eating = set-state redu origin ss (f ++ (p ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む set-state redu origin (true ∷ ss) f b env envl exit | p ∷ ps | C_thinking = set-state redu origin ss (f ++ (record p{next-code = C_pickup_rfork} ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む set-state redu origin (false ∷ ss) f b env envl exit | p ∷ ps | C_thinking = set-state redu origin ss (f ++ (p ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む - set-state redu origin (s ∷ ss) f b env envl exit | p ∷ ps | _ = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする + set-state redu origin (s ∷ ss) f b env envl exit | p ∷ ps | _ = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする test-search : List Env
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/.latexmkrc Thu May 12 15:44:39 2022 +0900 @@ -0,0 +1,12 @@ +#!/usr/bin/env perl +$latex = 'platex -shell-escape -synctex=1 -halt-on-error'; +$latex_silent = 'platex -shell-escape -synctex=1 -halt-on-error -interaction=batchmode'; +$bibtex = 'pbibtex'; +$dvipdf = 'dvipdfmx %O -o %D %S'; +$makeindex = 'mendex %O -o %D %S'; +$max_repeat = 5; +$pdf_mode = 3; # generates pdf via dvipdfmx + +# Prevent latexmk from removing PDF after typeset. +# This enables Skim to chase the update in PDF automatically. +$pvc_view_file_via_temporary = 0;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/fig/Dining.svg Thu May 12 15:44:39 2022 +0900 @@ -0,0 +1,1 @@ +<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" version="1.1" width="521px" height="466px" viewBox="-0.5 -0.5 521 466"><defs/><g><ellipse cx="260" cy="260" rx="180" ry="180" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><ellipse cx="94" cy="405" rx="40" ry="40" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 405px; margin-left: 55px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: normal; overflow-wrap: normal;">P0</div></div></div></foreignObject><text x="94" y="411" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">P0</text></switch></g><ellipse cx="115" cy="185" rx="15" ry="15" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><ellipse cx="260" cy="95" rx="15" ry="15" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><ellipse cx="405" cy="185" rx="15" ry="15" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><image x="244.5" y="377.65" width="38" height="53.7" xlink:href="https://harigamiya.jp/2x/illust-fork@2x-100.jpg" preserveAspectRatio="none"/><image x="159.5" y="109.5" width="38" height="53.7" xlink:href="https://harigamiya.jp/2x/illust-fork@2x-100.jpg" preserveAspectRatio="none" transform="rotate(139,179,136.85)"/><image x="315.5" y="115.8" width="38" height="53.7" xlink:href="https://harigamiya.jp/2x/illust-fork@2x-100.jpg" preserveAspectRatio="none" transform="rotate(-133,335,143.15)"/><image x="95.5" y="249.5" width="38" height="53.7" xlink:href="https://harigamiya.jp/2x/illust-fork@2x-100.jpg" preserveAspectRatio="none" transform="rotate(80,115,276.85)"/><image x="385.5" y="239.5" width="38" height="53.7" xlink:href="https://harigamiya.jp/2x/illust-fork@2x-100.jpg" preserveAspectRatio="none" transform="rotate(-84,405,266.85)"/><ellipse cx="60" cy="170" rx="40" ry="40" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 170px; margin-left: 21px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: normal; overflow-wrap: normal;">P1</div></div></div></foreignObject><text x="60" y="176" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">P1</text></switch></g><ellipse cx="260" cy="40" rx="40" ry="40" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 40px; margin-left: 221px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: normal; overflow-wrap: normal;">P2</div></div></div></foreignObject><text x="260" y="46" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">P2</text></switch></g><ellipse cx="455" cy="160" rx="40" ry="40" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 160px; margin-left: 416px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: normal; overflow-wrap: normal;">P3</div></div></div></foreignObject><text x="455" y="166" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">P3</text></switch></g><ellipse cx="430" cy="400" rx="40" ry="40" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 400px; margin-left: 391px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: normal; overflow-wrap: normal;">P4</div></div></div></foreignObject><text x="430" y="406" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">P4</text></switch></g><rect x="220" y="435" width="80" height="30" fill="none" stroke="none" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 1px; height: 1px; padding-top: 450px; margin-left: 260px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: nowrap;">table[0]</div></div></div></foreignObject><text x="260" y="456" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">table[0]</text></switch></g><rect x="0" y="265" width="80" height="30" fill="none" stroke="none" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 1px; height: 1px; padding-top: 280px; margin-left: 40px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: nowrap;">table[1]</div></div></div></foreignObject><text x="40" y="286" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">table[1]</text></switch></g><rect x="90" y="80" width="80" height="30" fill="none" stroke="none" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 1px; height: 1px; padding-top: 95px; margin-left: 130px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: nowrap;">table[2]</div></div></div></foreignObject><text x="130" y="101" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">table[2]</text></switch></g><rect x="344" y="80" width="80" height="30" fill="none" stroke="none" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 1px; height: 1px; padding-top: 95px; margin-left: 384px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: nowrap;">table[3]</div></div></div></foreignObject><text x="384" y="101" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">table[3]</text></switch></g><rect x="440" y="265" width="80" height="30" fill="none" stroke="none" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility" style="overflow: visible; text-align: left;"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 1px; height: 1px; padding-top: 280px; margin-left: 480px;"><div data-drawio-colors="color: rgb(0, 0, 0); " style="box-sizing: border-box; font-size: 0px; text-align: center;"><div style="display: inline-block; font-size: 19px; font-family: Helvetica; color: rgb(0, 0, 0); line-height: 1.2; pointer-events: all; white-space: nowrap;">table[4]</div></div></div></foreignObject><text x="480" y="286" fill="rgb(0, 0, 0)" font-family="Helvetica" font-size="19px" text-anchor="middle">table[4]</text></switch></g><ellipse cx="140" cy="372" rx="15" ry="15" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/><ellipse cx="390" cy="363.15" rx="15" ry="15" fill="rgb(255, 255, 255)" stroke="rgb(0, 0, 0)" pointer-events="all"/></g><switch><g requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"/><a transform="translate(0,-5)" xlink:href="https://www.diagrams.net/doc/faq/svg-export-text-problems" target="_blank"><text text-anchor="middle" font-size="10px" x="50%" y="100%">Text is not SVG - cannot display</text></a></switch></svg> \ No newline at end of file
--- a/Paper/soto-sigos.aux Thu May 05 22:32:45 2022 +0900 +++ b/Paper/soto-sigos.aux Thu May 12 15:44:39 2022 +0900 @@ -6,7 +6,7 @@ \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces メタ計算を可視化した CodeGear と DataGear\relax }}{2}{}\protected@file@percent } \providecommand*\caption@xref[2]{\@setref\relax\@undefined{#1}} \newlabel{fig:meta-cgdg}{{1}{2}} -\@writefile{toc}{\contentsline {section}{\numberline {3}\hskip 1zw{GearsAgda 形式で書く agda}}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3}\hskip 1zw{GearsAgda 形式で書く Agda}}{2}{}\protected@file@percent } \newlabel{agda-dg}{{1}{2}} \@writefile{lol}{\contentsline {lstlisting}{\numberline {1}{\ignorespaces Agdaでの Data Gear の定義}}{2}{}\protected@file@percent } \newlabel{agda-cg}{{2}{2}} @@ -15,16 +15,16 @@ \@writefile{lol}{\contentsline {lstlisting}{\numberline {3}{\ignorespaces Agdaでの 停止性が示せない CodeGear の例}}{2}{}\protected@file@percent } \newlabel{agda-exec-cg}{{4}{2}} \@writefile{lol}{\contentsline {lstlisting}{\numberline {4}{\ignorespaces Agdaでの CodeGear の初期化}}{2}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}{agda による Meta Gears}}{3}{}\protected@file@percent } +\@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{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 } +\@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 } \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}}
--- a/Paper/soto-sigos.fdb_latexmk Thu May 05 22:32:45 2022 +0900 +++ b/Paper/soto-sigos.fdb_latexmk Thu May 12 15:44:39 2022 +0900 @@ -1,18 +1,18 @@ # Fdb version 3 -["bibtex soto-sigos"] 1651754755 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1651755492 +["bibtex soto-sigos"] 1652336878 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1652337198 "./ipsjsort.bst" 1541385384 25930 d27669b348c8e9a5c1cc93168b2b5e89 "" "reference.bib" 1651750808 1954 450535f55d95a8a5d9e23cbab665da67 "" - "soto-sigos.aux" 1651755491 3788 a3a1a24c3dfa57ec20d5268a2cd1bf7c "latex" + "soto-sigos.aux" 1652337197 3788 e6360850c00625e0ba5d4ee670e67429 "latex" (generated) "soto-sigos.bbl" "soto-sigos.blg" -["dvipdf"] 1651755491 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1651755492 - "soto-sigos.dvi" 1651755491 59660 af25cc31678831b42d07032c653f6125 "latex" +["dvipdf"] 1652337198 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1652337198 + "soto-sigos.dvi" 1652337197 57752 bb64bc83944f0a338037faf6a48d46de "latex" (generated) "soto-sigos.pdf" -["latex"] 1651755491 "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" "soto-sigos.dvi" "soto-sigos" 1651755492 +["latex"] 1652337197 "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" "soto-sigos.dvi" "soto-sigos" 1652337198 "/dev/null" 0 -1 0 "" - "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" 1651755257 5146 1123a0eaf74dcc5e95f41207ee79342f "" + "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" 1652337196 5147 4ce2abc8b7f3d8237774c296b483cc6a "" "/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 "" @@ -163,20 +163,20 @@ "/usr/share/texmf-dist/tex/platex/japanese-otf/mlutf.sty" 1647806829 5572 2718e332ffca67065c2d32dda76f558f "" "/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 "" + "/var/lib/texmf/web2c/eptex/platex.fmt" 1652194558 2834361 f544bb78bd897b09030b7538a3a900b8 "" "fig/Dining.pdf" 1651685530 126415 635fdfd0d90894b78e5da1c3af0ef19f "" - "fig/cbc_codegear.pdf" 1651684831 30110 abae9d544b613e6b77036cde8327a20f "" + "fig/cbc_codegear.pdf" 1651684830 30110 abae9d544b613e6b77036cde8327a20f "" "ipsj.cls" 1650809266 142123 ecf81ecc4679baed6ac44a1571336871 "" "ipsjtech.sty" 1541385384 6572 e6269869e3c126f2d200f352d590509a "" - "soto-sigos.aux" 1651755491 3788 a3a1a24c3dfa57ec20d5268a2cd1bf7c "latex" - "soto-sigos.bbl" 1651754755 1492 2b5d2ad68939782993b214beefd4c97b "bibtex soto-sigos" - "soto-sigos.tex" 1651755257 5146 1123a0eaf74dcc5e95f41207ee79342f "" - "src/agda-dpp-impl.agda.replaced" 1651667549 2824 60454fbbf20d18849d1886385e94384b "" - "src/agda/cbc-agda.agda.replaced" 1651647471 1143 ab39102eb0f69d3b9f8e4e985a7c1e37 "" + "soto-sigos.aux" 1652337197 3788 e6360850c00625e0ba5d4ee670e67429 "latex" + "soto-sigos.bbl" 1652336878 1492 2b5d2ad68939782993b214beefd4c97b "bibtex soto-sigos" + "soto-sigos.tex" 1652337196 5147 4ce2abc8b7f3d8237774c296b483cc6a "" + "src/agda-dpp-impl.agda.replaced" 1651667548 2824 60454fbbf20d18849d1886385e94384b "" + "src/agda/cbc-agda.agda.replaced" 1651647470 1143 ab39102eb0f69d3b9f8e4e985a7c1e37 "" "tex/cbc.tex" 1651755242 2253 b995cbd082eafbc6aa946f8e4f2d1282 "" - "tex/cbc_agda.tex" 1651754681 4613 af1478d06e60552962ce70ffd3e86a78 "" - "tex/dpp_impl.tex" 1651755490 7192 bfce887cfeb07dfd06b40449d6215e5a "" - "tex/intro.tex" 1651753637 3466 0307f5084892aaa4629f720086cf9f6e "" + "tex/cbc_agda.tex" 1651825924 4613 3a8278c7e2d6b3cbdd4dd0dc6acde5d7 "" + "tex/dpp_impl.tex" 1651827650 6068 394a5d01cca5dcbce71d77b68b2248ea "" + "tex/intro.tex" 1651753636 3466 0307f5084892aaa4629f720086cf9f6e "" (generated) "soto-sigos.aux" "soto-sigos.dvi"
--- a/Paper/soto-sigos.log Thu May 05 22:32:45 2022 +0900 +++ b/Paper/soto-sigos.log Thu May 12 15:44:39 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) 5 MAY 2022 21:58 +This is e-pTeX, Version 3.141592653-p3.9.0-210218-2.6 (utf8.euc) (TeX Live 2021/Arch Linux) (preloaded format=platex 2022.5.10) 12 MAY 2022 15:33 entering extended mode \write18 enabled. file:line:error style messages enabled. @@ -3578,9 +3578,9 @@ ) (./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 + (./src/agda-dpp-impl.agda.replaced) (./src/agda-dpp-impl.agda.replaced consecutive: -) (./src/agda-dpp-impl.agda.replaced +[3]) (./src/agda-dpp-impl.agda.replaced consecutive: ) (./src/agda-dpp-impl.agda.replaced consecutive: @@ -3610,7 +3610,9 @@ (Font) No change on input line 8. LaTeX Font Info: Kanji font shape `JY1/hgt/m/it' undefined (Font) No change on input line 11. -) [5] (./soto-sigos.aux) +) [5 + +] (./soto-sigos.aux) LaTeX Font Warning: Some font shapes were not available, defaults substituted. @@ -3618,10 +3620,10 @@ Here is how much of TeX's memory you used: 13846 strings out of 478739 227762 string characters out of 5863952 - 1307732 words of memory out of 5000000 + 1282732 words of memory out of 5000000 31965 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 - 94i,10n,92p,483b,1986s stack positions out of 5000i,500n,10000p,200000b,80000s - -Output written on soto-sigos.dvi (5 pages, 59660 bytes). + 94i,11n,92p,483b,1986s stack positions out of 5000i,500n,10000p,200000b,80000s + +Output written on soto-sigos.dvi (5 pages, 57752 bytes).
--- a/Paper/soto-sigos.tex Thu May 05 22:32:45 2022 +0900 +++ b/Paper/soto-sigos.tex Thu May 12 15:44:39 2022 +0900 @@ -114,7 +114,7 @@ 今後はプロセスがすべてほかのプロセスの終了待ちになった場合に dead lock 状態になっていることを検知できるようにしたい． 加えて，assert の機能をつけて仕様通りの動作がされていることを検証したい． - + \nocite{*} \bibliographystyle{ipsjsort} \bibliography{reference}
--- a/Paper/tex/cbc_agda.tex Thu May 05 22:32:45 2022 +0900 +++ b/Paper/tex/cbc_agda.tex Thu May 12 15:44:39 2022 +0900 @@ -1,4 +1,4 @@ -\section{GearsAgda 形式で書く agda} +\section{GearsAgda 形式で書く Agda} CbC の継続の概念を取り入れた Agda の記法を説明する． Agdaでは関数の再帰呼び出しが可能であるが，CbCでは値が 帰って来ない．そのためAgda で実装を行う際には再帰呼び出しを行わないようにする． @@ -37,7 +37,7 @@ 実行時に減少しその関数がいずれ停止することを示す reducer を含めるようにしている． reducerを含めなかった際の Code Gear を Code \ref{agda-not-cg}に示す． -agdaではパターンマッチを行うことで場合分けを考えることができるが， +Agdaではパターンマッチを行うことで場合分けを考えることができるが， 受け取った Code Gear であるenvを with を使用してパターンマッチを試みている． パターンマッチ自体は可能だが，この方法だとAgdaが関数が停止することを認識できない． そのため，\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし @@ -51,7 +51,7 @@ Data Gear を作成する Code Gear を用いる． 加えて，実行なので命題の部分の最後が Env になっている． -\subsection{agda による Meta Gears} +\subsection{Agda による Meta Gears} 通常の Meta Gears はノーマルレベルの CodeGear， DataGear では扱えないメタレベルの計算を扱う単位である． 今回はモデル検査を行う際に使用する
--- a/Paper/tex/dpp_impl.tex Thu May 05 22:32:45 2022 +0900 +++ b/Paper/tex/dpp_impl.tex Thu May 12 15:44:39 2022 +0900 @@ -14,21 +14,7 @@ \label{fig:DPP} \end{figure} -問題の条件を以下に示す． - -\begin{itemize} - \item 哲学者が$N$人円卓についている（Nは2以上の自然数） - \item 哲学者の目の前には食べ物が用意されている - \item 哲学者の人数と同じだけのフォークがそれぞれ哲学者の間に置かれている - \item 哲学者はしばらく思考したのち，しばらく食事する動作を繰り返しおこなう - \item 思考から食事をする際には右のフォークを取ったのちに左のフォークを取ることで食事を始める - \item 食事するためには2本のフォークを取る必要があり，これを同時に取ることはできない - \item しばらくの食事から思考に戻る際には両手に持ったフォークをテーブルに置く - \item 最後に取ったフォークから先に置くため，左のフォークから置き，右のフォークを置く - \item 哲学者はこの食事と思考を繰り返し行い，哲学者同士が会話することはない -\end{itemize} - -つまり，哲学者は以下のようなフローを独立して並列に実行することとなる． +したがって，哲学者は以下のようなフローを独立して並列に繰り返し実行することとなる． \begin{enumerate} \item しばらくの間思考を行う @@ -37,7 +23,6 @@ \item 両方のフォークを取ったら，しばらく食事をする \item 思考に戻るために左手に持っているフォークをテーブルに置く \item 左手のフォークを置いたあとは右のフォークをテーブルに置く - \item しばらくの間思考する．つまり最初に戻る \end{enumerate} この際，すべての哲学者が同時に右のフォークを取った場合のことを考える． @@ -68,10 +53,8 @@ next-code は次に行う動作を格納している． Code \ref{agda-dpp-dg} が Data Gear になる． - phは前もって定義した一人の哲学者のプロセスの List になる． List になっている理由は，哲学者が複数人いるためである． - そのため実行時にListから一人ずつ取り出して実行をしていく． tableはテーブルに置いてあるフォークの状態のことで，