Struct LIAThresholdAutomaton 

pub struct LIAThresholdAutomaton {
    ta: GeneralThresholdAutomaton,
    init_variable_constr: Vec<LIAVariableConstraint>,
    rules: HashMap<Location, Vec<LIARule>>,
    additional_vars_for_sums: HashMap<Variable, WeightedSum<Variable>>,
}

A linear arithmetic threshold automaton or LIAThresholdAutomaton is a threshold automaton containing linear arithmetic guards. The goal of the LIAThresholdAutomaton is to stay as close to the formal definition of a threshold automaton as possible.

To convert a GeneralThresholdAutomaton to a LIAThresholdAutomaton all guards are translated into one of these forms:

• SingleAtomConstraint: Which represents a threshold in the form x <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c where c_1, ..., c_n, c are rational constants, p_1, ..., p_n are Parameters and x is a single shared variable.
• SumAtomConstraint: Represents a threshold of the form cx_1 * x_1 + ... + cx_m * x_m <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c where c_1, ..., c_n, cx_1, ..., cx_m, c are rational constants, p_1, ..., p_n are Parameters and x_1, …, x_m are shared variables. Additionally, all coefficients cx_1, ..., cx_m must be all positive.
• ComparisonConstraint: Comparison constraints are structured analog to a SumAtomConstraint, but allow mixing positive and negative constants in the constants cx_1, ..., cx_m.

Note that not all algorithms support all types of guards. Especially the ComparisonConstraint makes the verification problem undecidable (even without decrements and or resets). For more information see:

All Flavors of Threshold Automata - Jure Kukovec, Igor Konnov, Josef Widder - https://doi.org/10.4230/LIPIcs.CONCUR.2018.19

Fields

ta: GeneralThresholdAutomaton

GeneralThresholdAutomaton the canonical automaton has been constructed from

init_variable_constr: Vec<LIAVariableConstraint>

Initial conditions on variables in linear arithmetic

rules: HashMap<Location, Vec<LIARule>>

Transition rules of the threshold automaton indexed by source location

additional_vars_for_sums: HashMap<Variable, WeightedSum<Variable>>

Additional variables that are used to replace sums TODO: remove when a proper ordering for sums of variables is implemented

Implementations

impl LIAThresholdAutomaton

pub fn into_ta_without_sum_vars(self) -> Self

This function will remove any LIAVariableConstraint::SumVarConstraint and replace them with a new variable that is incremented/reset/decremented when any of its components is incremented, reset, or decremented.

This is not the most efficient solution for error graphs, but it is the simplest.

TODO: replace when more capable interval ordering is ready (see note in module no_sum_var docs)

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

Get the helper variables that have been added to replace sums of variables

fn create_new_variable_for_sumvar( s: &WeightedSum<Variable>, lta: &LIAThresholdAutomaton, ) -> Variable

Creates a new unique name for a sum of variables

impl LIAThresholdAutomaton

pub fn get_max_number_of_thresholds_per_rule(&self) -> u32

Get the maximum number of thresholds in a single rule of the threshold automaton

pub fn get_ta(&self) -> &GeneralThresholdAutomaton

Get a reference to the GeneralThresholdAutomaton this automaton has been derived from

pub fn has_sum_var_threshold_guard(&self) -> bool

Check if the canonical threshold automaton contains a guard over as sum of variables, i.e., some guard contains a SumAtomConstraint

pub fn has_comparison_guard(&self) -> bool

Check if the canonical threshold automaton has a comparison guard,i.e., some guard contains a ComparisonConstraint

pub fn get_single_var_constraints_rules( &self, ) -> HashSet<SingleAtomConstraint<Variable>>

Get all appearing SingleAtomConstraints

This function returns all appearing SingleAtomConstraints in the rules of a threshold automaton. The constraints are deduplicated.

pub fn get_sum_var_constraints(&self) -> HashSet<SumAtomConstraint<Variable>>

Get all appearing SumAtomConstraints

This function returns all appearing SumAtomConstraints in the rules of a threshold automaton. The constraints are deduplicated.

pub fn get_comparison_guards(&self) -> HashSet<ComparisonConstraint<Variable>>

Get all appearing ComparisonConstraints

This function returns all appearing ComparisonConstraints in the rules of a threshold automaton. The constraints are deduplicated.

pub fn get_thresholds(&self) -> HashSet<Threshold>

Get the number of distinct thresholds appearing in the definition of the threshold automaton

pub fn get_derived_rule(&self, r: &LIARule) -> Rule

Get the Rule this rule has been derived from

Trait Implementations

impl Clone for LIAThresholdAutomaton

fn clone(&self) -> LIAThresholdAutomaton

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LIAThresholdAutomaton

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

Formats the value using the given formatter.

impl Display for LIAThresholdAutomaton

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

Formats the value using the given formatter.

impl IsDeclared<Location> for LIAThresholdAutomaton

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

Check if object of type T is declared

impl IsDeclared<Parameter> for LIAThresholdAutomaton

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

Check if object of type T is declared

impl IsDeclared<Variable> for LIAThresholdAutomaton

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

Check if object of type T is declared

impl PartialEq for LIAThresholdAutomaton

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

type Rule = LIARule

Type of the rules of the threshold automaton

type InitialVariableConstraintType = LIAVariableConstraint

Type of the initial variable conditions of the threshold automaton

fn name(&self) -> &str

Get the name of the threshold automaton

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

Get the shared variables of the threshold automaton

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

Get the parameters of the threshold automaton

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

Get the locations of the threshold automaton

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

Get the resilience condition 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 = &LIAVariableConstraint>

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

impl TryFrom<GeneralThresholdAutomaton> for LIAThresholdAutomaton

type Error = LIATransformationError

The type returned in the event of a conversion error.

fn try_from(ta: GeneralThresholdAutomaton) -> Result<Self, Self::Error>

Performs the conversion.

impl StructuralPartialEq for LIAThresholdAutomaton