Struct CompetitiveSelectionHardExclusive 

pub struct CompetitiveSelectionHardExclusive {
    pub num_seats: usize,
    pub num_candidates: usize,
    pub max_score: u64,
    pub allocation: Vec<Option<u64>>,
    pub scores: Vec<Vec<u64>>,
}

CompetitiveSelectionHardExclusive carrier. Candidate indices are the executable WEnum order, so numeric order is exactly Pos order for deterministic ties. The carrier applies the cross-seat availability filter during argmax selection and globally invalidates the coupled assignment on a score update.

Fields

num_seats: usize

Number of independently allocated seats.

num_candidates: usize

Number of candidates shared by every seat.

max_score: u64

Inclusive score ceiling.

allocation: Vec<Option<u64>>

Selected candidate by seat, encoded as u64.

scores: Vec<Vec<u64>>

Candidate scores indexed by seat and candidate.

Implementations

impl CompetitiveSelectionHardExclusive

pub fn new( num_seats: usize, num_candidates: usize, max_score: u64, ) -> CompetitiveSelectionHardExclusive

Construct empty allocations and zero scores for every seat.

pub fn score_at(&self, s: usize, c: usize) -> u64

Read one in-range seat-candidate score.

pub fn candidate_available(&self, s: usize, c: usize) -> bool

Executable Available(s) membership check.

pub fn has_available(&self, s: usize) -> bool

Executable guard for Available(s) /= {}.

pub fn evaluate(&mut self, s: usize)

TLA+ Evaluate(s): atomically select the lowest-index argmax from the candidates not held by another seat.

pub fn update_score(&mut self, s: usize, c: usize, v: u64)

TLA+ UpdateScore(s,c,v): update one score and invalidate every seat in the same commit because availability couples their optimality.