forked from tlaplus/Examples
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Added Leslie's Paxos How To Win A Turing Award lecture
- Loading branch information
Showing
19 changed files
with
1,192 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,113 @@ | ||
| ----------------------------- MODULE Consensus ------------------------------ | ||
| (***************************************************************************) | ||
| (* This is an very abstract specification of the consensus problem, in *) | ||
| (* which a set of processes must choose a single value. We abstract away *) | ||
| (* even the processes. We specify the simple requirement that at most one *) | ||
| (* value is chosen by describing the set of all chosen values. The naive *) | ||
| (* requirement is that this set never contains more than one value, which *) | ||
| (* is an invariance property. But a little thought shows that this *) | ||
| (* requirement allows a value to be chosen then unchosen, and then another *) | ||
| (* value to be chosen. So we specify that the set of chosen values is *) | ||
| (* initially empty, it can be set to a single value, and then it can never *) | ||
| (* change. *) | ||
| (* *) | ||
| (* We are ignoring liveness, so we do not any requirement that a value is *) | ||
| (* eventually chosen. *) | ||
| (***************************************************************************) | ||
|
|
||
| EXTENDS Naturals, FiniteSets | ||
| (*************************************************************************) | ||
| (* Imports standard modules that define operators of arithmetic on *) | ||
| (* natural numbers and the Cardinality operator, where Cardinality(S) is *) | ||
| (* the number of elements in the set S, if S is finite. *) | ||
| (*************************************************************************) | ||
| CONSTANT Value | ||
| (*************************************************************************) | ||
| (* The set of all values that can be chosen. *) | ||
| (*************************************************************************) | ||
| VARIABLE chosen | ||
| (*************************************************************************) | ||
| (* The set of all values that have been chosen. *) | ||
| (*************************************************************************) | ||
|
|
||
| (***************************************************************************) | ||
| (* The type-correctness invariant asserting the "type" of the variable *) | ||
| (* 'chosen'. It isn't part of the spec itself--that is, the formula *) | ||
| (* describing the possible sequence of values that 'chosen' can have in a *) | ||
| (* behavior correct behavior of the system, but is an invariance property *) | ||
| (* that the spec should satisfy. *) | ||
| (***************************************************************************) | ||
| TypeOK == /\ chosen \subseteq Value | ||
| /\ IsFiniteSet(chosen) | ||
|
|
||
| (***************************************************************************) | ||
| (* The initial predicate describing the possible initial state of *) | ||
| (* 'chosen'. *) | ||
| (***************************************************************************) | ||
| Init == chosen = {} | ||
|
|
||
| (***************************************************************************) | ||
| (* The next-state relation describing how 'chosen' can change from one *) | ||
| (* step to the next. Note that is enabled (equals true for some next *) | ||
| (* value chosen' of choseen) if and only if chosen equals the empty set. *) | ||
| (***************************************************************************) | ||
| Next == /\ chosen = {} | ||
| /\ \E v \in Value : chosen' = {v} | ||
|
|
||
| (***************************************************************************) | ||
| (* The TLA+ temporal formula that is the spec. *) | ||
| (***************************************************************************) | ||
| Spec == Init /\ [][Next]_chosen | ||
|
|
||
| ----------------------------------------------------------------------------- | ||
| (***************************************************************************) | ||
| (* The specification should imply the safety property that 'chosen' can *) | ||
| (* contain at most one value in any reachable state. This condition on *) | ||
| (* the state is expressed by Inv defined here. *) | ||
| (***************************************************************************) | ||
| Inv == /\ TypeOK | ||
| /\ Cardinality(chosen) \leq 1 | ||
|
|
||
| (***************************************************************************) | ||
| (* The following theorem asserts the desired safety propert. Its proof *) | ||
| (* appears after the theorem. This proof is easily checked by the TLAPS *) | ||
| (* prover. *) | ||
| (***************************************************************************) | ||
| THEOREM Invariance == Spec => []Inv | ||
| <1>1. Init => Inv | ||
|
|
||
| <1>2. Inv /\ [Next]_chosen => Inv' | ||
|
|
||
| <1>3. QED | ||
| BY <1>1, <1>2 DEF Spec | ||
|
|
||
| (***************************************************************************) | ||
| (* If you are reading this specification in the Toolbox as you should be *) | ||
| (* (either the source file or its pretty-printed version), then you have *) | ||
| (* already opened the specification in the Toolbox. If not, you should do *) | ||
| (* that now. Download and run the Toolbox. Open a new specification with *) | ||
| (* this module file (Consensus.tla) as the root file, using the default *) | ||
| (* specification name, which is the name of the root file. Along with the *) | ||
| (* module, this will install a TLC model named 3Values. Open that model. *) | ||
| (* You will see that the model specifies three things: *) | ||
| (* *) | ||
| (* - The specification is formula Spec. *) | ||
| (* *) | ||
| (* - Three unspecified constants a, b, and c (called model values) *) | ||
| (* are substituted for the declared constants Values. *) | ||
| (* *) | ||
| (* - TLC should check that formula Inv is an invariant (a *) | ||
| (* formula true on all reachable states of he specification. *) | ||
| (* *) | ||
| (* Run TLC on the model. For this tiny spec, this just takes perhaps a *) | ||
| (* millisecond plus the couple of seconds that TLC needs to start and stop *) | ||
| (* running any spec. *) | ||
| (* *) | ||
| (* TLC's default setting to check for deadlock would cause it to report a *) | ||
| (* deadlock because no action is possible after a value is chosen. We *) | ||
| (* would say that the system terminated, but termination is just deadlock *) | ||
| (* that we want to happen, and the model tells TLC that we want deadlock *) | ||
| (* by disabling its check for it. *) | ||
| (***************************************************************************) | ||
|
|
||
| ============================================================================= |
24 changes: 24 additions & 0 deletions
24
specifications/PaxosHowToWinATuringAward/Consensus.toolbox/.project
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,24 @@ | ||
| <?xml version="1.0" encoding="UTF-8"?> | ||
| <projectDescription> | ||
| <name>Consensus</name> | ||
| <comment></comment> | ||
| <projects> | ||
| </projects> | ||
| <buildSpec> | ||
| <buildCommand> | ||
| <name>toolbox.builder.TLAParserBuilder</name> | ||
| <arguments> | ||
| </arguments> | ||
| </buildCommand> | ||
| </buildSpec> | ||
| <natures> | ||
| <nature>toolbox.natures.TLANature</nature> | ||
| </natures> | ||
| <linkedResources> | ||
| <link> | ||
| <name>Consensus.tla</name> | ||
| <type>1</type> | ||
| <locationURI>PARENT-1-PROJECT_LOC/Consensus.tla</locationURI> | ||
| </link> | ||
| </linkedResources> | ||
| </projectDescription> |
2 changes: 2 additions & 0 deletions
2
...tions/PaxosHowToWinATuringAward/Consensus.toolbox/.settings/org.lamport.tla.toolbox.prefs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| ProjectRootFile=PARENT-1-PROJECT_LOC/Consensus.tla | ||
| eclipse.preferences.version=1 |
29 changes: 29 additions & 0 deletions
29
specifications/PaxosHowToWinATuringAward/Consensus.toolbox/Consensus___3Values.launch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <stringAttribute key="configurationName" value="3Values"/> | ||
| <intAttribute key="distributedFPSetCount" value="0"/> | ||
| <stringAttribute key="distributedNetworkInterface" value="100.64.12.255"/> | ||
| <intAttribute key="distributedNodesCount" value="1"/> | ||
| <stringAttribute key="distributedTLC" value="off"/> | ||
| <intAttribute key="fpIndex" value="0"/> | ||
| <intAttribute key="maxHeapSize" value="25"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value="Spec"/> | ||
| <intAttribute key="modelBehaviorSpecType" value="1"/> | ||
| <stringAttribute key="modelBehaviorVars" value="chosen"/> | ||
| <stringAttribute key="modelComments" value="A simple model of our trivial spec, in which Value is assigned the value {a, b, c} for unspecified constants a, b, and c. It checks that Inv is an invariant. If 'Deadlock' hadn't been unchecked, TLC would report termination as deadlock."/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/> | ||
| <listAttribute key="modelCorrectnessInvariants"> | ||
| <listEntry value="1Inv"/> | ||
| </listAttribute> | ||
| <listAttribute key="modelCorrectnessProperties"/> | ||
| <stringAttribute key="modelExpressionEval" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="Value;;{a, b, c};1;0"/> | ||
| </listAttribute> | ||
| <intAttribute key="numberOfWorkers" value="2"/> | ||
| <stringAttribute key="result.mail.address" value=""/> | ||
| <stringAttribute key="specName" value="Consensus"/> | ||
| <stringAttribute key="tlcResourcesProfile" value="local custom"/> | ||
| </launchConfiguration> |
Binary file not shown.
Oops, something went wrong.