public abstract class AbstractExecutionNode<S extends SourceElement> extends AbstractExecutionElement implements IExecutionNode<S>
IExecutionNode
.Modifier and Type | Field and Description |
---|---|
private java.util.Map<IExecutionBlockStartNode<?>,Term> |
blockCompletionConditions
The already computed block completion conditions.
|
private IExecutionNode<?>[] |
callStack
The contained call stack.
|
private java.util.List<IExecutionNode<?>> |
children
Contains all child
IExecutionNode s. |
private ImmutableList<IExecutionBlockStartNode<?>> |
completedBlocks
The up to know discovered completed
IExecutionBlockStartNode s. |
private java.util.Map<Term,IExecutionVariable[]> |
conditionalVariables
The variable value pairs of the current state under given conditions.
|
private IExecutionConstraint[] |
constraints
The available
IExecutionConstraint s. |
private java.util.Map<IExecutionBlockStartNode<?>,java.lang.String> |
formatedBlockCompletionConditions
The already computed human readable block completion conditions.
|
private ImmutableList<IExecutionLink> |
incomingLinks
The up to know discovered incoming links.
|
private ExecutionNodeSymbolicLayoutExtractor |
layoutExtractor
The used
ExecutionNodeSymbolicLayoutExtractor . |
private PosInOccurrence |
modalityPIO
The
PosInOccurrence of the modality or its updates. |
private ImmutableList<IExecutionLink> |
outgoingLinks
The up to know discovered outgoing links.
|
private AbstractExecutionNode<?> |
parent
Reference to the parent
IExecutionNode . |
private IExecutionVariable[] |
variables
The variable value pairs of the current state.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
AbstractExecutionNode(ITreeSettings settings,
Node proofNode)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addChild(AbstractExecutionNode<?> child)
Adds a new child
AbstractExecutionNode . |
void |
addCompletedBlock(IExecutionBlockStartNode<?> completedBlock)
Registers the given
IExecutionBlockStartNode . |
void |
addIncomingLink(IExecutionLink link)
Adds the given
IExecutionLink as incoming link. |
void |
addOutgoingLink(IExecutionLink link)
Adds the given
IExecutionLink as outgoing link. |
PositionInfo |
getActivePositionInfo()
Returns the
PositionInfo of IExecutionNode.getActiveStatement() . |
S |
getActiveStatement()
Returns the active statement which is executed in the code.
|
Term |
getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
IExecutionNode<?>[] |
getCallStack()
Returns the method call stack.
|
AbstractExecutionNode<?>[] |
getChildren()
Returns the available children.
|
ImmutableList<IExecutionBlockStartNode<?>> |
getCompletedBlocks()
Returns all code blocks completed by this
IExecutionBlockStartNode . |
IExecutionConstraint[] |
getConstraints()
Returns all available
IExecutionConstraint s. |
ISymbolicLayout |
getCurrentLayout(int layoutIndex)
Returns the current memory layout which shows the memory
structure before the current node in the symbolic execution tree is executed.
|
java.lang.String |
getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the human readable condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
java.lang.String |
getFormatedPathCondition()
Returns the human readable path condition to reach this node as string.
|
IExecutionLink |
getIncomingLink(IExecutionNode<?> source)
Returns the incoming
IExecutionLink . |
ImmutableList<IExecutionLink> |
getIncomingLinks()
Returns all available incoming links.
|
ISymbolicLayout |
getInitialLayout(int layoutIndex)
Returns the initial memory layout before the method was executed.
|
ExecutionNodeSymbolicLayoutExtractor |
getLayoutExtractor()
Returns the used
ExecutionNodeSymbolicLayoutExtractor . |
int |
getLayoutsCount()
Returns the number of memory layouts.
|
ImmutableList<ISymbolicEquivalenceClass> |
getLayoutsEquivalenceClasses(int layoutIndex)
Returns the equivalence classes of the memory layout with the given index.
|
PosInOccurrence |
getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
IExecutionLink |
getOutgoingLink(IExecutionNode<?> target)
Returns the outgoing
IExecutionLink . |
ImmutableList<IExecutionLink> |
getOutgoingLinks()
Returns all available outgoing links.
|
AbstractExecutionNode<?> |
getParent()
Returns the parent
IExecutionNode or null if the
current node is the root. |
Term |
getPathCondition()
Returns the path condition to reach this node as
Term . |
IExecutionVariable[] |
getVariables()
Returns the variable value pairs of the current state.
|
IExecutionVariable[] |
getVariables(Term condition)
Returns the variable value pairs of the current state under the given condition.
|
boolean |
isPathConditionChanged()
Checks if this node has changed the path condition of the parent.
|
protected java.lang.Object |
lazyComputeBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode,
boolean returnFormatedCondition)
Computes the condition lazily when
#getBlockCompletionCondition(IExecutionNode)
or #getFormatedBlockCompletionCondition(IExecutionNode) is called the first time. |
protected abstract IExecutionConstraint[] |
lazyComputeConstraints()
Computes the constraints lazily when
getConstraints() is
called the first time. |
protected ExecutionNodeSymbolicLayoutExtractor |
lazyComputeLayoutExtractor()
Instantiates the used
ExecutionNodeSymbolicLayoutExtractor lazily
when getLayoutExtractor() is called the first time. |
protected PosInOccurrence |
lazyComputeModalityPIO()
Computes the
PosInOccurrence lazily when getModalityPIO() is
called the first time. |
protected IExecutionVariable[] |
lazyComputeVariables()
Computes the variables lazily when
getVariables() is
called the first time. |
protected IExecutionVariable[] |
lazyComputeVariables(Term condition)
Computes the variables lazily when
getVariables(Term) is
called the first time. |
void |
removeChild(IExecutionNode<?> child)
Removes the given child.
|
void |
removeCompletedBlock(IExecutionBlockStartNode<?> completedBlock)
Removes the given
IExecutionBlockStartNode from registration. |
void |
removeIncomingLink(IExecutionLink link)
Removes the given
IExecutionLink from the incoming links. |
void |
removeOutgoingLink(IExecutionLink link)
Removes the given
IExecutionLink from the outgoing links. |
void |
setCallStack(IExecutionNode<?>[] callStack)
Sets the call stack.
|
void |
setParent(AbstractExecutionNode<?> parent)
Sets the parent
AbstractExecutionNode . |
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, lazyComputeName, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getAppliedRuleApp, getElementType, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private AbstractExecutionNode<?> parent
IExecutionNode
.private final java.util.List<IExecutionNode<?>> children
IExecutionNode
s.private IExecutionNode<?>[] callStack
private IExecutionConstraint[] constraints
IExecutionConstraint
s.private IExecutionVariable[] variables
private final java.util.Map<Term,IExecutionVariable[]> conditionalVariables
private ExecutionNodeSymbolicLayoutExtractor layoutExtractor
ExecutionNodeSymbolicLayoutExtractor
.private PosInOccurrence modalityPIO
PosInOccurrence
of the modality or its updates.private ImmutableList<IExecutionBlockStartNode<?>> completedBlocks
IExecutionBlockStartNode
s.private final java.util.Map<IExecutionBlockStartNode<?>,Term> blockCompletionConditions
private final java.util.Map<IExecutionBlockStartNode<?>,java.lang.String> formatedBlockCompletionConditions
private ImmutableList<IExecutionLink> outgoingLinks
private ImmutableList<IExecutionLink> incomingLinks
public AbstractExecutionNode(ITreeSettings settings, Node proofNode)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.public AbstractExecutionNode<?> getParent()
IExecutionNode
or null
if the
current node is the root.getParent
in interface IExecutionNode<S extends SourceElement>
IExecutionNode
or null
on root.public void setParent(AbstractExecutionNode<?> parent)
AbstractExecutionNode
.parent
- The parent AbstractExecutionNode
to set.public AbstractExecutionNode<?>[] getChildren()
getChildren
in interface IExecutionNode<S extends SourceElement>
public void addChild(AbstractExecutionNode<?> child)
AbstractExecutionNode
.child
- A new child AbstractExecutionNode
.public boolean isPathConditionChanged()
isPathConditionChanged
in interface IExecutionNode<S extends SourceElement>
true
has different path condition compared to its parent, false
has same path condition as parent.public Term getPathCondition() throws ProofInputException
Term
.getPathCondition
in interface IExecutionNode<S extends SourceElement>
Term
.ProofInputException
public java.lang.String getFormatedPathCondition() throws ProofInputException
getFormatedPathCondition
in interface IExecutionNode<S extends SourceElement>
ProofInputException
public IExecutionNode<?>[] getCallStack()
getCallStack
in interface IExecutionNode<S extends SourceElement>
public void setCallStack(IExecutionNode<?>[] callStack)
callStack
- The call stack.public IExecutionConstraint[] getConstraints()
IExecutionConstraint
s.getConstraints
in interface IExecutionNode<S extends SourceElement>
IExecutionConstraint
s.protected abstract IExecutionConstraint[] lazyComputeConstraints()
getConstraints()
is
called the first time.IExecutionConstraint
s of the current state.public S getActiveStatement()
getActiveStatement
in interface IExecutionNode<S extends SourceElement>
public PositionInfo getActivePositionInfo()
PositionInfo
of IExecutionNode.getActiveStatement()
.getActivePositionInfo
in interface IExecutionNode<S extends SourceElement>
PositionInfo
of IExecutionNode.getActiveStatement()
.public IExecutionVariable[] getVariables() throws ProofInputException
getVariables
in interface IExecutionNode<S extends SourceElement>
ProofInputException
- Occurred Exception.protected IExecutionVariable[] lazyComputeVariables() throws ProofInputException
getVariables()
is
called the first time.IExecutionVariable
s of the current state.ProofInputException
public IExecutionVariable[] getVariables(Term condition) throws ProofInputException
getVariables
in interface IExecutionNode<S extends SourceElement>
condition
- A Term
specifying some additional constraints to consider.ProofInputException
protected IExecutionVariable[] lazyComputeVariables(Term condition) throws ProofInputException
getVariables(Term)
is
called the first time.condition
- A Term
specifying some additional constraints to consider.IExecutionVariable
s of the current state under the given condition.ProofInputException
public ExecutionNodeSymbolicLayoutExtractor getLayoutExtractor() throws ProofInputException
ExecutionNodeSymbolicLayoutExtractor
.ExecutionNodeSymbolicLayoutExtractor
.ProofInputException
- Occurred Exception.protected ExecutionNodeSymbolicLayoutExtractor lazyComputeLayoutExtractor() throws ProofInputException
ExecutionNodeSymbolicLayoutExtractor
lazily
when getLayoutExtractor()
is called the first time.ExecutionNodeSymbolicLayoutExtractor
.ProofInputException
- Occurred Exception.public int getLayoutsCount() throws ProofInputException
getLayoutsCount
in interface IExecutionNode<S extends SourceElement>
ProofInputException
- Occurred Exception.public ISymbolicLayout getInitialLayout(int layoutIndex) throws ProofInputException
getInitialLayout
in interface IExecutionNode<S extends SourceElement>
layoutIndex
- The index of the memory layout.ProofInputException
- Occurred Exception.public ISymbolicLayout getCurrentLayout(int layoutIndex) throws ProofInputException
getCurrentLayout
in interface IExecutionNode<S extends SourceElement>
layoutIndex
- The index of the memory layout.ProofInputException
- Occurred Exception.public ImmutableList<ISymbolicEquivalenceClass> getLayoutsEquivalenceClasses(int layoutIndex) throws ProofInputException
getLayoutsEquivalenceClasses
in interface IExecutionNode<S extends SourceElement>
layoutIndex
- The index of the memory layout.ProofInputException
- Occurred Exception.public PosInOccurrence getModalityPIO()
PosInOccurrence
of the modality of interest including updates.getModalityPIO
in interface IExecutionElement
PosInOccurrence
of the modality of interest including updates.protected PosInOccurrence lazyComputeModalityPIO()
PosInOccurrence
lazily when getModalityPIO()
is
called the first time.PosInOccurrence
s of the modality or its updates.public ImmutableList<IExecutionBlockStartNode<?>> getCompletedBlocks()
IExecutionBlockStartNode
.getCompletedBlocks
in interface IExecutionNode<S extends SourceElement>
IExecutionBlockStartNode
.public void addCompletedBlock(IExecutionBlockStartNode<?> completedBlock)
IExecutionBlockStartNode
.completedBlock
- The IExecutionBlockStartNode
to register.public void removeCompletedBlock(IExecutionBlockStartNode<?> completedBlock)
IExecutionBlockStartNode
from registration.completedBlock
- The IExecutionBlockStartNode
to be remove.public Term getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode) throws ProofInputException
IExecutionBlockStartNode
.getBlockCompletionCondition
in interface IExecutionNode<S extends SourceElement>
completedNode
- The completed IExecutionBlockStartNode
for which the condition is requested.IExecutionBlockStartNode
.ProofInputException
public java.lang.String getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode) throws ProofInputException
IExecutionBlockStartNode
.getFormatedBlockCompletionCondition
in interface IExecutionNode<S extends SourceElement>
completedNode
- The completed IExecutionBlockStartNode
for which the condition is requested.IExecutionBlockStartNode
.ProofInputException
protected java.lang.Object lazyComputeBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode, boolean returnFormatedCondition) throws ProofInputException
#getBlockCompletionCondition(IExecutionNode)
or #getFormatedBlockCompletionCondition(IExecutionNode)
is called the first time.completedNode
- The completed IExecutionNode
for which the condition is requested.returnFormatedCondition
- true
formated condition is returned, false
Term
is returned.ProofInputException
- Occurred Exceptionpublic void removeChild(IExecutionNode<?> child)
child
- The child to be removed.public void addOutgoingLink(IExecutionLink link)
IExecutionLink
as outgoing link.link
- The IExecutionLink
to add.public void removeOutgoingLink(IExecutionLink link)
IExecutionLink
from the outgoing links.link
- The IExecutionLink
to remove.public IExecutionLink getOutgoingLink(IExecutionNode<?> target)
IExecutionLink
.getOutgoingLink
in interface IExecutionNode<S extends SourceElement>
target
- The target IExecutionNode
.IExecutionLink
or null
if such a link is not available.public ImmutableList<IExecutionLink> getOutgoingLinks()
getOutgoingLinks
in interface IExecutionNode<S extends SourceElement>
public IExecutionLink getIncomingLink(IExecutionNode<?> source)
IExecutionLink
.getIncomingLink
in interface IExecutionNode<S extends SourceElement>
source
- The source IExecutionNode
.IExecutionLink
or null
if such a link is not available.public void addIncomingLink(IExecutionLink link)
IExecutionLink
as incoming link.link
- The IExecutionLink
to add.public void removeIncomingLink(IExecutionLink link)
IExecutionLink
from the incoming links.link
- The IExecutionLink
to remove.public ImmutableList<IExecutionLink> getIncomingLinks()
getIncomingLinks
in interface IExecutionNode<S extends SourceElement>