public class StateBuilder
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static interface |
StateBuilder.StateQueue
Interface used in the execution of en enabled node in the current state.
|
Modifier and Type | Field and Description |
---|---|
protected int |
configurationNumber |
static int |
E
constant indicating the current node is enabled
|
static int |
F
constant indicating the current node is not enabled yet, but will be in
the future
|
static StateBuilder.StateQueue |
MEMORYLESSQUEUE
stateQueue that does not store anything.
|
static int |
N
constant indicating no token is present in the subtree under a node
|
static int |
P
constant indicating the current node is not enabled, but there are
enabled nodes in the subtee.
|
protected StateBuilder.StateQueue |
queue |
static int |
T
constant indicating the current node of type OR is ready to terminate.
|
protected NAryTree |
tree |
protected int |
treeSize |
Constructor and Description |
---|
StateBuilder(NAryTree tree,
int configuationNumber)
initialize the statebuilder.
|
StateBuilder(NAryTree tree,
int configurationNumber,
boolean useQueue)
initialize the statebuilder.
|
Modifier and Type | Method and Description |
---|---|
StateSpace |
buildStateSpace(boolean doPushDown) |
gnu.trove.iterator.TIntIterator |
enabledIterator(byte[] state)
returns an iterator to iterate over the enabled nodes.
|
gnu.trove.iterator.TIntIterator |
enabledIterator(byte[] state,
boolean skipLeafsUnderORIfOREnabled)
returns an iterator to iterate over the enabled nodes.
|
gnu.trove.iterator.TIntIterator |
enabledIterator(byte[] state,
short leafType)
returns an iterator to iterate over the enabled nodes.
|
boolean |
equals(byte[] state,
byte[] state2) |
byte[] |
execute(byte[] state,
int node)
execute the given node .
|
byte[] |
execute(byte[] state,
int node,
StateBuilder.StateQueue queue)
execute the given node.
|
byte[] |
executeAll(byte[] state,
int node)
Executes the given node from the given state while filling the queue and
continues to execute implied nodes until the queue is empty again.
|
protected boolean |
executeAND(int node,
StateBuilder.StateQueue queue,
byte[] newState,
boolean immediateTermination) |
protected boolean |
executeILV(int node,
StateBuilder.StateQueue queue,
byte[] newState,
boolean immediateTermination) |
protected void |
executeLOOP(int node,
StateBuilder.StateQueue queue,
byte[] newState) |
protected void |
executeORTermination(int node,
byte[] newState) |
protected boolean |
executeREVSEQ(int node,
StateBuilder.StateQueue queue,
byte[] newState,
boolean immediateTermination) |
protected boolean |
executeSEQ(int node,
StateBuilder.StateQueue queue,
byte[] newState,
boolean immediateTermination) |
protected void |
executeXORandInitialOR(int node,
StateBuilder.StateQueue queue,
byte[] newState) |
gnu.trove.iterator.TIntIterator |
futureIterator(byte[] state)
returns an iterator to iterate over the nodes that are in future.
|
int |
getConfigurationNumber() |
StateBuilder.StateQueue |
getQueue() |
int |
getState(byte[] state,
int node) |
int |
getStateSizeInBytes()
return the number of bytes needed to store the state for the tree on
which this builder is used.
|
NAryTree |
getTree() |
int |
hashCode(byte[] state) |
byte[] |
initializeState()
initializes an empty state, with the root enabled
|
boolean |
isAllowImplicitOrTermination() |
boolean |
isEnabled(byte[] state,
int node) |
boolean |
isFinal(byte[] state)
returns true if and only if this state is an array of 0's, i.e.
|
boolean |
isPushDownUnderAND() |
static void |
main(java.lang.String[] args) |
protected void |
processChoiceExecution(byte[] state,
NAryTree tree,
int node,
int parent) |
protected void |
processEmptySubtree(byte[] state,
NAryTree tree,
StateBuilder.StateQueue queue,
int p) |
protected void |
processFinishedSubtree(byte[] state,
NAryTree tree,
int node,
StateBuilder.StateQueue queue) |
protected void |
processFinishedSubtreeIlv(byte[] state,
NAryTree tree,
StateBuilder.StateQueue queue,
int p) |
protected void |
processFinishedSubtreeLoop(byte[] state,
NAryTree tree,
int node,
StateBuilder.StateQueue queue,
int p) |
protected void |
processFinishedSubtreeOr(byte[] state,
NAryTree tree,
StateBuilder.StateQueue queue,
int p) |
protected void |
processFinishedSubtreeRevSeq(byte[] state,
NAryTree tree,
int node,
StateBuilder.StateQueue queue,
int p) |
protected void |
processFinishedSubtreeSeq(byte[] state,
NAryTree tree,
int node,
StateBuilder.StateQueue queue,
int p) |
void |
setAllowImplicitOrTermination(boolean allowImplicitOrTermination) |
void |
setPushDownUnderAND(boolean pushDownUnderAND) |
java.lang.String |
toString(byte[] state)
returns a string representation of the state by listing the enabled nodes
first, then the future nodes.
|
public static StateBuilder.StateQueue MEMORYLESSQUEUE
public static final int N
public static final int E
public static final int P
public static final int T
public static final int F
protected final NAryTree tree
protected final StateBuilder.StateQueue queue
protected final int configurationNumber
protected final int treeSize
public StateBuilder(NAryTree tree, int configuationNumber)
tree
- public StateBuilder(NAryTree tree, int configurationNumber, boolean useQueue)
tree
- public StateBuilder.StateQueue getQueue()
public NAryTree getTree()
public int getConfigurationNumber()
public int getStateSizeInBytes()
public byte[] initializeState()
numNodes
- public boolean isEnabled(byte[] state, int node)
public int getState(byte[] state, int node)
public boolean equals(byte[] state, byte[] state2)
public int hashCode(byte[] state)
public byte[] execute(byte[] state, int node)
node
- public byte[] execute(byte[] state, int node, StateBuilder.StateQueue queue)
// initialize a queue. This necessary only once for the entire tree.
StateQueue queue = builder.getQueue();
// current is the current state.
byte[] current;
// add the node that needs execution to the queue
queue.add(node);
// set the next state to be the current one
byte[] next = current;
while (!queue.isEmpty()) {
// continue while the queue is not empty
// and overwrite next with the state obtained from
// executing the next element from the queue.
next = execute(next, queue.poll(), queue);
}
failing to properly empty the queue using the code above may lead to
unexpected results as the queue has a maximum capacity equal to the
number of leafs and if full it will "overflow" without warningstate
- the current statenode
- the node that has to execute. This node should be enabled in
the current state.queue
- a queue for storing implicit nodes.protected void executeORTermination(int node, byte[] newState)
protected void executeXORandInitialOR(int node, StateBuilder.StateQueue queue, byte[] newState)
protected void executeLOOP(int node, StateBuilder.StateQueue queue, byte[] newState)
protected boolean executeSEQ(int node, StateBuilder.StateQueue queue, byte[] newState, boolean immediateTermination)
protected boolean executeREVSEQ(int node, StateBuilder.StateQueue queue, byte[] newState, boolean immediateTermination)
protected boolean executeAND(int node, StateBuilder.StateQueue queue, byte[] newState, boolean immediateTermination)
protected boolean executeILV(int node, StateBuilder.StateQueue queue, byte[] newState, boolean immediateTermination)
public byte[] executeAll(byte[] state, int node)
state
- node
- queue
- protected void processChoiceExecution(byte[] state, NAryTree tree, int node, int parent)
protected void processFinishedSubtree(byte[] state, NAryTree tree, int node, StateBuilder.StateQueue queue)
protected void processEmptySubtree(byte[] state, NAryTree tree, StateBuilder.StateQueue queue, int p)
protected void processFinishedSubtreeOr(byte[] state, NAryTree tree, StateBuilder.StateQueue queue, int p)
protected void processFinishedSubtreeIlv(byte[] state, NAryTree tree, StateBuilder.StateQueue queue, int p)
protected void processFinishedSubtreeLoop(byte[] state, NAryTree tree, int node, StateBuilder.StateQueue queue, int p)
protected void processFinishedSubtreeSeq(byte[] state, NAryTree tree, int node, StateBuilder.StateQueue queue, int p)
protected void processFinishedSubtreeRevSeq(byte[] state, NAryTree tree, int node, StateBuilder.StateQueue queue, int p)
public boolean isFinal(byte[] state)
state
- public gnu.trove.iterator.TIntIterator enabledIterator(byte[] state)
public gnu.trove.iterator.TIntIterator enabledIterator(byte[] state, boolean skipLeafsUnderORIfOREnabled)
public gnu.trove.iterator.TIntIterator enabledIterator(byte[] state, short leafType)
public gnu.trove.iterator.TIntIterator futureIterator(byte[] state)
public java.lang.String toString(byte[] state)
state
- public StateSpace buildStateSpace(boolean doPushDown)
public static void main(java.lang.String[] args) throws java.io.FileNotFoundException
java.io.FileNotFoundException
public void setPushDownUnderAND(boolean pushDownUnderAND)
public boolean isPushDownUnderAND()
public void setAllowImplicitOrTermination(boolean allowImplicitOrTermination)
public boolean isAllowImplicitOrTermination()