[tlaplus] TLA+ Expressions - need clarification

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.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.