de.uka.ilkd.key.strategy.definition

Class StrategySettingsDefinition

java.lang.Object

de.uka.ilkd.key.strategy.definition.StrategySettingsDefinition

public class StrategySettingsDefinition
extends java.lang.Object

Instances of this class defines how a user interfaces has to look like which edits StrategySettings.

The StrategySettingsDefinition itself and all its provided sub classes are read-only.

Each StrategyFactory should provide an instance of this class to define the user interface which the user can use to edit supported StrategySettings in created Strategy instances. If a StrategyFactory provides no StrategySettingsDefinition an empty user interface or even bedder an error message should be shown to the user.

Author:

Martin Hentschel

See Also:

StrategyFactory, AbstractStrategyPropertyDefinition, OneOfStrategyPropertyDefinition, StrategyPropertyValueDefinition

Field Summary

Fields

Modifier and Type	Field and Description
private int	defaultMaxRuleApplications The default maximal rule applications.
private IDefaultStrategyPropertiesFactory	defaultPropertiesFactory The IDefaultStrategyPropertiesFactory used to create default StrategyProperties.
private java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>>	furtherDefaults Further default settings, for example suitable for simplification.
private java.lang.String	maxRuleApplicationsLabel The label shown in front of the control to edit StrategySettings.getMaxSteps().
private ImmutableArray<AbstractStrategyPropertyDefinition>	properties Defines the controls to edit StrategyProperties.
private java.lang.String	propertiesTitle The label shown in front of the controls to edit StrategyProperties.
private boolean	showMaxRuleApplications Defines if a user interface control is shown to edit StrategySettings.getMaxSteps().
private static java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>>	STD_FURTHER_DEFAULTS

Constructor Summary

Constructors

Constructor and Description
StrategySettingsDefinition(boolean showMaxRuleApplications, java.lang.String maxRuleApplicationsLabel, int defaultMaxRuleApplications, java.lang.String propertiesTitle, IDefaultStrategyPropertiesFactory defaultPropertiesFactory, java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>> furtherDefaults, AbstractStrategyPropertyDefinition... properties) Constructor.
StrategySettingsDefinition(java.lang.String propertiesTitle, AbstractStrategyPropertyDefinition... properties) Constructor.

Method Summary

Modifier and Type	Method and Description
int	getDefaultMaxRuleApplications() Returns the default maximal rule applications.
IDefaultStrategyPropertiesFactory	getDefaultPropertiesFactory() Returns the IDefaultStrategyPropertiesFactory used to create default StrategyProperties.
java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>>	getFurtherDefaults()
java.lang.String	getMaxRuleApplicationsLabel() Returns the label shown in front of the control to edit StrategySettings.getMaxSteps().
ImmutableArray<AbstractStrategyPropertyDefinition>	getProperties() Returns the definition of controls to edit StrategyProperties.
java.lang.String	getPropertiesTitle() Returns the label shown in front of the controls to edit StrategyProperties.
boolean	isShowMaxRuleApplications() Checks if the user interface control to edit StrategySettings.getMaxSteps() should be shown or not.

Methods inherited from class java.lang.Object

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

Field Detail

STD_FURTHER_DEFAULTS

private static final java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>> STD_FURTHER_DEFAULTS

showMaxRuleApplications

private final boolean showMaxRuleApplications

Defines if a user interface control is shown to edit StrategySettings.getMaxSteps().

maxRuleApplicationsLabel

private final java.lang.String maxRuleApplicationsLabel

The label shown in front of the control to edit StrategySettings.getMaxSteps().

propertiesTitle

private final java.lang.String propertiesTitle

The label shown in front of the controls to edit StrategyProperties.

properties

private final ImmutableArray<AbstractStrategyPropertyDefinition> properties

Defines the controls to edit StrategyProperties.

defaultMaxRuleApplications

private final int defaultMaxRuleApplications

The default maximal rule applications.

defaultPropertiesFactory

private final IDefaultStrategyPropertiesFactory defaultPropertiesFactory

The IDefaultStrategyPropertiesFactory used to create default StrategyProperties.

furtherDefaults

private final java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>> furtherDefaults

Further default settings, for example suitable for simplification. Consists of triples (DEFAULT_NAME, MAX_RULE_APPS, PROPERTIES).

Constructor Detail

StrategySettingsDefinition

public StrategySettingsDefinition(java.lang.String propertiesTitle,
                                  AbstractStrategyPropertyDefinition... properties)

Constructor.

Parameters:

propertiesTitle - The label shown in front of the controls to edit StrategyProperties.

properties - Defines the controls to edit StrategyProperties.

StrategySettingsDefinition

public StrategySettingsDefinition(boolean showMaxRuleApplications,
                                  java.lang.String maxRuleApplicationsLabel,
                                  int defaultMaxRuleApplications,
                                  java.lang.String propertiesTitle,
                                  IDefaultStrategyPropertiesFactory defaultPropertiesFactory,
                                  java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>> furtherDefaults,
                                  AbstractStrategyPropertyDefinition... properties)

Constructor.

Parameters:

showMaxRuleApplications - Defines if a user interface control is shown to edit StrategySettings.getMaxSteps().

maxRuleApplicationsLabel - The label shown in front of the control to edit StrategySettings.getMaxSteps().

defaultMaxRuleApplications - The default maximal rule applications.

propertiesTitle - The label shown in front of the controls to edit StrategyProperties.

defaultPropertiesFactory - The IDefaultStrategyPropertiesFactory used to create default StrategyProperties.

furtherDefaults - further defaults used to create default StrategyProperties.

properties - Defines the controls to edit StrategyProperties.

Method Detail

isShowMaxRuleApplications

public boolean isShowMaxRuleApplications()

Checks if the user interface control to edit StrategySettings.getMaxSteps() should be shown or not.

Returns:

true show control, false do not provide a control.

getMaxRuleApplicationsLabel

public java.lang.String getMaxRuleApplicationsLabel()

Returns the label shown in front of the control to edit StrategySettings.getMaxSteps().

Returns:

The label shown in front of the control to edit StrategySettings.getMaxSteps() or null if no label should be shown.

getPropertiesTitle

public java.lang.String getPropertiesTitle()

Returns the label shown in front of the controls to edit StrategyProperties.

Returns:

The label shown in front of the controls to edit StrategyProperties or null if no label should be shown.

getProperties

public ImmutableArray<AbstractStrategyPropertyDefinition> getProperties()

Returns the definition of controls to edit StrategyProperties.

Returns:

The definition of controls to edit StrategyProperties.

getDefaultMaxRuleApplications

public int getDefaultMaxRuleApplications()

Returns the default maximal rule applications.

Returns:

The default maximal rule applications.

getDefaultPropertiesFactory

public IDefaultStrategyPropertiesFactory getDefaultPropertiesFactory()

Returns the IDefaultStrategyPropertiesFactory used to create default StrategyProperties.

Returns:

The IDefaultStrategyPropertiesFactory used to create default StrategyProperties.

getFurtherDefaults

public java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>> getFurtherDefaults()

Returns:

Further default settings, e.g. for simplification.