Invariant valid in all states but one

[stefa...@xxxxxxxxx]

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
begin
    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.

Cheers,
Stefan