de.uka.ilkd.key.macros

Class TestGenMacro.TestGenStrategy

java.lang.Object

de.uka.ilkd.key.macros.FilterStrategy

de.uka.ilkd.key.macros.TestGenMacro.TestGenStrategy

All Implemented Interfaces:

Named, Feature, Strategy

Enclosing class:

TestGenMacro

private static class TestGenMacro.TestGenStrategy
extends FilterStrategy

The Class FilterAppManager is a special strategy assigning to any rule infinite costs if the goal has no modality

Field Summary

Fields

Modifier and Type	Field and Description
private int	limit
private static Name	NAME
private static int	UNWIND_COST
private static java.util.Set<java.lang.String>	unwindRules

Constructor Summary

Constructors

Constructor and Description
TestGenStrategy(Strategy delegate)

Method Summary

Modifier and Type	Method and Description
RuleAppCost	computeCost(RuleApp app, PosInOccurrence pio, Goal goal) Evaluate the cost of a RuleApp.
private int	computeUnwindRules(Goal goal)
boolean	isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal) Re-Evaluate a RuleApp.
boolean	isStopAtFirstNonCloseableGoal() Checks if the Strategy should stop at the first non closeable Goal.
private static boolean	isUnwindRule(Rule rule)
Name	name() returns the name of this element

Methods inherited from class de.uka.ilkd.key.macros.FilterStrategy

instantiateApp

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

updateStrategySettings

Field Detail

NAME

private static final Name NAME

unwindRules

private static final java.util.Set<java.lang.String> unwindRules

UNWIND_COST

private static final int UNWIND_COST

See Also:

Constant Field Values

limit

private final int limit

Constructor Detail

TestGenStrategy

public TestGenStrategy(Strategy delegate)

Method Detail

isUnwindRule

private static boolean isUnwindRule(Rule rule)

computeCost

public RuleAppCost computeCost(RuleApp app,
                               PosInOccurrence pio,
                               Goal goal)

Description copied from interface: Feature

Evaluate the cost of a RuleApp.

Specified by:

computeCost in interface Feature

Overrides:

computeCost in class FilterStrategy

Parameters:

app - the RuleApp

pio - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

the cost of the rule application expressed as a RuleAppCost object. TopRuleAppCost.INSTANCE indicates that the rule shall not be applied at all (it is discarded by the strategy).

computeUnwindRules

private int computeUnwindRules(Goal goal)

isApprovedApp

public boolean isApprovedApp(RuleApp app,
                             PosInOccurrence pio,
                             Goal goal)

Description copied from interface: Strategy

Re-Evaluate a RuleApp. This method is called immediately before a rule is really applied

Specified by:

isApprovedApp in interface Strategy

Overrides:

isApprovedApp in class FilterStrategy

Returns:

true iff the rule should be applied, false otherwise

name

public Name name()

Description copied from interface: Named

returns the name of this element

Returns:

the name of the element

isStopAtFirstNonCloseableGoal

public boolean isStopAtFirstNonCloseableGoal()

Description copied from interface: Strategy

Checks if the Strategy should stop at the first non closeable Goal.

Returns:

true stop, false continue on other Goals.