Trait ThresholdAutomaton 

pub trait ThresholdAutomaton:
    Debug
    + Clone
    + Display
    + IsDeclared<Parameter>
    + IsDeclared<Variable>
    + IsDeclared<Location> {
    type Rule: RuleDefinition;
    type InitialVariableConstraintType: VariableConstraint;

    // Required methods
    fn name(&self) -> &str;
    fn parameters(&self) -> impl Iterator<Item = &Parameter>;
    fn initial_location_constraints(
        &self,
    ) -> impl Iterator<Item = &LocationConstraint>;
    fn initial_variable_constraints(
        &self,
    ) -> impl Iterator<Item = &Self::InitialVariableConstraintType>;
    fn resilience_conditions(
        &self,
    ) -> impl Iterator<Item = &BooleanExpression<Parameter>>;
    fn variables(&self) -> impl Iterator<Item = &Variable>;
    fn locations(&self) -> impl Iterator<Item = &Location>;
    fn can_be_initial_location(&self, location: &Location) -> bool;
    fn rules(&self) -> impl Iterator<Item = &Self::Rule>;
    fn incoming_rules(
        &self,
        location: &Location,
    ) -> impl Iterator<Item = &Self::Rule>;
    fn outgoing_rules(
        &self,
        location: &Location,
    ) -> impl Iterator<Item = &Self::Rule>;

    // Provided methods
    fn has_decrements_or_resets(&self) -> bool { ... }
    fn has_decrements(&self) -> bool { ... }
    fn has_resets(&self) -> bool { ... }
}

Common trait for different types of threshold automata

This trait is implemented by all types and flavors of threshold automata and provides a common interface for interacting with threshold automata.

This trait is for example implemented by general_threshold_automaton::GeneralThresholdAutomaton or lia_threshold_automaton::LIAThresholdAutomaton.

Required Associated Types

type Rule: RuleDefinition

Type of the rules of the threshold automaton

type InitialVariableConstraintType: VariableConstraint

Type of the initial variable conditions of the threshold automaton

Required Methods

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

Returns true if the location can be an initial location of the threshold

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

Returns the rules that have the given location as target location. This means that the location is the target of the transition.

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

Get outgoing rules for a location

Returns the rules that have the given location as source location.

Provided Methods

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

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl ThresholdAutomaton for GeneralThresholdAutomaton

type Rule = Rule

type InitialVariableConstraintType = BooleanExpression<Variable>

impl ThresholdAutomaton for LIAThresholdAutomaton

type Rule = LIARule

type InitialVariableConstraintType = LIAVariableConstraint