Hello,I didn't find your TLA spec in your GitHub repository, but since it includes logical clocks that get incremented repeatedly, I am assuming that you use a state constraint for bounding the clock values? (You mention MaxValue but do not indicate how it is used.) For example, you could add\A p \in Proc : clock[p] <= MaxClockas a state constraint for a suitable value of MaxClock (Additional spec options -> State Constraint in the TLC Toolbox pane). Similarly, you are appending clock values to sequences (inbox and sent) [1] and you will probably have to bound the length of these sequences using constraints such as\A p \in Proc : Len(inbox[p]) <= MaxChannel /\ Len(sent[p]) <= MaxChannelOf course, with these constraints TLC will not explore the full (infinite) state space of the model but you gain confidence because the set of states that can be reached while respecting these constraints is explored exhaustively. Use engineering judgment for choosing the bounding constants, looking for a compromise between what TLC can handle and what part of the state space you believe should be explored in order gain confidence.Stephan[1] By the way, the text is ambiguous about whether you mean to append clock[self] or clock[self]+1.On 22 Apr 2020, at 02:53, Todd Greenwood-Geer wrote: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 theclocks 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 changesRunning 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 = 2I'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 specremains small enough to be useful/tractable etc.? Am I miss-using auxillary/ghost variables? Should theybe put in a separate spec? Or am I misunderstanding something more fundamental ?-Toddp.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. -- 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/CBC7C298-D53A-46EB-AD60-5B779E27387E%40gmail.com.