Let me amplify Stephan's answer. The next-state relation
~TrySomething => TrySomethingElse
is equivalent to
TrySomething \/ TrySomethingElse
The latter strikes me and most TLA+ users as the more natural way to
write that next-state relation. At any rate, that's the way TLC
expects it to be written and it won't handle the first way--unless
TrySomething is a state predicate.
IF TrySomething THEN success' = TRUE
ELSE DoSomethingElse /\ success' = FALSE
is equivalent to
\/ TrySomething /\ success' = TRUE
\/ ~TrySomething /\ DoSomethingElse /\ success' = FALSE
which is a rather weird spec. If TrySomething /\ DoSomethingElse = FALSE,
then it's just an overly complicated way to write
\/ TrySomething /\ success' = TRUE
\/ DoSomethingElse /\ success' = FALSE
However, I suspect that what you really want to write is
IF it's possible to do a TrySomething action
THEN TrySomething /\ success' = TRUE
ELSE DoSomethingElse /\ success' = FALSE
You can write this as
IF ENABLED TrySomething
THEN TrySomething /\ (success'=TRUE)
ELSE DoSomethingElse /\ success' = FALSE
and that will work fine. But you can usually find an _expression_
that's equivalent to `ENABLED TrySomething' and save TLC (and the
reader of the spec) the trouble of evaluating the ENABLED _expression_.
Leslie