Skip to main content

SpecificationTrait

taco_model_checker

Trait SpecificationTrait 

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

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

Trait that needs to be implemented by an internal specification representation

Required Associated Types§

Source

type TransformationError: Error + Sized

Error occurring when transformation from ELTL specification fails

Source

type InternalSpecType: Sized + TASpecification

Internal specification type the model checker works on

Required Methods§

Source

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

Returns the translated specifications and the names of the properties that could not be translated, but should be reported as unknown.

Source

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

Create threshold automata to check

This function allows to pair a specification with a threshold automaton. Each pair is labeled with the name of the property it belongs to.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§