Skip to content

Commit 73a56dc

Browse files
lemmylemmy
committed
Add operators to the Relation module.
* Is[Strictly]PartiallyOrdered * Is[Stringly]TotallyOrdered * Is*Under(op(_,_), S) Signed-off-by: Markus Alexander Kuppe <[email protected]>
1 parent 9c13c11 commit 73a56dc

File tree

4 files changed

+126
-4
lines changed

4 files changed

+126
-4
lines changed

‎README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ The Modules
2525
| [`HTML.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/HTML.tla) | Format strings into HTML tags | | [@afonsof](https://github.com/afonsof) |
2626
| [`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) |
2727
| [`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) |
28-
| [`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) |
28+
| [`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) |
2929
| [`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) |
3030
| [`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) |
3131
| [`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) |

‎modules/Relation.tla

Lines changed: 68 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
----------------------------- MODULE Relation ------------------------------
22
LOCAL INSTANCE Naturals
3-
LOCAL INSTANCE FiniteSets
3+
LOCAL INSTANCE FiniteSets \* TODO Consider moving to a more specific module.
44

55
(***************************************************************************)
66
(* This module provides some basic operations on relations, represented *)
@@ -12,26 +12,92 @@ LOCAL INSTANCE FiniteSets
1212
(***************************************************************************)
1313
IsReflexive(R, S) == \A x \in S : R[x,x]
1414

15+
IsReflexiveUnder(op(_,_), S) ==
16+
IsReflexive([<<x,y>> \in S \X S |-> op(x,y)], S)
17+
1518
(***************************************************************************)
1619
(* Is the relation R irreflexive over set S? *)
1720
(***************************************************************************)
1821
IsIrreflexive(R, S) == \A x \in S : ~ R[x,x]
1922

23+
IsIrreflexiveUnder(op(_,_), S) ==
24+
IsIrreflexive([<<x,y>> \in S \X S |-> op(x,y)], S)
25+
2026
(***************************************************************************)
2127
(* Is the relation R symmetric over set S? *)
2228
(***************************************************************************)
2329
IsSymmetric(R, S) == \A x,y \in S : R[x,y] <=> R[y,x]
2430

31+
IsSymmetricUnder(op(_,_), S) ==
32+
IsSymmetric([<<x,y>> \in S \X S |-> op(x,y)], S)
33+
34+
(***************************************************************************)
35+
(* Is the relation R antisymmetric over set S? *)
36+
(***************************************************************************)
37+
IsAntiSymmetric(R, S) == \A x,y \in S : R[x,y] /\ R[y,x] => x=y
38+
39+
IsAntiSymmetricUnder(op(_,_), S) ==
40+
IsAntiSymmetric([<<x,y>> \in S \X S |-> op(x,y)], S)
41+
2542
(***************************************************************************)
2643
(* Is the relation R asymmetric over set S? *)
2744
(***************************************************************************)
2845
IsAsymmetric(R, S) == \A x,y \in S : ~(R[x,y] /\ R[y,x])
2946

47+
IsAsymmetricUnder(op(_,_), S) ==
48+
IsAsymmetric([<<x,y>> \in S \X S |-> op(x,y)], S)
49+
3050
(***************************************************************************)
3151
(* Is the relation R transitive over set S? *)
3252
(***************************************************************************)
3353
IsTransitive(R, S) == \A x,y,z \in S : R[x,y] /\ R[y,z] => R[x,z]
3454

55+
IsTransitiveUnder(op(_,_), S) ==
56+
IsTransitive([<<x,y>> \in S \X S |-> op(x,y)], S)
57+
58+
(***************************************************************************)
59+
(* Is the set S strictly partially ordered under the (binary) relation R? *)
60+
(***************************************************************************)
61+
IsStrictlyPartiallyOrdered(R, S) ==
62+
/\ IsIrreflexive(R, S)
63+
/\ IsAntiSymmetric(R, S)
64+
/\ IsTransitive(R, S)
65+
66+
IsStrictlyPartiallyOrderedUnder(op(_,_), S) ==
67+
IsStrictlyPartiallyOrdered([<<x,y>> \in S \X S |-> op(x,y)], S)
68+
69+
(***************************************************************************)
70+
(* Is the set S (weakly) partially ordered under the (binary) relation R? *)
71+
(***************************************************************************)
72+
IsPartiallyOrdered(R, S) ==
73+
/\ IsReflexive(R, S)
74+
/\ IsAntiSymmetric(R, S)
75+
/\ IsTransitive(R, S)
76+
77+
IsPartiallyOrderedUnder(op(_,_), S) ==
78+
IsPartiallyOrdered([<<x,y>> \in S \X S |-> op(x,y)], S)
79+
80+
(***************************************************************************)
81+
(* Is the set S strictly totally ordered under the (binary) relation R? *)
82+
(***************************************************************************)
83+
IsStrictlyTotallyOrdered(R, S) ==
84+
/\ IsStrictlyPartiallyOrdered(R, S)
85+
\* Trichotomy (R is irreflexive)
86+
/\ \A x,y \in S : x # y => R[x,y] \/ R[y,x]
87+
88+
IsStrictlyTotallyOrderedUnder(op(_,_), S) ==
89+
IsStrictlyTotallyOrdered([<<x,y>> \in S \X S |-> op(x,y)], S)
90+
91+
(***************************************************************************)
92+
(* Is the set S totally ordered under the (binary) relation R? *)
93+
(***************************************************************************)
94+
IsTotallyOrdered(R, S) ==
95+
/\ IsPartiallyOrdered(R, S)
96+
/\ \A x,y \in S : R[x,y] \/ R[y,x]
97+
98+
IsTotallyOrderedUnder(op(_,_), S) ==
99+
IsTotallyOrdered([<<x,y>> \in S \X S |-> op(x,y)], S)
100+
35101
(***************************************************************************)
36102
(* Compute the transitive closure of relation R over set S. *)
37103
(***************************************************************************)
@@ -60,5 +126,5 @@ IsConnected(R, S) ==
60126

61127
=============================================================================
62128
\* Modification History
63-
\* Last modified Sun Jun 14 15:32:47 CEST 2020 by merz
129+
\* Last modified Tues Sept 17 06:20:47 CEST 2024 by Markus Alexander Kuppe
64130
\* Created Tue Apr 26 10:24:07 CEST 2016 by merz

‎tests/AllTests.tla

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,8 @@
44
(* Add new tests (the ones with ASSUME statements) *)
55
(* to the comma-separated list of EXTENDS below. *)
66
(***************************************************)
7-
EXTENDS SequencesExtTests,
7+
EXTENDS RelationTests,
8+
SequencesExtTests,
89
SVGTests,
910
JsonTests,
1011
BitwiseTests,

‎tests/RelationTests.tla

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
------------------------- MODULE RelationTests -------------------------
2+
EXTENDS Relation, Naturals, TLC
3+
4+
ASSUME LET T == INSTANCE TLC IN T!PrintT("RelationTests")
5+
6+
S == {0, 1, 2, 3}
7+
8+
ASSUME IsReflexiveUnder(=, S)
9+
ASSUME ~IsReflexiveUnder(<, S)
10+
ASSUME IsReflexiveUnder(<=, S)
11+
12+
ASSUME ~IsIrreflexiveUnder(=, S)
13+
ASSUME IsIrreflexiveUnder(<, S)
14+
ASSUME ~IsIrreflexiveUnder(<=, S)
15+
16+
ASSUME IsSymmetricUnder(=, S)
17+
ASSUME ~IsSymmetricUnder(<, S)
18+
ASSUME ~IsSymmetricUnder(<=, S)
19+
20+
ASSUME LET R == [<<x,y>> \in S \X S |-> <(x,y)]
21+
T == <<0,2>> :> TRUE @@ <<2,0>> :> TRUE @@ R
22+
IN ~IsAntiSymmetric(T, S)
23+
24+
ASSUME IsAntiSymmetricUnder(=, S)
25+
ASSUME IsAntiSymmetricUnder(<, S)
26+
ASSUME IsAntiSymmetricUnder(<=, S)
27+
28+
ASSUME ~IsAsymmetricUnder(=, S)
29+
ASSUME IsAsymmetricUnder(<, S)
30+
ASSUME ~IsAsymmetricUnder(<=, S)
31+
32+
ASSUME LET R == [<<x,y>> \in S \X S |-> <(x,y)]
33+
T == <<0,2>> :> FALSE @@ R
34+
IN ~IsTransitive(T, S)
35+
36+
ASSUME IsTransitiveUnder(=, S)
37+
ASSUME IsTransitiveUnder(<, S)
38+
ASSUME IsTransitiveUnder(<=, S)
39+
40+
ASSUME ~IsStrictlyPartiallyOrderedUnder(=, S)
41+
ASSUME IsStrictlyPartiallyOrderedUnder(<, S)
42+
ASSUME ~IsStrictlyPartiallyOrderedUnder(<=, S)
43+
44+
ASSUME IsPartiallyOrderedUnder(=, S)
45+
ASSUME ~IsPartiallyOrderedUnder(<, S)
46+
ASSUME IsPartiallyOrderedUnder(<=, S)
47+
48+
ASSUME ~IsStrictlyTotallyOrderedUnder(=, S)
49+
ASSUME IsStrictlyTotallyOrderedUnder(<, S)
50+
ASSUME ~IsStrictlyTotallyOrderedUnder(<=, S)
51+
52+
ASSUME ~IsTotallyOrderedUnder(=, S)
53+
ASSUME ~IsTotallyOrderedUnder(<, S)
54+
ASSUME IsTotallyOrderedUnder(<=, S)
55+
=============================================================================

0 commit comments

Comments
 (0)