Struct ErrorSpec 

pub struct ErrorSpec {
    name: String,
    source: Box<ELTLExpression>,
    ef: ErrorFormula,
}

Named specification of erroneous behavior

An ErrorSpec pairs the original ELTL property with the ErrorFormula describing its violations. The threshold automaton violates the property if and only if there exists a run satisfying the error formula.

Fields

name: String

Name of the property

source: Box<ELTLExpression>

The ELTL property this error specification was derived from

ef: ErrorFormula

Formula describing the violations of the property

Implementations

impl ErrorSpec

pub fn from_named_eltl<S: Into<String>>( name: S, property: ELTLExpression, ) -> Result<Self, ExtractionError>

Error specification of a named ELTL formula

property describes the erroneous behavior and is not negated here. Negations are pushed to the atoms, then the formula is transformed into an ErrorFormula. Temporal operators at the top level become targets. Atoms at the top level restrict the initial configuration.

impl ErrorSpec

pub fn name(&self) -> &str

Get the name of the specification

pub fn source(&self) -> &ELTLExpression

Get the ELTL property this specification was derived from

pub fn error_formula(&self) -> &ErrorFormula

Get the formula describing the violations of the property

pub fn create_tas_to_check<T: ModifiableThresholdAutomaton>( &self, ta: &T, ) -> impl Iterator<Item = (ErrorTarget, T)>

Create the threshold automata that need to be checked

Trait Implementations

impl Clone for ErrorSpec

fn clone(&self) -> ErrorSpec

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ErrorSpec

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

Formats the value using the given formatter.

impl Display for ErrorSpec

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

Formats the value using the given formatter.

impl PartialEq for ErrorSpec

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

type TransformationError = ExtractionError

Error occurring when transformation from ELTL specification fails

type InternalSpecType = ErrorTarget

Internal specification type the model checker works on

fn try_from_eltl( spec: impl Iterator<Item = (String, ELTLExpression)>, _ctx: &C, ) -> Result<(Vec<Self>, Vec<String>), 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<(String, Self::InternalSpecType, TA)>

Create threshold automata to check

impl StructuralPartialEq for ErrorSpec