Struct Reachability 

pub struct Reachability {
    precondition_par: Vec<BooleanExpression<Parameter>>,
    precondition_loc: Vec<BooleanExpression<Location>>,
    precondition_var: Vec<BooleanExpression<Variable>>,
    target: DisjunctionTargetConfig,
}

Formula of the form (preconditions) => <>(target)

A reachability constraint specifies

• a set of starting configurations
• a set of target configurations

The set of starting configurations is a subset of the threshold automaton. This type allows these restriction to be arbitrary boolean conditions on parameters, variables and locations (mostly since they appear in benchmarks of the ByMC tool).

Target constraints are more restricted. We only allow for lower bounds on the number of processes, or specifying that a location should not be covered. These constraints match the formal definition of ELTL formulas in the related literature (e.g., see paper “A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms” by Konnov et al.). Other constraints, such as upper bounds, can be seen as pathological and decision procedures may be incomplete for these specifications.

To handle these conditions, add them to the initial constraints of the threshold automaton, preferably before transforming the automaton in a necessary intermediate format.

Fields

precondition_par: Vec<BooleanExpression<Parameter>>

Conjunction of conditions on the parameter evaluation

precondition_loc: Vec<BooleanExpression<Location>>

Conjunction of conditions on the initial distribution of processes in the threshold automaton

precondition_var: Vec<BooleanExpression<Variable>>

Conjunction of conditions on the initial valuation of the shared variables

target: DisjunctionTargetConfig

Conditions on the configuration to reach

Implementations

impl Reachability

fn new_unconstrained(name: String) -> Self

Create a new reachability constraint that has no constraints

fn new_with_parameter_constr( name: String, lhs: Box<IntegerExpression<Parameter>>, op: ComparisonOp, rhs: Box<IntegerExpression<Parameter>>, ) -> Self

Create a new reachability constraint with only a single parameter constraint

fn new_with_initial_loc_constr( name: String, lhs: Box<IntegerExpression<Location>>, op: ComparisonOp, rhs: Box<IntegerExpression<Location>>, ) -> Self

Create a new reachability constraint with only a single initial location constraint

fn new_with_initial_var_constr( name: String, lhs: Box<IntegerExpression<Variable>>, op: ComparisonOp, rhs: Box<IntegerExpression<Variable>>, ) -> Self

Create a new reachability constraint with only a single initial variable constraint

fn new_with_eventual_reach(disj: DisjunctionTargetConfig) -> Self

Create a new reachability constraint with only an eventual constraint

pub fn contains_reachability_constraint(&self) -> bool

Check whether this constraint contains a reachability constraint

A reachability constraint requires at least one location to be empty.

pub fn get_target_conditions(&self) -> &DisjunctionTargetConfig

Get the target specification of the reachability specification

A Reachability object is a specification of the form (preconditions) => <>(target) This function returns the target as a DisjunctionTargetConfig

fn try_from_eltl( name: String, spec: NonNegatedELTLExpression, ) -> Result<Vec<Self>, ReachabilityTransformationError>

Try to construct a reachability constraint from a an ELTL formula

fn parse_in_eventually( name: String, expr: NonNegatedELTLExpression, ) -> Result<DisjunctionTargetConfig, ReachabilityTransformationError>

Try to parse the constraints behind an eventually operator into a disjunction of upwards closed sets

Trait Implementations

impl And for Reachability

fn and(self, other: Reachability) -> Self

Get the conjunction of self and other

impl Clone for Reachability

fn clone(&self) -> Reachability

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Reachability

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

Formats the value using the given formatter.

impl<D: Into<DisjunctionTargetConfig>> From<D> for Reachability

fn from(value: D) -> Self

Converts to this type from the input type.

impl PartialEq for Reachability

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