title: How can I set CONSTANTS in TLA+ configuration file when using VS Code?
body: <p>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:</p>
  
  <pre><code>---- MODULE test ----
  EXTENDS TLC, Integers, Sequences
  
  CONSTANTS Capacity, Items, ValueRange, SizeRange
  
  ItemParams == [size: SizeRange, value: ValueRange]
  ItemSets == [Items -&gt; ItemParams]
  ===
  </code></pre>
  
  <p>I would like to set the following in the cfg file:</p>
  
  <pre><code>SPECIFICATION Spec
  
  CONSTANTS
      SizeRange = 1..4
      ValueRange = 0..3
      Capacity = 7
      Items = {"a", "b", "c"}
  </code></pre>
  
  <p>But this causes the following error:</p>
  
  <pre><code>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 &lt;-, but did not find it.
  </code></pre>
  
  <p>So far I only found this workaround:</p>
  
  <p>.tla</p>
  
  <pre><code>---- MODULE test ----
  EXTENDS TLC, Integers, Sequences
  
  CONSTANTS Capacity, Items, ValueRange, SizeRange
  
  ConstSizeRange == 1..4
  ConstValueRange == 0..3
  
  ItemParams == [size: SizeRange, value: ValueRange]
  ItemSets == [Items -&gt; ItemParams]
  ====
  </code></pre>
  
  <p>.cfg</p>
  
  <pre><code>SPECIFICATION Spec
  
  CONSTANTS
      SizeRange &lt;- ConstSizeRange
      ValueRange &lt;- ConstValueRange
      Capacity = 7
      Items = {"a", "b", "c"}
  </code></pre>
  
  <p>So, it seems useless to define a CONSTANT.</p>
  
  <p>I'm doing something wrong, or is this the expected behaviour?</p>
  
  <p>Thanks</p>