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

• Date: Wed, 29 Jun 2022 14:31:27 -0700
• Ironport-data: A9a23:LpHo+a3qrAB2NlFwP/bD5Sl0kn2cJEfYwER7XKvMYLTBsI5bpzFWy 2EfWWnXPqzfNDP1e9lwPYzjoxwAucCGztE1GVBv3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/nOHNIQMcacUsxLbVYMpBwJ1FQywYbVvqYy2YLjW13X6 IuoyyHiEAbNNwBcYjp8B52r80sHUMTa4Fv0aXRjDRzjlAa2e0g9VPrzF4npR5fLatU88tqBe gr25OrRElU1UPsaIojNfr7TKiXmS1NJVOSEoiI+t6OK2nCuqsGuu0o2HKJ0VKtZt9mGt8JJ+ O8ShIbqcgISDKvupOQ7DkNUSD4raMWq+JefSZS+mcmazkmDbGG1hvswUAc5OooX/usxCmZLn RAaAGpVP1bT2qTsmuv9FLUEascLdKEHOKsDvnh4ySzCTvwgSrroY5fyyu907B4ZvOpoONSAQ OkgTBVWQTedPzMVBmY/B5U5k+OliWP4biVD7lmSoMLb5kCPl1EpiOS2aLI5fPSPbN9osmefg FicvEn7GRUqac2bzDa8pyfEaujnxHunAur+DoaQ+v9xi0CI3UQPDBRQUECh5Pi/kE+3HdNZM U0dvCQ0xZXe72SuR9j5GgKi+TuK4EJaVN1XHOk3rgqKz8I4/jp1GEAWdg57N+087vQzfg4s9 GOJuY6zCWdw5ej9pW2myp+Yqja7OC4wJGAEZDMZQQZt3zUFiNFj5v4oZoYzeJNZnuEZChmrn G/X9HlWa6E7yJ9Uh//irDgrlhr1/sCRJjPZ8Dk7SY5M0++UTIusZojt9kKCqPgecMCWSV6Ou HVCkM+bhAzvMX1vvHPWKAnuNOvxjxpgDNE6qQIwd3XG32jyk0NPhagKvFlDyL5Ba67ogwPBb k7Joh9275ROJnasZqIfS9vvVpp3l/e8To6/C6+8gj9yjn5ZJF/vEMZGNR744owRuBVEfVwXY srELZ73UR7294w+nGLmF4/xLoPHNghnnT+JLXwK5xug1rWaaRaopUQtYTOzghQCxPLUyC2Mq 4g3H5LTm313DbOiCgGKrtZ7BQ1afBATWMGqw+QKJ77rClQ8RAkJVaSKqZt/INMNokigvregE oeVBxcHkTISRBTvcm23V5yUQOqxB8kn8CJiYHJE0JTB8yFLXLtDJZw3L/MfFYTLPsQ5pRKtZ /VaKciGHNpVTTHLp2YUYZXn9dIwexOsigaDMDCifSAkOZVnQlWRqNPjewLu8ggIDza25Jtl+ OT7iV2ETMpRXRlmAebXdOmrkwG7s08blb8gREDPONRSJBjh/dEyeSz8h/M6Oe8WLhDHymfI3 gqaG05B9+3Apoou7NTTw6yJ9t/7H+x7F0tcPm/a8bfvaXiEpDX+m9cYXb/RLz7HVW7y9KGzX slvzqnxYK8dgVJHk4tgCLI3n6gw0N3i+u1BxQN+EXSXMlmmB+o7cHmL1MVCrJdA3rtIpQyyV h7d89VWI+zXasziF1EVKQU/afmbzrcfnTyLtaY5J0Dz5SlW+rubUBQCZELV03MDc7YlYpk4x eoBudIN71DtgBQdNNvb3Dtf8H6BLyBdXqgq6sMaDYvshlZ5w11Oe8aHWCr/4ZXKdM8Vd0d0f nmbg63Ng7kazU3HKiJhGX/I1OtbpJIPpBEakwNYdgrRwoLI1q0twRlc0TUrVQAJnB9J5OR+Z zpwPEpvKKTSojpl1ZpHXnuwJgdaGRed9hCjwlcFjjOJHUyhV2jRKz8yPuGC+E0W6WVBZiMe+ biewWnoEm21LJCtg3ViBhc89b/+S8ds/BbJgsGtEuyKGJ41ZTfqmKizfXFOoBziWJtjiErCr Ohs3eBxdayqZXVL+vZkVdaXheYKVRSJBG1eWvU9rqkHKmfRJWOp0j+UJkHtJ85AK6CY+EO0E ZA/dMJTSwylhmHJoSocGLYXZbBzm/Et6ZwJfbasKnQBrqPYsj5gqJbN7W/lmWUwSM9vm8swJ 9+DbT6ECWDM13JYl3WX95tBM2u8JMYePUjygrzz/+IOGJYO9uprdBhqgLezunyUNiph/g6V7 FyfPf6Il7Q6xNQ+hZboH4VCGx6wdYH5WtOO/V3hqN9Jd97ObZrDug59RoML5OiK0Wb9muibl IhhdPby1ULB+aksCiXXxcXHGK5O6sG/GuFQN6ob6ZWccTSqAKfRD9kroghU6qClVPtS4c6oQ wa3csytbcVTUNBYrJGQQzYLCA4TUswbcY+5zR5QbJ2w5tw13gvAI9eq+mXucHlAMCQPPvUSz +MyV+mGvrhlkWiHOPPI6zyKzXO1zJ8PlJbKr+HMiAQ=
• Ironport-hdrordr: A9a23:MSFdrapkZOUBTbpGmD8AwkYaV5qJeYIsimQD101hICG9Lfb15r iTdaUguG6MtN9OYhtQ/+xoWZPwPk80kKQb3WB/B8bTYOCLghrVEGgm1/qW/9UPcxeOt9K0+8 9bAuZD4Z7LfBJHZf+T2nj2Lz9Y+qjGzEgc7t2uhEuFMzsaH52Inj0JdDpzSXcGDDWubKBRfP Hsgrs91kedlGwsH76G7zs+Lpv+Trvw5dvbiDE9ZiLPgzP+/A9AhoSKYSRxH38lIlZyKHQZkV QtUTaW2k0S2MvLhiM0G1WjjKi/lbDau61+7DzmsLljFtwksHfLFeNccozHhik8pKWE6Vohkt XA5zcme+pp7W/JF1vF7CfQ5w==
• Ironport-sdr: xgtrpX2tcNcKo1z38INKeJLOvu8XoMTkEJzauHzpI0fM1aVgnYg/Foesy2hXlOOOtRGnPH+5LK JkGBPPvlZAKon2DCkv6jBtrbh5xvvoMxpwBmn1JGsWq87KnOizvWPF0sFtvEeevhPgoSyvP9vl NFBduJBcwlEzkB5l/dNExBjWhJOQKqkpCX7icAFdn0TJnziV9N47ZE84sIW5ZhyfNbNI5U5dGw F8wLEXqzfaW/ugaqeemUygH1gdVlIWX7OU+I/dhfIdB+3ReGQx0ivO1Numcd+UjqeM8hrDqvt2 vheLjC3LH/R1AEWTBLcAkHXj

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

> On Jun 29, 2022, at 2: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.