Hi Jesse and Igor,
From the description of the algorithm in the Attiya-Welch book, one can see that the algorithm consists of three parts:
1. a broadcast step where process broadcasts its current time,
2. a collection phase where the process collects the messages from other processes and stores intermediate diff values,
3. an evaluation step where the process uses the diffs to compute the adjustment.
Since we assume in this model that the clocks are ticking at the same rate and that messages are always delivered with a delay in the interval [d - u, d], the intermediate diff values and the final adjustment value only depend on d, u, and HC. This fact is captured in Lemma 6.16, which is used to prove Thm. 6.15.
The TLA spec shared by Igor allows the broadcast step to occur spontaneously at any point in time. We can use the property discussed in the above paragraph to argue that it is equivalent to a new spec in which the broadcast step is forced to occur at time 0, for each process. In the new spec, the evaluation step is guaranteed to occur before time d, and thus finite state model checking can be used (picking d, u, HC from finite sets and eliminating time). Model checking is not a good fit for analyzing the new spec: the analysis in the proof for Thm. 6.15 is quite straightforward and verifies the property we are interested in.
The property discussed in the first paragraph allows us to shift events in time so that instead of analyzing a large set of behaviors we can focus our attention on a small set of behaviors. This pattern is a crucial step in the analysis of many real-time models.
Regards,
Abhishek