public class ExecutionStart extends AbstractExecutionNode<SourceElement> implements IExecutionStart
IExecutionStart
.Modifier and Type | Field and Description |
---|---|
private ImmutableList<IExecutionTermination> |
terminations
The up to know discovered
IExecutionTermination s. |
DEFAULT_START_NODE_NAME
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionStart(ITreeSettings settings,
Node proofNode)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addTermination(IExecutionTermination termination)
Registers the given
IExecutionTermination . |
SourceElement |
getActiveStatement()
Returns the active statement which is executed in the code.
|
java.lang.String |
getElementType()
Returns a human readable element type name.
|
ImmutableList<IExecutionTermination> |
getTerminations()
Returns the up to now discovered
IExecutionTermination s. |
protected IExecutionConstraint[] |
lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected PosInOccurrence |
lazyComputeModalityPIO()
Computes the
PosInOccurrence lazily when AbstractExecutionNode.getModalityPIO() is
called the first time. |
protected java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
void |
removeTermination(IExecutionTermination termination)
Removes the given termination.
|
addChild, addCompletedBlock, addIncomingLink, addOutgoingLink, getActivePositionInfo, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutExtractor, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged, lazyComputeBlockCompletionCondition, lazyComputeLayoutExtractor, lazyComputeVariables, lazyComputeVariables, removeChild, removeCompletedBlock, removeIncomingLink, removeOutgoingLink, setCallStack, setParent
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getActivePositionInfo, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private ImmutableList<IExecutionTermination> terminations
IExecutionTermination
s.public ExecutionStart(ITreeSettings settings, Node proofNode)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.protected java.lang.String lazyComputeName()
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.protected IExecutionConstraint[] lazyComputeConstraints()
AbstractExecutionNode.getConstraints()
is
called the first time.lazyComputeConstraints
in class AbstractExecutionNode<SourceElement>
IExecutionConstraint
s of the current state.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public ImmutableList<IExecutionTermination> getTerminations()
IExecutionTermination
s.getTerminations
in interface IExecutionStart
IExecutionTermination
s.public void addTermination(IExecutionTermination termination)
IExecutionTermination
.termination
- The IExecutionTermination
to register.protected PosInOccurrence lazyComputeModalityPIO()
PosInOccurrence
lazily when AbstractExecutionNode.getModalityPIO()
is
called the first time.lazyComputeModalityPIO
in class AbstractExecutionNode<SourceElement>
PosInOccurrence
s of the modality or its updates.public SourceElement getActiveStatement()
getActiveStatement
in interface IExecutionNode<SourceElement>
getActiveStatement
in class AbstractExecutionNode<SourceElement>
public void removeTermination(IExecutionTermination termination)
termination
- The termination to be deleted.