public class BreakpointStopCondition extends Object implements IBreakpointStopCondition
IBreakpointStopCondition
which can be used during proof.Modifier and Type | Field and Description |
---|---|
private boolean |
breakpointHit
Indicates that a breakpoint is hit.
|
private Set<IBreakpoint> |
breakpoints
The used
IBreakpoint s. |
Constructor and Description |
---|
BreakpointStopCondition(IBreakpoint... breakpoints)
Creates a new
BreakpointStopCondition . |
Modifier and Type | Method and Description |
---|---|
void |
addBreakpoint(IBreakpoint breakpoint)
Adds a new
IBreakpoint . |
Set<IBreakpoint> |
getBreakpoints()
Returns all available
IBreakpoint s. |
String |
getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
IGoalChooser goalChooser,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, IGoalChooser, long, int, Goal)
has stopped the apply strategy. |
int |
getMaximalWork(int maxApplications,
long timeout,
Proof proof,
IGoalChooser goalChooser)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
String |
getStopMessage(int maxApplications,
long timeout,
Proof proof,
IGoalChooser goalChooser,
long startTime,
int countApplied,
ApplyStrategy.SingleRuleApplicationInfo singleRuleApplicationInfo)
Returns a human readable message which explains why the previous
#shouldStop(ApplyStrategy, Proof, IGoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy. |
protected boolean |
isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
boolean |
isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
IGoalChooser goalChooser,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the IGoalChooser before it is applied. |
void |
removeBreakpoint(IBreakpoint breakpoint)
Removes an
IBreakpoint . |
boolean |
shouldStop(int maxApplications,
long timeout,
Proof proof,
IGoalChooser goalChooser,
long startTime,
int countApplied,
ApplyStrategy.SingleRuleApplicationInfo singleRuleApplicationInfo)
Checks after each applied rule if more rules should be applied or if the strategy should stop.
|
private final Set<IBreakpoint> breakpoints
IBreakpoint
s.private boolean breakpointHit
public BreakpointStopCondition(IBreakpoint... breakpoints)
BreakpointStopCondition
.breakpoints
- The IBreakpoint
to use.public int getMaximalWork(int maxApplications, long timeout, Proof proof, IGoalChooser goalChooser)
0
to indicate unknown size.getMaximalWork
in interface ApplyStrategy.IStopCondition
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
.goalChooser
- The current IGoalChooser
.0
if it is unknown.public boolean isGoalAllowed(int maxApplications, long timeout, Proof proof, IGoalChooser goalChooser, long startTime, int countApplied, Goal goal)
Goal
chosen by the IGoalChooser
before it is applied.
If it is not allowed the apply strategy will stop.isGoalAllowed
in interface ApplyStrategy.IStopCondition
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
.goalChooser
- The current IGoalChooser
.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 strategypublic String getGoalNotAllowedMessage(int maxApplications, long timeout, Proof proof, IGoalChooser goalChooser, long startTime, int countApplied, Goal goal)
#isGoalAllowed(ApplyStrategy, int, long, Proof, IGoalChooser, long, int, Goal)
has stopped the apply strategy.getGoalNotAllowedMessage
in interface ApplyStrategy.IStopCondition
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
.goalChooser
- The current IGoalChooser
.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, IGoalChooser goalChooser, long startTime, int countApplied, ApplyStrategy.SingleRuleApplicationInfo singleRuleApplicationInfo)
shouldStop
in interface ApplyStrategy.IStopCondition
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
.goalChooser
- The current IGoalChooser
.startTime
- The timestamp when the apply strategy has started, computed via System.currentTimeMillis()
countApplied
- The number of already applied rules.singleRuleApplicationInfo
- An optional ApplyStrategy.SingleRuleApplicationInfo
.true
stop strategy, false
continue strategy and apply next rule.protected boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, Proof proof, Node node)
activeStatement
- the activeStatement of the noderuleApp
- the applied RuleApp
proof
- the current proofnode
- the current nodetrue
at least one breakpoint is hit, false
all breakpoints are not hit.public String getStopMessage(int maxApplications, long timeout, Proof proof, IGoalChooser goalChooser, long startTime, int countApplied, ApplyStrategy.SingleRuleApplicationInfo singleRuleApplicationInfo)
#shouldStop(ApplyStrategy, Proof, IGoalChooser, long, int, SingleRuleApplicationInfo)
has stopped the strategy.getStopMessage
in interface ApplyStrategy.IStopCondition
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
.goalChooser
- The current IGoalChooser
.startTime
- The timestamp when the apply strategy has started, computed via System.currentTimeMillis()
countApplied
- The number of already applied rules.singleRuleApplicationInfo
- An optional ApplyStrategy.SingleRuleApplicationInfo
.public void addBreakpoint(IBreakpoint breakpoint)
IBreakpoint
.addBreakpoint
in interface IBreakpointStopCondition
breakpoint
- The IBreakpoint
to add.public void removeBreakpoint(IBreakpoint breakpoint)
IBreakpoint
.removeBreakpoint
in interface IBreakpointStopCondition
breakpoint
- The IBreakpoint
to remove.public Set<IBreakpoint> getBreakpoints()
IBreakpoint
s.getBreakpoints
in interface IBreakpointStopCondition
IBreakpoint
s.