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.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/68ae5b95-a7c2-4590-ab08-36e2074f403e%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.