[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Q on prophecy vars again


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

and what does it mean: ending the module by adding "====="

Thanks in advance. Alex.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7fb85549-032e-4bcc-a0ab-b79ffd3d34f4%40googlegroups.com.