Struct ACSIntervalState 

pub struct ACSIntervalState {
    v_to_interval: Vec<ACSInterval>,
}

Assignment of variables to their current value

An interval state represents a valuation of the shared variables of a threshold automaton with interval abstraction.

Use this type with care. IntervalStates of different automata should never be indexed by variables or intervals of other automata.

Fields

v_to_interval: Vec<ACSInterval>

Intervals of the configuration Index of the entry represents the variable

Implementations

impl ACSIntervalState

pub fn into_iterator_variable_interval( &self, ) -> impl Iterator<Item = (CSVariable, ACSInterval)>

fn new_cfg_all_zero_interval(ta: &ACSThresholdAutomaton) -> Self

Create a new interval configuration where all variables are in the interval mapped to zero

The resulting configuration of this function should not be used directly as it does not necessarily correspond to a valid configuration. It should only be used for initialization purposes.

pub fn all_possible_interval_configs( ta: &ACSThresholdAutomaton, ) -> Vec<ACSIntervalState>

Compute all interval states that are possible in the threshold automaton

pub fn get_target_interval_configs( constr: IntervalConstraint, ta: &ACSThresholdAutomaton, ) -> Vec<ACSIntervalState>

Compute all interval states that are allowed by the given interval constraint in the threshold automaton

pub fn compute_all_predecessor_configs( &self, rule: &CSRule, ta: &ACSThresholdAutomaton, ) -> Vec<Self>

Compute all potential predecessor interval configurations

fn compute_possible_interval_state_before_application_of_act( &self, act: &CSIntervalAction, ta: &ACSThresholdAutomaton, ) -> HashSet<Self>

Compute all possible interval configurations before the application of the action

Concretely, for

• Increment actions: The increment could have lead to jumping to the next interval, or could have stayed in the current interval.
• Decrement actions: The decrement could have lead to a jump to a smaller interval or could have stayed in the current interval.
• Reset actions: A reset will always go to the 0 interval.

pub fn display(&self, ta: &ACSThresholdAutomaton) -> String

Get a string representation of the interval state

pub fn display_compact(&self, ta: &ACSThresholdAutomaton) -> String

Get a string representation of the interval state, leaving out variables in their zero interval

Trait Implementations

impl Clone for ACSIntervalState

fn clone(&self) -> ACSIntervalState

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ACSIntervalState

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

Formats the value using the given formatter.

impl Hash for ACSIntervalState

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Index<&CSVariable> for ACSIntervalState

type Output = ACSInterval

The returned type after indexing.

fn index(&self, var: &CSVariable) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<CSVariable> for ACSIntervalState

type Output = ACSInterval

The returned type after indexing.

fn index(&self, var: CSVariable) -> &Self::Output

Performs the indexing (container[index]) operation.

impl IndexMut<&CSVariable> for ACSIntervalState

fn index_mut(&mut self, var: &CSVariable) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl IndexMut<CSVariable> for ACSIntervalState

fn index_mut(&mut self, var: CSVariable) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl Ord for ACSIntervalState

fn cmp(&self, other: &ACSIntervalState) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for ACSIntervalState

fn eq(&self, other: &ACSIntervalState) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for ACSIntervalState

fn partial_cmp(&self, other: &ACSIntervalState) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl PartialOrder for ACSIntervalState

fn part_cmp(&self, other: &Self) -> PartialOrdCompResult

fn is_greater_or_equal(&self, other: &Self) -> bool

Check whether self is greater or equal to other in the partial order

fn is_smaller_or_equal(&self, other: &Self) -> bool

Check whether self is smaller or equal to other in the partial order

impl Eq for ACSIntervalState

impl StructuralPartialEq for ACSIntervalState