Package jline.api.mdd

Class Mdd_reachset

java.lang.Object

jline.api.mdd.Mdd_reachset

public class Mdd_reachset
extends Object

Reachability set generation into a decision diagram.

After A.S. Miner, G. Ciardo, "Efficient Reachability Set Generation and Storage Using Decision Diagrams", ICATPN 1999, LNCS 1639, pp.6-25.

Method Summary

Modifier and Type	Method	Description
static MDD	mdd_reachset(int[] domain, int[] init, MddNextState nextfun)	Generate and store the reachability set into a quasi-reduced ordered MDD.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

mdd_reachset

public static MDD mdd_reachset(int[] domain,
 int[] init,
 MddNextState nextfun)

Generate and store the reachability set into a quasi-reduced ordered MDD.

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.

Parameters:

domain - per-level local-state counts, values 0..domain[k]-1

init - the initial global state, 0-based local values

nextfun - the next-state function

Returns:

an MDD holding every state reachable from init