public class ExecutionJoin extends AbstractExecutionNode<SourceElement> implements IExecutionJoin
IExecutionJoin
.INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionJoin(ITreeSettings settings,
Node proofNode)
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.
|
protected IExecutionConstraint[] |
lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() 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. |
addChild, addCompletedBlock, addIncomingLink, addOutgoingLink, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutExtractor, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged, lazyComputeBlockCompletionCondition, lazyComputeLayoutExtractor, lazyComputeModalityPIO, 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, 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 ExecutionJoin(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 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.