line::mdd::MddStats Struct Reference

Storage description of the set held in an MDD. More...

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

Collaboration diagram for line::mdd::MddStats:

Public Member Functions
double	compression () const
	Explicit footprint divided by the diagram footprint.

Public Attributes
std::size_t	levels = 0
std::vector< int >	nodes_per_level
	Reachable node count per level.
int	num_nodes = 0
	Reachable non-terminal nodes.
int	table_nodes = 0
	Nodes physically held in the tables, dead ones included.
long long	num_states = 0
	|S|.
long long	mdd_ints = 0
	Integers in the reachable arc arrays, the diagram footprint.
long long	explicit_ints = 0
	Integers an explicit state list would need, |S| * K.

Detailed Description

Storage description of the set held in an MDD.

Definition at line 74 of file mdd.h.

Member Function Documentation

compression()

double line::mdd::MddStats::compression ( ) const

inline

Explicit footprint divided by the diagram footprint.

Definition at line 90 of file mdd.h.

References explicit_ints, and mdd_ints.

Member Data Documentation

explicit_ints

long long line::mdd::MddStats::explicit_ints = 0

Integers an explicit state list would need, |S| * K.

Definition at line 87 of file mdd.h.

Referenced by compression(), line::mdd::mdd_to_string(), and line::mdd::MDD::stats().

levels

std::size_t line::mdd::MddStats::levels = 0

Definition at line 75 of file mdd.h.

Referenced by line::mdd::MDD::stats().

mdd_ints

long long line::mdd::MddStats::mdd_ints = 0

Integers in the reachable arc arrays, the diagram footprint.

Definition at line 85 of file mdd.h.

Referenced by compression(), line::mdd::mdd_to_string(), and line::mdd::MDD::stats().

nodes_per_level

std::vector<int> line::mdd::MddStats::nodes_per_level

Reachable node count per level.

Definition at line 77 of file mdd.h.

Referenced by line::mdd::MDD::stats().

num_nodes

int line::mdd::MddStats::num_nodes = 0

Reachable non-terminal nodes.

Definition at line 79 of file mdd.h.

Referenced by line::mdd::mdd_to_string(), and line::mdd::MDD::stats().

num_states

long long line::mdd::MddStats::num_states = 0

|S|.

Definition at line 83 of file mdd.h.

Referenced by line::mdd::mdd_to_string(), and line::mdd::MDD::stats().

table_nodes

int line::mdd::MddStats::table_nodes = 0

Nodes physically held in the tables, dead ones included.

Definition at line 81 of file mdd.h.

Referenced by line::mdd::mdd_to_string(), and line::mdd::MDD::stats().

---

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

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