Struct EContextMgr 

pub struct EContextMgr {
    solver: SMTSolver,
    ta: Rc<GeneralThresholdAutomaton>,
    k: usize,
    ctx_mgr: SMTConfigMgr<LazyStepContext<GeneralThresholdAutomaton, ConfigCtx>, ConfigCtx>,
}

Fields

solver: SMTSolver

ta: Rc<GeneralThresholdAutomaton>

k: usize

ctx_mgr: SMTConfigMgr<LazyStepContext<GeneralThresholdAutomaton, ConfigCtx>, ConfigCtx>

Implementations

impl EContextMgr

pub fn new( ta: GeneralThresholdAutomaton, target_constr: &[&LIAVariableConstraint], smt_builder: &SMTSolverBuilder, ) -> Result<Self, ContextMgrError>

pub fn check_spec(self, spec: &DisjunctionTargetConfig) -> Option<Path>

Check whether spec holds

If the specification holds None is returned. Otherwise an error path is returned

fn compute_k_for_ta( ta: &GeneralThresholdAutomaton, target_constr: &[&LIAVariableConstraint], ) -> Result<usize, ContextMgrError>

Compute the number K for the threshold automaton

In the paper, the number of guards is simply given as the size of the set of guards ϕ plus one, i.e. K = |ϕ| + 1.

However, this assumes that all guards are in their strict upper and lower guard form. Therefore we need to convert the threshold automaton first into a LIAThresholdAutomaton and then compute the number K.

fn encode_phi_reach(&mut self, spec: &DisjunctionTargetConfig)

Encodes the ϕ_{reach} of the threshold automaton

fn encode_final_error_condition( &self, spec: &DisjunctionTargetConfig, ) -> SMTExpr

Encodes the goal condition of the threshold automaton into an SMT

Trait Implementations

impl Debug for EContextMgr

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.