I'm working through the TLA+ Lecture 5 example and trying to nail down the notation as implemented by TLA+. I have looked at the TLA+ book and the "cheat sheet" of notation, but I'm having a hard time wrapping my head around a couple things.
The primary question is related to the "type" of "rmState" and how it is used in the spec as a variable. The other questions have to do with how/when to interpret the meaning of square brackets in the TLA _expression_ syntax - in some cases they return a set of functions, in others they seem to represent a single function.
For example. This definition in the example spec:
TCTypeOK == rmState \in [RM -> {"working","prepared","committed","aborted"}]
In the TLA documentation, the _expression_ [S->T] is a "set of functions f, with f(x) /in T for x /in S".
So, according to the definition given, I can interpret as: S = RM and T = {"working","prepared","committed","aborted"}, and rmState is any function that maps S to T. Correct?
Which leads me to this definition _expression_ in the spec:
TCInit == rmState = [r \in RM |-> "working"]
Here the TLA documentation says the _expression_ of form "[x in S |-> e]" is a "function f, such that f(x) = e for x in S". Even though we're seeing [] brackets - which implies a set of functions, that function which returns a specific (constant _expression_ 'e') value for any x in S can really only be a constant function. In this case, rmState seems to be representing a function that returns "working" for all r in RM. Correct?
To summarize:
1. I think rmState's type, based on the above definitions/context, is "function".
2. The square bracket notation can return or reference either a set of functions or a specific function.
Thanks for any clarification or support.