[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Actions Debugging
Is there any way in TLC to debug spec?
For example, I have an action "ResendRequest" which is not "fired", i.e. TLC shows it has 0 distinct states.
Is there any way in TLC to set a breakpoint on a particular condition so that I could see why my action doesn't fire?
Example is below.
ResendRequest == /\ responses # << >>
/\ \E i \in 1..Len(responses):
LET response == responses[i]
/\ response = "SUSPENDED"
/\ requests' = Append(requests, <<"SENT", response>>)
/\ responses' = Tail(responses)
It would be convenient to set a breakpoint on a condition "response = "SUSPENDED"" so that I could see why behaviours traversing ResendRequest don't fire this action, i.e. why its not enabled.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4f5676de-92f9-4ea3-8b52-3ed7e94dc819n%40googlegroups.com.