[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Invariant valid in all states but one
I try to come up of an invariant which holds in all states but one. I'm wondering if it is possible to define such an invariant in TLA+. I'm new to TLA+ and from all the documentation I have red so far, I got the impression that an invariant may not contain temporal formulas and has to be true in *all* states.
Here is a minimal working example:
(* --algorithm test
variable x = 1
process foo \in 1..3
A: x := (x + 1) % 2;
B: x := 5;
C: x := (x - 1) % 2;
end algorithm *)
Inv == x < 2 \* holds except for B
In all states of all processes the invariant x < 2 holds except for label B. Is it possible to state that at B x = 5 has to hold and in all other states x < 2?
Any help is appreciated.