Added models for bcastByz and sums_even

ahelwer · ahelwer · commit 1962ef239237 · 2024-01-19T11:41:12.000-05:00
Signed-off-by: Andrew Helwer &lt;2n8rn1w1f@mozmail.com&gt;
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
+====================================================================
+

Original file line number	Diff line number	Diff line change
`@@ -78,7 +78,7 @@`
`78`	`78`	`"type": "array",`
`79`	`79`	`"items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint", "ignore deadlock"]}`
`80`	`80`	`},`
`81`		`- "result": {"enum": ["success", "safety failure", "liveness failure", "deadlock failure", "unknown"]}`
	`81`	`+ "result": {"enum": ["success", "assumption failure", "deadlock failure", "safety failure", "liveness failure", "unknown"]}`
`82`	`82`	`}`
`83`	`83`	`}`
`84`	`84`	`}`