[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Understanding PlusCal 'either' translation to TLA

When you say "doesn't work" what is the behavior you're seeing?

On Saturday, October 9, 2021 at 10:25:14 PM UTC-4 fernande...@xxxxxxxxx wrote:
I'm following Hillel Wayne's book car & traffic light example and found that doing

    do_something := TRUE
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?

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/11ba9ce1-bbff-4087-b904-1db4b41bc6dbn%40googlegroups.com.