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

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

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.

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

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?

--
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.