| 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 TCInit == /\ 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. Stephan
--
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. |