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

Re: [tlaplus] Invariant valid in all states but one

I'm not sure I understand your problem: you have access to the program counter, so you can simply write something like

\A self \in Proc : pc[self] # "B" => x < 2

But perhaps you simplified your problem so much that it becomes trivial here?


On 4 Jul 2018, at 18:58, stefa...@xxxxxxxxx wrote:

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.


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.