Re: [tlaplus] MC file naming convention?

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.


> On Apr 12, 2024, at 10:03 AM, hwa...@xxxxxxxxx <hwayne@xxxxxxxxx> wrote:
> 
> 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?

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/A2F9DC90-00AA-48CA-90D1-F6B04F5F83F0%40lemmster.de.