How to debug unexpected exception when the error call stack is empty?

47 views
Skip to first unread message

myzh...@gmail.com

unread,
Mar 16, 2021, 5:16:22 AMMar 16
to tlaplus
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


Markus Kuppe

unread,
Mar 16, 2021, 11:09:19 AMMar 16
to tla...@googlegroups.com
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

Mingyang Zhang

unread,
Mar 16, 2021, 11:48:00 PMMar 16
to tla...@googlegroups.com
Thank you so much, Markus! That's exactly what I need. I will have a try!

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/53b896d2-86e3-1075-3e3a-f1cdbb9f64be%40lemmster.de.


--
Thanks,
Mingyang

myzh...@gmail.com

unread,
Mar 19, 2021, 2:55:18 AMMar 19
to tlaplus
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

Markus Kuppe

unread,
Mar 19, 2021, 12:01:06 PMMar 19
to tla...@googlegroups.com
On 18.03.21 23:55, myzh...@gmail.com 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

myzh...@gmail.com

unread,
Mar 19, 2021, 3:44:17 PMMar 19
to tlaplus
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

Calvin Loncaric

unread,
Mar 19, 2021, 3:59:45 PMMar 19
to tla...@googlegroups.com
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


--
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...@googlegroups.com.

myzh...@gmail.com

unread,
Mar 20, 2021, 6:57:40 PMMar 20
to tlaplus
@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.

Andrew Helwer

unread,
Mar 22, 2021, 11:21:55 AMMar 22
to tlaplus
It sounds like since the call stack is empty the bug is being hit when evaluating either Init or one of your invariants in the initial state(s). You might be able to identify the problem by disabling checking some of your invariants to see if you can get further before something is hit; that will identify the problematic invariant. You can then sort of do a binary search on that invariant by commenting out half of it, re-running the model checker, and seeing whether the error is hit.

Andrew
Reply all
Reply to author
Forward
0 new messages