Struct TransitionSystem 

pub struct TransitionSystem {
    pub registers: Vec<Register>,
    pub property: BoundedExpr,
}

A synchronous transition system over Boolean and bitvector registers.

Fields

registers: Vec<Register>

property: BoundedExpr

The safety property that must hold in every reachable state (unindexed, boolean).

Implementations

impl TransitionSystem

pub fn bmc(&self, max_k: u32) -> BmcOutcome

Bounded model check: is a state violating property reachable within max_k steps?

pub fn prove_invariant(&self, k: u32) -> InductionOutcome

Prove (by k-induction) that property holds in EVERY reachable state.

pub fn witness_trace(&self, steps: u32) -> Option<Vec<(String, bool)>>

A concrete witnessing execution: a model of init ∧ trans(0..steps) with NO property negation. For a deterministic controller this is the unique real run from the initial state — used to ANIMATE the proven-safe machine, which (by construction) has no counterexample to show. Returns the signal@t bit assignments of the run, or None if the obligation leaves the supported fragment.

Trait Implementations

impl Clone for TransitionSystem

fn clone(&self) -> TransitionSystem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TransitionSystem

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

Formats the value using the given formatter.