Struct Sequential 

pub struct Sequential {
    pub steps: usize,
    pub value_domain_size: u64,
    pub pc: usize,
    pub value: u64,
    pub active: bool,
    pub history: Vec<u64>,
}

Totally ordered execution owner.

Fields

steps: usize

Total number of steps.

value_domain_size: u64

Exclusive upper bound of carried values.

pc: usize

Program counter identifying the next step.

value: u64

Current carried value.

active: bool

Whether the current step is active.

history: Vec<u64>

Values committed by completed steps.

Implementations

impl Sequential

pub fn new( steps: usize, value_domain_size: u64, initial_value: u64, ) -> Sequential

Construct an inactive execution at the first step.

pub fn begin_step(&mut self) -> bool

BeginStep, with disabled calls exposed as a stuttering rejection.

pub fn complete_step(&mut self, next_value: u64) -> bool

CompleteStep, including its nondeterministic ValueDomain choice as an explicit caller value. An out-of-domain choice is not an enabled TLA+ action and therefore stutters with false.

pub fn done_stuttering(&mut self) -> bool

DoneStuttering: enabled exactly at the terminal inactive state and never changes carrier state.