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

[David Bakin <david@xxxxxxxxxxxxxxx>]

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

-- 
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/2854f616-5296-4d2d-9e1a-2812cf652f34n%40googlegroups.com.