mdd_reachset.h File Reference

Reachability set generation into a decision diagram. More...

#include <cstddef>
#include <vector>
#include "line/api/mdd/mdd.h"
#include "line/api/mdd/mdd_types.h"

Include dependency graph for mdd_reachset.h:

Go to the source code of this file.

Namespaces
namespace	line
namespace	line::mdd

Functions
MDD	line::mdd::mdd_reachset (const std::vector< int > &domain, const std::vector< int > &init, const MddNextState &nextfun)
	Generate and store the reachability set into a quasi-reduced ordered MDD.

Detailed Description

Reachability set generation into a decision diagram.

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

This is the basic (explicit-frontier) realisation: a breadth-first search enumerates successors while the MDD provides the O(K) membership test that replaces the usual explicit visited hash. The stored set lives entirely in the MDD (O(#nodes) memory); only the transient BFS frontier is held explicitly. Symbolic image computation / saturation, which removes the explicit frontier too, is the natural next step but is out of scope here and is what caps the wall-clock saving – the storage saving is real regardless.

Definition in file mdd_reachset.h.