Dear Giuliano,The bug you reported has been fixed in the code, and the fix will
appear in the next release. It does appear to be the same bug as the
one reported earlier. This was a saerious bug that could, in rare
cases, could cause TLC to incorrectly evaluate the spec. Until thenext release, a workaround is to replace the _expression_ exp that isthe right-hand side of the definition by TLCEval(exp), where TLCEvalis defined in the TLC module.
You also had two requests. The first was:
TLC cannot evaluate x' = something when x is not a variable
and it would be handy to do it when x it is a sequence or record
composed of variables for example.
It appears to me that all this would achieve is allowing you to write
<<x, y, z>>' = <<A, B, C>>
(x' = A) /\ (y' = B) /\ (z' = C)
This doesn't save any significant amount of effort, and it would
encourage people to write things lik
(x + 1)' = x
which TLC couldn't possibly evaluate because it doesn't uniquely
specify the value of x'.
You also wanted to allow the suppression of the error when TLC finds
UNCHANGED x when evaluating an action in which x' has been assigned a
value. It seemed to me that in your example, this would have saved
you from writing
(x' = x) /\ UNCHANGED vars2
instead of UNCHANGED <<vars2, x>>. This doesn't seem sufficient
reason to introduce a new TLC option.