Should we fix the autogenerated model file?

[hwayne]

Currently the model file is this:

\* SPECIFICATION
\* Uncomment the previous line and provide the specification name if it's declared
\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.

CONSTANTS
    greeting = "Hello"

INIT Init
NEXT Next

\* PROPERTY
\* Uncomment the previous line and add property names

\* INVARIANT
\* Uncomment the previous line and add invariant names

99.99% of TLA+ configs I've seen do SPECIFICATION Spec, what if we just made that the default instead of Init/Next? I can whip up a PR if people are okay with it

[lemmy]

The generated config file is primarily for beginners. Therefore, the template should be thoroughly documented to clearly guide users on what steps they need to take.

Regarding Init/Next versus Spec: It doesn't make sense for the template to combine Init/Next with PROPERTY. The template should either include CONSTANT, INIT, NEXT, and INVARIANT (hide temporal), or alternatively, CONSTANT, SPECIFICATION, INVARIANT, and PROPERTY (expose temporal).

[hwayne]

I just thought of an advantage of defaulting to SPECIFICATION Spec: When writing pluscal specs, you specify fairness by writing fair process. This is automatically conjoined to the translated Spec. If we default to Init/Next, the fairness will be ignored and the user won't have a clear picture why.

[lemmy]

One more consideration: Many of us have likely been bitten by forgetting to change INIT/NEXT to SPECIFICATION when checking liveness properties, leading to confusion about stuttering behavior. To help users avoid this, SPECIFICATION seems like a better default. However, a comment in the autogenerated file should provide clear guidance for new users on how to address the case where there is only INIT/NEXT and no Spec formula (it would obviously be best to traverse the parse tree and search for Init, Next, Spec, ... before generating the model).

Error: The name Spec specified in the configuration file
is not defined in the specification.