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

[tlaplus] Re: Init formula does not work

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

четверг, 19 марта 2020 г., 14:35:50 UTC+4 пользователь Alex Tim написал:
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/083680a7-5475-4fbb-8921-cc34160b20d6%40googlegroups.com.