Idiomatically verifying state does not change

[Hillel Wayne]

Hi,

I've started learning TLA+ to help blueprint some product work, and I've been finding it really useful. One problem I've run into is that I'm not sure what's the best way to model "if A is false, B cannot happen." Here's an PlusCal toy example:

(* --algorithm apples \* Taking apples out of a basket

variables inside = {1,2,3,4,5} ;

          outside = {};

          basket_open = TRUE; \* Is the lid off?

          

begin while inside # {} do

    either 

            with apple \in inside do

                inside := inside \ {apple};

                outside := outside \cup {apple};

            end with

        or

            basket_open := ~basket_open; \* Put on or take off the lid

    end either

end while

end algorithm *)

The temporal formula I want to test is "you cannot take an apple out if the basket is not open". Note that this will fail (there's no code to do anything with basket_open). Here's what I've tried:

• I1 == (~basket_open) => UNCHANGED inside. Fails to evaluate. Not 100% certain but from what I understand it's because you cannot have an action as part of an invariant. 
  
• T1 == ~basket_open => [][UNCHANGED inside]_vars. This seems like it would be an accurate temporal formula, but TLC can't check it (Specifying Systems, 235)
• T2 == [][~basket_open => UNCHANGED inside]_vars. This works, but I'm not sure I understand why. I think what's going on is that it's effectively the same as I1, except that it's a boxed-action so TLC can check it. I don't know, though, whether it's due to implementation details or because I1 is nonsense TLA+ (or some other reason)
  

T2 seems to work, but it seems complicated enough that I'm wondering if I missed a simpler, more obvious way. Also, because there's an emphasis in the book on "testing safety is much more important that testing liveness", I'm wondering if there's a simple way to turn it from an temporal formula into a state predicate. Or maybe I'm approaching the design entirely in the wrong way. Any suggestions, examples, etc would be appreciated. Thanks!

[Stephan Merz]

The idiomatic way to express "if A is false, B cannot happen" is

  ~A => ~ ENABLED B

When you write your algorithm in PlusCal, B will be expressed as the action corresponding to a label in the PlusCal algorithm, or perhaps to a disjunction of such actions.

Your formula T2 also works, but the expression is less direct. Note that it is a safety property, even if it goes into the "properties" section of the TLC Toolbox pane. The invariants section may only hold state predicates (evaluated at every reachable state), and may therefore not contain any action formulas, such as UNCHANGED v, which is just shorthand for (v' = v).

Hope this helps,

Stephan

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Hillel Wayne]

This not only answered my question, it also answered a few other questions I hadn't thought to ask yet. Thank you so much for your help!

[Leslie Lamport]

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