Fix proofs

.github/scripts/check_proofs.py

@@ -48,7 +48,8 @@
     tlapm = subprocess.run(
         [
             tlapm_path, module_path,
-            '-I', module_dir
+            '-I', module_dir,
+            '--stretch', '5'
         ],
         stdout=subprocess.PIPE,
         stderr=subprocess.STDOUT,

.github/workflows/CI.yml

@@ -108,7 +108,9 @@ jobs:
       - name: Check small models
         run: |
           # Need to have a nonempty list to pass as a skip parameter
-          SKIP=("does/not/exist")
+          # SKIP=("does/not/exist")
+          # strange issue with parsing TLC output
+          SKIP=("specifications/ewd840/EWD840.cfg")
           if [ ${{ matrix.unicode }} ]; then
             # Apalache does not yet support Unicode
             SKIP+=("specifications/EinsteinRiddle/Einstein.cfg")
@@ -143,21 +145,16 @@ jobs:
         if: matrix.os != 'windows-latest' && !matrix.unicode
         run: |
           SKIP=(
-            ## ATD/EWD require TLAPS' update_enabled_cdot branch
-            specifications/ewd998/AsyncTerminationDetection_proof.tla
+            # Long-running; see https://github.com/tlaplus/tlapm/issues/85
             specifications/ewd998/EWD998_proof.tla
-            # Failing; see https://github.com/tlaplus/Examples/issues/67
             specifications/Bakery-Boulangerie/Bakery.tla
             specifications/Bakery-Boulangerie/Boulanger.tla
-            specifications/Paxos/Consensus.tla
-            specifications/PaxosHowToWinATuringAward/Consensus.tla
-            specifications/lamport_mutex/LamportMutex_proofs.tla
-            specifications/byzpaxos/VoteProof.tla
-            # Long-running; see https://github.com/tlaplus/tlapm/issues/85
             specifications/LoopInvariance/Quicksort.tla
             specifications/LoopInvariance/SumSequence.tla
+            specifications/lamport_mutex/LamportMutex_proofs.tla
             specifications/bcastByz/bcastByz.tla
-            specifications/MisraReachability/ReachabilityProofs.tla
+            # specifications/MisraReachability/ReachabilityProofs.tla
+            specifications/byzpaxos/VoteProof.tla
             specifications/byzpaxos/BPConProof.tla # Takes about 30 minutes
           )
           python $SCRIPT_DIR/check_proofs.py       \

README.md

@@ -29,7 +29,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)                                                       | Martin Riener                                       |    ✔     |      ✔      |         |     ✔     |          |
 | [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                                      |    ✔     |             |         |     ✔     |          |
@@ -48,11 +48,11 @@ Here is a list of specs included in this repository, with links to the relevant
 | [Byzantizing Paxos by Refinement](specifications/byzpaxos)                                          | 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                                      |          |      ✔      |         |     ✔     |          |
+| [The Paxos Protocol](specifications/Paxos)                                                          | Leslie Lamport                                      |          |     (✔)     |         |     ✔     |          |
 | [Asynchronous Reliable Broadcast](specifications/bcastByz)                                          | Thanh Hai Tran, Igor Konnov, Josef Widder           |          |      ✔      |         |     ✔     |          |
 | [Distributed Mutual Exclusion](specifications/lamport_mutex)                                        | Stephan Merz                                        |          |      ✔      |         |     ✔     |          |
 | [Two-Phase Handshaking](specifications/TwoPhase)                                                    | Leslie Lamport, Stephan Merz                        |          |      ✔      |         |     ✔     |          |
-| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward)                       | Leslie Lamport                                      |          |      ✔      |         |     ✔     |          |
+| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward)                       | Leslie Lamport                                      |          |     (✔)     |         |     ✔     |          |
 | [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex)                              | Leslie Lamport                                      |          |             |    ✔    |     ✔     |          |
 | [The Echo Algorithm](specifications/echo)                                                           | Stephan Merz                                        |          |             |    ✔    |     ✔     |          |
 | [The TLC Safety Checking Algorithm](specifications/TLC)                                             | Markus Kuppe                                        |          |             |    ✔    |     ✔     |          |

manifest.json

@@ -46,8 +46,8 @@
                 "ignore deadlock"
               ],
               "result": "success",
-              "distinctStates": 598608,
-              "totalStates": 3141768,
+              "distinctStates": 655200,
+              "totalStates": 3403584,
               "stateDepth": 1
             }
           ]
@@ -587,6 +587,20 @@
           "features": [],
           "models": []
         },
+        {
+          "path": "specifications/FiniteMonotonic/Functions.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/FiniteMonotonic/Folds.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
         {
           "path": "specifications/FiniteMonotonic/MCCRDT.tla",
           "communityDependencies": [
@@ -3271,15 +3285,6 @@
             }
           ]
         },
-        {
-          "path": "specifications/TwoPhase/TLAPS.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
         {
           "path": "specifications/TwoPhase/TwoPhase.tla",
           "communityDependencies": [],
@@ -4502,7 +4507,8 @@
               "size": "small",
               "mode": "exhaustive search",
               "features": [
-                "ignore deadlock"
+                "ignore deadlock",
+                "liveness"
               ],
               "result": "success",
               "distinctStates": 302,
@@ -4588,12 +4594,10 @@
           ]
         },
         {
-          "path": "specifications/ewd840/TLAPS.tla",
+          "path": "specifications/ewd840/SyncTerminationDetection_proof.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
+          "features": ["proof"],
           "models": []
         }
       ]
@@ -4645,7 +4649,6 @@
         {
           "path": "specifications/ewd998/EWD998.tla",
           "communityDependencies": [
-            "Functions",
             "SequencesExt"
           ],
           "tlaLanguageVersion": 2,
@@ -4658,7 +4661,8 @@
               "mode": "exhaustive search",
               "features": [
                 "ignore deadlock",
-                "state constraint"
+                "state constraint",
+                "liveness"
               ],
               "result": "success"
             },
@@ -4853,6 +4857,20 @@
           ],
           "models": []
         },
+        {
+          "path": "specifications/ewd998/Functions.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/ewd998/Folds.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
         {
           "path": "specifications/ewd998/SmokeEWD998.tla",
           "communityDependencies": [
@@ -4899,19 +4917,9 @@
             }
           ]
         },
-        {
-          "path": "specifications/ewd998/TLAPS.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
         {
           "path": "specifications/ewd998/Utils.tla",
           "communityDependencies": [
-            "Functions",
             "SequencesExt"
           ],
           "tlaLanguageVersion": 2,
@@ -5007,13 +5015,6 @@
       ],
       "tags": [],
       "modules": [
-        {
-          "path": "specifications/lamport_mutex/Functions.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
         {
           "path": "specifications/lamport_mutex/LamportMutex.tla",
           "communityDependencies": [],
@@ -5050,36 +5051,6 @@
               "stateDepth": 61
             }
           ]
-        },
-        {
-          "path": "specifications/lamport_mutex/NaturalsInduction.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/lamport_mutex/SequenceTheorems.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/lamport_mutex/TLAPS.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
-        {
-          "path": "specifications/lamport_mutex/WellFoundedInduction.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
         }
       ]
     },
@@ -5194,7 +5165,7 @@
       "description": "Two proofs that x+x is even for every natural number x",
       "sources": [],
       "authors": [
-        "Stephan Merz"
+        "Martin Riener"
       ],
       "tags": [
         "beginner"
@@ -5219,15 +5190,6 @@
             }
           ]
         },
-        {
-          "path": "specifications/sums_even/TLAPS.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [
-            "proof"
-          ],
-          "models": []
-        },
         {
           "path": "specifications/sums_even/sums_even.tla",
           "communityDependencies": [],