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

["myzh...@xxxxxxxxx" <myzh1989@xxxxxxxxx>]

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

-- 
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/ed2a5733-958d-4734-bdfc-6de7d287fa78n%40googlegroups.com.