de.uka.ilkd.key.symbolic_execution

Class AbstractUpdateExtractor.NodeGoal

java.lang.Object

de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor.NodeGoal

Enclosing class:

AbstractUpdateExtractor

protected static class AbstractUpdateExtractor.NodeGoal
extends java.lang.Object

Utility class used by AbstractUpdateExtractor#computeValueConditions(Set, Map). Instances of this class store the current Node and the Goals at which backward iteration on parents has started.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Node	currentNode The current Node.
private ImmutableList<Goal>	startingGoals The Goals at which backward iteration has started.

Constructor Summary

Constructors

Constructor and Description
NodeGoal(Goal goal) Constructor.
NodeGoal(Node currentNode, ImmutableList<Goal> startingGoals) A reached child node during backward iteration.

Method Summary

Modifier and Type	Method and Description
Node	getCurrentNode() Returns the current Node.
Node	getParent() Returns the parent of getCurrentNode().
int	getSerialNr() Returns the serial number of getCurrentNode().
ImmutableList<Goal>	getStartingGoals() Returns the Goals at which backward iteration has started.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

currentNode

private final Node currentNode

The current Node.

startingGoals

private final ImmutableList<Goal> startingGoals

The Goals at which backward iteration has started.

Constructor Detail

NodeGoal

public NodeGoal(Goal goal)

Constructor.

Parameters:

goal - The current Goal to start backward iteration at.

NodeGoal

public NodeGoal(Node currentNode,
                ImmutableList<Goal> startingGoals)

A reached child node during backward iteration.

Parameters:

currentNode - The current Node.

startingGoals - The Goals at which backward iteration has started.

Method Detail

getCurrentNode

public Node getCurrentNode()

Returns the current Node.

Returns:

The current Node.

getParent

public Node getParent()

Returns the parent of getCurrentNode().

Returns:

The parent of getCurrentNode().

getSerialNr

public int getSerialNr()

Returns the serial number of getCurrentNode().

Returns:

The serial number of getCurrentNode().

getStartingGoals

public ImmutableList<Goal> getStartingGoals()

Returns the Goals at which backward iteration has started.

Returns:

The Goals at which backward iteration has started.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object