public static class ExecutionNodeReader.KeYlessBranchCondition extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement> implements IExecutionBranchCondition
IExecutionLoopCondition
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private java.lang.String |
additionalBranchLabel
The optional additional branch label.
|
private boolean |
branchConditionComputed
Indicates if branch condition is computed or not.
|
private java.lang.String |
formatedBranchCondition
The formated branch condition.
|
private boolean |
mergedBranchCondition
Merged branch condition?
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
KeYlessBranchCondition(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
java.lang.String formatedBranchCondition,
boolean mergedBranchCondition,
boolean branchConditionComputed,
java.lang.String additionalBranchLabel)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
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.
|
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 . |
boolean |
isBranchConditionComputed()
Checks if the value of
IExecutionBranchCondition.getBranchCondition() is already computed. |
boolean |
isMergedBranchCondition()
Checks if this branch condition is a merged one.
|
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, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final java.lang.String formatedBranchCondition
private final boolean mergedBranchCondition
private final boolean branchConditionComputed
private final java.lang.String additionalBranchLabel
public KeYlessBranchCondition(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, java.lang.String formatedBranchCondition, boolean mergedBranchCondition, boolean branchConditionComputed, java.lang.String additionalBranchLabel)
parent
- The parent IExecutionNode
.name
- The name of this node.formatedPathCondition
- The formated path condition.pathConditionChanged
- Is the path condition changed compared to parent?formatedBranchCondition
- The formated branch condition.mergedBranchCondition
- Merged branch condition?branchConditionComputed
- Is branch condition computed?additionalBranchLabel
- The optional additional branch label.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public Term getBranchCondition()
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
.public java.lang.String getFormatedBranchCondition()
getFormatedBranchCondition
in interface IExecutionBranchCondition
public boolean isMergedBranchCondition()
isMergedBranchCondition
in interface IExecutionBranchCondition
true
is merged branch condition, false
is normal branch condition.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
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 java.lang.String getAdditionalBranchLabel()
getAdditionalBranchLabel
in interface IExecutionBranchCondition
null
if not available.