ClassCastException: LetInNode cannot be cast to class OpApplNode

[Hengfeng Wei]

Dear All,

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?

Best regards,

Hengxin

[Markus Kuppe]

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].

Markus

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