AbstractExecutionNode (KeY API Documentation)

java.lang.Object
- de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement
- - de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionNode<S>

All Implemented Interfaces:

IExecutionElement, IExecutionNode<S>

Direct Known Subclasses:

AbstractExecutionBlockStartNode, AbstractExecutionMethodReturn, ExecutionAuxiliaryContract, ExecutionBranchCondition, ExecutionJoin, ExecutionLoopInvariant, ExecutionMethodCall, ExecutionOperationContract, ExecutionStart, ExecutionStatement, ExecutionTermination
```
public abstract class AbstractExecutionNode<S extends SourceElement>
extends AbstractExecutionElement
implements IExecutionNode<S>
```
Provides a basic implementation of IExecutionNode.

Author:

Martin Hentschel

Field Summary

Fields
Modifier and Type	Field and Description
`private java.util.Map<IExecutionBlockStartNode<?>,Term>`	`blockCompletionConditions` The already computed block completion conditions.
`private IExecutionNode<?>[]`	`callStack` The contained call stack.
`private java.util.List<IExecutionNode<?>>`	`children` Contains all child `IExecutionNode`s.
`private ImmutableList<IExecutionBlockStartNode<?>>`	`completedBlocks` The up to know discovered completed `IExecutionBlockStartNode`s.
`private java.util.Map<Term,IExecutionVariable[]>`	`conditionalVariables` The variable value pairs of the current state under given conditions.
`private IExecutionConstraint[]`	`constraints` The available `IExecutionConstraint`s.
`private java.util.Map<IExecutionBlockStartNode<?>,java.lang.String>`	`formatedBlockCompletionConditions` The already computed human readable block completion conditions.
`private ImmutableList<IExecutionLink>`	`incomingLinks` The up to know discovered incoming links.
`private ExecutionNodeSymbolicLayoutExtractor`	`layoutExtractor` The used `ExecutionNodeSymbolicLayoutExtractor`.
`private PosInOccurrence`	`modalityPIO` The `PosInOccurrence` of the modality or its updates.
`private ImmutableList<IExecutionLink>`	`outgoingLinks` The up to know discovered outgoing links.
`private AbstractExecutionNode<?>`	`parent` Reference to the parent `IExecutionNode`.
`private IExecutionVariable[]`	`variables` The variable value pairs of the current state.

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

AbstractExecutionNode(ITreeSettings settings, Node proofNode)
Constructor.

Constructors
Constructor and Description
`AbstractExecutionNode(ITreeSettings settings, Node proofNode)` Constructor.

Method Summary

All Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method and Description
`void`	`addChild(AbstractExecutionNode<?> child)` Adds a new child `AbstractExecutionNode`.
`void`	`addCompletedBlock(IExecutionBlockStartNode<?> completedBlock)` Registers the given `IExecutionBlockStartNode`.
`void`	`addIncomingLink(IExecutionLink link)` Adds the given `IExecutionLink` as incoming link.
`void`	`addOutgoingLink(IExecutionLink link)` Adds the given `IExecutionLink` as outgoing link.
`PositionInfo`	`getActivePositionInfo()` Returns the `PositionInfo` of `IExecutionNode.getActiveStatement()`.
`S`	`getActiveStatement()` Returns the active statement which is executed in the code.
`Term`	`getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)` Returns the condition under which this node completes the code block of the given `IExecutionBlockStartNode`.
`IExecutionNode<?>[]`	`getCallStack()` Returns the method call stack.
`AbstractExecutionNode<?>[]`	`getChildren()` Returns the available children.
`ImmutableList<IExecutionBlockStartNode<?>>`	`getCompletedBlocks()` Returns all code blocks completed by this `IExecutionBlockStartNode`.
`IExecutionConstraint[]`	`getConstraints()` Returns all available `IExecutionConstraint`s.
`ISymbolicLayout`	`getCurrentLayout(int layoutIndex)` Returns the current memory layout which shows the memory structure before the current node in the symbolic execution tree is executed.
`java.lang.String`	`getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)` Returns the human readable condition under which this node completes the code block of the given `IExecutionBlockStartNode`.
`java.lang.String`	`getFormatedPathCondition()` Returns the human readable path condition to reach this node as string.
`IExecutionLink`	`getIncomingLink(IExecutionNode<?> source)` Returns the incoming `IExecutionLink`.
`ImmutableList<IExecutionLink>`	`getIncomingLinks()` Returns all available incoming links.
`ISymbolicLayout`	`getInitialLayout(int layoutIndex)` Returns the initial memory layout before the method was executed.
`ExecutionNodeSymbolicLayoutExtractor`	`getLayoutExtractor()` Returns the used `ExecutionNodeSymbolicLayoutExtractor`.
`int`	`getLayoutsCount()` Returns the number of memory layouts.
`ImmutableList<ISymbolicEquivalenceClass>`	`getLayoutsEquivalenceClasses(int layoutIndex)` Returns the equivalence classes of the memory layout with the given index.
`PosInOccurrence`	`getModalityPIO()` Returns the `PosInOccurrence` of the modality of interest including updates.
`IExecutionLink`	`getOutgoingLink(IExecutionNode<?> target)` Returns the outgoing `IExecutionLink`.
`ImmutableList<IExecutionLink>`	`getOutgoingLinks()` Returns all available outgoing links.
`AbstractExecutionNode<?>`	`getParent()` Returns the parent `IExecutionNode` or `null` if the current node is the root.
`Term`	`getPathCondition()` Returns the path condition to reach this node as `Term`.
`IExecutionVariable[]`	`getVariables()` Returns the variable value pairs of the current state.
`IExecutionVariable[]`	`getVariables(Term condition)` Returns the variable value pairs of the current state under the given condition.
`boolean`	`isPathConditionChanged()` Checks if this node has changed the path condition of the parent.
`protected java.lang.Object`	`lazyComputeBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode, boolean returnFormatedCondition)` Computes the condition lazily when `#getBlockCompletionCondition(IExecutionNode)` or `#getFormatedBlockCompletionCondition(IExecutionNode)` is called the first time.
`protected abstract IExecutionConstraint[]`	`lazyComputeConstraints()` Computes the constraints lazily when `getConstraints()` is called the first time.
`protected ExecutionNodeSymbolicLayoutExtractor`	`lazyComputeLayoutExtractor()` Instantiates the used `ExecutionNodeSymbolicLayoutExtractor` lazily when `getLayoutExtractor()` is called the first time.
`protected PosInOccurrence`	`lazyComputeModalityPIO()` Computes the `PosInOccurrence` lazily when `getModalityPIO()` is called the first time.
`protected IExecutionVariable[]`	`lazyComputeVariables()` Computes the variables lazily when `getVariables()` is called the first time.
`protected IExecutionVariable[]`	`lazyComputeVariables(Term condition)` Computes the variables lazily when `getVariables(Term)` is called the first time.
`void`	`removeChild(IExecutionNode<?> child)` Removes the given child.
`void`	`removeCompletedBlock(IExecutionBlockStartNode<?> completedBlock)` Removes the given `IExecutionBlockStartNode` from registration.
`void`	`removeIncomingLink(IExecutionLink link)` Removes the given `IExecutionLink` from the incoming links.
`void`	`removeOutgoingLink(IExecutionLink link)` Removes the given `IExecutionLink` from the outgoing links.
`void`	`setCallStack(IExecutionNode<?>[] callStack)` Sets the call stack.
`void`	`setParent(AbstractExecutionNode<?> parent)` Sets the parent `AbstractExecutionNode`.

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.IExecutionElement
getAppliedRuleApp, getElementType, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

- Field Detail
  - parent
```
private AbstractExecutionNode<?> parent
```
    Reference to the parent IExecutionNode.
  - children
```
private final java.util.List<IExecutionNode<?>> children
```
    Contains all child IExecutionNodes.
  - callStack
```
private IExecutionNode<?>[] callStack
```
    The contained call stack.
  - constraints
```
private IExecutionConstraint[] constraints
```
    The available IExecutionConstraints.
  - variables
```
private IExecutionVariable[] variables
```
    The variable value pairs of the current state.
  - conditionalVariables
```
private final java.util.Map<Term,IExecutionVariable[]> conditionalVariables
```
    The variable value pairs of the current state under given conditions.
  - layoutExtractor
```
private ExecutionNodeSymbolicLayoutExtractor layoutExtractor
```
    The used ExecutionNodeSymbolicLayoutExtractor.
  - modalityPIO
```
private PosInOccurrence modalityPIO
```
    The PosInOccurrence of the modality or its updates.
  - completedBlocks
```
private ImmutableList<IExecutionBlockStartNode<?>> completedBlocks
```
    The up to know discovered completed IExecutionBlockStartNodes.
  - blockCompletionConditions
```
private final java.util.Map<IExecutionBlockStartNode<?>,Term> blockCompletionConditions
```
    The already computed block completion conditions.
  - formatedBlockCompletionConditions
```
private final java.util.Map<IExecutionBlockStartNode<?>,java.lang.String> formatedBlockCompletionConditions
```
    The already computed human readable block completion conditions.
  - outgoingLinks
```
private ImmutableList<IExecutionLink> outgoingLinks
```
    The up to know discovered outgoing links.
  - incomingLinks
```
private ImmutableList<IExecutionLink> incomingLinks
```
    The up to know discovered incoming links.
- Constructor Detail
  - AbstractExecutionNode
```
public AbstractExecutionNode(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
  - getParent
```
public AbstractExecutionNode<?> getParent()
```
    Returns the parent IExecutionNode or null if the current node is the root.
    
    Specified by:
    
    getParent in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The parent IExecutionNode or null on root.
  - setParent
```
public void setParent(AbstractExecutionNode<?> parent)
```
    Sets the parent AbstractExecutionNode.
    
    Parameters:
    
    parent - The parent AbstractExecutionNode to set.
  - getChildren
```
public AbstractExecutionNode<?>[] getChildren()
```
    Returns the available children.
    
    Specified by:
    
    getChildren in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The available children.
  - addChild
```
public void addChild(AbstractExecutionNode<?> child)
```
    Adds a new child AbstractExecutionNode.
    
    Parameters:
    
    child - A new child AbstractExecutionNode.
  - isPathConditionChanged
```
public boolean isPathConditionChanged()
```
    Checks if this node has changed the path condition of the parent.
    
    Specified by:
    
    isPathConditionChanged in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    true has different path condition compared to its parent, false has same path condition as parent.
  - getPathCondition
```
public Term getPathCondition()
                      throws ProofInputException
```
    Returns the path condition to reach this node as Term.
    
    Specified by:
    
    getPathCondition in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The path condition to reach this node as Term.
    
    Throws:
    
    ProofInputException
  - getFormatedPathCondition
```
public java.lang.String getFormatedPathCondition()
                                          throws ProofInputException
```
    Returns the human readable path condition to reach this node as string.
    
    Specified by:
    
    getFormatedPathCondition in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The human readable path condition as string.
    
    Throws:
    
    ProofInputException
  - getCallStack
```
public IExecutionNode<?>[] getCallStack()
```
    Returns the method call stack.
    
    Specified by:
    
    getCallStack in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The method call stack.
  - setCallStack
```
public void setCallStack(IExecutionNode<?>[] callStack)
```
    Sets the call stack.
    
    Parameters:
    
    callStack - The call stack.
  - getConstraints
```
public IExecutionConstraint[] getConstraints()
```
    Returns all available IExecutionConstraints.
    
    Specified by:
    
    getConstraints in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The available IExecutionConstraints.
  - lazyComputeConstraints
```
protected abstract IExecutionConstraint[] lazyComputeConstraints()
```
    Computes the constraints lazily when getConstraints() is called the first time.
    
    Returns:
    
    The IExecutionConstraints of the current state.
  - getActiveStatement
```
public S getActiveStatement()
```
    Returns the active statement which is executed in the code.
    
    Specified by:
    
    getActiveStatement in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The active statement which is executed in the code.
  - getActivePositionInfo
```
public PositionInfo getActivePositionInfo()
```
    Returns the PositionInfo of IExecutionNode.getActiveStatement().
    
    Specified by:
    
    getActivePositionInfo in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The PositionInfo of IExecutionNode.getActiveStatement().
  - getVariables
```
public IExecutionVariable[] getVariables()
                                  throws ProofInputException
```
    Returns the variable value pairs of the current state.
    
    Specified by:
    
    getVariables in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The variable value pairs.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - lazyComputeVariables
```
protected IExecutionVariable[] lazyComputeVariables()
                                             throws ProofInputException
```
    Computes the variables lazily when getVariables() is called the first time.
    
    Returns:
    
    The IExecutionVariables of the current state.
    
    Throws:
    
    ProofInputException
  - getVariables
```
public IExecutionVariable[] getVariables(Term condition)
                                  throws ProofInputException
```
    Returns the variable value pairs of the current state under the given condition.
    
    Specified by:
    
    getVariables in interface IExecutionNode<S extends SourceElement>
    
    Parameters:
    
    condition - A Term specifying some additional constraints to consider.
    
    Returns:
    
    The variable value pairs.
    
    Throws:
    
    ProofInputException
  - lazyComputeVariables
```
protected IExecutionVariable[] lazyComputeVariables(Term condition)
                                             throws ProofInputException
```
    Computes the variables lazily when getVariables(Term) is called the first time.
    
    Parameters:
    
    condition - A Term specifying some additional constraints to consider.
    
    Returns:
    
    The IExecutionVariables of the current state under the given condition.
    
    Throws:
    
    ProofInputException
  - getLayoutExtractor
```
public ExecutionNodeSymbolicLayoutExtractor getLayoutExtractor()
                                                        throws ProofInputException
```
    Returns the used ExecutionNodeSymbolicLayoutExtractor.
    
    Returns:
    
    The used ExecutionNodeSymbolicLayoutExtractor.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - lazyComputeLayoutExtractor
```
protected ExecutionNodeSymbolicLayoutExtractor lazyComputeLayoutExtractor()
                                                                   throws ProofInputException
```
    Instantiates the used ExecutionNodeSymbolicLayoutExtractor lazily when getLayoutExtractor() is called the first time.
    
    Returns:
    
    The created ExecutionNodeSymbolicLayoutExtractor.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getLayoutsCount
```
public int getLayoutsCount()
                    throws ProofInputException
```
    Returns the number of memory layouts.
    
    Specified by:
    
    getLayoutsCount in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The number of memory layouts.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getInitialLayout
```
public ISymbolicLayout getInitialLayout(int layoutIndex)
                                 throws ProofInputException
```
    Returns the initial memory layout before the method was executed.
    
    Specified by:
    
    getInitialLayout in interface IExecutionNode<S extends SourceElement>
    
    Parameters:
    
    layoutIndex - The index of the memory layout.
    
    Returns:
    
    The initial memory layout at the given index.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getCurrentLayout
```
public ISymbolicLayout getCurrentLayout(int layoutIndex)
                                 throws ProofInputException
```
    Returns the current memory layout which shows the memory structure before the current node in the symbolic execution tree is executed.
    
    Specified by:
    
    getCurrentLayout in interface IExecutionNode<S extends SourceElement>
    
    Parameters:
    
    layoutIndex - The index of the memory layout.
    
    Returns:
    
    The current memory layout at the given index.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getLayoutsEquivalenceClasses
```
public ImmutableList<ISymbolicEquivalenceClass> getLayoutsEquivalenceClasses(int layoutIndex)
                                                                      throws ProofInputException
```
    Returns the equivalence classes of the memory layout with the given index.
    
    Specified by:
    
    getLayoutsEquivalenceClasses in interface IExecutionNode<S extends SourceElement>
    
    Parameters:
    
    layoutIndex - The index of the memory layout.
    
    Returns:
    
    The equivalence classes of the memory layout at the given index.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getModalityPIO
```
public PosInOccurrence getModalityPIO()
```
    Returns the PosInOccurrence of the modality of interest including updates.
    
    Specified by:
    
    getModalityPIO in interface IExecutionElement
    
    Returns:
    
    The PosInOccurrence of the modality of interest including updates.
  - lazyComputeModalityPIO
```
protected PosInOccurrence lazyComputeModalityPIO()
```
    Computes the PosInOccurrence lazily when getModalityPIO() is called the first time.
    
    Returns:
    
    The PosInOccurrences of the modality or its updates.
  - getCompletedBlocks
```
public ImmutableList<IExecutionBlockStartNode<?>> getCompletedBlocks()
```
    Returns all code blocks completed by this IExecutionBlockStartNode.
    
    Specified by:
    
    getCompletedBlocks in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    All code blocks completed by this IExecutionBlockStartNode.
  - addCompletedBlock
```
public void addCompletedBlock(IExecutionBlockStartNode<?> completedBlock)
```
    Registers the given IExecutionBlockStartNode.
    
    Parameters:
    
    completedBlock - The IExecutionBlockStartNode to register.
  - removeCompletedBlock
```
public void removeCompletedBlock(IExecutionBlockStartNode<?> completedBlock)
```
    Removes the given IExecutionBlockStartNode from registration.
    
    Parameters:
    
    completedBlock - The IExecutionBlockStartNode to be remove.
  - getBlockCompletionCondition
```
public Term getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
                                 throws ProofInputException
```
    Returns the condition under which this node completes the code block of the given IExecutionBlockStartNode.
    
    Specified by:
    
    getBlockCompletionCondition in interface IExecutionNode<S extends SourceElement>
    
    Parameters:
    
    completedNode - The completed IExecutionBlockStartNode for which the condition is requested.
    
    Returns:
    
    The condition under which this node completes the code block of the given IExecutionBlockStartNode.
    
    Throws:
    
    ProofInputException
  - getFormatedBlockCompletionCondition
```
public java.lang.String getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
                                                     throws ProofInputException
```
    Returns the human readable condition under which this node completes the code block of the given IExecutionBlockStartNode.
    
    Specified by:
    
    getFormatedBlockCompletionCondition in interface IExecutionNode<S extends SourceElement>
    
    Parameters:
    
    completedNode - The completed IExecutionBlockStartNode for which the condition is requested.
    
    Returns:
    
    The human readable condition under which this node completes the code block of the given IExecutionBlockStartNode.
    
    Throws:
    
    ProofInputException
  - lazyComputeBlockCompletionCondition
```
protected java.lang.Object lazyComputeBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode,
                                                               boolean returnFormatedCondition)
                                                        throws ProofInputException
```
    Computes the condition lazily when #getBlockCompletionCondition(IExecutionNode) or #getFormatedBlockCompletionCondition(IExecutionNode) is called the first time.
    
    Parameters:
    
    completedNode - The completed IExecutionNode for which the condition is requested.
    
    returnFormatedCondition - true formated condition is returned, false Term is returned.
    
    Throws:
    
    ProofInputException - Occurred Exception
  - removeChild
```
public void removeChild(IExecutionNode<?> child)
```
    Removes the given child.
    
    Parameters:
    
    child - The child to be removed.
  - addOutgoingLink
```
public void addOutgoingLink(IExecutionLink link)
```
    Adds the given IExecutionLink as outgoing link.
    
    Parameters:
    
    link - The IExecutionLink to add.
  - removeOutgoingLink
```
public void removeOutgoingLink(IExecutionLink link)
```
    Removes the given IExecutionLink from the outgoing links.
    
    Parameters:
    
    link - The IExecutionLink to remove.
  - getOutgoingLink
```
public IExecutionLink getOutgoingLink(IExecutionNode<?> target)
```
    Returns the outgoing IExecutionLink.
    
    Specified by:
    
    getOutgoingLink in interface IExecutionNode<S extends SourceElement>
    
    Parameters:
    
    target - The target IExecutionNode.
    
    Returns:
    
    The found IExecutionLink or null if such a link is not available.
  - getOutgoingLinks
```
public ImmutableList<IExecutionLink> getOutgoingLinks()
```
    Returns all available outgoing links.
    
    Specified by:
    
    getOutgoingLinks in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The available outgoing links.
  - getIncomingLink
```
public IExecutionLink getIncomingLink(IExecutionNode<?> source)
```
    Returns the incoming IExecutionLink.
    
    Specified by:
    
    getIncomingLink in interface IExecutionNode<S extends SourceElement>
    
    Parameters:
    
    source - The source IExecutionNode.
    
    Returns:
    
    The found IExecutionLink or null if such a link is not available.
  - addIncomingLink
```
public void addIncomingLink(IExecutionLink link)
```
    Adds the given IExecutionLink as incoming link.
    
    Parameters:
    
    link - The IExecutionLink to add.
  - removeIncomingLink
```
public void removeIncomingLink(IExecutionLink link)
```
    Removes the given IExecutionLink from the incoming links.
    
    Parameters:
    
    link - The IExecutionLink to remove.
  - getIncomingLinks
```
public ImmutableList<IExecutionLink> getIncomingLinks()
```
    Returns all available incoming links.
    
    Specified by:
    
    getIncomingLinks in interface IExecutionNode<S extends SourceElement>
    
    Returns:
    
    The available incoming links.

Class AbstractExecutionNode<S extends SourceElement>

Field Summary

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

Constructor Summary

Method Summary

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

Methods inherited from class java.lang.Object

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

Field Detail

parent

children

callStack

constraints

variables

conditionalVariables

layoutExtractor

modalityPIO

completedBlocks

blockCompletionConditions

formatedBlockCompletionConditions

outgoingLinks

incomingLinks

Constructor Detail

AbstractExecutionNode

Method Detail

getParent

setParent

getChildren

addChild

isPathConditionChanged

getPathCondition

getFormatedPathCondition

getCallStack

setCallStack

getConstraints

lazyComputeConstraints

getActiveStatement

getActivePositionInfo

getVariables

lazyComputeVariables

getVariables

lazyComputeVariables

getLayoutExtractor

lazyComputeLayoutExtractor

getLayoutsCount

getInitialLayout

getCurrentLayout

getLayoutsEquivalenceClasses

getModalityPIO

lazyComputeModalityPIO

getCompletedBlocks

addCompletedBlock

removeCompletedBlock

getBlockCompletionCondition

getFormatedBlockCompletionCondition

lazyComputeBlockCompletionCondition

removeChild

addOutgoingLink

removeOutgoingLink

getOutgoingLink

getOutgoingLinks

getIncomingLink

addIncomingLink

removeIncomingLink

getIncomingLinks