Add operators to the Relation module.

* Is[Strictly]PartiallyOrdered * Is[Stringly]TotallyOrdered * Is*Under(op(_,_), S) Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
tlaplus · Sep 17, 2024 · 73a56dc · 73a56dc
1 parent 9c13c11
commit 73a56dc
Show file tree

Hide file tree

Showing 4 changed files with 126 additions and 4 deletions.
diff --git 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. | [&#10004;](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. | [&#10004;](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.) | [&#10004;](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.) | [&#10004;](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
@@ -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([<<x,y>> \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([<<x,y>> \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([<<x,y>> \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([<<x,y>> \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([<<x,y>> \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([<<x,y>> \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([<<x,y>> \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([<<x,y>> \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([<<x,y>> \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([<<x,y>> \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
@@ -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
@@ -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 == [<<x,y>> \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 == [<<x,y>> \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)
+=============================================================================