|TLC interprets formulas of the form|
var = <_expression_> or var \in <_expression_>
as assignments in initial conditions (and similarly for actions). The formula
\A r \in RM : rmState[r] = "working"
is not of this form, and also it does not properly define the value of rmState (e.g., it could be a function whose domain is a strict superset of RM) or even state that rmState is a function at all. TLC therefore does not interpret it as an assignment but as a standard state predicate to be evaluated. Because rmState does not yet have a value in the initial state that is being created, this leads to the error message that you have observed.
You could write
/\ rmState \in [RM -> Status]
/\ \A r \in RM : rmState[r] = "working"
(where Status contains all possible statuses) but your definition of CInit is simpler and will be evaluated more efficiently by TLC.
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/506DDFEC-ED16-4EA9-91D4-F6866720F3DD%40gmail.com.