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

[Stephan Merz <stepha...@xxxxxxxxx>]

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?

Regards,

Stephan

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