Struct ZCSModelCheckerContext 

pub struct ZCSModelCheckerContext<'a> {
    pub(crate) ctx: &'a SMTBddContext,
    pub(crate) heuristics: ZCSModelCheckerHeuristics,
    pub(crate) ta: &'a IntervalThresholdAutomaton,
    pub(crate) spec: &'a DisjunctionTargetConfig,
    pub(crate) print_spurious_ce: bool,
}

This struct contains all the necessary configurations when using the symbolic model checker (ZCS model checker)

Fields

ctx: &'a SMTBddContext

used smt and bdd libraries

heuristics: ZCSModelCheckerHeuristics

underlying heuristics

ta: &'a IntervalThresholdAutomaton

underlying TA

spec: &'a DisjunctionTargetConfig

underlying specification

print_spurious_ce: bool

indicates if the symbolic model checker should print spurious counterexamples

Implementations

impl<'a> ZCSModelCheckerContext<'a>

pub(crate) fn new( ctx: &'a SMTBddContext, heuristics: ZCSModelCheckerHeuristics, ta: &'a IntervalThresholdAutomaton, spec: &'a DisjunctionTargetConfig, ) -> Self

creates a new symbolic model checker context

pub(crate) fn smt_bdd_context(&self) -> &SMTBddContext

returns the SMTBddContext

pub(crate) fn heuristics(&self) -> ZCSModelCheckerHeuristics

returns the heuristics

pub(crate) fn ta(&self) -> &IntervalThresholdAutomaton

returns the underlying TA

pub(crate) fn spec(&self) -> &DisjunctionTargetConfig

returns the underlying specification

pub(crate) fn print_spurious_ce(&self) -> bool

returns if spurious counterexamples should be printed