-
Notifications
You must be signed in to change notification settings - Fork 201
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Re-added Paxos (Turing Award) toolbox setting files
Signed-off-by: Andrew Helwer <[email protected]>
- Loading branch information
Showing
11 changed files
with
270 additions
and
0 deletions.
There are no files selected for viewing
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> |
34 changes: 34 additions & 0 deletions
34
specifications/PaxosHowToWinATuringAward/Paxos.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,34 @@ | ||
| <?xml version="1.0" encoding="UTF-8"?> | ||
| <projectDescription> | ||
| <name>Paxos</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> | ||
| <location>PARENT-1-PROJECT_LOC/Consensus.tla</location> | ||
| </link> | ||
| <link> | ||
| <name>Paxos.tla</name> | ||
| <type>1</type> | ||
| <locationURI>PARENT-1-PROJECT_LOC/Paxos.tla</locationURI> | ||
| </link> | ||
| <link> | ||
| <name>Voting.tla</name> | ||
| <type>1</type> | ||
| <location>PARENT-1-PROJECT_LOC/Voting.tla</location> | ||
| </link> | ||
| </linkedResources> | ||
| </projectDescription> |
2 changes: 2 additions & 0 deletions
2
...fications/PaxosHowToWinATuringAward/Paxos.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/Paxos.tla | ||
| eclipse.preferences.version=1 |
43 changes: 43 additions & 0 deletions
43
specifications/PaxosHowToWinATuringAward/Paxos.toolbox/Paxos___SmallModel.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,43 @@ | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <stringAttribute key="configurationName" value="SmallModel"/> | ||
| <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="maxVal, maxVBal, msgs, maxBal"/> | ||
| <stringAttribute key="modelComments" value="Has three acceptors, two values, and three ballots."/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"> | ||
| <listEntry value="1Inv"/> | ||
| </listAttribute> | ||
| <listAttribute key="modelCorrectnessProperties"> | ||
| <listEntry value="1V!Spec"/> | ||
| </listAttribute> | ||
| <intAttribute key="modelEditorOpenTabs" value="6"/> | ||
| <stringAttribute key="modelExpressionEval" value=""/> | ||
| <stringAttribute key="modelParameterActionConstraint" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="Acceptor;;{a1, a2, a3};1;0"/> | ||
| <listEntry value="Quorum;;{{a1, a2}, {a1, a3}, {a2, a3}};0;0"/> | ||
| <listEntry value="Value;;{v1, v2};1;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterContraint" value=""/> | ||
| <listAttribute key="modelParameterDefinitions"> | ||
| <listEntry value="None;;None;1;0"/> | ||
| <listEntry value="Ballot;;0..2;0;0"/> | ||
| <listEntry value="V!Ballot;;0..2;0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterModelValues" value="{}"/> | ||
| <stringAttribute key="modelParameterNewDefinitions" value=""/> | ||
| <intAttribute key="numberOfWorkers" value="2"/> | ||
| <stringAttribute key="result.mail.address" value=""/> | ||
| <stringAttribute key="specName" value="Paxos"/> | ||
| <stringAttribute key="tlcResourcesProfile" value="local custom"/> | ||
| </launchConfiguration> |
48 changes: 48 additions & 0 deletions
48
specifications/PaxosHowToWinATuringAward/Paxos.toolbox/Paxos___TinyModel.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,48 @@ | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <stringAttribute key="configurationName" value="TinyModel"/> | ||
| <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="40"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value="Spec"/> | ||
| <intAttribute key="modelBehaviorSpecType" value="1"/> | ||
| <stringAttribute key="modelBehaviorVars" value="maxVal, maxVBal, msgs, maxBal"/> | ||
| <stringAttribute key="modelComments" value="Has three acceptors, two values, and two ballots."/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"> | ||
| <listEntry value="1Inv"/> | ||
| </listAttribute> | ||
| <listAttribute key="modelCorrectnessProperties"> | ||
| <listEntry value="1V!Spec"/> | ||
| </listAttribute> | ||
| <intAttribute key="modelEditorOpenTabs" value="2"/> | ||
| <stringAttribute key="modelExpressionEval" value=""/> | ||
| <stringAttribute key="modelParameterActionConstraint" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="Acceptor;;{a1, a2, a3};1;0"/> | ||
| <listEntry value="Quorum;;{{a1, a2}, {a1, a3}, {a2, a3}};0;0"/> | ||
| <listEntry value="Value;;{v1, v2};1;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterContraint" value=""/> | ||
| <listAttribute key="modelParameterDefinitions"> | ||
| <listEntry value="None;;None;1;0"/> | ||
| <listEntry value="Ballot;;0..1;0;0"/> | ||
| <listEntry value="V!Ballot;;0..1;0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterModelValues" value="{}"/> | ||
| <stringAttribute key="modelParameterNewDefinitions" value=""/> | ||
| <intAttribute key="numberOfWorkers" value="2"/> | ||
| <stringAttribute key="result.mail.address" value=""/> | ||
| <stringAttribute key="specName" value="Paxos"/> | ||
| <stringAttribute key="tlcResourcesProfile" value="local nomal"/> | ||
| <listAttribute key="traceExploreExpressions"> | ||
| <listEntry value="1V!chosen"/> | ||
| <listEntry value="1V!Next"/> | ||
| <listEntry value="1votes"/> | ||
| </listAttribute> | ||
| </launchConfiguration> |
29 changes: 29 additions & 0 deletions
29
specifications/PaxosHowToWinATuringAward/Voting.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,29 @@ | ||
| <?xml version="1.0" encoding="UTF-8"?> | ||
| <projectDescription> | ||
| <name>Voting</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> | ||
| <location>PARENT-1-PROJECT_LOC/Consensus.tla</location> | ||
| </link> | ||
| <link> | ||
| <name>Voting.tla</name> | ||
| <type>1</type> | ||
| <locationURI>PARENT-1-PROJECT_LOC/Voting.tla</locationURI> | ||
| </link> | ||
| </linkedResources> | ||
| </projectDescription> |
2 changes: 2 additions & 0 deletions
2
...ications/PaxosHowToWinATuringAward/Voting.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/Voting.tla | ||
| eclipse.preferences.version=1 |
Binary file not shown.
57 changes: 57 additions & 0 deletions
57
specifications/PaxosHowToWinATuringAward/Voting.toolbox/Voting___SmallModel.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,57 @@ | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <stringAttribute key="TLCCmdLineParameters" value=""/> | ||
| <intAttribute key="collectCoverage" value="1"/> | ||
| <stringAttribute key="configurationName" value="SmallModel"/> | ||
| <booleanAttribute key="deferLiveness" value="false"/> | ||
| <intAttribute key="dfidDepth" value="100"/> | ||
| <booleanAttribute key="dfidMode" value="false"/> | ||
| <intAttribute key="distributedFPSetCount" value="0"/> | ||
| <stringAttribute key="distributedNetworkInterface" value="100.64.12.255"/> | ||
| <intAttribute key="distributedNodesCount" value="1"/> | ||
| <stringAttribute key="distributedTLC" value="off"/> | ||
| <stringAttribute key="distributedTLCVMArgs" value=""/> | ||
| <intAttribute key="fpBits" value="1"/> | ||
| <intAttribute key="fpIndex" value="108"/> | ||
| <booleanAttribute key="fpIndexRandom" value="true"/> | ||
| <intAttribute key="maxHeapSize" value="25"/> | ||
| <intAttribute key="maxSetSize" value="1000000"/> | ||
| <booleanAttribute key="mcMode" value="true"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value="Spec"/> | ||
| <intAttribute key="modelBehaviorSpecType" value="1"/> | ||
| <stringAttribute key="modelBehaviorVars" value="maxBal, votes"/> | ||
| <stringAttribute key="modelComments" value="Has three acceptors, two values, and three ballots."/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/> | ||
| <listAttribute key="modelCorrectnessInvariants"> | ||
| <listEntry value="1Inv"/> | ||
| </listAttribute> | ||
| <listAttribute key="modelCorrectnessProperties"> | ||
| <listEntry value="1C!Spec"/> | ||
| </listAttribute> | ||
| <intAttribute key="modelEditorOpenTabs" value="6"/> | ||
| <stringAttribute key="modelExpressionEval" value=""/> | ||
| <stringAttribute key="modelParameterActionConstraint" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="Acceptor;;{a1, a2, a3};1;0"/> | ||
| <listEntry value="Value;;{v1, v2};1;0"/> | ||
| <listEntry value="Quorum;;{{a1, a2}, {a1, a3}, {a2, a3}};0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterContraint" value=""/> | ||
| <listAttribute key="modelParameterDefinitions"> | ||
| <listEntry value="Ballot;;0..2;0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterModelValues" value="{}"/> | ||
| <stringAttribute key="modelParameterNewDefinitions" value=""/> | ||
| <intAttribute key="numberOfWorkers" value="2"/> | ||
| <booleanAttribute key="recover" value="false"/> | ||
| <stringAttribute key="result.mail.address" value=""/> | ||
| <intAttribute key="simuAril" value="-1"/> | ||
| <intAttribute key="simuDepth" value="100"/> | ||
| <intAttribute key="simuSeed" value="-1"/> | ||
| <stringAttribute key="specName" value="Voting"/> | ||
| <stringAttribute key="tlcResourcesProfile" value="local custom"/> | ||
| <stringAttribute key="view" value=""/> | ||
| <booleanAttribute key="visualizeStateGraph" value="false"/> | ||
| </launchConfiguration> |