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

[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.

Andrew

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

--
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.