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.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
Visit this group at https://groups.google.com/group/tlaplus
For more options, visit https://groups.google.com/d/optout