rewriter error: ... is not implemented

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint

https://apalache-mc.org/

Apache License 2.0

440 stars 40 forks source link

rewriter error: ... is not implemented #1801

Open nano-o opened 2 years ago

nano-o commented 2 years ago

Hello, I'm trying to find an inductive invariant for the specification in the attached bug report, so I started with TypeOkay. When I run apalache-mc check --inv=TypeOkay --init=TypeOkay TerminationNoPlusCal.tla I get Rewriting for the type FinFunSet[CellTFrom(Set(P)), FinFunSet[CellTFrom(Set(P)), InfSet[CellTFrom(Int)]]] is not implemented. Raise an issue.

So I guess this is a feature request!

BugReport.md

nano-o commented 2 years ago

After a little thought I replaced all functions P -> P -> Int by <<P,P>> -> Int. The specification does not look as good but it works.

konnov commented 2 years ago

Interesting. There is probably a case missing in the rewriting rule.

konnov commented 2 years ago

Thanks for filing this one!