Re: A few issues with TLC

[Leslie Lamport <tlapl...@xxxxxxxxx>]

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 the

next release, a workaround is to replace the _expression_ exp that is

the right-hand side of the definition by TLCEval(exp), where TLCEval

is 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
something like

   <<x, y, z>>' = <<A, B, C>>

instead of

   (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.

Leslie Lamport