Trait SpecificationTrait 

pub trait SpecificationTrait<C: ModelCheckerContext>: Sized + Debug {
    type TransformationError: Error + Sized;
    type InternalSpecType: Sized + TargetSpec;

    // Required methods
    fn try_from_eltl(
        spec: impl Iterator<Item = (String, ELTLExpression)>,
        ctx: &C,
    ) -> Result<Vec<Self>, Self::TransformationError>;
    fn transform_threshold_automaton<TA: ThresholdAutomaton + ModifiableThresholdAutomaton>(
        ta: TA,
        specs: Vec<Self>,
        ctx: &C,
    ) -> Vec<(Self::InternalSpecType, TA)>;
}

Trait that needs to be implemented by an internal specification representation

Required Associated Types

type TransformationError: Error + Sized

Error occurring when transformation from ELTL specification fails

type InternalSpecType: Sized + TargetSpec

Internal specification type the model checker works on

Required Methods

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

This function allows to pair a specification with a threshold automaton

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<C: ModelCheckerContext> SpecificationTrait<C> for ReachabilityProperty

type TransformationError = ReachabilityTransformationError

type InternalSpecType = DisjunctionTargetConfig