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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Tue, 5 Jul 2022 07:02:59 -0700 (PDT)*References*: <2854f616-5296-4d2d-9e1a-2812cf652f34n@googlegroups.com>

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.

Andrew

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

I'm learning TLA+ by readingSpecifying 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) discusseshidden 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 acrucial wayin 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 beingreallyused.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/3a3e7dab-5feb-40ef-b429-2af71c113379n%40googlegroups.com.

**References**:**[tlaplus] Hidden variables (via existential quantifier bold-∃)***From:*David Bakin

- Prev by Date:
**[tlaplus] Hidden variables (via existential quantifier bold-∃)** - Next by Date:
**[tlaplus] Simple Question - Safety and Liveness** - Previous by thread:
**[tlaplus] Hidden variables (via existential quantifier bold-∃)** - Next by thread:
**[tlaplus] Simple Question - Safety and Liveness** - Index(es):