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


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.