[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Understanding PlusCal 'either' translation to TLA
- From: Pablo Fernandez <fernandezpablo85@xxxxxxxxx>
- Date: Sat, 9 Oct 2021 19:25:14 -0700 (PDT)
- Ironport-hdrordr: A9a23:yk8rjaDfdwr/6ZLlHenP55DYdb4zR+YMi2TDsHoQdfU1SK2lfq+V98jzuSWftN9zYh8dcLK7VJVoKEm0naKdirN/AV7NZmTbhFc=
I'm following Hillel Wayne's book car & traffic light example and found that doing
do_something := TRUE
In PlusCal gets translated to:
\/ /\ do_something' = TRUE
\/ /\ TRUE
/\ UNCHANGED do_something
And replacing this with:
do_something' = TRUE \/ UNCHANGED do_something
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.