mdd.h File Reference

Quasi-reduced ordered Multi-valued Decision Diagram. More...

#include <algorithm>
#include <cstddef>
#include <map>
#include <string>
#include <vector>
#include "line/util/error.h"

Include dependency graph for mdd.h:

Go to the source code of this file.

Classes
struct	line::mdd::MddStruct
	Plain-array export of an MDD, the input contract of mdd_mcd. More...
struct	line::mdd::MddStats
	Storage description of the set held in an MDD. More...
class	line::mdd::MDD
	The diagram: insert / member / index / enumerate / cardinality. More...

Namespaces
namespace	line
namespace	line::mdd

Functions
std::string	line::mdd::mdd_to_string (const MDD &m)
	Human-readable storage summary, the twin of MDD.toString.

Variables
const int	line::mdd::TERM_TRUE = -1
	Terminal node "1": a completed path is accepted.
const int	line::mdd::TERM_FALSE = 0
	Terminal node "0": empty subgraph.

Detailed Description

Quasi-reduced ordered Multi-valued Decision Diagram.

Port of matlab/src/api/mdd/MDD.m, jline.api.mdd.MDD and python/line_solver/api/mdd/mdd.py, after A.S. Miner, G. Ciardo, "Efficient Reachability Set Generation and Storage Using Decision Diagrams", ICATPN 1999, LNCS 1639, pp.6-25.

A global state is a K-tuple of LOCAL state values, one per level/submodel, state[k] in {0,...,domain[k]-1}. The set is stored as a directed acyclic graph with K variable levels plus a terminal level: level 0 is the top (root), a node at level k has domain[k] outgoing arcs to level k+1 nodes, and a state belongs to the set iff its path of arcs reaches the TRUE terminal. Canonicity is enforced by a per-level unique table (no duplicate nodes) and by collapsing the all-FALSE node to the FALSE terminal. Storage is O(#nodes), typically O(K * #local-states), instead of O(|S|).

Node ids are 1-based in every codebase so that 0 can serve as TERM_FALSE, and the unique table is keyed by the arc row itself: the encodings differ across codebases (a byte-packed string in MATLAB, a tuple key in python) but the canonical form does not.

The diagram is pure combinatorics, so unlike the rest of the api layer it is NOT templated on the numeric type: no rate ever enters it.

Definition in file mdd.h.