Struct ZCSErrorGraph 

pub struct ZCSErrorGraph<'a> {
    error_states: ZCSStates,
    explored_states: Vec<ZCSStates>,
    initial_states: ZCSStates,
    cs: ZCS<'a>,
}

Type representing a symbolic error graph (ZCS error graph)

Fields

error_states: ZCSStates

set of error states

explored_states: Vec<ZCSStates>

all iteratively explored states, these states contain bdd variables for transitions the first entry is equal to the error states

initial_states: ZCSStates

set of reached initial states of the error graph

cs: ZCS<'a>

underlying 01-CS (ZCS)

Implementations

impl ZCSErrorGraph<'_>

pub fn is_empty(&self) -> bool

checks if an initial state has been reached

pub fn initial_states(&self) -> ZCSStates

reachable initial_states

pub fn compute_successors( &self, from: ZCSStates, with: SymbolicTransition, ) -> ZCSStates

computes the set of successors reachable in the symbolic error graph (ZCS error graph) for a given symbolic transition

pub fn get_non_error_intersection(&self, states: ZCSStates) -> (bool, ZCSStates)

for set of states, it removes the error states additionally returns false, if the intersection is empty

pub fn get_error_intersection(&self, states: ZCSStates) -> (bool, ZCSStates)

computes the intersection of a set of states with the set of error states additionally returns, if the intersection is empty

pub fn get_sym_state_for_loc(&self, loc: &Location) -> ZCSStates

returns the set of states where a given location is occupied

pub fn get_sym_state_for_shared_interval( &self, shared: &Variable, interval: &Interval, ) -> ZCSStates

returns the set of states where the given shared variable is in the given interval

pub fn get_sym_state_for_rule(&self, rule: &IntervalTARule) -> ZCSStates

returns the set of states where the rule_id of a given rule is applied

pub fn transitions(&self) -> impl Iterator<Item = &SymbolicTransition>

returns an iterator over the encoded transition rules in the underlying 01-cs

pub fn new_empty_sym_state(&self) -> ZCSStates

returns a new empty Symbolic State

pub fn contains_non_spurious_error_path( &self, smc_ctx: &ZCSModelCheckerContext<'_>, ) -> SpuriousResult

checks if the error graph contains a non-spurious error path spurious_checker is used to check if a path is spurious

returns None if every path is spurious

Note that this function is a semi-decision procedure if the underlying threshold automaton contains decrements or resets, i.e., it might not terminate.

queue ← Queue::new()
queue.push(SteadyPath::new(initial_states))
while (queue ≠ ∅) {
    steady_path ← queue.pop()
    for rule in transitions {
        successor_states ← compute_successors(steady_path.last_states, rule)
         
        // check if an error state can be reached
        error_intersection ← get_error_intersection(successor_states)
        if (error_intersection ≠ ∅) {
            foreach assignment {
                if ((error_intersecion ∧ assignment) ≠ ∅) {
                    updated_steady_path ← steady_path.add_successor(rule, error_intersection ∧ assignment)
                    if updated_steady_path.is_non_spurious() {
                        return "Found non spurious counter example"
                    }  
                }
            }
        }

        // check all other reachable steady paths which do not lead to an error state for spuriousness
        non_error_intersection ← get_non_error_intersection(successor_states)
        if (non_error_intersection ≠ ∅) {
            foreach assignment {
                if ((non_error_intersection ∧ assignment) ≠ ∅) {
                    // construct steady path for the given assignment
                    successor_steady_path ← construct_steady_path(non_error_intersection ∧ assignment, assignment)
                    updated_steady_path ← steady_path.add_successor(rule, successor_steady_path)
                    if updated_steady_path.is_non_spurious() {
                        queue.push(updated_steady_path)
                    }
                }
            }
        }   
    }
}
return "All error paths are spurious"

fn get_all_possible_variable_assignments( &self, ) -> Vec<SymbolicVariableAssignment>

returns all possible variable assignments

fn compute_reachable_variable_assignments( &self, ) -> Vec<SymbolicVariableAssignment>

computes all reachable variable assignments of the error graph (except for error states)

fn construct_steady_path( &self, sym_state: ZCSStates, assignment: SymbolicVariableAssignment, ) -> SteadyPath

constructs the steady path for a given ‘SymbolicState’ and a ‘SymbolicVariableAssignment’

i.e., it computes all reachable states and possible transitions to stay in the same variable assignment

Note that it only computes reachable states that are not an error state

pub fn locations(&self) -> impl Iterator<Item = &Location>

returns an iterator over the locations of the underlying threshold automaton

pub fn variables(&self) -> impl Iterator<Item = &Variable>

returns an iterator over the shared variables of the underlying threshold automaton

pub fn get_ordered_intervals_for_shared( &self, shared: &Variable, ) -> &Vec<Interval>

returns an iterator over the ordered intervals for a given shared variable

Trait Implementations

impl<'a> Clone for ZCSErrorGraph<'a>

fn clone(&self) -> ZCSErrorGraph<'a>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'a> Debug for ZCSErrorGraph<'a>

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

Formats the value using the given formatter.