| 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] <= MaxClock
as 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]) <= MaxChannel
Of 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.
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
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.
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.
|