From 2781401d87c6d88b566e0e6618335923630c6f87 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 30 Oct 2026 09:48:39 -0700 Subject: [PATCH 1/5] CI: run Apalache from the TLAPS library directory. Apalache looks up modules only in the directory of the spec, in its own standard library, and in its working directory. It ignores TLA-Library, and the classpath that lets TLC find TLAPS.tla does not reach it. A spec that extends TLAPS, or instantiates a module that does, therefore fails to parse with "Cannot find source file for module TLAPS". Running Apalache from the TLAPS library directory lets it find the module. All paths passed to Apalache are now absolute, and --out-dir keeps its output in _apalache-out at the root of the repository. https://github.com/tlaplus/Examples/actions/runs/41087129395/job/124171232756 Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- .github/scripts/tla_utils.py | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) 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, From ab4979e94e6ac08e0d86b02dd24cbdeda5b73e78 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 29 Oct 2026 11:17:45 -0700 Subject: [PATCH 2/5] EWD840: extend TLAPS to work around a tlapm bug. tlapm rewrites ENABLED into EnabledWrapper from the TLAPS module when it instantiates a module. If the module with the INSTANCE does not extend TLAPS, ExpandENABLED fails with "Operator EnabledWrapper not found". With tlapm#321, every instantiated WF contains ENABLED, so EWD840_proof hits this bug through TD == INSTANCE SyncTerminationDetection. https://github.com/tlaplus/tlapm/issues/250 https://github.com/tlaplus/tlapm/pull/321 Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- specifications/ewd840/EWD840.tla | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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} From affe2586a814074b1d046dc4014e5bb8754cfce5 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 29 Oct 2026 11:17:45 -0700 Subject: [PATCH 3/5] EWD840_proof: do not rely on instantiation distributing over WF. Instantiation does not distribute over ENABLED, and hence not over WF. The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination) matching the fairness conjunct of TD!Spec, which tlapm#321 no longer allows. SyncTerminationDetection now names its fairness condition Fair, and the proof derives TD!Fair from the new lemma SyncTerminationDetection_proof!Fairness. Apalache accepts only fairness written out in Spec, so APSyncTerminationDetection.cfg now names Init and Next instead. https://github.com/tlaplus/tlapm/issues/69 https://github.com/tlaplus/tlapm/pull/321 Co-authored-by: Stephan Merz <7482229+muenchnerkindl@users.noreply.github.com> Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- .../ewd840/APSyncTerminationDetection.cfg | 3 ++- specifications/ewd840/EWD840_proof.tla | 21 +++++++++++-------- .../ewd840/SyncTerminationDetection.tla | 3 ++- .../ewd840/SyncTerminationDetection_proof.tla | 7 ++++++- 4 files changed, 22 insertions(+), 12 deletions(-) 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_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 ============================================================================= From 61973f6d858580164470f46943b1bd96e2b71186 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 30 Oct 2026 09:52:30 -0700 Subject: [PATCH 4/5] EWD998: extend TLAPS to work around a tlapm bug. tlapm rewrites ENABLED into EnabledWrapper from the TLAPS module when it instantiates a module. If the module with the INSTANCE does not extend TLAPS, ExpandENABLED fails with "Operator EnabledWrapper not found". With tlapm#321, every instantiated WF contains ENABLED, so EWD998_proof hits this bug through TD == INSTANCE AsyncTerminationDetection. https://github.com/tlaplus/tlapm/issues/250 https://github.com/tlaplus/tlapm/pull/321 Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- specifications/ewd998/EWD998.tla | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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; From 8e320b301ae7a498bd2e2cfb7b654115bdb79fd0 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 30 Oct 2026 09:52:30 -0700 Subject: [PATCH 5/5] EWD998_proof: do not rely on instantiation distributing over WF. Instantiation does not distribute over ENABLED, and hence not over WF. The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination) matching the fairness conjunct of TD!Spec, which tlapm#321 no longer allows. AsyncTerminationDetection now names its fairness condition Fair, and the proof derives TD!Fair from the new lemma AsyncTerminationDetection_proof!Fairness. https://github.com/tlaplus/tlapm/issues/69 https://github.com/tlaplus/tlapm/pull/321 Co-authored-by: Stephan Merz <7482229+muenchnerkindl@users.noreply.github.com> Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- .../ewd998/AsyncTerminationDetection.tla | 3 +- .../AsyncTerminationDetection_proof.tla | 7 +++- specifications/ewd998/EWD998_proof.tla | 38 ++++++++++--------- 3 files changed, 29 insertions(+), 19 deletions(-) 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_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`: *)