de.uka.ilkd.key.settings

Class StrategySettings

java.lang.Object

de.uka.ilkd.key.settings.StrategySettings

All Implemented Interfaces:

Settings, java.lang.Cloneable

public class StrategySettings
extends java.lang.Object
implements Settings, java.lang.Cloneable

Field Summary

Fields

Modifier and Type	Field and Description
private Name	activeStrategy
private GoalChooser	customApplyStrategyGoalChooser An optional customized GoalChooser which is used in an ApplyStrategy instance to select the next Goal to apply a rule on.
private StopCondition	customApplyStrategyStopCondition An optional customized StopCondition which is used in an ApplyStrategy instance to determine after each applied rule if more rules should be applied or not.
private java.util.LinkedList<SettingsListener>	listenerList
private int	maxSteps maximal number of automatic rule applications before an interaction is required
private static java.lang.String	STEPS_KEY
private static java.lang.String	STRATEGY_KEY
private StrategyProperties	strategyProperties
private long	timeout maximal time in ms after which automatic rule application is aborted
private static java.lang.String	TIMEOUT_KEY

Constructor Summary

Constructors

Constructor and Description
StrategySettings()

Method Summary

Modifier and Type	Method and Description
void	addSettingsListener(SettingsListener l) adds a listener to the settings object
protected void	fireSettingsChanged() sends the message that the state of this setting has been changed to its registered listeners (not thread-safe)
StrategyProperties	getActiveStrategyProperties() returns a shallow copy of the strategy properties
StopCondition	getApplyStrategyStopCondition() Returns the StopCondition to use in an ApplyStrategy instance to determine after each applied rule if more rules should be applied or not.
GoalChooser	getCustomApplyStrategyGoalChooser() Returns the customized GoalChooser which is used in an ApplyStrategy instance to select the next Goal to apply a rule on.
StopCondition	getCustomApplyStrategyStopCondition() Returns a customized StopCondition which is used in an ApplyStrategy to determine after each applied rule if more rules should be applied or not.
int	getMaxSteps() returns the maximal amount of heuristics steps before a user interaction is required
Name	getStrategy() Get the name of the active strategy
long	getTimeout() retrieves the time in ms after which automatic rule application shall be aborted (-1 disables timeout)
void	readSettings(java.lang.Object sender, java.util.Properties props) gets a Properties object and has to perform the necessary steps in order to change this object in a way that it represents the stored settings sender is the object calling this method.
void	removeSettingsListener(SettingsListener l)
void	setActiveStrategyProperties(StrategyProperties p) sets the strategy properties if different from current ones
void	setCustomApplyStrategyGoalChooser(GoalChooser customGoalChooser) Sets the customized GoalChooser which is used in an ApplyStrategy instance to select the next Goal to apply a rule on.
void	setCustomApplyStrategyStopCondition(StopCondition customApplyStrategyStopCondition) Defines the StopCondition which is used in an ApplyStrategy to determine after each applied rule if more rules should be applied or not.
void	setMaxSteps(int mSteps) sets the maximal amount of heuristic steps before a user interaction is required
void	setStrategy(Name name) Set the name of the active strategy
void	setTimeout(long timeout) sets the time after which automatic rule application shall be aborted (-1 disables timeout)
void	writeSettings(java.lang.Object sender, java.util.Properties props) The settings to store are written to the given Properties object.

Methods inherited from class java.lang.Object

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

Field Detail

STRATEGY_KEY

private static final java.lang.String STRATEGY_KEY

See Also:

Constant Field Values

STEPS_KEY

private static final java.lang.String STEPS_KEY

See Also:

Constant Field Values

TIMEOUT_KEY

private static final java.lang.String TIMEOUT_KEY

See Also:

Constant Field Values

listenerList

private final java.util.LinkedList<SettingsListener> listenerList

activeStrategy

private Name activeStrategy

maxSteps

private int maxSteps

maximal number of automatic rule applications before an interaction is required

timeout

private long timeout

maximal time in ms after which automatic rule application is aborted

strategyProperties

private StrategyProperties strategyProperties

customApplyStrategyStopCondition

private StopCondition customApplyStrategyStopCondition

An optional customized StopCondition which is used in an ApplyStrategy instance to determine after each applied rule if more rules should be applied or not.

customApplyStrategyGoalChooser

private GoalChooser customApplyStrategyGoalChooser

An optional customized GoalChooser which is used in an ApplyStrategy instance to select the next Goal to apply a rule on. If no one is defined the default one of the ApplyStrategy, which is defined by the user interface, is used.

Constructor Detail

StrategySettings

public StrategySettings()

Method Detail

getMaxSteps

public int getMaxSteps()

returns the maximal amount of heuristics steps before a user interaction is required

Returns:

the maximal amount of heuristics steps before a user interaction is required

setMaxSteps

public void setMaxSteps(int mSteps)

sets the maximal amount of heuristic steps before a user interaction is required

Parameters:

mSteps - maximal amount of heuristic steps

getStrategy

public Name getStrategy()

Get the name of the active strategy

Returns:

the name of the active strategy

setStrategy

public void setStrategy(Name name)

Set the name of the active strategy

Parameters:

name -

readSettings

public void readSettings(java.lang.Object sender,
                         java.util.Properties props)

Description copied from interface: Settings

gets a Properties object and has to perform the necessary steps in order to change this object in a way that it represents the stored settings sender is the object calling this method.

Specified by:

readSettings in interface Settings

writeSettings

public void writeSettings(java.lang.Object sender,
                          java.util.Properties props)

Description copied from interface: Settings

The settings to store are written to the given Properties object.

Specified by:

writeSettings in interface Settings

props - the Properties object where to write the settings as (key, value) pair sender is the object calling this method.

fireSettingsChanged

protected void fireSettingsChanged()

sends the message that the state of this setting has been changed to its registered listeners (not thread-safe)

addSettingsListener

public void addSettingsListener(SettingsListener l)

adds a listener to the settings object

Specified by:

addSettingsListener in interface Settings

Parameters:

l - the listener

removeSettingsListener

public void removeSettingsListener(SettingsListener l)

getActiveStrategyProperties

public StrategyProperties getActiveStrategyProperties()

returns a shallow copy of the strategy properties

setActiveStrategyProperties

public void setActiveStrategyProperties(StrategyProperties p)

sets the strategy properties if different from current ones

getTimeout

public long getTimeout()

retrieves the time in ms after which automatic rule application shall be aborted (-1 disables timeout)

Returns:

time in ms after which automatic rule application shall be aborted

setTimeout

public void setTimeout(long timeout)

sets the time after which automatic rule application shall be aborted (-1 disables timeout)

Parameters:

timeout - a long specifying the timeout in ms

getApplyStrategyStopCondition

public StopCondition getApplyStrategyStopCondition()

Returns the StopCondition to use in an ApplyStrategy instance to determine after each applied rule if more rules should be applied or not.

By default is an AppliedRuleStopCondition used which stops the auto mode if the given maximal number of rule applications or a defined timeout is reached. If a customized implementation is defined for the current proof via setCustomApplyStrategyStopCondition(StopCondition) this instance is returned instead.

Returns:

The StopCondition to use in an ApplyStrategy instance.

getCustomApplyStrategyStopCondition

public StopCondition getCustomApplyStrategyStopCondition()

Returns a customized StopCondition which is used in an ApplyStrategy to determine after each applied rule if more rules should be applied or not.

Returns:

The customized StopCondition or null if the default one should be used.

setCustomApplyStrategyStopCondition

public void setCustomApplyStrategyStopCondition(StopCondition customApplyStrategyStopCondition)

Defines the StopCondition which is used in an ApplyStrategy to determine after each applied rule if more rules should be applied or not.

Parameters:

customApplyStrategyStopCondition - The customized StopCondition to use or null to use the default one.

getCustomApplyStrategyGoalChooser

public GoalChooser getCustomApplyStrategyGoalChooser()

Returns the customized GoalChooser which is used in an ApplyStrategy instance to select the next Goal to apply a rule on. If no one is defined the default one of the ApplyStrategy, which is defined by the user interface, is used.

Returns:

The customized GoalChooser to use or null to use the default one of the ApplyStrategy.

setCustomApplyStrategyGoalChooser

public void setCustomApplyStrategyGoalChooser(GoalChooser customGoalChooser)

Sets the customized GoalChooser which is used in an ApplyStrategy instance to select the next Goal to apply a rule on. If no one is defined the default one of the ApplyStrategy, which is defined by the user interface, is used.

Parameters:

customGoalChooser - The customized GoalChooser to use or null to use the default one of the ApplyStrategy.