[tlaplus] Hiding variables with TLC

[Michael Chonewicz <wawrzynchonewicz@xxxxxxxxx>]

Hello. I am a beginner and I'm writing a specification of a large system. Coming from programming, I naturally want to divide it into multiple files to avoid ending up with a 1k+ lines monstrosity. 

My idea is to somehow replicate object oriented programming, by letting a module represent an object (for example a Queue) and then using the INSTANCE operator whenever I need an instance of that object. This introduces a problem- every time i do this, i need to redeclare variables used in the object in the current module like so:

VARIABLES msgQueue, queueOut

LOCAL MsgQueue == INSTANCE Queue WITH out <- queueOut,
    Values <- Messages, NoValue <- NoMessage, q <- msgQueue

If i want 5 queues in my current module i need to redeclare 10 variables.

Using the existential quantifier \E for hiding variables doesn't work when using TLC. But checking my specification is the primary goal of writing it. Is there an easier way of doing this?

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.