[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] ClassCastException: LetInNode cannot be cast to class OpApplNode
On 26.01.20 01:25, Hengfeng Wei wrote:
> When I run the "CM" model (not TypeOK; see the attached files; [online]:
> I got the following 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 tla2sany.semantic.LetInNode cannot be cast to class
> (tla2sany.semantic.LetInNode and tla2sany.semantic.OpApplNode are in
> unnamed module of loader 'app')
> By trial and error, I have figured out that it fails at Line 221
> However, what does the error mean and how should I fix it?
thanks for reporting the issue. The bug has already been fixed in the
nightly build . A workaround for the released version of TLC is
outlined at .
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/5ae70315-6016-2dc1-9e48-e76d9fdd7898%40lemmster.de.