Struct BDDModelChecker 

pub struct BDDModelChecker {
    pub mgr: BDDManager,
    pub num_vars: usize,
    pub init_bdd: usize,
    pub trans_bdd: usize,
}

A symbolic model checker that uses BDDs to verify CTL properties.

Fields

mgr: BDDManager

The BDD manager.

num_vars: usize

Number of state variables (state encoded as num_vars bits).

init_bdd: usize

BDD id representing the initial states.

trans_bdd: usize

BDD id representing the transition relation T(s, s’).

Implementations

impl BDDModelChecker

pub fn new(num_vars: usize) -> Self

Create a new BDD model checker.

pub fn set_init(&mut self, bdd: usize)

Set the initial state BDD.

pub fn set_trans(&mut self, bdd: usize)

Set the transition relation BDD.

pub fn post(&mut self, states: usize) -> usize

Compute the set of states reachable from states in one step.

pub fn pre(&mut self, states: usize) -> usize

Compute the set of states that can reach states in one step.

pub fn reachable(&mut self) -> usize

Compute the set of all reachable states (forward BFS via BDDs).

pub fn check_ag_safe(&mut self, safe: usize) -> bool

Check AG(safe): all reachable states satisfy the safe BDD predicate.

pub fn check_ef(&mut self, target: usize) -> bool

Check EF(target): some reachable state satisfies target.

Trait Implementations

impl Clone for BDDModelChecker

fn clone(&self) -> BDDModelChecker

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BDDModelChecker

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

Formats the value using the given formatter.