public abstract static class ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<S extends SourceElement> extends ExecutionNodeReader.AbstractKeYlessExecutionNode<S> implements IExecutionBlockStartNode<S>
IExecutionBlockStartNode
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private ImmutableList<IExecutionNode<?>> |
blockCompletions
The block completions.
|
private boolean |
blockOpened
Is a block opened?
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
AbstractKeYlessExecutionBlockStartNode(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean blockOpened)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addBlockCompletion(IExecutionNode<?> blockCompletion)
Adds the given block completion.
|
ImmutableList<IExecutionNode<?>> |
getBlockCompletions()
Returns the up to now discovered
IExecutionNode s. |
boolean |
isBlockOpened()
Checks if a block might be opened.
|
addCallStackEntry, addChild, addCompletedBlock, addConstraint, addIncomingLink, addOutgoingLink, addVariable, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private ImmutableList<IExecutionNode<?>> blockCompletions
private final boolean blockOpened
public AbstractKeYlessExecutionBlockStartNode(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, boolean blockOpened)
parent
- The parent IExecutionNode
.name
- The name of this node.formatedPathCondition
- The formated path condition.pathConditionChanged
- Is the path condition changed compared to parent?blockOpened
- false
block is definitively not opened, true
block is or might be opened.public ImmutableList<IExecutionNode<?>> getBlockCompletions()
IExecutionNode
s.getBlockCompletions
in interface IExecutionBlockStartNode<S extends SourceElement>
IExecutionNode
s.public void addBlockCompletion(IExecutionNode<?> blockCompletion)
blockCompletion
- The block completion to add.public boolean isBlockOpened()
isBlockOpened
in interface IExecutionBlockStartNode<S extends SourceElement>
false
block is definitively not opened, true
block is or might be opened.