public abstract class AbstractExecutionBlockStartNode<S extends SourceElement> extends AbstractExecutionNode<S> implements IExecutionBlockStartNode<S>
IExecutionBlockStartNode
.Modifier and Type | Field and Description |
---|---|
private ImmutableList<IExecutionNode<?>> |
blockCompletions
The up to know discovered completing
IExecutionNode s. |
private boolean |
blockOpened
Defines if a block is or might be opened.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
AbstractExecutionBlockStartNode(ITreeSettings settings,
Node proofNode)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addBlockCompletion(IExecutionNode<?> blockCompletion)
Registers the given
IExecutionNode . |
ImmutableList<IExecutionNode<?>> |
getBlockCompletions()
Returns the up to now discovered
IExecutionNode s. |
boolean |
isBlockOpened()
Checks if a block might be opened.
|
void |
removeBlockCompletion(IExecutionNode<?> completion)
Removes the given block completion.
|
void |
setBlockOpened(boolean blockOpened)
Defines if a block might be opened or not.
|
addChild, addCompletedBlock, addIncomingLink, addOutgoingLink, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutExtractor, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged, lazyComputeBlockCompletionCondition, lazyComputeConstraints, lazyComputeLayoutExtractor, lazyComputeModalityPIO, lazyComputeVariables, lazyComputeVariables, removeChild, removeCompletedBlock, removeIncomingLink, removeOutgoingLink, setCallStack, setParent
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, lazyComputeName, setName, 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
IExecutionNode
s.private boolean blockOpened
public AbstractExecutionBlockStartNode(ITreeSettings settings, Node proofNode)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.public boolean isBlockOpened()
isBlockOpened
in interface IExecutionBlockStartNode<S extends SourceElement>
false
block is definitively not opened, true
block is or might be opened.public void setBlockOpened(boolean blockOpened)
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 removeBlockCompletion(IExecutionNode<?> completion)
completion
- The block completion to be removed.public void addBlockCompletion(IExecutionNode<?> blockCompletion)
IExecutionNode
.blockCompletion
- The IExecutionNode
to register.