How can I set CONSTANTS in TLA+ configuration file when using VS Code?

Question

I'm learning TLA+ using VS Code and vscode-tlaplus plugin instead of TLA+ Toolbox. Now I have this TLA file where I define some constants:

---- MODULE test ----
EXTENDS TLC, Integers, Sequences

CONSTANTS Capacity, Items, ValueRange, SizeRange

ItemParams == [size: SizeRange, value: ValueRange]
ItemSets == [Items -> ItemParams]
===

I would like to set the following in the cfg file:

SPECIFICATION Spec

CONSTANTS
    SizeRange = 1..4
    ValueRange = 0..3
    Capacity = 7
    Items = {"a", "b", "c"}

But this causes the following error:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a tlc2.tool.ConfigFileException
:
TLC found an error in the configuration file at line 5
It was expecting = or <-, but did not find it.

So far I only found this workaround:

.tla

---- MODULE test ----
EXTENDS TLC, Integers, Sequences

CONSTANTS Capacity, Items, ValueRange, SizeRange

ConstSizeRange == 1..4
ConstValueRange == 0..3

ItemParams == [size: SizeRange, value: ValueRange]
ItemSets == [Items -> ItemParams]
====

.cfg

SPECIFICATION Spec

CONSTANTS
    SizeRange <- ConstSizeRange
    ValueRange <- ConstValueRange
    Capacity = 7
    Items = {"a", "b", "c"}

So, it seems useless to define a CONSTANT.

I'm doing something wrong, or is this the expected behaviour?

Thanks

Answer 1

This is the expected behavior. TLC only supports very specific TLA+ expressions as values assigned to constants in the CFG file. I agree it would be nice if more powerful expressions were supported.

This is generally handled by convention: you have one "good copy" SpecName.tla TLA+ spec which isn't directly model-checkable by TLC, and a second MCSpecName.tla TLA+ spec which overrides various definitions in the first to make it model-checkable, plus defines constant values. So in your case you'd have:

Test.tla:

---- MODULE Test ----
EXTENDS TLC, Integers, Sequences

CONSTANTS Capacity, Items, ValueRange, SizeRange

ConstSizeRange == 1..4
ConstValueRange == 0..3

ItemParams == [size: SizeRange, value: ValueRange]
ItemSets == [Items -> ItemParams]
====

MCTest.tla:

---- MODULE MCTest ----
EXTENDS Test

ConstSizeRange == 1..4

ConstValueRange == 0..3

====

MCTest.cfg:

SPECIFICATION Spec

CONSTANTS
    SizeRange <- ConstSizeRange
    ValueRange <- ConstValueRange
    Capacity = 7
    Items = {"a", "b", "c"}

You can see this convention used throughout the TLA+ examples, such as Paxos. It's actually quite a good convention, freeing you to write your "good copy" spec to more accurately reflect reality instead of conforming to the whims of the model checker. For example, in your good copy spec you might have a now variable which defines the current time; it could be Real-valued, and advance by an arbitrary positive Real value after every Tick action. In your MC spec you would override now and Tick to use some subset of the Naturals.