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: /*
012:
013: Uses code by Hans Muller and Kathy Walrath from
014: http://java.sun.com/products/jfc/tsc/articles/threads/threads2.html
015:
016: */
017:
018: package de.uka.ilkd.key.gui;
019:
020: import java.io.File;
021: import java.io.FileWriter;
022: import java.io.IOException;
023: import java.io.PrintWriter;
024: import java.util.ArrayList;
025: import java.util.List;
026:
027: import de.uka.ilkd.key.gui.notification.events.GeneralFailureEvent;
028: import de.uka.ilkd.key.proof.*;
029: import de.uka.ilkd.key.proof.proofevent.IteratorOfNodeReplacement;
030: import de.uka.ilkd.key.proof.proofevent.RuleAppInfo;
031: import de.uka.ilkd.key.proof.reuse.ReusePoint;
032: import de.uka.ilkd.key.rule.RuleApp;
033: import de.uka.ilkd.key.util.Debug;
034:
035: /**
036: * Applies rules in an automated fashion in a separate thread.
037: */
038: public class ApplyStrategy {
039:
040: private static final String PROCESSING_STRATEGY = "Processing Strategy";
041:
042: private KeYMediator medi;
043: /** the proof that is worked with */
044: private Proof proof;
045: /** the maximum of allowed rule applications */
046: private int maxApplications;
047:
048: /** chooses goals to which rules are applied*/
049: private IGoalChooser goalChooser;
050:
051: private SwingWorker worker;
052:
053: /** number of rules automatically applied */
054: private int countApplied = 0;
055: private long time;
056:
057: /** interrupted by the user? */
058: private boolean autoModeActive = false;
059:
060: private ProofListener proofListener = new ProofListener();
061:
062: private boolean startedAsInteractive;
063:
064: private List proverTaskObservers = new ArrayList();
065:
066: private ReusePoint reusePoint;
067:
068: /** time in ms after which rule application shall be aborted, -1 disables timeout */
069: private long timeout = -1;
070:
071: // Please create this object beforehand and re-use it.
072: // Otherwise the addition/removal of the InteractiveProofListener
073: // can cause a ConcurrentModificationException during ongoing operation
074: public ApplyStrategy(KeYMediator medi) {
075: this .medi = medi;
076: medi.addRuleAppListener(proofListener);
077: this .goalChooser = medi.getProfile()
078: .getSelectedGoalChooserBuilder().create();
079: }
080:
081: /** applies rules that are chosen by the active strategy
082: * @return true iff a rule has been applied, false otherwise
083: */
084: private synchronized boolean applyAutomaticRule() {
085: // Look for the strategy ...
086: RuleApp app = null;
087: Goal g;
088: ReuseListener rl = mediator().getReuseListener();
089:
090: if (reusePoint != null) {
091: g = reusePoint.target();
092: app = reusePoint.getReuseApp();
093: g.node().setReuseSource(reusePoint);
094: rl.removeRPConsumedMarker(reusePoint.source());
095: rl.removeRPConsumedGoal(g);
096: ListOfGoal goalList = g.apply(app);
097: rl.addRPOldMarkersNewGoals(goalList);
098: rl.addRPNewMarkersAllGoals(reusePoint.source());
099: } else {
100: while ((g = goalChooser.getNextGoal()) != null) {
101:
102: app = g.getRuleAppManager().next();
103:
104: if (app == null)
105: goalChooser.removeGoal(g);
106: else
107: break;
108: }
109: if (app == null)
110: return false;
111: rl.removeRPConsumedGoal(g);
112: rl.addRPOldMarkersNewGoals(g.apply(app));
113: }
114:
115: if (rl.reusePossible())
116: reusePoint = rl.getBestReusePoint();
117: else
118: reusePoint = null;
119:
120: return true;
121: }
122:
123: /**
124: * applies rules until this is no longer
125: * possible or the thread is interrupted.
126: */
127: Object doWork() {
128: time = System.currentTimeMillis();
129: try {
130: Debug.out("Strategy started.");
131: while (!maxRuleApplicationOrTimeoutExceeded()) {
132: if (!applyAutomaticRule()) {
133: // no more rules applicable
134: break;
135: }
136: countApplied++;
137: fireTaskProgress();
138: if (Thread.interrupted())
139: throw new InterruptedException();
140: }
141: } catch (InterruptedException e) {
142: return "Interrupted"; // SwingWorker.get() returns this
143: } catch (Throwable t) { // treated later in finished()
144: System.err.println(t);
145: t.printStackTrace();
146: return "Error";
147: } finally {
148: time = System.currentTimeMillis() - time;
149: Debug.out("Strategy stopped.");
150: Debug.out("Applied ", countApplied);
151: Debug.out("Time elapsed: ", time);
152: }
153: return "Done.";
154: }
155:
156: /**
157: * returns if the maximum number of rule applications or
158: * the timeout has been reached
159: * @return true if automatic rule application shall be stopped because the maximal
160: * number of rules have been applied or the time out has been reached
161: */
162: private boolean maxRuleApplicationOrTimeoutExceeded() {
163: return countApplied >= maxApplications || timeout >= 0 ? System
164: .currentTimeMillis()
165: - time >= timeout : false;
166: }
167:
168: private synchronized void fireTaskStarted() {
169: for (int i = 0, sz = proverTaskObservers.size(); i < sz; i++) {
170: ((ProverTaskListener) proverTaskObservers.get(i))
171: .taskStarted(PROCESSING_STRATEGY, maxApplications);
172: }
173: }
174:
175: private synchronized void fireTaskProgress() {
176: for (int i = 0, sz = proverTaskObservers.size(); i < sz; i++) {
177: ((ProverTaskListener) proverTaskObservers.get(i))
178: .taskProgress(countApplied);
179: }
180: }
181:
182: private synchronized void fireTaskFinished() {
183: for (int i = 0, sz = proverTaskObservers.size(); i < sz; i++) {
184: ((ProverTaskListener) proverTaskObservers.get(i))
185: .taskFinished();
186: }
187: }
188:
189: private void init(ListOfGoal goals, int maxSteps, long timeout) {
190: proof = medi.getProof();
191: maxApplications = maxSteps;
192: this .timeout = timeout;
193: countApplied = 0;
194: goalChooser.init(proof, goals);
195: setAutoModeActive(true);
196: startedAsInteractive = !mediator().autoMode();
197: if (startedAsInteractive) {
198: mediator().stopInterface(true);
199: }
200: mediator().setInteractive(false);
201: fireTaskStarted();
202: }
203:
204: private KeYMediator mediator() {
205: return medi;
206: }
207:
208: public void start(ListOfGoal goals, int maxSteps, long timeout) {
209: init(goals, maxSteps, timeout);
210:
211: worker = new AutoModeWorker();
212: worker.start();
213: }
214:
215: /**
216: * Called by the "Stop" button, interrupts the worker thread
217: * which is running this.doWork(). Note that the doWork()
218: * method handles InterruptedExceptions cleanly.
219: */
220: public void stop() {
221: worker.interrupt();
222: }
223:
224: private void displayResults(Main main, String timeString) {
225: String message;
226: int closed = mediator().getNrGoalsClosedByAutoMode();
227:
228: // display message in the status bar
229:
230: if (countApplied != 0) {
231: message = "Strategy: Applied " + countApplied + " rule";
232: if (countApplied != 1)
233: message += "s";
234: message += " (" + timeString + " sec), ";
235: message += " closed " + closed + " goal";
236: if (closed != 1)
237: message += "s";
238: message += ", " + main.displayedOpenGoalNumber();
239: message += " remaining";
240: main.setStatusLine(message);
241: }
242:
243: mediator().resetNrGoalsClosedByHeuristics();
244: }
245:
246: private void finishedBatchMode(Object result) {
247:
248: if (Main.statisticsFile != null)
249: printStatistics(Main.statisticsFile, result);
250:
251: if ("Error".equals(result)) {
252: // Error in batchMode. Terminate with status -1.
253: System.exit(-1);
254: }
255:
256: // Save the proof before exit.
257:
258: String baseName = Main.fileNameOnStartUp;
259: int idx = baseName.indexOf(".key");
260: if (idx == -1) {
261: idx = baseName.indexOf(".proof");
262: }
263: baseName = baseName.substring(0, idx == -1 ? baseName.length()
264: : idx);
265:
266: File f;
267: int counter = 0;
268: do {
269:
270: f = new File(baseName + ".auto." + counter + ".proof");
271: counter++;
272: } while (f.exists());
273:
274: Main.getInstance().saveProof(f.getAbsolutePath());
275: if (proof.openGoals().size() == 0) {
276: // Says that all Proofs have succeeded
277: if (proof.getBasicTask().getStatus()
278: .getProofClosedButLemmasLeft()) {
279: // Says that the proof is closed by depends on (unproved) lemmas
280: System.exit(2);
281: }
282: System.exit(0);
283: } else {
284: // Says that there is at least one open Proof
285: System.exit(1);
286: }
287: }
288:
289: private void printStatistics(String file, Object result) {
290: try {
291: final FileWriter statistics = new FileWriter(file, true);
292: final PrintWriter statPrinter = new PrintWriter(statistics);
293:
294: String fileName = Main.fileNameOnStartUp;
295: final int slashIndex = fileName.lastIndexOf("examples/");
296: if (slashIndex >= 0)
297: fileName = fileName.substring(slashIndex);
298:
299: statPrinter.print(fileName + ", ");
300: if ("Error".equals(result))
301: statPrinter.println("-1, -1");
302: else
303: statPrinter.println("" + countApplied + ", " + time);
304: statPrinter.close();
305: } catch (IOException e) {
306: }
307: }
308:
309: public synchronized void addProverTaskObserver(
310: ProverTaskListener observer) {
311: proverTaskObservers.add(observer);
312: }
313:
314: public synchronized void removeProverTaskObserver(
315: ProverTaskListener observer) {
316: proverTaskObservers.remove(observer);
317: }
318:
319: /* Invoking start() on the SwingWorker causes a new Thread
320: * to be created that will call construct(), and then
321: * finished(). Note that finished() is called even if
322: * the worker is interrupted because we catch the
323: * InterruptedException in doWork().
324: */
325: private class AutoModeWorker extends SwingWorker {
326:
327: public Object construct() {
328: Object res = doWork();
329: return res;
330: }
331:
332: public void finished() {
333: setAutoModeActive(false);
334: fireTaskFinished();
335: String timeString = "" + (time / 1000) + "."
336: + ((time % 1000) / 100);
337:
338: final Object result = get();
339:
340: if (Main.batchMode) {
341: // This method does not return.
342: finishedBatchMode(result);
343: Debug.fail("Control flow should not reach this point.");
344: }
345:
346: if ("Error".equals(result)) {
347: mediator().startInterface(true);
348: mediator().notify(
349: new GeneralFailureEvent(
350: "An exception occurred during"
351: + " strategy execution."));
352: } else {
353: if (startedAsInteractive)
354: mediator().startInterface(true);
355: }
356:
357: mediator().setInteractive(true);
358: displayResults(Main.getInstance(), timeString);
359: }
360: }
361:
362: private class ProofListener implements RuleAppListener {
363:
364: /** invoked when a rule has been applied */
365: public void ruleApplied(ProofEvent e) {
366: if (!isAutoModeActive())
367: return;
368: RuleAppInfo rai = e.getRuleAppInfo();
369: if (rai == null)
370: return;
371:
372: synchronized (ApplyStrategy.this ) {
373: ListOfGoal newGoals = SLListOfGoal.EMPTY_LIST;
374: IteratorOfNodeReplacement it = rai
375: .getReplacementNodes();
376: Node node;
377: Goal goal;
378:
379: while (it.hasNext()) {
380: node = it.next().getNode();
381: goal = proof.getGoal(node);
382: if (goal != null)
383: newGoals = newGoals.prepend(goal);
384: }
385:
386: goalChooser.updateGoalList(rai.getOriginalNode(),
387: newGoals);
388: }
389: }
390:
391: }
392:
393: public boolean isAutoModeActive() {
394: return autoModeActive;
395: }
396:
397: public void setAutoModeActive(boolean autoModeActive) {
398: this.autoModeActive = autoModeActive;
399: }
400:
401: }
|