Port learntla text to VSCode

[sishtiaq]

TLA+ Toolbox seems clunky. All the cool kids are using VSCode! (And TLA+ is VSCode is nice and useable thanks to https://github.com/tlaplus/vscode-tlaplus.) The learntla text uses TLA+ Toolbox. But there's no direct 1-1 mapping of TLA+ Toolbox screens/fields/commands (and there are a lot of screens/fields/commands there!) to VSCode. As a specific example, it took me a bit of time to figure out where to put duplicates's (just started on your learntla website --- thanks for this) invariants and properties in the duplicate.cfg. Can the learntla text (examples, in particular) be ported to use VSCode instead?

[hwayne]

I teach my classes in VSCode, the problem that keeps me from migrarting everything (besides laziness) is that you can't put negative numbers or sequences as constants in VScode, at least not without some file shenaniganry

[sishtiaq]

ah ok.
I can help with the laziness: if you file tickets here outlining what's to be done, I can pick up some of them. (And easy to do when I'm just starting your series.)
VSCode issues: presumably you've filed them with the extension maintainers? They sound pretty critical to making VSCode a replacement tool.

[hwayne]

The problem isn't with VSCode, it's with TLC. TLC's .cfg format can't accept anything besides basics numbers and sets.

To make constants with sequences or negative numbers, you need to create a separate file called, like MySpecMC.tla, and then INSTANCE MySpec WITH Constant1 <- -1, Constant2 <- <<foo, bar>>, and then define a new MySpecMC.cfg. The Toolbox does this automatically for you.

[hwayne]

Maybe I can make a .. vscode:: directive and use it to call out differences

[sishtiaq]

The problem...'s with TLC. TLC's .cfg format can't accept anything besides basics numbers and sets.
Is there an issue on the TLC repo about this?
Seems like what the Toolbox does is a workaround.

[hwayne]

Update, I've since found that the toolbox is no longer as actively maintained so I will probably have to migrate all examples to vscode anyway

[fgmarand]

Or IntelliJ plugin ? TLC-based too, it seems.

[iinuwa]

For those following along with VS Code and trying to use constants, here are some tips:

(hwayne's previous comment may be an easier way to do this, but I didn't understand quite how to use it, so I copied the steps of what Toolbox does.)

Ordinary Assignment

To assign to ordinary variables for myspec:

1. Add the reference to the constant in myspec.tla:

   ---- MODULE myspec ----
   \* ...
   CONSTANT MyConst
   

2. Create a new spec file in the same folder as myspec.tla called MCmyspec.tla¹. Fill it in with the following data:

   ---- MODULE MCmyspec ----
   EXTENDS myspec \* pulls in all the operators from your original spec
   \* This can be any name or value
   ConstMyConst == "some value"
   =====
   

3. Copy your myspec.cfg file to MCmyspec.cfg, or create a new one with the SPECIFICATION, INVARIANTS, etc. set as you wish. Add an assignment to the CONSTANT from your in this new config file:

   SPECIFICATION
       Spec
   CONSTANT MyConst <- ConstMyConst
   \* ...
   

Make sure to use <- for the ordinary assignment, or you may receive an error:

TLC found an error in the configuration file at line 8
It was expecting = or <-, but did not find it.

or

The second argument of < should be an integer, but instead it is:
ConstMyConst

Also make sure to execute your model from the MCmyspec.cfg or MCmyspec.tla files, rather than the myspec.tla file.

Model Value

If you want to insert a model value, you don't need to create a separate config file (but you can). You just assign the the CONSTANT to itself with the = sign in the config file:

\* myspec.tla
---- MODULE myspec ----
\* ...
CONSTANT NULL
\* ...

\* myspec.cfg
CONSTANT NULL = NULL

Make sure to use the = symbol for model values, otherwise you may get an error:

In the configuration file, the identifier NULL appears
on the right-hand side of a <- after already appearing on the
left-hand side of one.

Hope that helps!

Footnotes

1. MC is for "model checker". The name of the module doesn't actually matter, but this is the convention that TLA+ Toolbox uses, and one of the names that the VSCode plugin will prompt you to use if it doesn't detect any .cfg files. ↩

[hwayne]

For those following along with VS Code and trying to use constants, here are some tips:

(hwayne's previous comment may be an easier way to do this, but I didn't understand quite how to use it, so I copied the steps of what Toolbox does.)

See https://learntla.com/topics/cli.html#config-format for a better description of how to make it work without needing an extra MC file.