de.uka.ilkd.key.symbolic_execution.strategy

Class StepOverSymbolicExecutionTreeNodesStopCondition

java.lang.Object

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

de.uka.ilkd.key.symbolic_execution.strategy.StepOverSymbolicExecutionTreeNodesStopCondition

All Implemented Interfaces:

StopCondition

public class StepOverSymbolicExecutionTreeNodesStopCondition
extends AbstractCallStackBasedStopCondition

This StopCondition stops the auto mode when a "step over" is completed. This is the case when the next symbolic execution tree node was executed on a Goal which has the same call or lower stack size as the symbolic execution tree node of the Goal on which the auto mode was started.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
StepOverSymbolicExecutionTreeNodesStopCondition()

Method Summary

Modifier and Type	Method and Description
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.
protected boolean	isCallStackSizeReached(int initialCallStackSize, int currentCallStackSize) Checks if the call stack size limit is reached.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.strategy.AbstractCallStackBasedStopCondition

getMaximalWork, getStopMessage, isGoalAllowed, shouldStop

Methods inherited from class java.lang.Object

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

Constructor Detail

StepOverSymbolicExecutionTreeNodesStopCondition

public StepOverSymbolicExecutionTreeNodesStopCondition()

Method Detail

isCallStackSizeReached

protected boolean isCallStackSizeReached(int initialCallStackSize,
                                         int currentCallStackSize)

Checks if the call stack size limit is reached.

Specified by:

isCallStackSizeReached in class AbstractCallStackBasedStopCondition

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.

getGoalNotAllowedMessage

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

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: