commit 70c944a2b7e90a51b4996ae793329973676bdec4 Author: hellerve Date: Thu Dec 27 16:07:37 2018 +0100 i... dont know what to commit diff --git a/DieHard.tla b/DieHard.tla new file mode 100644 index 0000000..a2e2c9c --- /dev/null +++ b/DieHard.tla @@ -0,0 +1,46 @@ +------------------------------ MODULE DieHard ------------------------------ + +EXTENDS Integers +VARIABLES small, big + +TypeOK == /\ small \in 0..3 + /\ big \in 0..5 + + Init == /\ small = 0 + /\ big = 0 + + FillSmall == /\ big' = big + /\ small' = 3 + + FillBig == /\ big' = 5 + /\ small' = small + + EmptySmall == /\ big' = big + /\ small' = 0 + + EmptyBig == /\ big' = 0 + /\ small' = small + + SmallToBig == IF big + small <= 5 + THEN /\ big' = big + small + /\ small' = 0 + ELSE /\ big' = 5 + /\ small' = small - (5 - big) + + BigToSmall == IF big + small <= 3 + THEN /\ big' = 0 + /\ small' = big + small + ELSE /\ small' = 3 + /\ big' = big - (3 - small) + + Next == \/ FillSmall + \/ FillBig + \/ EmptySmall + \/ EmptyBig + \/ SmallToBig + \/ BigToSmall + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 16:33:15 CET 2018 by veitheller +\* Created Fri Dec 21 16:16:46 CET 2018 by veitheller diff --git a/DieHard.toolbox/.project b/DieHard.toolbox/.project new file mode 100644 index 0000000..9e00a41 --- /dev/null +++ b/DieHard.toolbox/.project @@ -0,0 +1,24 @@ + + + DieHard + + + + + + toolbox.builder.TLAParserBuilder + + + + + + toolbox.natures.TLANature + + + + DieHard.tla + 1 + PARENT-1-PROJECT_LOC/DieHard.tla + + + diff --git a/DieHard.toolbox/.settings/org.lamport.tla.toolbox.prefs b/DieHard.toolbox/.settings/org.lamport.tla.toolbox.prefs new file mode 100644 index 0000000..f80647d --- /dev/null +++ b/DieHard.toolbox/.settings/org.lamport.tla.toolbox.prefs @@ -0,0 +1,2 @@ +ProjectRootFile=PARENT-1-PROJECT_LOC/DieHard.tla +eclipse.preferences.version=1 diff --git a/DieHard.toolbox/DieHard___Model_1.launch b/DieHard.toolbox/DieHard___Model_1.launch new file mode 100644 index 0000000..b2f6597 --- /dev/null +++ b/DieHard.toolbox/DieHard___Model_1.launch @@ -0,0 +1,46 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406431357.launch b/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406431357.launch new file mode 100644 index 0000000..fccdd07 --- /dev/null +++ b/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406431357.launch @@ -0,0 +1,43 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406506746.launch b/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406506746.launch new file mode 100644 index 0000000..6906605 --- /dev/null +++ b/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406506746.launch @@ -0,0 +1,45 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406592577.launch b/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406592577.launch new file mode 100644 index 0000000..38e2b4b --- /dev/null +++ b/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406592577.launch @@ -0,0 +1,46 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DieHard.toolbox/Model_1/DieHard.tla b/DieHard.toolbox/Model_1/DieHard.tla new file mode 100644 index 0000000..a2e2c9c --- /dev/null +++ b/DieHard.toolbox/Model_1/DieHard.tla @@ -0,0 +1,46 @@ +------------------------------ MODULE DieHard ------------------------------ + +EXTENDS Integers +VARIABLES small, big + +TypeOK == /\ small \in 0..3 + /\ big \in 0..5 + + Init == /\ small = 0 + /\ big = 0 + + FillSmall == /\ big' = big + /\ small' = 3 + + FillBig == /\ big' = 5 + /\ small' = small + + EmptySmall == /\ big' = big + /\ small' = 0 + + EmptyBig == /\ big' = 0 + /\ small' = small + + SmallToBig == IF big + small <= 5 + THEN /\ big' = big + small + /\ small' = 0 + ELSE /\ big' = 5 + /\ small' = small - (5 - big) + + BigToSmall == IF big + small <= 3 + THEN /\ big' = 0 + /\ small' = big + small + ELSE /\ small' = 3 + /\ big' = big - (3 - small) + + Next == \/ FillSmall + \/ FillBig + \/ EmptySmall + \/ EmptyBig + \/ SmallToBig + \/ BigToSmall + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 16:33:15 CET 2018 by veitheller +\* Created Fri Dec 21 16:16:46 CET 2018 by veitheller diff --git a/DieHard.toolbox/Model_1/MC.cfg b/DieHard.toolbox/Model_1/MC.cfg new file mode 100644 index 0000000..4259c62 --- /dev/null +++ b/DieHard.toolbox/Model_1/MC.cfg @@ -0,0 +1,11 @@ +\* INIT definition +INIT +init_154540658308222000 +\* NEXT definition +NEXT +next_154540658308223000 +\* INVARIANT definition +INVARIANT +inv_154540658308324000 +inv_154540658308325000 +\* Generated on Fri Dec 21 16:36:23 CET 2018 \ No newline at end of file diff --git a/DieHard.toolbox/Model_1/MC.tla b/DieHard.toolbox/Model_1/MC.tla new file mode 100644 index 0000000..a791433 --- /dev/null +++ b/DieHard.toolbox/Model_1/MC.tla @@ -0,0 +1,22 @@ +---- MODULE MC ---- +EXTENDS DieHard, TLC + +\* INIT definition @modelBehaviorInit:0 +init_154540658308222000 == +Init +---- +\* NEXT definition @modelBehaviorNext:0 +next_154540658308223000 == +Next +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154540658308324000 == +TypeOK +---- +\* INVARIANT definition @modelCorrectnessInvariants:1 +inv_154540658308325000 == +big # 4 +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 16:36:23 CET 2018 by veitheller diff --git a/DieHard.toolbox/Model_1_SnapShot_1545406431357/DieHard.tla b/DieHard.toolbox/Model_1_SnapShot_1545406431357/DieHard.tla new file mode 100644 index 0000000..a2e2c9c --- /dev/null +++ b/DieHard.toolbox/Model_1_SnapShot_1545406431357/DieHard.tla @@ -0,0 +1,46 @@ +------------------------------ MODULE DieHard ------------------------------ + +EXTENDS Integers +VARIABLES small, big + +TypeOK == /\ small \in 0..3 + /\ big \in 0..5 + + Init == /\ small = 0 + /\ big = 0 + + FillSmall == /\ big' = big + /\ small' = 3 + + FillBig == /\ big' = 5 + /\ small' = small + + EmptySmall == /\ big' = big + /\ small' = 0 + + EmptyBig == /\ big' = 0 + /\ small' = small + + SmallToBig == IF big + small <= 5 + THEN /\ big' = big + small + /\ small' = 0 + ELSE /\ big' = 5 + /\ small' = small - (5 - big) + + BigToSmall == IF big + small <= 3 + THEN /\ big' = 0 + /\ small' = big + small + ELSE /\ small' = 3 + /\ big' = big - (3 - small) + + Next == \/ FillSmall + \/ FillBig + \/ EmptySmall + \/ EmptyBig + \/ SmallToBig + \/ BigToSmall + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 16:33:15 CET 2018 by veitheller +\* Created Fri Dec 21 16:16:46 CET 2018 by veitheller diff --git a/DieHard.toolbox/Model_1_SnapShot_1545406431357/MC.cfg b/DieHard.toolbox/Model_1_SnapShot_1545406431357/MC.cfg new file mode 100644 index 0000000..e3f8031 --- /dev/null +++ b/DieHard.toolbox/Model_1_SnapShot_1545406431357/MC.cfg @@ -0,0 +1,7 @@ +\* INIT definition +INIT +init_154540641525210000 +\* NEXT definition +NEXT +next_154540641525211000 +\* Generated on Fri Dec 21 16:33:35 CET 2018 \ No newline at end of file diff --git a/DieHard.toolbox/Model_1_SnapShot_1545406431357/MC.tla b/DieHard.toolbox/Model_1_SnapShot_1545406431357/MC.tla new file mode 100644 index 0000000..f82c8f8 --- /dev/null +++ b/DieHard.toolbox/Model_1_SnapShot_1545406431357/MC.tla @@ -0,0 +1,14 @@ +---- MODULE MC ---- +EXTENDS DieHard, TLC + +\* INIT definition @modelBehaviorInit:0 +init_154540641525210000 == +Init +---- +\* NEXT definition @modelBehaviorNext:0 +next_154540641525211000 == +Next +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 16:33:35 CET 2018 by veitheller diff --git a/DieHard.toolbox/Model_1_SnapShot_1545406506746/DieHard.tla b/DieHard.toolbox/Model_1_SnapShot_1545406506746/DieHard.tla new file mode 100644 index 0000000..a2e2c9c --- /dev/null +++ b/DieHard.toolbox/Model_1_SnapShot_1545406506746/DieHard.tla @@ -0,0 +1,46 @@ +------------------------------ MODULE DieHard ------------------------------ + +EXTENDS Integers +VARIABLES small, big + +TypeOK == /\ small \in 0..3 + /\ big \in 0..5 + + Init == /\ small = 0 + /\ big = 0 + + FillSmall == /\ big' = big + /\ small' = 3 + + FillBig == /\ big' = 5 + /\ small' = small + + EmptySmall == /\ big' = big + /\ small' = 0 + + EmptyBig == /\ big' = 0 + /\ small' = small + + SmallToBig == IF big + small <= 5 + THEN /\ big' = big + small + /\ small' = 0 + ELSE /\ big' = 5 + /\ small' = small - (5 - big) + + BigToSmall == IF big + small <= 3 + THEN /\ big' = 0 + /\ small' = big + small + ELSE /\ small' = 3 + /\ big' = big - (3 - small) + + Next == \/ FillSmall + \/ FillBig + \/ EmptySmall + \/ EmptyBig + \/ SmallToBig + \/ BigToSmall + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 16:33:15 CET 2018 by veitheller +\* Created Fri Dec 21 16:16:46 CET 2018 by veitheller diff --git a/DieHard.toolbox/Model_1_SnapShot_1545406506746/MC.cfg b/DieHard.toolbox/Model_1_SnapShot_1545406506746/MC.cfg new file mode 100644 index 0000000..4bfc4e8 --- /dev/null +++ b/DieHard.toolbox/Model_1_SnapShot_1545406506746/MC.cfg @@ -0,0 +1,10 @@ +\* INIT definition +INIT +init_154540649359515000 +\* NEXT definition +NEXT +next_154540649359516000 +\* INVARIANT definition +INVARIANT +inv_154540649359517000 +\* Generated on Fri Dec 21 16:34:53 CET 2018 \ No newline at end of file diff --git a/DieHard.toolbox/Model_1_SnapShot_1545406506746/MC.tla b/DieHard.toolbox/Model_1_SnapShot_1545406506746/MC.tla new file mode 100644 index 0000000..38304f3 --- /dev/null +++ b/DieHard.toolbox/Model_1_SnapShot_1545406506746/MC.tla @@ -0,0 +1,18 @@ +---- MODULE MC ---- +EXTENDS DieHard, TLC + +\* INIT definition @modelBehaviorInit:0 +init_154540649359515000 == +Init +---- +\* NEXT definition @modelBehaviorNext:0 +next_154540649359516000 == +Next +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154540649359517000 == +TypeOK +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 16:34:53 CET 2018 by veitheller diff --git a/DieHard.toolbox/Model_1_SnapShot_1545406592577/DieHard.tla b/DieHard.toolbox/Model_1_SnapShot_1545406592577/DieHard.tla new file mode 100644 index 0000000..a2e2c9c --- /dev/null +++ b/DieHard.toolbox/Model_1_SnapShot_1545406592577/DieHard.tla @@ -0,0 +1,46 @@ +------------------------------ MODULE DieHard ------------------------------ + +EXTENDS Integers +VARIABLES small, big + +TypeOK == /\ small \in 0..3 + /\ big \in 0..5 + + Init == /\ small = 0 + /\ big = 0 + + FillSmall == /\ big' = big + /\ small' = 3 + + FillBig == /\ big' = 5 + /\ small' = small + + EmptySmall == /\ big' = big + /\ small' = 0 + + EmptyBig == /\ big' = 0 + /\ small' = small + + SmallToBig == IF big + small <= 5 + THEN /\ big' = big + small + /\ small' = 0 + ELSE /\ big' = 5 + /\ small' = small - (5 - big) + + BigToSmall == IF big + small <= 3 + THEN /\ big' = 0 + /\ small' = big + small + ELSE /\ small' = 3 + /\ big' = big - (3 - small) + + Next == \/ FillSmall + \/ FillBig + \/ EmptySmall + \/ EmptyBig + \/ SmallToBig + \/ BigToSmall + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 16:33:15 CET 2018 by veitheller +\* Created Fri Dec 21 16:16:46 CET 2018 by veitheller diff --git a/DieHard.toolbox/Model_1_SnapShot_1545406592577/MC.cfg b/DieHard.toolbox/Model_1_SnapShot_1545406592577/MC.cfg new file mode 100644 index 0000000..4259c62 --- /dev/null +++ b/DieHard.toolbox/Model_1_SnapShot_1545406592577/MC.cfg @@ -0,0 +1,11 @@ +\* INIT definition +INIT +init_154540658308222000 +\* NEXT definition +NEXT +next_154540658308223000 +\* INVARIANT definition +INVARIANT +inv_154540658308324000 +inv_154540658308325000 +\* Generated on Fri Dec 21 16:36:23 CET 2018 \ No newline at end of file diff --git a/DieHard.toolbox/Model_1_SnapShot_1545406592577/MC.tla b/DieHard.toolbox/Model_1_SnapShot_1545406592577/MC.tla new file mode 100644 index 0000000..a791433 --- /dev/null +++ b/DieHard.toolbox/Model_1_SnapShot_1545406592577/MC.tla @@ -0,0 +1,22 @@ +---- MODULE MC ---- +EXTENDS DieHard, TLC + +\* INIT definition @modelBehaviorInit:0 +init_154540658308222000 == +Init +---- +\* NEXT definition @modelBehaviorNext:0 +next_154540658308223000 == +Next +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154540658308324000 == +TypeOK +---- +\* INVARIANT definition @modelCorrectnessInvariants:1 +inv_154540658308325000 == +big # 4 +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 16:36:23 CET 2018 by veitheller diff --git a/README.md b/README.md new file mode 100644 index 0000000..5bbfee4 --- /dev/null +++ b/README.md @@ -0,0 +1,4 @@ +# tla-notes + +Notes and doodles I collected while learning TLA+ with the [Video +Course](http://lamport.azurewebsites.net/video/videos.html). diff --git a/SimpleProgram.pdf b/SimpleProgram.pdf new file mode 100644 index 0000000..993e481 Binary files /dev/null and b/SimpleProgram.pdf differ diff --git a/SimpleProgram.tla b/SimpleProgram.tla new file mode 100644 index 0000000..b7db42b --- /dev/null +++ b/SimpleProgram.tla @@ -0,0 +1,21 @@ +--------------------------- MODULE SimpleProgram --------------------------- + +EXTENDS Integers +VARIABLES i, pc + +Init == (pc = "start") /\ (i = 0) + +Pick == /\ pc = "start" + /\ i' \in 0..1000 + /\ pc' = "middle" + +Add1 == /\ pc = "middle" + /\ i' = i + 1 + /\ pc' = "done" + +Next == Pick \/ Add1 + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 15:46:32 CET 2018 by veitheller +\* Created Fri Dec 21 15:45:07 CET 2018 by veitheller diff --git a/TCommit.pdf b/TCommit.pdf new file mode 100644 index 0000000..aad8983 Binary files /dev/null and b/TCommit.pdf differ diff --git a/TCommit.tla b/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TCommit.toolbox/.project b/TCommit.toolbox/.project new file mode 100644 index 0000000..c3a7cdd --- /dev/null +++ b/TCommit.toolbox/.project @@ -0,0 +1,24 @@ + + + TCommit + + + + + + toolbox.builder.TLAParserBuilder + + + + + + toolbox.natures.TLANature + + + + TCommit.tla + 1 + PARENT-1-PROJECT_LOC/TCommit.tla + + + diff --git a/TCommit.toolbox/.settings/org.lamport.tla.toolbox.prefs b/TCommit.toolbox/.settings/org.lamport.tla.toolbox.prefs new file mode 100644 index 0000000..cc1d253 --- /dev/null +++ b/TCommit.toolbox/.settings/org.lamport.tla.toolbox.prefs @@ -0,0 +1,2 @@ +ProjectRootFile=PARENT-1-PROJECT_LOC/TCommit.tla +eclipse.preferences.version=1 diff --git a/TCommit.toolbox/Model_1/MC.cfg b/TCommit.toolbox/Model_1/MC.cfg new file mode 100644 index 0000000..b6e7eae --- /dev/null +++ b/TCommit.toolbox/Model_1/MC.cfg @@ -0,0 +1,14 @@ +\* CONSTANT definitions +CONSTANT +RM <- const_154541058889823000 +\* INIT definition +INIT +init_154541058889824000 +\* NEXT definition +NEXT +next_154541058889825000 +\* INVARIANT definition +INVARIANT +inv_154541058889826000 +inv_154541058889827000 +\* Generated on Fri Dec 21 17:43:08 CET 2018 \ No newline at end of file diff --git a/TCommit.toolbox/Model_1/MC.tla b/TCommit.toolbox/Model_1/MC.tla new file mode 100644 index 0000000..c09bec9 --- /dev/null +++ b/TCommit.toolbox/Model_1/MC.tla @@ -0,0 +1,27 @@ +---- MODULE MC ---- +EXTENDS TCommit, TLC + +\* CONSTANT definitions @modelParameterConstants:0RM +const_154541058889823000 == +{"r1","r2","r3"} +---- + +\* INIT definition @modelBehaviorInit:0 +init_154541058889824000 == +TCInit +---- +\* NEXT definition @modelBehaviorNext:0 +next_154541058889825000 == +TCNext +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154541058889826000 == +TCTypeOK +---- +\* INVARIANT definition @modelCorrectnessInvariants:1 +inv_154541058889827000 == +TCConsistent +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 17:43:08 CET 2018 by veitheller diff --git a/TCommit.toolbox/Model_1/TCommit.tla b/TCommit.toolbox/Model_1/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TCommit.toolbox/Model_1/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TCommit.toolbox/Model_1_SnapShot_1545410479536/MC.cfg b/TCommit.toolbox/Model_1_SnapShot_1545410479536/MC.cfg new file mode 100644 index 0000000..13c6793 --- /dev/null +++ b/TCommit.toolbox/Model_1_SnapShot_1545410479536/MC.cfg @@ -0,0 +1,13 @@ +\* CONSTANT definitions +CONSTANT +RM <- const_15454104746206000 +\* INIT definition +INIT +init_15454104746207000 +\* NEXT definition +NEXT +next_15454104746208000 +\* INVARIANT definition +INVARIANT +inv_15454104746209000 +\* Generated on Fri Dec 21 17:41:14 CET 2018 \ No newline at end of file diff --git a/TCommit.toolbox/Model_1_SnapShot_1545410479536/MC.tla b/TCommit.toolbox/Model_1_SnapShot_1545410479536/MC.tla new file mode 100644 index 0000000..4de6902 --- /dev/null +++ b/TCommit.toolbox/Model_1_SnapShot_1545410479536/MC.tla @@ -0,0 +1,23 @@ +---- MODULE MC ---- +EXTENDS TCommit, TLC + +\* CONSTANT definitions @modelParameterConstants:0RM +const_15454104746206000 == +{"r1","r2","r3"} +---- + +\* INIT definition @modelBehaviorInit:0 +init_15454104746207000 == +TCInit +---- +\* NEXT definition @modelBehaviorNext:0 +next_15454104746208000 == +TCNext +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_15454104746209000 == +TCTypeOK +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 17:41:14 CET 2018 by veitheller diff --git a/TCommit.toolbox/Model_1_SnapShot_1545410479536/TCommit.tla b/TCommit.toolbox/Model_1_SnapShot_1545410479536/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TCommit.toolbox/Model_1_SnapShot_1545410479536/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TCommit.toolbox/Model_1_SnapShot_1545410497334/MC.cfg b/TCommit.toolbox/Model_1_SnapShot_1545410497334/MC.cfg new file mode 100644 index 0000000..f7789bf --- /dev/null +++ b/TCommit.toolbox/Model_1_SnapShot_1545410497334/MC.cfg @@ -0,0 +1,13 @@ +\* CONSTANT definitions +CONSTANT +RM <- const_154541048821114000 +\* INIT definition +INIT +init_154541048821115000 +\* NEXT definition +NEXT +next_154541048821116000 +\* INVARIANT definition +INVARIANT +inv_154541048821117000 +\* Generated on Fri Dec 21 17:41:28 CET 2018 \ No newline at end of file diff --git a/TCommit.toolbox/Model_1_SnapShot_1545410497334/MC.tla b/TCommit.toolbox/Model_1_SnapShot_1545410497334/MC.tla new file mode 100644 index 0000000..d5bcceb --- /dev/null +++ b/TCommit.toolbox/Model_1_SnapShot_1545410497334/MC.tla @@ -0,0 +1,23 @@ +---- MODULE MC ---- +EXTENDS TCommit, TLC + +\* CONSTANT definitions @modelParameterConstants:0RM +const_154541048821114000 == +{"r1","r2","r3"} +---- + +\* INIT definition @modelBehaviorInit:0 +init_154541048821115000 == +TCInit +---- +\* NEXT definition @modelBehaviorNext:0 +next_154541048821116000 == +TCNext +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154541048821117000 == +TCTypeOK +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 17:41:28 CET 2018 by veitheller diff --git a/TCommit.toolbox/Model_1_SnapShot_1545410497334/TCommit.tla b/TCommit.toolbox/Model_1_SnapShot_1545410497334/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TCommit.toolbox/Model_1_SnapShot_1545410497334/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TCommit.toolbox/Model_1_SnapShot_1545410597019/MC.cfg b/TCommit.toolbox/Model_1_SnapShot_1545410597019/MC.cfg new file mode 100644 index 0000000..b6e7eae --- /dev/null +++ b/TCommit.toolbox/Model_1_SnapShot_1545410597019/MC.cfg @@ -0,0 +1,14 @@ +\* CONSTANT definitions +CONSTANT +RM <- const_154541058889823000 +\* INIT definition +INIT +init_154541058889824000 +\* NEXT definition +NEXT +next_154541058889825000 +\* INVARIANT definition +INVARIANT +inv_154541058889826000 +inv_154541058889827000 +\* Generated on Fri Dec 21 17:43:08 CET 2018 \ No newline at end of file diff --git a/TCommit.toolbox/Model_1_SnapShot_1545410597019/MC.tla b/TCommit.toolbox/Model_1_SnapShot_1545410597019/MC.tla new file mode 100644 index 0000000..c09bec9 --- /dev/null +++ b/TCommit.toolbox/Model_1_SnapShot_1545410597019/MC.tla @@ -0,0 +1,27 @@ +---- MODULE MC ---- +EXTENDS TCommit, TLC + +\* CONSTANT definitions @modelParameterConstants:0RM +const_154541058889823000 == +{"r1","r2","r3"} +---- + +\* INIT definition @modelBehaviorInit:0 +init_154541058889824000 == +TCInit +---- +\* NEXT definition @modelBehaviorNext:0 +next_154541058889825000 == +TCNext +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154541058889826000 == +TCTypeOK +---- +\* INVARIANT definition @modelCorrectnessInvariants:1 +inv_154541058889827000 == +TCConsistent +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 17:43:08 CET 2018 by veitheller diff --git a/TCommit.toolbox/Model_1_SnapShot_1545410597019/TCommit.tla b/TCommit.toolbox/Model_1_SnapShot_1545410597019/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TCommit.toolbox/Model_1_SnapShot_1545410597019/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TCommit.toolbox/TCommit.pdf b/TCommit.toolbox/TCommit.pdf new file mode 100644 index 0000000..aad8983 Binary files /dev/null and b/TCommit.toolbox/TCommit.pdf differ diff --git a/TCommit.toolbox/TCommit.tex b/TCommit.toolbox/TCommit.tex new file mode 100644 index 0000000..21d3ae1 --- /dev/null +++ b/TCommit.toolbox/TCommit.tex @@ -0,0 +1,1082 @@ +\batchmode %% Suppresses most terminal output. +\documentclass{article} +\usepackage{color} +\definecolor{boxshade}{gray}{0.85} +\setlength{\textwidth}{360pt} +\setlength{\textheight}{541pt} +\usepackage{latexsym} +\usepackage{ifthen} +% \usepackage{color} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% SWITCHES % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newboolean{shading} +\setboolean{shading}{false} +\makeatletter + %% this is needed only when inserted into the file, not when + %% used as a package file. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % +% DEFINITIONS OF SYMBOL-PRODUCING COMMANDS % +% % +% TLA+ LaTeX % +% symbol command % +% ------ ------- % +% => \implies % +% <: \ltcolon % +% :> \colongt % +% == \defeq % +% .. \dotdot % +% :: \coloncolon % +% =| \eqdash % +% ++ \pp % +% -- \mm % +% ** \stst % +% // \slsl % +% ^ \ct % +% \A \A % +% \E \E % +% \AA \AA % +% \EE \EE % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newlength{\symlength} +\newcommand{\implies}{\Rightarrow} +\newcommand{\ltcolon}{\mathrel{<\!\!\mbox{:}}} +\newcommand{\colongt}{\mathrel{\!\mbox{:}\!\!>}} +\newcommand{\defeq}{\;\mathrel{\smash %% keep this symbol from being too tall + {{\stackrel{\scriptscriptstyle\Delta}{=}}}}\;} +\newcommand{\dotdot}{\mathrel{\ldotp\ldotp}} +\newcommand{\coloncolon}{\mathrel{::\;}} +\newcommand{\eqdash}{\mathrel = \joinrel \hspace{-.28em}|} +\newcommand{\pp}{\mathbin{++}} +\newcommand{\mm}{\mathbin{--}} +\newcommand{\stst}{*\!*} +\newcommand{\slsl}{/\!/} +\newcommand{\ct}{\hat{\hspace{.4em}}} +\newcommand{\A}{\forall} +\newcommand{\E}{\exists} +\renewcommand{\AA}{\makebox{$\raisebox{.05em}{\makebox[0pt][l]{% + $\forall\hspace{-.517em}\forall\hspace{-.517em}\forall$}}% + \forall\hspace{-.517em}\forall \hspace{-.517em}\forall\,$}} +\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox[0pt][l]{% + $\exists\hspace{-.517em}\exists\hspace{-.517em}\exists$}}% + \exists\hspace{-.517em}\exists\hspace{-.517em}\exists\,$}} +\newcommand{\whileop}{\.{\stackrel + {\mbox{\raisebox{-.3em}[0pt][0pt]{$\scriptscriptstyle+\;\,$}}}% + {-\hspace{-.16em}\triangleright}}} + +% Commands are defined to produce the upper-case keywords. +% Note that some have space after them. +\newcommand{\ASSUME}{\textsc{assume }} +\newcommand{\ASSUMPTION}{\textsc{assumption }} +\newcommand{\AXIOM}{\textsc{axiom }} +\newcommand{\BOOLEAN}{\textsc{boolean }} +\newcommand{\CASE}{\textsc{case }} +\newcommand{\CONSTANT}{\textsc{constant }} +\newcommand{\CONSTANTS}{\textsc{constants }} +\newcommand{\ELSE}{\settowidth{\symlength}{\THEN}% + \makebox[\symlength][l]{\textsc{ else}}} +\newcommand{\EXCEPT}{\textsc{ except }} +\newcommand{\EXTENDS}{\textsc{extends }} +\newcommand{\FALSE}{\textsc{false}} +\newcommand{\IF}{\textsc{if }} +\newcommand{\IN}{\settowidth{\symlength}{\LET}% + \makebox[\symlength][l]{\textsc{in}}} +\newcommand{\INSTANCE}{\textsc{instance }} +\newcommand{\LET}{\textsc{let }} +\newcommand{\LOCAL}{\textsc{local }} +\newcommand{\MODULE}{\textsc{module }} +\newcommand{\OTHER}{\textsc{other }} +\newcommand{\STRING}{\textsc{string}} +\newcommand{\THEN}{\textsc{ then }} +\newcommand{\THEOREM}{\textsc{theorem }} +\newcommand{\LEMMA}{\textsc{lemma }} +\newcommand{\PROPOSITION}{\textsc{proposition }} +\newcommand{\COROLLARY}{\textsc{corollary }} +\newcommand{\TRUE}{\textsc{true}} +\newcommand{\VARIABLE}{\textsc{variable }} +\newcommand{\VARIABLES}{\textsc{variables }} +\newcommand{\WITH}{\textsc{ with }} +\newcommand{\WF}{\textrm{WF}} +\newcommand{\SF}{\textrm{SF}} +\newcommand{\CHOOSE}{\textsc{choose }} +\newcommand{\ENABLED}{\textsc{enabled }} +\newcommand{\UNCHANGED}{\textsc{unchanged }} +\newcommand{\SUBSET}{\textsc{subset }} +\newcommand{\UNION}{\textsc{union }} +\newcommand{\DOMAIN}{\textsc{domain }} +% Added for tla2tex +\newcommand{\BY}{\textsc{by }} +\newcommand{\OBVIOUS}{\textsc{obvious }} +\newcommand{\HAVE}{\textsc{have }} +\newcommand{\QED}{\textsc{qed }} +\newcommand{\TAKE}{\textsc{take }} +\newcommand{\DEF}{\textsc{ def }} +\newcommand{\HIDE}{\textsc{hide }} +\newcommand{\RECURSIVE}{\textsc{recursive }} +\newcommand{\USE}{\textsc{use }} +\newcommand{\DEFINE}{\textsc{define }} +\newcommand{\PROOF}{\textsc{proof }} +\newcommand{\WITNESS}{\textsc{witness }} +\newcommand{\PICK}{\textsc{pick }} +\newcommand{\DEFS}{\textsc{defs }} +\newcommand{\PROVE}{\settowidth{\symlength}{\ASSUME}% + \makebox[\symlength][l]{\textsc{prove}}\@s{-4.1}}% + %% The \@s{-4.1) is a kludge added on 24 Oct 2009 [happy birthday, Ellen] + %% so the correct alignment occurs if the user types + %% ASSUME X + %% PROVE Y + %% because it cancels the extra 4.1 pts added because of the + %% extra space after the PROVE. This seems to works OK. + %% However, the 4.1 equals Parameters.LaTeXLeftSpace(1) and + %% should be changed if that method ever changes. +\newcommand{\SUFFICES}{\textsc{suffices }} +\newcommand{\NEW}{\textsc{new }} +\newcommand{\LAMBDA}{\textsc{lambda }} +\newcommand{\STATE}{\textsc{state }} +\newcommand{\ACTION}{\textsc{action }} +\newcommand{\TEMPORAL}{\textsc{temporal }} +\newcommand{\ONLY}{\textsc{only }} %% added by LL on 2 Oct 2009 +\newcommand{\OMITTED}{\textsc{omitted }} %% added by LL on 31 Oct 2009 +\newcommand{\@pfstepnum}[2]{\ensuremath{\langle#1\rangle}\textrm{#2}} +\newcommand{\bang}{\@s{1}\mbox{\small !}\@s{1}} +%% We should format || differently in PlusCal code than in TLA+ formulas. +\newcommand{\p@barbar}{\ifpcalsymbols + \,\,\rule[-.25em]{.075em}{1em}\hspace*{.2em}\rule[-.25em]{.075em}{1em}\,\,% + \else \,||\,\fi} +%% PlusCal keywords +\newcommand{\p@fair}{\textbf{fair }} +\newcommand{\p@semicolon}{\textbf{\,; }} +\newcommand{\p@algorithm}{\textbf{algorithm }} +\newcommand{\p@mmfair}{\textbf{-{}-fair }} +\newcommand{\p@mmalgorithm}{\textbf{-{}-algorithm }} +\newcommand{\p@assert}{\textbf{assert }} +\newcommand{\p@await}{\textbf{await }} +\newcommand{\p@begin}{\textbf{begin }} +\newcommand{\p@end}{\textbf{end }} +\newcommand{\p@call}{\textbf{call }} +\newcommand{\p@define}{\textbf{define }} +\newcommand{\p@do}{\textbf{ do }} +\newcommand{\p@either}{\textbf{either }} +\newcommand{\p@or}{\textbf{or }} +\newcommand{\p@goto}{\textbf{goto }} +\newcommand{\p@if}{\textbf{if }} +\newcommand{\p@then}{\,\,\textbf{then }} +\newcommand{\p@else}{\ifcsyntax \textbf{else } \else \,\,\textbf{else }\fi} +\newcommand{\p@elsif}{\,\,\textbf{elsif }} +\newcommand{\p@macro}{\textbf{macro }} +\newcommand{\p@print}{\textbf{print }} +\newcommand{\p@procedure}{\textbf{procedure }} +\newcommand{\p@process}{\textbf{process }} +\newcommand{\p@return}{\textbf{return}} +\newcommand{\p@skip}{\textbf{skip}} +\newcommand{\p@variable}{\textbf{variable }} +\newcommand{\p@variables}{\textbf{variables }} +\newcommand{\p@while}{\textbf{while }} +\newcommand{\p@when}{\textbf{when }} +\newcommand{\p@with}{\textbf{with }} +\newcommand{\p@lparen}{\textbf{(\,\,}} +\newcommand{\p@rparen}{\textbf{\,\,) }} +\newcommand{\p@lbrace}{\textbf{\{\,\,}} +\newcommand{\p@rbrace}{\textbf{\,\,\} }} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% REDEFINE STANDARD COMMANDS TO MAKE THEM FORMAT BETTER % +% % +% We redefine \in and \notin % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\renewcommand{\_}{\rule{.4em}{.06em}\hspace{.05em}} +\newlength{\equalswidth} +\let\oldin=\in +\let\oldnotin=\notin +\renewcommand{\in}{% + {\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth][c]{$\oldin$}}} +\renewcommand{\notin}{% + {\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth]{$\oldnotin$}}} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % +% HORIZONTAL BARS: % +% % +% \moduleLeftDash |~~~~~~~~~~ % +% \moduleRightDash ~~~~~~~~~~| % +% \midbar |----------| % +% \bottombar |__________| % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newlength{\charwidth}\settowidth{\charwidth}{{\small\tt M}} +\newlength{\boxrulewd}\setlength{\boxrulewd}{.4pt} +\newlength{\boxlineht}\setlength{\boxlineht}{.5\baselineskip} +\newcommand{\boxsep}{\charwidth} +\newlength{\boxruleht}\setlength{\boxruleht}{.5ex} +\newlength{\boxruledp}\setlength{\boxruledp}{-\boxruleht} +\addtolength{\boxruledp}{\boxrulewd} +\newcommand{\boxrule}{\leaders\hrule height \boxruleht depth \boxruledp + \hfill\mbox{}} +\newcommand{\@computerule}{% + \setlength{\boxruleht}{.5ex}% + \setlength{\boxruledp}{-\boxruleht}% + \addtolength{\boxruledp}{\boxrulewd}} + +\newcommand{\bottombar}{\hspace{-\boxsep}% + \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd}{\boxlineht}}% + \boxrule + \raisebox{-\boxrulewd}[0pt][0pt]{% + \rule[.5ex]{\boxrulewd}{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}} + +\newcommand{\moduleLeftDash}% + {\hspace*{-\boxsep}% + \raisebox{-\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd + }{\boxlineht}}% + \boxrule\hspace*{.4em }} + +\newcommand{\moduleRightDash}% + {\hspace*{.4em}\boxrule + \raisebox{-\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd + }{\boxlineht}}\hspace{-\boxsep}}%\vspace{.2em} + +\newcommand{\midbar}{\hspace{-\boxsep}\raisebox{-.5\boxlineht}[0pt][0pt]{% + \rule[.5ex]{\boxrulewd}{\boxlineht}}\boxrule\raisebox{-.5\boxlineht% + }[0pt][0pt]{\rule[.5ex]{\boxrulewd}{\boxlineht}}\hspace{-\boxsep}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% FORMATING COMMANDS % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% PLUSCAL SHADING % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% The TeX pcalshading switch is set on to cause PlusCal shading to be +% performed. This changes the behavior of the following commands and +% environments to cause full-width shading to be performed on all lines. +% +% \tstrut \@x cpar mcom \@pvspace +% +% The TeX pcalsymbols switch is turned on when typesetting a PlusCal algorithm, +% whether or not shading is being performed. It causes symbols (other than +% parentheses and braces and PlusCal-only keywords) that should be typeset +% differently depending on whether they are in an algorithm to be typeset +% appropriately. Currently, the only such symbol is "||". +% +% The TeX csyntax switch is turned on when typesetting a PlusCal algorithm in +% c-syntax. This allows symbols to be format differently in the two syntaxes. +% The "else" keyword is the only one that is. + +\newif\ifpcalshading \pcalshadingfalse +\newif\ifpcalsymbols \pcalsymbolsfalse +\newif\ifcsyntax \csyntaxtrue + +% The \@pvspace command makes a vertical space. It uses \vspace +% except with \ifpcalshading, in which case it sets \pvcalvspace +% and the space is added by a following \@x command. +% +\newlength{\pcalvspace}\setlength{\pcalvspace}{0pt}% +\newcommand{\@pvspace}[1]{% + \ifpcalshading + \par\global\setlength{\pcalvspace}{#1}% + \else + \par\vspace{#1}% + \fi +} + +% The lcom environment was changed to set \lcomindent equal to +% the indentation it produces. This length is used by the +% cpar environment to make shading extend for the full width +% of the line. This assumes that lcom environments are not +% nested. I hope TLATeX does not nest them. +% +\newlength{\lcomindent}% +\setlength{\lcomindent}{0pt}% + +%\tstrut: A strut to produce inter-paragraph space in a comment. +%\rstrut: A strut to extend the bottom of a one-line comment so +% there's no break in the shading between comments on +% successive lines. +\newcommand\tstrut% + {\raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{1.15em}}}% + \global\setlength{\vshadelen}{0pt}} +\newcommand\rstrut{\raisebox{-.25em}{\rule{0pt}{1.15em}}% + \global\setlength{\vshadelen}{0pt}} + + +% \.{op} formats operator op in math mode with empty boxes on either side. +% Used because TeX otherwise vary the amount of space it leaves around op. +\renewcommand{\.}[1]{\ensuremath{\mbox{}#1\mbox{}}} + +% \@s{n} produces an n-point space +\newcommand{\@s}[1]{\hspace{#1pt}} + +% \@x{txt} starts a specification line in the beginning with txt +% in the final LaTeX source. +\newlength{\@xlen} +\newcommand\xtstrut% + {\setlength{\@xlen}{1.05em}% + \addtolength{\@xlen}{\pcalvspace}% + \raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{\@xlen}}}% + \global\setlength{\vshadelen}{0pt}% + \global\setlength{\pcalvspace}{0pt}} + +\newcommand{\@x}[1]{\par + \ifpcalshading + \makebox[0pt][l]{\shadebox{\xtstrut\hspace*{\textwidth}}}% + \fi + \mbox{$\mbox{}#1\mbox{}$}} + +% \@xx{txt} continues a specification line with the text txt. +\newcommand{\@xx}[1]{\mbox{$\mbox{}#1\mbox{}$}} + +% \@y{cmt} produces a one-line comment. +\newcommand{\@y}[1]{\mbox{\footnotesize\hspace{.65em}% + \ifthenelse{\boolean{shading}}{% + \shadebox{#1\hspace{-\the\lastskip}\rstrut}}% + {#1\hspace{-\the\lastskip}\rstrut}}} + +% \@z{cmt} produces a zero-width one-line comment. +\newcommand{\@z}[1]{\makebox[0pt][l]{\footnotesize + \ifthenelse{\boolean{shading}}{% + \shadebox{#1\hspace{-\the\lastskip}\rstrut}}% + {#1\hspace{-\the\lastskip}\rstrut}}} + + +% \@w{str} produces the TLA+ string "str". +\newcommand{\@w}[1]{\textsf{``{#1}''}} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% SHADING % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\def\graymargin{1} + % The number of points of margin in the shaded box. + +% \definecolor{boxshade}{gray}{.85} +% Defines the darkness of the shading: 1 = white, 0 = black +% Added by TLATeX only if needed. + +% \shadebox{txt} puts txt in a shaded box. +\newlength{\templena} +\newlength{\templenb} +\newsavebox{\tempboxa} +\newcommand{\shadebox}[1]{{\setlength{\fboxsep}{\graymargin pt}% + \savebox{\tempboxa}{#1}% + \settoheight{\templena}{\usebox{\tempboxa}}% + \settodepth{\templenb}{\usebox{\tempboxa}}% + \hspace*{-\fboxsep}\raisebox{0pt}[\templena][\templenb]% + {\colorbox{boxshade}{\usebox{\tempboxa}}}\hspace*{-\fboxsep}}} + +% \vshade{n} makes an n-point inter-paragraph space, with +% shading if the `shading' flag is true. +\newlength{\vshadelen} +\setlength{\vshadelen}{0pt} +\newcommand{\vshade}[1]{\ifthenelse{\boolean{shading}}% + {\global\setlength{\vshadelen}{#1pt}}% + {\vspace{#1pt}}} + +\newlength{\boxwidth} +\newlength{\multicommentdepth} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE cpar ENVIRONMENT % +% ^^^^^^^^^^^^^^^^^^^^ % +% The LaTeX input % +% % +% \begin{cpar}{pop}{nest}{isLabel}{d}{e}{arg6} % +% XXXXXXXXXXXXXXX % +% XXXXXXXXXXXXXXX % +% XXXXXXXXXXXXXXX % +% \end{cpar} % +% % +% produces one of two possible results. If isLabel is the letter "T", % +% it produces the following, where [label] is the result of typesetting % +% arg6 in an LR box, and d is is a number representing a distance in % +% points. % +% % +% prevailing |<-- d -->[label]<- e ->XXXXXXXXXXXXXXX % +% left | XXXXXXXXXXXXXXX % +% margin | XXXXXXXXXXXXXXX % +% % +% If isLabel is the letter "F", then it produces % +% % +% prevailing |<-- d -->XXXXXXXXXXXXXXXXXXXXXXX % +% left | <- e ->XXXXXXXXXXXXXXXX % +% margin | XXXXXXXXXXXXXXXX % +% % +% where d and e are numbers representing distances in points. % +% % +% The prevailing left margin is the one in effect before the most recent % +% pop (argument 1) cpar environments with "T" as the nest argument, where % +% pop is a number \geq 0. % +% % +% If the nest argument is the letter "T", then the prevailing left % +% margin is moved to the left of the second (and following) lines of % +% X's. Otherwise, the prevailing left margin is left unchanged. % +% % +% An \unnest{n} command moves the prevailing left margin to where it was % +% before the most recent n cpar environments with "T" as the nesting % +% argument. % +% % +% The environment leaves no vertical space above or below it, or between % +% its paragraphs. (TLATeX inserts the proper amount of vertical space.) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcounter{pardepth} +\setcounter{pardepth}{0} + +% \setgmargin{txt} defines \gmarginN to be txt, where N is \roman{pardepth}. +% \thegmargin equals \gmarginN, where N is \roman{pardepth}. +\newcommand{\setgmargin}[1]{% + \expandafter\xdef\csname gmargin\roman{pardepth}\endcsname{#1}} +\newcommand{\thegmargin}{\csname gmargin\roman{pardepth}\endcsname} +\newcommand{\gmargin}{0pt} + +\newsavebox{\tempsbox} + +\newlength{\@cparht} +\newlength{\@cpardp} +\newenvironment{cpar}[6]{% + \addtocounter{pardepth}{-#1}% + \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}% + \begin{minipage}[t]{\linewidth}}{}% + \begin{list}{}{% + \edef\temp{\thegmargin} + \ifthenelse{\equal{#3}{T}}% + {\settowidth{\leftmargin}{\hspace{\temp}\footnotesize #6\hspace{#5pt}}% + \addtolength{\leftmargin}{#4pt}}% + {\setlength{\leftmargin}{#4pt}% + \addtolength{\leftmargin}{#5pt}% + \addtolength{\leftmargin}{\temp}% + \setlength{\itemindent}{-#5pt}}% + \ifthenelse{\equal{#2}{T}}{\addtocounter{pardepth}{1}% + \setgmargin{\the\leftmargin}}{}% + \setlength{\labelwidth}{0pt}% + \setlength{\labelsep}{0pt}% + \setlength{\itemindent}{-\leftmargin}% + \setlength{\topsep}{0pt}% + \setlength{\parsep}{0pt}% + \setlength{\partopsep}{0pt}% + \setlength{\parskip}{0pt}% + \setlength{\itemsep}{0pt} + \setlength{\itemindent}{#4pt}% + \addtolength{\itemindent}{-\leftmargin}}% + \ifthenelse{\equal{#3}{T}}% + {\item[\tstrut\footnotesize \hspace{\temp}{#6}\hspace{#5pt}] + }% + {\item[\tstrut\hspace{\temp}]% + }% + \footnotesize} + {\hspace{-\the\lastskip}\tstrut + \end{list}% + \ifthenelse{\boolean{shading}}% + {\end{minipage}% + \end{lrbox}% + \ifpcalshading + \setlength{\@cparht}{\ht\tempsbox}% + \setlength{\@cpardp}{\dp\tempsbox}% + \addtolength{\@cparht}{.15em}% + \addtolength{\@cpardp}{.2em}% + \addtolength{\@cparht}{\@cpardp}% + % I don't know what's going on here. I want to add a + % \pcalvspace high shaded line, but I don't know how to + % do it. A little trial and error shows that the following + % does a reasonable job approximating that, eliminating + % the line if \pcalvspace is small. + \addtolength{\@cparht}{\pcalvspace}% + \ifdim \pcalvspace > .8em + \addtolength{\pcalvspace}{-.2em}% + \hspace*{-\lcomindent}% + \shadebox{\rule{0pt}{\pcalvspace}\hspace*{\textwidth}}\par + \global\setlength{\pcalvspace}{0pt}% + \fi + \hspace*{-\lcomindent}% + \makebox[0pt][l]{\raisebox{-\@cpardp}[0pt][0pt]{% + \shadebox{\rule{0pt}{\@cparht}\hspace*{\textwidth}}}}% + \hspace*{\lcomindent}\usebox{\tempsbox}% + \par + \else + \shadebox{\usebox{\tempsbox}}\par + \fi}% + {}% + } + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE ppar ENVIRONMENT % +% ^^^^^^^^^^^^^^^^^^^^ % +% The environment % +% % +% \begin{ppar} ... \end{ppar} % +% % +% is equivalent to % +% % +% \begin{cpar}{0}{F}{F}{0}{0}{} ... \end{cpar} % +% % +% The environment is put around each line of the output for a PlusCal % +% algorithm. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%\newenvironment{ppar}{% +% \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}% +% \begin{minipage}[t]{\linewidth}}{}% +% \begin{list}{}{% +% \edef\temp{\thegmargin} +% \setlength{\leftmargin}{0pt}% +% \addtolength{\leftmargin}{\temp}% +% \setlength{\itemindent}{0pt}% +% \setlength{\labelwidth}{0pt}% +% \setlength{\labelsep}{0pt}% +% \setlength{\itemindent}{-\leftmargin}% +% \setlength{\topsep}{0pt}% +% \setlength{\parsep}{0pt}% +% \setlength{\partopsep}{0pt}% +% \setlength{\parskip}{0pt}% +% \setlength{\itemsep}{0pt} +% \setlength{\itemindent}{0pt}% +% \addtolength{\itemindent}{-\leftmargin}}% +% \item[\tstrut\hspace{\temp}]}% +% {\hspace{-\the\lastskip}\tstrut +% \end{list}% +% \ifthenelse{\boolean{shading}}{\end{minipage} +% \end{lrbox}% +% \shadebox{\usebox{\tempsbox}}\par}{}% +% } + + %%% TESTING + \newcommand{\xtest}[1]{\par + \makebox[0pt][l]{\shadebox{\xtstrut\hspace*{\textwidth}}}% + \mbox{$\mbox{}#1\mbox{}$}} + +% \newcommand{\xxtest}[1]{\par +% \makebox[0pt][l]{\shadebox{\xtstrut{#1}\hspace*{\textwidth}}}% +% \mbox{$\mbox{}#1\mbox{}$}} + +%\newlength{\pcalvspace} +%\setlength{\pcalvspace}{0pt} +% \newlength{\xxtestlen} +% \setlength{\xxtestlen}{0pt} +% \newcommand\xtstrut% +% {\setlength{\xxtestlen}{1.15em}% +% \addtolength{\xxtestlen}{\pcalvspace}% +% \raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{\xxtestlen}}}% +% \global\setlength{\vshadelen}{0pt}% +% \global\setlength{\pcalvspace}{0pt}} + + %%%% TESTING + + %% The xcpar environment + %% Note: overloaded use of \pcalvspace for testing. + %% +% \newlength{\xcparht}% +% \newlength{\xcpardp}% + +% \newenvironment{xcpar}[6]{% +% \addtocounter{pardepth}{-#1}% +% \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}% +% \begin{minipage}[t]{\linewidth}}{}% +% \begin{list}{}{% +% \edef\temp{\thegmargin}% +% \ifthenelse{\equal{#3}{T}}% +% {\settowidth{\leftmargin}{\hspace{\temp}\footnotesize #6\hspace{#5pt}}% +% \addtolength{\leftmargin}{#4pt}}% +% {\setlength{\leftmargin}{#4pt}% +% \addtolength{\leftmargin}{#5pt}% +% \addtolength{\leftmargin}{\temp}% +% \setlength{\itemindent}{-#5pt}}% +% \ifthenelse{\equal{#2}{T}}{\addtocounter{pardepth}{1}% +% \setgmargin{\the\leftmargin}}{}% +% \setlength{\labelwidth}{0pt}% +% \setlength{\labelsep}{0pt}% +% \setlength{\itemindent}{-\leftmargin}% +% \setlength{\topsep}{0pt}% +% \setlength{\parsep}{0pt}% +% \setlength{\partopsep}{0pt}% +% \setlength{\parskip}{0pt}% +% \setlength{\itemsep}{0pt}% +% \setlength{\itemindent}{#4pt}% +% \addtolength{\itemindent}{-\leftmargin}}% +% \ifthenelse{\equal{#3}{T}}% +% {\item[\xtstrut\footnotesize \hspace{\temp}{#6}\hspace{#5pt}]% +% }% +% {\item[\xtstrut\hspace{\temp}]% +% }% +% \footnotesize} +% {\hspace{-\the\lastskip}\tstrut +% \end{list}% +% \ifthenelse{\boolean{shading}}{\end{minipage} +% \end{lrbox}% +% \setlength{\xcparht}{\ht\tempsbox}% +% \setlength{\xcpardp}{\dp\tempsbox}% +% \addtolength{\xcparht}{.15em}% +% \addtolength{\xcpardp}{.2em}% +% \addtolength{\xcparht}{\xcpardp}% +% \hspace*{-\lcomindent}% +% \makebox[0pt][l]{\raisebox{-\xcpardp}[0pt][0pt]{% +% \shadebox{\rule{0pt}{\xcparht}\hspace*{\textwidth}}}}% +% \hspace*{\lcomindent}\usebox{\tempsbox}% +% \par}{}% +% } +% +% \newlength{\xmcomlen} +%\newenvironment{xmcom}[1]{% +% \setcounter{pardepth}{0}% +% \hspace{.65em}% +% \begin{lrbox}{\alignbox}\sloppypar% +% \setboolean{shading}{false}% +% \setlength{\boxwidth}{#1pt}% +% \addtolength{\boxwidth}{-.65em}% +% \begin{minipage}[t]{\boxwidth}\footnotesize +% \parskip=0pt\relax}% +% {\end{minipage}\end{lrbox}% +% \setlength{\xmcomlen}{\textwidth}% +% \addtolength{\xmcomlen}{-\wd\alignbox}% +% \settodepth{\alignwidth}{\usebox{\alignbox}}% +% \global\setlength{\multicommentdepth}{\alignwidth}% +% \setlength{\boxwidth}{\alignwidth}% +% \global\addtolength{\alignwidth}{-\maxdepth}% +% \addtolength{\boxwidth}{.1em}% +% \raisebox{0pt}[0pt][0pt]{% +% \ifthenelse{\boolean{shading}}% +% {\hspace*{-\xmcomlen}\shadebox{\rule[-\boxwidth]{0pt}{0pt}% +% \hspace*{\xmcomlen}\usebox{\alignbox}}}% +% {\usebox{\alignbox}}}% +% \vspace*{\alignwidth}\pagebreak[0]\vspace{-\alignwidth}\par} +% % a multi-line comment, whose first argument is its width in points. +% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE lcom ENVIRONMENT % +% ^^^^^^^^^^^^^^^^^^^^ % +% A multi-line comment with no text to its left is typeset in an lcom % +% environment, whose argument is a number representing the indentation % +% of the left margin, in points. All the text of the comment should be % +% inside cpar environments. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newenvironment{lcom}[1]{% + \setlength{\lcomindent}{#1pt} % Added for PlusCal handling. + \par\vspace{.2em}% + \sloppypar + \setcounter{pardepth}{0}% + \footnotesize + \begin{list}{}{% + \setlength{\leftmargin}{#1pt} + \setlength{\labelwidth}{0pt}% + \setlength{\labelsep}{0pt}% + \setlength{\itemindent}{0pt}% + \setlength{\topsep}{0pt}% + \setlength{\parsep}{0pt}% + \setlength{\partopsep}{0pt}% + \setlength{\parskip}{0pt}} + \item[]}% + {\end{list}\vspace{.3em}\setlength{\lcomindent}{0pt}% + } + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE mcom ENVIRONMENT AND \mutivspace COMMAND % +% ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ % +% % +% A part of the spec containing a right-comment of the form % +% % +% xxxx (*************) % +% yyyy (* ccccccccc *) % +% ... (* ccccccccc *) % +% (* ccccccccc *) % +% (* ccccccccc *) % +% (*************) % +% % +% is typeset by % +% % +% XXXX \begin{mcom}{d} % +% CCCC ... CCC % +% \end{mcom} % +% YYYY ... % +% \multivspace{n} % +% % +% where the number d is the width in points of the comment, n is the % +% number of xxxx, yyyy, ... lines to the left of the comment. % +% All the text of the comment should be typeset in cpar environments. % +% % +% This puts the comment into a single box (so no page breaks can occur % +% within it). The entire box is shaded iff the shading flag is true. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newlength{\xmcomlen}% +\newenvironment{mcom}[1]{% + \setcounter{pardepth}{0}% + \hspace{.65em}% + \begin{lrbox}{\alignbox}\sloppypar% + \setboolean{shading}{false}% + \setlength{\boxwidth}{#1pt}% + \addtolength{\boxwidth}{-.65em}% + \begin{minipage}[t]{\boxwidth}\footnotesize + \parskip=0pt\relax}% + {\end{minipage}\end{lrbox}% + \setlength{\xmcomlen}{\textwidth}% % For PlusCal shading + \addtolength{\xmcomlen}{-\wd\alignbox}% % For PlusCal shading + \settodepth{\alignwidth}{\usebox{\alignbox}}% + \global\setlength{\multicommentdepth}{\alignwidth}% + \setlength{\boxwidth}{\alignwidth}% % For PlusCal shading + \global\addtolength{\alignwidth}{-\maxdepth}% + \addtolength{\boxwidth}{.1em}% % For PlusCal shading + \raisebox{0pt}[0pt][0pt]{% + \ifthenelse{\boolean{shading}}% + {\ifpcalshading + \hspace*{-\xmcomlen}% + \shadebox{\rule[-\boxwidth]{0pt}{0pt}\hspace*{\xmcomlen}% + \usebox{\alignbox}}% + \else + \shadebox{\usebox{\alignbox}} + \fi + }% + {\usebox{\alignbox}}}% + \vspace*{\alignwidth}\pagebreak[0]\vspace{-\alignwidth}\par} + % a multi-line comment, whose first argument is its width in points. + + +% \multispace{n} produces the vertical space indicated by "|"s in +% this situation +% +% xxxx (*************) +% xxxx (* ccccccccc *) +% | (* ccccccccc *) +% | (* ccccccccc *) +% | (* ccccccccc *) +% | (*************) +% +% where n is the number of "xxxx" lines. +\newcommand{\multivspace}[1]{\addtolength{\multicommentdepth}{-#1\baselineskip}% + \addtolength{\multicommentdepth}{1.2em}% + \ifthenelse{\lengthtest{\multicommentdepth > 0pt}}% + {\par\vspace{\multicommentdepth}\par}{}} + +%\newenvironment{hpar}[2]{% +% \begin{list}{}{\setlength{\leftmargin}{#1pt}% +% \addtolength{\leftmargin}{#2pt}% +% \setlength{\itemindent}{-#2pt}% +% \setlength{\topsep}{0pt}% +% \setlength{\parsep}{0pt}% +% \setlength{\partopsep}{0pt}% +% \setlength{\parskip}{0pt}% +% \addtolength{\labelsep}{0pt}}% +% \item[]\footnotesize}{\end{list}} +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % Typesets a sequence of paragraphs like this: % +% % % +% % left |<-- d1 --> XXXXXXXXXXXXXXXXXXXXXXXX % +% % margin | <- d2 -> XXXXXXXXXXXXXXX % +% % | XXXXXXXXXXXXXXX % +% % | % +% % | XXXXXXXXXXXXXXX % +% % | XXXXXXXXXXXXXXX % +% % % +% % where d1 = #1pt and d2 = #2pt, but with no vspace between % +% % paragraphs. % +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Commands for repeated characters that produce dashes. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% \raisedDash{wd}{ht}{thk} makes a horizontal line wd characters wide, +% raised a distance ht ex's above the baseline, with a thickness of +% thk em's. +\newcommand{\raisedDash}[3]{\raisebox{#2ex}{\setlength{\alignwidth}{.5em}% + \rule{#1\alignwidth}{#3em}}} + +% The following commands take a single argument n and produce the +% output for n repeated characters, as follows +% \cdash: - +% \tdash: ~ +% \ceqdash: = +% \usdash: _ +\newcommand{\cdash}[1]{\raisedDash{#1}{.5}{.04}} +\newcommand{\usdash}[1]{\raisedDash{#1}{0}{.04}} +\newcommand{\ceqdash}[1]{\raisedDash{#1}{.5}{.08}} +\newcommand{\tdash}[1]{\raisedDash{#1}{1}{.08}} + +\newlength{\spacewidth} +\setlength{\spacewidth}{.2em} +\newcommand{\e}[1]{\hspace{#1\spacewidth}} +%% \e{i} produces space corresponding to i input spaces. + + +%% Alignment-file Commands + +\newlength{\alignboxwidth} +\newlength{\alignwidth} +\newsavebox{\alignbox} + +% \al{i}{j}{txt} is used in the alignment file to put "%{i}{j}{wd}" +% in the log file, where wd is the width of the line up to that point, +% and txt is the following text. +\newcommand{\al}[3]{% + \typeout{\%{#1}{#2}{\the\alignwidth}}% + \cl{#3}} + +%% \cl{txt} continues a specification line in the alignment file +%% with text txt. +\newcommand{\cl}[1]{% + \savebox{\alignbox}{\mbox{$\mbox{}#1\mbox{}$}}% + \settowidth{\alignboxwidth}{\usebox{\alignbox}}% + \addtolength{\alignwidth}{\alignboxwidth}% + \usebox{\alignbox}} + +% \fl{txt} in the alignment file begins a specification line that +% starts with the text txt. +\newcommand{\fl}[1]{% + \par + \savebox{\alignbox}{\mbox{$\mbox{}#1\mbox{}$}}% + \settowidth{\alignwidth}{\usebox{\alignbox}}% + \usebox{\alignbox}} + + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Ordinarily, TeX typesets letters in math mode in a special math italic % +% font. This makes it typeset "it" to look like the product of the % +% variables i and t, rather than like the word "it". The following % +% commands tell TeX to use an ordinary italic font instead. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\ifx\documentclass\undefined +\else + \DeclareSymbolFont{tlaitalics}{\encodingdefault}{cmr}{m}{it} + \let\itfam\symtlaitalics +\fi + +\makeatletter +\newcommand{\tlx@c}{\c@tlx@ctr\advance\c@tlx@ctr\@ne} +\newcounter{tlx@ctr} +\c@tlx@ctr=\itfam \multiply\c@tlx@ctr"100\relax \advance\c@tlx@ctr "7061\relax +\mathcode`a=\tlx@c \mathcode`b=\tlx@c \mathcode`c=\tlx@c \mathcode`d=\tlx@c +\mathcode`e=\tlx@c \mathcode`f=\tlx@c \mathcode`g=\tlx@c \mathcode`h=\tlx@c +\mathcode`i=\tlx@c \mathcode`j=\tlx@c \mathcode`k=\tlx@c \mathcode`l=\tlx@c +\mathcode`m=\tlx@c \mathcode`n=\tlx@c \mathcode`o=\tlx@c \mathcode`p=\tlx@c +\mathcode`q=\tlx@c \mathcode`r=\tlx@c \mathcode`s=\tlx@c \mathcode`t=\tlx@c +\mathcode`u=\tlx@c \mathcode`v=\tlx@c \mathcode`w=\tlx@c \mathcode`x=\tlx@c +\mathcode`y=\tlx@c \mathcode`z=\tlx@c +\c@tlx@ctr=\itfam \multiply\c@tlx@ctr"100\relax \advance\c@tlx@ctr "7041\relax +\mathcode`A=\tlx@c \mathcode`B=\tlx@c \mathcode`C=\tlx@c \mathcode`D=\tlx@c +\mathcode`E=\tlx@c \mathcode`F=\tlx@c \mathcode`G=\tlx@c \mathcode`H=\tlx@c +\mathcode`I=\tlx@c \mathcode`J=\tlx@c \mathcode`K=\tlx@c \mathcode`L=\tlx@c +\mathcode`M=\tlx@c \mathcode`N=\tlx@c \mathcode`O=\tlx@c \mathcode`P=\tlx@c +\mathcode`Q=\tlx@c \mathcode`R=\tlx@c \mathcode`S=\tlx@c \mathcode`T=\tlx@c +\mathcode`U=\tlx@c \mathcode`V=\tlx@c \mathcode`W=\tlx@c \mathcode`X=\tlx@c +\mathcode`Y=\tlx@c \mathcode`Z=\tlx@c +\makeatother + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE describe ENVIRONMENT % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% +% It is like the description environment except it takes an argument +% ARG that should be the text of the widest label. It adjusts the +% indentation so each item with label LABEL produces +%% LABEL blah blah blah +%% <- width of ARG ->blah blah blah +%% blah blah blah +\newenvironment{describe}[1]% + {\begin{list}{}{\settowidth{\labelwidth}{#1}% + \setlength{\labelsep}{.5em}% + \setlength{\leftmargin}{\labelwidth}% + \addtolength{\leftmargin}{\labelsep}% + \addtolength{\leftmargin}{\parindent}% + \def\makelabel##1{\rm ##1\hfill}}% + \setlength{\topsep}{0pt}}%% + % Sets \topsep to 0 to reduce vertical space above + % and below embedded displayed equations + {\end{list}} + +% For tlatex.TeX +\usepackage{verbatim} +\makeatletter +\def\tla{\let\%\relax% + \@bsphack + \typeout{\%{\the\linewidth}}% + \let\do\@makeother\dospecials\catcode`\^^M\active + \let\verbatim@startline\relax + \let\verbatim@addtoline\@gobble + \let\verbatim@processline\relax + \let\verbatim@finish\relax + \verbatim@} +\let\endtla=\@esphack + +\let\pcal=\tla +\let\endpcal=\endtla +\let\ppcal=\tla +\let\endppcal=\endtla + +% The tlatex environment is used by TLATeX.TeX to typeset TLA+. +% TLATeX.TLA starts its files by writing a \tlatex command. This +% command/environment sets \parindent to 0 and defines \% to its +% standard definition because the writing of the log files is messed up +% if \% is defined to be something else. It also executes +% \@computerule to determine the dimensions for the TLA horizonatl +% bars. +\newenvironment{tlatex}{\@computerule% + \setlength{\parindent}{0pt}% + \makeatletter\chardef\%=`\%}{} + + +% The notla environment produces no output. You can turn a +% tla environment to a notla environment to prevent tlatex.TeX from +% re-formatting the environment. + +\def\notla{\let\%\relax% + \@bsphack + \let\do\@makeother\dospecials\catcode`\^^M\active + \let\verbatim@startline\relax + \let\verbatim@addtoline\@gobble + \let\verbatim@processline\relax + \let\verbatim@finish\relax + \verbatim@} +\let\endnotla=\@esphack + +\let\nopcal=\notla +\let\endnopcal=\endnotla +\let\noppcal=\notla +\let\endnoppcal=\endnotla + +%%%%%%%%%%%%%%%%%%%%%%%% end of tlatex.sty file %%%%%%%%%%%%%%%%%%%%%%% +% last modified on Fri 3 August 2012 at 14:23:49 PST by lamport + +\begin{document} +\tlatex +\setboolean{shading}{true} +\@x{}\moduleLeftDash\@xx{ {\MODULE} TCommit}\moduleRightDash\@xx{}% +\@pvspace{8.0pt}% +\begin{lcom}{0}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +This specification is explained in ``Transaction Commit'', Lecture 5 of + the TLA+ Video Course. +\end{cpar}% +\end{lcom}% +\@x{ {\CONSTANT} RM\@s{24.59}}% +\@y{\@s{0}% + The set of participating resource managers +}% +\@xx{}% +\@pvspace{8.0pt}% +\@x{ {\VARIABLE} rmState\@s{10.70}}% +\@y{\@s{0}% + \ensuremath{rmState[rm]} is the state of resource manager \ensuremath{r}. +}% +\@xx{}% +\@x{}\midbar\@xx{}% +\@x{ TCTypeOK \.{\defeq}}% +\begin{lcom}{8.2}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +The type-correctness invariant +\end{cpar}% +\end{lcom}% + \@x{\@s{8.2} rmState \.{\in} [ RM \.{\rightarrow} \{\@w{working} + ,\,\@w{prepared} ,\,\@w{committed} ,\,\@w{aborted} \} ]}% +\@pvspace{8.0pt}% + \@x{ TCInit \.{\defeq}\@s{8.2} rmState \.{=} [ r \.{\in} RM + \.{\mapsto}\@w{working} ]}% +\begin{lcom}{8.2}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +The initial predicate. +\end{cpar}% +\end{lcom}% +\@pvspace{8.0pt}% + \@x{ canCommit \.{\defeq} \A\, r \.{\in} RM \.{:} rmState [ r ] \.{\in} + \{\@w{prepared} ,\,\@w{committed} \}}% +\begin{lcom}{8.2}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + True iff all \ensuremath{RMs} are in the \ensuremath{\@w{prepared}} or + \ensuremath{\@w{committed}} state. +\end{cpar}% +\end{lcom}% +\@pvspace{8.0pt}% + \@x{ notCommitted \.{\defeq} \A\, r \.{\in} RM \.{:} rmState [ r ] + \.{\neq}\@w{committed}}% +\begin{lcom}{8.2}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +True iff no resource manager has decided to commit. +\end{cpar}% +\end{lcom}% +\@x{}\midbar\@xx{}% +\begin{lcom}{0}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + We now define the actions that may be performed by the \ensuremath{RMs}, and + then + define the complete next-state action of the specification to be the + disjunction of the possible \ensuremath{RM} actions. +\end{cpar}% +\end{lcom}% +\@x{ Prepare ( r ) \.{\defeq} \.{\land} rmState [ r ] \.{=}\@w{working}}% + \@x{\@s{65.81} \.{\land} rmState \.{'} \.{=} [ rmState {\EXCEPT} {\bang} [ r + ] \.{=}\@w{prepared} ]}% +\@pvspace{8.0pt}% + \@x{ Decide ( r )\@s{4.08} \.{\defeq} \.{\lor} \.{\land} rmState [ r ] + \.{=}\@w{prepared}}% +\@x{\@s{76.92} \.{\land} canCommit}% + \@x{\@s{76.92} \.{\land} rmState \.{'} \.{=} [ rmState {\EXCEPT} {\bang} [ r + ] \.{=}\@w{committed} ]}% + \@x{\@s{65.81} \.{\lor} \.{\land} rmState [ r ] \.{\in} \{\@w{working} + ,\,\@w{prepared} \}}% +\@x{\@s{76.92} \.{\land} notCommitted}% + \@x{\@s{76.92} \.{\land} rmState \.{'} \.{=} [ rmState {\EXCEPT} {\bang} [ r + ] \.{=}\@w{aborted} ]}% +\@pvspace{8.0pt}% + \@x{ TCNext \.{\defeq} \E\, r \.{\in} RM \.{:} Prepare ( r ) \.{\lor} Decide + ( r )}% +\begin{lcom}{8.2}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +The next-state action. +\end{cpar}% +\end{lcom}% +\@x{}\midbar\@xx{}% +\@x{ TCConsistent \.{\defeq}}% +\begin{lcom}{8.2}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +A state predicate asserting that two \ensuremath{RMs} have not arrived at + conflicting decisions. It is an invariant of the specification. +\end{cpar}% +\end{lcom}% + \@x{\@s{8.2} \A\, r1 ,\, r2 \.{\in} RM \.{:} {\lnot} \.{\land} rmState [ r1 ] + \.{=}\@w{aborted}}% +\@x{\@s{88.35} \.{\land} rmState [ r2 ] \.{=}\@w{committed}}% +\@x{}\midbar\@xx{}% +\begin{lcom}{0}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +The following part of the spec is not discussed in Video Lecture 5. It + will be explained in Video Lecture 8. +\end{cpar}% +\end{lcom}% +\@x{ TCSpec \.{\defeq} TCInit \.{\land} {\Box} [ TCNext ]_{ rmState}}% +\begin{lcom}{8.2}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +The complete specification of the protocol written as a temporal + formula. +\end{cpar}% +\end{lcom}% +\@pvspace{8.0pt}% + \@x{ {\THEOREM} TCSpec \.{\implies} {\Box} ( TCTypeOK \.{\land} TCConsistent + )}% +\begin{lcom}{8.2}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +This theorem asserts the truth of the temporal formula whose meaning + is that the state predicate \ensuremath{TCTypeOK \.{\land} TCInvariant} is + an invariant + of the specification \ensuremath{TCSpec}. Invariance of this conjunction is + equivalent to invariance of both of the formulas \ensuremath{TCTypeOK} and + \ensuremath{TCConsistent}. +\end{cpar}% +\end{lcom}% +\@pvspace{8.0pt}% +\@x{}\bottombar\@xx{}% +\setboolean{shading}{false} +\begin{lcom}{0}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +\ensuremath{\.{\,\backslash\,}}* Modification History +\end{cpar}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + \ensuremath{\.{\,\backslash\,}}* Last modified \ensuremath{Fri} + \ensuremath{Dec} 21 17:16:06 \ensuremath{CET} 2018 by \ensuremath{veitheller +}% +\end{cpar}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + \ensuremath{\.{\,\backslash\,}}* Created \ensuremath{Fri} \ensuremath{Dec} 21 + 17:15:44 \ensuremath{CET} 2018 by \ensuremath{veitheller +}% +\end{cpar}% +\end{lcom}% +\end{document} diff --git a/TCommit.toolbox/TCommit___Model_1.launch b/TCommit.toolbox/TCommit___Model_1.launch new file mode 100644 index 0000000..1a8db62 --- /dev/null +++ b/TCommit.toolbox/TCommit___Model_1.launch @@ -0,0 +1,48 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410479536.launch b/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410479536.launch new file mode 100644 index 0000000..700b4d7 --- /dev/null +++ b/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410479536.launch @@ -0,0 +1,47 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410497334.launch b/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410497334.launch new file mode 100644 index 0000000..f7e01b5 --- /dev/null +++ b/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410497334.launch @@ -0,0 +1,47 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410597019.launch b/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410597019.launch new file mode 100644 index 0000000..db2aec6 --- /dev/null +++ b/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410597019.launch @@ -0,0 +1,48 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/TwoPhase.tla b/TwoPhase.tla new file mode 100644 index 0000000..87617e6 --- /dev/null +++ b/TwoPhase.tla @@ -0,0 +1,182 @@ +------------------------------ MODULE TwoPhase ------------------------------ + +(***************************************************************************) +(* This specification is discussed in "Two-Phase Commit", Lecture 6 of the *) +(* TLA+ Video Course. It describes the Two-Phase Commit protocol, in *) +(* which a transaction manager (TM) coordinates the resource managers *) +(* (RMs) to implement the Transaction Commit specification of module *) +(* TCommit. In this specification, RMs spontaneously issue Prepared *) +(* messages. We ignore the Prepare messages that the TM can send to the *) +(* RMs. *) +(* *) +(* For simplicity, we also eliminate Abort messages sent by an RM when it *) +(* decides to abort. Such a message would cause the TM to abort the *) +(* transaction, an event represented here by the TM spontaneously deciding *) +(* to abort. *) +(***************************************************************************) +CONSTANT RM \* The set of resource managers + +VARIABLES + rmState, \* rmState[r] is the state of resource manager r. + tmState, \* The state of the transaction manager. + tmPrepared, \* The set of RMs from which the TM has received "Prepared" + \* messages. + msgs + (***********************************************************************) + (* In the protocol, processes communicate with one another by sending *) + (* messages. For simplicity, we represent message passing with the *) + (* variable msgs whose value is the set of all messages that have been *) + (* sent. A message is sent by adding it to the set msgs. An action *) + (* that, in an implementation, would be enabled by the receipt of a *) + (* certain message is here enabled by the presence of that message in *) + (* msgs. For simplicity, messages are never removed from msgs. This *) + (* allows a single message to be received by multiple receivers. *) + (* Receipt of the same message twice is therefore allowed; but in this *) + (* particular protocol, that's not a problem. *) + (***********************************************************************) + +Messages == + (*************************************************************************) + (* The set of all possible messages. Messages of type "Prepared" are *) + (* sent from the RM indicated by the message's rm field to the TM. *) + (* Messages of type "Commit" and "Abort" are broadcast by the TM, to be *) + (* received by all RMs. The set msgs contains just a single copy of *) + (* such a message. *) + (*************************************************************************) + [type : {"Prepared"}, rm : RM] \cup [type : {"Commit", "Abort"}] + +TPTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + /\ tmState \in {"init", "done"} + /\ tmPrepared \subseteq RM + /\ msgs \subseteq Messages + +TPInit == + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + /\ rmState = [r \in RM |-> "working"] + /\ tmState = "init" + /\ tmPrepared = {} + /\ msgs = {} +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the processes, first *) +(* the TM's actions, then the RMs' actions. *) +(***************************************************************************) +TMRcvPrepared(r) == + (*************************************************************************) + (* The TM receives a "Prepared" message from resource manager r. We *) + (* could add the additional enabling condition r \notin tmPrepared, *) + (* which disables the action if the TM has already received this *) + (* message. But there is no need, because in that case the action has *) + (* no effect; it leaves the state unchanged. *) + (*************************************************************************) + /\ tmState = "init" + /\ [type |-> "Prepared", rm |-> r] \in msgs + /\ tmPrepared' = tmPrepared \cup {r} + /\ UNCHANGED <> + +TMCommit == + (*************************************************************************) + (* The TM commits the transaction; enabled iff the TM is in its initial *) + (* state and every RM has sent a "Prepared" message. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmPrepared = RM + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Commit"]} + /\ UNCHANGED <> + +TMAbort == + (*************************************************************************) + (* The TM spontaneously aborts the transaction. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Abort"]} + /\ UNCHANGED <> + +RMPrepare(r) == + (*************************************************************************) + (* Resource manager r prepares. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]} + /\ UNCHANGED <> + +RMChooseToAbort(r) == + (*************************************************************************) + (* Resource manager r spontaneously decides to abort. As noted above, r *) + (* does not send any message in our simplified spec. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +RMRcvCommitMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to commit. *) + (*************************************************************************) + /\ [type |-> "Commit"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + /\ UNCHANGED <> + +RMRcvAbortMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to abort. *) + (*************************************************************************) + /\ [type |-> "Abort"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +TPNext == + \/ TMCommit \/ TMAbort + \/ \E r \in RM : + TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r) + \/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r) +----------------------------------------------------------------------------- +(***************************************************************************) +(* The material below this point is not discussed in Video Lecture 6. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) + +TPSpec == TPInit /\ [][TPNext]_<> + (*************************************************************************) + (* The complete spec of the Two-Phase Commit protocol. *) + (*************************************************************************) + +THEOREM TPSpec => []TPTypeOK + (*************************************************************************) + (* This theorem asserts that the type-correctness predicate TPTypeOK is *) + (* an invariant of the specification. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now assert that the Two-Phase Commit protocol implements the *) +(* Transaction Commit protocol of module TCommit. The following statement *) +(* imports all the definitions from module TCommit into the current *) +(* module. *) +(***************************************************************************) +INSTANCE TCommit + +THEOREM TPSpec => TCSpec + (*************************************************************************) + (* This theorem asserts that the specification TPSpec of the Two-Phase *) + (* Commit protocol implements the specification TCSpec of the *) + (* Transaction Commit protocol. *) + (*************************************************************************) +(***************************************************************************) +(* The two theorems in this module have been checked with TLC for six *) +(* RMs, a configuration with 50816 reachable states, in a little over a *) +(* minute on a 1 GHz PC. *) +(***************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Thu Dec 27 15:46:42 CET 2018 by veitheller +\* Created Thu Dec 27 15:46:21 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/.project b/TwoPhase.toolbox/.project new file mode 100644 index 0000000..bdb139b --- /dev/null +++ b/TwoPhase.toolbox/.project @@ -0,0 +1,29 @@ + + + TwoPhase + + + + + + toolbox.builder.TLAParserBuilder + + + + + + toolbox.natures.TLANature + + + + TCommit.tla + 1 + /Users/veitheller/Documents/Code/Github/simple/TCommit.tla + + + TwoPhase.tla + 1 + PARENT-1-PROJECT_LOC/TwoPhase.tla + + + diff --git a/TwoPhase.toolbox/.settings/org.lamport.tla.toolbox.prefs b/TwoPhase.toolbox/.settings/org.lamport.tla.toolbox.prefs new file mode 100644 index 0000000..31b2e59 --- /dev/null +++ b/TwoPhase.toolbox/.settings/org.lamport.tla.toolbox.prefs @@ -0,0 +1,2 @@ +ProjectRootFile=PARENT-1-PROJECT_LOC/TwoPhase.tla +eclipse.preferences.version=1 diff --git a/TwoPhase.toolbox/Model_1/MC.cfg b/TwoPhase.toolbox/Model_1/MC.cfg new file mode 100644 index 0000000..b750119 --- /dev/null +++ b/TwoPhase.toolbox/Model_1/MC.cfg @@ -0,0 +1,21 @@ +\* MV CONSTANT declarations +CONSTANTS +r1 = r1 +r2 = r2 +r3 = r3 +\* MV CONSTANT definitions +CONSTANT +RM <- const_154592300704034000 +\* SYMMETRY definition +SYMMETRY symm_154592300704035000 +\* INIT definition +INIT +init_154592300704036000 +\* NEXT definition +NEXT +next_154592300704037000 +\* INVARIANT definition +INVARIANT +inv_154592300704038000 +inv_154592300704039000 +\* Generated on Thu Dec 27 16:03:27 CET 2018 \ No newline at end of file diff --git a/TwoPhase.toolbox/Model_1/MC.tla b/TwoPhase.toolbox/Model_1/MC.tla new file mode 100644 index 0000000..150e7b1 --- /dev/null +++ b/TwoPhase.toolbox/Model_1/MC.tla @@ -0,0 +1,37 @@ +---- MODULE MC ---- +EXTENDS TwoPhase, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +r1, r2, r3 +---- + +\* MV CONSTANT definitions RM +const_154592300704034000 == +{r1, r2, r3} +---- + +\* SYMMETRY definition +symm_154592300704035000 == +Permutations(const_154592300704034000) +---- + +\* INIT definition @modelBehaviorInit:0 +init_154592300704036000 == +TPInit +---- +\* NEXT definition @modelBehaviorNext:0 +next_154592300704037000 == +TPNext +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154592300704038000 == +TPTypeOK +---- +\* INVARIANT definition @modelCorrectnessInvariants:1 +inv_154592300704039000 == +TCConsistent +---- +============================================================================= +\* Modification History +\* Created Thu Dec 27 16:03:27 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1/TCommit.tla b/TwoPhase.toolbox/Model_1/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TwoPhase.toolbox/Model_1/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1/TwoPhase.tla b/TwoPhase.toolbox/Model_1/TwoPhase.tla new file mode 100644 index 0000000..87617e6 --- /dev/null +++ b/TwoPhase.toolbox/Model_1/TwoPhase.tla @@ -0,0 +1,182 @@ +------------------------------ MODULE TwoPhase ------------------------------ + +(***************************************************************************) +(* This specification is discussed in "Two-Phase Commit", Lecture 6 of the *) +(* TLA+ Video Course. It describes the Two-Phase Commit protocol, in *) +(* which a transaction manager (TM) coordinates the resource managers *) +(* (RMs) to implement the Transaction Commit specification of module *) +(* TCommit. In this specification, RMs spontaneously issue Prepared *) +(* messages. We ignore the Prepare messages that the TM can send to the *) +(* RMs. *) +(* *) +(* For simplicity, we also eliminate Abort messages sent by an RM when it *) +(* decides to abort. Such a message would cause the TM to abort the *) +(* transaction, an event represented here by the TM spontaneously deciding *) +(* to abort. *) +(***************************************************************************) +CONSTANT RM \* The set of resource managers + +VARIABLES + rmState, \* rmState[r] is the state of resource manager r. + tmState, \* The state of the transaction manager. + tmPrepared, \* The set of RMs from which the TM has received "Prepared" + \* messages. + msgs + (***********************************************************************) + (* In the protocol, processes communicate with one another by sending *) + (* messages. For simplicity, we represent message passing with the *) + (* variable msgs whose value is the set of all messages that have been *) + (* sent. A message is sent by adding it to the set msgs. An action *) + (* that, in an implementation, would be enabled by the receipt of a *) + (* certain message is here enabled by the presence of that message in *) + (* msgs. For simplicity, messages are never removed from msgs. This *) + (* allows a single message to be received by multiple receivers. *) + (* Receipt of the same message twice is therefore allowed; but in this *) + (* particular protocol, that's not a problem. *) + (***********************************************************************) + +Messages == + (*************************************************************************) + (* The set of all possible messages. Messages of type "Prepared" are *) + (* sent from the RM indicated by the message's rm field to the TM. *) + (* Messages of type "Commit" and "Abort" are broadcast by the TM, to be *) + (* received by all RMs. The set msgs contains just a single copy of *) + (* such a message. *) + (*************************************************************************) + [type : {"Prepared"}, rm : RM] \cup [type : {"Commit", "Abort"}] + +TPTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + /\ tmState \in {"init", "done"} + /\ tmPrepared \subseteq RM + /\ msgs \subseteq Messages + +TPInit == + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + /\ rmState = [r \in RM |-> "working"] + /\ tmState = "init" + /\ tmPrepared = {} + /\ msgs = {} +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the processes, first *) +(* the TM's actions, then the RMs' actions. *) +(***************************************************************************) +TMRcvPrepared(r) == + (*************************************************************************) + (* The TM receives a "Prepared" message from resource manager r. We *) + (* could add the additional enabling condition r \notin tmPrepared, *) + (* which disables the action if the TM has already received this *) + (* message. But there is no need, because in that case the action has *) + (* no effect; it leaves the state unchanged. *) + (*************************************************************************) + /\ tmState = "init" + /\ [type |-> "Prepared", rm |-> r] \in msgs + /\ tmPrepared' = tmPrepared \cup {r} + /\ UNCHANGED <> + +TMCommit == + (*************************************************************************) + (* The TM commits the transaction; enabled iff the TM is in its initial *) + (* state and every RM has sent a "Prepared" message. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmPrepared = RM + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Commit"]} + /\ UNCHANGED <> + +TMAbort == + (*************************************************************************) + (* The TM spontaneously aborts the transaction. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Abort"]} + /\ UNCHANGED <> + +RMPrepare(r) == + (*************************************************************************) + (* Resource manager r prepares. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]} + /\ UNCHANGED <> + +RMChooseToAbort(r) == + (*************************************************************************) + (* Resource manager r spontaneously decides to abort. As noted above, r *) + (* does not send any message in our simplified spec. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +RMRcvCommitMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to commit. *) + (*************************************************************************) + /\ [type |-> "Commit"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + /\ UNCHANGED <> + +RMRcvAbortMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to abort. *) + (*************************************************************************) + /\ [type |-> "Abort"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +TPNext == + \/ TMCommit \/ TMAbort + \/ \E r \in RM : + TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r) + \/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r) +----------------------------------------------------------------------------- +(***************************************************************************) +(* The material below this point is not discussed in Video Lecture 6. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) + +TPSpec == TPInit /\ [][TPNext]_<> + (*************************************************************************) + (* The complete spec of the Two-Phase Commit protocol. *) + (*************************************************************************) + +THEOREM TPSpec => []TPTypeOK + (*************************************************************************) + (* This theorem asserts that the type-correctness predicate TPTypeOK is *) + (* an invariant of the specification. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now assert that the Two-Phase Commit protocol implements the *) +(* Transaction Commit protocol of module TCommit. The following statement *) +(* imports all the definitions from module TCommit into the current *) +(* module. *) +(***************************************************************************) +INSTANCE TCommit + +THEOREM TPSpec => TCSpec + (*************************************************************************) + (* This theorem asserts that the specification TPSpec of the Two-Phase *) + (* Commit protocol implements the specification TCSpec of the *) + (* Transaction Commit protocol. *) + (*************************************************************************) +(***************************************************************************) +(* The two theorems in this module have been checked with TLC for six *) +(* RMs, a configuration with 50816 reachable states, in a little over a *) +(* minute on a 1 GHz PC. *) +(***************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Thu Dec 27 15:46:42 CET 2018 by veitheller +\* Created Thu Dec 27 15:46:21 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/MC.cfg b/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/MC.cfg new file mode 100644 index 0000000..8c379b1 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/MC.cfg @@ -0,0 +1,13 @@ +\* CONSTANT definitions +CONSTANT +RM <- const_15459227497686000 +\* INIT definition +INIT +init_15459227497687000 +\* NEXT definition +NEXT +next_15459227497688000 +\* INVARIANT definition +INVARIANT +inv_15459227497689000 +\* Generated on Thu Dec 27 15:59:09 CET 2018 \ No newline at end of file diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/MC.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/MC.tla new file mode 100644 index 0000000..22fce1f --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/MC.tla @@ -0,0 +1,23 @@ +---- MODULE MC ---- +EXTENDS TwoPhase, TLC + +\* CONSTANT definitions @modelParameterConstants:0RM +const_15459227497686000 == +{"r1", "r2", "r3"} +---- + +\* INIT definition @modelBehaviorInit:0 +init_15459227497687000 == +TPInit +---- +\* NEXT definition @modelBehaviorNext:0 +next_15459227497688000 == +TPNext +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_15459227497689000 == +TPTypeOK +---- +============================================================================= +\* Modification History +\* Created Thu Dec 27 15:59:09 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/TCommit.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/TwoPhase.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/TwoPhase.tla new file mode 100644 index 0000000..87617e6 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/TwoPhase.tla @@ -0,0 +1,182 @@ +------------------------------ MODULE TwoPhase ------------------------------ + +(***************************************************************************) +(* This specification is discussed in "Two-Phase Commit", Lecture 6 of the *) +(* TLA+ Video Course. It describes the Two-Phase Commit protocol, in *) +(* which a transaction manager (TM) coordinates the resource managers *) +(* (RMs) to implement the Transaction Commit specification of module *) +(* TCommit. In this specification, RMs spontaneously issue Prepared *) +(* messages. We ignore the Prepare messages that the TM can send to the *) +(* RMs. *) +(* *) +(* For simplicity, we also eliminate Abort messages sent by an RM when it *) +(* decides to abort. Such a message would cause the TM to abort the *) +(* transaction, an event represented here by the TM spontaneously deciding *) +(* to abort. *) +(***************************************************************************) +CONSTANT RM \* The set of resource managers + +VARIABLES + rmState, \* rmState[r] is the state of resource manager r. + tmState, \* The state of the transaction manager. + tmPrepared, \* The set of RMs from which the TM has received "Prepared" + \* messages. + msgs + (***********************************************************************) + (* In the protocol, processes communicate with one another by sending *) + (* messages. For simplicity, we represent message passing with the *) + (* variable msgs whose value is the set of all messages that have been *) + (* sent. A message is sent by adding it to the set msgs. An action *) + (* that, in an implementation, would be enabled by the receipt of a *) + (* certain message is here enabled by the presence of that message in *) + (* msgs. For simplicity, messages are never removed from msgs. This *) + (* allows a single message to be received by multiple receivers. *) + (* Receipt of the same message twice is therefore allowed; but in this *) + (* particular protocol, that's not a problem. *) + (***********************************************************************) + +Messages == + (*************************************************************************) + (* The set of all possible messages. Messages of type "Prepared" are *) + (* sent from the RM indicated by the message's rm field to the TM. *) + (* Messages of type "Commit" and "Abort" are broadcast by the TM, to be *) + (* received by all RMs. The set msgs contains just a single copy of *) + (* such a message. *) + (*************************************************************************) + [type : {"Prepared"}, rm : RM] \cup [type : {"Commit", "Abort"}] + +TPTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + /\ tmState \in {"init", "done"} + /\ tmPrepared \subseteq RM + /\ msgs \subseteq Messages + +TPInit == + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + /\ rmState = [r \in RM |-> "working"] + /\ tmState = "init" + /\ tmPrepared = {} + /\ msgs = {} +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the processes, first *) +(* the TM's actions, then the RMs' actions. *) +(***************************************************************************) +TMRcvPrepared(r) == + (*************************************************************************) + (* The TM receives a "Prepared" message from resource manager r. We *) + (* could add the additional enabling condition r \notin tmPrepared, *) + (* which disables the action if the TM has already received this *) + (* message. But there is no need, because in that case the action has *) + (* no effect; it leaves the state unchanged. *) + (*************************************************************************) + /\ tmState = "init" + /\ [type |-> "Prepared", rm |-> r] \in msgs + /\ tmPrepared' = tmPrepared \cup {r} + /\ UNCHANGED <> + +TMCommit == + (*************************************************************************) + (* The TM commits the transaction; enabled iff the TM is in its initial *) + (* state and every RM has sent a "Prepared" message. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmPrepared = RM + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Commit"]} + /\ UNCHANGED <> + +TMAbort == + (*************************************************************************) + (* The TM spontaneously aborts the transaction. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Abort"]} + /\ UNCHANGED <> + +RMPrepare(r) == + (*************************************************************************) + (* Resource manager r prepares. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]} + /\ UNCHANGED <> + +RMChooseToAbort(r) == + (*************************************************************************) + (* Resource manager r spontaneously decides to abort. As noted above, r *) + (* does not send any message in our simplified spec. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +RMRcvCommitMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to commit. *) + (*************************************************************************) + /\ [type |-> "Commit"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + /\ UNCHANGED <> + +RMRcvAbortMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to abort. *) + (*************************************************************************) + /\ [type |-> "Abort"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +TPNext == + \/ TMCommit \/ TMAbort + \/ \E r \in RM : + TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r) + \/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r) +----------------------------------------------------------------------------- +(***************************************************************************) +(* The material below this point is not discussed in Video Lecture 6. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) + +TPSpec == TPInit /\ [][TPNext]_<> + (*************************************************************************) + (* The complete spec of the Two-Phase Commit protocol. *) + (*************************************************************************) + +THEOREM TPSpec => []TPTypeOK + (*************************************************************************) + (* This theorem asserts that the type-correctness predicate TPTypeOK is *) + (* an invariant of the specification. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now assert that the Two-Phase Commit protocol implements the *) +(* Transaction Commit protocol of module TCommit. The following statement *) +(* imports all the definitions from module TCommit into the current *) +(* module. *) +(***************************************************************************) +INSTANCE TCommit + +THEOREM TPSpec => TCSpec + (*************************************************************************) + (* This theorem asserts that the specification TPSpec of the Two-Phase *) + (* Commit protocol implements the specification TCSpec of the *) + (* Transaction Commit protocol. *) + (*************************************************************************) +(***************************************************************************) +(* The two theorems in this module have been checked with TLC for six *) +(* RMs, a configuration with 50816 reachable states, in a little over a *) +(* minute on a 1 GHz PC. *) +(***************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Thu Dec 27 15:46:42 CET 2018 by veitheller +\* Created Thu Dec 27 15:46:21 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/MC.cfg b/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/MC.cfg new file mode 100644 index 0000000..f0cd133 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/MC.cfg @@ -0,0 +1,13 @@ +\* CONSTANT definitions +CONSTANT +RM <- const_154592286770714000 +\* INIT definition +INIT +init_154592286770715000 +\* NEXT definition +NEXT +next_154592286770716000 +\* INVARIANT definition +INVARIANT +inv_154592286770717000 +\* Generated on Thu Dec 27 16:01:07 CET 2018 \ No newline at end of file diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/MC.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/MC.tla new file mode 100644 index 0000000..5c504ea --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/MC.tla @@ -0,0 +1,23 @@ +---- MODULE MC ---- +EXTENDS TwoPhase, TLC + +\* CONSTANT definitions @modelParameterConstants:0RM +const_154592286770714000 == +{"r1", "r2", "r3", "r4", "r5"} +---- + +\* INIT definition @modelBehaviorInit:0 +init_154592286770715000 == +TPInit +---- +\* NEXT definition @modelBehaviorNext:0 +next_154592286770716000 == +TPNext +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154592286770717000 == +TPTypeOK +---- +============================================================================= +\* Modification History +\* Created Thu Dec 27 16:01:07 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/TCommit.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/TwoPhase.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/TwoPhase.tla new file mode 100644 index 0000000..87617e6 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/TwoPhase.tla @@ -0,0 +1,182 @@ +------------------------------ MODULE TwoPhase ------------------------------ + +(***************************************************************************) +(* This specification is discussed in "Two-Phase Commit", Lecture 6 of the *) +(* TLA+ Video Course. It describes the Two-Phase Commit protocol, in *) +(* which a transaction manager (TM) coordinates the resource managers *) +(* (RMs) to implement the Transaction Commit specification of module *) +(* TCommit. In this specification, RMs spontaneously issue Prepared *) +(* messages. We ignore the Prepare messages that the TM can send to the *) +(* RMs. *) +(* *) +(* For simplicity, we also eliminate Abort messages sent by an RM when it *) +(* decides to abort. Such a message would cause the TM to abort the *) +(* transaction, an event represented here by the TM spontaneously deciding *) +(* to abort. *) +(***************************************************************************) +CONSTANT RM \* The set of resource managers + +VARIABLES + rmState, \* rmState[r] is the state of resource manager r. + tmState, \* The state of the transaction manager. + tmPrepared, \* The set of RMs from which the TM has received "Prepared" + \* messages. + msgs + (***********************************************************************) + (* In the protocol, processes communicate with one another by sending *) + (* messages. For simplicity, we represent message passing with the *) + (* variable msgs whose value is the set of all messages that have been *) + (* sent. A message is sent by adding it to the set msgs. An action *) + (* that, in an implementation, would be enabled by the receipt of a *) + (* certain message is here enabled by the presence of that message in *) + (* msgs. For simplicity, messages are never removed from msgs. This *) + (* allows a single message to be received by multiple receivers. *) + (* Receipt of the same message twice is therefore allowed; but in this *) + (* particular protocol, that's not a problem. *) + (***********************************************************************) + +Messages == + (*************************************************************************) + (* The set of all possible messages. Messages of type "Prepared" are *) + (* sent from the RM indicated by the message's rm field to the TM. *) + (* Messages of type "Commit" and "Abort" are broadcast by the TM, to be *) + (* received by all RMs. The set msgs contains just a single copy of *) + (* such a message. *) + (*************************************************************************) + [type : {"Prepared"}, rm : RM] \cup [type : {"Commit", "Abort"}] + +TPTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + /\ tmState \in {"init", "done"} + /\ tmPrepared \subseteq RM + /\ msgs \subseteq Messages + +TPInit == + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + /\ rmState = [r \in RM |-> "working"] + /\ tmState = "init" + /\ tmPrepared = {} + /\ msgs = {} +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the processes, first *) +(* the TM's actions, then the RMs' actions. *) +(***************************************************************************) +TMRcvPrepared(r) == + (*************************************************************************) + (* The TM receives a "Prepared" message from resource manager r. We *) + (* could add the additional enabling condition r \notin tmPrepared, *) + (* which disables the action if the TM has already received this *) + (* message. But there is no need, because in that case the action has *) + (* no effect; it leaves the state unchanged. *) + (*************************************************************************) + /\ tmState = "init" + /\ [type |-> "Prepared", rm |-> r] \in msgs + /\ tmPrepared' = tmPrepared \cup {r} + /\ UNCHANGED <> + +TMCommit == + (*************************************************************************) + (* The TM commits the transaction; enabled iff the TM is in its initial *) + (* state and every RM has sent a "Prepared" message. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmPrepared = RM + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Commit"]} + /\ UNCHANGED <> + +TMAbort == + (*************************************************************************) + (* The TM spontaneously aborts the transaction. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Abort"]} + /\ UNCHANGED <> + +RMPrepare(r) == + (*************************************************************************) + (* Resource manager r prepares. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]} + /\ UNCHANGED <> + +RMChooseToAbort(r) == + (*************************************************************************) + (* Resource manager r spontaneously decides to abort. As noted above, r *) + (* does not send any message in our simplified spec. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +RMRcvCommitMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to commit. *) + (*************************************************************************) + /\ [type |-> "Commit"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + /\ UNCHANGED <> + +RMRcvAbortMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to abort. *) + (*************************************************************************) + /\ [type |-> "Abort"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +TPNext == + \/ TMCommit \/ TMAbort + \/ \E r \in RM : + TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r) + \/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r) +----------------------------------------------------------------------------- +(***************************************************************************) +(* The material below this point is not discussed in Video Lecture 6. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) + +TPSpec == TPInit /\ [][TPNext]_<> + (*************************************************************************) + (* The complete spec of the Two-Phase Commit protocol. *) + (*************************************************************************) + +THEOREM TPSpec => []TPTypeOK + (*************************************************************************) + (* This theorem asserts that the type-correctness predicate TPTypeOK is *) + (* an invariant of the specification. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now assert that the Two-Phase Commit protocol implements the *) +(* Transaction Commit protocol of module TCommit. The following statement *) +(* imports all the definitions from module TCommit into the current *) +(* module. *) +(***************************************************************************) +INSTANCE TCommit + +THEOREM TPSpec => TCSpec + (*************************************************************************) + (* This theorem asserts that the specification TPSpec of the Two-Phase *) + (* Commit protocol implements the specification TCSpec of the *) + (* Transaction Commit protocol. *) + (*************************************************************************) +(***************************************************************************) +(* The two theorems in this module have been checked with TLC for six *) +(* RMs, a configuration with 50816 reachable states, in a little over a *) +(* minute on a 1 GHz PC. *) +(***************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Thu Dec 27 15:46:42 CET 2018 by veitheller +\* Created Thu Dec 27 15:46:21 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/MC.cfg b/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/MC.cfg new file mode 100644 index 0000000..5f1cfb2 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/MC.cfg @@ -0,0 +1,20 @@ +\* MV CONSTANT declarations +CONSTANTS +r1 = r1 +r2 = r2 +r3 = r3 +\* MV CONSTANT definitions +CONSTANT +RM <- const_154592291369123000 +\* SYMMETRY definition +SYMMETRY symm_154592291369124000 +\* INIT definition +INIT +init_154592291369125000 +\* NEXT definition +NEXT +next_154592291369126000 +\* INVARIANT definition +INVARIANT +inv_154592291369127000 +\* Generated on Thu Dec 27 16:01:53 CET 2018 \ No newline at end of file diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/MC.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/MC.tla new file mode 100644 index 0000000..64572bf --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/MC.tla @@ -0,0 +1,33 @@ +---- MODULE MC ---- +EXTENDS TwoPhase, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +r1, r2, r3 +---- + +\* MV CONSTANT definitions RM +const_154592291369123000 == +{r1, r2, r3} +---- + +\* SYMMETRY definition +symm_154592291369124000 == +Permutations(const_154592291369123000) +---- + +\* INIT definition @modelBehaviorInit:0 +init_154592291369125000 == +TPInit +---- +\* NEXT definition @modelBehaviorNext:0 +next_154592291369126000 == +TPNext +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154592291369127000 == +TPTypeOK +---- +============================================================================= +\* Modification History +\* Created Thu Dec 27 16:01:53 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/TCommit.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/TwoPhase.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/TwoPhase.tla new file mode 100644 index 0000000..87617e6 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/TwoPhase.tla @@ -0,0 +1,182 @@ +------------------------------ MODULE TwoPhase ------------------------------ + +(***************************************************************************) +(* This specification is discussed in "Two-Phase Commit", Lecture 6 of the *) +(* TLA+ Video Course. It describes the Two-Phase Commit protocol, in *) +(* which a transaction manager (TM) coordinates the resource managers *) +(* (RMs) to implement the Transaction Commit specification of module *) +(* TCommit. In this specification, RMs spontaneously issue Prepared *) +(* messages. We ignore the Prepare messages that the TM can send to the *) +(* RMs. *) +(* *) +(* For simplicity, we also eliminate Abort messages sent by an RM when it *) +(* decides to abort. Such a message would cause the TM to abort the *) +(* transaction, an event represented here by the TM spontaneously deciding *) +(* to abort. *) +(***************************************************************************) +CONSTANT RM \* The set of resource managers + +VARIABLES + rmState, \* rmState[r] is the state of resource manager r. + tmState, \* The state of the transaction manager. + tmPrepared, \* The set of RMs from which the TM has received "Prepared" + \* messages. + msgs + (***********************************************************************) + (* In the protocol, processes communicate with one another by sending *) + (* messages. For simplicity, we represent message passing with the *) + (* variable msgs whose value is the set of all messages that have been *) + (* sent. A message is sent by adding it to the set msgs. An action *) + (* that, in an implementation, would be enabled by the receipt of a *) + (* certain message is here enabled by the presence of that message in *) + (* msgs. For simplicity, messages are never removed from msgs. This *) + (* allows a single message to be received by multiple receivers. *) + (* Receipt of the same message twice is therefore allowed; but in this *) + (* particular protocol, that's not a problem. *) + (***********************************************************************) + +Messages == + (*************************************************************************) + (* The set of all possible messages. Messages of type "Prepared" are *) + (* sent from the RM indicated by the message's rm field to the TM. *) + (* Messages of type "Commit" and "Abort" are broadcast by the TM, to be *) + (* received by all RMs. The set msgs contains just a single copy of *) + (* such a message. *) + (*************************************************************************) + [type : {"Prepared"}, rm : RM] \cup [type : {"Commit", "Abort"}] + +TPTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + /\ tmState \in {"init", "done"} + /\ tmPrepared \subseteq RM + /\ msgs \subseteq Messages + +TPInit == + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + /\ rmState = [r \in RM |-> "working"] + /\ tmState = "init" + /\ tmPrepared = {} + /\ msgs = {} +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the processes, first *) +(* the TM's actions, then the RMs' actions. *) +(***************************************************************************) +TMRcvPrepared(r) == + (*************************************************************************) + (* The TM receives a "Prepared" message from resource manager r. We *) + (* could add the additional enabling condition r \notin tmPrepared, *) + (* which disables the action if the TM has already received this *) + (* message. But there is no need, because in that case the action has *) + (* no effect; it leaves the state unchanged. *) + (*************************************************************************) + /\ tmState = "init" + /\ [type |-> "Prepared", rm |-> r] \in msgs + /\ tmPrepared' = tmPrepared \cup {r} + /\ UNCHANGED <> + +TMCommit == + (*************************************************************************) + (* The TM commits the transaction; enabled iff the TM is in its initial *) + (* state and every RM has sent a "Prepared" message. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmPrepared = RM + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Commit"]} + /\ UNCHANGED <> + +TMAbort == + (*************************************************************************) + (* The TM spontaneously aborts the transaction. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Abort"]} + /\ UNCHANGED <> + +RMPrepare(r) == + (*************************************************************************) + (* Resource manager r prepares. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]} + /\ UNCHANGED <> + +RMChooseToAbort(r) == + (*************************************************************************) + (* Resource manager r spontaneously decides to abort. As noted above, r *) + (* does not send any message in our simplified spec. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +RMRcvCommitMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to commit. *) + (*************************************************************************) + /\ [type |-> "Commit"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + /\ UNCHANGED <> + +RMRcvAbortMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to abort. *) + (*************************************************************************) + /\ [type |-> "Abort"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +TPNext == + \/ TMCommit \/ TMAbort + \/ \E r \in RM : + TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r) + \/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r) +----------------------------------------------------------------------------- +(***************************************************************************) +(* The material below this point is not discussed in Video Lecture 6. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) + +TPSpec == TPInit /\ [][TPNext]_<> + (*************************************************************************) + (* The complete spec of the Two-Phase Commit protocol. *) + (*************************************************************************) + +THEOREM TPSpec => []TPTypeOK + (*************************************************************************) + (* This theorem asserts that the type-correctness predicate TPTypeOK is *) + (* an invariant of the specification. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now assert that the Two-Phase Commit protocol implements the *) +(* Transaction Commit protocol of module TCommit. The following statement *) +(* imports all the definitions from module TCommit into the current *) +(* module. *) +(***************************************************************************) +INSTANCE TCommit + +THEOREM TPSpec => TCSpec + (*************************************************************************) + (* This theorem asserts that the specification TPSpec of the Two-Phase *) + (* Commit protocol implements the specification TCSpec of the *) + (* Transaction Commit protocol. *) + (*************************************************************************) +(***************************************************************************) +(* The two theorems in this module have been checked with TLC for six *) +(* RMs, a configuration with 50816 reachable states, in a little over a *) +(* minute on a 1 GHz PC. *) +(***************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Thu Dec 27 15:46:42 CET 2018 by veitheller +\* Created Thu Dec 27 15:46:21 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/MC.cfg b/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/MC.cfg new file mode 100644 index 0000000..b750119 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/MC.cfg @@ -0,0 +1,21 @@ +\* MV CONSTANT declarations +CONSTANTS +r1 = r1 +r2 = r2 +r3 = r3 +\* MV CONSTANT definitions +CONSTANT +RM <- const_154592300704034000 +\* SYMMETRY definition +SYMMETRY symm_154592300704035000 +\* INIT definition +INIT +init_154592300704036000 +\* NEXT definition +NEXT +next_154592300704037000 +\* INVARIANT definition +INVARIANT +inv_154592300704038000 +inv_154592300704039000 +\* Generated on Thu Dec 27 16:03:27 CET 2018 \ No newline at end of file diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/MC.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/MC.tla new file mode 100644 index 0000000..150e7b1 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/MC.tla @@ -0,0 +1,37 @@ +---- MODULE MC ---- +EXTENDS TwoPhase, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +r1, r2, r3 +---- + +\* MV CONSTANT definitions RM +const_154592300704034000 == +{r1, r2, r3} +---- + +\* SYMMETRY definition +symm_154592300704035000 == +Permutations(const_154592300704034000) +---- + +\* INIT definition @modelBehaviorInit:0 +init_154592300704036000 == +TPInit +---- +\* NEXT definition @modelBehaviorNext:0 +next_154592300704037000 == +TPNext +---- +\* INVARIANT definition @modelCorrectnessInvariants:0 +inv_154592300704038000 == +TPTypeOK +---- +\* INVARIANT definition @modelCorrectnessInvariants:1 +inv_154592300704039000 == +TCConsistent +---- +============================================================================= +\* Modification History +\* Created Thu Dec 27 16:03:27 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/TCommit.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/TCommit.tla new file mode 100644 index 0000000..86364e1 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/TCommit.tla @@ -0,0 +1,82 @@ +------------------------------ MODULE TCommit ------------------------------ + +(***************************************************************************) +(* This specification is explained in "Transaction Commit", Lecture 5 of *) +(* the TLA+ Video Course. *) +(***************************************************************************) +CONSTANT RM \* The set of participating resource managers + +VARIABLE rmState \* rmState[rm] is the state of resource manager r. +----------------------------------------------------------------------------- +TCTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + +TCInit == rmState = [r \in RM |-> "working"] + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + +canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"} + (*************************************************************************) + (* True iff all RMs are in the "prepared" or "committed" state. *) + (*************************************************************************) + +notCommitted == \A r \in RM : rmState[r] # "committed" + (*************************************************************************) + (* True iff no resource manager has decided to commit. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the RMs, and then *) +(* define the complete next-state action of the specification to be the *) +(* disjunction of the possible RM actions. *) +(***************************************************************************) +Prepare(r) == /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + +Decide(r) == \/ /\ rmState[r] = "prepared" + /\ canCommit + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + \/ /\ rmState[r] \in {"working", "prepared"} + /\ notCommitted + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + +TCNext == \E r \in RM : Prepare(r) \/ Decide(r) + (*************************************************************************) + (* The next-state action. *) + (*************************************************************************) +----------------------------------------------------------------------------- +TCConsistent == + (*************************************************************************) + (* A state predicate asserting that two RMs have not arrived at *) + (* conflicting decisions. It is an invariant of the specification. *) + (*************************************************************************) + \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted" + /\ rmState[r2] = "committed" +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not discussed in Video Lecture 5. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) +TCSpec == TCInit /\ [][TCNext]_rmState + (*************************************************************************) + (* The complete specification of the protocol written as a temporal *) + (* formula. *) + (*************************************************************************) + +THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) + (*************************************************************************) + (* This theorem asserts the truth of the temporal formula whose meaning *) + (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant *) + (* of the specification TCSpec. Invariance of this conjunction is *) + (* equivalent to invariance of both of the formulas TCTypeOK and *) + (* TCConsistent. *) + (*************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 17:16:06 CET 2018 by veitheller +\* Created Fri Dec 21 17:15:44 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/TwoPhase.tla b/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/TwoPhase.tla new file mode 100644 index 0000000..87617e6 --- /dev/null +++ b/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/TwoPhase.tla @@ -0,0 +1,182 @@ +------------------------------ MODULE TwoPhase ------------------------------ + +(***************************************************************************) +(* This specification is discussed in "Two-Phase Commit", Lecture 6 of the *) +(* TLA+ Video Course. It describes the Two-Phase Commit protocol, in *) +(* which a transaction manager (TM) coordinates the resource managers *) +(* (RMs) to implement the Transaction Commit specification of module *) +(* TCommit. In this specification, RMs spontaneously issue Prepared *) +(* messages. We ignore the Prepare messages that the TM can send to the *) +(* RMs. *) +(* *) +(* For simplicity, we also eliminate Abort messages sent by an RM when it *) +(* decides to abort. Such a message would cause the TM to abort the *) +(* transaction, an event represented here by the TM spontaneously deciding *) +(* to abort. *) +(***************************************************************************) +CONSTANT RM \* The set of resource managers + +VARIABLES + rmState, \* rmState[r] is the state of resource manager r. + tmState, \* The state of the transaction manager. + tmPrepared, \* The set of RMs from which the TM has received "Prepared" + \* messages. + msgs + (***********************************************************************) + (* In the protocol, processes communicate with one another by sending *) + (* messages. For simplicity, we represent message passing with the *) + (* variable msgs whose value is the set of all messages that have been *) + (* sent. A message is sent by adding it to the set msgs. An action *) + (* that, in an implementation, would be enabled by the receipt of a *) + (* certain message is here enabled by the presence of that message in *) + (* msgs. For simplicity, messages are never removed from msgs. This *) + (* allows a single message to be received by multiple receivers. *) + (* Receipt of the same message twice is therefore allowed; but in this *) + (* particular protocol, that's not a problem. *) + (***********************************************************************) + +Messages == + (*************************************************************************) + (* The set of all possible messages. Messages of type "Prepared" are *) + (* sent from the RM indicated by the message's rm field to the TM. *) + (* Messages of type "Commit" and "Abort" are broadcast by the TM, to be *) + (* received by all RMs. The set msgs contains just a single copy of *) + (* such a message. *) + (*************************************************************************) + [type : {"Prepared"}, rm : RM] \cup [type : {"Commit", "Abort"}] + +TPTypeOK == + (*************************************************************************) + (* The type-correctness invariant *) + (*************************************************************************) + /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + /\ tmState \in {"init", "done"} + /\ tmPrepared \subseteq RM + /\ msgs \subseteq Messages + +TPInit == + (*************************************************************************) + (* The initial predicate. *) + (*************************************************************************) + /\ rmState = [r \in RM |-> "working"] + /\ tmState = "init" + /\ tmPrepared = {} + /\ msgs = {} +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now define the actions that may be performed by the processes, first *) +(* the TM's actions, then the RMs' actions. *) +(***************************************************************************) +TMRcvPrepared(r) == + (*************************************************************************) + (* The TM receives a "Prepared" message from resource manager r. We *) + (* could add the additional enabling condition r \notin tmPrepared, *) + (* which disables the action if the TM has already received this *) + (* message. But there is no need, because in that case the action has *) + (* no effect; it leaves the state unchanged. *) + (*************************************************************************) + /\ tmState = "init" + /\ [type |-> "Prepared", rm |-> r] \in msgs + /\ tmPrepared' = tmPrepared \cup {r} + /\ UNCHANGED <> + +TMCommit == + (*************************************************************************) + (* The TM commits the transaction; enabled iff the TM is in its initial *) + (* state and every RM has sent a "Prepared" message. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmPrepared = RM + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Commit"]} + /\ UNCHANGED <> + +TMAbort == + (*************************************************************************) + (* The TM spontaneously aborts the transaction. *) + (*************************************************************************) + /\ tmState = "init" + /\ tmState' = "done" + /\ msgs' = msgs \cup {[type |-> "Abort"]} + /\ UNCHANGED <> + +RMPrepare(r) == + (*************************************************************************) + (* Resource manager r prepares. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]} + /\ UNCHANGED <> + +RMChooseToAbort(r) == + (*************************************************************************) + (* Resource manager r spontaneously decides to abort. As noted above, r *) + (* does not send any message in our simplified spec. *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +RMRcvCommitMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to commit. *) + (*************************************************************************) + /\ [type |-> "Commit"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + /\ UNCHANGED <> + +RMRcvAbortMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the TM to abort. *) + (*************************************************************************) + /\ [type |-> "Abort"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> + +TPNext == + \/ TMCommit \/ TMAbort + \/ \E r \in RM : + TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r) + \/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r) +----------------------------------------------------------------------------- +(***************************************************************************) +(* The material below this point is not discussed in Video Lecture 6. It *) +(* will be explained in Video Lecture 8. *) +(***************************************************************************) + +TPSpec == TPInit /\ [][TPNext]_<> + (*************************************************************************) + (* The complete spec of the Two-Phase Commit protocol. *) + (*************************************************************************) + +THEOREM TPSpec => []TPTypeOK + (*************************************************************************) + (* This theorem asserts that the type-correctness predicate TPTypeOK is *) + (* an invariant of the specification. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now assert that the Two-Phase Commit protocol implements the *) +(* Transaction Commit protocol of module TCommit. The following statement *) +(* imports all the definitions from module TCommit into the current *) +(* module. *) +(***************************************************************************) +INSTANCE TCommit + +THEOREM TPSpec => TCSpec + (*************************************************************************) + (* This theorem asserts that the specification TPSpec of the Two-Phase *) + (* Commit protocol implements the specification TCSpec of the *) + (* Transaction Commit protocol. *) + (*************************************************************************) +(***************************************************************************) +(* The two theorems in this module have been checked with TLC for six *) +(* RMs, a configuration with 50816 reachable states, in a little over a *) +(* minute on a 1 GHz PC. *) +(***************************************************************************) + +============================================================================= +\* Modification History +\* Last modified Thu Dec 27 15:46:42 CET 2018 by veitheller +\* Created Thu Dec 27 15:46:21 CET 2018 by veitheller diff --git a/TwoPhase.toolbox/TwoPhase___Model_1.launch b/TwoPhase.toolbox/TwoPhase___Model_1.launch new file mode 100644 index 0000000..2e3e8c3 --- /dev/null +++ b/TwoPhase.toolbox/TwoPhase___Model_1.launch @@ -0,0 +1,48 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922765832.launch b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922765832.launch new file mode 100644 index 0000000..18d7099 --- /dev/null +++ b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922765832.launch @@ -0,0 +1,47 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922881813.launch b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922881813.launch new file mode 100644 index 0000000..574af93 --- /dev/null +++ b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922881813.launch @@ -0,0 +1,47 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922927774.launch b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922927774.launch new file mode 100644 index 0000000..e70277a --- /dev/null +++ b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922927774.launch @@ -0,0 +1,47 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545923020132.launch b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545923020132.launch new file mode 100644 index 0000000..f6cfe52 --- /dev/null +++ b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545923020132.launch @@ -0,0 +1,48 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Untitled.toolbox/.project b/Untitled.toolbox/.project new file mode 100644 index 0000000..b919234 --- /dev/null +++ b/Untitled.toolbox/.project @@ -0,0 +1,24 @@ + + + Untitled + + + + + + toolbox.builder.TLAParserBuilder + + + + + + toolbox.natures.TLANature + + + + SimpleProgram.tla + 1 + PARENT-1-PROJECT_LOC/SimpleProgram.tla + + + diff --git a/Untitled.toolbox/.settings/org.lamport.tla.toolbox.prefs b/Untitled.toolbox/.settings/org.lamport.tla.toolbox.prefs new file mode 100644 index 0000000..62403c1 --- /dev/null +++ b/Untitled.toolbox/.settings/org.lamport.tla.toolbox.prefs @@ -0,0 +1,2 @@ +ProjectRootFile=PARENT-1-PROJECT_LOC/SimpleProgram.tla +eclipse.preferences.version=1 diff --git a/Untitled.toolbox/Model_1/MC.cfg b/Untitled.toolbox/Model_1/MC.cfg new file mode 100644 index 0000000..903ef9b --- /dev/null +++ b/Untitled.toolbox/Model_1/MC.cfg @@ -0,0 +1,7 @@ +\* INIT definition +INIT +init_15454038741536000 +\* NEXT definition +NEXT +next_15454038741537000 +\* Generated on Fri Dec 21 15:51:14 CET 2018 \ No newline at end of file diff --git a/Untitled.toolbox/Model_1/MC.tla b/Untitled.toolbox/Model_1/MC.tla new file mode 100644 index 0000000..32b1e70 --- /dev/null +++ b/Untitled.toolbox/Model_1/MC.tla @@ -0,0 +1,14 @@ +---- MODULE MC ---- +EXTENDS SimpleProgram, TLC + +\* INIT definition @modelBehaviorInit:0 +init_15454038741536000 == +Init +---- +\* NEXT definition @modelBehaviorNext:0 +next_15454038741537000 == +Next +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 15:51:14 CET 2018 by veitheller diff --git a/Untitled.toolbox/Model_1/SimpleProgram.tla b/Untitled.toolbox/Model_1/SimpleProgram.tla new file mode 100644 index 0000000..b7db42b --- /dev/null +++ b/Untitled.toolbox/Model_1/SimpleProgram.tla @@ -0,0 +1,21 @@ +--------------------------- MODULE SimpleProgram --------------------------- + +EXTENDS Integers +VARIABLES i, pc + +Init == (pc = "start") /\ (i = 0) + +Pick == /\ pc = "start" + /\ i' \in 0..1000 + /\ pc' = "middle" + +Add1 == /\ pc = "middle" + /\ i' = i + 1 + /\ pc' = "done" + +Next == Pick \/ Add1 + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 15:46:32 CET 2018 by veitheller +\* Created Fri Dec 21 15:45:07 CET 2018 by veitheller diff --git a/Untitled.toolbox/Model_1_SnapShot_1545403778936/MC.cfg b/Untitled.toolbox/Model_1_SnapShot_1545403778936/MC.cfg new file mode 100644 index 0000000..671d938 --- /dev/null +++ b/Untitled.toolbox/Model_1_SnapShot_1545403778936/MC.cfg @@ -0,0 +1,7 @@ +\* INIT definition +INIT +init_15454037685082000 +\* NEXT definition +NEXT +next_15454037685093000 +\* Generated on Fri Dec 21 15:49:28 CET 2018 \ No newline at end of file diff --git a/Untitled.toolbox/Model_1_SnapShot_1545403778936/MC.tla b/Untitled.toolbox/Model_1_SnapShot_1545403778936/MC.tla new file mode 100644 index 0000000..5305397 --- /dev/null +++ b/Untitled.toolbox/Model_1_SnapShot_1545403778936/MC.tla @@ -0,0 +1,14 @@ +---- MODULE MC ---- +EXTENDS SimpleProgram, TLC + +\* INIT definition @modelBehaviorInit:0 +init_15454037685082000 == +Init +---- +\* NEXT definition @modelBehaviorNext:0 +next_15454037685093000 == +Next +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 15:49:28 CET 2018 by veitheller diff --git a/Untitled.toolbox/Model_1_SnapShot_1545403778936/SimpleProgram.tla b/Untitled.toolbox/Model_1_SnapShot_1545403778936/SimpleProgram.tla new file mode 100644 index 0000000..b7db42b --- /dev/null +++ b/Untitled.toolbox/Model_1_SnapShot_1545403778936/SimpleProgram.tla @@ -0,0 +1,21 @@ +--------------------------- MODULE SimpleProgram --------------------------- + +EXTENDS Integers +VARIABLES i, pc + +Init == (pc = "start") /\ (i = 0) + +Pick == /\ pc = "start" + /\ i' \in 0..1000 + /\ pc' = "middle" + +Add1 == /\ pc = "middle" + /\ i' = i + 1 + /\ pc' = "done" + +Next == Pick \/ Add1 + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 15:46:32 CET 2018 by veitheller +\* Created Fri Dec 21 15:45:07 CET 2018 by veitheller diff --git a/Untitled.toolbox/Model_1_SnapShot_1545403888272/MC.cfg b/Untitled.toolbox/Model_1_SnapShot_1545403888272/MC.cfg new file mode 100644 index 0000000..903ef9b --- /dev/null +++ b/Untitled.toolbox/Model_1_SnapShot_1545403888272/MC.cfg @@ -0,0 +1,7 @@ +\* INIT definition +INIT +init_15454038741536000 +\* NEXT definition +NEXT +next_15454038741537000 +\* Generated on Fri Dec 21 15:51:14 CET 2018 \ No newline at end of file diff --git a/Untitled.toolbox/Model_1_SnapShot_1545403888272/MC.tla b/Untitled.toolbox/Model_1_SnapShot_1545403888272/MC.tla new file mode 100644 index 0000000..32b1e70 --- /dev/null +++ b/Untitled.toolbox/Model_1_SnapShot_1545403888272/MC.tla @@ -0,0 +1,14 @@ +---- MODULE MC ---- +EXTENDS SimpleProgram, TLC + +\* INIT definition @modelBehaviorInit:0 +init_15454038741536000 == +Init +---- +\* NEXT definition @modelBehaviorNext:0 +next_15454038741537000 == +Next +---- +============================================================================= +\* Modification History +\* Created Fri Dec 21 15:51:14 CET 2018 by veitheller diff --git a/Untitled.toolbox/Model_1_SnapShot_1545403888272/SimpleProgram.tla b/Untitled.toolbox/Model_1_SnapShot_1545403888272/SimpleProgram.tla new file mode 100644 index 0000000..b7db42b --- /dev/null +++ b/Untitled.toolbox/Model_1_SnapShot_1545403888272/SimpleProgram.tla @@ -0,0 +1,21 @@ +--------------------------- MODULE SimpleProgram --------------------------- + +EXTENDS Integers +VARIABLES i, pc + +Init == (pc = "start") /\ (i = 0) + +Pick == /\ pc = "start" + /\ i' \in 0..1000 + /\ pc' = "middle" + +Add1 == /\ pc = "middle" + /\ i' = i + 1 + /\ pc' = "done" + +Next == Pick \/ Add1 + +============================================================================= +\* Modification History +\* Last modified Fri Dec 21 15:46:32 CET 2018 by veitheller +\* Created Fri Dec 21 15:45:07 CET 2018 by veitheller diff --git a/Untitled.toolbox/SimpleProgram.pdf b/Untitled.toolbox/SimpleProgram.pdf new file mode 100644 index 0000000..993e481 Binary files /dev/null and b/Untitled.toolbox/SimpleProgram.pdf differ diff --git a/Untitled.toolbox/SimpleProgram.tex b/Untitled.toolbox/SimpleProgram.tex new file mode 100644 index 0000000..c71ce72 --- /dev/null +++ b/Untitled.toolbox/SimpleProgram.tex @@ -0,0 +1,976 @@ +\batchmode %% Suppresses most terminal output. +\documentclass{article} +\usepackage{color} +\definecolor{boxshade}{gray}{0.85} +\setlength{\textwidth}{360pt} +\setlength{\textheight}{541pt} +\usepackage{latexsym} +\usepackage{ifthen} +% \usepackage{color} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% SWITCHES % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newboolean{shading} +\setboolean{shading}{false} +\makeatletter + %% this is needed only when inserted into the file, not when + %% used as a package file. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % +% DEFINITIONS OF SYMBOL-PRODUCING COMMANDS % +% % +% TLA+ LaTeX % +% symbol command % +% ------ ------- % +% => \implies % +% <: \ltcolon % +% :> \colongt % +% == \defeq % +% .. \dotdot % +% :: \coloncolon % +% =| \eqdash % +% ++ \pp % +% -- \mm % +% ** \stst % +% // \slsl % +% ^ \ct % +% \A \A % +% \E \E % +% \AA \AA % +% \EE \EE % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newlength{\symlength} +\newcommand{\implies}{\Rightarrow} +\newcommand{\ltcolon}{\mathrel{<\!\!\mbox{:}}} +\newcommand{\colongt}{\mathrel{\!\mbox{:}\!\!>}} +\newcommand{\defeq}{\;\mathrel{\smash %% keep this symbol from being too tall + {{\stackrel{\scriptscriptstyle\Delta}{=}}}}\;} +\newcommand{\dotdot}{\mathrel{\ldotp\ldotp}} +\newcommand{\coloncolon}{\mathrel{::\;}} +\newcommand{\eqdash}{\mathrel = \joinrel \hspace{-.28em}|} +\newcommand{\pp}{\mathbin{++}} +\newcommand{\mm}{\mathbin{--}} +\newcommand{\stst}{*\!*} +\newcommand{\slsl}{/\!/} +\newcommand{\ct}{\hat{\hspace{.4em}}} +\newcommand{\A}{\forall} +\newcommand{\E}{\exists} +\renewcommand{\AA}{\makebox{$\raisebox{.05em}{\makebox[0pt][l]{% + $\forall\hspace{-.517em}\forall\hspace{-.517em}\forall$}}% + \forall\hspace{-.517em}\forall \hspace{-.517em}\forall\,$}} +\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox[0pt][l]{% + $\exists\hspace{-.517em}\exists\hspace{-.517em}\exists$}}% + \exists\hspace{-.517em}\exists\hspace{-.517em}\exists\,$}} +\newcommand{\whileop}{\.{\stackrel + {\mbox{\raisebox{-.3em}[0pt][0pt]{$\scriptscriptstyle+\;\,$}}}% + {-\hspace{-.16em}\triangleright}}} + +% Commands are defined to produce the upper-case keywords. +% Note that some have space after them. +\newcommand{\ASSUME}{\textsc{assume }} +\newcommand{\ASSUMPTION}{\textsc{assumption }} +\newcommand{\AXIOM}{\textsc{axiom }} +\newcommand{\BOOLEAN}{\textsc{boolean }} +\newcommand{\CASE}{\textsc{case }} +\newcommand{\CONSTANT}{\textsc{constant }} +\newcommand{\CONSTANTS}{\textsc{constants }} +\newcommand{\ELSE}{\settowidth{\symlength}{\THEN}% + \makebox[\symlength][l]{\textsc{ else}}} +\newcommand{\EXCEPT}{\textsc{ except }} +\newcommand{\EXTENDS}{\textsc{extends }} +\newcommand{\FALSE}{\textsc{false}} +\newcommand{\IF}{\textsc{if }} +\newcommand{\IN}{\settowidth{\symlength}{\LET}% + \makebox[\symlength][l]{\textsc{in}}} +\newcommand{\INSTANCE}{\textsc{instance }} +\newcommand{\LET}{\textsc{let }} +\newcommand{\LOCAL}{\textsc{local }} +\newcommand{\MODULE}{\textsc{module }} +\newcommand{\OTHER}{\textsc{other }} +\newcommand{\STRING}{\textsc{string}} +\newcommand{\THEN}{\textsc{ then }} +\newcommand{\THEOREM}{\textsc{theorem }} +\newcommand{\LEMMA}{\textsc{lemma }} +\newcommand{\PROPOSITION}{\textsc{proposition }} +\newcommand{\COROLLARY}{\textsc{corollary }} +\newcommand{\TRUE}{\textsc{true}} +\newcommand{\VARIABLE}{\textsc{variable }} +\newcommand{\VARIABLES}{\textsc{variables }} +\newcommand{\WITH}{\textsc{ with }} +\newcommand{\WF}{\textrm{WF}} +\newcommand{\SF}{\textrm{SF}} +\newcommand{\CHOOSE}{\textsc{choose }} +\newcommand{\ENABLED}{\textsc{enabled }} +\newcommand{\UNCHANGED}{\textsc{unchanged }} +\newcommand{\SUBSET}{\textsc{subset }} +\newcommand{\UNION}{\textsc{union }} +\newcommand{\DOMAIN}{\textsc{domain }} +% Added for tla2tex +\newcommand{\BY}{\textsc{by }} +\newcommand{\OBVIOUS}{\textsc{obvious }} +\newcommand{\HAVE}{\textsc{have }} +\newcommand{\QED}{\textsc{qed }} +\newcommand{\TAKE}{\textsc{take }} +\newcommand{\DEF}{\textsc{ def }} +\newcommand{\HIDE}{\textsc{hide }} +\newcommand{\RECURSIVE}{\textsc{recursive }} +\newcommand{\USE}{\textsc{use }} +\newcommand{\DEFINE}{\textsc{define }} +\newcommand{\PROOF}{\textsc{proof }} +\newcommand{\WITNESS}{\textsc{witness }} +\newcommand{\PICK}{\textsc{pick }} +\newcommand{\DEFS}{\textsc{defs }} +\newcommand{\PROVE}{\settowidth{\symlength}{\ASSUME}% + \makebox[\symlength][l]{\textsc{prove}}\@s{-4.1}}% + %% The \@s{-4.1) is a kludge added on 24 Oct 2009 [happy birthday, Ellen] + %% so the correct alignment occurs if the user types + %% ASSUME X + %% PROVE Y + %% because it cancels the extra 4.1 pts added because of the + %% extra space after the PROVE. This seems to works OK. + %% However, the 4.1 equals Parameters.LaTeXLeftSpace(1) and + %% should be changed if that method ever changes. +\newcommand{\SUFFICES}{\textsc{suffices }} +\newcommand{\NEW}{\textsc{new }} +\newcommand{\LAMBDA}{\textsc{lambda }} +\newcommand{\STATE}{\textsc{state }} +\newcommand{\ACTION}{\textsc{action }} +\newcommand{\TEMPORAL}{\textsc{temporal }} +\newcommand{\ONLY}{\textsc{only }} %% added by LL on 2 Oct 2009 +\newcommand{\OMITTED}{\textsc{omitted }} %% added by LL on 31 Oct 2009 +\newcommand{\@pfstepnum}[2]{\ensuremath{\langle#1\rangle}\textrm{#2}} +\newcommand{\bang}{\@s{1}\mbox{\small !}\@s{1}} +%% We should format || differently in PlusCal code than in TLA+ formulas. +\newcommand{\p@barbar}{\ifpcalsymbols + \,\,\rule[-.25em]{.075em}{1em}\hspace*{.2em}\rule[-.25em]{.075em}{1em}\,\,% + \else \,||\,\fi} +%% PlusCal keywords +\newcommand{\p@fair}{\textbf{fair }} +\newcommand{\p@semicolon}{\textbf{\,; }} +\newcommand{\p@algorithm}{\textbf{algorithm }} +\newcommand{\p@mmfair}{\textbf{-{}-fair }} +\newcommand{\p@mmalgorithm}{\textbf{-{}-algorithm }} +\newcommand{\p@assert}{\textbf{assert }} +\newcommand{\p@await}{\textbf{await }} +\newcommand{\p@begin}{\textbf{begin }} +\newcommand{\p@end}{\textbf{end }} +\newcommand{\p@call}{\textbf{call }} +\newcommand{\p@define}{\textbf{define }} +\newcommand{\p@do}{\textbf{ do }} +\newcommand{\p@either}{\textbf{either }} +\newcommand{\p@or}{\textbf{or }} +\newcommand{\p@goto}{\textbf{goto }} +\newcommand{\p@if}{\textbf{if }} +\newcommand{\p@then}{\,\,\textbf{then }} +\newcommand{\p@else}{\ifcsyntax \textbf{else } \else \,\,\textbf{else }\fi} +\newcommand{\p@elsif}{\,\,\textbf{elsif }} +\newcommand{\p@macro}{\textbf{macro }} +\newcommand{\p@print}{\textbf{print }} +\newcommand{\p@procedure}{\textbf{procedure }} +\newcommand{\p@process}{\textbf{process }} +\newcommand{\p@return}{\textbf{return}} +\newcommand{\p@skip}{\textbf{skip}} +\newcommand{\p@variable}{\textbf{variable }} +\newcommand{\p@variables}{\textbf{variables }} +\newcommand{\p@while}{\textbf{while }} +\newcommand{\p@when}{\textbf{when }} +\newcommand{\p@with}{\textbf{with }} +\newcommand{\p@lparen}{\textbf{(\,\,}} +\newcommand{\p@rparen}{\textbf{\,\,) }} +\newcommand{\p@lbrace}{\textbf{\{\,\,}} +\newcommand{\p@rbrace}{\textbf{\,\,\} }} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% REDEFINE STANDARD COMMANDS TO MAKE THEM FORMAT BETTER % +% % +% We redefine \in and \notin % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\renewcommand{\_}{\rule{.4em}{.06em}\hspace{.05em}} +\newlength{\equalswidth} +\let\oldin=\in +\let\oldnotin=\notin +\renewcommand{\in}{% + {\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth][c]{$\oldin$}}} +\renewcommand{\notin}{% + {\settowidth{\equalswidth}{$\.{=}$}\makebox[\equalswidth]{$\oldnotin$}}} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % +% HORIZONTAL BARS: % +% % +% \moduleLeftDash |~~~~~~~~~~ % +% \moduleRightDash ~~~~~~~~~~| % +% \midbar |----------| % +% \bottombar |__________| % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newlength{\charwidth}\settowidth{\charwidth}{{\small\tt M}} +\newlength{\boxrulewd}\setlength{\boxrulewd}{.4pt} +\newlength{\boxlineht}\setlength{\boxlineht}{.5\baselineskip} +\newcommand{\boxsep}{\charwidth} +\newlength{\boxruleht}\setlength{\boxruleht}{.5ex} +\newlength{\boxruledp}\setlength{\boxruledp}{-\boxruleht} +\addtolength{\boxruledp}{\boxrulewd} +\newcommand{\boxrule}{\leaders\hrule height \boxruleht depth \boxruledp + \hfill\mbox{}} +\newcommand{\@computerule}{% + \setlength{\boxruleht}{.5ex}% + \setlength{\boxruledp}{-\boxruleht}% + \addtolength{\boxruledp}{\boxrulewd}} + +\newcommand{\bottombar}{\hspace{-\boxsep}% + \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd}{\boxlineht}}% + \boxrule + \raisebox{-\boxrulewd}[0pt][0pt]{% + \rule[.5ex]{\boxrulewd}{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}} + +\newcommand{\moduleLeftDash}% + {\hspace*{-\boxsep}% + \raisebox{-\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd + }{\boxlineht}}% + \boxrule\hspace*{.4em }} + +\newcommand{\moduleRightDash}% + {\hspace*{.4em}\boxrule + \raisebox{-\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd + }{\boxlineht}}\hspace{-\boxsep}}%\vspace{.2em} + +\newcommand{\midbar}{\hspace{-\boxsep}\raisebox{-.5\boxlineht}[0pt][0pt]{% + \rule[.5ex]{\boxrulewd}{\boxlineht}}\boxrule\raisebox{-.5\boxlineht% + }[0pt][0pt]{\rule[.5ex]{\boxrulewd}{\boxlineht}}\hspace{-\boxsep}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% FORMATING COMMANDS % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% PLUSCAL SHADING % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% The TeX pcalshading switch is set on to cause PlusCal shading to be +% performed. This changes the behavior of the following commands and +% environments to cause full-width shading to be performed on all lines. +% +% \tstrut \@x cpar mcom \@pvspace +% +% The TeX pcalsymbols switch is turned on when typesetting a PlusCal algorithm, +% whether or not shading is being performed. It causes symbols (other than +% parentheses and braces and PlusCal-only keywords) that should be typeset +% differently depending on whether they are in an algorithm to be typeset +% appropriately. Currently, the only such symbol is "||". +% +% The TeX csyntax switch is turned on when typesetting a PlusCal algorithm in +% c-syntax. This allows symbols to be format differently in the two syntaxes. +% The "else" keyword is the only one that is. + +\newif\ifpcalshading \pcalshadingfalse +\newif\ifpcalsymbols \pcalsymbolsfalse +\newif\ifcsyntax \csyntaxtrue + +% The \@pvspace command makes a vertical space. It uses \vspace +% except with \ifpcalshading, in which case it sets \pvcalvspace +% and the space is added by a following \@x command. +% +\newlength{\pcalvspace}\setlength{\pcalvspace}{0pt}% +\newcommand{\@pvspace}[1]{% + \ifpcalshading + \par\global\setlength{\pcalvspace}{#1}% + \else + \par\vspace{#1}% + \fi +} + +% The lcom environment was changed to set \lcomindent equal to +% the indentation it produces. This length is used by the +% cpar environment to make shading extend for the full width +% of the line. This assumes that lcom environments are not +% nested. I hope TLATeX does not nest them. +% +\newlength{\lcomindent}% +\setlength{\lcomindent}{0pt}% + +%\tstrut: A strut to produce inter-paragraph space in a comment. +%\rstrut: A strut to extend the bottom of a one-line comment so +% there's no break in the shading between comments on +% successive lines. +\newcommand\tstrut% + {\raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{1.15em}}}% + \global\setlength{\vshadelen}{0pt}} +\newcommand\rstrut{\raisebox{-.25em}{\rule{0pt}{1.15em}}% + \global\setlength{\vshadelen}{0pt}} + + +% \.{op} formats operator op in math mode with empty boxes on either side. +% Used because TeX otherwise vary the amount of space it leaves around op. +\renewcommand{\.}[1]{\ensuremath{\mbox{}#1\mbox{}}} + +% \@s{n} produces an n-point space +\newcommand{\@s}[1]{\hspace{#1pt}} + +% \@x{txt} starts a specification line in the beginning with txt +% in the final LaTeX source. +\newlength{\@xlen} +\newcommand\xtstrut% + {\setlength{\@xlen}{1.05em}% + \addtolength{\@xlen}{\pcalvspace}% + \raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{\@xlen}}}% + \global\setlength{\vshadelen}{0pt}% + \global\setlength{\pcalvspace}{0pt}} + +\newcommand{\@x}[1]{\par + \ifpcalshading + \makebox[0pt][l]{\shadebox{\xtstrut\hspace*{\textwidth}}}% + \fi + \mbox{$\mbox{}#1\mbox{}$}} + +% \@xx{txt} continues a specification line with the text txt. +\newcommand{\@xx}[1]{\mbox{$\mbox{}#1\mbox{}$}} + +% \@y{cmt} produces a one-line comment. +\newcommand{\@y}[1]{\mbox{\footnotesize\hspace{.65em}% + \ifthenelse{\boolean{shading}}{% + \shadebox{#1\hspace{-\the\lastskip}\rstrut}}% + {#1\hspace{-\the\lastskip}\rstrut}}} + +% \@z{cmt} produces a zero-width one-line comment. +\newcommand{\@z}[1]{\makebox[0pt][l]{\footnotesize + \ifthenelse{\boolean{shading}}{% + \shadebox{#1\hspace{-\the\lastskip}\rstrut}}% + {#1\hspace{-\the\lastskip}\rstrut}}} + + +% \@w{str} produces the TLA+ string "str". +\newcommand{\@w}[1]{\textsf{``{#1}''}} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% SHADING % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\def\graymargin{1} + % The number of points of margin in the shaded box. + +% \definecolor{boxshade}{gray}{.85} +% Defines the darkness of the shading: 1 = white, 0 = black +% Added by TLATeX only if needed. + +% \shadebox{txt} puts txt in a shaded box. +\newlength{\templena} +\newlength{\templenb} +\newsavebox{\tempboxa} +\newcommand{\shadebox}[1]{{\setlength{\fboxsep}{\graymargin pt}% + \savebox{\tempboxa}{#1}% + \settoheight{\templena}{\usebox{\tempboxa}}% + \settodepth{\templenb}{\usebox{\tempboxa}}% + \hspace*{-\fboxsep}\raisebox{0pt}[\templena][\templenb]% + {\colorbox{boxshade}{\usebox{\tempboxa}}}\hspace*{-\fboxsep}}} + +% \vshade{n} makes an n-point inter-paragraph space, with +% shading if the `shading' flag is true. +\newlength{\vshadelen} +\setlength{\vshadelen}{0pt} +\newcommand{\vshade}[1]{\ifthenelse{\boolean{shading}}% + {\global\setlength{\vshadelen}{#1pt}}% + {\vspace{#1pt}}} + +\newlength{\boxwidth} +\newlength{\multicommentdepth} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE cpar ENVIRONMENT % +% ^^^^^^^^^^^^^^^^^^^^ % +% The LaTeX input % +% % +% \begin{cpar}{pop}{nest}{isLabel}{d}{e}{arg6} % +% XXXXXXXXXXXXXXX % +% XXXXXXXXXXXXXXX % +% XXXXXXXXXXXXXXX % +% \end{cpar} % +% % +% produces one of two possible results. If isLabel is the letter "T", % +% it produces the following, where [label] is the result of typesetting % +% arg6 in an LR box, and d is is a number representing a distance in % +% points. % +% % +% prevailing |<-- d -->[label]<- e ->XXXXXXXXXXXXXXX % +% left | XXXXXXXXXXXXXXX % +% margin | XXXXXXXXXXXXXXX % +% % +% If isLabel is the letter "F", then it produces % +% % +% prevailing |<-- d -->XXXXXXXXXXXXXXXXXXXXXXX % +% left | <- e ->XXXXXXXXXXXXXXXX % +% margin | XXXXXXXXXXXXXXXX % +% % +% where d and e are numbers representing distances in points. % +% % +% The prevailing left margin is the one in effect before the most recent % +% pop (argument 1) cpar environments with "T" as the nest argument, where % +% pop is a number \geq 0. % +% % +% If the nest argument is the letter "T", then the prevailing left % +% margin is moved to the left of the second (and following) lines of % +% X's. Otherwise, the prevailing left margin is left unchanged. % +% % +% An \unnest{n} command moves the prevailing left margin to where it was % +% before the most recent n cpar environments with "T" as the nesting % +% argument. % +% % +% The environment leaves no vertical space above or below it, or between % +% its paragraphs. (TLATeX inserts the proper amount of vertical space.) % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcounter{pardepth} +\setcounter{pardepth}{0} + +% \setgmargin{txt} defines \gmarginN to be txt, where N is \roman{pardepth}. +% \thegmargin equals \gmarginN, where N is \roman{pardepth}. +\newcommand{\setgmargin}[1]{% + \expandafter\xdef\csname gmargin\roman{pardepth}\endcsname{#1}} +\newcommand{\thegmargin}{\csname gmargin\roman{pardepth}\endcsname} +\newcommand{\gmargin}{0pt} + +\newsavebox{\tempsbox} + +\newlength{\@cparht} +\newlength{\@cpardp} +\newenvironment{cpar}[6]{% + \addtocounter{pardepth}{-#1}% + \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}% + \begin{minipage}[t]{\linewidth}}{}% + \begin{list}{}{% + \edef\temp{\thegmargin} + \ifthenelse{\equal{#3}{T}}% + {\settowidth{\leftmargin}{\hspace{\temp}\footnotesize #6\hspace{#5pt}}% + \addtolength{\leftmargin}{#4pt}}% + {\setlength{\leftmargin}{#4pt}% + \addtolength{\leftmargin}{#5pt}% + \addtolength{\leftmargin}{\temp}% + \setlength{\itemindent}{-#5pt}}% + \ifthenelse{\equal{#2}{T}}{\addtocounter{pardepth}{1}% + \setgmargin{\the\leftmargin}}{}% + \setlength{\labelwidth}{0pt}% + \setlength{\labelsep}{0pt}% + \setlength{\itemindent}{-\leftmargin}% + \setlength{\topsep}{0pt}% + \setlength{\parsep}{0pt}% + \setlength{\partopsep}{0pt}% + \setlength{\parskip}{0pt}% + \setlength{\itemsep}{0pt} + \setlength{\itemindent}{#4pt}% + \addtolength{\itemindent}{-\leftmargin}}% + \ifthenelse{\equal{#3}{T}}% + {\item[\tstrut\footnotesize \hspace{\temp}{#6}\hspace{#5pt}] + }% + {\item[\tstrut\hspace{\temp}]% + }% + \footnotesize} + {\hspace{-\the\lastskip}\tstrut + \end{list}% + \ifthenelse{\boolean{shading}}% + {\end{minipage}% + \end{lrbox}% + \ifpcalshading + \setlength{\@cparht}{\ht\tempsbox}% + \setlength{\@cpardp}{\dp\tempsbox}% + \addtolength{\@cparht}{.15em}% + \addtolength{\@cpardp}{.2em}% + \addtolength{\@cparht}{\@cpardp}% + % I don't know what's going on here. I want to add a + % \pcalvspace high shaded line, but I don't know how to + % do it. A little trial and error shows that the following + % does a reasonable job approximating that, eliminating + % the line if \pcalvspace is small. + \addtolength{\@cparht}{\pcalvspace}% + \ifdim \pcalvspace > .8em + \addtolength{\pcalvspace}{-.2em}% + \hspace*{-\lcomindent}% + \shadebox{\rule{0pt}{\pcalvspace}\hspace*{\textwidth}}\par + \global\setlength{\pcalvspace}{0pt}% + \fi + \hspace*{-\lcomindent}% + \makebox[0pt][l]{\raisebox{-\@cpardp}[0pt][0pt]{% + \shadebox{\rule{0pt}{\@cparht}\hspace*{\textwidth}}}}% + \hspace*{\lcomindent}\usebox{\tempsbox}% + \par + \else + \shadebox{\usebox{\tempsbox}}\par + \fi}% + {}% + } + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE ppar ENVIRONMENT % +% ^^^^^^^^^^^^^^^^^^^^ % +% The environment % +% % +% \begin{ppar} ... \end{ppar} % +% % +% is equivalent to % +% % +% \begin{cpar}{0}{F}{F}{0}{0}{} ... \end{cpar} % +% % +% The environment is put around each line of the output for a PlusCal % +% algorithm. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%\newenvironment{ppar}{% +% \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}% +% \begin{minipage}[t]{\linewidth}}{}% +% \begin{list}{}{% +% \edef\temp{\thegmargin} +% \setlength{\leftmargin}{0pt}% +% \addtolength{\leftmargin}{\temp}% +% \setlength{\itemindent}{0pt}% +% \setlength{\labelwidth}{0pt}% +% \setlength{\labelsep}{0pt}% +% \setlength{\itemindent}{-\leftmargin}% +% \setlength{\topsep}{0pt}% +% \setlength{\parsep}{0pt}% +% \setlength{\partopsep}{0pt}% +% \setlength{\parskip}{0pt}% +% \setlength{\itemsep}{0pt} +% \setlength{\itemindent}{0pt}% +% \addtolength{\itemindent}{-\leftmargin}}% +% \item[\tstrut\hspace{\temp}]}% +% {\hspace{-\the\lastskip}\tstrut +% \end{list}% +% \ifthenelse{\boolean{shading}}{\end{minipage} +% \end{lrbox}% +% \shadebox{\usebox{\tempsbox}}\par}{}% +% } + + %%% TESTING + \newcommand{\xtest}[1]{\par + \makebox[0pt][l]{\shadebox{\xtstrut\hspace*{\textwidth}}}% + \mbox{$\mbox{}#1\mbox{}$}} + +% \newcommand{\xxtest}[1]{\par +% \makebox[0pt][l]{\shadebox{\xtstrut{#1}\hspace*{\textwidth}}}% +% \mbox{$\mbox{}#1\mbox{}$}} + +%\newlength{\pcalvspace} +%\setlength{\pcalvspace}{0pt} +% \newlength{\xxtestlen} +% \setlength{\xxtestlen}{0pt} +% \newcommand\xtstrut% +% {\setlength{\xxtestlen}{1.15em}% +% \addtolength{\xxtestlen}{\pcalvspace}% +% \raisebox{\vshadelen}{\raisebox{-.25em}{\rule{0pt}{\xxtestlen}}}% +% \global\setlength{\vshadelen}{0pt}% +% \global\setlength{\pcalvspace}{0pt}} + + %%%% TESTING + + %% The xcpar environment + %% Note: overloaded use of \pcalvspace for testing. + %% +% \newlength{\xcparht}% +% \newlength{\xcpardp}% + +% \newenvironment{xcpar}[6]{% +% \addtocounter{pardepth}{-#1}% +% \ifthenelse{\boolean{shading}}{\par\begin{lrbox}{\tempsbox}% +% \begin{minipage}[t]{\linewidth}}{}% +% \begin{list}{}{% +% \edef\temp{\thegmargin}% +% \ifthenelse{\equal{#3}{T}}% +% {\settowidth{\leftmargin}{\hspace{\temp}\footnotesize #6\hspace{#5pt}}% +% \addtolength{\leftmargin}{#4pt}}% +% {\setlength{\leftmargin}{#4pt}% +% \addtolength{\leftmargin}{#5pt}% +% \addtolength{\leftmargin}{\temp}% +% \setlength{\itemindent}{-#5pt}}% +% \ifthenelse{\equal{#2}{T}}{\addtocounter{pardepth}{1}% +% \setgmargin{\the\leftmargin}}{}% +% \setlength{\labelwidth}{0pt}% +% \setlength{\labelsep}{0pt}% +% \setlength{\itemindent}{-\leftmargin}% +% \setlength{\topsep}{0pt}% +% \setlength{\parsep}{0pt}% +% \setlength{\partopsep}{0pt}% +% \setlength{\parskip}{0pt}% +% \setlength{\itemsep}{0pt}% +% \setlength{\itemindent}{#4pt}% +% \addtolength{\itemindent}{-\leftmargin}}% +% \ifthenelse{\equal{#3}{T}}% +% {\item[\xtstrut\footnotesize \hspace{\temp}{#6}\hspace{#5pt}]% +% }% +% {\item[\xtstrut\hspace{\temp}]% +% }% +% \footnotesize} +% {\hspace{-\the\lastskip}\tstrut +% \end{list}% +% \ifthenelse{\boolean{shading}}{\end{minipage} +% \end{lrbox}% +% \setlength{\xcparht}{\ht\tempsbox}% +% \setlength{\xcpardp}{\dp\tempsbox}% +% \addtolength{\xcparht}{.15em}% +% \addtolength{\xcpardp}{.2em}% +% \addtolength{\xcparht}{\xcpardp}% +% \hspace*{-\lcomindent}% +% \makebox[0pt][l]{\raisebox{-\xcpardp}[0pt][0pt]{% +% \shadebox{\rule{0pt}{\xcparht}\hspace*{\textwidth}}}}% +% \hspace*{\lcomindent}\usebox{\tempsbox}% +% \par}{}% +% } +% +% \newlength{\xmcomlen} +%\newenvironment{xmcom}[1]{% +% \setcounter{pardepth}{0}% +% \hspace{.65em}% +% \begin{lrbox}{\alignbox}\sloppypar% +% \setboolean{shading}{false}% +% \setlength{\boxwidth}{#1pt}% +% \addtolength{\boxwidth}{-.65em}% +% \begin{minipage}[t]{\boxwidth}\footnotesize +% \parskip=0pt\relax}% +% {\end{minipage}\end{lrbox}% +% \setlength{\xmcomlen}{\textwidth}% +% \addtolength{\xmcomlen}{-\wd\alignbox}% +% \settodepth{\alignwidth}{\usebox{\alignbox}}% +% \global\setlength{\multicommentdepth}{\alignwidth}% +% \setlength{\boxwidth}{\alignwidth}% +% \global\addtolength{\alignwidth}{-\maxdepth}% +% \addtolength{\boxwidth}{.1em}% +% \raisebox{0pt}[0pt][0pt]{% +% \ifthenelse{\boolean{shading}}% +% {\hspace*{-\xmcomlen}\shadebox{\rule[-\boxwidth]{0pt}{0pt}% +% \hspace*{\xmcomlen}\usebox{\alignbox}}}% +% {\usebox{\alignbox}}}% +% \vspace*{\alignwidth}\pagebreak[0]\vspace{-\alignwidth}\par} +% % a multi-line comment, whose first argument is its width in points. +% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE lcom ENVIRONMENT % +% ^^^^^^^^^^^^^^^^^^^^ % +% A multi-line comment with no text to its left is typeset in an lcom % +% environment, whose argument is a number representing the indentation % +% of the left margin, in points. All the text of the comment should be % +% inside cpar environments. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newenvironment{lcom}[1]{% + \setlength{\lcomindent}{#1pt} % Added for PlusCal handling. + \par\vspace{.2em}% + \sloppypar + \setcounter{pardepth}{0}% + \footnotesize + \begin{list}{}{% + \setlength{\leftmargin}{#1pt} + \setlength{\labelwidth}{0pt}% + \setlength{\labelsep}{0pt}% + \setlength{\itemindent}{0pt}% + \setlength{\topsep}{0pt}% + \setlength{\parsep}{0pt}% + \setlength{\partopsep}{0pt}% + \setlength{\parskip}{0pt}} + \item[]}% + {\end{list}\vspace{.3em}\setlength{\lcomindent}{0pt}% + } + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE mcom ENVIRONMENT AND \mutivspace COMMAND % +% ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ % +% % +% A part of the spec containing a right-comment of the form % +% % +% xxxx (*************) % +% yyyy (* ccccccccc *) % +% ... (* ccccccccc *) % +% (* ccccccccc *) % +% (* ccccccccc *) % +% (*************) % +% % +% is typeset by % +% % +% XXXX \begin{mcom}{d} % +% CCCC ... CCC % +% \end{mcom} % +% YYYY ... % +% \multivspace{n} % +% % +% where the number d is the width in points of the comment, n is the % +% number of xxxx, yyyy, ... lines to the left of the comment. % +% All the text of the comment should be typeset in cpar environments. % +% % +% This puts the comment into a single box (so no page breaks can occur % +% within it). The entire box is shaded iff the shading flag is true. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newlength{\xmcomlen}% +\newenvironment{mcom}[1]{% + \setcounter{pardepth}{0}% + \hspace{.65em}% + \begin{lrbox}{\alignbox}\sloppypar% + \setboolean{shading}{false}% + \setlength{\boxwidth}{#1pt}% + \addtolength{\boxwidth}{-.65em}% + \begin{minipage}[t]{\boxwidth}\footnotesize + \parskip=0pt\relax}% + {\end{minipage}\end{lrbox}% + \setlength{\xmcomlen}{\textwidth}% % For PlusCal shading + \addtolength{\xmcomlen}{-\wd\alignbox}% % For PlusCal shading + \settodepth{\alignwidth}{\usebox{\alignbox}}% + \global\setlength{\multicommentdepth}{\alignwidth}% + \setlength{\boxwidth}{\alignwidth}% % For PlusCal shading + \global\addtolength{\alignwidth}{-\maxdepth}% + \addtolength{\boxwidth}{.1em}% % For PlusCal shading + \raisebox{0pt}[0pt][0pt]{% + \ifthenelse{\boolean{shading}}% + {\ifpcalshading + \hspace*{-\xmcomlen}% + \shadebox{\rule[-\boxwidth]{0pt}{0pt}\hspace*{\xmcomlen}% + \usebox{\alignbox}}% + \else + \shadebox{\usebox{\alignbox}} + \fi + }% + {\usebox{\alignbox}}}% + \vspace*{\alignwidth}\pagebreak[0]\vspace{-\alignwidth}\par} + % a multi-line comment, whose first argument is its width in points. + + +% \multispace{n} produces the vertical space indicated by "|"s in +% this situation +% +% xxxx (*************) +% xxxx (* ccccccccc *) +% | (* ccccccccc *) +% | (* ccccccccc *) +% | (* ccccccccc *) +% | (*************) +% +% where n is the number of "xxxx" lines. +\newcommand{\multivspace}[1]{\addtolength{\multicommentdepth}{-#1\baselineskip}% + \addtolength{\multicommentdepth}{1.2em}% + \ifthenelse{\lengthtest{\multicommentdepth > 0pt}}% + {\par\vspace{\multicommentdepth}\par}{}} + +%\newenvironment{hpar}[2]{% +% \begin{list}{}{\setlength{\leftmargin}{#1pt}% +% \addtolength{\leftmargin}{#2pt}% +% \setlength{\itemindent}{-#2pt}% +% \setlength{\topsep}{0pt}% +% \setlength{\parsep}{0pt}% +% \setlength{\partopsep}{0pt}% +% \setlength{\parskip}{0pt}% +% \addtolength{\labelsep}{0pt}}% +% \item[]\footnotesize}{\end{list}} +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % Typesets a sequence of paragraphs like this: % +% % % +% % left |<-- d1 --> XXXXXXXXXXXXXXXXXXXXXXXX % +% % margin | <- d2 -> XXXXXXXXXXXXXXX % +% % | XXXXXXXXXXXXXXX % +% % | % +% % | XXXXXXXXXXXXXXX % +% % | XXXXXXXXXXXXXXX % +% % % +% % where d1 = #1pt and d2 = #2pt, but with no vspace between % +% % paragraphs. % +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Commands for repeated characters that produce dashes. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% \raisedDash{wd}{ht}{thk} makes a horizontal line wd characters wide, +% raised a distance ht ex's above the baseline, with a thickness of +% thk em's. +\newcommand{\raisedDash}[3]{\raisebox{#2ex}{\setlength{\alignwidth}{.5em}% + \rule{#1\alignwidth}{#3em}}} + +% The following commands take a single argument n and produce the +% output for n repeated characters, as follows +% \cdash: - +% \tdash: ~ +% \ceqdash: = +% \usdash: _ +\newcommand{\cdash}[1]{\raisedDash{#1}{.5}{.04}} +\newcommand{\usdash}[1]{\raisedDash{#1}{0}{.04}} +\newcommand{\ceqdash}[1]{\raisedDash{#1}{.5}{.08}} +\newcommand{\tdash}[1]{\raisedDash{#1}{1}{.08}} + +\newlength{\spacewidth} +\setlength{\spacewidth}{.2em} +\newcommand{\e}[1]{\hspace{#1\spacewidth}} +%% \e{i} produces space corresponding to i input spaces. + + +%% Alignment-file Commands + +\newlength{\alignboxwidth} +\newlength{\alignwidth} +\newsavebox{\alignbox} + +% \al{i}{j}{txt} is used in the alignment file to put "%{i}{j}{wd}" +% in the log file, where wd is the width of the line up to that point, +% and txt is the following text. +\newcommand{\al}[3]{% + \typeout{\%{#1}{#2}{\the\alignwidth}}% + \cl{#3}} + +%% \cl{txt} continues a specification line in the alignment file +%% with text txt. +\newcommand{\cl}[1]{% + \savebox{\alignbox}{\mbox{$\mbox{}#1\mbox{}$}}% + \settowidth{\alignboxwidth}{\usebox{\alignbox}}% + \addtolength{\alignwidth}{\alignboxwidth}% + \usebox{\alignbox}} + +% \fl{txt} in the alignment file begins a specification line that +% starts with the text txt. +\newcommand{\fl}[1]{% + \par + \savebox{\alignbox}{\mbox{$\mbox{}#1\mbox{}$}}% + \settowidth{\alignwidth}{\usebox{\alignbox}}% + \usebox{\alignbox}} + + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Ordinarily, TeX typesets letters in math mode in a special math italic % +% font. This makes it typeset "it" to look like the product of the % +% variables i and t, rather than like the word "it". The following % +% commands tell TeX to use an ordinary italic font instead. % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\ifx\documentclass\undefined +\else + \DeclareSymbolFont{tlaitalics}{\encodingdefault}{cmr}{m}{it} + \let\itfam\symtlaitalics +\fi + +\makeatletter +\newcommand{\tlx@c}{\c@tlx@ctr\advance\c@tlx@ctr\@ne} +\newcounter{tlx@ctr} +\c@tlx@ctr=\itfam \multiply\c@tlx@ctr"100\relax \advance\c@tlx@ctr "7061\relax +\mathcode`a=\tlx@c \mathcode`b=\tlx@c \mathcode`c=\tlx@c \mathcode`d=\tlx@c +\mathcode`e=\tlx@c \mathcode`f=\tlx@c \mathcode`g=\tlx@c \mathcode`h=\tlx@c +\mathcode`i=\tlx@c \mathcode`j=\tlx@c \mathcode`k=\tlx@c \mathcode`l=\tlx@c +\mathcode`m=\tlx@c \mathcode`n=\tlx@c \mathcode`o=\tlx@c \mathcode`p=\tlx@c +\mathcode`q=\tlx@c \mathcode`r=\tlx@c \mathcode`s=\tlx@c \mathcode`t=\tlx@c +\mathcode`u=\tlx@c \mathcode`v=\tlx@c \mathcode`w=\tlx@c \mathcode`x=\tlx@c +\mathcode`y=\tlx@c \mathcode`z=\tlx@c +\c@tlx@ctr=\itfam \multiply\c@tlx@ctr"100\relax \advance\c@tlx@ctr "7041\relax +\mathcode`A=\tlx@c \mathcode`B=\tlx@c \mathcode`C=\tlx@c \mathcode`D=\tlx@c +\mathcode`E=\tlx@c \mathcode`F=\tlx@c \mathcode`G=\tlx@c \mathcode`H=\tlx@c +\mathcode`I=\tlx@c \mathcode`J=\tlx@c \mathcode`K=\tlx@c \mathcode`L=\tlx@c +\mathcode`M=\tlx@c \mathcode`N=\tlx@c \mathcode`O=\tlx@c \mathcode`P=\tlx@c +\mathcode`Q=\tlx@c \mathcode`R=\tlx@c \mathcode`S=\tlx@c \mathcode`T=\tlx@c +\mathcode`U=\tlx@c \mathcode`V=\tlx@c \mathcode`W=\tlx@c \mathcode`X=\tlx@c +\mathcode`Y=\tlx@c \mathcode`Z=\tlx@c +\makeatother + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% THE describe ENVIRONMENT % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% +% It is like the description environment except it takes an argument +% ARG that should be the text of the widest label. It adjusts the +% indentation so each item with label LABEL produces +%% LABEL blah blah blah +%% <- width of ARG ->blah blah blah +%% blah blah blah +\newenvironment{describe}[1]% + {\begin{list}{}{\settowidth{\labelwidth}{#1}% + \setlength{\labelsep}{.5em}% + \setlength{\leftmargin}{\labelwidth}% + \addtolength{\leftmargin}{\labelsep}% + \addtolength{\leftmargin}{\parindent}% + \def\makelabel##1{\rm ##1\hfill}}% + \setlength{\topsep}{0pt}}%% + % Sets \topsep to 0 to reduce vertical space above + % and below embedded displayed equations + {\end{list}} + +% For tlatex.TeX +\usepackage{verbatim} +\makeatletter +\def\tla{\let\%\relax% + \@bsphack + \typeout{\%{\the\linewidth}}% + \let\do\@makeother\dospecials\catcode`\^^M\active + \let\verbatim@startline\relax + \let\verbatim@addtoline\@gobble + \let\verbatim@processline\relax + \let\verbatim@finish\relax + \verbatim@} +\let\endtla=\@esphack + +\let\pcal=\tla +\let\endpcal=\endtla +\let\ppcal=\tla +\let\endppcal=\endtla + +% The tlatex environment is used by TLATeX.TeX to typeset TLA+. +% TLATeX.TLA starts its files by writing a \tlatex command. This +% command/environment sets \parindent to 0 and defines \% to its +% standard definition because the writing of the log files is messed up +% if \% is defined to be something else. It also executes +% \@computerule to determine the dimensions for the TLA horizonatl +% bars. +\newenvironment{tlatex}{\@computerule% + \setlength{\parindent}{0pt}% + \makeatletter\chardef\%=`\%}{} + + +% The notla environment produces no output. You can turn a +% tla environment to a notla environment to prevent tlatex.TeX from +% re-formatting the environment. + +\def\notla{\let\%\relax% + \@bsphack + \let\do\@makeother\dospecials\catcode`\^^M\active + \let\verbatim@startline\relax + \let\verbatim@addtoline\@gobble + \let\verbatim@processline\relax + \let\verbatim@finish\relax + \verbatim@} +\let\endnotla=\@esphack + +\let\nopcal=\notla +\let\endnopcal=\endnotla +\let\noppcal=\notla +\let\endnoppcal=\endnotla + +%%%%%%%%%%%%%%%%%%%%%%%% end of tlatex.sty file %%%%%%%%%%%%%%%%%%%%%%% +% last modified on Fri 3 August 2012 at 14:23:49 PST by lamport + +\begin{document} +\tlatex +\setboolean{shading}{true} +\@x{}\moduleLeftDash\@xx{ {\MODULE} SimpleProgram}\moduleRightDash\@xx{}% +\@pvspace{8.0pt}% +\@x{ {\EXTENDS} Integers}% +\@x{ {\VARIABLES} i ,\, pc}% +\@pvspace{8.0pt}% +\@x{ Init\@s{6.36} \.{\defeq} ( pc \.{=}\@w{start} ) \.{\land} ( i \.{=} 0 )}% +\@pvspace{8.0pt}% +\@x{ Pick\@s{3.05} \.{\defeq} \.{\land} pc \.{=}\@w{start}}% +\@x{\@s{42.06} \.{\land} i \.{'}\@s{2.87} \.{\in} 0 \.{\dotdot} 1000}% +\@x{\@s{42.06} \.{\land} pc \.{'} \.{=}\@w{middle}}% +\@pvspace{8.0pt}% +\@x{ Add1 \.{\defeq} \.{\land} pc \.{=}\@w{middle}}% +\@x{\@s{42.06} \.{\land} i \.{'}\@s{2.87} \.{=} i \.{+} 1}% +\@x{\@s{42.06} \.{\land} pc \.{'} \.{=}\@w{done}}% +\@pvspace{8.0pt}% +\@x{ Next\@s{2.23} \.{\defeq} Pick \.{\lor} Add1}% +\@pvspace{8.0pt}% +\@x{}\bottombar\@xx{}% +\setboolean{shading}{false} +\begin{lcom}{0}% +\begin{cpar}{0}{F}{F}{0}{0}{}% +\ensuremath{\.{\,\backslash\,}}* Modification History +\end{cpar}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + \ensuremath{\.{\,\backslash\,}}* Last modified \ensuremath{Fri} + \ensuremath{Dec} 21 15:46:32 \ensuremath{CET} 2018 by \ensuremath{veitheller +}% +\end{cpar}% +\begin{cpar}{0}{F}{F}{0}{0}{}% + \ensuremath{\.{\,\backslash\,}}* Created \ensuremath{Fri} \ensuremath{Dec} 21 + 15:45:07 \ensuremath{CET} 2018 by \ensuremath{veitheller +}% +\end{cpar}% +\end{lcom}% +\end{document} diff --git a/Untitled.toolbox/Untitled___Model_1.launch b/Untitled.toolbox/Untitled___Model_1.launch new file mode 100644 index 0000000..4d582e0 --- /dev/null +++ b/Untitled.toolbox/Untitled___Model_1.launch @@ -0,0 +1,43 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403778936.launch b/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403778936.launch new file mode 100644 index 0000000..90ea0d2 --- /dev/null +++ b/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403778936.launch @@ -0,0 +1,8 @@ + + + + + + + + diff --git a/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403888272.launch b/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403888272.launch new file mode 100644 index 0000000..c742cc6 --- /dev/null +++ b/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403888272.launch @@ -0,0 +1,43 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +