Struct IntervalTABuilder 

pub struct IntervalTABuilder {
    lia_ta: LIAThresholdAutomaton,
    solver_builder: SMTSolverBuilder,
    target_constr: Vec<LIAVariableConstraint>,
}

Builder for generating interval threshold automata

This builder takes a linear integer arithmetic threshold automaton and derives all valid interval threshold automata.

An interval threshold automaton is a threshold automaton where the guards are abstracted to intervals and the order of the intervals is defined.

The builder generates all possible interval orders for the given threshold linear integer arithmetic automaton, and for each interval order, it generates the corresponding interval threshold automaton.

Fields

lia_ta: LIAThresholdAutomaton

Underlying threshold automaton

solver_builder: SMTSolverBuilder

Solver builder for generating the interval orders

target_constr: Vec<LIAVariableConstraint>

Additional variable constraints derived from the target specification

Implementations

impl IntervalTABuilder

pub fn new( lia_ta: LIAThresholdAutomaton, solver_builder: SMTSolverBuilder, target_constr: Vec<LIAVariableConstraint>, ) -> Self

Create a new interval threshold automaton builder from a linear integer arithmetic threshold automaton

The solver builder is used to generate the interval orders.

pub fn build( self, ) -> Result<impl Iterator<Item = IntervalThresholdAutomaton>, IntervalTATransformationError>

Generate all possible orders on the intervals and derive the interval automaton for every possible order

fn derive_interval_threshold_automaton( lia_ta: LIAThresholdAutomaton, interval_order: StaticIntervalOrder, ) -> IntervalThresholdAutomaton

Given a fixed order, derive the abstract threshold automaton

fn discover_interval_boundaries_in_lia_variable_constraint( guard: &LIAVariableConstraint, order_builder: StaticIntervalOrderBuilder, ) -> Option<StaticIntervalOrderBuilder>

Extract variable intervals from a rule guard of the threshold automaton

Returns None if a comparison guard has been discovered