de.uka.ilkd.key.symbolic_execution.model.impl

Class AbstractExecutionBlockStartNode<S extends SourceElement>

java.lang.Object

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionNode<S>

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionBlockStartNode<S>

All Implemented Interfaces:

IExecutionBlockStartNode<S>, IExecutionElement, IExecutionNode<S>

Direct Known Subclasses:

ExecutionBranchStatement, ExecutionLoopCondition, ExecutionLoopStatement

public abstract class AbstractExecutionBlockStartNode<S extends SourceElement>
extends AbstractExecutionNode<S>
implements IExecutionBlockStartNode<S>

Provides a basic implementation of IExecutionBlockStartNode.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableList<IExecutionNode<?>>	blockCompletions The up to know discovered completing IExecutionNodes.
private boolean	blockOpened Defines if a block is or might be opened.

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Constructor Summary

Constructors

Constructor and Description
AbstractExecutionBlockStartNode(ITreeSettings settings, Node proofNode) Constructor.

Method Summary

Modifier and Type	Method and Description
void	addBlockCompletion(IExecutionNode<?> blockCompletion) Registers the given IExecutionNode.
ImmutableList<IExecutionNode<?>>	getBlockCompletions() Returns the up to now discovered IExecutionNodes.
boolean	isBlockOpened() Checks if a block might be opened.
void	removeBlockCompletion(IExecutionNode<?> completion) Removes the given block completion.
void	setBlockOpened(boolean blockOpened) Defines if a block might be opened or not.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionNode

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, lazyComputeConstraints, lazyComputeLayoutExtractor, lazyComputeModalityPIO, lazyComputeVariables, lazyComputeVariables, removeChild, removeCompletedBlock, removeIncomingLink, removeOutgoingLink, setCallStack, setParent

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, lazyComputeName, setName, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

blockCompletions

private ImmutableList<IExecutionNode<?>> blockCompletions

The up to know discovered completing IExecutionNodes.

blockOpened

private boolean blockOpened

Defines if a block is or might be opened.

Constructor Detail

AbstractExecutionBlockStartNode

public AbstractExecutionBlockStartNode(ITreeSettings settings,
                                       Node proofNode)

Constructor.

Parameters:

settings - The ITreeSettings to use.

proofNode - The Node of KeY's proof tree which is represented by this IExecutionNode.

Method Detail

isBlockOpened

public boolean isBlockOpened()

Checks if a block might be opened.

Specified by:

isBlockOpened in interface IExecutionBlockStartNode<S extends SourceElement>

Returns:

false block is definitively not opened, true block is or might be opened.

setBlockOpened

public void setBlockOpened(boolean blockOpened)

Defines if a block might be opened or not.

Parameters:

blockOpened - false block is definitively not opened, true block is or might be opened.

getBlockCompletions

public ImmutableList<IExecutionNode<?>> getBlockCompletions()

Returns the up to now discovered IExecutionNodes.

Specified by:

getBlockCompletions in interface IExecutionBlockStartNode<S extends SourceElement>

Returns:

The up to now discovered IExecutionNodes.

removeBlockCompletion

public void removeBlockCompletion(IExecutionNode<?> completion)

Removes the given block completion.

Parameters:

completion - The block completion to be removed.

addBlockCompletion

public void addBlockCompletion(IExecutionNode<?> blockCompletion)

Registers the given IExecutionNode.

Parameters:

blockCompletion - The IExecutionNode to register.