tla+pluscal

TLA+, pluscal: variable is in a set

In TLA+ I can write

x' \in {TRUE, FALSE}

and it will mean, that from this point Model Checker should study two branches, where my variable got different values. Is there a way to write the same thing in Pluscal?

Solution

  • First of all, that's not correct TLA+: you want to write either x' \in {TRUE, FALSE} or (more preferably) \E y \in {TRUE, FALSE}: x' = y.

    For PlusCal, you would write

    \* P-syntax
with y \in {TRUE, FALSE} do \* or {
  x := y;
end with \* or }

\* C-syntax
with y \in {TRUE, FALSE} {
  x := y;
}

    In all cases you can replace {TRUE, FALSE} with the builtin BOOLEAN.