Could I estimate how long will it take for TLC to finish checking a model?

[jarr...@gmail.com]

Diego Ongaro presents a TLA+ specification for raft protocol in his PHD thesis.
The spec is complex so I run it in a linux server with 20 threads in parallel. But it still takes too long to finish.
Actually, I think it will never stop. I mean it is unacceptable if it takes a month or a year.
Is there any way to know how long will it take for TLC to finish checking a model?
Or how can I decrease the time it takes?

PS: symmetry sets optimization does not help.

[Stephan Merz]

Here's what Diego Ongaro says in the thesis (section 8.2):

> We attempted to use the TLA model checker on our specification. We found bugs in creating the specification this way but abandoned this approach because it did not scale well to larger models.

I understand that as saying that there is not much point in running TLC on his spec because all the "easy" errors have already been found, and the state space is too big for computing all states, even under stringent constraints. However, it may still be useful to run TLC on a restricted spec in order to explore specific situations.

There was a presentation on Raft in the DrTLA series [1], which includes some remarks on model checking the TLA+ specification of Raft. Did you have a look?

Hope this helps,
Stephan

[1] https://github.com/tlaplus/DrTLAPlus

> --
> 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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[jarr...@gmail.com]

Great ! It helps me a lot ! Thank you very much!