When writing larger TLA+ specs with numerous variables I find that maintaining the UNCHANGED statements for each action can become tedious. For example, if I add a new variable to an existing spec that is not changed by most actions, I need to go through every UNCHANGED statement and add it. Using PlusCal may address this kind of pain, but I have not yet used PlusCal to write any specs. I am wondering if there is a relatively simple pattern within TLA+ that will make UNCHANGED statements less tedious to work with and maintain. Consider the following spec snippet:
VARIABLES x, y, z
Action ==
/\ x' = x + 1
/\ UNCHANGED <<y, z>>
When writing an UNCHANGED _expression_ for an action, it is often easier to write down the variables that do change, instead of listing all the variables in the spec and then deleting only those that changed in an action. Also, If I want to add a new variable that is unaffected by Action then I need to go and edit its UNCHANGED statement. I have been thinking about doing something like the following to work around this:
VARIABLES x, y, z
varsTable == [x |-> x, y |-> y, z |-> z]
\* A function equal to 'f' but with the elements in the set 'delete' removed from its original domain.
Without(f, delete) == [s \in ((DOMAIN f) \ delete) |-> f[s]]
Action ==
/\ x' = x + 1
/\ UNCHANGED Without(varsTable, {"x"})
By only writing down the changed variables in the UNCHANGED statement, I don't need to edit this action at all if I decide to add a new variable later on. Also, I find it easier when writing a new action to only think about the variables that changed in that action. If I have 10 variables in my spec, then I need to remember or go find all 10 variables and put them in an UNCHANGED statement. I am curious if others have been similarly bothered by this issue and if there is a better way to go about doing this.