diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index e152fcb6..81c65efe 100644 --- a/.github/scripts/tla_utils.py +++ b/.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, diff --git a/specifications/ewd840/APSyncTerminationDetection.cfg b/specifications/ewd840/APSyncTerminationDetection.cfg index 1cef4991..1df90b72 100644 --- a/specifications/ewd840/APSyncTerminationDetection.cfg +++ b/specifications/ewd840/APSyncTerminationDetection.cfg @@ -4,4 +4,5 @@ INVARIANT TypeOK TDCorrect -SPECIFICATION Spec +INIT Init +NEXT Next diff --git a/specifications/ewd840/EWD840.tla b/specifications/ewd840/EWD840.tla index 36618d33..4b7d9fad 100644 --- a/specifications/ewd840/EWD840.tla +++ b/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} diff --git a/specifications/ewd840/EWD840_proof.tla b/specifications/ewd840/EWD840_proof.tla index 1cb8ef4f..f966ac88 100644 --- a/specifications/ewd840/EWD840_proof.tla +++ b/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!vars + /\ <>[](TDP!terminated /\ ~terminationDetected) => FALSE - BY PTL - <2>1. TypeOK /\ ENABLED <>_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 diff --git a/specifications/ewd840/SyncTerminationDetection.tla b/specifications/ewd840/SyncTerminationDetection.tla index 86c3dd6a..d663218f 100644 --- a/specifications/ewd840/SyncTerminationDetection.tla +++ b/specifications/ewd840/SyncTerminationDetection.tla @@ -50,7 +50,8 @@ Next == \/ DetectTermination vars == <> -Spec == Init /\ [][Next]_vars /\ WF_vars(DetectTermination) +Fair == WF_vars(DetectTermination) +Spec == Init /\ [][Next]_vars /\ Fair ------------------------------------------------------------------------------ (* Correctness properties *) diff --git a/specifications/ewd840/SyncTerminationDetection_proof.tla b/specifications/ewd840/SyncTerminationDetection_proof.tla index 008616e0..32d10215 100644 --- a/specifications/ewd840/SyncTerminationDetection_proof.tla +++ b/specifications/ewd840/SyncTerminationDetection_proof.tla @@ -39,6 +39,11 @@ LEMMA Enabled_ST == PROVE (ENABLED <>_vars) <=> terminated /\ ~terminationDetected BY ExpandENABLED DEF TypeOK, DetectTermination, terminated, vars +LEMMA Fairness == + ASSUME []TypeOK + PROVE Fair <=> (<>[](terminated /\ ~terminationDetected) => []<><>_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 <>_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 ============================================================================= diff --git a/specifications/ewd998/AsyncTerminationDetection.tla b/specifications/ewd998/AsyncTerminationDetection.tla index a28c7e84..093fc36d 100644 --- a/specifications/ewd998/AsyncTerminationDetection.tla +++ b/specifications/ewd998/AsyncTerminationDetection.tla @@ -65,8 +65,9 @@ Next == \/ DetectTermination vars == <> +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)) diff --git a/specifications/ewd998/AsyncTerminationDetection_proof.tla b/specifications/ewd998/AsyncTerminationDetection_proof.tla index 167da342..c8e9087e 100644 --- a/specifications/ewd998/AsyncTerminationDetection_proof.tla +++ b/specifications/ewd998/AsyncTerminationDetection_proof.tla @@ -43,6 +43,11 @@ LEMMA EnabledDT == PROVE (ENABLED <>_vars) <=> (terminated /\ ~ terminationDetected) BY ExpandENABLED DEF TypeOK, DetectTermination, terminated, vars +LEMMA Fairness == + ASSUME []TypeOK + PROVE Fair <=> (<>[](terminated /\ ~ terminationDetected) => []<><>_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 <>_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 diff --git a/specifications/ewd998/EWD998.tla b/specifications/ewd998/EWD998.tla index f0b172c8..cb5afe94 100644 --- a/specifications/ewd998/EWD998.tla +++ b/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; diff --git a/specifications/ewd998/EWD998_proof.tla b/specifications/ewd998/EWD998_proof.tla index 9515d554..ce14d036 100644 --- a/specifications/ewd998/EWD998_proof.tla +++ b/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!vars) + /\ <>[](TDP!terminated /\ ~ terminationDetected) => FALSE - BY PTL - <2>2. TypeOK /\ ENABLED <>_(TD!vars) - => Termination /\ ~ terminationDetected - <3>. SUFFICES ASSUME TypeOK, ENABLED <>_(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`: *)