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