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

*From*: jarr...@xxxxxxxxx*Date*: Sun, 17 Dec 2017 21:56:30 -0800 (PST)

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.

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] How to run TLA+ ToolBox model checking from command line?** - Next by Date:
**Re: [tlaplus] Could I estimate how long will it take for TLC to finish checking a model?** - Previous by thread:
**Re: [tlaplus] Need help to update the state with EXCEPT.** - Next by thread:
**Re: [tlaplus] Could I estimate how long will it take for TLC to finish checking a model?** - Index(es):