Init formula does not work

[alex.t...@gmail.com]

Hello all!

I've just started learning TLA+ with the well-known video course.

Can someone please explain why the formula (used as init predicate):

TCInit == \A r \in RM : rmState[r] = "working" 

induces an exception in TLC:

In evaluation, the identifier rmState is either undefined or not an operator.
line 16, col 25 to line 16, col 31 of module TCommit

while this one

CInit == rmState = [r \in RM |-> "working"]

works fine.

Thanks in advance.

[Stephan Merz]

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/91e593ce-867b-42a0-b28d-4cbfcfd2e836%40googlegroups.com.

[Alex Tim]

Hi. Thanks a lot. I guessed something like this, now it is much more clear.

четверг, 19 марта 2020 г., 14:35:50 UTC+4 пользователь Alex Tim написал: