Update CheckQuorum and DropIgnoredMessage in ccfraft.tla

[cjen1-msft]

I found two places where our spec overapproximates the behaviours of CCF.

First CheckQuorum can always trigger on a leader, so in the case of a single nodeconfiguration it can trigger in the spec but never in practise.

Next the DropIgnoredMessage was allowed to drop messages if they were ignored. We specifically don't ignore RequestVote messages from unknown replicas, while this is allowed by the spec.

Both of these were causing false liveness counterexamples in testing of the prevote changes.

[achamayou]

In other words, there must be backups, if only on the horizon, for it to make sense to check quorum at all.

[cjen1-msft]

Not quite, more that the condition will always succeed (thus not triggering checkquorum) unless there is at least one backup. But I'll update the comment to reflect that.

[achamayou]

I think they are the same? "there must be backups" <=> "there is at least one backup"? On the horizon as in, in active configs (but not necessarily committed yet).

[achamayou]

@cjen1-msft when Model Checking, we pass --disable-check-quorum, which goes through here, here and ultimately here.

The simulation is doing some CheckQuorum though.

[Copilot]

Pull Request Overview

This PR fixes two instances where the TLA+ specification over-approximated CCF's behavior, causing false liveness counterexamples. The changes align the specification more closely with the actual implementation by restricting when CheckQuorum can trigger and when messages can be dropped.

• Adds a constraint to prevent CheckQuorum from triggering in single-node configurations
• Prevents DropIgnoredMessage from dropping RequestVoteRequest messages from unknown nodes