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

[Timi]

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

[Markus Kuppe]

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

> --
> 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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ce26738c-ab85-4d9f-b6b3-61d59ce884b5n%40googlegroups.com.

[Hillel Wayne]

Hi Timi,

Simulation mode runs forever, you have to cancel it manually.

H

[Timi Adeniran]

Thank you both for your responses.

Markus - I'm running the model checker on the linked spec now and will see how long it takes.

Hillel - That's good to know. I had heard a speaker say it ran faster with simulation mode, but I now realize he just meant it found errors quicker.

Thank you once again.

Timi

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/5gaUCiXyvd4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8szDpHKaZESG4dsbwgDQv_h2AJscMVmpFZTf5G1Ln8u5_g%40mail.gmail.com.