From 52947075741dfccf84a669fb74efae55a82ac926 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Thu, 26 Feb 2026 12:16:28 +0100 Subject: [PATCH 1/2] make syntax compatible with TLAPM Signed-off-by: Stephan Merz --- modules/Graphs.tla | 12 ++++----- modules/Relation.tla | 45 +++++++++++++++++++++++---------- tests/UndirectedGraphsTests.tla | 4 +-- 3 files changed, 39 insertions(+), 22 deletions(-) diff --git a/modules/Graphs.tla b/modules/Graphs.tla index 62ee31e..cca38a3 100644 --- a/modules/Graphs.tla +++ b/modules/Graphs.tla @@ -157,7 +157,9 @@ AllPredecessors(G, S) == UNION {Predecessors(G, n): n \in S} (***************************************************************************) Ancestors(G, n) == LET EdgeRelation == - [<> \in G.node \X G.node |-> <> \in G.edge] +\* restore when TLAPS supports this syntax +\* [<> \in G.node \X G.node |-> <> \in G.edge] + [p \in G.node \X G.node |-> <> \in G.edge] IN { m \in G.node : TransitiveClosure(EdgeRelation, G.node)[m, n] } (***************************************************************************) @@ -169,7 +171,9 @@ Ancestors(G, n) == (***************************************************************************) Descendants(G, n) == LET EdgeRelation == - [<> \in G.node \X G.node |-> <> \in G.edge] +\* restore when TLAPS supports this syntax +\* [<> \in G.node \X G.node |-> <> \in G.edge] + [p \in G.node \X G.node |-> <> \in G.edge] IN { m \in G.node : TransitiveClosure(EdgeRelation, G.node)[n, m] } (*************************************************************) @@ -218,7 +222,3 @@ EmptyGraph == [node |-> {}, edge |-> {}] (************************************************************************) Graphs(S) == [node: {S}, edge: SUBSET (S \X S)] ============================================================================= -\* Modification History -\* Last modified Sun Mar 06 18:10:34 CET 2022 by Stephan Merz -\* Last modified Tue Dec 21 15:55:45 PST 2021 by Markus Kuppe -\* Created Tue Jun 18 11:44:08 PST 2002 by Leslie Lamport \ No newline at end of file diff --git a/modules/Relation.tla b/modules/Relation.tla index 123630f..bd48f2f 100644 --- a/modules/Relation.tla +++ b/modules/Relation.tla @@ -1,6 +1,6 @@ ----------------------------- MODULE Relation ------------------------------ LOCAL INSTANCE Naturals -LOCAL INSTANCE FiniteSets \* TODO Consider moving to a more specific module. +LOCAL INSTANCE FiniteSets (***************************************************************************) (* This module provides some basic operations on relations, represented *) @@ -33,7 +33,9 @@ LOCAL INSTANCE FiniteSets \* TODO Consider moving to a more specific module. IsReflexive(R, S) == \A x \in S : R[x,x] IsReflexiveUnder(op(_,_), S) == - IsReflexive([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsReflexive([<> \in S \X S |-> op(x,y)], S) + IsReflexive([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Is the relation R irreflexive over set S? *) @@ -48,7 +50,9 @@ IsReflexiveUnder(op(_,_), S) == IsIrreflexive(R, S) == \A x \in S : ~ R[x,x] IsIrreflexiveUnder(op(_,_), S) == - IsIrreflexive([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsIrreflexive([<> \in S \X S |-> op(x,y)], S) + IsIrreflexive([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Is the relation R symmetric over set S? *) @@ -62,7 +66,9 @@ IsIrreflexiveUnder(op(_,_), S) == IsSymmetric(R, S) == \A x,y \in S : R[x,y] <=> R[y,x] IsSymmetricUnder(op(_,_), S) == - IsSymmetric([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsSymmetric([<> \in S \X S |-> op(x,y)], S) + IsSymmetric([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Is the relation R antisymmetric over set S? *) @@ -77,7 +83,9 @@ IsSymmetricUnder(op(_,_), S) == IsAntiSymmetric(R, S) == \A x,y \in S : R[x,y] /\ R[y,x] => x=y IsAntiSymmetricUnder(op(_,_), S) == - IsAntiSymmetric([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsAntiSymmetric([<> \in S \X S |-> op(x,y)], S) + IsAntiSymmetric([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Is the relation R asymmetric over set S? *) @@ -92,7 +100,9 @@ IsAntiSymmetricUnder(op(_,_), S) == IsAsymmetric(R, S) == \A x,y \in S : ~(R[x,y] /\ R[y,x]) IsAsymmetricUnder(op(_,_), S) == - IsAsymmetric([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsAsymmetric([<> \in S \X S |-> op(x,y)], S) + IsAsymmetric([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Is the relation R transitive over set S? *) @@ -107,7 +117,9 @@ IsAsymmetricUnder(op(_,_), S) == IsTransitive(R, S) == \A x,y,z \in S : R[x,y] /\ R[y,z] => R[x,z] IsTransitiveUnder(op(_,_), S) == - IsTransitive([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsTransitive([<> \in S \X S |-> op(x,y)], S) + IsTransitive([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Is the set S strictly partially ordered under the (binary) relation R? *) @@ -125,7 +137,9 @@ IsStrictlyPartiallyOrdered(R, S) == /\ IsTransitive(R, S) IsStrictlyPartiallyOrderedUnder(op(_,_), S) == - IsStrictlyPartiallyOrdered([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsStrictlyPartiallyOrdered([<> \in S \X S |-> op(x,y)], S) + IsStrictlyPartiallyOrdered([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Is the set S (weakly) partially ordered under the (binary) relation R? *) @@ -143,7 +157,9 @@ IsPartiallyOrdered(R, S) == /\ IsTransitive(R, S) IsPartiallyOrderedUnder(op(_,_), S) == - IsPartiallyOrdered([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsPartiallyOrdered([<> \in S \X S |-> op(x,y)], S) + IsPartiallyOrdered([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Is the set S strictly totally ordered under the (binary) relation R? *) @@ -160,7 +176,9 @@ IsStrictlyTotallyOrdered(R, S) == /\ \A x,y \in S : x # y => R[x,y] \/ R[y,x] IsStrictlyTotallyOrderedUnder(op(_,_), S) == - IsStrictlyTotallyOrdered([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsStrictlyTotallyOrdered([<> \in S \X S |-> op(x,y)], S) + IsStrictlyTotallyOrdered([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Is the set S totally ordered under the (binary) relation R? *) @@ -175,7 +193,9 @@ IsTotallyOrdered(R, S) == /\ \A x,y \in S : R[x,y] \/ R[y,x] IsTotallyOrderedUnder(op(_,_), S) == - IsTotallyOrdered([<> \in S \X S |-> op(x,y)], S) +\* restore the following when TLAPS accepts this syntax +\* IsTotallyOrdered([<> \in S \X S |-> op(x,y)], S) + IsTotallyOrdered([p \in S \X S |-> op(p[1], p[2])], S) (***************************************************************************) (* Compute the transitive closure of relation R over set S. *) @@ -204,6 +224,3 @@ IsConnected(R, S) == IN \A x,y \in S : rtrcl[x,y] ============================================================================= -\* Modification History -\* Last modified Tues Sept 17 06:20:47 CEST 2024 by Markus Alexander Kuppe -\* Created Tue Apr 26 10:24:07 CEST 2016 by merz diff --git a/tests/UndirectedGraphsTests.tla b/tests/UndirectedGraphsTests.tla index 9773875..86dda82 100644 --- a/tests/UndirectedGraphsTests.tla +++ b/tests/UndirectedGraphsTests.tla @@ -1,4 +1,4 @@ -------------------------- MODULE GraphsTests ------------------------- +------------------------- MODULE UndirectedGraphsTests ------------------- EXTENDS UndirectedGraphs, TLCExt ASSUME LET T == INSTANCE TLC IN T!PrintT("UndirectedGraphsTests") @@ -14,7 +14,7 @@ ASSUME LET G == [edge|-> {{1,2}}, node |-> {1,2,3}] /\ AreConnectedIn(1, 2, G) /\ ~ AreConnectedIn(1, 3, G) -AssertEq(ConnectedComponents([edge|-> {{1,2}}, node |-> {1,2,3}]), +ASSUME AssertEq(ConnectedComponents([edge|-> {{1,2}}, node |-> {1,2,3}]), {{1,2}, {3}}) ASSUME LET G == [node |-> {1,2,3,4,5}, edge |-> {{1,3}, {1,4}, {2,3}, {2,4}, {3,5}, {4,5}}] From 7675a70c00b58b9759ccf53d172c0eb434b99547 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Thu, 26 Feb 2026 18:18:50 +0100 Subject: [PATCH 2/2] reformulation of comment on syntax not supported by TLAPS Signed-off-by: Stephan Merz --- modules/Graphs.tla | 6 ++++-- modules/Relation.tla | 30 ++++++++++++++++++++---------- 2 files changed, 24 insertions(+), 12 deletions(-) diff --git a/modules/Graphs.tla b/modules/Graphs.tla index cca38a3..72e49b1 100644 --- a/modules/Graphs.tla +++ b/modules/Graphs.tla @@ -157,7 +157,8 @@ AllPredecessors(G, S) == UNION {Predecessors(G, n): n \in S} (***************************************************************************) Ancestors(G, n) == LET EdgeRelation == -\* restore when TLAPS supports this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* [<> \in G.node \X G.node |-> <> \in G.edge] [p \in G.node \X G.node |-> <> \in G.edge] IN { m \in G.node : TransitiveClosure(EdgeRelation, G.node)[m, n] } @@ -171,7 +172,8 @@ Ancestors(G, n) == (***************************************************************************) Descendants(G, n) == LET EdgeRelation == -\* restore when TLAPS supports this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* [<> \in G.node \X G.node |-> <> \in G.edge] [p \in G.node \X G.node |-> <> \in G.edge] IN { m \in G.node : TransitiveClosure(EdgeRelation, G.node)[n, m] } diff --git a/modules/Relation.tla b/modules/Relation.tla index bd48f2f..0820cbf 100644 --- a/modules/Relation.tla +++ b/modules/Relation.tla @@ -33,7 +33,8 @@ LOCAL INSTANCE FiniteSets IsReflexive(R, S) == \A x \in S : R[x,x] IsReflexiveUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsReflexive([<> \in S \X S |-> op(x,y)], S) IsReflexive([p \in S \X S |-> op(p[1], p[2])], S) @@ -50,7 +51,8 @@ IsReflexiveUnder(op(_,_), S) == IsIrreflexive(R, S) == \A x \in S : ~ R[x,x] IsIrreflexiveUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsIrreflexive([<> \in S \X S |-> op(x,y)], S) IsIrreflexive([p \in S \X S |-> op(p[1], p[2])], S) @@ -66,7 +68,8 @@ IsIrreflexiveUnder(op(_,_), S) == IsSymmetric(R, S) == \A x,y \in S : R[x,y] <=> R[y,x] IsSymmetricUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsSymmetric([<> \in S \X S |-> op(x,y)], S) IsSymmetric([p \in S \X S |-> op(p[1], p[2])], S) @@ -83,7 +86,8 @@ IsSymmetricUnder(op(_,_), S) == IsAntiSymmetric(R, S) == \A x,y \in S : R[x,y] /\ R[y,x] => x=y IsAntiSymmetricUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsAntiSymmetric([<> \in S \X S |-> op(x,y)], S) IsAntiSymmetric([p \in S \X S |-> op(p[1], p[2])], S) @@ -100,7 +104,8 @@ IsAntiSymmetricUnder(op(_,_), S) == IsAsymmetric(R, S) == \A x,y \in S : ~(R[x,y] /\ R[y,x]) IsAsymmetricUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsAsymmetric([<> \in S \X S |-> op(x,y)], S) IsAsymmetric([p \in S \X S |-> op(p[1], p[2])], S) @@ -117,7 +122,8 @@ IsAsymmetricUnder(op(_,_), S) == IsTransitive(R, S) == \A x,y,z \in S : R[x,y] /\ R[y,z] => R[x,z] IsTransitiveUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsTransitive([<> \in S \X S |-> op(x,y)], S) IsTransitive([p \in S \X S |-> op(p[1], p[2])], S) @@ -137,7 +143,8 @@ IsStrictlyPartiallyOrdered(R, S) == /\ IsTransitive(R, S) IsStrictlyPartiallyOrderedUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsStrictlyPartiallyOrdered([<> \in S \X S |-> op(x,y)], S) IsStrictlyPartiallyOrdered([p \in S \X S |-> op(p[1], p[2])], S) @@ -157,7 +164,8 @@ IsPartiallyOrdered(R, S) == /\ IsTransitive(R, S) IsPartiallyOrderedUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsPartiallyOrdered([<> \in S \X S |-> op(x,y)], S) IsPartiallyOrdered([p \in S \X S |-> op(p[1], p[2])], S) @@ -176,7 +184,8 @@ IsStrictlyTotallyOrdered(R, S) == /\ \A x,y \in S : x # y => R[x,y] \/ R[y,x] IsStrictlyTotallyOrderedUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsStrictlyTotallyOrdered([<> \in S \X S |-> op(x,y)], S) IsStrictlyTotallyOrdered([p \in S \X S |-> op(p[1], p[2])], S) @@ -193,7 +202,8 @@ IsTotallyOrdered(R, S) == /\ \A x,y \in S : R[x,y] \/ R[y,x] IsTotallyOrderedUnder(op(_,_), S) == -\* restore the following when TLAPS accepts this syntax +\* revert to the following syntax once TLAPS uses SANY +\* (https://github.com/tlaplus/tlapm/issues/213) \* IsTotallyOrdered([<> \in S \X S |-> op(x,y)], S) IsTotallyOrdered([p \in S \X S |-> op(p[1], p[2])], S)