[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 19 Mar 2020 11:43:40 +0100*References*: <91e593ce-867b-42a0-b28d-4cbfcfd2e836@googlegroups.com>

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. |

**References**:**[tlaplus] Init formula does not work***From:*alex . timimin

- Prev by Date:
**[tlaplus] Init formula does not work** - Next by Date:
**[tlaplus] Re: Init formula does not work** - Previous by thread:
**[tlaplus] Init formula does not work** - Next by thread:
**[tlaplus] Re: Init formula does not work** - Index(es):