Trait ModifiableThresholdAutomaton 

pub trait ModifiableThresholdAutomaton: ThresholdAutomaton {
    // Required methods
    fn set_name(&mut self, new_name: String);
    fn add_rule(&mut self, rule: Self::Rule);
    fn add_resilience_conditions<C: IntoIterator<Item = BooleanExpression<Parameter>>>(
        &mut self,
        conditions: C,
    );
    fn add_initial_location_constraints<C: IntoIterator<Item = LocationConstraint>>(
        &mut self,
        constraints: C,
    );
    fn add_initial_variable_constraints<C: IntoIterator<Item = BooleanVarConstraint>>(
        &mut self,
        constraints: C,
    );
    fn retain_rules<F>(&mut self, predicate: F)
       where F: Fn(&Self::Rule) -> bool;
    fn transform_rules<F>(&mut self, f: F)
       where F: FnMut(&mut Self::Rule);
    fn remove_location_and_replace_with(
        &mut self,
        location: &Location,
        subst: IntegerExpression<Location>,
    );
    fn remove_variable_and_replace_with(
        &mut self,
        variable: &Variable,
        subst: IntegerExpression<Variable>,
    );
    fn replace_initial_location_constraints<C: IntoIterator<Item = LocationConstraint>>(
        &mut self,
        constraints: C,
    );
    fn replace_initial_variable_constraints<C: IntoIterator<Item = BooleanVarConstraint>>(
        &mut self,
        constraints: C,
    );
}

Trait for threshold automata that can be modified

This trait is implemented by threshold automata that can be modified. for example, through preprocessing or other means. It provides methods to modify, remove or add components of the threshold automaton.

Note the resulting threshold automaton is not validated. It is up to the user to ensure that transformations result in a valid threshold automaton. Invalid threshold automata can lead to panics of other methods or functions. If a type does not implement this trait, you should modify a higher level representation.

Methods from this trait should not be used to construct a threshold automaton, but rather to modify an existing one. To build a threshold automaton, use the corresponding builder, e.g., general_threshold_automaton::builder::GeneralThresholdAutomatonBuilder.

Required Methods

fn set_name(&mut self, new_name: String)

Rename the threshold automaton

fn add_rule(&mut self, rule: Self::Rule)

Add a new rule to the threshold automaton

Note: The rule that is inserted is not validated. To build a threshold automaton, you should use the corresponding builder, e.g., GeneralThresholdAutomatonBuilder.

fn add_resilience_conditions<C: IntoIterator<Item = BooleanExpression<Parameter>>>( &mut self, conditions: C, )

Add a new resilience condition to the threshold automaton

Note: The resilience condition that is inserted is not validated. To build a threshold automaton, you should use the corresponding builder, e.g., GeneralThresholdAutomatonBuilder.

fn add_initial_location_constraints<C: IntoIterator<Item = LocationConstraint>>( &mut self, constraints: C, )

Add a new initial location constraint to the threshold automaton

Note: The initial location constraint that is inserted is not validated. To build a threshold automaton, you should use the corresponding builder, e.g., GeneralThresholdAutomatonBuilder.

fn add_initial_variable_constraints<C: IntoIterator<Item = BooleanVarConstraint>>( &mut self, constraints: C, )

Add a new initial variable constraint to the threshold automaton

Note: The initial variable constraint that is inserted is not validated. To build a threshold automaton, you should use the corresponding builder, e.g., GeneralThresholdAutomatonBuilder.

fn retain_rules<F>(&mut self, predicate: F)

where F: Fn(&Self::Rule) -> bool,

Retains only the rules specified by the predicate.

In other words, remove all rules r for which predicate(&r) returns false.

Note: The method predicate can be called multiple times per rule.

fn transform_rules<F>(&mut self, f: F)

where F: FnMut(&mut Self::Rule),

Apply a transformation to each rule

This method is used to apply a transformation to each rule of the threshold automaton. The transformation is applied in place, meaning that the rule is modified directly.

Note:

• The method f can be called multiple times per rule.
• The transformed rule is not validated

fn remove_location_and_replace_with( &mut self, location: &Location, subst: IntegerExpression<Location>, )

Remove a location location from the threshold automaton, removes rules referencing the location and replace every occurrence in initial conditions with subst

Note: The resulting location constraints are not validated

fn remove_variable_and_replace_with( &mut self, variable: &Variable, subst: IntegerExpression<Variable>, )

Remove a variable variable from the threshold automaton, replace every occurrence in initial conditions or guards with subst and remove all updates to variable from the rules

Note: The resulting variable constraints and guards are not validated

fn replace_initial_location_constraints<C: IntoIterator<Item = LocationConstraint>>( &mut self, constraints: C, )

Remove all location_constraints from the threshold automaton Needed to specify initial configurations for coverability and reachability through the CLI.

fn replace_initial_variable_constraints<C: IntoIterator<Item = BooleanVarConstraint>>( &mut self, constraints: C, )

Remove all variable_constraints from the threshold automaton Needed to specify initial configurations for coverability and reachability through the CLI.

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 ModifiableThresholdAutomaton for GeneralThresholdAutomaton