Package org.jreliability.bdd.javabdd

Class JBDD<T>

java.lang.Object
org.jreliability.bdd.javabdd.JBDD<T>
Type Parameters:
T - the type of the variables
All Implemented Interfaces:
BDD<T>
public class JBDD<T> extends Object implements BDD<T>
The JBDD is a BDD based on the JavaBDD standard java implementation.

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    protected com.github.javabdd.BDD
    bdd
     
    protected JBDDProvider<T>
    provider
     

  • Method Summary

    Modifier and Type
    Method
    Description
    Iterator<BDD<T>>
    allsat()
    Returns a BDD Iterator containing all satisfying variable assignments.
    BDD<T>
    and(BDD<T> that)
    Returns the logical and of two BDDs.
    void
    andWith(Collection<T> that)
    Makes this BDD the logical and of this and that variables.
    void
    andWith(BDD<T> that)
    Makes this BDD the logical and of this and that BDD.
    void
    andWith(T that)
    Makes this BDD the logical and of this and that variable.
    BDD<T>
    copy()
    Returns a copy of this BDD.
    boolean
    equals(Object that)
    TODO Returns true if this BDD equals that BDD.
    BDD<T>
    exist(T variable)
    Returns this BDD after an existential quantification of the specified variable.
    BDD<T>
    forAll(T variable)
    Returns this BDD after a universal quantification of the specified variable.
    void
    free()
    Destroys this BDD.
    BDDProvider<T>
    getProvider()
    Returns the used BDDProvider.
    Set<T>
    getVariables()
    Returns the set of variables that are used in this BDD.
    int
    hashCode()
     
    BDD<T>
    high()
    Returns the true or 1 branch of this BDD.
    BDD<T>
    imp(BDD<T> that)
    Returns the logical implication of two BDDs.
    void
    impWith(BDD<T> that)
    Returns the logical implication of two BDDs.
    void
    impWith(T that)
    Makes this BDD the logical implication of this and that variable.
    boolean
    isOne()
    Returns true if this BDD is the one BDD.
    boolean
    isZero()
    Returns true if this BDD is the zero BDD.
    BDD<T>
    ite(BDD<T> thenBDD, BDD<T> elseBDD)
    Returns the if-then-else} BDD with this BDD being the if, the thenBDD being the then and elseBDD being the else statement.
    int
    level()
    Returns the level of this BDD.
    BDD<T>
    low()
    Returns the false or 0 branch of this BDD.
    int
    nodeCount()
    Returns the number of node in this BDD.
    BDD<T>
    not()
    Returns a BDD that is the negation of this BDD.
    BDD<T>
    or(BDD<T> that)
    Returns the logical or of two BDDs.
    void
    orWith(Collection<T> that)
    Makes this BDD the logical or of this and that variables.
    void
    orWith(BDD<T> that)
    Makes this BDD the logical or of this and that BDD.
    void
    orWith(T that)
    Makes this BDD the logical or of this and that variable.
    BDD<T>
    replace(T variable1, T variable2)
    Returns a BDD where the variable for variable1 is replaced with the variable of variable2.
    void
    replaceWith(T variable1, T variable2)
    Replaces the variable for variable1 with the variable of variable2 in this BDD.
    BDD<T>
    restrict(BDD<T> that)
    Returns a BDD where the variables of that BDD are set to constant reliabilityFunctions in this BDD.
    void
    restrictWith(BDD<T> that)
    Restricts the variables of that to constant reliabilityFunctions in this BDD.
    BDD<T>
    sat()
    Returns one satisfying variable assignment as a BDD.
    String
    toString()
     
    T
    var()
    Returns the variable labeling the BDD.
    BDD<T>
    xor(BDD<T> that)
    Returns the logical xor of two BDDs.
    void
    xorWith(BDD<T> that)
    Makes this BDD the logical xor of this and that BDD.
    void
    xorWith(T that)
    Makes this BDD the logical xor of this and that variable.

    Methods inherited from class java.lang.Object

    clone, finalize, getClass, notify, notifyAll, wait, wait, wait

  • Field Details

    • provider

      protected JBDDProvider<T> provider

    • bdd

      protected com.github.javabdd.BDD bdd

  • Method Details

    • allsat

      public Iterator<BDD<T>> allsat()
      Description copied from interface: BDD
      Returns a BDD Iterator containing all satisfying variable assignments.
      Specified by:
      allsat in interface BDD<T>
      Returns:
      all satisfying variable assignments

    • and

      public BDD<T> and(BDD<T> that)
      Description copied from interface: BDD
      Returns the logical and of two BDDs. Note: Both BDDs remain unchanged after this and-operation.
      Specified by:
      and in interface BDD<T>
      Parameters:
      that - the BDD to and with this BDD
      Returns:
      the logical and of the two BDDs

    • andWith

      public void andWith(BDD<T> that)
      Description copied from interface: BDD
      Makes this BDD the logical and of this and that BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
      Specified by:
      andWith in interface BDD<T>
      Parameters:
      that - the BDD to and with this BDD

    • equals

      public boolean equals(Object that)
      Description copied from interface: BDD
      TODO Returns true if this BDD equals that BDD.
      Specified by:
      equals in interface BDD<T>
      Overrides:
      equals in class Object
      Parameters:
      that - the BDD to compare with this BDD
      Returns:
      true if this BDD equals that BDD

    • exist

      public BDD<T> exist(T variable)
      Description copied from interface: BDD
      Returns this BDD after an existential quantification of the specified variable.
      Specified by:
      exist in interface BDD<T>
      Parameters:
      variable - the variable for the existential quantification
      Returns:
      this BDD after an existential quantification of the specified variables

    • forAll

      public BDD<T> forAll(T variable)
      Description copied from interface: BDD
      Returns this BDD after a universal quantification of the specified variable.
      Specified by:
      forAll in interface BDD<T>
      Parameters:
      variable - the variable for the universal quantification
      Returns:
      this BDD after a universal quantification of the specified variables

    • getProvider

      public BDDProvider<T> getProvider()
      Description copied from interface: BDD
      Returns the used BDDProvider.
      Specified by:
      getProvider in interface BDD<T>
      Returns:
      the used bdd provider

    • high

      public BDD<T> high()
      Description copied from interface: BDD
      Returns the true or 1 branch of this BDD.
      Specified by:
      high in interface BDD<T>
      Returns:
      the true or 1 branch of this BDD

    • isOne

      public boolean isOne()
      Description copied from interface: BDD
      Returns true if this BDD is the one BDD.
      Specified by:
      isOne in interface BDD<T>
      Returns:
      true if this BDD is the one BDD

    • isZero

      public boolean isZero()
      Description copied from interface: BDD
      Returns true if this BDD is the zero BDD.
      Specified by:
      isZero in interface BDD<T>
      Returns:
      true if this BDD is the zero BDD

    • ite

      public BDD<T> ite(BDD<T> thenBDD, BDD<T> elseBDD)
      Description copied from interface: BDD
      Returns the if-then-else} BDD with this BDD being the if, the thenBDD being the then and elseBDD being the else statement.
      Specified by:
      ite in interface BDD<T>
      Parameters:
      thenBDD - the BDD for the then statement
      elseBDD - the BDD for the else statement
      Returns:
      the if-then-else BDD

    • level

      public int level()
      Description copied from interface: BDD
      Returns the level of this BDD.
      Specified by:
      level in interface BDD<T>
      Returns:
      the level of this BDD

    • low

      public BDD<T> low()
      Description copied from interface: BDD
      Returns the false or 0 branch of this BDD.
      Specified by:
      low in interface BDD<T>
      Returns:
      the false or 0 branch of this BDD

    • not

      public BDD<T> not()
      Description copied from interface: BDD
      Returns a BDD that is the negation of this BDD.
      Specified by:
      not in interface BDD<T>
      Returns:
      a BDD that is the negation of this BDD

    • nodeCount

      public int nodeCount()
      Description copied from interface: BDD
      Returns the number of node in this BDD.
      Specified by:
      nodeCount in interface BDD<T>
      Returns:
      the number of nodes in this bdd

    • or

      public BDD<T> or(BDD<T> that)
      Description copied from interface: BDD
      Returns the logical or of two BDDs. Note: Both BDDs remain unchanged after this or-operation.
      Specified by:
      or in interface BDD<T>
      Parameters:
      that - the BDD to or with this BDD
      Returns:
      the logical or of the two BDDs

    • orWith

      public void orWith(BDD<T> that)
      Description copied from interface: BDD
      Makes this BDD the logical or of this and that BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
      Specified by:
      orWith in interface BDD<T>
      Parameters:
      that - the BDD to or with this BDD

    • replace

      public BDD<T> replace(T variable1, T variable2)
      Description copied from interface: BDD
      Returns a BDD where the variable for variable1 is replaced with the variable of variable2.
      Specified by:
      replace in interface BDD<T>
      Parameters:
      variable1 - the first variable
      variable2 - the second variable
      Returns:
      a BDD where the variable for variable1 is replaced with the variable of variable2

    • replaceWith

      public void replaceWith(T variable1, T variable2)
      Description copied from interface: BDD
      Replaces the variable for variable1 with the variable of variable2 in this BDD.
      Specified by:
      replaceWith in interface BDD<T>
      Parameters:
      variable1 - the first variable
      variable2 - the second variable

    • restrict

      public BDD<T> restrict(BDD<T> that)
      Description copied from interface: BDD
      Returns a BDD where the variables of that BDD are set to constant reliabilityFunctions in this BDD. Note: Both BDDs remain unchanged after this or-operation.
      Specified by:
      restrict in interface BDD<T>
      Parameters:
      that - the BDD to restrict this BDD with
      Returns:
      a new BDD representing this BDD restricted with that BDD

    • restrictWith

      public void restrictWith(BDD<T> that)
      Description copied from interface: BDD
      Restricts the variables of that to constant reliabilityFunctions in this BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
      Specified by:
      restrictWith in interface BDD<T>
      Parameters:
      that - the BDD to restrict this BDD with

    • sat

      public BDD<T> sat()
      Description copied from interface: BDD
      Returns one satisfying variable assignment as a BDD.
      Specified by:
      sat in interface BDD<T>
      Returns:
      one satisfying variable assignment as a BDD

    • var

      public T var()
      Description copied from interface: BDD
      Returns the variable labeling the BDD.
      Specified by:
      var in interface BDD<T>
      Returns:
      the variable labeling the BDD

    • xor

      public BDD<T> xor(BDD<T> that)
      Description copied from interface: BDD
      Returns the logical xor of two BDDs. Note: Both BDDs remain unchanged after this xor-operation.
      Specified by:
      xor in interface BDD<T>
      Parameters:
      that - the BDD to xor with this BDD
      Returns:
      the logical xor of the two BDDs

    • xorWith

      public void xorWith(BDD<T> that)
      Description copied from interface: BDD
      Makes this BDD the logical xor of this and that BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
      Specified by:
      xorWith in interface BDD<T>
      Parameters:
      that - the BDD to xor with this BDD

    • imp

      public BDD<T> imp(BDD<T> that)
      Description copied from interface: BDD
      Returns the logical implication of two BDDs. Note: Both BDDs remain unchanged after this and-operation.
      Specified by:
      imp in interface BDD<T>
      Parameters:
      that - the BDD to implicate with this BDD
      Returns:
      the logical implication of the two BDDs

    • impWith

      public void impWith(BDD<T> that)
      Description copied from interface: BDD
      Returns the logical implication of two BDDs. Note: That BDD is consumed(!) within this operation and invalid afterwards.
      Specified by:
      impWith in interface BDD<T>
      Parameters:
      that - the BDD to implicate with this BDD

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Object

    • andWith

      public void andWith(Collection<T> that)
      Description copied from interface: BDD
      Makes this BDD the logical and of this and that variables.
      Specified by:
      andWith in interface BDD<T>
      Parameters:
      that - the variables to and with this BDD

    • andWith

      public void andWith(T that)
      Description copied from interface: BDD
      Makes this BDD the logical and of this and that variable.
      Specified by:
      andWith in interface BDD<T>
      Parameters:
      that - the variable to and with this BDD

    • orWith

      public void orWith(Collection<T> that)
      Description copied from interface: BDD
      Makes this BDD the logical or of this and that variables.
      Specified by:
      orWith in interface BDD<T>
      Parameters:
      that - the variables to or with this BDD

    • orWith

      public void orWith(T that)
      Description copied from interface: BDD
      Makes this BDD the logical or of this and that variable.
      Specified by:
      orWith in interface BDD<T>
      Parameters:
      that - the variable to or with this BDD

    • impWith

      public void impWith(T that)
      Description copied from interface: BDD
      Makes this BDD the logical implication of this and that variable.
      Specified by:
      impWith in interface BDD<T>
      Parameters:
      that - the variable to implicate with this BDD

    • xorWith

      public void xorWith(T that)
      Description copied from interface: BDD
      Makes this BDD the logical xor of this and that variable.
      Specified by:
      xorWith in interface BDD<T>
      Parameters:
      that - the variable to or with this BDD

    • copy

      public BDD<T> copy()
      Description copied from interface: BDD
      Returns a copy of this BDD.
      Specified by:
      copy in interface BDD<T>
      Returns:
      a copy of this object

    • getVariables

      public Set<T> getVariables()
      Description copied from interface: BDD
      Returns the set of variables that are used in this BDD.
      Specified by:
      getVariables in interface BDD<T>
      Returns:
      the set of variables that are used in this bdd

    • free

      public void free()
      Description copied from interface: BDD
      Destroys this BDD.
      Specified by:
      free in interface BDD<T>