The example below (copied from https://learntla.com/pluscal/behaviors/) is bogus and future Pcal translator versions won't accept it (see screenshot below). The "f" in the either statement is a bound identifier and thus cannot be assigned a value.
---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
variables f1 \in BOOLEAN, f2 \in BOOLEAN, f3 \in BOOLEAN
begin
while TRUE do
with f \in {f1, f2, f3} do
either
f := TRUE;
or
f := FALSE;
end either;
end with;
end while;
end algorithm; *)
====
The example below (copied from https://learntla.com/pluscal/behaviors/) is bogus and future Pcal translator versions won't accept it (see screenshot below). The "f" in the either statement is a bound identifier and thus cannot be assigned a value.