A few issues with the Raft spec

[heidihoward]

There seems to be a few issues with the Raft spec in this repo.

(1) The quorums in the APAraft.tla should be subsets of the servers but they are not.

https://github.com/informalsystems/apalache-tests/blob/2760e1cacb6f6f8d2c8f89ee0b69a91dee1dcf5d/performance/raft/APAraft.tla#L13

https://github.com/informalsystems/apalache-tests/blob/2760e1cacb6f6f8d2c8f89ee0b69a91dee1dcf5d/performance/raft/APAraft.tla#L21-L32

(2) The invariant OneLeader should be violated at some point. It is possible for multiple servers to believe themselves to be leaders so long as they are in different terms.

https://github.com/informalsystems/apalache-tests/blob/2760e1cacb6f6f8d2c8f89ee0b69a91dee1dcf5d/performance/raft/APAraft.tla#L571

(3) Apalache (version: 0.22.1) will not check this spec without modification due to the following issue:

Assignment error: APAraft.tla:545:15-545:51: Manual assignment is spurious, votedFor is already assigned!

[shonfeder]

Thanks for filing the issue. We'll look into this ASAP :)

[heidihoward]

No worries!

I am happy to help if needs be. I am new to Apalache but I do have experience in checking TLA+ specs of Paxos/Raft using TLC hence why I spotted issues (1) and (2) without running the spec though Apalache during to issue (3).

I also just double checked, and issue (3) also occurs with Apalache version 0.24.0

[konnov]

I think Jure @Kukovec has found a fix for it.

[Kukovec]

re. (3), there are 2 votedFor in
https://github.com/informalsystems/apalache-tests/blob/2760e1cacb6f6f8d2c8f89ee0b69a91dee1dcf5d/performance/raft/APAraft.tla#L401

Basically, Apalache requires exactly 1 assignment (:=) per transition, but it translates UNCHANGED <<a,a>> to

a' := a /\ a' := a

See here for details.

[thpani]

(3) is fixed through #127