public static class ExecutionNodeReader.KeYlessLoopCondition extends ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<JavaStatement> implements IExecutionLoopCondition
IExecutionLoopCondition
which is independent
from KeY and provides such only children and default attributes.INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
KeYlessLoopCondition(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean blockOpened)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getElementType()
Returns a human readable element type name.
|
Expression |
getGuardExpression()
Returns the loop expression which is executed.
|
PositionInfo |
getGuardExpressionPositionInfo()
Returns the code position of the executed loop expression (
IExecutionLoopCondition.getGuardExpression() ). |
addBlockCompletion, getBlockCompletions, isBlockOpened
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
getBlockCompletions, isBlockOpened
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 KeYlessLoopCondition(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, boolean blockOpened)
parent
- The parent IExecutionNode
.name
- The name of this node.formatedPathCondition
- The formated path condition.pathConditionChanged
- Is the path condition changed compared to parent?blockOpened
- false
block is definitively not opened, true
block is or might be opened.public Expression getGuardExpression()
getGuardExpression
in interface IExecutionLoopCondition
public PositionInfo getGuardExpressionPositionInfo()
IExecutionLoopCondition.getGuardExpression()
).getGuardExpressionPositionInfo
in interface IExecutionLoopCondition
public java.lang.String getElementType()
getElementType
in interface IExecutionElement