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

[tlaplus] Raft Spec Checking problem

From: sadjad tala <sadjadtalakoob74@xxxxxxxxx>
Date: Wed, 30 Sep 2020 02:15:03 -0700 (PDT)

Hello,

I run the raft protocol specification from Diego Ongaro's Ph.D. dissertation. Now I use a server and run thread on 6 core with 25Gb ram. After 3 hours, it still keeps running.

How can I estimate how long will it take for a complex spec. is there any Variants or Liveness property that may help? does anyone got any suggestion?

Thanks a lot.

--
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/ba3fac42-9887-4223-8349-15d338a66281n%40googlegroups.com.

Follow-Ups:
- Re: [tlaplus] Raft Spec Checking problem
  - From: Jack Vanlightly

Prev by Date: [tlaplus] The recording of "Conjunction Capers: A TLA+ Truffle" by Ron Pressler (was: TLA+ community meeting 2020)
Next by Date: Re: [tlaplus] Raft Spec Checking problem
Previous by thread: [tlaplus] Re: Java overflow when using RandomSubset to check inductive invariance
Next by thread: Re: [tlaplus] Raft Spec Checking problem
Index(es):
- Date
- Thread