de.uka.ilkd.key.symbolic_execution.util

Class SymbolicExecutionUtil.FindModalityWithSymbolicExecutionLabelId

java.lang.Object

de.uka.ilkd.key.logic.DefaultVisitor

de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil.FindModalityWithSymbolicExecutionLabelId

All Implemented Interfaces:

Visitor

Enclosing class:

SymbolicExecutionUtil

private static final class SymbolicExecutionUtil.FindModalityWithSymbolicExecutionLabelId
extends DefaultVisitor

Utility class used to find the maximal modality Term used by SymbolicExecutionUtil.findModalityWithMaxSymbolicExecutionLabelId(Term).

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private PosInTerm	currentPosInTerm The current PosInTerm.
private java.util.Deque<java.lang.Integer>	indexStack
private int	maxId The maximal ID.
private boolean	maximum true search maximal ID, false search minimal ID.
private PosInTerm	posInTerm The modality PosInTerm with the maximal ID.

Constructor Summary

Constructors

Constructor and Description
FindModalityWithSymbolicExecutionLabelId(boolean maximum) Constructor.

Method Summary

Modifier and Type	Method and Description
PosInTerm	getPosInTerm() Returns the modality PosInTerm with the maximal ID.
void	subtreeEntered(Term subtreeRoot) this method is called in execPreOrder and execPostOrder in class Term when entering the subtree rooted in the term subtreeRoot.
void	subtreeLeft(Term subtreeRoot) this method is called in execPreOrder and execPostOrder in class Term when leaving the subtree rooted in the term subtreeRoot.
void	visit(Term visited) the entry method for the visitor pattern

Methods inherited from class de.uka.ilkd.key.logic.DefaultVisitor

visitSubtree

Methods inherited from class java.lang.Object

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

Field Detail

posInTerm

private PosInTerm posInTerm

The modality PosInTerm with the maximal ID.

maxId

private int maxId

The maximal ID.

maximum

private boolean maximum

true search maximal ID, false search minimal ID.

currentPosInTerm

private PosInTerm currentPosInTerm

The current PosInTerm.

indexStack

private java.util.Deque<java.lang.Integer> indexStack

Constructor Detail

FindModalityWithSymbolicExecutionLabelId

public FindModalityWithSymbolicExecutionLabelId(boolean maximum)

Constructor.

Parameters:

maximum - true search maximal ID, false search minimal ID.

Method Detail

visit

public void visit(Term visited)

the entry method for the visitor pattern

Parameters:

visited - the Term to be visited

subtreeEntered

public void subtreeEntered(Term subtreeRoot)

this method is called in execPreOrder and execPostOrder in class Term when entering the subtree rooted in the term subtreeRoot. Default implementation is to do nothing. Subclasses can override this method when the visitor behaviour depends on informations bound to subtrees.

Specified by:

subtreeEntered in interface Visitor

Overrides:

subtreeEntered in class DefaultVisitor

Parameters:

subtreeRoot - root of the subtree which the visitor enters.

subtreeLeft

public void subtreeLeft(Term subtreeRoot)

this method is called in execPreOrder and execPostOrder in class Term when leaving the subtree rooted in the term subtreeRoot. Default implementation is to do nothing. Subclasses can override this method when the visitor behaviour depends on informations bound to subtrees.

Specified by:

subtreeLeft in interface Visitor

Overrides:

subtreeLeft in class DefaultVisitor

Parameters:

subtreeRoot - root of the subtree which the visitor leaves.

getPosInTerm

public PosInTerm getPosInTerm()

Returns the modality PosInTerm with the maximal ID.

Returns:

The modality PosInTerm with the maximal ID.