[tlaplus] Re: Hidden variables (via existential quantifier bold-∃)

Should be noted that TLC doesn't support variable hiding in that way, so if you're only interested in using TLA+ to model-check your specifications I would not worry about that section. Specifying Systems is a great resource (it's how i learned!) but there are a good number of specs in it that aren't model-checkable.

On Monday, July 4, 2022 at 7:51:15 PM UTC-4 da...@xxxxxxxxxxxxxxx wrote:

I'm learning TLA+ by reading Specifying Systems (2003). (I know that 's an older version of TLA+ but don't think it'll make a difference to this question.)

Section 4.3 "Hiding the Queue" (pg 41) discusses hidden variables. I get why that's an interesting idea esp. w/ modules. But I don't get what's going on when:

1) The inner module (InnerFIFO)'s variable q needs to be mentioned in the outer module (FIFO)'s formula Spec (pg 41) even as just part of the existential quantifier clause, and what's more puzzling:
2) The inner module's variable q is used in a crucial way in the definition of the outer module (BoundedFIFO)'s formula BNext)(q) (pg 43, section 4.4) where the length of the "hidden" queue is used.

Point #1 I guess could be considered something about just the notation used, but point #2 shows the "hidden" variable being really used.

So what's really "hidden" about it?

-- David Bakin