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

*From*: David Bakin <david@xxxxxxxxxxxxxxx>*Date*: Mon, 4 Jul 2022 16:51:15 -0700 (PDT)

I'm learning TLA+ by reading

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.

**Follow-Ups**:**[tlaplus] Re: Hidden variables (via existential quantifier bold-∃)***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Reevaluations of operators in TLC** - Next by Date:
**[tlaplus] Re: Hidden variables (via existential quantifier bold-∃)** - Previous by thread:
**Re: [tlaplus] Pluscal-2** - Next by thread:
**[tlaplus] Re: Hidden variables (via existential quantifier bold-∃)** - Index(es):