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

Re: Unclear TLC evaluation behavior

Aha! ENABLED! That's what I've been looking for! (although it took a roundabout way to get there)...

As to the rest of your proposals, I've tried them all first but found them lacking. I realize their obvious superiority -- when applicable -- but the examples I've provided are a gross (over)simplification of the actual spec, so those other forms don't work well. I think that my attempts to provide minimal examples have only taken us off the path...

For one, the conditions in TrySomething are complex and each results in a different assignment to data', so refactoring TrySomething into a state predicate and an action is rather ugly and results in a lot of duplication (b/c TrySomething is enabled if A \/ B \/ C, but assigns data' something different for each, and specifying "A \/ B \/ C" in TrySomething's "caller" -- sorry for using programming terms -- is a replication that might cause errors). For another,

    \/ TrySomething /\ success' = TRUE
    \/ DoSomethingElse /\ success' = FALSE

doesn't work because DoSomethingElse is always enabled (in my case, they correspond to "handle incoming message", and "postpone message handling for later"). 

Thanks to the both of you!