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