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