Hello
Stephan, can you please give some more comments on this paragraph (p. 38) (the second part of it, starting from "We can either move all definitions....):
We encounter the same problem here that we encountered in checking con-
dition (4.11) for the SendSet example. We would like to put these requirements
in module SendSetUndoP (Figure 10), right before the declaration of the vari-
able p. However, TLC can't check the theorem in a model for that speci fication
because SpecU does not specify the values of variable p. We can either move
all the de nitions that are now in SendSetUndoP before the declaration of p
into a separate module, put them at the end of module SendSetUndo, or end
the module before the declaration of p by adding "=====" when checking the
condition.
and what does it mean: ending the module by adding "====="
Thanks in advance. Alex.