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

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



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





On Wed, 29 Jun 2022 at 22:35, Hillel Wayne <hwayne@xxxxxxxxx> wrote:
Hi Timi,

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

H

On Wed, Jun 29, 2022 at 4: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 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8szDpHKaZESG4dsbwgDQv_h2AJscMVmpFZTf5G1Ln8u5_g%40mail.gmail.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/CAPCwney4B2HOig_7sjibPzreWUxM4G%3DuPGp5tw_%2BcScAMx5eMA%40mail.gmail.com.