I am modelling a small algorithm with three processes and several steps. Even with small input, the model checker does not finish - number of states and diameter grows with no chance to finish. I _know_ that the algorithm might runaway (e.g. clock ticking to infinity) and I try to predict such conditions when checking the model.
Question: how to debug what happens? What are the standard techniques? Unless an assertion fails, I have no insight in what happens in the model.