Added models for Stones, Bakery-Boulangerie, TeachingConcurrency

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
tlaplus · Jan 18, 2024 · 4fb92bc · 4fb92bc
1 parent a46ca79
commit 4fb92bc
Show file tree

Hide file tree

Showing 15 changed files with 1,036 additions and 930 deletions.
diff --git a/README.md b/README.md
@@ -18,8 +18,8 @@ All specs in this repository are subject to CI validation to ensure quality.
 Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:
 | Name                                                                                                | Author(s)                                  | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
 | --------------------------------------------------------------------------------------------------- | ------------------------------------------ | :------: | :---------: | :-----: | :-------: | :------: |
+| [Teaching Concurrency](specifications/TeachingConcurrency)                                          | Leslie Lamport                             |    ✔     |      ✔      |    ✔    |     ✔     |          |
 | [Learn TLA⁺ Proofs](specifications/LearnProofs)                                                     | Andrew Helwer                              |    ✔     |      ✔      |    ✔    |     ✔     |          |
-| [Teaching Concurrency](specifications/TeachingConcurrency)                                          | Leslie Lamport                             |    ✔     |      ✔      |    ✔    |           |          |
 | [Boyer-Moore Majority Vote](specifications/Majority)                                                | Stephan Merz                               |    ✔     |      ✔      |         |     ✔     |          |
 | [Proof x+x is Even](specifications/sums_even)                                                       | Stephan Merz                               |    ✔     |      ✔      |         |           |          |
 | [The N-Queens Puzzle](specifications/N-Queens)                                                      | Stephan Merz                               |    ✔     |             |    ✔    |     ✔     |          |
@@ -31,8 +31,8 @@ Here is a list of specs included in this repository, with links to the relevant
 | [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi)                                          | Markus Kuppe, Alexander Niederbühl         |    ✔     |             |         |     ✔     |          |
 | [Missionaries and Cannibals](specifications/MissionariesAndCannibals)                               | Leslie Lamport                             |    ✔     |             |         |     ✔     |          |
 | [The Coffee Can Bean Problem](specifications/CoffeeCan)                                             | Andrew Helwer                              |    ✔     |             |         |     ✔     |          |
-| [Stone Scale Puzzle](specifications/Stones)                                                         | Leslie Lamport                             |    ✔     |             |         |           |          |
-| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie)                                      | Leslie Lamport, Stephan Merz               |          |      ✔      |    ✔    |           |          |
+| [Stone Scale Puzzle](specifications/Stones)                                                         | Leslie Lamport                             |    ✔     |             |         |     ✔     |          |
+| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie)                                      | Leslie Lamport, Stephan Merz               |          |      ✔      |    ✔    |     ✔     |          |
 | [Misra Reachability Algorithm](specifications/MisraReachability)                                    | Leslie Lamport                             |          |      ✔      |    ✔    |           |          |
 | [Loop Invariance](specifications/LoopInvariance)                                                    | Leslie Lamport                             |          |      ✔      |    ✔    |           |          |
 | [EWD840: Termination Detection in a Ring](specifications/ewd840)                                    | Stephan Merz                               |          |      ✔      |         |     ✔     |          |

diff --git a/manifest.json b/manifest.json
@@ -30,6 +30,42 @@
             "proof"
           ],
           "models": []
+        },
+        {
+          "path": "specifications/Bakery-Boulangerie/MCBakery.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/Bakery-Boulangerie/MCBakery.cfg",
+              "runtime": "00:00:10",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock"
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/Bakery-Boulangerie/MCBoulanger.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/Bakery-Boulangerie/MCBoulanger.cfg",
+              "runtime": "00:01:00",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "state constraint"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2370,7 +2406,16 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/Stones/Stones.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         }
       ]
     },
@@ -2433,7 +2478,16 @@
             "pluscal",
             "proof"
           ],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/TeachingConcurrency/Simple.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/TeachingConcurrency/SimpleRegular.tla",
@@ -2443,7 +2497,16 @@
             "pluscal",
             "proof"
           ],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/TeachingConcurrency/SimpleRegular.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         }
       ]
     },