Struct ACSThresholdAutomaton 

pub struct ACSThresholdAutomaton {
    idx_ctx: IndexCtx,
    interval_ta: IntervalThresholdAutomaton,
    initial_locs: Vec<ACSLocation>,
    initial_intervals: Vec<HashSet<ACSInterval>>,
    rules: Vec<CSRule>,
}

A variant of an [IntervalThresholdAutomaton] allowing for low-memory representations of configurations (by a ACSTAConfig) and efficient predecessor computations

This type is a variant of an [IntervalThresholdAutomaton] that translates variables (see CSVariable), locations (see ACSLocation) and intervals (see ACSInterval) into indices, that can then be used to in ACSTAConfig instead of the corresponding concrete types. The mapping is then maintained in this type.

Additionally, initial location configurations and intervals, as well as rules (see CSRule) are already translated into operations on the abstracted states, such that they do not need to be translated on the fly.

Fields

idx_ctx: IndexCtx

Main index maintaining the mapping of locations, variables and intervals

interval_ta: IntervalThresholdAutomaton

[IntervalThresholdAutomaton] that this threshold automaton is an abstraction of

initial_locs: Vec<ACSLocation>

Initial locations (as ACSLocations)

initial_intervals: Vec<HashSet<ACSInterval>>

Initial intervals (as ACSIntervals, indexed by CSVariable)

rules: Vec<CSRule>

Rules operation on cs types

Implementations

impl ACSThresholdAutomaton

pub fn new(interval_ta: IntervalThresholdAutomaton) -> Self

Create the corresponding ACSThresholdAutomaton from the given [IntervalThresholdAutomaton]

pub fn is_initial_loc(&self, loc: &ACSLocation) -> bool

Check whether the location is an initial location, i.e. processes can start in this location

pub fn is_initial_interval(&self, var: &CSVariable, i: &ACSInterval) -> bool

Check whether the interval i is an initial interval for variable var

pub fn get_zero_interval(&self, var: &CSVariable) -> ACSInterval

Get the zero interval for variable var

pub fn get_all_intervals<'a>( &'a self, var: &'a CSVariable, ) -> impl Iterator<Item = &'a ACSInterval>

Get all intervals for the variable

pub fn get_prev_interval( &self, _var: &CSVariable, interval: &ACSInterval, ) -> Option<ACSInterval>

Get the previous interval

pub fn get_next_interval( &self, var: &CSVariable, interval: &ACSInterval, ) -> Option<ACSInterval>

Get the next interval

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

Get all variables appearing in the threshold automaton

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

Get all ACSLocations of the automaton

pub fn rules(&self) -> impl Iterator<Item = &CSRule>

Get all rules of the automaton

pub fn get_rule_by_id(&self, id: u32) -> Option<&Rule>

Get rule by id

pub fn get_interval_ta(&self) -> &IntervalThresholdAutomaton

Get a reference to the interval threshold automaton the automaton has been derived from

Trait Implementations

impl Clone for ACSThresholdAutomaton

fn clone(&self) -> ACSThresholdAutomaton

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ACSThresholdAutomaton

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

Formats the value using the given formatter.

impl Display for ACSThresholdAutomaton

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

Formats the value using the given formatter.

impl From<IntervalThresholdAutomaton> for ACSThresholdAutomaton

fn from(value: IntervalThresholdAutomaton) -> Self

Converts to this type from the input type.

impl IsDeclared<Location> for ACSThresholdAutomaton

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

Check if object of type T is declared

impl IsDeclared<Parameter> for ACSThresholdAutomaton

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

Check if object of type T is declared

impl IsDeclared<Variable> for ACSThresholdAutomaton

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

Check if object of type T is declared

impl ThresholdAutomaton for ACSThresholdAutomaton

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 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 = &Self::InitialVariableConstraintType>

Get the initial variable constraints 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 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