[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Init formula does not work
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"]
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.