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

[Hengfeng Wei <hengxin0912@xxxxxxxxx>]

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

-- 
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/0519ced7-42d8-4b90-b084-78f06db24c6c%40googlegroups.com.

Attachment: cure-kvstore-tla.zip
Description: Zip archive