Moved Paxos (Turing) models into directory

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
tlaplus · Jan 22, 2024 · d212e7a · d212e7a
1 parent 64cb2d2
commit d212e7a
Show file tree

Hide file tree

Showing 33 changed files with 35 additions and 2,569 deletions.
diff --git a/manifest.json b/manifest.json
@@ -1374,29 +1374,13 @@
           "models": []
         },
         {
-          "path": "specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/Consensus.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/FiniteSets.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.tla",
+          "path": "specifications/PaxosHowToWinATuringAward/MCConsensus.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
           "models": [
             {
-              "path": "specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.cfg",
+              "path": "specifications/PaxosHowToWinATuringAward/MCConsensus.cfg",
               "runtime": "00:00:01",
               "size": "small",
               "mode": "exhaustive search",
@@ -1408,86 +1392,23 @@
           ]
         },
         {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Consensus.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/FiniteSets.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.tla",
+          "path": "specifications/PaxosHowToWinATuringAward/MCPaxos.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
           "models": [
             {
-              "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.cfg",
+              "path": "specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg",
               "runtime": "00:01:00",
               "size": "medium",
               "mode": "exhaustive search",
               "features": [
                 "liveness"
               ],
               "result": "success"
-            }
-          ]
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Paxos.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Voting.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Consensus.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/FiniteSets.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": [
+            },
             {
-              "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.cfg",
+              "path": "specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg",
               "runtime": "00:00:01",
               "size": "small",
               "mode": "exhaustive search",
@@ -1499,54 +1420,13 @@
           ]
         },
         {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Paxos.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Voting.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Voting.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Consensus.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/FiniteSets.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/MC.tla",
+          "path": "specifications/PaxosHowToWinATuringAward/MCVoting.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
           "models": [
             {
-              "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/MC.cfg",
+              "path": "specifications/PaxosHowToWinATuringAward/MCVoting.cfg",
               "runtime": "00:00:01",
               "size": "small",
               "mode": "exhaustive search",
@@ -1559,7 +1439,14 @@
           ]
         },
         {
-          "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Voting.tla",
+          "path": "specifications/PaxosHowToWinATuringAward/Paxos.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/PaxosHowToWinATuringAward/Voting.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [

diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/.project b/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/.project
diff --git a/...tions/PaxosHowToWinATuringAward/Consensus.toolbox/.settings/org.lamport.tla.toolbox.prefs b/...tions/PaxosHowToWinATuringAward/Consensus.toolbox/.settings/org.lamport.tla.toolbox.prefs
diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/Consensus.tla b/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/Consensus.tla
diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/FiniteSets.tla b/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/FiniteSets.tla
diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/Consensus___3Values.launch b/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/Consensus___3Values.launch
diff --git a/...ingAward/Consensus.toolbox/3Values/MC.cfg → ...PaxosHowToWinATuringAward/MCConsensus.cfg b/...ingAward/Consensus.toolbox/3Values/MC.cfg → ...PaxosHowToWinATuringAward/MCConsensus.cfg
diff --git a/...ingAward/Consensus.toolbox/3Values/MC.tla → ...PaxosHowToWinATuringAward/MCConsensus.tla b/...ingAward/Consensus.toolbox/3Values/MC.tla → ...PaxosHowToWinATuringAward/MCConsensus.tla
@@ -1,4 +1,4 @@
----- MODULE MC ----
+---- MODULE MCConsensus ----
 EXTENDS Consensus, TLC
 
 \* MV CONSTANT declarations@modelParameterConstants

diff --git a/...uringAward/Paxos.toolbox/TinyModel/MC.tla → ...ons/PaxosHowToWinATuringAward/MCPaxos.tla b/...uringAward/Paxos.toolbox/TinyModel/MC.tla → ...ons/PaxosHowToWinATuringAward/MCPaxos.tla
@@ -1,6 +1,8 @@
----- MODULE MC ----
+---- MODULE MCPaxos ----
 EXTENDS Paxos, TLC
 
+CONSTANT MaxBallot
+
 \* MV CONSTANT declarations@modelParameterConstants
 CONSTANTS
 a1, a2, a3
@@ -28,11 +30,11 @@ const_1560336937634607000 ==
 
 \* CONSTANT definition @modelParameterDefinitions:1
 def_ov_1560336937634609000 ==
-0..1
+0..MaxBallot
 ----
 \* CONSTANT definition @modelParameterDefinitions:2
 def_ov_1560336937634610000 ==
-0..1
+0..MaxBallot
 ----
 \* PROPERTY definition @modelCorrectnessProperties:0
 prop_1560336937635612000 ==