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

--
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/d54894f6-7282-4c29-be50-8cf19439953d%40googlegroups.com.

• Follow-Ups: