Struct ModelCheckingBound 

pub struct ModelCheckingBound {
    pub depth: usize,
    pub max_depth: usize,
    pub counterexample_found: bool,
}

Bounded model checking state: BMC encoding with a depth bound.

Fields

depth: usize

Current unfolding depth.

max_depth: usize

Maximum depth allowed.

counterexample_found: bool

Whether a counterexample was found within depth steps.

Implementations

impl ModelCheckingBound

pub fn new(max_depth: usize) -> Self

Create a bounded model checking instance.

pub fn unfold(&mut self)

Increment the unfolding depth by one.

pub fn at_bound(&self) -> bool

Returns true if the bound has been reached.

Trait Implementations

impl Clone for ModelCheckingBound

fn clone(&self) -> ModelCheckingBound

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ModelCheckingBound

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

Formats the value using the given formatter.