public class SymbolicExecutionGoalChooser extends DepthFirstGoalChooser
This GoalChooser
is a special implementation of the default
DepthFirstGoalChooser
. The difference is that a rule which
creates a new symbolic execution tree node on a Goal
is only applied
if all other Goal
s will also creates new symbolic execution tree
nodes. This has the advantage that invalid branches may closed before
new symbolic execution tree nodes are created.
The order in which new symbolic execution tree nodes are created is also
managed by this GoalChooser
. The idea is that on each Goal
a new symbolic execution tree node is created before on one Goal
a second one will be created. This has the affect that for instance on all
branches of a branch statement the next statement is evaluated before the first
branch executes the second statement.
A second criteria is the used custom StopCondition
of the current
Proof
. Goal
s on that the next set node is allowed are
preferred to branches on which is not allowed. This is required to make
sure that for instance a step over or step return result is completely
performed on all Goal
s before on one Goal
a further
set node is executed.
SymbolicExecutionGoalChooserBuilder
Modifier and Type | Field and Description |
---|---|
private java.util.Set<Goal> |
goalsToPrefer
This
Set is used to count on which Goal s a
symbolic execution node was executed. |
private StopCondition |
stopCondition
The optional custom stop condition used in the current proof.
|
allGoalsSatisfiable, currentSubtreeRoot, goalList, nextGoalCounter, nextGoals, proof, selectedList
Constructor and Description |
---|
SymbolicExecutionGoalChooser() |
Modifier and Type | Method and Description |
---|---|
Goal |
getNextGoal() |
void |
init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
void |
removeGoal(Goal p_goal)
Remove p_goal from selectedList (e.g. no taclet can be applied to
p_goal)
|
void |
updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
insertNewGoals, updateGoalListHelp
findMinimalSubtree, findMinimalSubtreeBelow, isSatisfiableSubtree, removeClosedGoals, rotateList, setupGoals
private java.util.Set<Goal> goalsToPrefer
Set
is used to count on which Goal
s a
symbolic execution node was executed. Initially it is filled in
getNextGoal()
with all possible Goal
s. Every call
of getNextGoal()
will then remove a Goal
from this list.
If a Goal
is not contained in this list it is skipped in
getNextGoal()
until the Set
is empty which indicates
that on all Goal
s a symbolic execution tree node was created.
Then the process starts again.private StopCondition stopCondition
public Goal getNextGoal()
getNextGoal
in interface GoalChooser
getNextGoal
in class DepthFirstGoalChooser
public void init(Proof p_proof, ImmutableList<Goal> p_goals)
init
in interface GoalChooser
init
in class DefaultGoalChooser
p_proof
- *param p_goals the initial list of goalspublic void removeGoal(Goal p_goal)
removeGoal
in interface GoalChooser
removeGoal
in class DefaultGoalChooser
public void updateGoalList(Node node, ImmutableList<Goal> newGoals)
updateGoalList
in interface GoalChooser
updateGoalList
in class DefaultGoalChooser