Struct ErrorGraph 

pub struct ErrorGraph {
    initial_leafs: Vec<Rc<RefCell<ErrorGraphNode>>>,
    ta: ACSThresholdAutomaton,
    spec: DisjunctionTargetConfig,
}

Error Graph storing all paths from initial abstract configurations to error configurations

Fields

initial_leafs: Vec<Rc<RefCell<ErrorGraphNode>>>

All nodes that have an initial configuration

ta: ACSThresholdAutomaton

Threshold automaton for which the error graph has been constructed

spec: DisjunctionTargetConfig

Specification for which the error graph has been constructed

Implementations

impl ErrorGraph

pub fn compute_error_graph( spec: DisjunctionTargetConfig, ta: ACSThresholdAutomaton, ) -> Self

Compute the error graph of the given specification

Constructing the error graph can be a time and memory heavy operation.

fn construct_full_error_graph( spec: &DisjunctionTargetConfig, ta: &ACSThresholdAutomaton, ) -> PartiallyOrderedConfigMap<Rc<RefCell<ErrorGraphNode>>>

Compute the full error graph for the ACSThresholdAutomaton and the given [DisjunctionTargetConfig]

pub fn is_empty(&self) -> bool

Check whether the error graph is empty, i.e. whether no counter example exists

pub fn check_for_non_spurious_counter_example( self, context: SMTSolver, ) -> ModelCheckerResult

Check whether a non-spurious counter example exists

This method might not terminate for threshold automata with resets