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

Re: [tlaplus] How to run TLA+ ToolBox model checking from command line?

Hi, Stephan
I run the raft protocol specification from Diego Ongaro's Ph.D. dissertation. Now I use a server and run 20 threads in parallel. After 3 hours, it still keeps running.
How can I estimate how long will it take for a complex spec. Or how to reduce the time consuming? 
PS: The symmetry sets optimization does not help a lot.

Hi Jarry,

at the bottom of the TLA+ tools page [1] you'll find a short description on how to use the tools from the command line. If you have any questions that are not answered there, please come back here.


[1] http://lamport.azurewebsites.net/tla/tools.html

> On 14 Nov 2017, at 13:42, jar...@xxxxxxxxx wrote:
> I write a TLA+ script, but it seems too slow for model checking in my laptop, even in the multithread mode. So I want to run it in a Linux server which do not have a GUI. Anybody know how to run model checking from command line?
> Thx.
> --
> 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...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.