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