Unexpected exception about apalache HOT 2 CLOSED

I looked into it, and the underlying issue is that the use of model values in the config files is incompatible with the type annotation in the spec. For example, the config defines

Producers = {p1,p2}

but the spec defines

\* @type: Set(PROC);
Producers

Uninterpreted literals in Apalache, that is, values of type PROC, have the shape <identifier>_OF_PROC, whereas "model values" (such as p1,p2), as TLC uses them, get parsed to ModelValue_<identifier> _of type Str.

Note that none of the following is supported at the moment:

• Parsing uninterpreted type literals from .cfg files
• Using TLC model values with anything but a Str annotation.

The issue arises, because Apalache "trusts" config files, and performs type-checking before the configuration pass, so it does not validate that the substitutions generated in the configuration pass are typesafe. This is a known issue, and I'll link the other cases as soon as I track them down.

from apalache.

Previous instance of this issue: #2682 (comment)

from apalache.