[tlaplus] (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)

How do I limit the state space of the model checker?

I am implementing a logical clock and attempting to verify that the clock operates as expected... that the

clocks always increment, and that this property holds:

\A s,t \in S : s->t => clock[s] < clock[t]

The logical clock is described by:

clock, \* each clock has it's current value
inbox, \* each clock process has a msg inbox (queue)

And reasoning about the clock is aided by these auxillary/ghost variables:
    read,                       \* messages that the process has read from inbox
    sent,                       \* each clock process has a history of sent changes
    clock_h                   \* each clock has a history of value changes

Running this model with 1 process is straight forward (3 states):

CONSTANT Proc = { p1 }

CONSTANT MaxValue = 2

But when I increase the number of processes to 2, the state space explodes (I stopped after

1,349,853 states):

CONSTANT Proc = { p1, p2 }

CONSTANT MaxValue = 2

I've written this up in much more detail here (see solution 2).

My implementation doesn't seem that different from the LamportMutex example here.

So my question is, what's the idiomatic way to write a spec such that the state space of the actual spec

remains small enough to be useful/tractable etc.? Am I miss-using auxillary/ghost variables? Should they

be put in a separate spec? Or am I misunderstanding something more fundamental ?

-Todd

p.s. Markus K. thank you for the pointer about not using Print|PrintT in my last email.