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

*From*: stefa...@xxxxxxxxx*Date*: Wed, 4 Jul 2018 09:58:48 -0700 (PDT)

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

**Follow-Ups**:**Re: [tlaplus] Invariant valid in all states but one***From:*Stephan Merz

- Prev by Date:
**Re: A spec for a trading algo** - Next by Date:
**Re: [tlaplus] Invariant valid in all states but one** - Previous by thread:
**Re: Why TLA+ is based on explicit state model-checking instead of symbolic one?** - Next by thread:
**Re: [tlaplus] Invariant valid in all states but one** - Index(es):