EWD840 and EWD998 proofs rely on tlapm soundness bug

.github/scripts/tla_utils.py

@@ -3,7 +3,7 @@
 from datetime import timedelta
 import json
 import os
-from os.path import join, normpath, pathsep, dirname
+from os.path import abspath, join, normpath, pathsep, dirname
 from pathlib import PureWindowsPath
 import subprocess
 import sys
@@ -199,9 +199,9 @@ def check_model(
     # through `cmd.exe /c`. On Linux/macOS it is the unsuffixed shell script
     # `apalache-mc` and we invoke it directly.
     apalache_launcher = (
-        ['cmd.exe', '/c', normpath(join(apalache_path, 'bin', 'apalache-mc.bat'))]
+        ['cmd.exe', '/c', abspath(join(apalache_path, 'bin', 'apalache-mc.bat'))]
         if sys.platform == 'win32' else
-        [normpath(join(apalache_path, 'bin', 'apalache-mc'))])
+        [abspath(join(apalache_path, 'bin', 'apalache-mc'))])
     module_path = normpath(module_path)
     model_path = normpath(model_path)
     tlapm_lib_path = normpath(tlapm_lib_path)
@@ -212,13 +212,19 @@ def check_model(
             # example. Apalache's own default of 10 is itself an arbitrary
             # choice; 5 keeps CI runtimes manageable across the suite while
             # still exercising each spec non-trivially.
+            # Apalache resolves modules only from the spec's directory, its
+            # own standard library, and the working directory; it ignores
+            # TLA-Library. Run it from the TLAPS library directory so specs
+            # that extend TLAPS parse, and pass every path absolutely.
             apalache = subprocess.run(
                 apalache_launcher + [
                     'check',
                     '--length=5',
-                    f'--config={model_path}',
-                    module_path
+                    f'--out-dir={abspath("_apalache-out")}',
+                    f'--config={abspath(model_path)}',
+                    abspath(module_path)
                 ],
+                cwd=tlapm_lib_path,
                 timeout=hard_timeout_in_seconds,
                 stdout=subprocess.PIPE,
                 stderr=subprocess.STDOUT,

specifications/ewd840/APSyncTerminationDetection.cfg

@@ -4,4 +4,5 @@ INVARIANT
   TypeOK
   TDCorrect
 
-SPECIFICATION Spec
+INIT Init
+NEXT Next

specifications/ewd840/EWD840.tla

@@ -5,7 +5,8 @@
 (* Derivation of a termination detection algorithm for distributed         *)
 (* computations (with W.H.J.Feijen and A.J.M. van Gasteren).               *)
 (***************************************************************************)
-EXTENDS Naturals
+\* TLAPS is needed for instantiating SyncTerminationDetection, see https://github.com/tlaplus/tlapm/issues/250
+EXTENDS Naturals, TLAPS
 
 CONSTANT N
 ASSUME NAssumption == N \in Nat \ {0}

specifications/ewd840/EWD840_proof.tla

@@ -281,8 +281,10 @@ BY Live, TypeCorrect, Invariant, PTL DEF Spec
 (* Note that the parameters of the module SyncTerminationDetection are     *)
 (* instantiated by the symbols of the same name in the present module.     *)
 (***************************************************************************)
+TDP == INSTANCE SyncTerminationDetection_proof
+
 THEOREM Spec => TD!Spec
-<1>. USE DEF Node, TD!Node
+<1>. USE DEF Node, TD!Node, TDP!Node
 <1>1. Init => TD!Init
   BY DEF Init, TD!Init, terminationDetected
 <1>2. TypeOK /\ Inv /\ [Next]_vars => [TD!Next]_TD!vars
@@ -299,18 +301,19 @@ THEOREM Spec => TD!Spec
     BY <2>4 DEF Deactivate, TD!Next, TD!Terminate, TD!terminated
   <2>. QED  BY <2>1, <2>2, <2>3, <2>4 DEF Next, System, Environment
 <1>3. []TypeOK /\ []Inv /\ [][Next]_vars /\ WF_vars(System)
-      => WF_TD!vars(TD!DetectTermination)
+      => TDP!Fair
   <2>. SUFFICES /\ []TypeOK /\ []Inv /\ [][Next]_vars /\ WF_vars(System)
-                /\ []ENABLED <<TD!DetectTermination>>_TD!vars
+                /\ <>[](TDP!terminated /\ ~terminationDetected)
                 => FALSE 
-    BY PTL
-  <2>1. TypeOK /\ ENABLED <<TD!DetectTermination>>_TD!vars
-        => terminated /\ ~terminationDetected
-    BY ExpandENABLED 
-       DEF TypeOK, TD!DetectTermination, TD!vars, terminated, TD!terminated, terminationDetected
+    <3>. TypeOK => TDP!TypeOK
+      BY DEF TypeOK, TDP!TypeOK, terminationDetected
+    <3>. QED  BY TDP!Fairness, PTL
+  <2>1. TDP!terminated => terminated
+    BY DEF TDP!terminated, terminated
   <2>. QED BY <2>1, Live, PTL DEF Liveness
 <1>. QED  
-  BY <1>1, <1>2, <1>3, TypeCorrect, Invariant, PTL DEF Spec, TD!Spec
+  BY <1>1, <1>2, <1>3, TypeCorrect, Invariant, PTL DEF Spec, TD!Spec, TD!Fair, TDP!Fair, 
+     TD!vars, TDP!vars, TD!DetectTermination, TDP!DetectTermination, TD!terminated, TDP!terminated
 =============================================================================
 \* Modification History
 \* Created Mon Sep 09 11:33:10 CEST 2013 by merz

specifications/ewd840/SyncTerminationDetection.tla

@@ -50,7 +50,8 @@ Next ==
   \/ DetectTermination
 
 vars == <<active, terminationDetected>>
-Spec == Init /\ [][Next]_vars /\ WF_vars(DetectTermination)
+Fair == WF_vars(DetectTermination)
+Spec == Init /\ [][Next]_vars /\ Fair
 
 ------------------------------------------------------------------------------
 (* Correctness properties *)

specifications/ewd840/SyncTerminationDetection_proof.tla

@@ -39,6 +39,11 @@ LEMMA Enabled_ST ==
     PROVE (ENABLED <<DetectTermination>>_vars) <=> terminated /\ ~terminationDetected
 BY ExpandENABLED DEF TypeOK, DetectTermination, terminated, vars
 
+LEMMA Fairness ==
+    ASSUME []TypeOK
+    PROVE  Fair <=> (<>[](terminated /\ ~terminationDetected) => []<><<DetectTermination>>_vars)
+BY Enabled_ST, PTL DEF Fair
+
 (****************************************************************************)
 (* Proving liveness is easy since a single occurrence of the helpful action *)
 (* DetectTermination leads to the desired state.                            *)
@@ -52,6 +57,6 @@ THEOREM Live == Spec => Liveness
   BY DEF TypeOK, DetectTermination
 <1>3. TypeOK /\ P => ENABLED <<DetectTermination>>_vars
   BY Enabled_ST
-<1>. QED  BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec, Liveness
+<1>. QED  BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec, Fair, Liveness
 
 =============================================================================

specifications/ewd998/AsyncTerminationDetection.tla

@@ -65,8 +65,9 @@ Next ==
   \/ DetectTermination
 
 vars == <<active, pending, terminationDetected>>
+Fair == WF_vars(DetectTermination)
 Spec == /\ Init /\ [][Next]_vars
-        /\ WF_vars(DetectTermination)
+        /\ Fair
            \* reasonable but not necessary for detecting termination
            \* /\ \A i \in Node : WF_vars(Wakeup(i))
 

specifications/ewd998/AsyncTerminationDetection_proof.tla

@@ -43,6 +43,11 @@ LEMMA EnabledDT ==
   PROVE  (ENABLED <<DetectTermination>>_vars) <=> (terminated /\ ~ terminationDetected)
 BY ExpandENABLED DEF TypeOK, DetectTermination, terminated, vars
 
+LEMMA Fairness ==
+  ASSUME []TypeOK
+  PROVE  Fair <=> (<>[](terminated /\ ~ terminationDetected) => []<><<DetectTermination>>_vars)
+BY EnabledDT, PTL DEF Fair
+
 THEOREM Liveness == Spec => Live
 <1>. DEFINE P == terminated /\ ~ terminationDetected
             Q == terminationDetected
@@ -52,7 +57,7 @@ THEOREM Liveness == Spec => Live
   BY DEF DetectTermination
 <1>3. TypeOK /\ P => ENABLED <<DetectTermination>>_vars
   BY EnabledDT
-<1>. QED  BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec, Live
+<1>. QED  BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec, Fair, Live
 
 =============================================================================
 \* Modification History

specifications/ewd998/EWD998.tla

@@ -5,7 +5,8 @@
 (* Shmuel Safra's version of termination detection.                        *)
 (* https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF                  *)
 (***************************************************************************)
-EXTENDS Integers, FiniteSets, Functions
+\* TLAPS is needed for instantiating AsyncTerminationDetection, see https://github.com/tlaplus/tlapm/issues/250
+EXTENDS Integers, FiniteSets, Functions, TLAPS
 
 CONSTANT
     \* @type: Int;

specifications/ewd998/EWD998_proof.tla

@@ -759,8 +759,10 @@ BY TypeCorrect, Invariance, Live, PTL DEF Spec
 (* In order to reuse lemmas about the high-level specification, we         *)
 (* instantiate the corresponding proof module.                             *)
 (***************************************************************************)
-LEMMA NodeIsNode == TD!Node = Node
-BY DEF Node, TD!Node
+TDP == INSTANCE AsyncTerminationDetection_proof
+
+LEMMA NodeIsNode == TD!Node = Node /\ TDP!Node = Node
+BY DEF Node, TD!Node, TDP!Node
 
 THEOREM Refinement == Spec => TD!Spec
 <1>. USE NodeIsNode
@@ -841,25 +843,27 @@ THEOREM Refinement == Spec => TD!Spec
   <2>7. QED
     BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6 DEF Environment, Next, System
 <1>4. []TypeOK /\ []Inv /\ [][Next]_vars /\ WF_vars(System) 
-         => WF_(TD!vars)(TD!DetectTermination)
+         => TDP!Fair
   <2>1. SUFFICES /\ []TypeOK /\ []Inv /\ [][Next]_vars /\ WF_vars(System)
-                 /\ []ENABLED <<TD!DetectTermination>>_(TD!vars)
+                 /\ <>[](TDP!terminated /\ ~ terminationDetected)
                  => FALSE
-    BY PTL
-  <2>2. TypeOK /\ ENABLED <<TD!DetectTermination>>_(TD!vars) 
-           => Termination /\ ~ terminationDetected
-    <3>. SUFFICES ASSUME TypeOK, ENABLED <<TD!DetectTermination>>_(TD!vars)
-                  PROVE  Termination /\ ~ terminationDetected
+    <3>. TypeOK => TDP!TypeOK
+      BY DEF TypeOK, TDP!TypeOK, terminationDetected
+    <3>. QED  BY TDP!Fairness, PTL
+  <2>2. TypeOK /\ TDP!terminated => Termination
+    <3>. SUFFICES ASSUME TypeOK, TDP!terminated
+                  PROVE  Termination
       OBVIOUS
-    <3>1. TD!terminated /\ ~ terminationDetected
-      BY ExpandENABLED DEF TD!DetectTermination, TD!vars, terminationDetected
-    <3>2. \A n \in Node : ~ active[n] /\ pending[n] = 0
-      BY <3>1 DEF TD!terminated
-    <3>3. B = 0
-      BY <3>2, SumZero, pending \in [Node -> Int] DEF TypeOK, B
-    <3>. QED  BY <3>1, <3>2, <3>3 DEF Termination
+    <3>1. \A n \in Node : ~ active[n] /\ pending[n] = 0
+      BY DEF TDP!terminated
+    <3>2. B = 0
+      BY <3>1, SumZero, pending \in [Node -> Int] DEF TypeOK, B
+    <3>. QED  BY <3>1, <3>2 DEF Termination
   <2>. QED  BY <2>2, Live, TypeCorrect, Invariance, PTL DEF Liveness
-<1>. QED  BY <1>1, <1>2, <1>4, TypeCorrect, Invariance, PTL DEF Spec, TD!Spec
+<1>. QED  
+  BY <1>1, <1>2, <1>4, TypeCorrect, Invariance, PTL DEF Spec, TD!Spec, TD!Fair, TDP!Fair,
+     TD!vars, TDP!vars, TD!DetectTermination, TDP!DetectTermination, TD!terminated, TDP!terminated,
+     Node, TD!Node, TDP!Node
 
 (***************************************************************************)
 (* The (state-level) safety invariant `TerminationDetection`:              *)