public class ExecutionBranchCondition extends AbstractExecutionNode<SourceElement> implements IExecutionBranchCondition
IExecutionBranchCondition
.Modifier and Type | Field and Description |
---|---|
private java.lang.String |
additionalBranchLabel
The optional additional branch label.
|
private Term |
branchCondition
The
Term which represents the branch condition. |
private java.lang.String |
formatedBranchCondition
The human readable branch condition.
|
private java.lang.String |
formatedPathCondition
The human readable path condition to reach this node.
|
private Term[] |
mergedBranchCondtions
Contains the merged branch conditions.
|
private java.util.List<Node> |
mergedProofNodes
Merged branch conditions.
|
private Term |
pathCondition
The path condition to reach this node.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionBranchCondition(ITreeSettings settings,
Node proofNode,
java.lang.String additionalBranchLabel)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addMergedProofNode(Node node)
Adds a merged proof
Node . |
SourceElement |
getActiveStatement()
Returns the active statement which is executed in the code.
|
java.lang.String |
getAdditionalBranchLabel()
Returns the optional additional branch label.
|
Term |
getBranchCondition()
Returns the branch condition as
Term . |
java.lang.String |
getElementType()
Returns a human readable element type name.
|
java.lang.String |
getFormatedBranchCondition()
Returns the human readable branch condition as string.
|
java.lang.String |
getFormatedPathCondition()
Returns the human readable path condition to reach this node as string.
|
Term[] |
getMergedBranchCondtions()
Returns the branch condition
Term s. |
Node[] |
getMergedProofNodes()
Returns the branch condition nodes in KeY's proof tree
which are merged into this
IExecutionBranchCondition . |
Term |
getPathCondition()
Returns the path condition to reach this node as
Term . |
boolean |
isBranchConditionComputed()
Checks if the value of
IExecutionBranchCondition.getBranchCondition() is already computed. |
boolean |
isMergedBranchCondition()
Checks if this branch condition is a merged one.
|
boolean |
isPathConditionChanged()
Checks if this node has changed the path condition of the parent.
|
protected void |
lazyComputeBranchCondition()
Computes the branch condition lazily when
getBranchCondition()
or getFormatedBranchCondition() is called the first time. |
protected IExecutionConstraint[] |
lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected Term[] |
lazyComputeMergedBranchCondtions()
Computes the branch condition lazily when
getMergedBranchCondtions()
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. |
protected void |
lazyComputePathCondition()
Computes the path condition lazily when
getPathCondition()
or getFormatedPathCondition() is called the first time. |
addChild, addCompletedBlock, addIncomingLink, addOutgoingLink, getActivePositionInfo, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutExtractor, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getVariables, getVariables, 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, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getVariables, getVariables
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final java.lang.String additionalBranchLabel
private java.lang.String formatedBranchCondition
private Term pathCondition
private java.lang.String formatedPathCondition
private java.util.List<Node> mergedProofNodes
private Term[] mergedBranchCondtions
public ExecutionBranchCondition(ITreeSettings settings, Node proofNode, java.lang.String additionalBranchLabel)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.additionalBranchLabel
- The optional additional branch label.protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.ProofInputException
public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public java.lang.String getFormatedBranchCondition() throws ProofInputException
getFormatedBranchCondition
in interface IExecutionBranchCondition
ProofInputException
public boolean isBranchConditionComputed()
IExecutionBranchCondition.getBranchCondition()
is already computed.isBranchConditionComputed
in interface IExecutionBranchCondition
true
value of IExecutionBranchCondition.getBranchCondition()
is already computed, false
value of IExecutionBranchCondition.getBranchCondition()
needs to be computed.public Term getBranchCondition() throws ProofInputException
Returns the branch condition as Term
.
If this branch conditions merged proof nodes this Term
is the overall branch condition.
getBranchCondition
in interface IExecutionBranchCondition
Term
.ProofInputException
protected void lazyComputeBranchCondition() throws ProofInputException
getBranchCondition()
or getFormatedBranchCondition()
is called the first time.ProofInputException
- Occurred Exceptionpublic boolean isPathConditionChanged()
isPathConditionChanged
in interface IExecutionNode<SourceElement>
isPathConditionChanged
in class AbstractExecutionNode<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<SourceElement>
getPathCondition
in class AbstractExecutionNode<SourceElement>
Term
.ProofInputException
public java.lang.String getFormatedPathCondition() throws ProofInputException
getFormatedPathCondition
in interface IExecutionNode<SourceElement>
getFormatedPathCondition
in class AbstractExecutionNode<SourceElement>
ProofInputException
protected void lazyComputePathCondition() throws ProofInputException
getPathCondition()
or getFormatedPathCondition()
is called the first time.ProofInputException
- Occurred Exceptionpublic void addMergedProofNode(Node node)
Node
.node
- The proof Node
to add.public Node[] getMergedProofNodes()
Returns the branch condition nodes in KeY's proof tree
which are merged into this IExecutionBranchCondition
.
It includes also IExecutionElement.getProofNode()
.
getMergedProofNodes
in interface IExecutionBranchCondition
public Term[] getMergedBranchCondtions() throws ProofInputException
Term
s.getMergedBranchCondtions
in interface IExecutionBranchCondition
Term
s.ProofInputException
protected Term[] lazyComputeMergedBranchCondtions() throws ProofInputException
getMergedBranchCondtions()
is called the first time.ProofInputException
- Occurred Exceptionpublic boolean isMergedBranchCondition()
isMergedBranchCondition
in interface IExecutionBranchCondition
true
is merged branch condition, false
is normal branch condition.public java.lang.String getAdditionalBranchLabel()
getAdditionalBranchLabel
in interface IExecutionBranchCondition
null
if not available.protected IExecutionConstraint[] lazyComputeConstraints()
AbstractExecutionNode.getConstraints()
is
called the first time.lazyComputeConstraints
in class AbstractExecutionNode<SourceElement>
IExecutionConstraint
s of the current state.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>