Feature Request: `update vars` command

[hwayne]

Motivation

This came up in the Community Outreach meeting as a good potential first "refactoring tool" for TLA+. Given we have the AST, we know 1) all of the variables in the system, and 2) know if vars is an operator. It is also a lot of tedious work to update vars every time we add or remove a variable.

With that in mind, it may be useful to make a VSCode command that automatically updates vars with all variables.

How it works

Given

VARIABLES x, y
+ VARIABLES z
VARIABLES w

vars <<x, y, w>>

The refactoring would be

VARIABLES x, y
VARIABLES z
VARIABLES w

- vars <<x, y, w>>
+ vars <<x, y, z, w>>

Implementation

Probably just a new command like tlaplus.refactor.update_vars

Concerns

Complex var tuples

I often break vars down into subsets of variables:

state_vars == <<a, b, c>>
aux_vars == <<d, e, f>>
vars == <<state_vars, aux_vars, g, h>>

What should the refactor do in this case?

EXTENDS

EXTENDS Foo

VARIABLES x

vars == <<x>>

What if Foo also defines variables? Should those be included in vars?

Would this be a problem for PlusCal?

[lemmy]

/cc @craft095

[lemmy]

TLA+ has a lot of boilerplate. One of the most notorious examples is UNCHANGED rules. Specifications are extremely precise — so precise that you have to specify what variables don't change in every step. This takes the form of an UNCHANGED clause at the end of relevant actions:

RemoveObjectFromStore(srv, o, s) ==
/\ o \in stored[s]
/\ stored' = [stored EXCEPT ![s] = @ \ {o}]
/\ UNCHANGED <<capacity, log, objectsize, pc>>
Writing this is really annoying. Updating these whenever you change an action, or add a new variable to the spec, is doubly so. Syntax checking and error analysis are important for beginners, but this is what I wanted for myself. I took a spec and prompted Claude

Add UNCHANGED <> for each variable not changed in an action.

And it worked! It successfully updated the UNCHANGED in every action.

(Note, though, that it was a "well-behaved" spec in this regard: only one "action" happened at a time. In TLA+ you can have two actions happen simultaneously, that each update half of the variables, meaning neither of them should have an UNCHANGED clause. I haven't tested how Claude handles that!)

https://buttondown.com/hillelwayne/archive/ai-is-a-gamechanger-for-tla-users/

[lemmy]

Updating vars is just one part of the process when adding new variables to a spec. @hwayne, did you intentionally leave out the other aspects—like updating the initial predicate and the next-state relation—because they’re significantly more complex? Or do you see those steps as less essential?

[lemmy]

AI-assisted code completion in Cursor and Visual Studio Code seems quite effective at adding a newly introduced variable to the various UNCHANGED sections throughout a specification.