de.uka.ilkd.key.prover

Interface StopCondition

All Known Subinterfaces:

IBreakpointStopCondition

All Known Implementing Classes:

AbstractCallStackBasedStopCondition, AppliedRuleStopCondition, BreakpointStopCondition, CompoundStopCondition, ExecutedSymbolicExecutionTreeNodesStopCondition, StepOverSymbolicExecutionTreeNodesStopCondition, StepReturnSymbolicExecutionTreeNodesStopCondition, SymbolicExecutionBreakpointStopCondition

public interface StopCondition

Implementation of this interface are used in ApplyStrategy to determine if the strategy should stop or continue.

The first check is done before a rule is applied on a Goal via #isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal). If this method returns false the strategy stops and the reason shown to the user is computed via #getGoalNotAllowedMessage(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal).

The second check is after a rule was applied via #shouldStop(ApplyStrategy, int, long, Proof, GoalChooser, long, int, SingleRuleApplicationInfo). If this method returns true the strategy stops and the reason shown to the user is computed via #getStopMessage(ApplyStrategy, int, long, Proof, GoalChooser, long, int, SingleRuleApplicationInfo).

Attention: It is possible that an StopCondition has to check one Goal with the same node multiple times. It is required that the called check method always returns the same result for the same Node of a Goal.

Author:

Martin Hentschel

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

Method Detail

getMaximalWork

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.

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

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.

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

getGoalNotAllowedMessage

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:

shouldStop

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.

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

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.

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.