Struct SteadyErrorPath 

pub struct SteadyErrorPath<'a> {
    steady_paths: Vec<SteadyPath>,
    step_transitions: Vec<SymbolicTransition>,
    error_graph: &'a ZCSErrorGraph<'a>,
}

Type that represents a steady error path

A steady error path consists of a sequence of steady paths π_0, … , π_k and a sequence of symbolic transitions r_0,…,r_{k-1} where ∀ 0 < i \leq k: π_i is reached by applying rule r_{i-1} from π_{i-1}

Fields

steady_paths: Vec<SteadyPath>

step_transitions: Vec<SymbolicTransition>

error_graph: &'a ZCSErrorGraph<'a>

Implementations

impl<'a> SteadyErrorPath<'a>

pub fn new(steady_path: SteadyPath, error_graph: &'a ZCSErrorGraph<'_>) -> Self

creates a new Steady Error Path for a given SteadyPath

pub fn get_last_states(&self) -> ZCSStates

returns the last SymbolicState of the last steady path

pub fn get_last_assignment(&self) -> SymbolicVariableAssignment

returns the last SymbolicVariableAssignment of the last steady path

pub fn add_successor( &mut self, step_transition: &SymbolicTransition, steady_path: SteadyPath, )

adds a new steady path to the steady error path that is reached with the given transition rule

pub fn is_non_spurious( &self, reached_error_state: bool, smc_ctx: &ZCSModelCheckerContext<'_>, ) -> SpuriousResult

checks if the steady error path is non-spurious

reached_error_states indicates if the last steady path reached an error state

pub fn length_configurations(&self) -> u32

returns the length of different contexts that is defined by the number of steady paths

pub fn concrete_rules_ordered( &self, ta: &'a IntervalThresholdAutomaton, ) -> impl Iterator<Item = &'a Rule>

returns an ordered iterator over all applied rules including the step rules

pub fn steady_paths(&self) -> impl Iterator<Item = &SteadyPath>

returns an ordered iterator over the steady paths

pub fn last_is_monotonic(&self, ta: &IntervalThresholdAutomaton) -> bool

returns if the last steady error path is monotonic i.e., if for every shared variable the value is either only increasing or only decreasing

Trait Implementations

impl<'a> Clone for SteadyErrorPath<'a>

fn clone(&self) -> SteadyErrorPath<'a>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'a> Debug for SteadyErrorPath<'a>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for SteadyErrorPath<'_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.