Add operators to the Relation module.

* IsComparable * IsPartiallyOrdered * IsTotallyOrdered * (ToRelation) Signed-off-by: Markus Alexander Kuppe <[email protected]>
tlaplus · Sep 16, 2024 · 1e2f2d4 · 1e2f2d4
1 parent 9c13c11
commit 1e2f2d4
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 2 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,12 +1,18 @@
 ----------------------------- 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    *)
 (* as binary Boolean functions over some set S.                            *)
 (***************************************************************************)
 
+(***************************************************************************)
+(* Given a binary operator op, return the relation it represents over set  *)
+(* S.                                                                      *)
+(***************************************************************************)
+ToRelation(op(_, _), S) == [x, y \in S |-> op(x,y)]
+
 (***************************************************************************)
 (* Is the relation R reflexive over S?                                     *)
 (***************************************************************************)
@@ -32,6 +38,27 @@ IsAsymmetric(R, S) == \A x,y \in S : ~(R[x,y] /\ R[y,x])
 (***************************************************************************)
 IsTransitive(R, S) == \A x,y,z \in S : R[x,y] /\ R[y,z] => R[x,z]
 
+(***************************************************************************)
+(* Determines if, for any two elements in S, the two elements are          *)
+(* comparable under the relation R.                                        *)
+(***************************************************************************)
+IsComparable(R, S) == \A x,y \in S : R[x,y] \/ R[y,x]
+
+(***************************************************************************)
+(* Is the set S partially ordered under the (binary) relation R?           *)
+(***************************************************************************)
+IsPartiallyOrdered(R, S) ==
+    /\ IsReflexive(R, S)
+    /\ IsTransitive(R, S)
+    /\ IsAsymmetric(R, S)
+
+(***************************************************************************)
+(* Is the set S totally ordered under the (binary) relation R?             *)
+(***************************************************************************)
+IsTotallyOrdered(R, S) ==
+    /\ IsPartiallyOrdered(R, S)
+    /\ IsComparable(R, S)
+
 (***************************************************************************)
 (* Compute the transitive closure of relation R over set S.                *)
 (***************************************************************************)