MC file naming convention?

[hwa...@gmail.com]

You have a file `Spec.tla` which requires some constant C in the form of a tuple, which `.cfg` files cannot accept as a value. If you can't use the TLA+ Toolbox, the idiomatic solution is to write a new "model checkable spec" file which `EXTENDS Spec`, define the constant as an operator `Op` in that file, and then put `CONSTANT C <- Op` in that file's `.cfg`.

How do you name the "model checkable spec" file? I think Apalache does `MC_Spec.tla`, the toolbox calls it just `MC.tla`. Do you do one of those, `MCSpec.tla`, `SpecMC.tla`, or something else?

[Markus Kuppe]

If the files MCSpec.tla and MCSpec.cfg exist, the VSCode extension will automatically check them when the current editor is Spec.tla. Additionally, it will check SmokeSpec.tla and its corresponding SmokeSpec.cfg each time the editor is saved.