Struct IntervalThresholdAutomaton 

pub struct IntervalThresholdAutomaton {
    pub(crate) lia_ta: LIAThresholdAutomaton,
    pub(crate) initial_variable_constraints: Vec<IntervalConstraint>,
    pub(crate) rules: Vec<IntervalTARule>,
    pub(crate) order: StaticIntervalOrder,
    pub order_expr: Vec<BooleanExpression<Parameter>>,
}

Threshold automaton with guards abstracted to sets of intervals

A threshold automaton where a specific order on intervals is defined and the guards are abstracted to sets of intervals in which they are enabled.

Fields

lia_ta: LIAThresholdAutomaton

Underlying linear integer arithmetic threshold automaton

initial_variable_constraints: Vec<IntervalConstraint>

Initial variable constraints as intervals

rules: Vec<IntervalTARule>

Abstract rules of the threshold automaton

order: StaticIntervalOrder

Current interval order

order_expr: Vec<BooleanExpression<Parameter>>

Order expression

Implementations

impl IntervalThresholdAutomaton

pub fn get_initial_interval<'a>(&'a self, var: &Variable) -> Vec<&'a Interval>

Get the initial interval for variable var

pub fn get_zero_interval<'a>(&'a self, var: &Variable) -> &'a Interval

Get the zero interval for variable var

pub fn get_intervals(&self, var: &Variable) -> &Vec<Interval>

Get intervals for variable var

pub fn get_previous_interval( &self, var: &Variable, i: &Interval, ) -> Option<&Interval>

Get the previous interval of i for variable var

Returns None if i is the first interval

pub fn get_next_interval( &self, var: &Variable, i: &Interval, ) -> Option<&Interval>

Get the next interval of i for variable var

Returns None if i is the open interval

pub fn get_derived_rule(&self, abstract_rule: &IntervalTARule) -> &Rule

Get the corresponding concrete rule for a given abstract rule

pub fn get_interval_constraint( &self, constr: &LIAVariableConstraint, ) -> Result<IntervalConstraint, IntervalConstraintConstructionError>

Translate a [LIAVariableConstraint] into an IntervalConstraint in the interval order of the automaton

This function will return an error if the constraint contains a threshold that was not present when the interval order was constructed

pub fn get_enabled_intervals<'a>( &'a self, constr: &'a IntervalConstraint, var: &Variable, ) -> impl Iterator<Item = &'a Interval>

Get the intervals in which the interval constraint is enabled

pub fn get_variables_constrained( &self, constr: &IntervalConstraint, ) -> Vec<&Variable>

Get all variables for which the interval constraint actually constrains the interval a variable can be in

pub fn get_ta(&self) -> &GeneralThresholdAutomaton

Get the underlying threshold automaton

pub fn get_ordered_intervals( &self, var: &Variable, ) -> Result<&Vec<Interval>, IntervalOrderError<Variable>>

Get the interval order for a specific variable

Returns all intervals for variable var in the interval order of the automaton

pub fn get_helper_vars_for_sumvars( &self, ) -> &HashMap<Variable, WeightedSum<Variable>>

TODO: Remove when interval order is ready

Trait Implementations

impl Clone for IntervalThresholdAutomaton

fn clone(&self) -> IntervalThresholdAutomaton

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IntervalThresholdAutomaton

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

Formats the value using the given formatter.

impl Display for IntervalThresholdAutomaton

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

Formats the value using the given formatter.

impl IsDeclared<Location> for IntervalThresholdAutomaton

fn is_declared(&self, obj: &Location) -> bool

Check if object of type T is declared

impl IsDeclared<Parameter> for IntervalThresholdAutomaton

fn is_declared(&self, obj: &Parameter) -> bool

Check if object of type T is declared

impl IsDeclared<Variable> for IntervalThresholdAutomaton

fn is_declared(&self, obj: &Variable) -> bool

Check if object of type T is declared

impl<C: ModelCheckerContext + ProvidesSMTSolverBuilder, SC: TargetSpec> TATrait<C, SC> for IntervalThresholdAutomaton

type TransformationError = IntervalTATransformationError

Error type that can occur when trying to convert from threshold automaton

fn try_from_general_ta( ta: GeneralThresholdAutomaton, ctx: &C, spec_ctx: &SC, ) -> Result<Vec<Self>, Self::TransformationError>

Try to derive the internal threshold automaton representation from a general threshold automaton

impl ThresholdAutomaton for IntervalThresholdAutomaton

type Rule = IntervalTARule

Type of the rules of the threshold automaton

type InitialVariableConstraintType = IntervalConstraint

Type of the initial variable conditions of the threshold automaton

fn name(&self) -> &str

Get the name of the threshold automaton

fn parameters(&self) -> impl Iterator<Item = &Parameter>

Get the parameters of the threshold automaton

fn resilience_conditions( &self, ) -> impl Iterator<Item = &BooleanExpression<Parameter>>

Get the resilience condition of the threshold automaton

fn variables(&self) -> impl Iterator<Item = &Variable>

Get the shared variables of the threshold automaton

fn locations(&self) -> impl Iterator<Item = &Location>

Get the locations of the threshold automaton

fn can_be_initial_location(&self, location: &Location) -> bool

Check if a location can be initial by the location constraints of the threshold automaton

fn rules(&self) -> impl Iterator<Item = &Self::Rule>

Get the rules of the threshold automaton

fn incoming_rules( &self, location: &Location, ) -> impl Iterator<Item = &Self::Rule>

Get incoming rules to a location

fn outgoing_rules( &self, location: &Location, ) -> impl Iterator<Item = &Self::Rule>

Get outgoing rules for a location

fn initial_location_constraints( &self, ) -> impl Iterator<Item = &LocationConstraint>

Get the initial location constraints of the threshold automaton

fn initial_variable_constraints( &self, ) -> impl Iterator<Item = &IntervalConstraint>

Get the initial variable constraints of the threshold automaton

fn has_decrements_or_resets(&self) -> bool

Check whether the threshold automaton contains any decrements or resets

fn has_decrements(&self) -> bool

Check whether the threshold automaton contains any decrements

fn has_resets(&self) -> bool

Check whether the threshold automaton contains any resets