ResendRequest == /\ responses # << >>
/\ \E i \in 1..Len(responses):
LET response == responses[i]
IN
/\ response[1] = "SUSPENDED"
/\ response[3] = "SUSPENDED"
/\ requests' = Append(requests, <<"SENT", response[2]>>)
/\ responses' = Tail(responses)
Here I added "response[3] = "SUSPENDED"" condition which raised exception because tuple response only has length 2.
This is just to check that TLC has traversed a behaviour which has condition "/\ response[1] = "SUSPENDED"" evaluated to TRUE.
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.