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

Idiomatically verifying state does not change


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


            with apple \in inside do

                inside := inside \ {apple};

                outside := outside \cup {apple};

            end with


            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:

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!