Re: [tlaplus] TLC does not finish, how to debug

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 03.08.2018 14:02, jakub....@xxxxxxxxx wrote:
> 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.

Hi,

you should verify that your model is actually finite? If your spec has a
variable modeling a "clock ticking to infinity", TLC has no chance to
ever (exhaustively) check the complete state space. Use a state
constraint (advanced options page of the model editor) to restrict the
possible states or a definition override to redefine e.g. Nat to 1..3.

To make TLC go faster and scale to larger state spaces, you might want
to watch the talk on large scale model checking [1].

It would help if you could share your spec with us.

Hope this helps
Markus

[1] https://www.youtube.com/watch?v=zGIK2p6csAo