tla-plus: add spec for raft leader election

This commit adds a new TLA+ specification (expressed in PlusCal) called
RaftLeader. RaftLeader is a specification for the Raft leader election
protocol, as described in section 3.4 of the Raft thesis[^1]. The spec
models multiple terms, node restarts, and the Pre-Vote election phase
extension.

The central safety property of leader election is exclusivity. In Raft,
this is defined as the Election Safety Property: "at most one leader can
be elected in a given term". This property is defined as an invariant of
the spec.

My goal is to use this spec to verify the correctness of leader-leases.
We can start with this simpler spec and then extend it to include
notions of store liveness and of leases associated with leaders. From
there, we can define the lease disjointness invariant and prove that it
holds.

[^1]: https://web.stanford.edu/~ouster/cgi-bin/papers/OngaroPhD.pdf

Epic: None
Release note: None

docs/tla-plus/LeaderLeases/RaftLeader.cfg

@@ -0,0 +1,29 @@
+SPECIFICATION
+  Spec
+
+CONSTANT
+  Nodes = {n1, n2, n3}
+  Terms = 3
+
+  StateFollower     = StateFollower
+  StatePreCandidate = StatePreCandidate
+  StateCandidate    = StateCandidate
+  StateLeader       = StateLeader
+
+  MsgVote        = MsgVote
+  MsgVoteResp    = MsgVoteResp
+  MsgPreVote     = MsgPreVote
+  MsgPreVoteResp = MsgPreVoteResp
+  MsgApp         = MsgApp
+  MsgAppResp     = MsgAppResp
+
+  WithRestarts = FALSE
+  UsePreVote   = FALSE
+  SendMsgApp   = TRUE
+
+INVARIANT
+  TypeInvariants
+  LeaderExclusivity
+
+SYMMETRY
+  Symmetry