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

Re: [tlaplus] How to debug unexpected exception when the error call stack is empty?



Mingyang,

Are you by any chance using symmetry sets to reduce the state space during model checking?

The call-stack-free error report looks similar to one I have encountered while using symmetry sets: https://github.com/tlaplus/tlaplus/issues/506

Although, it is hard for me to tell for sure if the issues are related without more information.

--
Calvin


On Fri, Mar 19, 2021 at 12:44 PM myzh...@xxxxxxxxx <myzh1989@xxxxxxxxx> wrote:
Thanks, Markus!

The spec is pretty long (2k pluscal --> 5k tla+) and still under-development (an academic project).
I could post it when it is more mature/ready to publish.

Mingyang

On Friday, March 19, 2021 at 9:01:06 AM UTC-7 Markus Alexander Kuppe wrote:
On 18.03.21 23:55, myzh...@xxxxxxxxx wrote:
> 1) Let's assume I set the breakpoint at Init. If I use "step over", I
> can reach the breakpoint step by step manually.
> However, if I use "continue", the debug process just ends without giving
> me anything.
> Do I miss something here?
>
> 2) Sometimes, when a breakpoint is reached, the trace list only contains
> "internal error" without showing any trace (I can continue to debug
> though).
> Do you know what does "internal error" mean here?


Hi Mingyang,

thanks for your feedback. I described a workaround for the breakpoint
problem in [1]. For the second bug you've encountered, please add the
spec that triggers it to the corresponding Github issue [2].

Markus

[1] https://github.com/lemmy/vscode-tlaplus/issues/3
[2] https://github.com/lemmy/vscode-tlaplus/issues/4

--
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/1b2f3ece-72c5-4ba6-a0e7-359a743728e0n%40googlegroups.com.

--
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/CABf5HMhwHdd_1HautxRLfzD_%2BXWZ8WL%3DxP4sPhWf4FUsMMXoCw%40mail.gmail.com.