Skip to content
Snippets Groups Projects
Verified Commit f4efe3ed authored by Miles Vella's avatar Miles Vella
Browse files

Improve type inference of FunctionsAsRelations.tla for TLA2B

parent 0c493167
No related branches found
No related tags found
No related merge requests found
Pipeline #157765 passed
------------------------ MODULE FunctionsAsRelations ----------------------------------
EXTENDS FiniteSets, Functions, TLC, Sequences
LOCAL RelDom(f) == { x[1] :x \in f} \* The domain of the function
LOCAL RelRan(f) == { x[2] :x \in f} \* The range of the function
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 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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment