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

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


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.

On Sunday, October 10, 2021 at 7:20:13 PM UTC-3 andrew...@xxxxxxxxx wrote:
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/9c32956d-55c5-404c-84d4-a756de2c67f0n%40googlegroups.com.