Better separate models and specs

[lemmy]

We want specs to describe systems. Verification with model-checkers such as TLC is import, but ultimately a secondary concern. We do not want users to write specs that are amenable to model-checking.
The primary purpose of the Toolbox's model editor is to make it convenient to check specs without amending them for model-checking. Until (if ever) vscode-tlaplus has first-class support for TLC models, I suggest to adopt the convention of the pre-toolbox era: Where vscode-tlaplus currently creates a Foo.cfg config file for a Foo spec, vscode-tlaplus should create the pair MCFoo.tla and MCFoo.cfg (with the necessary boilerplate such as EXTENDS Foo, ...).

/fyi @xxyzzn

[dricketts]

For whatever it's worth, I suprisingly haven't found this to be an issue for the kinds of specs I've written. I prefer having a single cfg file that I edit directly, rather than the indirection of either manually editing MCFoo.tla and MCFoo.cfg or clicking through a model editor UI.

On another thread, you wrote that users shouldn't have to write something like x \in 1..3 to make the model finite state, when they really mean x \in Nat. But in my opinion, in a lot of specs, I find it better to write:

CONSTANT XType
ASSUME XType \in SUBSET Nat

...x \in XType

Then a model can instantiate XType with a finite set of natural numbers. This maintains the separation between spec and model and makes the spec clearer in some places. It also gives more flexibility in model checking if there are two variables that should be drawn from different subsets of Nat because you can have two constants (XType and YType) and instantiate them in the model with different values, rather than the same override of Nat.

[lemmy]

@dricketts "if ever" above is supposed to indicate that this issue isn't about adding a clone of the Toolbox's model editor to vscode-tlaplus. I, for one, am frequently annoyed with the fact that the Toolbox's model editor doesn't have first-class keyboard support. From what I know, forms are also not a first-class UI paradigm of VSCode. That said, the Toolbox succeeds in encouraging users to use definition overrides or constants (make use of models). In contrast, most specs on Github written with vscode-tlaplus usually hardwire things. In other words, vscode-tlaplus works well for TLA+ experts but can be improved to guide novice users better.

[dricketts]

I wonder whether the pre-toolbox convention of MCFoo.tla and MCFoo.cfg would actually discourage novices from hardwiring constants.

To be clear, I wholeheartedly agree with the goal. I've seen many beginners hardwire things that should conceptually be constants/overrides. But I worry that generating the extra MC* files would not prevent novices from doing this and would annoy more experienced users. On the other hand, I don't have any other ideas.

[lemmy]

I don't think we need to be overly concerned about experienced vscode-tlaplus users. They will simply ignore the functionality to generate anything and do it manually/customize (expert customization is one area where the Toolbox is particularly weak).

[lemmy]

@dricketts How do you organize/handle TLC runtime settings (memory, cores, ...) with vscode-tlaplus? From my experience, storing them as VSCode settings is not ideal.

[dricketts]

@lemmy That's a good point - experienced users could just disable a feature like auto-generation of MC*. I'm still skeptical that it will discourage novices from hardcoding things, but I have no evidence to support that skepticism nor a better idea, so it's probably best to ignore my earlier comments.

I don't organize runtime settings in vscode. When I run TLC from vscode, it's always a small model on my laptop, so I just use the defaults (I'm not even sure what those are). If I want to run a larger model, it's always on a remote machine, from the command line, so I just have a script to launch TLC from the command line with the appropriate settings. It's not a great workflow, but I haven't had too much trouble with it.

[lemmy]

One idea would be to get rid of MC.cfg entirely and extend the approach of apalache with CInit. Instead of naming conventions, though, there would be a special module with operators to define state constraints, action constraints, ...

[dricketts]

How would model values work with the apalache approach?

[lemmy]

I don't have a complete proposal yet (in this particular case, I could imagine some syntax along the lines of mv == MC!ModelValue).

What do you think about the premise of merging MC.tla and MC.cfg into SuperMC.tla? I would assume that especially text-first IDEs would benefit from a config that is all TLA+ syntax.

[dricketts]

I very much like that idea. It seems like it would hit the sweet spot for both novices and experienced users.

[lemmy]

FWIW: I just spent five minutes figuring out why TLC takes forever to check a small-ish spec. The reason was that the extension settings included TLC's -dump ... parameter as "leftover" from checking another spec.

[lemmy]

How would model values work with the apalache approach?

@dricketts tlaplus/tlaplus@f50d67d

[lemmy]

An example of a user having problems with writing a correct TLC config file: http://discuss.tlapl.us/msg04859.html

[JoshuaRowePhantom]

I consider myself fairly proficient with TLA+, but not so much with the .cfg files since I'm used to using the Toolbox. I'm trying to make the switch to VSCode, and the mapping between the Toolbox way and the VsCode way is eluding me. I do find that having several Toolbox models helps me make tradeoffs that I can communicate to other engineers by checking them in.

Whether or not support is added for toolbox-style models, at least documenting how to achieve a similar result would be helpful for users trying to make the transition like myself.

[lemmy]

You can reuse the generated MC.tla and MC.cfg files in VSCode. If you have two or more Toolbox models Model_1, Model_2, ..., copy and rename the Toolbox MC.tla/cfg files to something like Model_1.tla and Model_1.cfg in VSCode.

Note that TLC will check the active spec when TLA+: Check model with TLC is launched from the command emmet. In other words, to check Model_1, make Model_1.tla or Model_1.cfg the active editor. However, VSCode will look for MCSpec.tla/cfg iff the currently open spec Spec.tla has no Spec.cfg. You don't have to change the active editor while working on the main spec and repeatedly checking the same model (#233).

As to TLC performance flags and advanced configuration that lives outside TLC's config files, they have to be entered manually into the prompt that is part of the command emmet. VSCode remembers the latest value as part of its workspace settings (#216, #208, #207). #172 (comment) discussed alternatives.

[sfre-coop]

I hadn't realised that the trick to making this work is to run the Model spec. Does that mean that the config for the underlying spec is now ignored? Is there a way to "inherit" from it? Thx

[lemmy]

There is no support to inherit from configs. Let S.tla be the "underlying" spec and S.cfg the corresponding config. As a workaround, you can reuse S.cfg when checking the model spec MCS.tla by running TLC with tlc -config S.cfg MCS.tla. In VSCode, this amounts to selecting "TLA+: Check model with TLC using non-default config..." in the command palette.