[tlaplus] Init formula does not work

[alex.timimin@xxxxxxxxx]

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.