Struct DropUnsatisfiableRules 

pub struct DropUnsatisfiableRules {}

Preprocessor that drops rules where the guards are unsatisfiable

This preprocessor encodes the resilience condition of the threshold automaton into an SMT solver and checks whether rule guards are satisfiable.

If a rule guard is unsatisfiable, the rule is removed from the threshold automaton.

This preprocessing step is useful for machine generated threshold automata or if the resilience condition is complex. As it uses an SMT solver, it can be very expensive.

Implementations

impl DropUnsatisfiableRules

pub fn new() -> Self

Create a new instance of the preprocessor

fn get_unsatisfiable_rules<T: ThresholdAutomaton>( &self, solver_builder: SMTSolverBuilder, ta: &T, ) -> impl Iterator<Item = T::Rule>

Check whether the guard of the rule is satisfiable

Trait Implementations

impl Default for DropUnsatisfiableRules

fn default() -> Self

Returns the “default value” for a type.

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

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

Process the threshold automaton and attempt to simplify it