[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.