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



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/53b896d2-86e3-1075-3e3a-f1cdbb9f64be%40lemmster.de.