I'm following Hillel Wayne's book car & traffic light example and found that doing
either
do_something := TRUE
or
skip;
end either;
In PlusCal gets translated to:
\/ /\ do_something' = TRUE
\/ /\ TRUE
/\ UNCHANGED do_something
And replacing this with:
do_something' = TRUE \/ UNCHANGED do_something
Doesn't work.
Why aren't those equivalent?