Skip to content

K
KTLA Study
Commit 856b8ffa authored by Kirill Smelkov's avatar Kirill Smelkov
Browse files
Options

.

parent 1584a247
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1 addition and 12449 deletions
.gitignore
View file @ 856b8ffa
......@@ -3,6 +3,7 @@
*.toolbox/*.tex
*.toolbox/*.pdf
*.toolbox/*.log
*.toolbox/*.aux
*.toolbox/*/*.tla
*.toolbox/*/*.dot
......
1Bit.toolbox/1Bit.aux deleted 100644 → 0
View file @ 1584a247
\relax
\gdef \@abspage@last{2}
1Bit.toolbox/1Bit.log deleted 100644 → 0
View file @ 1584a247
This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020/Debian) (preloaded format=pdflatex 2021.6.9) 9 FEB 2022 21:12
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
**1Bit.tex
(./1Bit.tex
LaTeX2e <2020-10-01> patch level 4
L3 programming layer <2021-01-09> xparse <2020-03-03>
(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2020/04/10 v1.4m Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo
File: size10.clo 2020/04/10 v1.4m Standard LaTeX file (size option)
)
\c@part=\count177
\c@section=\count178
\c@subsection=\count179
\c@subsubsection=\count180
\c@paragraph=\count181
\c@subparagraph=\count182
\c@figure=\count183
\c@table=\count184
\abovecaptionskip=\skip47
\belowcaptionskip=\skip48
\bibindent=\dimen138
) (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
Package: color 2020/02/24 v1.2b Standard LaTeX Color (DPC)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg
File: color.cfg 2016/01/02 v1.6 sample color configuration
)
Package color Info: Driver file: pdftex.def on input line 147.
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def
File: pdftex.def 2020/10/05 v1.2a Graphics/color driver for pdftex
)) (/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty
Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols)
\symlasy=\mathgroup4
LaTeX Font Info: Overwriting symbol font `lasy' in version `bold'
(Font) U/lasy/m/n --> U/lasy/b/n on input line 52.
) (/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty
Package: ifthen 2014/09/29 v1.1c Standard LaTeX ifthen package (DPC)
)
\symlength=\skip49
\equalswidth=\skip50
\charwidth=\skip51
\boxrulewd=\skip52
\boxlineht=\skip53
\boxruleht=\skip54
\boxruledp=\skip55
\pcalvspace=\skip56
\lcomindent=\skip57
\@xlen=\skip58
\templena=\skip59
\templenb=\skip60
\tempboxa=\box47
\vshadelen=\skip61
\boxwidth=\skip62
\multicommentdepth=\skip63
\c@pardepth=\count185
\tempsbox=\box48
\@cparht=\skip64
\@cpardp=\skip65
\xmcomlen=\skip66
\spacewidth=\skip67
\alignboxwidth=\skip68
\alignwidth=\skip69
\alignbox=\box49
\symtlaitalics=\mathgroup5
\c@tlx@ctr=\count186
(/usr/share/texlive/texmf-dist/tex/latex/tools/verbatim.sty
Package: verbatim 2020-07-07 v1.5u LaTeX2e package for verbatim enhancements
\every@verbatim=\toks15
\verbatim@line=\toks16
\verbatim@in@stream=\read2
) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2020-01-29 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count187
\l__pdf_internal_box=\box50
) (./1Bit.aux)
\openout1 = `1Bit.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count188
\scratchdimen=\dimen139
\scratchbox=\box51
\nofMPsegments=\count189
\nofMParguments=\count190
\everyMPshowfont=\toks17
\MPscratchCnt=\count191
\MPscratchDim=\dimen140
\MPnumerator=\count192
\makeMPintoPDFobject=\count193
\everyMPtoPDFconversion=\toks18
)
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <7> on input line 942.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <5> on input line 942.
LaTeX Font Info: Trying to load font information for U+lasy on input line 94
2.
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd
File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions
)
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <8> on input line 946.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <6> on input line 946.
LaTeX Font Info: Trying to load font information for OMS+cmr on input line 9
63.
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd
File: omscmr.fd 2019/12/16 v2.5j Standard LaTeX font definitions
)
LaTeX Font Info: Font shape `OMS/cmr/bx/n' in size <10> not available
(Font) Font shape `OMS/cmsy/b/n' tried instead on input line 963.
[1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
Overfull \hbox (13.43173pt too wide) in paragraph at lines 1087--1089
[][]
[]
Overfull \hbox (83.84805pt too wide) in paragraph at lines 1089--1095
[][][][]
[]
Overfull \hbox (34.86755pt too wide) in paragraph at lines 1095--1096
[][]
[]
[2] (./1Bit.aux) )
Here is how much of TeX's memory you used:
1332 strings out of 479304
18669 string characters out of 5869780
316173 words of memory out of 5000000
18554 multiletter control sequences out of 15000+600000
409463 words of font info for 50 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
44i,11n,50p,213b,320s stack positions out of 5000i,500n,10000p,200000b,80000s
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
/cmbsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx
10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></us
r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share
/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/font
s/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/amsfonts/cm/cmss8.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf
onts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti7.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/latxfont/lasy10.pfb>
Output written on 1Bit.pdf (2 pages, 172310 bytes).
PDF statistics:
79 PDF objects out of 1000 (max. 8388607)
57 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000)
1Bit.toolbox/1Bit.tex deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
1Bit.toolbox/1Bit___Model_1.launch deleted 100644 → 0
View file @ 1584a247
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="77"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="flag, pc, turn"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1ME!MutualExclusion"/>
<listEntry value="0Inv"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1ME!Spec"/>
<listEntry value="1ME!Liveness"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="8"/>
<stringAttribute key="modelExpressionEval" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="N;;1;0;0"/>
</listAttribute>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="2"/>
<stringAttribute key="postCondition" value=""/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<stringAttribute key="simuNumTraces" value="9223372036854775807"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="1Bit"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="true"/>
</launchConfiguration>
1Bit.toolbox/Model_1/1Bit.tla deleted 100644 → 0
View file @ 1584a247
-------------------------------- MODULE 1Bit --------------------------------
\* 1Bit implementation of mutual exclusion
EXTENDS Integers
CONSTANT N
ASSUME N \in Nat
Procs == 0..N
\* PlusCal options (wf)
(********
--algorithm 1BitProtocol {
variables flag = [i \in Procs |-> FALSE], turn = 0 ;
process (P \in Procs) {
ncs: while (TRUE) {
skip ;
enter: flag[self] := TRUE ;
e2: if (flag[1-self]) {
e3: if (self /= turn) {
e4: flag[self] := FALSE;
goto e3;
}
else {
goto enter;
}
};
cs: skip ;
exit: flag[self] := FALSE ;
x2: turn := 1-self;
}
}
}
********)
\* BEGIN TRANSLATION (chksum(pcal) = "5149a336" /\ chksum(tla) = "c5e4a370")
VARIABLES flag, turn, pc
vars == << flag, turn, pc >>
ProcSet == (Procs)
Init == (* Global variables *)
/\ flag = [i \in Procs |-> FALSE]
/\ turn = 0
/\ pc = [self \in ProcSet |-> "ncs"]
ncs(self) == /\ pc[self] = "ncs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "enter"]
/\ UNCHANGED << flag, turn >>
enter(self) == /\ pc[self] = "enter"
/\ flag' = [flag EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "e2"]
/\ turn' = turn
e2(self) == /\ pc[self] = "e2"
/\ IF flag[1-self]
THEN /\ pc' = [pc EXCEPT ![self] = "e3"]
ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
/\ UNCHANGED << flag, turn >>
e3(self) == /\ pc[self] = "e3"
/\ IF self /= turn
THEN /\ pc' = [pc EXCEPT ![self] = "e4"]
ELSE /\ pc' = [pc EXCEPT ![self] = "enter"]
/\ UNCHANGED << flag, turn >>
e4(self) == /\ pc[self] = "e4"
/\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "e3"]
/\ turn' = turn
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "exit"]
/\ UNCHANGED << flag, turn >>
exit(self) == /\ pc[self] = "exit"
/\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "x2"]
/\ turn' = turn
x2(self) == /\ pc[self] = "x2"
/\ turn' = 1-self
/\ pc' = [pc EXCEPT ![self] = "ncs"]
/\ flag' = flag
P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ e4(self)
\/ cs(self) \/ exit(self) \/ x2(self)
Next == (\E self \in Procs: P(self))
Spec == /\ Init /\ [][Next]_vars
/\ \A self \in Procs : WF_vars(P(self))
\* END TRANSLATION
--------
\* Invariant which implies MutualExclusion
\*Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] = "e2"))
\*Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] \in {"e2","e3"}))
Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] \in {"e2","e3","e4"}))
ME == INSTANCE MutualExclusionSpec WITH
pc <- [proc \in Procs |-> CASE pc[proc] = "cs" -> "cs"
[] pc[proc] \in {"enter","e2","e3","e4","e5"} -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
THEOREM Spec => []ME!MutualExclusion
THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 22:19:36 MSK 2022 by kirr
\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr
1Bit.toolbox/Model_1/MC.out deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
1Bit.toolbox/Model_1/MC_TE.out deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
1Bit.toolbox/Model_1/Model_1.dot deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
1Bit.toolbox/Model_1/Model_1_liveness.dot deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
1Bit.toolbox/Model_1/MutualExclusionSpec.tla deleted 100644 → 0
View file @ 1584a247
------------------------ MODULE MutualExclusionSpec ------------------------
\* Module MutualExclusionSpec provides general specification for mutual-exclusion problem.
\* Procs is set of processes.
\* Every process is assumed to loop and enter into "cs" state on every interation.
\* Non-critical state is represented as "non-cs".
\* When process decides it want to enter into critical-section, it first goes into "csentry" state.
CONSTANT Procs
VARIABLES pc
TypeOK == pc \in [Procs -> {"non-cs", "csentry", "cs"}]
vars == <<pc>>
\* All processes start from non-critical section.
Init == pc \in [Procs -> {"non-cs"}]
\* WantCS(proc) is action when proc decides that it wants to enter into critical section.
WantCS(proc) ==
/\ pc[proc] = "non-cs"
/\ pc' = [pc EXCEPT ![proc] = "csentry"]
\* EnterCS(proc) is action when proc enters critical section.
EnterCS(proc) ==
/\ pc[proc] = "csentry"
/\ \A i \in Procs \ {proc} : pc[i] /= "cs"
/\ pc' = [pc EXCEPT ![proc] = "cs"]
\* ExitCS(proc) is action when proc leaves critical section.
ExitCS(proc) ==
/\ pc[proc] = "cs"
/\ pc' = [pc EXCEPT ![proc] = "non-cs"]
Next == \E i \in Procs: WantCS(i) \/ EnterCS(i) \/ ExitCS(i)
Spec == /\ Init
/\ [][Next]_vars
/\ \A i \in Procs: ( \* fairness
\* not fair for WantCS - it can pause and even hang there
/\ SF_vars(EnterCS(i))
/\ SF_vars(ExitCS(i)))
----------------
\* MutualExclusion is invariant indicating that no two processes can be inside critical section at the same time.
MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "cs"))
\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
Liveness == \A i \in Procs:
/\ (pc[i] = "csentry") ~> (pc[i] = "cs")
/\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
\* XXX
MELive == \A i \in Procs :
\/ <>[](pc[i] = "ncs") \* stuck in non-cs
\/ []<>(pc[i] = "cs") \* keeps on entering cs
THEOREM Spec => []TypeOK
THEOREM Spec => []MutualExclusion
THEOREM Spec => Liveness
=============================================================================
\* Modification History
\* Last modified Thu Feb 10 12:43:05 MSK 2022 by kirr
\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr
1Bit.toolbox/MutualExclusionSpec.log deleted 100644 → 0
View file @ 1584a247
This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020/Debian) (preloaded format=pdflatex 2021.6.9) 10 FEB 2022 12:49
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
**MutualExclusionSpec.tex
(./MutualExclusionSpec.tex
LaTeX2e <2020-10-01> patch level 4
L3 programming layer <2021-01-09> xparse <2020-03-03>
(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2020/04/10 v1.4m Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo
File: size10.clo 2020/04/10 v1.4m Standard LaTeX file (size option)
)
\c@part=\count177
\c@section=\count178
\c@subsection=\count179
\c@subsubsection=\count180
\c@paragraph=\count181
\c@subparagraph=\count182
\c@figure=\count183
\c@table=\count184
\abovecaptionskip=\skip47
\belowcaptionskip=\skip48
\bibindent=\dimen138
) (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
Package: color 2020/02/24 v1.2b Standard LaTeX Color (DPC)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg
File: color.cfg 2016/01/02 v1.6 sample color configuration
)
Package color Info: Driver file: pdftex.def on input line 147.
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def
File: pdftex.def 2020/10/05 v1.2a Graphics/color driver for pdftex
)) (/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty
Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols)
\symlasy=\mathgroup4
LaTeX Font Info: Overwriting symbol font `lasy' in version `bold'
(Font) U/lasy/m/n --> U/lasy/b/n on input line 52.
) (/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty
Package: ifthen 2014/09/29 v1.1c Standard LaTeX ifthen package (DPC)
)
\symlength=\skip49
\equalswidth=\skip50
\charwidth=\skip51
\boxrulewd=\skip52
\boxlineht=\skip53
\boxruleht=\skip54
\boxruledp=\skip55
\pcalvspace=\skip56
\lcomindent=\skip57
\@xlen=\skip58
\templena=\skip59
\templenb=\skip60
\tempboxa=\box47
\vshadelen=\skip61
\boxwidth=\skip62
\multicommentdepth=\skip63
\c@pardepth=\count185
\tempsbox=\box48
\@cparht=\skip64
\@cpardp=\skip65
\xmcomlen=\skip66
\spacewidth=\skip67
\alignboxwidth=\skip68
\alignwidth=\skip69
\alignbox=\box49
\symtlaitalics=\mathgroup5
\c@tlx@ctr=\count186
(/usr/share/texlive/texmf-dist/tex/latex/tools/verbatim.sty
Package: verbatim 2020-07-07 v1.5u LaTeX2e package for verbatim enhancements
\every@verbatim=\toks15
\verbatim@line=\toks16
\verbatim@in@stream=\read2
) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2020-01-29 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count187
\l__pdf_internal_box=\box50
) (./MutualExclusionSpec.aux)
\openout1 = `MutualExclusionSpec.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count188
\scratchdimen=\dimen139
\scratchbox=\box51
\nofMPsegments=\count189
\nofMParguments=\count190
\everyMPshowfont=\toks17
\MPscratchCnt=\count191
\MPscratchDim=\dimen140
\MPnumerator=\count192
\makeMPintoPDFobject=\count193
\everyMPtoPDFconversion=\toks18
)
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <7> on input line 942.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <5> on input line 942.
LaTeX Font Info: Trying to load font information for U+lasy on input line 94
2.
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd
File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions
)
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <8> on input line 948.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <6> on input line 948.
Overfull \hbox (51.37141pt too wide) in paragraph at lines 1043--1051
[][][][]
[]
Overfull \hbox (56.19621pt too wide) in paragraph at lines 1053--1059
[][][][]
[]
[1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
Overfull \hbox (1.33424pt too wide) in paragraph at lines 1068--1074
[][][][]
[]
Overfull \hbox (14.0878pt too wide) in paragraph at lines 1074--1079
[][][][]
[]
Overfull \hbox (73.20253pt too wide) in paragraph at lines 1081--1087
[][][][]
[]
[2] (./MutualExclusionSpec.aux) )
Here is how much of TeX's memory you used:
1309 strings out of 479304
18453 string characters out of 5869780
313203 words of memory out of 5000000
18536 multiletter control sequences out of 15000+600000
408900 words of font info for 48 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
44i,10n,50p,200b,239s stack positions out of 5000i,500n,10000p,200000b,80000s
</usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
r5.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb><
/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmss8.pfb></usr/share/texlive/te
xmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/font
s/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/amsfonts/cm/cmti7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfo
nts/cm/cmti8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/lat
xfont/lasy10.pfb>
Output written on MutualExclusionSpec.pdf (2 pages, 148216 bytes).
PDF statistics:
71 PDF objects out of 1000 (max. 8388607)
51 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000)
1Bit.toolbox/MutualExclusionSpec.tex deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
Alternate.toolbox/Alternate.aux deleted 100644 → 0
View file @ 1584a247
\relax
\gdef \@abspage@last{2}
Alternate.toolbox/Alternate.log deleted 100644 → 0
View file @ 1584a247
This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020/Debian) (preloaded format=pdflatex 2021.6.9) 10 FEB 2022 12:40
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
**Alternate.tex
(./Alternate.tex
LaTeX2e <2020-10-01> patch level 4
L3 programming layer <2021-01-09> xparse <2020-03-03>
(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2020/04/10 v1.4m Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo
File: size10.clo 2020/04/10 v1.4m Standard LaTeX file (size option)
)
\c@part=\count177
\c@section=\count178
\c@subsection=\count179
\c@subsubsection=\count180
\c@paragraph=\count181
\c@subparagraph=\count182
\c@figure=\count183
\c@table=\count184
\abovecaptionskip=\skip47
\belowcaptionskip=\skip48
\bibindent=\dimen138
) (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
Package: color 2020/02/24 v1.2b Standard LaTeX Color (DPC)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg
File: color.cfg 2016/01/02 v1.6 sample color configuration
)
Package color Info: Driver file: pdftex.def on input line 147.
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def
File: pdftex.def 2020/10/05 v1.2a Graphics/color driver for pdftex
)) (/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty
Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols)
\symlasy=\mathgroup4
LaTeX Font Info: Overwriting symbol font `lasy' in version `bold'
(Font) U/lasy/m/n --> U/lasy/b/n on input line 52.
) (/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty
Package: ifthen 2014/09/29 v1.1c Standard LaTeX ifthen package (DPC)
)
\symlength=\skip49
\equalswidth=\skip50
\charwidth=\skip51
\boxrulewd=\skip52
\boxlineht=\skip53
\boxruleht=\skip54
\boxruledp=\skip55
\pcalvspace=\skip56
\lcomindent=\skip57
\@xlen=\skip58
\templena=\skip59
\templenb=\skip60
\tempboxa=\box47
\vshadelen=\skip61
\boxwidth=\skip62
\multicommentdepth=\skip63
\c@pardepth=\count185
\tempsbox=\box48
\@cparht=\skip64
\@cpardp=\skip65
\xmcomlen=\skip66
\spacewidth=\skip67
\alignboxwidth=\skip68
\alignwidth=\skip69
\alignbox=\box49
\symtlaitalics=\mathgroup5
\c@tlx@ctr=\count186
(/usr/share/texlive/texmf-dist/tex/latex/tools/verbatim.sty
Package: verbatim 2020-07-07 v1.5u LaTeX2e package for verbatim enhancements
\every@verbatim=\toks15
\verbatim@line=\toks16
\verbatim@in@stream=\read2
) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2020-01-29 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count187
\l__pdf_internal_box=\box50
) (./Alternate.aux)
\openout1 = `Alternate.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 939.
LaTeX Font Info: ... okay on input line 939.
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count188
\scratchdimen=\dimen139
\scratchbox=\box51
\nofMPsegments=\count189
\nofMParguments=\count190
\everyMPshowfont=\toks17
\MPscratchCnt=\count191
\MPscratchDim=\dimen140
\MPnumerator=\count192
\makeMPintoPDFobject=\count193
\everyMPtoPDFconversion=\toks18
)
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <7> on input line 942.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <5> on input line 942.
LaTeX Font Info: Trying to load font information for U+lasy on input line 94
2.
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd
File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions
)
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <8> on input line 947.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <6> on input line 947.
LaTeX Font Info: Trying to load font information for OMS+cmr on input line 9
79.
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd
File: omscmr.fd 2019/12/16 v2.5j Standard LaTeX font definitions
)
LaTeX Font Info: Font shape `OMS/cmr/bx/n' in size <10> not available
(Font) Font shape `OMS/cmsy/b/n' tried instead on input line 979.
[1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
Overfull \hbox (2.3747pt too wide) in paragraph at lines 1085--1087
[][]
[]
Overfull \hbox (2.57756pt too wide) in paragraph at lines 1087--1088
[][]
[]
[2] (./Alternate.aux) )
Here is how much of TeX's memory you used:
1331 strings out of 479304
18714 string characters out of 5869780
316183 words of memory out of 5000000
18554 multiletter control sequences out of 15000+600000
409464 words of font info for 50 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
44i,10n,50p,223b,320s stack positions out of 5000i,500n,10000p,200000b,80000s
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc
10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/
share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/t
exlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dis
t/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/texmf-dist/fonts/type1/
public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti7.p
fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></us
r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/latxfont/lasy10.pfb>
Output written on Alternate.pdf (2 pages, 171121 bytes).
PDF statistics:
79 PDF objects out of 1000 (max. 8388607)
57 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000)
Alternate.toolbox/Alternate.tex deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
Alternate.toolbox/Model_1/Alternate.tla deleted 100644 → 0
View file @ 1584a247
----------------------------- MODULE Alternate -----------------------------
\* Module Alternate specifies turn-based solution for mutual-exclusion problem.
EXTENDS Integers
CONSTANT Procs
\*ASSUME \E N \in Nat : Procs = 0..N
ASSUME \E N \in 0..10 : Procs = 0..N
Max(s) == CHOOSE x \in s :
/\ \A y \in s: y =< x
/\ \E z \in s: z = x
NProcs == Max(Procs)+1 \* XXX assumes procs are 0..N
(********
--fair algorithm Alternate {
variable turn \in Procs;
process (p \in Procs) {
ncs: while (TRUE) {
skip; \* non-critical section
enter: await turn = self;
cs: skip; \* critical section
\* exit: turn := 1 - self
exit: turn := ((self + 1) % NProcs)
};
}
}
********)
\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "dc237cc6")
VARIABLES turn, pc
vars == << turn, pc >>
ProcSet == (Procs)
Init == (* Global variables *)
/\ turn \in Procs
/\ pc = [self \in ProcSet |-> "ncs"]
ncs(self) == /\ pc[self] = "ncs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "enter"]
/\ turn' = turn
enter(self) == /\ pc[self] = "enter"
/\ turn = self
/\ pc' = [pc EXCEPT ![self] = "cs"]
/\ turn' = turn
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "exit"]
/\ turn' = turn
exit(self) == /\ pc[self] = "exit"
/\ turn' = ((self + 1) % NProcs)
/\ pc' = [pc EXCEPT ![self] = "ncs"]
p(self) == ncs(self) \/ enter(self) \/ cs(self) \/ exit(self)
Next == (\E self \in Procs: p(self))
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
\* END TRANSLATION
--------
ME == INSTANCE MutualExclusionSpec WITH
pc <- [proc \in Procs |-> CASE pc[proc] = "cs" -> "cs"
[] pc[proc] = "enter" -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
THEOREM Spec => []ME!MutualExclusion
THEOREM Spec => ME!Liveness
KeepsEnteringCS == \A i \in Procs : []<>(pc[i] = "cs")
Stuck == \E i \in Procs : <>[](pc[i] = "ncs")
=============================================================================
\* Modification History
\* Last modified Thu Feb 10 12:38:33 MSK 2022 by kirr
\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr
Alternate.toolbox/Model_1/MC.out deleted 100644 → 0
View file @ 1584a247
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 117 and seed -6658046656861843322 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 89195] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module MutualExclusionSpec
Semantic processing of module Alternate
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-02-10 12:38:45)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 5 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 2 distinct states generated at 2022-02-10 12:38:46.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(5) at 2022-02-10 12:38:46: 26 states generated, 16 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 5 branches of temporal properties for the complete state space with 80 total distinct states at (2022-02-10 12:38:46)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 00s at 2022-02-10 12:38:46
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2193:0 @!@!@
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val = 8.7E-18
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2022-02-10 12:38:46
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 40, col 1 to line 40, col 4 of module Alternate>: 2:2
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 41, col 12 to line 41, col 25 of module Alternate: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 42, col 12 to line 42, col 44 of module Alternate: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 42, col 17 to line 42, col 44 of module Alternate: 2:4
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 42, col 27 to line 42, col 33 of module Alternate: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 8:18
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 44, col 17 to line 44, col 32 of module Alternate: 62
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 44, col 17 to line 44, col 24 of module Alternate: 44
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 45, col 17 to line 45, col 20 of module Alternate: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 46, col 17 to line 46, col 51 of module Alternate: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 47, col 17 to line 47, col 28 of module Alternate: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<enter line 49, col 1 to line 49, col 11 of module Alternate>: 3:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 49, col 19 to line 49, col 36 of module Alternate: 50
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 49, col 19 to line 49, col 26 of module Alternate: 44
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 50, col 19 to line 50, col 29 of module Alternate: 22
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 50, col 19 to line 50, col 22 of module Alternate: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 50, col 26 to line 50, col 29 of module Alternate: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 51, col 19 to line 51, col 50 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 52, col 19 to line 52, col 30 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<cs line 54, col 1 to line 54, col 8 of module Alternate>: 3:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 54, col 16 to line 54, col 30 of module Alternate: 50
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 54, col 16 to line 54, col 23 of module Alternate: 44
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 55, col 16 to line 55, col 19 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 56, col 16 to line 56, col 49 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 57, col 16 to line 57, col 27 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:4
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 59, col 18 to line 59, col 34 of module Alternate: 48
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 59, col 18 to line 59, col 25 of module Alternate: 44
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 60, col 18 to line 60, col 46 of module Alternate: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 61, col 18 to line 61, col 50 of module Alternate: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<inv_1644485925128910000 line 10, col 1 to line 10, col 23 of module MC>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 11, col 1 to line 11, col 18 of module MC: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 78, col 23 to line 80, col 82 of module Alternate: 83:94
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 78, col 33 to line 78, col 37 of module Alternate: 83
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 77, col 1 to line 80, col 82 of module Alternate: 42
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 47, col 20 to line 47, col 84 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 38 to line 47, col 84 of module MutualExclusionSpec: 64
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 39 to line 47, col 44 of module MutualExclusionSpec: 64
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 50 to line 47, col 84 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 47, col 52 to line 47, col 83 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||||line 47, col 53 to line 47, col 64 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||||line 47, col 71 to line 47, col 82 of module MutualExclusionSpec: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 31 to line 47, col 35 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<inv_1644485925128911000 line 14, col 1 to line 14, col 23 of module MC>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 15, col 1 to line 15, col 45 of module MC: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 15, col 18 to line 15, col 45 of module MC: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 15, col 19 to line 15, col 30 of module MC: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 15, col 37 to line 15, col 44 of module MC: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 15, col 10 to line 15, col 14 of module MC: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(5) at 2022-02-10 12:38:46: 26 states generated (1 173 s/min), 16 distinct states found (722 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
26 states generated, 16 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 5.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 1340ms at (2022-02-10 12:38:46)
@!@!@ENDMSG 2186 @!@!@
Alternate.toolbox/Model_1/MC_TE.out deleted 100644 → 0
View file @ 1584a247
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 117 and seed -6658046656861843322 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 89195] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module MutualExclusionSpec
Semantic processing of module Alternate
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-02-10 12:38:45)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 5 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 2 distinct states generated at 2022-02-10 12:38:46.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(5) at 2022-02-10 12:38:46: 26 states generated, 16 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 5 branches of temporal properties for the complete state space with 80 total distinct states at (2022-02-10 12:38:46)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 00s at 2022-02-10 12:38:46
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2193:0 @!@!@
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val = 8.7E-18
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2022-02-10 12:38:46
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 40, col 1 to line 40, col 4 of module Alternate>: 2:2
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 41, col 12 to line 41, col 25 of module Alternate: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 42, col 12 to line 42, col 44 of module Alternate: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 42, col 17 to line 42, col 44 of module Alternate: 2:4
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 42, col 27 to line 42, col 33 of module Alternate: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 8:18
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 44, col 17 to line 44, col 32 of module Alternate: 62
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 44, col 17 to line 44, col 24 of module Alternate: 44
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 45, col 17 to line 45, col 20 of module Alternate: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 46, col 17 to line 46, col 51 of module Alternate: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 47, col 17 to line 47, col 28 of module Alternate: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<enter line 49, col 1 to line 49, col 11 of module Alternate>: 3:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 49, col 19 to line 49, col 36 of module Alternate: 50
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 49, col 19 to line 49, col 26 of module Alternate: 44
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 50, col 19 to line 50, col 29 of module Alternate: 22
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 50, col 19 to line 50, col 22 of module Alternate: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 50, col 26 to line 50, col 29 of module Alternate: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 51, col 19 to line 51, col 50 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 52, col 19 to line 52, col 30 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<cs line 54, col 1 to line 54, col 8 of module Alternate>: 3:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 54, col 16 to line 54, col 30 of module Alternate: 50
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 54, col 16 to line 54, col 23 of module Alternate: 44
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 55, col 16 to line 55, col 19 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 56, col 16 to line 56, col 49 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 57, col 16 to line 57, col 27 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:4
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 59, col 18 to line 59, col 34 of module Alternate: 48
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 59, col 18 to line 59, col 25 of module Alternate: 44
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 60, col 18 to line 60, col 46 of module Alternate: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 61, col 18 to line 61, col 50 of module Alternate: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<inv_1644485925128910000 line 10, col 1 to line 10, col 23 of module MC>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 11, col 1 to line 11, col 18 of module MC: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 78, col 23 to line 80, col 82 of module Alternate: 83:94
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 78, col 33 to line 78, col 37 of module Alternate: 83
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 77, col 1 to line 80, col 82 of module Alternate: 42
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 47, col 20 to line 47, col 84 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 38 to line 47, col 84 of module MutualExclusionSpec: 64
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 39 to line 47, col 44 of module MutualExclusionSpec: 64
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 50 to line 47, col 84 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 47, col 52 to line 47, col 83 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||||line 47, col 53 to line 47, col 64 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||||line 47, col 71 to line 47, col 82 of module MutualExclusionSpec: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 31 to line 47, col 35 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<inv_1644485925128911000 line 14, col 1 to line 14, col 23 of module MC>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 15, col 1 to line 15, col 45 of module MC: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 15, col 18 to line 15, col 45 of module MC: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 15, col 19 to line 15, col 30 of module MC: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 15, col 37 to line 15, col 44 of module MC: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 15, col 10 to line 15, col 14 of module MC: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(5) at 2022-02-10 12:38:46: 26 states generated (1 173 s/min), 16 distinct states found (722 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
26 states generated, 16 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 5.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 1340ms at (2022-02-10 12:38:46)
@!@!@ENDMSG 2186 @!@!@
Alternate.toolbox/Model_1/Model_1.dot deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
Alternate.toolbox/Model_1/Model_1_liveness.dot deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
Alternate.toolbox/Model_1/MutualExclusionSpec.tla deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
Alternate.toolbox/MutualExclusionSpec.log deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
Alternate.toolbox/MutualExclusionSpec.tex deleted 100644 → 0
View file @ 1584a247
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment
GitLab Nexedi Edition | About GitLab | About Nexedi | 沪ICP备2021021310号-2 | 沪ICP备2021021310号-7