Struct GeneralThresholdAutomaton 

pub struct GeneralThresholdAutomaton {
    name: String,
    parameters: HashSet<Parameter>,
    variables: HashSet<Variable>,
    locations: HashSet<Location>,
    outgoing_rules: HashMap<Location, Vec<Rule>>,
    initial_location_constraint: Vec<LocationConstraint>,
    initial_variable_constraint: Vec<BooleanVarConstraint>,
    resilience_condition: Vec<ParameterConstraint>,
}

Type representing a general threshold automaton that can include variable comparisons, general non-linear arithmetic guards and as well as reset actions.

Fields

name: String

Name of the threshold automaton

parameters: HashSet<Parameter>

List of parameters appearing in the threshold automaton

variables: HashSet<Variable>

List of shared variables appearing in the threshold automaton

locations: HashSet<Location>

List of locations appearing in the threshold automaton

outgoing_rules: HashMap<Location, Vec<Rule>>

Transition rules of the threshold automaton indexed by source location

initial_location_constraint: Vec<LocationConstraint>

Initial constraints on the number of processes in a location

initial_variable_constraint: Vec<BooleanVarConstraint>

Initial constraint on the variable values

resilience_condition: Vec<ParameterConstraint>

Constraint over the parameters of the threshold automaton

Implementations

impl GeneralThresholdAutomaton

pub fn to_bymc(&self) -> String

Get the threshold automaton in the ByMC format

pub fn initial_variable_conditions( &self, ) -> impl Iterator<Item = &BooleanVarConstraint>

Returns an iterator over the initial location constraints of the threshold automaton

pub fn initial_location_conditions( &self, ) -> impl Iterator<Item = &LocationConstraint>

Returns an iterator over the initial location constraints of the threshold automaton

pub(crate) fn get_rule_map(&self) -> HashMap<Location, Vec<Rule>>

Get the internal set of rules of the threshold automaton

pub fn get_ta_body_in_bymc_format(&self) -> String

Returns the body of the threshold automaton, i.e. the definitions of locations, variables, rules, initial assumptions, etc. in ByMC format without the outer proc/ skel/ thresholdAutomaton declaration

Trait Implementations

impl Clone for GeneralThresholdAutomaton

fn clone(&self) -> GeneralThresholdAutomaton

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for GeneralThresholdAutomaton

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

Formats the value using the given formatter.

impl Display for GeneralThresholdAutomaton

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

Formats the value using the given formatter.

impl IsDeclared<Location> for GeneralThresholdAutomaton

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

Check if object of type T is declared

impl IsDeclared<Parameter> for GeneralThresholdAutomaton

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

Check if object of type T is declared

impl IsDeclared<Variable> for GeneralThresholdAutomaton

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

Check if object of type T is declared

impl ModifiableThresholdAutomaton for GeneralThresholdAutomaton

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

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

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

Retains only the rules specified by the predicate.

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

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

Apply a transformation to each rule

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

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

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

Add a new resilience condition to the threshold automaton

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

Add a new initial location constraint to the threshold automaton

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

Add a new initial variable constraint to the threshold automaton

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.

impl PartialEq for GeneralThresholdAutomaton

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

fn can_be_initial_location(&self, loc: &Location) -> bool

Check if the given location has an initial condition that prevents it from initially having any processes in it

Implementation

Many threshold automata have initial constraints of the form loc1 == 0, preventing any processes from starting in loc1 initially. This function checks if the given location has such a constraint.

It will not attempt to evaluate all initial constraints and check (for example by using an SMT solver) if the location can be initially occupied.

Instead, it will only check if the initial constraints contain a constraint of the form loc1 == <INTEGER EXPRESSION>, where <INTEGER EXPRESSION> evaluates to 0.

This approach does not sacrifice correctness, as the initial constraints are anyway encoded in the SMT query.

Example

use taco_threshold_automaton::expressions::*;
use taco_threshold_automaton::expressions::Location;
use taco_threshold_automaton::general_threshold_automaton::{GeneralThresholdAutomaton, builder::GeneralThresholdAutomatonBuilder};
use taco_threshold_automaton::ThresholdAutomaton;
use taco_threshold_automaton::LocationConstraint;
use std::collections::HashMap;

let ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
           .with_locations(vec![
               Location::new("loc1"),
               Location::new("loc2"),
               Location::new("loc3"),
           ]).unwrap()
           .initialize()
           .with_initial_location_constraints(vec![
               LocationConstraint::ComparisonExpression(
                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
                    ComparisonOp::Eq,
                    Box::new(IntegerExpression::Const(0)),
                ),
                LocationConstraint::ComparisonExpression(
                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
                    ComparisonOp::Geq,
                    Box::new(IntegerExpression::Const(0)),
                ) & LocationConstraint::ComparisonExpression(
                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
                    ComparisonOp::Leq,
                    Box::new(IntegerExpression::Const(0)),
                ),
           ]).unwrap()
           .build();
     
assert!(!ta.can_be_initial_location(&Location::new("loc1")));
assert!(!ta.can_be_initial_location(&Location::new("loc2")));
assert!(ta.can_be_initial_location(&Location::new("loc3")));

type Rule = Rule

Type of the rules of the threshold automaton

type InitialVariableConstraintType = BooleanExpression<Variable>

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 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 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 = &BooleanVarConstraint>

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