When I first started showing TLA+ to people, the first response was
usually that having to write UNCHANGED statements was such a nuisance;
why not just let there be an implicit unchanged statement for every
variable x for which x' doesn't appear. My answer was that the
UNCHANGED statements represent about 4% of the lines in a large spec
(and those were the simplest lines), and having to write 4% as much
was a small price to avoid the problems that would arise by making the
meaning of an action depend on exactly how it was written. When I
started using TLC, I stopped saying that because having TLC quickly
report an error when I forgot to specify the new value of a variable
in an action was so obviously worth the small effort of writing
UNCHANGEDs.I therefore regard it as obvious that replacing UNCHANGED by a CHANGED
construct is a bad idea. A command to add UNCHANGEDs for a variable
is a less bad idea only because a sensible person could simply not use
it. A better idea is an interactive command that, for each action,
asks you if you want to add the UNCHANGED, giving you a chance to look
at the action and see if the variable should be unchanged. There's
already such a command: a query replace of "UNCHANGED <<" by
"UNCHANGED <<v, ". It seems like that should work pretty well,
especially if the spec had been written with it in mind, so one always
wrote "UNCHANGED <<x>>" instead of "UNCHANGED x" or "x'=x". A more
sophisticated command could do better--especially if it were meant to
be used after all additions to the spec needed to specify changes to
the variables had been made. However, before expending effort to
implement something better, we should know how much better it would
be--especially since this is not something anyone else (including me)
has thought was worth doing. So we need to know how much better than
query replace a new command would be. That requires obtaining data on
real specs of exactly how much effort such a command would
save--especially if Ron Pressler's idea of grouping the variables
(which I often use myself) were used when appropriate. (By the way,
there's no reason why the groups of variables should be disjoint.)
Please send any data on this that you may have to Markus and me.
Leslie
On Thursday, January 10, 2019 at 6:31:49 PM UTC-8, William Schultz wrote: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.