| A formula such as
x = 0 /\ a = "" /\ [][Next]_<<a,x>>
is legal TLA+, but TLC refuses to evaluate it. In general, TLC evaluates formulas from left to right, and the first occurrence of a primed variable should be either
x' = e or x' \in S
(for expressions e and S that TLC knows to evaluate; also, S should evaluate to a finite set). The fine print is in the TLA+ book. The idea is that TLC works as an interpreter to generate all successor states such that the next-state predicate is true. There are some situations when a less naive approach to evaluation would be desirable, e.g. through constraint solving as done by ProB [1,2].
Concerning your remark on formula organization, it may depend on how you structure your definitions in building up "TrySomething", which currently appears to include both the conditions of applicability and the effects. Instead, I would typically write
IF SomeCondition THEN /\ DoSomething /\ success' = TRUE ELSE /\ UNCHANGED data /\ success' = FALSE
where "SomeCondition" is a state predicate.
Best, Stephan
[2] http://www3.hhu.de/stups/prob/index.php/TLA
Just to make sure I really understand, is the following next-state formula not OK or is it just rejected by TLC for implementation reasons? (assuming x and a are the only variables)
Next == IF x' = 3 THEN a' = "SUCCESS" ELSE /\ x' = 5 /\ a' = "FAIL"
(Or even: Next == ~(x' = 3) => x' = 5)
Because it seems to me that for any two states, s and t, the formula [Next]_<<x, a>> always determines whether t can be a next state of s.
If it is just a TLC issue, then it's come up in practice a few times while I writing my first spec. Not in that precise form but more like:
Next == IF TrySomething THEN success' = TRUE ELSE /\ UNCHANGED data /\ success' = FALSE
Or
Next == ~TrySomething => TrySomethingElse
Where TrySomething has some intricate conditions, depending on which it "sets" data' to one of several possible values, or if none of the conditions is met it doesn't touch data'. I'm interested to know whether TrySomething has succeeded or failed. Obviously, this can be refactored by taking the conditions out of TrySomething, but that would make the formula encapsulation and organization less optimal. So, assuming the formula is valid TLA+, it seems quite sensible yet TLC can't handle it...
It is also very likely that I still haven't internalized the TLA+ "style" yet, but at least from a beginner's perspective, the above formulas seem natural.
Ron
--
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 http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|