you can use TLC to verify the invariant
\A i \in 1 .. Len(responses) : responses[i] # "SUSPENDED"
If this invariant doesn't hold, TLC will show you a counter-example that you can follow to check if it corresponds to expected behavior.
If TLC reports that the invariant holds, you can check similar properties to debug further, for example check if
responses = << >>
is an invariant of your specification.
In case TLC shows 0 distinct states overall, the initial condition must be unsatisfiable.
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/3167BF18-EED5-419A-89E7-446C1C8405CB%40gmail.com.