public abstract class AbstractCallStackBasedStopCondition extends java.lang.Object implements StopCondition
StopCondition
s which stops
the auto mode when the call stack size of the starting set node has
a special difference to the call stack size of the current set node, e.g.
"step over" or "step return".StepOverSymbolicExecutionTreeNodesStopCondition
,
StepReturnSymbolicExecutionTreeNodesStopCondition
Modifier and Type | Class and Description |
---|---|
private static class |
AbstractCallStackBasedStopCondition.NodeStartEntry
Instances of this class are used in
startingCallStackSizePerGoal
to represent the initial Node of Goal on which
the auto mode was started together with its call stack size. |
Modifier and Type | Field and Description |
---|---|
private java.util.Map<Goal,AbstractCallStackBasedStopCondition.NodeStartEntry> |
startingCallStackSizePerGoal
Maps a
Goal to the initial call stack size at which the auto mode was started. |
Constructor and Description |
---|
AbstractCallStackBasedStopCondition() |
Modifier and Type | Method and Description |
---|---|
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 abstract boolean |
isCallStackSizeReached(int initialCallStackSize,
int currentCallStackSize)
Checks if the call stack size limit is reached.
|
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. |
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.
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getGoalNotAllowedMessage
private java.util.Map<Goal,AbstractCallStackBasedStopCondition.NodeStartEntry> startingCallStackSizePerGoal
Goal
to the initial call stack size at which the auto mode was started.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 abstract boolean isCallStackSizeReached(int initialCallStackSize, int currentCallStackSize)
initialCallStackSize
- The call stack size of the initial set node.currentCallStackSize
- The call stack size of the current set node.true
limit reached, false
limit node reached.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
.