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/506Although, it is hard for me to tell for sure if the issues are related without more information.--CalvinThanks, 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.MingyangOn 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.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1b2f3ece-72c5-4ba6-a0e7-359a743728e0n%40googlegroups.com.