Struct SymbolicTransitionRelation 

pub struct SymbolicTransitionRelation {
    pub bdd_id: usize,
    pub num_vars: usize,
}

Symbolic transition relation T(s, s’) represented as a BDD node id.

Fields

bdd_id: usize

The BDD manager shared by all operations.

num_vars: usize

Number of state variables.

Implementations

impl SymbolicTransitionRelation

pub fn new(bdd_id: usize, num_vars: usize) -> Self

Create a transition relation from a BDD node id.

pub fn image(&self, mgr: &mut BDDManager, states: usize) -> usize

Compute the forward image of states under this transition relation.

pub fn pre_image(&self, mgr: &mut BDDManager, states: usize) -> usize

Compute the backward pre-image of states under this transition relation.

Trait Implementations

impl Clone for SymbolicTransitionRelation

fn clone(&self) -> SymbolicTransitionRelation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SymbolicTransitionRelation

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

Formats the value using the given formatter.