[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]:
> https://github.com/hengxin/cure-kvstore-tla),
> 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.OpApplNode*
>     (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
> "Valid(sc)".
> However, what does the error mean and how should I fix it?

Hi Hengxin,

thanks for reporting the issue.  The bug has already been fixed in the
nightly build [1].  A workaround for the released version of TLC is
outlined at [2].


[1] https://nightly.tlapl.us/
[2] https://github.com/tlaplus/tlaplus/issues/422

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.