Example of model configurations

[alxiong]

Do we have a more comprehensive list of possible/example configuration .cfg files?

[lemmy]

For anything more complex, like the example you removed in an edit, you will have to use the MC.tla/MC.cfg approach.

[alxiong]

Yeah I figure that out, but still would appreciate an archive of example covering most cases of configurations

[lemmy]

Unfortunately, I'm not aware of a comprehensive list of examples. https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/ModelConfig.java is the link to TLC's config parser.

[sumuhans]

For anything more complex, like the example you removed in an edit, you will have to use the MC.tla/MC.cfg approach.

Please can you explain what the MC.tla/MC.cfg is?
For context, I am trying to specify two sets as symmetry sets in the config file and I am having problems
I tried

CONSTANTS
    RM = {r1, r2}
    Acceptor = {a1, a2, a3}


\* Mark RM and Acceptor as symmetry sets to reduce state space
SYMMETRY RM, Acceptor

But that errors. I found this approach which seems a bit messy but it works - but only for specifying one set as symmetry set. If I try to specify two sets as symmetry sets I still run into errors. Please can you show how to mark two or more sets are symmetry sets?

[lemmy]

------ MODULE MC -------
EXTENDS YourSpec

CONSTANTS
r1, r2
----

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
a1, a2, a3
----

\* MV CONSTANT definitions RM
const_17521415551458000 == 
{r1, r2}
----

\* MV CONSTANT definitions Acceptor
const_17521415551479000 == 
{a1, a2, a3}
----

\* SYMMETRY definition
symm_175214155514710000 == 
Permutations(const_17521415551458000) \union Permutations(const_17521415551479000)

====

SYMMETRY symm_175214155514710000

[sumuhans]

Amazing 🤩
Thank you so much @lemmy for clarifying this! That's really helpful!

[2BitSalute]

I don't understand the UI for non-default model config at all. Where do I pick the non-default config? What is its format?
I know I can figure it out if I feel very motivated, but it feels like it should be more obvious.

[lemmy]

The default model config for spec Foo.tla is Foo.cfg. The non-default model config lets you choose a different file such as Bar.cfg.

[2BitSalute]

Where is it located? Is the text box supposed to take the path to the file, or is it supposed to be in the same file?
And the default model config - I see one can create it when one chooses to use the default one, and then the syntax is more obvious (because the types of config are provided as a sample and some are commented out). I wish this was in the "getting started" somewhere.

[lemmy]

Screen.Recording.2024-02-18.at.7.45.46.PM.mov

[lemmy]

Generally, you have to manually create configurations. The difference between a default and non-default configuration is merely that a default configuration shares the name with the spec file, i.e., MC.tla and MC.cfg.

Note that the VSCode extension lacks a model editor (related #152).