[tlaplus] Actions Debugging

[Oleg Levchenko <olevzon@xxxxxxxxx>]

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]

                            IN 

                             /\ response[1] = "SUSPENDED"

                             /\ requests' = Append(requests, <<"SENT", response[2]>>)

                             /\ responses' = Tail(responses)

It would be convenient to set a breakpoint on a condition "response[1] = "SUSPENDED"" so that I could see why behaviours traversing ResendRequest don't fire this action, i.e. why its not enabled.

Oleg.

-- 
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.