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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Wed, 5 Oct 2016 22:54:47 -0700 (PDT)*References*: <69a562b8-616e-4375-939b-d0d79e94eff0@googlegroups.com>

What you want to check is a temporal safety property of your spec. The canonical way to write a safety property in TLA+ is in the form

(*) I /\ [][A]_v

where I is a state predicate, A an action, and v a state function. For example, the invariance formula []Inv can be written as

Inv /\ [][Inv']_Inv

Your formula T2 has the form (*), where I equals TRUE. TLC can generate the set of all possible behaviors allowed by (*) only when I, A, and v have a very special form. Not coincidentally, this is a natural form in which to describe algorithms and high-level designs of systems--which is why TLA+ and TLC are useful. TLC can check that a set of behaviors it can generate all satisfy (*) on a much larger class of formulas I, A, and v. It just has to be able to compute I, A, and v on all states or pairs of states that occur in that set of behaviors.

Leslie

**References**:**Idiomatically verifying state does not change***From:*Hillel Wayne

- Prev by Date:
**Re: [tlaplus] Idiomatically verifying state does not change** - Next by Date:
**Re: TLA+ community event 2016** - Previous by thread:
**Re: [tlaplus] Idiomatically verifying state does not change** - Next by thread:
**TLA+ and pluscal BNF grammars** - Index(es):