public class ExecutionVariableExtractor extends AbstractUpdateExtractor
IExecutionVariable
s.Modifier and Type | Class and Description |
---|---|
static class |
ExecutionVariableExtractor.ExtractedExecutionValue
The
IExecutionValue instantiated by the ExecutionVariableExtractor . |
static class |
ExecutionVariableExtractor.ExtractedExecutionVariable
The
IExecutionVariable instantiated by the ExecutionVariableExtractor . |
private static class |
ExecutionVariableExtractor.LocationDefinition
Utility class representing a location.
|
private static class |
ExecutionVariableExtractor.ParentDefinition
Utility class representing a parent definition.
|
private class |
ExecutionVariableExtractor.StateExecutionVariable
The
IExecutionVariable instantiated by the ExecutionVariableExtractor . |
AbstractUpdateExtractor.ExecutionVariableValuePair, AbstractUpdateExtractor.ExtractLocationParameter, AbstractUpdateExtractor.NodeGoal
Modifier and Type | Field and Description |
---|---|
private Term |
additionalCondition
An optional additional condition.
|
private java.util.Map<ExecutionVariableExtractor.LocationDefinition,ExecutionVariableExtractor.StateExecutionVariable> |
allStateVariables
The found
IExecutionVariable s available via analyse() . |
private java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
currentLocations
The current locations.
|
private IExecutionNode<?> |
executionNode
The current
IExecutionNode . |
private Term |
layoutTerm
The layout term.
|
private java.util.Set<Term> |
objectsToIgnore
The objects to ignore.
|
private boolean |
simplifyConditions
true simplify conditions, false do not simplify conditions. |
modalityPio, node
Constructor and Description |
---|
ExecutionVariableExtractor(Node node,
PosInOccurrence modalityPio,
IExecutionNode<?> executionNode,
Term condition,
boolean simplifyConditions)
Constructor.
|
collectAdditionalUpdates, collectLocationsFromHeapTerms, collectLocationsFromHeapUpdate, collectLocationsFromTerm, collectLocationsFromTerm, collectLocationsFromUpdates, computeBranchCondition, computeInitialObjectsToIgnore, computeOriginalUpdates, computeValueConditions, computeVariableValuePairs, containsImplicitProgramVariable, countOpenChildren, createLocationPredicateAndTerm, extractLocationsFromSequent, extractLocationsFromTerm, fillInitialObjectsToIgnoreRecursively, getProof, getRoot, getServices, hasFreeVariables, isImplicitProgramVariable, isParentReachedOnAllChildGoals, iterateBackOnParents, removeImplicitSubTermsFromPathCondition
private final IExecutionNode<?> executionNode
IExecutionNode
.private final Term additionalCondition
private final Term layoutTerm
private final java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> currentLocations
private final java.util.Set<Term> objectsToIgnore
private final java.util.Map<ExecutionVariableExtractor.LocationDefinition,ExecutionVariableExtractor.StateExecutionVariable> allStateVariables
IExecutionVariable
s available via analyse()
.private final boolean simplifyConditions
true
simplify conditions, false
do not simplify conditions.public ExecutionVariableExtractor(Node node, PosInOccurrence modalityPio, IExecutionNode<?> executionNode, Term condition, boolean simplifyConditions) throws ProofInputException
node
- The Node
which provides the state.modalityPio
- The PosInOccurrence
in the Node
.executionNode
- The current IExecutionNode
.condition
- An optional additional condition.simplifyConditions
- true
simplify conditions, false
do not simplify conditions.ProofInputException
- Occurred Exceptionpublic IExecutionVariable[] analyse() throws ProofInputException
IExecutionVariable
s.IExecutionVariable
s representing the current state.ProofInputException
- Occurred Exception.protected void analyzeTreeStructure(java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>> topVariables, java.util.Map<ExecutionVariableExtractor.ParentDefinition,java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap)
ExecutionVariableValuePair
s.pairs
- The ExecutionVariableValuePair
s to analyze.topVariables
- The state locations,contentMap
- The child locations.protected IExecutionVariable createVariablesValueStructure(java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, java.util.Map<ExecutionVariableExtractor.ParentDefinition,java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap, ExecutionVariableExtractor.ExtractedExecutionValue parentValue, ImmutableList<Term> alreadyVisitedObjects) throws ProofInputException
IExecutionVariable
for the given ExecutionVariableValuePair
s.pairs
- The ExecutionVariableValuePair
s to represent.contentMap
- The Map
providing child content information.parentValue
- The optional parent IExecutionValue
.alreadyVisitedObjects
- The value Term
s of already visited objects on the current path in the variable-value-hierarchy.IExecutionVariable
.ProofInputException
- Occurred Exception.protected void createValues(IExecutionVariable variable, java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, AbstractUpdateExtractor.ExecutionVariableValuePair firstPair, java.util.Map<ExecutionVariableExtractor.ParentDefinition,java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap, java.util.List<IExecutionValue> valueListToFill, ImmutableList<Term> alreadyVisitedObjects) throws ProofInputException
IExecutionValue
s of the given IExecutionVariable
.variable
- The IExecutionVariable
.pairs
- The ExecutionVariableValuePair
s which provides the content.firstPair
- The first entry in the ExecutionVariableValuePair
s.contentMap
- The content Map
.valueListToFill
- The result List
to fill.alreadyVisitedObjects
- The value Term
s of already visited objects on the current path in the variable-value-hierarchy.ProofInputException
- Occurred Exception.protected Pair<java.lang.Boolean,ImmutableList<Term>> updateAlreadyVisitedObjects(ImmutableList<Term> alreadyVisitedObjects, Term value)
alreadyVisitedObjects
- The value Term
s of already visited objects on the current path in the variable-value-hierarchy.value
- The current value.