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.