[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Digest for tlaplus@xxxxxxxxxxxxxxxx - 6 updates in 1 topic





On Tue, 2 Feb 2021 at 4:56 AM, <tlaplus@xxxxxxxxxxxxxxxx> wrote:
tlaplus@xxxxxxxxxxxxxxxx Google Groups
Oleg Levchenko <olevzon@xxxxxxxxx>: Feb 01 03:19AM -0800

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.
Stephan Merz <stephan.merz@xxxxxxxxx>: Feb 01 12:28PM +0100

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
 
 
Oleg Levchenko <olevzon@xxxxxxxxx>: Feb 01 03:28AM -0800

Interestingly, there is a workaround for "breakpoint". If purposely add
mistake into condition after "response[1] = "SUSPENDED"", TLA+ will raise
java.lang.RuntimeException exception and print out full behaviour.
 
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.
 
 
 
 
 
 
понедельник, 1 февраля 2021 г. в 14:19:23 UTC+3, Oleg Levchenko:
 
Oleg Levchenko <olevzon@xxxxxxxxx>: Feb 01 03:39AM -0800

Hello,
thanks for advice.
 
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:
 
Michael Leuschel <michael.leuschel@xxxxxxxxx>: Feb 01 01:43PM +0100

Hi Oleg,
 
> On 1 Feb 2021, at 12:19, Oleg Levchenko <olevzon@xxxxxxxxx> wrote:
 
> Is there any way in TLC to debug spec?
 
in case you can load your spec in ProB, you can use the animation views to debug your spec and inspect the enabling conditions
of the various actions.
 
Below is a screenshot of the ProB2-UI animator for the Peterson.tla example and showing why the action a1 is not enabled:
a1(self) == /\ pc[self] = "a1"
/\ flag' = [flag EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "a2"]
/\ UNCHANGED turn
 
Caveats:
- ProB only supports a subset of TLA+. In particular, it needs to be able to infer a type for every identifier.
- the terminology and syntax used in the State View and REPL comes from the B language, I am afraid
(but this can in principle be improved by extending the pretty-printer of ProB).
 
Greetings,
Michael
Oleg Levchenko <olevzon@xxxxxxxxx>: Feb 01 05:37AM -0800

Michael,
ProB at your screenshot looks just great!
 
Thanks, I will try it!
 
 
 
понедельник, 1 февраля 2021 г. в 15:43:12 UTC+3, leuschel:
 
You received this digest because you're subscribed to updates for this group. You can change your settings on the group membership page.
To unsubscribe from this group and stop receiving emails from it send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

--
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/CAN5YmhFTC5RYdrK%2BZg0aLGWQvU2SuGwoO-5VUBD0Ow-RDMNsCg%40mail.gmail.com.