line::mdd::MDD Class Reference

The diagram: insert / member / index / enumerate / cardinality. More...

#include <line/api/mdd/mdd.h>

Public Member Functions
	MDD (const std::vector< int > &domain)
	An empty set over the given per-level domains.
std::size_t	K () const
const std::vector< int > &	domain () const
int	root () const
	Id of the root node, or TERM_FALSE for the empty set.
int	node_count (std::size_t k) const
	Number of live nodes at level k.
const std::vector< int > &	arcs (std::size_t k, int id) const
	Arc row of level-k node id (1-based id).
void	insert (const std::vector< int > &state)
	Add a K-tuple of 0-based local values to the set.
bool	member (const std::vector< int > &state) const
	True iff state is in the set; O(K).
long long	cardinality () const
	|S|, the number of stored states.
long long	index (const std::vector< int > &state) const
	0-based lexicographic rank of state among the stored set, level 0 most significant, or -1 when the state is not stored.
std::vector< std::vector< int > >	enumerate () const
	All stored states as rows, in index() order.
MddStruct	to_struct () const
	Export the diagram as plain arrays for downstream algorithms.
void	compact ()
	Reclaim dead nodes left by the append-only build.
MddStats	stats () const
	Storage description of the current set; only reachable nodes are counted.

Static Public Member Functions
static MDD	from_states (const std::vector< int > &domain, const std::vector< std::vector< int > > &states)
	Build from a set of 0-based state tuples.

Detailed Description

The diagram: insert / member / index / enumerate / cardinality.

Definition at line 97 of file mdd.h.

Constructor & Destructor Documentation

MDD()

line::mdd::MDD::MDD ( const std::vector< int > & domain )

inlineexplicit

An empty set over the given per-level domains.

Definition at line 100 of file mdd.h.

References domain(), line::InputError::InputError(), and line::mdd::TERM_FALSE.

Referenced by from_states().

Member Function Documentation

arcs()

const std::vector< int > & line::mdd::MDD::arcs ( std::size_t k, int id ) const

inline

Arc row of level-k node id (1-based id).

Definition at line 125 of file mdd.h.

cardinality()

long long line::mdd::MDD::cardinality ( ) const

inline

|S|, the number of stored states.

Definition at line 145 of file mdd.h.

Referenced by line::mdd::mdd_closedqn(), line::ctmc::solver_ctmc_mdd_analyzer(), and stats().

compact()

void line::mdd::MDD::compact ( )

inline

Reclaim dead nodes left by the append-only build.

Membership, index and enumerate are unchanged. A production MDD would reference-count instead and never accumulate dead nodes; this is the basic sweep.

Definition at line 202 of file mdd.h.

References line::mdd::TERM_FALSE.

Referenced by line::mdd::mdd_reachset(), and line::spn::spn_mdd().

domain()

const std::vector< int > & line::mdd::MDD::domain ( ) const

inline

Definition at line 119 of file mdd.h.

Referenced by from_states(), and MDD().

enumerate()

std::vector< std::vector< int > > line::mdd::MDD::enumerate ( ) const

inline

All stored states as rows, in index() order.

Definition at line 172 of file mdd.h.

References line::mdd::TERM_FALSE.

Referenced by line::mdd::mdd_closedqn(), and line::spn::spn_pf().

from_states()

MDD line::mdd::MDD::from_states ( const std::vector< int > & domain, const std::vector< std::vector< int > > & states )

inlinestatic

Build from a set of 0-based state tuples.

Definition at line 111 of file mdd.h.

References domain(), insert(), and MDD().

index()

long long line::mdd::MDD::index ( const std::vector< int > & state ) const

inline

0-based lexicographic rank of state among the stored set, level 0 most significant, or -1 when the state is not stored.

This is a bijection S -> {0,...,|S|-1}, so a generator matrix can be assembled without an explicit state list.

Definition at line 157 of file mdd.h.

References line::mdd::TERM_FALSE, and line::mdd::TERM_TRUE.

Referenced by line::mdd::mdd_closedqn().

insert()

void line::mdd::MDD::insert ( const std::vector< int > & state )

inline

Add a K-tuple of 0-based local values to the set.

Definition at line 128 of file mdd.h.

References line::InputError::InputError().

Referenced by from_states(), line::mdd::mdd_reachset(), and line::spn::spn_mdd().

K()

std::size_t line::mdd::MDD::K ( ) const

inline

Definition at line 118 of file mdd.h.

Referenced by line::mdd::mdd_to_string().

member()

bool line::mdd::MDD::member ( const std::vector< int > & state ) const

inline

True iff state is in the set; O(K).

Definition at line 135 of file mdd.h.

References line::mdd::TERM_FALSE, and line::mdd::TERM_TRUE.

Referenced by line::mdd::mdd_reachset(), and line::spn::spn_mdd().

node_count()

int line::mdd::MDD::node_count ( std::size_t k ) const

inline

Number of live nodes at level k.

Definition at line 123 of file mdd.h.

root()

int line::mdd::MDD::root ( ) const

inline

Id of the root node, or TERM_FALSE for the empty set.

Definition at line 121 of file mdd.h.

stats()

MddStats line::mdd::MDD::stats ( ) const

inline

Storage description of the current set; only reachable nodes are counted.

Definition at line 233 of file mdd.h.

References cardinality(), line::mdd::MddStats::explicit_ints, line::mdd::MddStats::levels, line::mdd::MddStats::mdd_ints, line::mdd::MddStats::nodes_per_level, line::mdd::MddStats::num_nodes, line::mdd::MddStats::num_states, and line::mdd::MddStats::table_nodes.

Referenced by line::mdd::mdd_closedqn(), and line::mdd::mdd_to_string().

to_struct()

MddStruct line::mdd::MDD::to_struct ( ) const

inline

Export the diagram as plain arrays for downstream algorithms.

Definition at line 181 of file mdd.h.

References line::mdd::MddStruct::domain, line::mdd::MddStruct::K, line::mdd::MddStruct::nnodes, line::mdd::MddStruct::node, and line::mdd::MddStruct::root.

Referenced by line::ctmc::solver_ctmc_mdd_analyzer(), and line::spn::spn_mdd().

---

The documentation for this class was generated from the following file:

• include/line/api/mdd/mdd.h