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

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

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?


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.