[Qian-Cheng-nju]

There is one more quorum assumption missing after #233: a superset of a quorum must still be a quorum.

For example, the existing assumptions allow:

N == {a,b,c,d,e}
F == {d,e}
IsQuorum(Q) == Q \in {{a,b,c}, {b,c,d,e}, {a,b,c,d,e}}
IsBlocking(B) == B \cap {b,c} # {}

Here {a,b,c} is a quorum, but {a,b,c,d} is not. In an 11-transition replay, the three correct nodes vote for the round-1 leader, then d adds a vote. The resulting vote set fails IsQuorum, so a correct node enters round 3 without committing the round-1 leader, violating Liveness.

This states upward closure in Sailfish and checks it in both TLC wrappers. Ordinary threshold quorums satisfy it.

The new assumption rejects the counterexample parameters before initialization. Taking the upward closure of the same quorum family lets the replay complete and commit the leader. The existing TLCSailfish1 model also passes with unchanged state counts.

[lemmy]

/cc ^^ @nano-o