de.uka.ilkd.key.strategy

Class FIFOStrategy

java.lang.Object

de.uka.ilkd.key.strategy.FIFOStrategy

All Implemented Interfaces:

Named, Feature, Strategy

public class FIFOStrategy
extends java.lang.Object
implements Strategy

Trivial implementation of the Strategy interface that uses only the goal time to determine the cost of a RuleApp.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	FIFOStrategy.Factory

Field Summary

Fields

Modifier and Type	Field and Description
static Strategy	INSTANCE
private static Name	NAME

Constructor Summary

Constructors

Modifier	Constructor and Description
private	FIFOStrategy()

Method Summary

Modifier and Type	Method and Description
RuleAppCost	computeCost(RuleApp app, PosInOccurrence pio, Goal goal) Evaluate the cost of a RuleApp.
void	instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal, RuleAppCostCollector collector) Instantiate an incomplete RuleApp.
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.
Name	name() returns the name of this element

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

INSTANCE

public static Strategy INSTANCE

Constructor Detail

FIFOStrategy

private FIFOStrategy()

Method Detail

computeCost

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

Evaluate the cost of a RuleApp.

Specified by:

computeCost in interface Feature

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

isApprovedApp

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

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

Specified by:

isApprovedApp in interface Strategy

Returns:

true iff the rule should be applied, false otherwise

instantiateApp

public void instantiateApp(RuleApp app,
                           PosInOccurrence pio,
                           Goal goal,
                           RuleAppCostCollector collector)

Description copied from interface: Strategy

Instantiate an incomplete RuleApp. This method is called when the AutomatedRuleApplicationManager comes across a rule application in which some schema variables are not yet instantiated, or which is in some other way incomplete. The strategy then has the opportunity to return/provide a list of (more) complete rule applications by feeding them into the provided RuleAppCostCollector.

Specified by:

instantiateApp in interface Strategy

name

public Name name()

Description copied from interface: Named

returns the name of this element

Specified by:

name in interface Named

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.

Specified by:

isStopAtFirstNonCloseableGoal in interface Strategy

Returns:

true stop, false continue on other Goals.