Re: [tlaplus] ClassCastException: LetInNode cannot be cast to class OpApplNode

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

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