Package | Description |
---|---|
de.uni_due.inf.ti.raven.actions |
General Action Classes.
|
de.uni_due.inf.ti.raven.algorithms |
Classes to run different algorithms.
|
de.uni_due.inf.ti.raven.data.automata |
Classes to create, represent, manipulate automata.
|
de.uni_due.inf.ti.raven.data.bdd |
Classes to create, represent and manipulate binary decision diagrams (BDDs).
|
de.uni_due.inf.ti.raven.encodings |
Classes to encode the state space and the transitions of the various graph automata.
|
de.uni_due.inf.ti.raven.gui |
GUI Classes.
|
de.uni_due.inf.ti.raven.gui.graphs |
GUI Classes to visualize graphs.
|
de.uni_due.inf.ti.raven.io |
Classes to load, save and print data.
|
Modifier and Type | Method and Description |
---|---|
RavenBDD |
SimulationComputationAction.getResult() |
RavenBDD |
ReachabilityAction.getResult() |
Constructor and Description |
---|
PrintAction(BDDPrinter printer,
RavenBDD bdd)
Creates an action which prints a BDD to a given printer.
|
PrintDotAction(DotPrinter printer,
RavenBDD bdd)
Creates an action which prints a BDD to a given printer.
|
SimulationCheckingAction(RavenBDD simulation,
RavenBDD firstSet,
RavenBDD secondSet)
Creates a new
Action to check for the automaton automaton whether the
state set firstSet is simulated by the state set secondSet . |
Modifier and Type | Method and Description |
---|---|
RavenBDD |
IdentityRelationAlgorithm.getIdentityRelation(Automaton automaton)
Returns the identity relation on the states of the automaton
automaton . |
RavenBDD |
ForwardSimulationAlgorithm.getSimulation(Automaton automaton) |
RavenBDD |
SimulationAlgorithm.getSimulation(Automaton automaton)
Returns the simulation relation on the states of the automaton
automaton . |
RavenBDD |
BackwardSimulationAlgorithm.getSimulation(Automaton automaton) |
RavenBDD |
ForwardSimulationAlgorithm.getSimulation(Automaton firstAutomaton,
Automaton secondAutomaton) |
RavenBDD |
SimulationAlgorithm.getSimulation(Automaton firstAutomaton,
Automaton secondAutomaton)
Returns the simulation relation on the states of the automata
firstAutomaton
and secondAutomaton . |
RavenBDD |
BackwardSimulationAlgorithm.getSimulation(Automaton firstAutomaton,
Automaton secondAutomaton) |
Modifier and Type | Method and Description |
---|---|
boolean |
ForwardSimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
Automaton secondAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet) |
boolean |
SimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
Automaton secondAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet)
Returns
true if and only if the state set firstStateSet of the first
automaton firstAutomaton is simulated by the state set secondStateSet
of the second automaton secondAutomaton . |
boolean |
BackwardSimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
Automaton secondAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet) |
boolean |
ForwardSimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet) |
boolean |
SimulationAlgorithm.isSimulatedBy(Automaton automaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet)
Returns
true if and only if the state set firstStateSet of the automaton
automaton is simulated by the second state set secondStateSet of the
automaton automaton . |
boolean |
BackwardSimulationAlgorithm.isSimulatedBy(Automaton firstAutomaton,
RavenBDD firstStateSet,
RavenBDD secondStateSet) |
Modifier and Type | Method and Description |
---|---|
RavenBDD |
Automaton.getCurrentInterfaceSize(RavenBDD states)
Returns the interface size of the states in the given state set
states . |
RavenBDD |
Automaton.getFinalStates()
Returns the final state set encoded as an BDD.
|
RavenBDD |
Automaton.getInitialStates()
Returns the initial state set encoded as an BDD.
|
RavenBDD |
Automaton.getNonFinalStates()
Returns the non-final state set encoded as an BDD.
|
RavenBDD |
Automaton.getNonFinalStates(int size)
Returns the set of non-final states for the interface of size
size encoded as an BDD. |
RavenBDD |
Automaton.getPredecessorStates(RavenBDD currentStates,
Operation letter)
Returns the set of predecessor states for a given set of current states
and and a given input letter (i.e. a graph operation).
|
RavenBDD |
Automaton.getReachableStates(CospanDecomposition decomposition)
Returns the set of reachable states for a given graph decomposition
starting with the initial states.
|
RavenBDD |
Automaton.getStates()
Returns the state set encoded as an BDD.
|
RavenBDD |
Automaton.getStates(int size)
Returns the state set for the interface of size
size encoded as an BDD. |
RavenBDD |
Automaton.getStatesWithoutSuccessorFor(Operation letter)
Returns the set of states which have no successor state for the given
letter |
RavenBDD |
Automaton.getSuccessorStates(RavenBDD currentStates,
Operation letter)
Returns the set of successor states for a given set of current states and
and a given input letter (i.e. a graph operation).
|
RavenBDD |
Automaton.getTransitionRelation(Operation letter)
Returns the transition relation for the given letter
|
Modifier and Type | Method and Description |
---|---|
Map<Operation,RavenBDD> |
Automaton.getStateTransBDDs()
Returns the Transition BDD Map For saving purposes only
|
Modifier and Type | Method and Description |
---|---|
boolean |
Automaton.containsInitialState(RavenBDD stateSet)
Returns
true if the state set stateSet contains at least one
initial state. |
RavenBDD |
Automaton.getCurrentInterfaceSize(RavenBDD states)
Returns the interface size of the states in the given state set
states . |
int |
ColorabilityAutomaton.getNodeColor(RavenBDD state,
int node)
Returns the color of the
node -th interface node in the state state . |
RavenBDD |
Automaton.getPredecessorStates(RavenBDD currentStates,
Operation letter)
Returns the set of predecessor states for a given set of current states
and and a given input letter (i.e. a graph operation).
|
String |
Automaton.getStateName(RavenBDD state)
Returns the state name of a single state encoded as bdd.
|
RavenBDD |
Automaton.getSuccessorStates(RavenBDD currentStates,
Operation letter)
Returns the set of successor states for a given set of current states and
and a given input letter (i.e. a graph operation).
|
boolean |
SubgraphAutomaton.hasRecognizedEdge(RavenBDD state,
String edgeName)
Returns
true if and only if in the state state the edge
with name edgeName has been recognized. |
boolean |
Automaton.isAcceptingStateSet(RavenBDD stateSet)
Returns
true if the state set stateSet is a subset of the
final state set. |
boolean |
Automaton.isApplicable(Operation letter,
RavenBDD states)
Returns
true if the letter letter is applicable to the
states states , i.e. there exists at least one successor state
according to the transition relation for the letter letter . |
boolean |
DominatingSetAutomaton.isInDominatingSet(RavenBDD state,
int node)
Returns
true if and only if the interface at position node is a node of the
dominating set. |
boolean |
Automaton.isInitialStateSet(RavenBDD stateSet)
Returns
true if the state set stateSet is a subset of the
initial state set. |
boolean |
VertexCoverAutomaton.isInVertexCover(RavenBDD state,
int node)
Returns
true if and only if in the state state the node -th
interface is in the vertex cover. |
boolean |
SubgraphAutomaton.isNodeInInterface(RavenBDD state,
String nodeName,
int size)
Returns
true if and only if in the state state the node with name
nodeName is in the interface at position size . |
String |
Automaton.printStates(RavenBDD stateSet)
Prints a single state (seen as singleton state set) or a set of states.
|
Modifier and Type | Method and Description |
---|---|
RavenBDD |
RavenBDD.and(RavenBDD bdd)
Returns a BDD which is the logical AND of this BDD and the
BDD
bdd . |
RavenBDD |
RavenBDD.applyAll(RavenBDD bdd,
RavenBDDFactory.BDDOperator operator,
RavenBDD variables)
Applies the operator
operator to this BDD and
the BDD bdd and afterwards performs an universal
quantification of the BDD nodes specified by the BDD
variables . |
RavenBDD |
RavenBDD.applyEx(RavenBDD bdd,
RavenBDDFactory.BDDOperator operator,
RavenBDD variables)
Applies the operator
operator to this BDD and
the BDD bdd and afterwards performs an existential
quantification of the BDD nodes specified by the BDD
variables . |
RavenBDD |
RavenBDD.biimp(RavenBDD bdd)
Returns a BDD which is the logical BIIMPLICATION of this BDD and the
BDD
bdd . |
RavenBDD |
RavenBDD.clone() |
RavenBDD |
RavenBDD.exists(RavenBDD bdd)
Performs an existential quantification of the BDD nodes
specified by the given BDD.
|
RavenBDD |
RavenBDD.forAll(RavenBDD bdd)
Performs an universal quantification of the BDD nodes
specified by the given BDD.
|
RavenBDD |
RavenBDDDomain.getBDDForInteger(int number,
int bitLength)
Returns a BDD representing a (non-negative) integer value
number as binary encoding
of length bitLength . |
RavenBDD |
RavenBDDDomain.getDomainBDD()
Returns a BDD encoding all variables used by this BDD Domain
|
RavenBDD |
RavenBDDDomain.getIthBDD(int i)
Returns a BDD representing the
i -th variable of the BDD-Domain. |
RavenBDD |
RavenBDD.getOne()
Returns the One-BDD.
|
RavenBDD |
RavenBDD.getZero()
Returns the Zero-BDD.
|
RavenBDD |
RavenBDD.high()
Returns the high successor of this BDD.
|
RavenBDD |
RavenBDD.imp(RavenBDD bdd)
Returns a BDD which is the logical IMPLICATION of the this BDD and the
BDD
bdd . |
static RavenBDD |
RavenBDD.loadBDD(InputStream is)
Loads a BDD from the input stream
is ; |
RavenBDD |
RavenBDD.low()
Returns the low successor of this BDD.
|
RavenBDD |
RavenBDD.not()
Returns a BDD which is the logical NOT of this BDD.
|
static RavenBDD |
RavenBDDDomain.one()
Returns the One-BDD.
|
RavenBDD |
RavenBDDFactory.one()
Returns the One-BDD.
|
RavenBDD |
RavenBDD.or(RavenBDD bdd)
Returns a BDD which is the logical OR of this BDD and the
BDD
bdd . |
RavenBDD |
RavenBDD.replace(RavenBDDPairing pairing)
Replaces the BDD nodes according to the given BDD pairing.
|
RavenBDD |
RavenBDD.restrict(RavenBDD bdd)
Restricts the BDD according to the given BDD.
|
RavenBDD |
RavenBDD.xor(RavenBDD bdd)
Returns a BDD which is the logical XOR of this BDD and the
BDD
bdd . |
static RavenBDD |
RavenBDDDomain.zero()
Returns the Zero-BDD.
|
RavenBDD |
RavenBDDFactory.zero()
Returns the Zero-BDD.
|
Modifier and Type | Method and Description |
---|---|
List<RavenBDD> |
RavenBDD.getSatAssignments(RavenBDD var)
Returns a list of satisfying variable assignments (seen as BDDs) for the variables
var . |
Modifier and Type | Method and Description |
---|---|
RavenBDD |
RavenBDD.and(RavenBDD bdd)
Returns a BDD which is the logical AND of this BDD and the
BDD
bdd . |
RavenBDD |
RavenBDD.applyAll(RavenBDD bdd,
RavenBDDFactory.BDDOperator operator,
RavenBDD variables)
Applies the operator
operator to this BDD and
the BDD bdd and afterwards performs an universal
quantification of the BDD nodes specified by the BDD
variables . |
RavenBDD |
RavenBDD.applyEx(RavenBDD bdd,
RavenBDDFactory.BDDOperator operator,
RavenBDD variables)
Applies the operator
operator to this BDD and
the BDD bdd and afterwards performs an existential
quantification of the BDD nodes specified by the BDD
variables . |
RavenBDD |
RavenBDD.biimp(RavenBDD bdd)
Returns a BDD which is the logical BIIMPLICATION of this BDD and the
BDD
bdd . |
RavenBDD |
RavenBDD.exists(RavenBDD bdd)
Performs an existential quantification of the BDD nodes
specified by the given BDD.
|
RavenBDD |
RavenBDD.forAll(RavenBDD bdd)
Performs an universal quantification of the BDD nodes
specified by the given BDD.
|
static int |
RavenBDDDomain.getInteger(RavenBDD bdd)
Returns the integer which is encoded (as bit string) by the BDD
bdd . |
List<RavenBDD> |
RavenBDD.getSatAssignments(RavenBDD var)
Returns a list of satisfying variable assignments (seen as BDDs) for the variables
var . |
RavenBDD |
RavenBDD.imp(RavenBDD bdd)
Returns a BDD which is the logical IMPLICATION of the this BDD and the
BDD
bdd . |
RavenBDD |
RavenBDD.or(RavenBDD bdd)
Returns a BDD which is the logical OR of this BDD and the
BDD
bdd . |
RavenBDD |
RavenBDD.restrict(RavenBDD bdd)
Restricts the BDD according to the given BDD.
|
int |
RavenBDD.satCount(RavenBDD vars)
Returns the number of satisfying assignments to this BDD.
|
static void |
RavenBDD.saveBDD(RavenBDD ravenBDD,
ZipOutputStream zos,
String name)
Writes the BDD
ravenBDD to the stream zos and saves it to the zip file
named name . |
void |
RavenBDDPairing.set(RavenBDD first,
RavenBDD second)
Adds two BDDs as a pair to this BDD pairing.
|
RavenBDD |
RavenBDD.xor(RavenBDD bdd)
Returns a BDD which is the logical XOR of this BDD and the
BDD
bdd . |
Modifier and Type | Method and Description |
---|---|
RavenBDD |
ProductEncoding.convertFinalStates(Automaton automaton)
Converts the final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertFinalStates(Automaton automaton)
Converts the final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
ProductEncoding.convertInitialStates(Automaton automaton)
Converts the initial state set of the given automaton to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertInitialStates(Automaton automaton)
Converts the initial state set of the given automaton to the
UnionEncoding . |
RavenBDD |
ProductEncoding.convertNonFinalStates(Automaton automaton)
Converts the non-final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertNonFinalStates(Automaton automaton)
Converts the non-final state set of the given automaton to the
UnionEncoding . |
RavenBDD |
ProductEncoding.convertStates(Automaton automaton)
Converts the state set of the given automaton to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertStates(Automaton automaton)
Converts the state set of the given automaton to the
UnionEncoding . |
RavenBDD |
ProductEncoding.convertTransitions(Automaton automaton,
Operation letter)
Converts the transitions of the given automaton and the given letter to the
UnionEncoding . |
RavenBDD |
UnionEncoding.convertTransitions(Automaton automaton,
Operation letter)
Converts the transitions of the given automaton and the given letter to the
UnionEncoding . |
RavenBDD |
DefaultPathEncoding.existsPathBit(BDDEncoding.StateType type,
RavenBDD bdd,
int source,
int target) |
RavenBDD |
PathEncoding.existsPathBit(BDDEncoding.StateType type,
RavenBDD bdd,
int source,
int target)
Returns the BDD which describes the existence of an adjacency bit in the
type domain
of the BDD |
abstract RavenBDD |
ColorabilityEncoding.getBDDForColor(BDDEncoding.StateType type,
int node,
int color)
Constructs a BDD which is
true if and only if in the state state
the node -th interface node either has some color color . |
RavenBDD |
DefaultColorabilityEncoding.getBDDForColor(BDDEncoding.StateType type,
int node,
int color) |
RavenBDD |
BDDEncoding.getBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes in state
state the pos -th bit the encoding. |
abstract RavenBDD |
ColorabilityEncoding.getColorBit(BDDEncoding.StateType type,
int node,
int bit)
Returns the
bit -th BDD node of the color encoding of the node -th node
for the state state . |
RavenBDD |
DefaultColorabilityEncoding.getColorBit(BDDEncoding.StateType type,
int node,
int bit) |
abstract RavenBDD |
LinkEncoding.getConnectedNodeBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes in state
state whether the pos -th node of the
interface is connected to an initial node or not. |
RavenBDD |
AnotherLinkEncoding.getConnectedNodeBit(BDDEncoding.StateType type,
int node)
Get the connected (i.e. 2nd) bit of the
node -th (starting with 0) node markings. |
RavenBDD |
DefaultLinkEncoding.getConnectedNodeBit(BDDEncoding.StateType type,
int node)
Get the connected (i.e. 2nd) bit of the
node -th (starting with 0) node markings. |
abstract RavenBDD |
DominatingSetEncoding.getDominationBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that in state
state the node -th interface node
is dominated by some node of the dominating set if and only if the BDD is true . |
RavenBDD |
DefaultDominatingSetEncoding.getDominationBit(BDDEncoding.StateType type,
int node) |
RavenBDD |
AnotherDominatingSetEncoding.getDominationBit(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
DominatingSetEncoding.getDominationSizeBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes in state
state the pos -th bit of the
current size of the dominating set. |
RavenBDD |
DefaultDominatingSetEncoding.getDominationSizeBit(BDDEncoding.StateType type,
int pos) |
RavenBDD |
AnotherDominatingSetEncoding.getDominationSizeBit(BDDEncoding.StateType type,
int pos) |
abstract RavenBDD |
SubgraphEncoding.getEdgeBit(BDDEncoding.StateType type,
int edge)
Returns a BDD which encodes that in state
state the edge -th subgraph edge
has been recognized if and only if the BDD is true . |
RavenBDD |
DefaultSubgraphEncoding.getEdgeBit(BDDEncoding.StateType type,
int edge) |
abstract RavenBDD |
NoIsolatedNodesEncoding.getHasIsolatedNodes(BDDEncoding.StateType type)
Returns a BDD which encodes that in state
state isolated nodes are present
if and only if the BDD is true . |
RavenBDD |
DefaultNoIsolatedNodesEncoding.getHasIsolatedNodes(BDDEncoding.StateType type) |
abstract RavenBDD |
LinkEncoding.getInitialNodeBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes in state
state whether the pos -th node of the
interface is an initial node or not. |
RavenBDD |
AnotherLinkEncoding.getInitialNodeBit(BDDEncoding.StateType type,
int node)
Get the initial (i.e. 1st) bit of the
node -th (starting with 0) node markings. |
RavenBDD |
DefaultLinkEncoding.getInitialNodeBit(BDDEncoding.StateType type,
int node)
Get the initial (i.e. 1st) bit of the
node -th (starting with 0) node markings. |
RavenBDD |
BDDEncoding.getInterfaceBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes the
pos -th interface bit for
the state type type . |
RavenBDD |
BDDEncoding.getInterfaceEncodingBDD()
Returns a BDD encoding the bits of the interface
in the encoding for the current state.
|
RavenBDD |
BDDEncoding.getInterfaceSize(BDDEncoding.StateType type,
int size)
Returns a BDD which encodes the interface size
size for
the state state . |
RavenBDD |
BDDEncoding.getInterfaceSizeIsGreaterOrEqual(BDDEncoding.StateType type,
int size)
Returns a BDD encoding that in the state type
type the size of the
interface is greater or equal to size if and only if the BDD is true . |
RavenBDD |
BDDEncoding.getInterfaceSizeIsLessOrEqual(BDDEncoding.StateType type,
int size)
Returns a BDD encoding that in the state
state the size of the
interface is less or equal to size if and only if the BDD is true . |
abstract RavenBDD |
NoIsolatedNodesEncoding.getIsNodeIsolated(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that in state
state the node -th interface node
is isolated if and only if the BDD is true . |
RavenBDD |
DefaultNoIsolatedNodesEncoding.getIsNodeIsolated(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
SubgraphEncoding.getMappingBit(BDDEncoding.StateType type,
int node,
int pos)
Returns a BDD which encodes that in state
state the node -th subgraph node
is the image of pos -th interface node (of the function mapping the interface into
the subgraph node set) if and only if the BDD is true . |
RavenBDD |
DefaultSubgraphEncoding.getMappingBit(BDDEncoding.StateType type,
int node,
int size) |
abstract RavenBDD |
DominatingSetEncoding.getMembershipBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that the
node -th node of the interface
is a member of the dominating set. |
RavenBDD |
DefaultVertexCoverEncoding.getMembershipBit(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultDominatingSetEncoding.getMembershipBit(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
VertexCoverEncoding.getMembershipBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that the
node -th node of the interface
is a member of the vertex cover. |
RavenBDD |
AnotherDominatingSetEncoding.getMembershipBit(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
SubgraphEncoding.getNodeBit(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that in state
state the node -th subgraph node
has been recognized if and only if the BDD is true . |
RavenBDD |
DefaultSubgraphEncoding.getNodeBit(BDDEncoding.StateType type,
int node) |
RavenBDD |
AnotherPathEncoding.getPathBit(BDDEncoding.StateType type,
int source,
int target) |
RavenBDD |
DefaultPathEncoding.getPathBit(BDDEncoding.StateType type,
int source,
int target) |
abstract RavenBDD |
PathEncoding.getPathBit(BDDEncoding.StateType type,
int from,
int to)
Returns a BDD which encodes the (non)-existence of a path from the
from -th node
in the interface to the to -th node of the interface. |
RavenBDD |
DefaultEdgeCountingEncoding.getRemainderBit(BDDEncoding.StateType type,
int pos) |
abstract RavenBDD |
CountingEncoding.getRemainderBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes in state
state the pos -th bit of the
remainder. |
RavenBDD |
DefaultVertexCountingEncoding.getRemainderBit(BDDEncoding.StateType type,
int pos) |
RavenBDD |
UnionEncoding.getSeparationBit(BDDEncoding.StateType type)
Returns a BDD which encodes that in state
state the separation bit has been set if
and only if the BDD is true . |
RavenBDD |
AnotherPathEncoding.getSourcePathBit(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultPathEncoding.getSourcePathBit(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
PathEncoding.getSourcePathBit(BDDEncoding.StateType type,
int node)
Returns the BDD which encodes whether the
node -th interface node is connected to at
least one of the source nodes. |
RavenBDD |
BDDEncoding.getStateBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes the
pos -th state bit for
the state type type . |
RavenBDD |
BDDEncoding.getStateEncodingBDD()
Returns a BDD encoding the bits of the state information
in the encoding for the current state.
|
abstract RavenBDD |
DominatingSetEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that in state
state the node -th interface node
is not defined if and only if the BDD is true . |
RavenBDD |
DefaultVertexCoverEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultDominatingSetEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node) |
abstract RavenBDD |
NoIsolatedNodesEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that in state
state the node -th interface node
is not defined if and only if the BDD is true . |
abstract RavenBDD |
VertexCoverEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node)
Returns a BDD which encodes that in state
state the node -th interface node
is not defined if and only if the BDD is true . |
RavenBDD |
AnotherDominatingSetEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultNoIsolatedNodesEncoding.getUndefinedNode(BDDEncoding.StateType type,
int node) |
RavenBDD |
DefaultMinimumBoundEncoding.getValueBit(BDDEncoding.StateType type,
int pos) |
RavenBDD |
DefaultMaximumBoundEncoding.getValueBit(BDDEncoding.StateType type,
int pos) |
abstract RavenBDD |
BoundEncoding.getValueBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes the
pos -th bit of the value of the node/edge counter. |
RavenBDD |
DefaultVertexCoverEncoding.getVertexCoverSizeBit(BDDEncoding.StateType type,
int pos) |
abstract RavenBDD |
VertexCoverEncoding.getVertexCoverSizeBit(BDDEncoding.StateType type,
int pos)
Returns a BDD which encodes in state
state the pos -th bit of the
current size of the vertex cover. |
RavenBDD |
BDDEncoding.one()
Returns the
One -BDD for this encoding. |
RavenBDD |
BDDEncoding.zero()
Returns the
Zero -BDD for this encoding. |
Modifier and Type | Method and Description |
---|---|
RavenBDD |
DefaultPathEncoding.existsPathBit(BDDEncoding.StateType type,
RavenBDD bdd,
int source,
int target) |
RavenBDD |
PathEncoding.existsPathBit(BDDEncoding.StateType type,
RavenBDD bdd,
int source,
int target)
Returns the BDD which describes the existence of an adjacency bit in the
type domain
of the BDD |
String |
AnotherPathEncoding.printStates(RavenBDD stateSet) |
abstract String |
BDDEncoding.printStates(RavenBDD stateSet)
Prints a single state (seen as singleton state set) or a set of states.
|
String |
DefaultVertexCoverEncoding.printStates(RavenBDD stateSet) |
String |
DefaultEdgeCountingEncoding.printStates(RavenBDD stateSet) |
String |
DefaultDominatingSetEncoding.printStates(RavenBDD stateSet) |
String |
DefaultMinimumBoundEncoding.printStates(RavenBDD stateSet) |
String |
ProductEncoding.printStates(RavenBDD stateSet) |
String |
UnionEncoding.printStates(RavenBDD stateSet) |
String |
DefaultMaximumBoundEncoding.printStates(RavenBDD stateSet) |
String |
AnotherLinkEncoding.printStates(RavenBDD stateSet) |
String |
DefaultColorabilityEncoding.printStates(RavenBDD stateSet) |
String |
DefaultSubgraphEncoding.printStates(RavenBDD stateSet) |
String |
DefaultPathEncoding.printStates(RavenBDD stateSet) |
String |
AnotherDominatingSetEncoding.printStates(RavenBDD stateSet) |
String |
DefaultVertexCountingEncoding.printStates(RavenBDD stateSet) |
String |
DefaultNoIsolatedNodesEncoding.printStates(RavenBDD stateSet) |
String |
DefaultLinkEncoding.printStates(RavenBDD stateSet) |
Modifier and Type | Method and Description |
---|---|
static InformationPanel<RavenBDD> |
BDDInformationPanelBuilder.createPanel()
Creates an information panel displaying properties of a given Raven BDD.
|
Modifier and Type | Method and Description |
---|---|
void |
BDDDialog.displayBDD(RavenBDD bdd,
BDDEncoding encoding)
Displays the BDD
bdd using the BDD Encoding coding to highlight
additional informations. |
Modifier and Type | Method and Description |
---|---|
void |
BDDView.print(RavenBDD bdd) |
Modifier and Type | Method and Description |
---|---|
void |
TextAreaPrinter.print(RavenBDD bdd) |
void |
DotPrinter.print(RavenBDD bdd) |
void |
ConsolePrinter.print(RavenBDD bdd) |
void |
BDDPrinter.print(RavenBDD bdd)
Prints a BDD to this printer.
|