"None" parsing error about atomkraft HOT 3 CLOSED

@tomtau thanks for the issue report 🙂 I will close this issue as a duplicate of the modelator issue.

We are currently using apalache CLI to communicate - which lacks a standard parsing format. So, we may have missed some error cases in the parser. When apalache-chai is integrated, atomkraft will use its proper API to communicate success and errors.

Duplicate of informalsystems/modelator#297

PS. I started the process to add you to our slack channel 🥳

from atomkraft.

Hi @tomtau ! Agree that the error message is not really helpful -> it will be addressed once this issue is resolved.

In the meantime, probably the best way to get better error messages is by using Apalache directly.
By running atomkraft model apalache info you will get the info on where it is on your system, and then you can run apalache parse models/nft.tla and apalache typecheck models/nft.tla (after adding the path of the folder containing apalache to your PATH variable).

In the concrete case, I believe the problem is at the line \E token \in denom[token]:: token is just introduced by the quantifir so it's not clear what denom[token] is. What did you try to achieve there?

from atomkraft.

@ivan-gavran thanks, running Apalache directly indeed produces more helpful error messages! the issue was with View == where it should have been:

View ==
    VariantGetOrElse(
        "TransferNft",
...

for the denom, I rewrote it as:

    \E denom \in DENOMS:
    \E token \in balances[sender][denom]:

It seems to load fine now. Should I keep this issue open (for unhelpful parsing error messages), or close it as it's subsumed by informalsystems/modelator#297 ? And for any further Atomkraft/Apalache questions, shall I open issues here or is there a better venue for it (e.g. Cephalopod Discord)?

from atomkraft.