Optimized PrintT is now in the latest Toolbox daily build

The latest Toolbox daily build can be found here.  It removes most significant bottlenecks in handling large amount of TLC output (e.g., PrintT in TLC module).

Another notable change is a new modules node under the open spec node which lists all dependent modules.  This makes exploring dependencies much easier.  It also has "Quick Access..." menu item under Windows which also lists all dependent modules and the spec's models.

Selecting a sub-sequence

The standard Sequences module defines SelectSeq operator which provides a convenient way of selecting sequence elements that satisfy some condition.  However, when working with sequences, it is more practical to select a set of indices of the elements instead of elements themselves.  Having a set of indices, selected by SelectIdx operator, allows easily modify the original sequence, as shown below.

Composing TLA+ specs from modules

Suppose we have a system consisting a Client, a Device, and a Server. The Client talks to the Device, the Device communicates with the Server.   Naturally, we would have 3 TLA+ modules, one for each system component.

What's the best way to compose the modules into a final spec?

One way is to instantiate the Device from the Client module, and the Server from the Device module.  But TLC model checker does not deal with existential quantifiers of temporal logic:  the Device would have to accept the Server's variables as parameters so that it could pass them to the Server when instantiating the Server module.   It means the Device would have to declare variables that it does not use.

In reality, the Device does not need to know about the Server.  All it needs to know about is communication channels between the Client and the Server.  We can instantiate both the Device and the Server in the Client module, as shown below.  In this case the Device does not need to declare Server's variables and accept them as parameters.  This makes the spec cleaner.  As a bonus, Next step action reminds us at the top level which variables are not used by the Device and by the Server.

From practical point, a module's interface consists of constants and variables that it accepts as parameters,  TypeInvariant operator, and the Next step action.  In even cleaner approach, we could create a Test module and declare all the required variables there.  Then we could instantiate Client, Device, and Server modules from Test module, passing the required parameters.  Then we could compose Test's TypeInvariant and Next step action using the instantiated modules.  When modules are independent of each other, it is easier to test each module separately as described in this post.

Test your specs!

A practical advice: when specifying a large system, use modules and TLA+ support for module instantiation.  Split the system into logical components, map each component to a TLA+ module.  Create a test module for each component module.  Instantiate a component module within a test module. Create a model and run it to test the instantiated component module.

This helps a lot with finding specification bugs early in the process.

At the very minimum test type invariants. Test modules do not need to be complicated, just something simple like shown below.

Reducing number of fields in a record set

The TLA+ definition of records as functions makes it possible to manipulate records in ways that have no counterparts in programming languages.  For example, we can define an operator S such that S(r, s) is a record obtained from r by removing each field that is also a field of the record s:

S(r, s) == [ x \in (DOMAIN r \ DOMAIN s) |-> r[x] ]

Now, if we have a set of records defined as

Rec1 == [a : Nat, b : Nat, c : Nat, d : Nat]

we then can define another set of records that have all fields of records in the set Rec1, except the field b, as

Rec2 == { S(r, [b |-> {}]) : r \in Rec1 }

This is quite handy when records in Rec1 have many fields.