CODEWITHSUNDEEP
tla+pluscal
Andrew Samokish
Andrew Samokish

Reputation: 79

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?

Upvotes: 2

Views: 73

Answers (1)

Hovercouch
Hovercouch

Reputation: 2314

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.

Upvotes: 0

Related Questions