Document how to set/override constants

[lorin]

I'm not sure how to set or override constant values.

I've figured out how to set model values in the .cfg file, for example:

CONSTANT APPROVED = APPROVED

However, if I want to set a constant value (e.g., set the constant Vmax to 3), or override the value of Nat to 0..(Vmax+1), I'm not sure how to do that.

The TLA+ Toolbox creates two files: mc.cfg and mc.tla, and puts something like this in mc.cfg:

\* CONSTANT definitions
CONSTANT
Vmax <- const_158915461269331000
\* CONSTANT definition
CONSTANT
Nat <- def_ov_158915461269332000

And then puts this in mc.tla:

---- MODULE MC ----
EXTENDS mymodulename, TLC

\* CONSTANT definitions @modelParameterConstants:8Vmax
const_158915461269331000 ==
3
----

\* CONSTANT definition @modelParameterDefinitions:0
def_ov_158915461269332000 ==
0..(Vmax+1)
----
=============================================================================

But I don't know what the equivalent of the mc.tla file is for the vscode plugin. I can put those definitions directly in my .tla file, but that feels gross. Putting the constants directly in the cfg file itself doesn't work.

[lemmy]

@lorin AFAIK the prototype of a model editor is the only way to automatically generate the MC.tla/MC.cfg combi.

[lemmy]

Related: #219