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.
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/9F4BC7A9-FA9B-4407-94DA-6A6DE7E1FF16%40gmail.com.