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.
Regards,
Stephan
[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.