[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?
Hi Markus,
I have tried the debugger. I am still exploring how to use it.
I came across several things that I do not quite understand:
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?
Thanks,
Mingyang
On Tuesday, March 16, 2021 at 8:48:00 PM UTC-7 myzh...@xxxxxxxxx wrote:
Thank you so much, Markus! That's exactly what I need. I will have a try!
On 16.03.21 02:16, myzh...@xxxxxxxxx wrote:
> Hi guys,
>
> I am using a PlusCal to write a pretty complex spec. I got the following
> exception from the toolbox:
>
> "TLC threw an unexpected exception.
>
> This was probably caused by an error in the spec or model.
>
> See the User Output or TLC Console for clues to what happened.
>
> The exception was a java.lang.RuntimeException:
> util.Assert$TLCRuntimeException: Attempted to compare equality of
> boolean FALSE with non-boolean: ""
>
> The error occurred when TLC was evaluating the nested expressions at the
> following positions: The error call stack is empty."
>
> Since the error call stack is empty and the spec is pretty long (so I
> can't paste it here), it is hard for me to debug by just using print and
> assert.
>
> Any suggestions for debugging this?
>
> Thanks for your help,
>
> Mingyang
Hi Mingyang,
if you are comfortable debugging the TLA+ and not the PlusCal, check out
the error breakpoints [1] of the current TLA+ debugger prototype.
Rewind to the start of the screencast for installation instructions.
Markus
[1] https://youtu.be/6oMQYHogQek?t=777
--
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/b0883bb8-d74a-497f-8904-d3cb74ee7aeen%40googlegroups.com.