diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e097dbf --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +*.toolbox/ diff --git a/DieHard.toolbox/.project b/DieHard.toolbox/.project deleted file mode 100644 index 9e00a41..0000000 --- a/DieHard.toolbox/.project +++ /dev/null @@ -1,24 +0,0 @@ - - - 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 deleted file mode 100644 index f80647d..0000000 --- a/DieHard.toolbox/.settings/org.lamport.tla.toolbox.prefs +++ /dev/null @@ -1,2 +0,0 @@ -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 deleted file mode 100644 index b2f6597..0000000 --- a/DieHard.toolbox/DieHard___Model_1.launch +++ /dev/null @@ -1,46 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406431357.launch b/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406431357.launch deleted file mode 100644 index fccdd07..0000000 --- a/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406431357.launch +++ /dev/null @@ -1,43 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406506746.launch b/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406506746.launch deleted file mode 100644 index 6906605..0000000 --- a/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406506746.launch +++ /dev/null @@ -1,45 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406592577.launch b/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406592577.launch deleted file mode 100644 index 38e2b4b..0000000 --- a/DieHard.toolbox/DieHard___Model_1_SnapShot_1545406592577.launch +++ /dev/null @@ -1,46 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/DieHard.toolbox/Model_1/DieHard.tla b/DieHard.toolbox/Model_1/DieHard.tla deleted file mode 100644 index a2e2c9c..0000000 --- a/DieHard.toolbox/Model_1/DieHard.tla +++ /dev/null @@ -1,46 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 4259c62..0000000 --- a/DieHard.toolbox/Model_1/MC.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index a791433..0000000 --- a/DieHard.toolbox/Model_1/MC.tla +++ /dev/null @@ -1,22 +0,0 @@ ----- 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 deleted file mode 100644 index a2e2c9c..0000000 --- a/DieHard.toolbox/Model_1_SnapShot_1545406431357/DieHard.tla +++ /dev/null @@ -1,46 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index e3f8031..0000000 --- a/DieHard.toolbox/Model_1_SnapShot_1545406431357/MC.cfg +++ /dev/null @@ -1,7 +0,0 @@ -\* 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 deleted file mode 100644 index f82c8f8..0000000 --- a/DieHard.toolbox/Model_1_SnapShot_1545406431357/MC.tla +++ /dev/null @@ -1,14 +0,0 @@ ----- 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 deleted file mode 100644 index a2e2c9c..0000000 --- a/DieHard.toolbox/Model_1_SnapShot_1545406506746/DieHard.tla +++ /dev/null @@ -1,46 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 4bfc4e8..0000000 --- a/DieHard.toolbox/Model_1_SnapShot_1545406506746/MC.cfg +++ /dev/null @@ -1,10 +0,0 @@ -\* 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 deleted file mode 100644 index 38304f3..0000000 --- a/DieHard.toolbox/Model_1_SnapShot_1545406506746/MC.tla +++ /dev/null @@ -1,18 +0,0 @@ ----- 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 deleted file mode 100644 index a2e2c9c..0000000 --- a/DieHard.toolbox/Model_1_SnapShot_1545406592577/DieHard.tla +++ /dev/null @@ -1,46 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 4259c62..0000000 --- a/DieHard.toolbox/Model_1_SnapShot_1545406592577/MC.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index a791433..0000000 --- a/DieHard.toolbox/Model_1_SnapShot_1545406592577/MC.tla +++ /dev/null @@ -1,22 +0,0 @@ ----- 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/TCommit.toolbox/.project b/TCommit.toolbox/.project deleted file mode 100644 index c3a7cdd..0000000 --- a/TCommit.toolbox/.project +++ /dev/null @@ -1,24 +0,0 @@ - - - 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 deleted file mode 100644 index cc1d253..0000000 --- a/TCommit.toolbox/.settings/org.lamport.tla.toolbox.prefs +++ /dev/null @@ -1,2 +0,0 @@ -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 deleted file mode 100644 index b6e7eae..0000000 --- a/TCommit.toolbox/Model_1/MC.cfg +++ /dev/null @@ -1,14 +0,0 @@ -\* 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 deleted file mode 100644 index c09bec9..0000000 --- a/TCommit.toolbox/Model_1/MC.tla +++ /dev/null @@ -1,27 +0,0 @@ ----- 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 deleted file mode 100644 index 86364e1..0000000 --- a/TCommit.toolbox/Model_1/TCommit.tla +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 13c6793..0000000 --- a/TCommit.toolbox/Model_1_SnapShot_1545410479536/MC.cfg +++ /dev/null @@ -1,13 +0,0 @@ -\* 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 deleted file mode 100644 index 4de6902..0000000 --- a/TCommit.toolbox/Model_1_SnapShot_1545410479536/MC.tla +++ /dev/null @@ -1,23 +0,0 @@ ----- 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 deleted file mode 100644 index 86364e1..0000000 --- a/TCommit.toolbox/Model_1_SnapShot_1545410479536/TCommit.tla +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index f7789bf..0000000 --- a/TCommit.toolbox/Model_1_SnapShot_1545410497334/MC.cfg +++ /dev/null @@ -1,13 +0,0 @@ -\* 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 deleted file mode 100644 index d5bcceb..0000000 --- a/TCommit.toolbox/Model_1_SnapShot_1545410497334/MC.tla +++ /dev/null @@ -1,23 +0,0 @@ ----- 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 deleted file mode 100644 index 86364e1..0000000 --- a/TCommit.toolbox/Model_1_SnapShot_1545410497334/TCommit.tla +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index b6e7eae..0000000 --- a/TCommit.toolbox/Model_1_SnapShot_1545410597019/MC.cfg +++ /dev/null @@ -1,14 +0,0 @@ -\* 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 deleted file mode 100644 index c09bec9..0000000 --- a/TCommit.toolbox/Model_1_SnapShot_1545410597019/MC.tla +++ /dev/null @@ -1,27 +0,0 @@ ----- 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 deleted file mode 100644 index 86364e1..0000000 --- a/TCommit.toolbox/Model_1_SnapShot_1545410597019/TCommit.tla +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index aad8983..0000000 Binary files a/TCommit.toolbox/TCommit.pdf and /dev/null differ diff --git a/TCommit.toolbox/TCommit.tex b/TCommit.toolbox/TCommit.tex deleted file mode 100644 index 21d3ae1..0000000 --- a/TCommit.toolbox/TCommit.tex +++ /dev/null @@ -1,1082 +0,0 @@ -\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 deleted file mode 100644 index 1a8db62..0000000 --- a/TCommit.toolbox/TCommit___Model_1.launch +++ /dev/null @@ -1,48 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410479536.launch b/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410479536.launch deleted file mode 100644 index 700b4d7..0000000 --- a/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410479536.launch +++ /dev/null @@ -1,47 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410497334.launch b/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410497334.launch deleted file mode 100644 index f7e01b5..0000000 --- a/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410497334.launch +++ /dev/null @@ -1,47 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410597019.launch b/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410597019.launch deleted file mode 100644 index db2aec6..0000000 --- a/TCommit.toolbox/TCommit___Model_1_SnapShot_1545410597019.launch +++ /dev/null @@ -1,48 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/TwoPhase.toolbox/.project b/TwoPhase.toolbox/.project deleted file mode 100644 index bdb139b..0000000 --- a/TwoPhase.toolbox/.project +++ /dev/null @@ -1,29 +0,0 @@ - - - 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 deleted file mode 100644 index 31b2e59..0000000 --- a/TwoPhase.toolbox/.settings/org.lamport.tla.toolbox.prefs +++ /dev/null @@ -1,2 +0,0 @@ -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 deleted file mode 100644 index b750119..0000000 --- a/TwoPhase.toolbox/Model_1/MC.cfg +++ /dev/null @@ -1,21 +0,0 @@ -\* 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 deleted file mode 100644 index 150e7b1..0000000 --- a/TwoPhase.toolbox/Model_1/MC.tla +++ /dev/null @@ -1,37 +0,0 @@ ----- 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 deleted file mode 100644 index 86364e1..0000000 --- a/TwoPhase.toolbox/Model_1/TCommit.tla +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 87617e6..0000000 --- a/TwoPhase.toolbox/Model_1/TwoPhase.tla +++ /dev/null @@ -1,182 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 8c379b1..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/MC.cfg +++ /dev/null @@ -1,13 +0,0 @@ -\* 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 deleted file mode 100644 index 22fce1f..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/MC.tla +++ /dev/null @@ -1,23 +0,0 @@ ----- 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 deleted file mode 100644 index 86364e1..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/TCommit.tla +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 87617e6..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922765832/TwoPhase.tla +++ /dev/null @@ -1,182 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index f0cd133..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/MC.cfg +++ /dev/null @@ -1,13 +0,0 @@ -\* 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 deleted file mode 100644 index 5c504ea..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/MC.tla +++ /dev/null @@ -1,23 +0,0 @@ ----- 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 deleted file mode 100644 index 86364e1..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/TCommit.tla +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 87617e6..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922881813/TwoPhase.tla +++ /dev/null @@ -1,182 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 5f1cfb2..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/MC.cfg +++ /dev/null @@ -1,20 +0,0 @@ -\* 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 deleted file mode 100644 index 64572bf..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/MC.tla +++ /dev/null @@ -1,33 +0,0 @@ ----- 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 deleted file mode 100644 index 86364e1..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/TCommit.tla +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 87617e6..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545922927774/TwoPhase.tla +++ /dev/null @@ -1,182 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index b750119..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/MC.cfg +++ /dev/null @@ -1,21 +0,0 @@ -\* 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 deleted file mode 100644 index 150e7b1..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/MC.tla +++ /dev/null @@ -1,37 +0,0 @@ ----- 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 deleted file mode 100644 index 86364e1..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/TCommit.tla +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 87617e6..0000000 --- a/TwoPhase.toolbox/Model_1_SnapShot_1545923020132/TwoPhase.tla +++ /dev/null @@ -1,182 +0,0 @@ ------------------------------- 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 deleted file mode 100644 index 2e3e8c3..0000000 --- a/TwoPhase.toolbox/TwoPhase___Model_1.launch +++ /dev/null @@ -1,48 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922765832.launch b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922765832.launch deleted file mode 100644 index 18d7099..0000000 --- a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922765832.launch +++ /dev/null @@ -1,47 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922881813.launch b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922881813.launch deleted file mode 100644 index 574af93..0000000 --- a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922881813.launch +++ /dev/null @@ -1,47 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922927774.launch b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922927774.launch deleted file mode 100644 index e70277a..0000000 --- a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545922927774.launch +++ /dev/null @@ -1,47 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545923020132.launch b/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545923020132.launch deleted file mode 100644 index f6cfe52..0000000 --- a/TwoPhase.toolbox/TwoPhase___Model_1_SnapShot_1545923020132.launch +++ /dev/null @@ -1,48 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/Untitled.toolbox/.project b/Untitled.toolbox/.project deleted file mode 100644 index b919234..0000000 --- a/Untitled.toolbox/.project +++ /dev/null @@ -1,24 +0,0 @@ - - - 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 deleted file mode 100644 index 62403c1..0000000 --- a/Untitled.toolbox/.settings/org.lamport.tla.toolbox.prefs +++ /dev/null @@ -1,2 +0,0 @@ -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 deleted file mode 100644 index 903ef9b..0000000 --- a/Untitled.toolbox/Model_1/MC.cfg +++ /dev/null @@ -1,7 +0,0 @@ -\* 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 deleted file mode 100644 index 32b1e70..0000000 --- a/Untitled.toolbox/Model_1/MC.tla +++ /dev/null @@ -1,14 +0,0 @@ ----- 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 deleted file mode 100644 index b7db42b..0000000 --- a/Untitled.toolbox/Model_1/SimpleProgram.tla +++ /dev/null @@ -1,21 +0,0 @@ ---------------------------- 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 deleted file mode 100644 index 671d938..0000000 --- a/Untitled.toolbox/Model_1_SnapShot_1545403778936/MC.cfg +++ /dev/null @@ -1,7 +0,0 @@ -\* 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 deleted file mode 100644 index 5305397..0000000 --- a/Untitled.toolbox/Model_1_SnapShot_1545403778936/MC.tla +++ /dev/null @@ -1,14 +0,0 @@ ----- 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 deleted file mode 100644 index b7db42b..0000000 --- a/Untitled.toolbox/Model_1_SnapShot_1545403778936/SimpleProgram.tla +++ /dev/null @@ -1,21 +0,0 @@ ---------------------------- 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 deleted file mode 100644 index 903ef9b..0000000 --- a/Untitled.toolbox/Model_1_SnapShot_1545403888272/MC.cfg +++ /dev/null @@ -1,7 +0,0 @@ -\* 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 deleted file mode 100644 index 32b1e70..0000000 --- a/Untitled.toolbox/Model_1_SnapShot_1545403888272/MC.tla +++ /dev/null @@ -1,14 +0,0 @@ ----- 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 deleted file mode 100644 index b7db42b..0000000 --- a/Untitled.toolbox/Model_1_SnapShot_1545403888272/SimpleProgram.tla +++ /dev/null @@ -1,21 +0,0 @@ ---------------------------- 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 deleted file mode 100644 index 993e481..0000000 Binary files a/Untitled.toolbox/SimpleProgram.pdf and /dev/null differ diff --git a/Untitled.toolbox/SimpleProgram.tex b/Untitled.toolbox/SimpleProgram.tex deleted file mode 100644 index c71ce72..0000000 --- a/Untitled.toolbox/SimpleProgram.tex +++ /dev/null @@ -1,976 +0,0 @@ -\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 deleted file mode 100644 index 4d582e0..0000000 --- a/Untitled.toolbox/Untitled___Model_1.launch +++ /dev/null @@ -1,43 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403778936.launch b/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403778936.launch deleted file mode 100644 index 90ea0d2..0000000 --- a/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403778936.launch +++ /dev/null @@ -1,8 +0,0 @@ - - - - - - - - diff --git a/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403888272.launch b/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403888272.launch deleted file mode 100644 index c742cc6..0000000 --- a/Untitled.toolbox/Untitled___Model_1_SnapShot_1545403888272.launch +++ /dev/null @@ -1,43 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -