Re: [tlaplus] Q on prophecy vars again

Thanks. it helped.

Now i see, this is just a trick (partially hiding the module def) to make TLC check necessarily conditions.

вторник, 7 апреля 2020 г., 11:18:40 UTC+3 пользователь Stephan Merz написал:

Hello,

TLA+ considers a line "======" (at least 4 "=" symbols) as an end marker for a module: anything following that line is not considered to be part of the module. The objective in the text that you cite is to check a condition that ensures the validity of

SpecU => \EE p : SpecUP

The condition appears in module SendSetUndoP, which extends module SendSetUndo where SpecU is defined. Module SendSetUndoP also declares the variable p and defines the formula SpecUP, which is later used to check refinement of the high-level specification (defined in module SendSet). Note that we cannot have the declaration of p visible when checking the validity condition.

So we could have split module SendSetUndoP in two, with the first part introducing the operators required to define the validity condition and the second part (in a separate module) declaring the variable p, defining SpecUP, and checking refinement. Instead, we put everything in a single module, but only make the first part visible (up to but excluding the declaration of p) for checking validity. Inserting the line "=====" is just a hack so that TLC only sees the first part of the module.

Hope this is clearer.

Regards,
Stephan

On 6 Apr 2020, at 17:20, Alex Tim <alex....@xxxxxxxxx> wrote:

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

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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7fb85549-032e-4bcc-a0ab-b79ffd3d34f4%40googlegroups.com.