Re: [tlaplus] How can I speed up model checking for this revised TLA+ spec of Raft?

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Jack Vanlightly recently created https://github.com/Vanlightly/raft-tlaplus

> On Jun 29, 2022, at 2:26 PM, Timi <oluwatimilehinadeniran@xxxxxxxxx> wrote:
> 
> Hello everyone,
> 
> I'm new to writing TLA+ specifications and my current goal is to model a protocol that extends Raft's leader election algorithm based on some suggestions in the paper.
> 
> I came across this pull request in the raft.tla repository with changes to the original spec, which is supposed to make it easier to run a model checker on the spec.
> 
> However, I'm running the TLC model checker for the revised spec and it's taken over 6 hours so far. I'm running the spec with the following constant values:
> 
>     Server <- {"s1", "s2", "s3"} (Using an ordinary assignment)
>     MaxClientRequest <- 1
> 
> And I've set a state constraint such that: \A i \in Server: currentTerm[i] < 3, which I saw in the Dr. TLA+ video that discusses this revised spec.
> 
> I'm using 12 worker threads, simulation mode, and I've turned off profiling in my model. I'm running it on a 6 Core (12 Logical processors) machine with 64GB RAM. 
> 
> Do you have any suggestions on how I can make this check complete quicker, please, or is > 6 hrs in line with how long I should expect a spec with this many states to take?
> 
> Thanks,
> Timi
> 
> 
> 
> 
> -- 
> 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+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ce26738c-ab85-4d9f-b6b3-61d59ce884b5n%40googlegroups.com.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4550FCD6-16B6-4E53-8818-E3BDB5497162%40lemmster.de.