Struct CounterExample 

pub struct CounterExample {
    pub trace: Vec<usize>,
    pub loop_start: Option<usize>,
    pub violated_formula: String,
}

A counterexample: a trace (sequence of states) witnessing a formula violation.

Fields

trace: Vec<usize>

The sequence of states in the counterexample.

loop_start: Option<usize>

Index into trace where the lasso loop starts (-1 = no loop).

violated_formula: String

The violated formula (as a display string).

Implementations

impl CounterExample

pub fn finite(trace: Vec<usize>, formula: impl Into<String>) -> Self

Create a finite counterexample trace.

pub fn lasso( trace: Vec<usize>, loop_start: usize, formula: impl Into<String>, ) -> Self

Create a lasso (prefix + cycle) counterexample.

pub fn is_lasso(&self) -> bool

Returns true if this is a lasso (infinite path).

Trait Implementations

impl Clone for CounterExample

fn clone(&self) -> CounterExample

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CounterExample

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

Formats the value using the given formatter.