[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

TLC does not finish, how to debug

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.