Struct ACSTAConfig 

pub struct ACSTAConfig {
    loc_state: ACSLocState,
    interval_state: ACSIntervalState,
}

Configuration of a ACSThresholdAutomaton

This struct represents a configuration, i.e. an assignment of intervals for all shared variables and a number of processes in each location.

Use these configurations with care. Configurations of different automata should never be indexed by locations, variables or intervals of other automata.

Fields

loc_state: ACSLocState

Location state specifying how many processes are in each location

interval_state: ACSIntervalState

Interval state specifying the current interval for each variable

Implementations

impl ACSTAConfig

pub fn interval_state(&self) -> &ACSIntervalState

Get the interval state of the configuration

pub fn location_state(&self) -> &ACSLocState

Get the location state of the configuration

pub fn is_initial(&self, ta: &ACSThresholdAutomaton) -> bool

Check whether the current configuration is an initial configuration of the threshold automaton

pub fn compute_potential_predecessors( &self, rule: &CSRule, ta: &ACSThresholdAutomaton, ) -> Option<impl Iterator<Item = Self>>

Compute all predecessors of the configuration that could stem from rule r being applied

Note that the iterator returned here might contain comparable elements. Computing the minimal basis must be handled when collecting this iterator This function returns None if the rule contains a reset, and the variable the reset has been applied to is not in its 0 interval.

pub fn from_disjunct_target( spec: &DisjunctionTargetConfig, ta: &ACSThresholdAutomaton, ) -> impl Iterator<Item = ACSTAConfig>

Compute all configurations that correspond to an error state in the given disjunction over target configurations

pub fn from_target_config( spec: &TargetConfig, ta: &ACSThresholdAutomaton, ) -> HashSet<Self>

Compute a goal configuration from a single [TargetConfig]

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

Get a string representation of the configuration

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

Get a compact string representation of the configuration without locations that are not covered by processes or variables that are zero

pub fn encode_config_constraints_to_smt<C: SMTVariableContext<Parameter> + SMTVariableContext<Variable> + SMTVariableContext<Location>>( &self, ta: &ACSThresholdAutomaton, solver: &SMTSolver, ctx: &C, ) -> SMTExpr

Encode the conditions this abstract configuration places on the corresponding concrete configurations into an SMT expression

Trait Implementations

impl Clone for ACSTAConfig

fn clone(&self) -> ACSTAConfig

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ACSTAConfig

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

Formats the value using the given formatter.

impl Hash for ACSTAConfig

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 Ord for ACSTAConfig

fn cmp(&self, other: &ACSTAConfig) -> 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 ACSTAConfig

fn eq(&self, other: &ACSTAConfig) -> 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 ACSTAConfig

fn partial_cmp(&self, other: &ACSTAConfig) -> 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 ACSTAConfig

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 ACSTAConfig

impl StructuralPartialEq for ACSTAConfig