[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Invariant valid in all states but one

Hi all,

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 process

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.