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.