Struct ZCSErrorGraphBuilder 

pub struct ZCSErrorGraphBuilder<'a> {
    error_graph: ZCSErrorGraph<'a>,
}

Builder for constructing a symbolic error graph (ZCS error graph)

This builder takes a symnbolic 01-CS (ZCS) and a set of error states and derives the corresponding symbolic error graph.

The builder performs backwards reachability of all states in the 01-CS starting from the set of error states.

Fields

error_graph: ZCSErrorGraph<'a>

symbolic error graph that is constructed by the builder

Implementations

impl<'a> ZCSErrorGraphBuilder<'a>

pub fn new(cs: ZCS<'a>, err_states: ZCSStates) -> Self

creates a new symbolic error graph builder

pub fn compute_explored_states(&mut self)

predecessor computation to compute the reachable states

Pseudocode

 unexplored ← error_states
 visited ← unexplored
 while (unexplored ≠ ∅) {
    // 1. add new reachable states
    explored_states.push(unexplored)
     
    // 2. update unexplored
    unexplored ← Pred(∃ rule_vars: unexplored) ∧ ¬visited
    
    // 3. update visited
    visited ← visited ∨ unexplored
    abstract_unexplored ← ∃_rule_vars: unexplored
   
    for i in 0..|explored_states| {
        // 4. for each level i, check if a state `s` has already been reached with a different rule
        already_explored ← explored_states(i) ∧ abstract_unexplored

        if (already_explored ≠ ∅) {
            abstract_already_explored ← ∃ rule_vars: already_explored

            // 5. add state `s` with new outgoing rule `r` to the set of already explored states
            error_states(i) ← error_states(i) ∨ (unexplored ∧ abstract_already_explored)
       
            // 6. remove `s` from the set of unexplored states
            abstract_unexplored ← abstract_unexplored ∧ ¬abstract_already_explored
            unexplored ← unexplored ∧ ¬abstract_already_explored
        }
    }
 }

pub fn compute_reachable_initial_states(&mut self)

extracts all initial states that are reached in the error graph

pub fn build(self) -> ZCSErrorGraph<'a>

builds the symbolic error graph

Trait Implementations

impl<'a> Debug for ZCSErrorGraphBuilder<'a>

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

Formats the value using the given formatter.