From 73a56dcd77042c72d72b1a6811aaa884f85573f8 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 11 Sep 2024 18:16:57 -0700 Subject: [PATCH] Add operators to the Relation module. * Is[Strictly]PartiallyOrdered * Is[Stringly]TotallyOrdered * Is*Under(op(_,_), S) Signed-off-by: Markus Alexander Kuppe --- README.md | 2 +- modules/Relation.tla | 70 +++++++++++++++++++++++++++++++++++++++-- tests/AllTests.tla | 3 +- tests/RelationTests.tla | 55 ++++++++++++++++++++++++++++++++ 4 files changed, 126 insertions(+), 4 deletions(-) create mode 100644 tests/RelationTests.tla diff --git a/README.md b/README.md index 1a5bdc1..f59ccfa 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,7 @@ The Modules | [`HTML.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/HTML.tla) | Format strings into HTML tags | | [@afonsof](https://github.com/afonsof) | | [`IOUtils.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/IOUtils.tla) | Input/Output of TLA+ values & Spawn system commands from a spec. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/IOUtils.java) | [@lemmy](https://github.com/lemmy), [@lvanengelen](https://github.com/lvanengelen), [@afonsof](https://github.com/afonsof) | | [`Json.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Json.tla) | JSON serialization and deserialization into TLA+ values. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Json.java) | [@kuujo](https://github.com/kuujo), [@lemmy](https://github.com/lemmy), [@jobvs](https://github.com/jobvs), [@pfeodrippe](https://github.com/pfeodrippe) | -| [`Relation.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Relation.tla) | Basic operations on relations, represented as binary Boolean functions over some set S. | | [@muenchnerkindl](https://github.com/muenchnerkindl) | +| [`Relation.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Relation.tla) | Basic operations on relations, represented as binary Boolean functions over some set S. | | [@muenchnerkindl](https://github.com/muenchnerkindl), [@lemmy](https://github.com/lemmy) | | [`SequencesExt.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla) | Additional operators on sequences (e.g. `ToSet`, `Reverse`, `ReplaceAll`, `SelectInSeq`, etc.) | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/SequencesExt.java) | [@muenchnerkindl](https://github.com/muenchnerkindl), [@lemmy](https://github.com/lemmy), [@hwayne](https://github.com/hwayne), [@quicquid](https://github.com/quicquid), [@konnov](https://github.com/konnov), [@afonsof](https://github.com/afonsof) | | [`ShiViz.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/ShiViz.tla) | Visualize error-traces of multi-process PlusCal algorithms with an [Interactive Communication Graphs](https://bestchai.bitbucket.io/shiviz/). | | [@lemmy](https://github.com/lemmy) | | [`Statistics.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Statistics.tla) | Statistics operators (`ChiSquare`, etc.) | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Statistics.java) | [@lemmy](https://github.com/lemmy) | diff --git a/modules/Relation.tla b/modules/Relation.tla index e9299b2..55db3d9 100644 --- a/modules/Relation.tla +++ b/modules/Relation.tla @@ -1,6 +1,6 @@ ----------------------------- MODULE Relation ------------------------------ LOCAL INSTANCE Naturals -LOCAL INSTANCE FiniteSets +LOCAL INSTANCE FiniteSets \* TODO Consider moving to a more specific module. (***************************************************************************) (* This module provides some basic operations on relations, represented *) @@ -12,26 +12,92 @@ LOCAL INSTANCE FiniteSets (***************************************************************************) IsReflexive(R, S) == \A x \in S : R[x,x] +IsReflexiveUnder(op(_,_), S) == + IsReflexive([<> \in S \X S |-> op(x,y)], S) + (***************************************************************************) (* Is the relation R irreflexive over set S? *) (***************************************************************************) IsIrreflexive(R, S) == \A x \in S : ~ R[x,x] +IsIrreflexiveUnder(op(_,_), S) == + IsIrreflexive([<> \in S \X S |-> op(x,y)], S) + (***************************************************************************) (* Is the relation R symmetric over set 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) + +(***************************************************************************) +(* Is the relation R antisymmetric over set 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) + (***************************************************************************) (* Is the relation R asymmetric over set 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) + (***************************************************************************) (* Is the relation R transitive over set 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) + +(***************************************************************************) +(* Is the set S strictly partially ordered under the (binary) relation R? *) +(***************************************************************************) +IsStrictlyPartiallyOrdered(R, S) == + /\ IsIrreflexive(R, S) + /\ IsAntiSymmetric(R, S) + /\ IsTransitive(R, S) + +IsStrictlyPartiallyOrderedUnder(op(_,_), S) == + IsStrictlyPartiallyOrdered([<> \in S \X S |-> op(x,y)], S) + +(***************************************************************************) +(* Is the set S (weakly) partially ordered under the (binary) relation R? *) +(***************************************************************************) +IsPartiallyOrdered(R, S) == + /\ IsReflexive(R, S) + /\ IsAntiSymmetric(R, S) + /\ IsTransitive(R, S) + +IsPartiallyOrderedUnder(op(_,_), S) == + IsPartiallyOrdered([<> \in S \X S |-> op(x,y)], S) + +(***************************************************************************) +(* Is the set S strictly totally ordered under the (binary) relation R? *) +(***************************************************************************) +IsStrictlyTotallyOrdered(R, S) == + /\ IsStrictlyPartiallyOrdered(R, S) + \* Trichotomy (R is irreflexive) + /\ \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) + +(***************************************************************************) +(* Is the set S totally ordered under the (binary) relation R? *) +(***************************************************************************) +IsTotallyOrdered(R, S) == + /\ IsPartiallyOrdered(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) + (***************************************************************************) (* Compute the transitive closure of relation R over set S. *) (***************************************************************************) @@ -60,5 +126,5 @@ IsConnected(R, S) == ============================================================================= \* Modification History -\* Last modified Sun Jun 14 15:32:47 CEST 2020 by merz +\* 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/AllTests.tla b/tests/AllTests.tla index d04ba32..38b7ce2 100644 --- a/tests/AllTests.tla +++ b/tests/AllTests.tla @@ -4,7 +4,8 @@ (* Add new tests (the ones with ASSUME statements) *) (* to the comma-separated list of EXTENDS below. *) (***************************************************) -EXTENDS SequencesExtTests, +EXTENDS RelationTests, + SequencesExtTests, SVGTests, JsonTests, BitwiseTests, diff --git a/tests/RelationTests.tla b/tests/RelationTests.tla new file mode 100644 index 0000000..d4265c2 --- /dev/null +++ b/tests/RelationTests.tla @@ -0,0 +1,55 @@ +------------------------- MODULE RelationTests ------------------------- +EXTENDS Relation, Naturals, TLC + +ASSUME LET T == INSTANCE TLC IN T!PrintT("RelationTests") + +S == {0, 1, 2, 3} + +ASSUME IsReflexiveUnder(=, S) +ASSUME ~IsReflexiveUnder(<, S) +ASSUME IsReflexiveUnder(<=, S) + +ASSUME ~IsIrreflexiveUnder(=, S) +ASSUME IsIrreflexiveUnder(<, S) +ASSUME ~IsIrreflexiveUnder(<=, S) + +ASSUME IsSymmetricUnder(=, S) +ASSUME ~IsSymmetricUnder(<, S) +ASSUME ~IsSymmetricUnder(<=, S) + +ASSUME LET R == [<> \in S \X S |-> <(x,y)] + T == <<0,2>> :> TRUE @@ <<2,0>> :> TRUE @@ R + IN ~IsAntiSymmetric(T, S) + +ASSUME IsAntiSymmetricUnder(=, S) +ASSUME IsAntiSymmetricUnder(<, S) +ASSUME IsAntiSymmetricUnder(<=, S) + +ASSUME ~IsAsymmetricUnder(=, S) +ASSUME IsAsymmetricUnder(<, S) +ASSUME ~IsAsymmetricUnder(<=, S) + +ASSUME LET R == [<> \in S \X S |-> <(x,y)] + T == <<0,2>> :> FALSE @@ R + IN ~IsTransitive(T, S) + +ASSUME IsTransitiveUnder(=, S) +ASSUME IsTransitiveUnder(<, S) +ASSUME IsTransitiveUnder(<=, S) + +ASSUME ~IsStrictlyPartiallyOrderedUnder(=, S) +ASSUME IsStrictlyPartiallyOrderedUnder(<, S) +ASSUME ~IsStrictlyPartiallyOrderedUnder(<=, S) + +ASSUME IsPartiallyOrderedUnder(=, S) +ASSUME ~IsPartiallyOrderedUnder(<, S) +ASSUME IsPartiallyOrderedUnder(<=, S) + +ASSUME ~IsStrictlyTotallyOrderedUnder(=, S) +ASSUME IsStrictlyTotallyOrderedUnder(<, S) +ASSUME ~IsStrictlyTotallyOrderedUnder(<=, S) + +ASSUME ~IsTotallyOrderedUnder(=, S) +ASSUME ~IsTotallyOrderedUnder(<, S) +ASSUME IsTotallyOrderedUnder(<=, S) +=============================================================================