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

Re: Idiomatically verifying state does not change

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.