Understanding PlusCal 'either' translation to TLA

46 views
Skip to first unread message

Pablo Fernandez

unread,
Oct 9, 2021, 10:25:14 PM10/9/21
to tlaplus
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?

Andrew Helwer

unread,
Oct 10, 2021, 6:20:13 PM10/10/21
to tlaplus
When you say "doesn't work" what is the behavior you're seeing?

Pablo Fernandez

unread,
Oct 10, 2021, 10:26:34 PM10/10/21
to tlaplus
Andrew,

Thanks for answering. It seems I had an issue with my spec, I was doing

\/ /\ do_something' = TRUE
\/ /\ TRUE
\/ /\ UNCHANGED do_something

And was failing for a different reason. My bad.
Reply all
Reply to author
Forward
0 new messages