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 and Description |
---|
StrategySettings() |
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.
|
private static final java.lang.String STRATEGY_KEY
private static final java.lang.String STEPS_KEY
private static final java.lang.String TIMEOUT_KEY
private final java.util.LinkedList<SettingsListener> listenerList
private Name activeStrategy
private int maxSteps
private long timeout
private StrategyProperties strategyProperties
private StopCondition customApplyStrategyStopCondition
StopCondition
which is used in an
ApplyStrategy
instance to determine after each applied rule
if more rules should be applied or not.private GoalChooser customApplyStrategyGoalChooser
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.public int getMaxSteps()
public void setMaxSteps(int mSteps)
mSteps
- maximal amount of heuristic stepspublic Name getStrategy()
public void setStrategy(Name name)
name
- public void readSettings(java.lang.Object sender, java.util.Properties props)
Settings
sender
is the object calling this method.readSettings
in interface Settings
public void writeSettings(java.lang.Object sender, java.util.Properties props)
Settings
writeSettings
in interface Settings
props
- the Properties object where to write the settings as (key, value) pair
sender
is the object calling this method.protected void fireSettingsChanged()
public void addSettingsListener(SettingsListener l)
addSettingsListener
in interface Settings
l
- the listenerpublic void removeSettingsListener(SettingsListener l)
public StrategyProperties getActiveStrategyProperties()
public void setActiveStrategyProperties(StrategyProperties p)
public long getTimeout()
public void setTimeout(long timeout)
timeout
- a long specifying the timeout in mspublic 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.
StopCondition
to use in an ApplyStrategy
instance.public StopCondition getCustomApplyStrategyStopCondition()
StopCondition
which is used in an
ApplyStrategy
to determine after each applied rule if more rules
should be applied or not.StopCondition
or null
if the default one should be used.public void setCustomApplyStrategyStopCondition(StopCondition customApplyStrategyStopCondition)
StopCondition
which is used in an
ApplyStrategy
to determine after each applied rule if more rules
should be applied or not.customApplyStrategyStopCondition
- The customized StopCondition
to use or null
to use the default one.public GoalChooser getCustomApplyStrategyGoalChooser()
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.GoalChooser
to use or null
to use the default one of the ApplyStrategy
.public void setCustomApplyStrategyGoalChooser(GoalChooser customGoalChooser)
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.customGoalChooser
- The customized GoalChooser
to use or null
to use the default one of the ApplyStrategy
.