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?
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?
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
In all cases you can replace
{TRUE, FALSE}
with the builtinBOOLEAN
.