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

[tlaplus] Understanding PlusCal 'either' translation to TLA

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/1bebc6bc-b266-453f-8521-4906cff32b0an%40googlegroups.com.