Is there a way to add invariants as in the GUI?

tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code

MIT License

356 stars 32 forks source link

Is there a way to add invariants as in the GUI? #310

Closed erlingrj closed 1 year ago

erlingrj commented 1 year ago

Hi, thanks for this really nice plugin. I am learning TLA+ and PlusCal and in the guides we defined invariants as part of the PlusCal and then use the GUI to mark them as invariants. Is there a way to achieve something similar here?

I am also open to pluscal or TLA+ tips. Whats the best way of expressing an invariant in pluscal? Maybe having a label at the end of the algorithm which thus will be part of every state of the spec?

begin
  ... algorithm
  VerifyInvariant:
    assert Invariant;

lemmy commented 1 year ago

The VSCode extension does not have a model editor. You will have to write TLC's configuration files by hand
An invariant is true in every state, but only asserted at the label VerifyInvariant in your example. Define your invariant in PlusCal's define block or after its TLA+ translation, and add INVARIANT Invariant in TLC's configuration file

erlingrj commented 1 year ago

Great! Thanks. For any other noobs with the same questions. When you run the TLC with TLA+: Check model with TLC TLC will auto-generate a .cfg file with the same name as your .tla file. In this file you can add the INVARIANT MyInvariant at the bottom and for any consecutive runs of TLC it will also check that invariant.

Thanks @lemmy!