[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: Model checking a mutually recursive definition of a tree
On 7/26/21 4:31 AM, Andrew Helwer wrote:
However this then caused TLC to output a novel (to me) error:
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.ClassCastException
: class tlc2.tool.coverage.ActionWrapper cannot be cast to class
tlc2.tool.coverage.OpApplNodeWrapper (tlc2.tool.coverage.ActionWrapper
and tlc2.tool.coverage.OpApplNodeWrapper are in unnamed module of loader
'app')
This issue [1] has been fixed in the most up-to-date nightly [2].
As a workaround for previous versions of TLC, run TLC without the
-coverage parameter. In the Toolbox, turn off profiling on the "TLC
Options" page of the model editor.
Markus
[1] https://github.com/tlaplus/tlaplus/issues/649
[2] https://nightly.tlapl.us
--
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/2cfd0acc-4b4c-1dfb-d7b5-c643288f407b%40lemmster.de.