Hiding variables with TLC

[Michael Chonewicz]

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?

[Stephan Merz]

Hello,

first of all, it is probably not a good idea to try and faithfully represent the large system that you are interested in TLA+ (but by and large, this advice also holds for other formal specification languages). You will likely find most benefit in using TLA+ for writing high-level specifications of well-chosen parts of your system: the ones that you suspect most likely to contain errors. In particular, verification with TLC suffers from the state explosion problem, and you will probably not be able to verify a system with 5 queues with reasonable effort.

If you are interested in verifying the behavior of queues in your system, take one queue and write an abstract, non-deterministic description of the processes that communicate over the queue. If you are instead interested in the interaction between processes, take two processes linked by one or two (in case of bidirectional communication) queues and strip down the queue protocol to its bare bones. Because TLC computes the full state graph, it has repeatedly found to be very effective for finding bugs in tiny instances of systems whose implementations would exhibit these bugs only in large configurations. In any case, it is best to start small and coarse, and to add components or refine the grain of atomicity only when TLC cannot find problems in the toy specification. Deciding which aspects of your system warrant writing a formal model is a non-trivial decision that requires engineering judgment. Chapter 7 of "Specifying Systems" has some advice.

Encapsulating parts of a specification in separate modules can make a specification more readable, but since specifications tend to be small, it is less of an issue than in programming. (With few exceptions, TLA+ specifications rarely exceed a couple of hundred lines.) And then, redeclaration of parameters is not a big deal.

Regards,
Stephan

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