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

*From*: Hillel Wayne <hwa...@xxxxxxxxx>*Date*: Wed, 5 Oct 2016 11:00:50 -0700 (PDT)

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!

**Follow-Ups**:**Re: Idiomatically verifying state does not change***From:*Leslie Lamport

**Re: [tlaplus] Idiomatically verifying state does not change***From:*Stephan Merz

- Prev by Date:
**Re: Newcomer Questions** - Next by Date:
**Re: [tlaplus] Idiomatically verifying state does not change** - Previous by thread:
**Re: Newcomer Questions** - Next by thread:
**Re: [tlaplus] Idiomatically verifying state does not change** - Index(es):