diff --git a/src/main/resources/de/tlc4b/standardModules/FunctionsAsRelations.tla b/src/main/resources/de/tlc4b/standardModules/FunctionsAsRelations.tla index 07cd0f039bf87d52f39155c3ccdcb1d0460ffa05..326c7d0dbc81cd0b0ecd155baf5e11cd114178e9 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 80940e60a46e2fdb01cc7fa37eb91972d8b68c8d..901f724a00b898f0825f01383bc89aed78604cef 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)}