Added model for LoopInvariance, tagged it as Beginner

Reverted CRLF newline normalizations Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
tlaplus · Jan 19, 2024 · dd2270d · dd2270d
1 parent 4fb92bc
commit dd2270d
Show file tree

Hide file tree

Showing 12 changed files with 996 additions and 926 deletions.
diff --git a/README.md b/README.md
@@ -19,6 +19,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | Name                                                                                                | Author(s)                                  | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
 | --------------------------------------------------------------------------------------------------- | ------------------------------------------ | :------: | :---------: | :-----: | :-------: | :------: |
 | [Teaching Concurrency](specifications/TeachingConcurrency)                                          | Leslie Lamport                             |    ✔     |      ✔      |    ✔    |     ✔     |          |
+| [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                               |    ✔     |      ✔      |         |           |          |
@@ -34,7 +35,6 @@ Here is a list of specs included in this repository, with links to the relevant
 | [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                               |          |      ✔      |         |     ✔     |          |
 | [EWD998: Termination Detection in a Ring with Asynchronous Message Delivery](specifications/ewd998) | Stephan Merz, Markus Kuppe                 |          |      ✔      |         |     ✔     |          |
 | [The Paxos Protocol](specifications/Paxos)                                                          | Leslie Lamport                             |          |      ✔      |         |     ✔     |          |

diff --git a/manifest.json b/manifest.json
@@ -836,7 +836,9 @@
       "authors": [
         "Leslie Lamport"
       ],
-      "tags": [],
+      "tags": [
+        "beginner"
+      ],
       "modules": [
         {
           "path": "specifications/LoopInvariance/BinarySearch.tla",
@@ -848,6 +850,42 @@
           ],
           "models": []
         },
+        {
+          "path": "specifications/LoopInvariance/MCBinarySearch.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/LoopInvariance/MCBinarySearch.cfg",
+              "runtime": "small",
+              "size": "00:00:05",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/LoopInvariance/MCQuicksort.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/LoopInvariance/MCQuicksort.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/LoopInvariance/Quicksort.tla",
           "communityDependencies": [],