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)
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4f5676de-92f9-4ea3-8b52-3ed7e94dc819n%40googlegroups.com.
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.
On 1 Feb 2021, at 12:19, Oleg Levchenko <ole...@gmail.com> wrote:
Is there any way in TLC to debug spec?