public static class ExecutionNodeReader.KeYlessJoin extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement> implements IExecutionJoin
IExecutionJoin
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private boolean |
weakeningVerified
Is the weakening verified?
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
KeYlessJoin(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean weakeningVerified)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getElementType()
Returns a human readable element type name.
|
boolean |
isWeakeningVerificationSupported()
Checks if the weakening verification is supported.
|
boolean |
isWeakeningVerified()
Checks if the weakening is verified.
|
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
public KeYlessJoin(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, boolean weakeningVerified)
parent
- The parent IExecutionNode
.name
- The name of this node.pathConditionChanged
- Is the path condition changed compared to parent?formatedPathCondition
- The formated path condition.weakeningVerified
- Is the weakening verified?public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public boolean isWeakeningVerified()
isWeakeningVerified
in interface IExecutionJoin
true
is verified, false
is not verified.public boolean isWeakeningVerificationSupported()
isWeakeningVerificationSupported
in interface IExecutionJoin
true
supported, false
not supported.