[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?



@Calvin Thanks a lot, Calvin! I have not used any symmetry set. 
But the discussion you sent gives me some hints. 
I will try to replace some strings with model values and see if the problem can be solved.

On Friday, March 19, 2021 at 12:59:45 PM UTC-7 Calvin Loncaric wrote:
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 <myzh...@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+u...@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/4ccad82d-52a3-4519-9e6b-9eb1364e0d1fn%40googlegroups.com.