From c49b3a425fe85c085271912700faaba0fc0ab4d5 Mon Sep 17 00:00:00 2001
From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de>
Date: Fri, 27 Jun 2025 15:30:58 +0200
Subject: [PATCH] Also improve type inference of Relations.tla for TLA2B
---
.../de/tlc4b/standardModules/FunctionsAsRelations.tla | 6 ++++--
.../resources/de/tlc4b/standardModules/Relations.tla | 10 ++++++----
2 files changed, 10 insertions(+), 6 deletions(-)
diff --git a/src/main/resources/de/tlc4b/standardModules/FunctionsAsRelations.tla b/src/main/resources/de/tlc4b/standardModules/FunctionsAsRelations.tla
index 07cd0f0..326c7d0 100644
--- a/src/main/resources/de/tlc4b/standardModules/FunctionsAsRelations.tla
+++ b/src/main/resources/de/tlc4b/standardModules/FunctionsAsRelations.tla
@@ -1,8 +1,10 @@
------------------------ MODULE FunctionsAsRelations ----------------------------------
EXTENDS FiniteSets, Functions, TLC, Sequences
-LOCAL RelDom(f) == { <<x[1], x[2]>>[1] : x \in f } \* The domain of the function, syntax is weird to help TLA2B typechecker
-LOCAL RelRan(f) == { <<x[1], x[2]>>[2] : x \in f } \* The range of the function, syntax is weird to help TLA2B typechecker
+LOCAL GetKey(x) == <<x[1], x[2]>>[1] \* Get key of relational pair, also used as a type hint for TLA2B
+
+LOCAL RelDom(f) == {GetKey(x): x \in f} \* The domain of the function
+LOCAL RelRan(f) == {x[2]: x \in f} \* The range of the function
LOCAL MakeRel(f) == {<<x, f[x]>>: x \in DOMAIN f}
\* Converting a TLA+ function to a set of pairs
LOCAL Rel(S, T) == SUBSET (S \times T) \* The set of relations
diff --git a/src/main/resources/de/tlc4b/standardModules/Relations.tla b/src/main/resources/de/tlc4b/standardModules/Relations.tla
index 80940e6..901f724 100644
--- a/src/main/resources/de/tlc4b/standardModules/Relations.tla
+++ b/src/main/resources/de/tlc4b/standardModules/Relations.tla
@@ -1,10 +1,12 @@
---------------------------- MODULE Relations ----------------------------
EXTENDS FiniteSets, Naturals, Sequences, TLC
+LOCAL GetKey(x) == <<x[1], x[2]>>[1] \* Get key of relational pair, also used as a type hint for TLA2B
+
Relations(S, T) == SUBSET (S \times T)
\* The set of all relations
-RelDomain(R) == {x[1]: x \in R}
+RelDomain(R) == {GetKey(x): x \in R}
\* The domain of the relation R
RelRange(R) == {x[2]: x \in R}
@@ -13,10 +15,10 @@ RelRange(R) == {x[2]: x \in R}
RelId(S) == {<<x,x>>: x \in S}
\* The identity relation of set S
-RelDomRes(S, R) == {x \in R: x[1] \in S}
+RelDomRes(S, R) == {x \in R: GetKey(x) \in S}
\* The restriction on the domain of R for set S
-RelDomSub(S, R) == {x \in R: x[1] \notin S}
+RelDomSub(S, R) == {x \in R: GetKey(x) \notin S}
\* The subtraction on the domain of R for set S
RelRanRes(R, S) == {x \in R: x[2] \in S}
@@ -74,7 +76,7 @@ RelClosure1(R) == \* Warshall algorithm from Leslie Lamport's Hyperbook
IN W(NR)
\* The transitive closure of R
-RelClosure(R) == RelClosure1( R \cup {<<x[1],x[1]>>: x \in R} \cup RelIterate(R, 0))
+RelClosure(R) == RelClosure1( R \cup {<<x[1],x[1]>>: x \in R} \cup RelIterate(R, 0))
\* The transitive and reflexive closure of R.
RelFnc(R) == {<<x, RelImage(R, {x})>> :x \in RelDomain(R)}
--
GitLab