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

Re: [tlaplus] Init formula does not work



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

On 19 Mar 2020, at 11:02, alex.timimin@xxxxxxxxx wrote:

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.


--
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/91e593ce-867b-42a0-b28d-4cbfcfd2e836%40googlegroups.com.

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