001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.gui.configuration;
012:
013: import java.util.Iterator;
014: import java.util.LinkedList;
015: import java.util.Properties;
016:
017: import de.uka.ilkd.key.gui.GUIEvent;
018: import de.uka.ilkd.key.logic.Name;
019: import de.uka.ilkd.key.strategy.SimpleJavaCardDLOptions;
020: import de.uka.ilkd.key.strategy.StrategyProperties;
021: import de.uka.ilkd.key.util.Debug;
022:
023: public class StrategySettings implements Settings {
024:
025: private static final String STRATEGY_KEY = "[Strategy]ActiveStrategy";
026: private static final String STEPS_KEY = "[Strategy]MaximumNumberOfAutomaticApplications";
027: private static final String TIMEOUT_KEY = "[Strategy]Timeout";
028:
029: private LinkedList listenerList = new LinkedList();
030:
031: private Name activeStrategy;
032:
033: /** maximal number of automatic rule applications before an interaction is required */
034: private int maxSteps = -1;
035:
036: /** maximal time in ms after which automatic rule application is aborted */
037: private long timeout = -1;
038:
039: private StrategyProperties strategyProperties = new StrategyProperties();
040:
041: /** returns the maximal amount of heuristics steps before an user
042: * interaction is required
043: * @return the maximal amount of heuristics steps before an user
044: * interaction is required
045: */
046: public int getMaxSteps() {
047: return maxSteps;
048: }
049:
050: /** sets the maximal amount of heuristic steps before a user
051: * interaction is required
052: * @param mSteps maximal amount of heuristic steps
053: */
054: public void setMaxSteps(int mSteps) {
055: if (maxSteps != mSteps) {
056: maxSteps = mSteps;
057: fireSettingsChanged();
058: }
059: }
060:
061: /**
062: * Get the name of the active strategy
063: * @return the name of the active strategy
064: */
065: public Name getStrategy() {
066: return activeStrategy;
067: }
068:
069: /**
070: * Set the name of the active strategy
071: * @param name
072: */
073: public void setStrategy(Name name) {
074: if (!name.equals(activeStrategy)) {
075: activeStrategy = name;
076: fireSettingsChanged();
077: }
078: }
079:
080: /* (non-Javadoc)
081: * @see de.uka.ilkd.key.gui.Settings#readSettings(java.util.Properties)
082: */
083: public void readSettings(Properties props) {
084: String numString = props.getProperty(STEPS_KEY);
085: String strategyString = props.getProperty(STRATEGY_KEY);
086: String timeoutString = props.getProperty(TIMEOUT_KEY);
087:
088: long localTimeout = -1;
089: int numSteps = 1000;
090:
091: if (numString != null) {
092: try {
093: numSteps = Integer.parseInt(numString);
094: } catch (NumberFormatException e) {
095: Debug
096: .out(
097: "StrategySettings: failure while converting the string "
098: + "with the allowed steps of heuristics applications to int."
099: + "Use default value 1000 instead."
100: + "\nThe String that has been tried to convert was",
101: numString);
102: }
103: }
104:
105: if (timeoutString != null) {
106: try {
107: localTimeout = Long.parseLong(timeoutString);
108: } catch (NumberFormatException e) {
109: Debug
110: .out(
111: "StrategySettings: failure while converting the string "
112: + "with rule application timeout. "
113: + "\nThe String that has been tried to convert was",
114: timeoutString);
115: }
116: }
117:
118: // set active strategy
119: if (strategyString != null) {
120: activeStrategy = new Name(strategyString);
121: }
122:
123: // set strategy options
124: strategyProperties = StrategyProperties.read(props);
125:
126: // set max steps
127: maxSteps = numSteps;
128:
129: // set time out
130: this .timeout = localTimeout;
131: }
132:
133: /* (non-Javadoc)
134: * @see de.uka.ilkd.key.gui.Settings#writeSettings(java.util.Properties)
135: */
136: public void writeSettings(Properties props) {
137: if (getStrategy() == null) {
138: setStrategy(SimpleJavaCardDLOptions.LOOPS_METHODS.name());
139: }
140: if (maxSteps < 0) {
141: setMaxSteps(1000);
142: }
143: props.setProperty(STRATEGY_KEY, getStrategy().toString());
144: props.setProperty(STEPS_KEY, String.valueOf(getMaxSteps()));
145:
146: props.setProperty(TIMEOUT_KEY, String.valueOf(getTimeout()));
147: strategyProperties.write(props);
148: }
149:
150: /** sends the message that the state of this setting has been
151: * changed to its registered listeners (not thread-safe)
152: */
153: protected void fireSettingsChanged() {
154: Iterator it = listenerList.iterator();
155: while (it.hasNext()) {
156: ((SettingsListener) it.next())
157: .settingsChanged(new GUIEvent(this ));
158: }
159: }
160:
161: /** adds a listener to the settings object
162: * @param l the listener
163: */
164: public void addSettingsListener(SettingsListener l) {
165: listenerList.add(l);
166: }
167:
168: public void removeSettingsListener(SettingsListener l) {
169: listenerList.remove(l);
170: }
171:
172: /**
173: * returns a shallow copy of the strategy properties
174: */
175: public StrategyProperties getActiveStrategyProperties() {
176: return (StrategyProperties) strategyProperties.clone();
177: }
178:
179: /**
180: * sets the strategy properties if different from current ones
181: */
182: public void setActiveStrategyProperties(StrategyProperties p) {
183: if (!p.equals(strategyProperties)) {
184: this .strategyProperties = (StrategyProperties) p.clone();
185: fireSettingsChanged();
186: }
187: }
188:
189: /**
190: * retrieves the time in ms after which automatic rule application shall be aborted
191: * (-1 disables timeout)
192: * @return time in ms after which automatic rule application shall be aborted
193: */
194: public long getTimeout() {
195: return timeout;
196: }
197:
198: /**
199: * sets the time after which automatic rule application shall be aborted
200: * (-1 disables timeout)
201: * @param timeout a long specifying the timeout in ms
202: */
203: public void setTimeout(long timeout) {
204: if (timeout != this.timeout) {
205: this.timeout = timeout;
206: fireSettingsChanged();
207: }
208: }
209: }
|