# Re: [tlaplus] Actions Debugging

Hello,

Invariant proves that action ResendRequest does fire.
On the other side, TLC report shows that ResendRequest has 0 distinct states, but 31,440  "Found States".

How to treat figures "Found States" and "Distinct States" in TLC reports?

Does combination "Distinct States" = 0 and   "Found States" = 31, 440 mean that spec is still valid, i.e. ResendRequest generates states which are correct, they are just not "new" for the overall possible states found?

понедельник, 1 февраля 2021 г. в 14:28:40 UTC+3, Stephan Merz:
Hello,

you can use TLC to verify the invariant

\A i \in 1 .. Len(responses) : responses[i][1] # "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.

Regards,
Stephan

On 1 Feb 2021, at 12:19, Oleg Levchenko <ole...@xxxxxxxxx> wrote:

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+u...@xxxxxxxxxxxxxxxx.