var
are specified by a
subformula
F(..., var, ...)in the initial predicate, for some operator
F
such that expanding the
definition of F
results in a formula
containing more than one occurrence of var
,
not all occurring in separate disjuncts of that formula.
var
are specified by a subformula
F(..., var', ...)in the next-state relation, for some operator
F
such that expanding the
definition of F
results in a formula
containing more than one occurrence of var'
,
not all occurring in separate disjuncts of that formula.
An example of the first case is an initial predicate
Init
defined as
follows:
VARIABLES x, ... F(var) == \/ var \in 0..99 /\ var % 2 = 0 \/ var = -1 Init == /\ F(x) /\ ...The error would not appear if
F
were defined by:
F(var) == \/ var \in {i \in 0..99 : i % 2 = 0} \/ var = -1or if the definition of
F(x)
were expanded in
Init
:
Init == /\ \/ x \in 0..99 /\ x % 2 = 0 \/ x = -1 /\ ...A similar example holds for case 2 with the same operator
F
and the next-state formula
Next == /\ F(x') /\ ...