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