Added models for bcastByz and sums_even

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Jan 19, 2024 · 1962ef2 · 1962ef2
1 parent 40a1089
commit 1962ef2
Show file tree

Hide file tree

Showing 8 changed files with 47 additions and 2 deletions.
diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py
@@ -108,6 +108,7 @@ def resolve_tlc_exit_code(code):
     """
     tlc_exit_codes = {
         0   : 'success',
+        10  : 'assumption failure',
         11  : 'deadlock failure',
         12  : 'safety failure',
         13  : 'liveness failure'

diff --git a/README.md b/README.md
@@ -22,7 +22,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [Loop Invariance](specifications/LoopInvariance)                                                    | Leslie Lamport                             |    ✔     |      ✔      |    ✔    |     ✔     |          |
 | [Learn TLA⁺ Proofs](specifications/LearnProofs)                                                     | Andrew Helwer                              |    ✔     |      ✔      |    ✔    |     ✔     |          |
 | [Boyer-Moore Majority Vote](specifications/Majority)                                                | Stephan Merz                               |    ✔     |      ✔      |         |     ✔     |          |
-| [Proof x+x is Even](specifications/sums_even)                                                       | Stephan Merz                               |    ✔     |      ✔      |         |           |          |
+| [Proof x+x is Even](specifications/sums_even)                                                       | Stephan Merz                               |    ✔     |      ✔      |         |     ✔     |          |
 | [The N-Queens Puzzle](specifications/N-Queens)                                                      | Stephan Merz                               |    ✔     |             |    ✔    |     ✔     |          |
 | [The Dining Philosophers Problem](specifications/DiningPhilosophers)                                | Jeff Hemphill                              |    ✔     |             |    ✔    |     ✔     |          |
 | [The Car Talk Puzzle](specifications/CarTalkPuzzle)                                                 | Leslie Lamport                             |    ✔     |             |         |     ✔     |          |

diff --git a/manifest-schema.json b/manifest-schema.json
@@ -78,7 +78,7 @@
                         "type": "array",
                         "items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint", "ignore deadlock"]}
                       },
-                      "result": {"enum": ["success", "safety failure", "liveness failure", "deadlock failure", "unknown"]}
+                      "result": {"enum": ["success", "assumption failure", "deadlock failure", "safety failure", "liveness failure", "unknown"]}
                     }
                   }
                 }

diff --git a/manifest.json b/manifest.json
@@ -3760,6 +3760,22 @@
         "beginner"
       ],
       "modules": [
+        {
+          "path": "specifications/sums_even/MC_sums_even.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/sums_even/MC_sums_even.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/sums_even/TLAPS.tla",
           "communityDependencies": [],

diff --git a/specifications/bcastByz/bcastByz.cfg b/specifications/bcastByz/bcastByz.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  N = 4
+  T = 1
+  F = 1
+INVARIANTS TypeOK FCConstraints
+PROPERTIES CorrLtl RelayLtl UnforgLtl
+SPECIFICATION Spec
+
diff --git a/specifications/bcastByz/bcastByzNoBcast.cfg b/specifications/bcastByz/bcastByzNoBcast.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  N = 10
+  T = 3
+  F = 2
+INVARIANTS TypeOK FCConstraints Unforg
+PROPERTIES CorrLtl RelayLtl
+SPECIFICATION SpecNoBcast
+
diff --git a/specifications/sums_even/MC_sums_even.cfg b/specifications/sums_even/MC_sums_even.cfg
@@ -0,0 +1,4 @@
+CONSTANT
+  MaxNat = 1000000
+  Nat <- NatOverride
+
diff --git a/specifications/sums_even/MC_sums_even.tla b/specifications/sums_even/MC_sums_even.tla
@@ -0,0 +1,8 @@
+------------------------ MODULE MC_sums_even -----------------------
+EXTENDS sums_even
+CONSTANT MaxNat
+ASSUME MaxNat \in Nat
+NatOverride == 0 .. MaxNat
+ASSUME T1
+====================================================================
+