Struct ReachabilityProperty 

pub struct ReachabilityProperty {
    name: String,
    disj: Vec<Reachability>,
}

A named reachability Property

Fields

name: String

Name of the property

disj: Vec<Reachability>

Disjunctions over constraints of the form () && <>()

Implementations

impl ReachabilityProperty

pub fn from_named_eltl<S: ToString>( name: S, expr: ELTLExpression, ) -> Result<Self, ReachabilityTransformationError>

Try to construct a new reachability property from an ELTLExpression

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 create_tas_to_check<T: ModifiableThresholdAutomaton>( &self, ta: &T, ) -> impl Iterator<Item = (DisjunctionTargetConfig, T)>

Create the threshold automata that need to be checked

pub fn name(&self) -> &str

Get the name of the specification

pub fn new<S: Into<String>, T: Into<Reachability>>(name: S, targets: T) -> Self

Create a new property

Trait Implementations

impl Clone for ReachabilityProperty

fn clone(&self) -> ReachabilityProperty

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ReachabilityProperty

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

Formats the value using the given formatter.

impl PartialEq for ReachabilityProperty

fn eq(&self, other: &ReachabilityProperty) -> 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<C: ModelCheckerContext> SpecificationTrait<C> for ReachabilityProperty

type TransformationError = ReachabilityTransformationError

Error occurring when transformation from ELTL specification fails

type InternalSpecType = DisjunctionTargetConfig

Internal specification type the model checker works on

fn try_from_eltl( spec: impl Iterator<Item = (String, ELTLExpression)>, _ctx: &C, ) -> Result<Vec<Self>, Self::TransformationError>

Try to derive the specification type from ELTL specification

fn transform_threshold_automaton<TA: ThresholdAutomaton + ModifiableThresholdAutomaton>( ta: TA, specs: Vec<Self>, _ctx: &C, ) -> Vec<(Self::InternalSpecType, TA)>

Create threshold automata to check

impl StructuralPartialEq for ReachabilityProperty