public class ExecutedSymbolicExecutionTreeNodesStopCondition extends java.lang.Object implements StopCondition
This StopCondition
stops the auto mode (ApplyStrategy
) if
a given number (getMaximalNumberOfSetNodesToExecutePerGoal()
) of maximal
executed symbolic execution tree nodes is reached in a goal.
If a Node
in
KeY's proof tree is also a node in a symbolic execution tree is computed
via SymbolicExecutionUtil#isSymbolicExecutionTreeNode(Node)
.
The auto mode is stopped exactly in the open goal Node
which
will become the next symbolic execution tree node.
Modifier and Type | Field and Description |
---|---|
private java.util.Map<Goal,java.lang.Integer> |
executedNumberOfSetNodesPerGoal
Maps a
Goal to the number of executed symbolic execution tree nodes. |
private java.util.Map<Node,java.lang.Boolean> |
goalAllowedResultPerSetNode
Stores for each
Node which is a symbolic execution tree node the computed result
of isGoalAllowed(int, long, Proof, long, int, Goal) to make
sure that it is only computed once and that the number of executed set statements is
not increased multiple times for the same Node . |
static int |
MAXIMAL_NUMBER_OF_SET_NODES_TO_EXECUTE_PER_GOAL_FOR_ONE_STEP
The default maximal number of steps to do exactly one step in each goal.
|
static int |
MAXIMAL_NUMBER_OF_SET_NODES_TO_EXECUTE_PER_GOAL_IN_COMPLETE_RUN
The default maximal number of steps to simulate a complete program execution.
|
private int |
maximalNumberOfSetNodesToExecutePerGoal
The maximal number of allowed symbolic execution tree nodes per goal.
|
Constructor and Description |
---|
ExecutedSymbolicExecutionTreeNodesStopCondition()
Constructor to stop after one executed symbolic execution tree node.
|
ExecutedSymbolicExecutionTreeNodesStopCondition(int maximalNumberOfSetNodesToExecutePerGoal)
Constructor to stop after the given number of symbolic execution tree nodes.
|
Modifier and Type | Method and Description |
---|---|
java.util.Map<Goal,java.lang.Integer> |
getExectuedSetNodesPerGoal()
Returns the number of executed symbolic execution tree nodes per
Goal . |
java.lang.String |
getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
int |
getMaximalNumberOfSetNodesToExecutePerGoal()
Returns the maximal number of executed symbolic execution tree nodes per goal per auto mode run.
|
int |
getMaximalWork(int maxApplications,
long timeout,
Proof proof)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
java.lang.String |
getStopMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Returns a human readable message which explains why the previous
#shouldStop(ApplyStrategy, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy. |
protected void |
handleNodeLimitExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is exceeded.
|
protected void |
handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
boolean |
isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
void |
setMaximalNumberOfSetNodesToExecutePerGoal(int maximalNumberOfSetNodesToExecute)
Sets the maximal number of executed symbolic execution tree nodes per goal per auto mode run.
|
boolean |
shouldStop(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
SingleRuleApplicationInfo singleRuleApplicationInfo)
Checks after each applied rule if more rules should be applied or if the strategy should stop.
|
boolean |
wasSetNodeExecuted()
Checks if at least one symbolic execution tree node was executed.
|
public static final int MAXIMAL_NUMBER_OF_SET_NODES_TO_EXECUTE_PER_GOAL_IN_COMPLETE_RUN
public static final int MAXIMAL_NUMBER_OF_SET_NODES_TO_EXECUTE_PER_GOAL_FOR_ONE_STEP
private int maximalNumberOfSetNodesToExecutePerGoal
private final java.util.Map<Goal,java.lang.Integer> executedNumberOfSetNodesPerGoal
Goal
to the number of executed symbolic execution tree nodes.private final java.util.Map<Node,java.lang.Boolean> goalAllowedResultPerSetNode
Node
which is a symbolic execution tree node the computed result
of isGoalAllowed(int, long, Proof, long, int, Goal)
to make
sure that it is only computed once and that the number of executed set statements is
not increased multiple times for the same Node
.public ExecutedSymbolicExecutionTreeNodesStopCondition()
public ExecutedSymbolicExecutionTreeNodesStopCondition(int maximalNumberOfSetNodesToExecutePerGoal)
maximalNumberOfSetNodesToExecutePerGoal
- The maximal number of allowed symbolic execution tree nodes per goal.public int getMaximalWork(int maxApplications, long timeout, Proof proof)
0
to indicate unknown size.getMaximalWork
in interface StopCondition
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.0
if it is unknown.public boolean isGoalAllowed(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal)
Goal
chosen by the GoalChooser
before it is applied.
If it is not allowed the apply strategy will stop.isGoalAllowed
in interface StopCondition
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.startTime
- The timestamp when the apply strategy has started, computed via System.currentTimeMillis()
countApplied
- The number of already applied rules.goal
- The current Goal
on which the next rule will be applied.true
rule application is allowed, false
rule application is not allowed so stop apply strategyprotected void handleNodeLimitExceeded(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal, Node node, RuleApp ruleApp, java.lang.Integer executedNumberOfSetNodes)
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.startTime
- The timestamp when the apply strategy has started, computed via System.nanoTime()
countApplied
- The number of already applied rules.goal
- The current Goal
on which the next rule will be applied.node
- The Node
of the current Goal
.ruleApp
- The current RuleApp
.executedNumberOfSetNodes
- The executed number of SET nodes.protected void handleNodeLimitNotExceeded(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal, Node node, RuleApp ruleApp, java.lang.Integer executedNumberOfSetNodes)
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.startTime
- The timestamp when the apply strategy has started, computed via System.nanoTime()
countApplied
- The number of already applied rules.goal
- The current Goal
on which the next rule will be applied.node
- The Node
of the current Goal
.ruleApp
- The current RuleApp
.executedNumberOfSetNodes
- The executed number of SET nodes.public java.lang.String getGoalNotAllowedMessage(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal)
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy.getGoalNotAllowedMessage
in interface StopCondition
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.startTime
- The timestamp when the apply strategy has started, computed via System.currentTimeMillis()
countApplied
- The number of already applied rules.goal
- The current Goal
on which the next rule will be applied.public boolean shouldStop(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, SingleRuleApplicationInfo singleRuleApplicationInfo)
shouldStop
in interface StopCondition
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.startTime
- The timestamp when the apply strategy has started, computed via System.currentTimeMillis()
countApplied
- The number of already applied rules.singleRuleApplicationInfo
- An optional SingleRuleApplicationInfo
.true
stop strategy, false
continue strategy and apply next rule.public java.lang.String getStopMessage(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, SingleRuleApplicationInfo singleRuleApplicationInfo)
#shouldStop(ApplyStrategy, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy.getStopMessage
in interface StopCondition
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.startTime
- The timestamp when the apply strategy has started, computed via System.currentTimeMillis()
countApplied
- The number of already applied rules.singleRuleApplicationInfo
- An optional SingleRuleApplicationInfo
.public int getMaximalNumberOfSetNodesToExecutePerGoal()
public void setMaximalNumberOfSetNodesToExecutePerGoal(int maximalNumberOfSetNodesToExecute)
maximalNumberOfSetNodesToExecute
- The maximal number of executed symbolic execution tree nodes per per goal auto mode run.public boolean wasSetNodeExecuted()
true
at least one symbolic execution tree node was executed, false
no symbolic execution tree node was executed.