TLA+ spec for safekeeper membership change

[arssher]

Problem

We want to define the algorithm for safekeeper membership change.

Summary of changes

Add spec for it, several models and logs of checking them.

ref #8699

[github-actions]

7095 tests run: 6797 passed, 0 failed, 298 skipped (full report)

---

Flaky tests (3)

Postgres 17

• test_timeline_archival_chaos: release-arm64

Postgres 15

• test_logical_replication: release-arm64
• test_lr_with_slow_safekeeper: release-arm64

Code coverage* (full report)

• functions: 31.3% (8401 of 26877 functions)
• lines: 48.0% (66681 of 139059 lines)

* collected from Rust tests only

---

_{The comment gets automatically updated with the latest test results
5c8aee7 at 2024-12-30T15:45:59.103Z :recycle:}

[problame]

Initial review of everything reachable from Next and invariants.

As with static spec, there are no liveness invariants, right?

Let's have a meeting on my questions on >= vs = in StartChange/FinishChange/AbortChange . I think I'm not seeing something / misunderstood the simplifications.

By the way should document the spec's simplifcations at the top, simliar to how we do for static config.

[arssher]

Addressed all comments, please have another look.

As with static spec, there are no liveness invariants, right?

Yes.

By the way should document the spec's simplifcations at the top, simliar to how we do for static config.

Done.