[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 specification
because SpecU does not specify the values of variable p. We can either move
all the denitions 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.