Struct CompetitiveSelectionSoft 

pub struct CompetitiveSelectionSoft {
    pub extra: Vec<u64>,
    pub scores: Vec<u64>,
    pub weight_total: u64,
    pub max_score: u64,
}

Soft competitive selection: weights derived from an evolving extra via the reserved-floor sequential Webster award process, not chosen freely.

Fields

extra: Vec<u64>

Extra Webster awards by candidate index.

scores: Vec<u64>

Candidate scores by candidate index.

weight_total: u64

Total weight available for assignment.

max_score: u64

MaxScore for this refinement profile.

Implementations

impl CompetitiveSelectionSoft

pub fn weight_at(&self, i: usize) -> u64

Executable accessor for the derived weight (1 + extra[i]).

pub fn assigned_weight(&self) -> u64

Number of units currently assigned, including one reserved unit per candidate.

pub fn init( scores: Vec<u64>, weight_total: u64, max_score: u64, ) -> CompetitiveSelectionSoft

TLA+ Init: scores are mutable state and every candidate begins with only its reserved unit. Unlike new, this does not run the award process to Terminal; it exposes the action-level carrier state.

pub fn new( scores: Vec<u64>, weight_total: u64, max_score: u64, ) -> CompetitiveSelectionSoft

Construct the reserved-floor sequential Webster allocation over scores: one guaranteed unit per candidate, then Pool further units awarded one at a time to the current highest-priority candidate. Mirrors CompetitiveSelectionSoft.tla’s Init + AssignNext exactly.

pub fn assign_next(&mut self) -> usize

Award one further pool unit (TLA+ AssignNext, one step): re-establishes every invariant that holds at every reachable state (ScoreOrderPreservation, TieBoundedness, UniversalContribution); Normalization only holds once the pool is exhausted, matching the TLA+ construction exactly.

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

CompetitiveSelectionSoftMutableScores UpdateScore(c,v): update one mutable score and invalidate the partial apportionment in the same commit by resetting every extra award to the reserved floor.