Struct SpuriousGraphChecker 

pub struct SpuriousGraphChecker {
    solver: SMTSolver,
    spec: DisjunctionTargetConfig,
    cs_ta: Rc<ACSThresholdAutomaton>,
    ctx_mgr: SMTConfigMgr<LazyStepContext<ACSThresholdAutomaton, ConfigCtx>, ConfigCtx>,
}

Fields

solver: SMTSolver

spec: DisjunctionTargetConfig

cs_ta: Rc<ACSThresholdAutomaton>

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

Implementations

impl SpuriousGraphChecker

pub fn new( ta: &ACSThresholdAutomaton, spec: DisjunctionTargetConfig, solver: SMTSolver, ) -> Self

pub fn find_violation(&mut self, e_graph: &ErrorGraph) -> ModelCheckerResult

fn explore_node_for_violation( &mut self, node: &Rc<RefCell<ErrorGraphNode>>, prev_cfg_ctx: Rc<ConfigCtx>, index: usize, ) -> ModelCheckerResult

fn explore_next_interval_state_transition( &mut self, next_node: &Rc<RefCell<ErrorGraphNode>>, prev_cfg: Rc<ConfigCtx>, index: usize, ) -> ModelCheckerResult

fn encode_and_assert_steady_path_with_rules( &mut self, appl_rules: &HashSet<u32>, prev_cfg: Rc<ConfigCtx>, next_cfg: Rc<ConfigCtx>, index: usize, ) -> LazyStepContext<ACSThresholdAutomaton, ConfigCtx>

fn collect_enabled_rules_and_next_nodes( org_node: &Rc<RefCell<ErrorGraphNode>>, visited_nodes: &mut HashSet<ACSTAConfig>, ) -> (HashSet<u32>, Vec<Rc<RefCell<ErrorGraphNode>>>, bool)

This function collects the orders in which rules are applicable while staying in the same interval state along with the rules that would allow to transition out of the interval state.

The first set (HashSet<u32>) represents all applicable rules, and the second value is a vector of next nodes.

• The second element (Vec<NodeRef>) contains nodes that represent possible transitions out of the current interval state.
• The third element (bool) is true if any of the traversed nodes are in an error state, false otherwise.

fn check_spurious_error(&mut self, ctx: &ConfigCtx) -> ModelCheckerResult