This commit updates the ParallelCommit spec with a .cfg config file
which mirrors its Toolbox .launch file. This allows the spec to be
checked with the command-line version of the TLC model checker. As
a result, this allows the spec to play well with the VSCode TLA+
extension, which is more popular and easier to use than the original
eclipse-based TLA+ Toolbox.

Epic: None
Relase note: None

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