Package jline.api.mdd

Class MDD

java.lang.Object
jline.api.mdd.MDD
public class MDD extends Object
Quasi-reduced ordered Multi-valued Decision Diagram.

Compact symbolic store for a set of discrete states, 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|) as in an explicit state list.

Two constant terminals encode the boolean value of a completed path: TERM_FALSE = 0 (empty subgraph) and TERM_TRUE = -1 (state in set). Node ids are 1-based positive integers so that 0 can serve as TERM_FALSE, matching the MATLAB and python implementations.

See Also:

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    final int[]
    domain
    domain[k] is the number of local states at level k.
    final int
    K
    Number of variable levels.
    static final int
    TERM_FALSE
    Terminal node "0": empty subgraph.
    static final int
    TERM_TRUE
    Terminal node "1": a completed path is accepted.

  • Constructor Summary

    Constructors
    Constructor
    Description
    MDD(int[] domain)
    Create an empty set over the given per-level domains.

  • Method Summary

    Modifier and Type
    Method
    Description
    int[]
    arcs(int k, int id)
    Arc row of level-k node id (1-based id); the array is the live one, do not mutate.
    long
    cardinality()
    |S|, the number of stored states.
    void
    compact()
    Reclaim dead nodes left by the append-only build.
    int[][]
    enumerate()
    All stored states as rows, in index() order.
    static MDD
    fromStates(int[] domain, int[][] states)
    Build an MDD from a set of 0-based state tuples.
    int
    getRoot()
    Id of the root node, or TERM_FALSE for the empty set.
    long
    index(int[] state)
    0-based lexicographic rank of state among the stored set, level 0 most significant, or -1 when the state is not stored.
    void
    insert(int[] state)
    Add a K-tuple of 0-based local values to the set.
    boolean
    member(int[] state)
    True iff state is in the set; O(K).
    int
    nodeCount(int k)
    Number of live nodes at level k.
    MddStats
    stats()
    Storage description of the current set; only reachable nodes are counted.
    String
    toString()
     
    MddStruct
    toStruct()
    Export the diagram as plain arrays for downstream algorithms.

    Methods inherited from class java.lang.Object

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

  • Field Details

    • TERM_TRUE

      public static final int TERM_TRUE
      Terminal node "1": a completed path is accepted.
      See Also:

    • TERM_FALSE

      public static final int TERM_FALSE
      Terminal node "0": empty subgraph.
      See Also:

    • K

      public final int K
      Number of variable levels.

    • domain

      public final int[] domain
      domain[k] is the number of local states at level k.

  • Constructor Details

    • MDD

      public MDD(int[] domain)
      Create an empty set over the given per-level domains.

  • Method Details

    • fromStates

      public static MDD fromStates(int[] domain, int[][] states)
      Build an MDD from a set of 0-based state tuples.

    • insert

      public void insert(int[] state)
      Add a K-tuple of 0-based local values to the set.

    • member

      public boolean member(int[] state)
      True iff state is in the set; O(K).

    • cardinality

      public long cardinality()
      |S|, the number of stored states.

    • getRoot

      public int getRoot()
      Id of the root node, or TERM_FALSE for the empty set.

    • nodeCount

      public int nodeCount(int k)
      Number of live nodes at level k.

    • arcs

      public int[] arcs(int k, int id)
      Arc row of level-k node id (1-based id); the array is the live one, do not mutate.

    • index

      public long index(int[] state)
      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 to {0,...,|S|-1}, so a generator matrix can be assembled without an explicit state list.

    • enumerate

      public int[][] enumerate()
      All stored states as rows, in index() order.

    • toStruct

      public MddStruct toStruct()
      Export the diagram as plain arrays for downstream algorithms.

    • compact

      public void compact()
      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.

    • stats

      public MddStats stats()
      Storage description of the current set; only reachable nodes are counted.

    • toString

      public String toString()
      Overrides:
      toString in class Object