de.uka.ilkd.key.symbolic_execution.strategy

Class AbstractCallStackBasedStopCondition

java.lang.Object

de.uka.ilkd.key.symbolic_execution.strategy.AbstractCallStackBasedStopCondition

All Implemented Interfaces:

StopCondition

Direct Known Subclasses:

StepOverSymbolicExecutionTreeNodesStopCondition, StepReturnSymbolicExecutionTreeNodesStopCondition

public abstract class AbstractCallStackBasedStopCondition
extends java.lang.Object
implements StopCondition

Provides the basic functionality for StopConditions 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".

Author:

Martin Hentschel

See Also:

StepOverSymbolicExecutionTreeNodesStopCondition, StepReturnSymbolicExecutionTreeNodesStopCondition

Nested Class Summary

Nested Classes

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.

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
AbstractCallStackBasedStopCondition()

Method Summary

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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.prover.StopCondition

getGoalNotAllowedMessage

Field Detail

startingCallStackSizePerGoal

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 Detail

AbstractCallStackBasedStopCondition

public AbstractCallStackBasedStopCondition()

Method Detail

getMaximalWork

public 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. Pass 0 to indicate unknown size.

Specified by:

getMaximalWork in interface StopCondition

Parameters:

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.

Returns:

The maximal amount of work or 0 if it is unknown.

isGoalAllowed

public 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. If it is not allowed the apply strategy will stop.

Specified by:

isGoalAllowed in interface StopCondition

Parameters:

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.

Returns:

true rule application is allowed, false rule application is not allowed so stop apply strategy

isCallStackSizeReached

protected abstract boolean isCallStackSizeReached(int initialCallStackSize,
                                                  int currentCallStackSize)

Checks if the call stack size limit is reached.

Parameters:

initialCallStackSize - The call stack size of the initial set node.

currentCallStackSize - The call stack size of the current set node.

Returns:

true limit reached, false limit node reached.

shouldStop

public 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.

Specified by:

shouldStop in interface StopCondition

Parameters:

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.

Returns:

true stop strategy, false continue strategy and apply next rule.

getStopMessage

public 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.

Specified by:

getStopMessage in interface StopCondition

Parameters:

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.

Returns:

The human readable message which explains the stop reason.