Trait Preprocessor 

pub trait Preprocessor<T: ModifiableThresholdAutomaton + ThresholdAutomaton, S: TargetSpec, C: ModelCheckerContext> {
    // Required method
    fn process(&self, ta: &mut T, spec: &S, ctx: &C);
}

Trait for preprocessing threshold automata

This trait is implemented by types that can process a threshold automaton to simplify it for further analysis.

Required Methods

fn process(&self, ta: &mut T, spec: &S, ctx: &C)

Process the threshold automaton and attempt to simplify it

Trait Implementations

impl<S, C> From<ExistingPreprocessors> for Box<dyn Preprocessor<GeneralThresholdAutomaton, S, C>>

where S: TargetSpec, C: ModelCheckerContext + ProvidesSMTSolverBuilder,

fn from(val: ExistingPreprocessors) -> Self

Converts to this type from the input type.

Implementors

impl<S: TargetSpec, C: ModelCheckerContext + ProvidesSMTSolverBuilder> Preprocessor<GeneralThresholdAutomaton, S, C> for CheckInitCondSatSMT

impl<S: TargetSpec, C: ModelCheckerContext + ProvidesSMTSolverBuilder> Preprocessor<GeneralThresholdAutomaton, S, C> for ReplaceTrivialGuardsSMT

impl<S: TargetSpec, C: ModelCheckerContext> Preprocessor<GeneralThresholdAutomaton, S, C> for CollapseLocations

impl<S: TargetSpec, C: ModelCheckerContext> Preprocessor<GeneralThresholdAutomaton, S, C> for DropUnreachableLocations

impl<S: TargetSpec, C: ModelCheckerContext> Preprocessor<GeneralThresholdAutomaton, S, C> for RemoveUnusedVariables

impl<S: TargetSpec, C: ModelCheckerContext> Preprocessor<GeneralThresholdAutomaton, S, C> for ReplaceTrivialGuardsStatic

impl<T: ModifiableThresholdAutomaton, S: TargetSpec, C: ModelCheckerContext + ProvidesSMTSolverBuilder> Preprocessor<T, S, C> for DropUnsatisfiableRules

impl<T: ModifiableThresholdAutomaton, S: TargetSpec, C: ModelCheckerContext> Preprocessor<T, S, C> for DropSelfLoops