private static final class SymbolicExecutionUtil.FindModalityWithSymbolicExecutionLabelId extends DefaultVisitor
SymbolicExecutionUtil.findModalityWithMaxSymbolicExecutionLabelId(Term)
.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 and Description |
---|
FindModalityWithSymbolicExecutionLabelId(boolean maximum)
Constructor.
|
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
|
visitSubtree
private int maxId
private boolean maximum
true
search maximal ID, false
search minimal ID.private java.util.Deque<java.lang.Integer> indexStack
public FindModalityWithSymbolicExecutionLabelId(boolean maximum)
maximum
- true
search maximal ID, false
search minimal ID.public void visit(Term visited)
visited
- the Term to be visitedpublic void subtreeEntered(Term subtreeRoot)
subtreeEntered
in interface Visitor
subtreeEntered
in class DefaultVisitor
subtreeRoot
- root of the subtree which the visitor enters.public void subtreeLeft(Term subtreeRoot)
subtreeLeft
in interface Visitor
subtreeLeft
in class DefaultVisitor
subtreeRoot
- root of the subtree which the visitor leaves.