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;
012:
013: import java.awt.*;
014: import java.awt.event.*;
015: import java.beans.PropertyChangeEvent;
016: import java.beans.PropertyChangeListener;
017:
018: import javax.swing.*;
019: import javax.swing.border.Border;
020: import javax.swing.border.EtchedBorder;
021: import javax.swing.event.ChangeEvent;
022: import javax.swing.event.ChangeListener;
023:
024: import de.uka.ilkd.key.gui.configuration.ProofSettings;
025: import de.uka.ilkd.key.proof.Proof;
026: import de.uka.ilkd.key.strategy.*;
027:
028: public class StrategySelectionView extends JPanel {
029:
030: final JRadioButtonHashMap bSimpleFOLStrategy = new JRadioButtonHashMap(
031: "FOL", "FOLStrategy", false, false);
032: final JRadioButtonHashMap bSimpleJavaCardDLStrategy = new JRadioButtonHashMap(
033: "Java DL", "JavaCardDLStrategy", false, false);
034: final JRadioButtonHashMap bSimplificationOfOCLStrategy = new JRadioButtonHashMap(
035: "OCL simplification", "SimplificationOfOCLStrategy", false,
036: false);
037: final JRadioButtonHashMap bComputeSpecificationStrategy = new JRadioButtonHashMap(
038: "Specification extraction", "ComputeSpecificationStrategy",
039: false, false);
040: final JRadioButtonHashMap bVBTStrategy = new JRadioButtonHashMap(
041: "VBT Strategy", "VBTStrategy", false, false);
042: final JRadioButtonHashMap bDebuggerStrategy = new JRadioButtonHashMap(
043: "Debugger Strategy", "DebuggerStrategy", false, false);
044:
045: ButtonGroup stratGroup = new ButtonGroup();
046: ButtonGroup splittingGroup = new ButtonGroup();
047: ButtonGroup loopGroup = new ButtonGroup();
048: ButtonGroup methodGroup = new ButtonGroup();
049: ButtonGroup queryGroup = new ButtonGroup();
050: ButtonGroup nonLinArithGroup = new ButtonGroup();
051: ButtonGroup quantifierGroup = new ButtonGroup();
052: ButtonGroup[] userTacletsGroup = new ButtonGroup[StrategyProperties.USER_TACLETS_NUM];
053: {
054: for (int i = 0; i < StrategyProperties.USER_TACLETS_NUM; ++i)
055: userTacletsGroup[i] = new ButtonGroup();
056: }
057: JRadioButtonHashMap rdBut9;
058: JRadioButtonHashMap rdBut10;
059: JRadioButtonHashMap rdBut11;
060: JRadioButtonHashMap rdBut12;
061: JRadioButtonHashMap rdBut13;
062: JRadioButtonHashMap rdBut14;
063: private JRadioButtonHashMap splittingNormal;
064: private JRadioButtonHashMap splittingOff;
065: private JRadioButtonHashMap splittingDelayed;
066: private JRadioButtonHashMap queryNone;
067: private JRadioButtonHashMap queryExpand;
068: private JRadioButtonHashMap queryProgramsToRight;
069: private JRadioButtonHashMap nonLinArithNone;
070: private JRadioButtonHashMap nonLinArithDefOps;
071: private JRadioButtonHashMap nonLinArithCompletion;
072: private JRadioButtonHashMap quantifierNone;
073: private JRadioButtonHashMap quantifierNonSplitting;
074: private JRadioButtonHashMap quantifierNonSplittingWithProgs;
075: private JRadioButtonHashMap quantifierInstantiate;
076:
077: private KeYMediator mediator;
078:
079: private TimeoutSpinner timeoutSpinner;
080:
081: JPanel javaDLOptionsPanel = new JPanel() {
082:
083: public void setEnabled(boolean enabled) {
084: super .setEnabled(enabled);
085: setChildrenEnabled(this , enabled);
086: }
087:
088: private void setChildrenEnabled(Container container,
089: boolean enabled) {
090: for (int i = 0; i < container.getComponentCount(); i++) {
091: Component comp = container.getComponent(i);
092: comp.setEnabled(enabled);
093: if (comp instanceof Container)
094: setChildrenEnabled((Container) comp, enabled);
095: }
096: }
097: };
098:
099: JScrollPane javaDLOptionsScrollPane = new JScrollPane(
100: javaDLOptionsPanel,
101: JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED,
102: JScrollPane.HORIZONTAL_SCROLLBAR_NEVER);
103:
104: Border loweredetched =
105: // BorderFactory.createEtchedBorder(EtchedBorder.LOWERED);
106: BorderFactory.createEmptyBorder();
107:
108: public StrategySelectionView() {
109: layoutPane();
110: refresh(mediator == null ? null : mediator.getSelectedProof());
111: setVisible(true);
112: addComponentListener(new java.awt.event.ComponentAdapter() {
113: public void componentShown(java.awt.event.ComponentEvent e) {
114: maxSlider.refresh();
115: timeoutSpinner.refresh();
116: }
117: });
118: }
119:
120: /** Build everything */
121: private void layoutPane() {
122: final JavaDLOptionListener javaDLOptionListener = new JavaDLOptionListener();
123: bSimpleJavaCardDLStrategy.addPropertyChangeListener("enabled",
124: javaDLOptionListener);
125: bSimpleJavaCardDLStrategy.addItemListener(javaDLOptionListener);
126: javaDLOptionsPanel.setEnabled(false);
127:
128: StratListener stratListener = new StratListener();
129: OptListener optListener = new OptListener();
130:
131: this .setLayout(new BoxLayout(this , BoxLayout.Y_AXIS));
132:
133: javaDLOptionsScrollPane.setBorder(BorderFactory
134: .createTitledBorder("Java DL Options"));
135: GridBagConstraints gbcpanel5 = new GridBagConstraints();
136: final GridBagLayout javaDLOptionsLayout = new GridBagLayout();
137: javaDLOptionsPanel.setLayout(javaDLOptionsLayout);
138:
139: javaDLOptionsScrollPane.getVerticalScrollBar()
140: .setUnitIncrement(10);
141:
142: // javaDLOptionsPanel.setBorder(BorderFactory.createEmptyBorder());
143:
144: ////////////////////////////////////////////////////////////////////////
145:
146: int yCoord = 0;
147:
148: addJavaDLOption(new JLabel("Logical splitting"),
149: javaDLOptionsLayout, 1, yCoord, 7);
150:
151: // JPanel splittingPanel = new JPanel();
152: // splittingPanel.setBorder(BorderFactory.createTitledBorder(
153: // loweredetched, "Logical Splitting"));
154: // javaDLOptionsPanel.add(splittingPanel);
155:
156: ++yCoord;
157:
158: splittingNormal = new JRadioButtonHashMap("Normal",
159: StrategyProperties.SPLITTING_NORMAL, true, false);
160: splittingGroup.add(splittingNormal);
161: addJavaDLOption(splittingNormal, javaDLOptionsLayout, 2,
162: yCoord, 2);
163:
164: splittingDelayed = new JRadioButtonHashMap("Delayed",
165: StrategyProperties.SPLITTING_DELAYED, true, false);
166: splittingDelayed
167: .setToolTipText("<html>"
168: + "Do not split formulas (if-then-else expressions,<br>"
169: + "disjunctions in the antecedent, conjunctions in<br>"
170: + "the succedent) as long as programs are present in<br>"
171: + "the sequent.<br>"
172: + "NB: This does not affect the splitting of formulas<br>"
173: + "that themselves contain programs.<br>"
174: + "NB2: Delaying splits often prevents KeY from finding<br>"
175: + "short proofs, but in some cases it can significantly<br>"
176: + "improve the performance." + "</html>");
177: splittingGroup.add(splittingDelayed);
178: addJavaDLOption(splittingDelayed, javaDLOptionsLayout, 4,
179: yCoord, 2);
180:
181: splittingOff = new JRadioButtonHashMap("Off",
182: StrategyProperties.SPLITTING_OFF, true, false);
183: splittingOff
184: .setToolTipText("<html>"
185: + "Do never split formulas (if-then-else expressions,<br>"
186: + "disjunctions in the antecedent, conjunctions in<br>"
187: + "the succedent).<br>"
188: + "NB: This does not affect the splitting of formulas<br>"
189: + "that contain programs.<br>"
190: + "NB2: Without splitting, KeY is often unable to find<br>"
191: + "proofs even for simple problems. This option can,<br>"
192: + "nevertheless, be meaningful to keep the complexity<br>"
193: + "of proofs small and support interactive proving."
194: + "</html>");
195: splittingGroup.add(splittingOff);
196: addJavaDLOption(splittingOff, javaDLOptionsLayout, 6, yCoord, 2);
197:
198: ++yCoord;
199: addJavaDLOptionSpace(javaDLOptionsLayout, yCoord);
200:
201: ////////////////////////////////////////////////////////////////////////
202:
203: ++yCoord;
204:
205: addJavaDLOption(new JLabel("Loop treatment"),
206: javaDLOptionsLayout, 1, yCoord, 7);
207:
208: ++yCoord;
209:
210: rdBut9 = new JRadioButtonHashMap("Expand",
211: StrategyProperties.LOOP_EXPAND, true, false);
212: loopGroup.add(rdBut9);
213: addJavaDLOption(rdBut9, javaDLOptionsLayout, 2, yCoord, 2);
214:
215: rdBut10 = new JRadioButtonHashMap("Invariant",
216: StrategyProperties.LOOP_INVARIANT, false, false);
217: loopGroup.add(rdBut10);
218: addJavaDLOption(rdBut10, javaDLOptionsLayout, 4, yCoord, 2);
219:
220: rdBut11 = new JRadioButtonHashMap("None",
221: StrategyProperties.LOOP_NONE, false, false);
222: loopGroup.add(rdBut11);
223: addJavaDLOption(rdBut11, javaDLOptionsLayout, 6, yCoord, 2);
224:
225: ++yCoord;
226: addJavaDLOptionSpace(javaDLOptionsLayout, yCoord);
227:
228: ////////////////////////////////////////////////////////////////////////
229:
230: ++yCoord;
231:
232: addJavaDLOption(new JLabel("Method treatment"),
233: javaDLOptionsLayout, 1, yCoord, 7);
234:
235: ++yCoord;
236:
237: rdBut12 = new JRadioButtonHashMap("Expand",
238: StrategyProperties.METHOD_EXPAND, true, false);
239: methodGroup.add(rdBut12);
240: addJavaDLOption(rdBut12, javaDLOptionsLayout, 2, yCoord, 2);
241:
242: rdBut13 = new JRadioButtonHashMap("Contracts",
243: StrategyProperties.METHOD_CONTRACT, false, false);
244: methodGroup.add(rdBut13);
245: addJavaDLOption(rdBut13, javaDLOptionsLayout, 4, yCoord, 2);
246:
247: rdBut14 = new JRadioButtonHashMap("None",
248: StrategyProperties.METHOD_NONE, false, false);
249: methodGroup.add(rdBut14);
250: addJavaDLOption(rdBut14, javaDLOptionsLayout, 6, yCoord, 2);
251:
252: ++yCoord;
253: addJavaDLOptionSpace(javaDLOptionsLayout, yCoord);
254:
255: ////////////////////////////////////////////////////////////////////////
256:
257: ++yCoord;
258:
259: addJavaDLOption(new JLabel("Query treatment"),
260: javaDLOptionsLayout, 1, yCoord, 7);
261:
262: ++yCoord;
263:
264: queryExpand = new JRadioButtonHashMap("Expand",
265: StrategyProperties.QUERY_EXPAND, false, false);
266: queryGroup.add(queryExpand);
267: addJavaDLOption(queryExpand, javaDLOptionsLayout, 2, yCoord, 2);
268:
269: queryProgramsToRight = new JRadioButtonHashMap("Prog2Succ",
270: StrategyProperties.QUERY_PROGRAMS_TO_RIGHT, false,
271: false);
272: queryProgramsToRight
273: .setToolTipText("<html>Move all program blocks to the"
274: + " succedent.<br>" + " This is necessary"
275: + " when query invocations<br>" + " are"
276: + " supposed to be eliminated" + " using<br>"
277: + " method contracts.</html>");
278: queryGroup.add(queryProgramsToRight);
279: addJavaDLOption(queryProgramsToRight, javaDLOptionsLayout, 4,
280: yCoord, 2);
281:
282: queryNone = new JRadioButtonHashMap("None",
283: StrategyProperties.QUERY_NONE, true, false);
284: queryGroup.add(queryNone);
285: addJavaDLOption(queryNone, javaDLOptionsLayout, 6, yCoord, 2);
286:
287: ++yCoord;
288: addJavaDLOptionSpace(javaDLOptionsLayout, yCoord);
289:
290: ////////////////////////////////////////////////////////////////////////
291:
292: ++yCoord;
293:
294: addJavaDLOption(new JLabel("Arithmetic treatment"),
295: javaDLOptionsLayout, 1, yCoord, 7);
296:
297: ++yCoord;
298:
299: nonLinArithNone = new JRadioButtonHashMap("Basic",
300: StrategyProperties.NON_LIN_ARITH_NONE, true, false);
301: nonLinArithNone
302: .setToolTipText("<html>"
303: + "Basic arithmetic support:"
304: + "<ul>"
305: + "<li>Simplification of polynomial expressions</li>"
306: + "<li>Computation of Gröbner Bases for polynomials in the antecedent</li>"
307: + "<li>(Partial) Omega procedure for handling linear inequations</li>"
308: + "</ul>" + "</html>");
309: nonLinArithGroup.add(nonLinArithNone);
310: addJavaDLOption(nonLinArithNone, javaDLOptionsLayout, 2,
311: yCoord, 2);
312:
313: nonLinArithDefOps = new JRadioButtonHashMap("DefOps",
314: StrategyProperties.NON_LIN_ARITH_DEF_OPS, false, false);
315: nonLinArithDefOps
316: .setToolTipText("<html>"
317: + "Automatically expand defined symbols like:"
318: + "<ul>"
319: + "<li><tt>/</tt>, <tt>%</tt>, <tt>jdiv</tt>, <tt>jmod</tt>, ...</li>"
320: + "<li><tt>int_RANGE</tt>, <tt>short_MIN</tt>, ...</li>"
321: + "<li><tt>inInt</tt>, <tt>inByte</tt>, ...</li>"
322: + "<li><tt>addJint</tt>, <tt>mulJshort</tt>, ...</li>"
323: + "</ul>" + "</html>");
324: nonLinArithGroup.add(nonLinArithDefOps);
325: addJavaDLOption(nonLinArithDefOps, javaDLOptionsLayout, 4,
326: yCoord, 2);
327:
328: nonLinArithCompletion = new JRadioButtonHashMap("Model Search",
329: StrategyProperties.NON_LIN_ARITH_COMPLETION, false,
330: false);
331: nonLinArithCompletion
332: .setToolTipText("<html>"
333: + "Support for non-linear inequations and model search.<br>"
334: + "In addition, this performs:"
335: + "<ul>"
336: + "<li>Multiplication of inequations with each other</li>"
337: + "<li>Systematic case distinctions (cuts)</li>"
338: + "</ul>"
339: + "This method is guaranteed to find counterexamples for<br>"
340: + "invalid goals that only contain polynomial (in)equations.<br>"
341: + "Such counterexamples turn up as trivially unprovable goals.<br>"
342: + "It is also able to prove many more valid goals involving<br>"
343: + "(in)equations, but will in general not terminate on such goals."
344: + "</html>");
345: nonLinArithGroup.add(nonLinArithCompletion);
346: addJavaDLOption(nonLinArithCompletion, javaDLOptionsLayout, 6,
347: yCoord, 2);
348:
349: ++yCoord;
350: addJavaDLOptionSpace(javaDLOptionsLayout, yCoord);
351:
352: ////////////////////////////////////////////////////////////////////////
353:
354: ++yCoord;
355:
356: addJavaDLOption(new JLabel("Quantifier treatment"),
357: javaDLOptionsLayout, 1, yCoord, 7);
358:
359: ++yCoord;
360:
361: quantifierNone = new JRadioButtonHashMap("None",
362: StrategyProperties.QUANTIFIERS_NONE, true, false);
363: quantifierNone
364: .setToolTipText("<html>"
365: + "Do not instantiate quantified formulas automatically"
366: + "</html>");
367: quantifierGroup.add(quantifierNone);
368: addJavaDLOption(quantifierNone, javaDLOptionsLayout, 2, yCoord,
369: 4);
370:
371: quantifierNonSplitting = new JRadioButtonHashMap("No Splits",
372: StrategyProperties.QUANTIFIERS_NON_SPLITTING, true,
373: false);
374: quantifierNonSplitting
375: .setToolTipText("<html>"
376: + "Instantiate quantified formulas automatically<br>"
377: + "with terms that occur in a sequent, but only if<br>"
378: + "this does not cause proof splitting. Further, quantified<br>"
379: + "formulas that contain queries are not instantiated<br>"
380: + "automatically." + "</html>");
381: quantifierGroup.add(quantifierNonSplitting);
382: addJavaDLOption(quantifierNonSplitting, javaDLOptionsLayout, 6,
383: yCoord, 2);
384:
385: ++yCoord;
386:
387: quantifierNonSplittingWithProgs = new JRadioButtonHashMap(
388: "No Splits with Progs",
389: StrategyProperties.QUANTIFIERS_NON_SPLITTING_WITH_PROGS,
390: true, false);
391: quantifierNonSplittingWithProgs
392: .setToolTipText("<html>"
393: + "Instantiate quantified formulas automatically<br>"
394: + "with terms that occur in a sequent, but if the<br>"
395: + "sequent contains programs then only perform<br>"
396: + "instantiations that do not cause proof splitting.<br>"
397: + "Further, quantified formulas that contain queries<br>"
398: + "are not instantiated automatically."
399: + "</html>");
400: quantifierGroup.add(quantifierNonSplittingWithProgs);
401: addJavaDLOption(quantifierNonSplittingWithProgs,
402: javaDLOptionsLayout, 2, yCoord, 4);
403:
404: quantifierInstantiate = new JRadioButtonHashMap("Unrestricted",
405: StrategyProperties.QUANTIFIERS_INSTANTIATE, true, false);
406: quantifierInstantiate
407: .setToolTipText("<html>"
408: + "Instantiate quantified formulas automatically<br>"
409: + "with terms that occur in a sequent, also if this<br>"
410: + "might cause proof splitting." + "</html>");
411: quantifierGroup.add(quantifierInstantiate);
412: addJavaDLOption(quantifierInstantiate, javaDLOptionsLayout, 6,
413: yCoord, 2);
414:
415: ++yCoord;
416: addJavaDLOptionSpace(javaDLOptionsLayout, yCoord);
417:
418: ////////////////////////////////////////////////////////////////////////
419:
420: ++yCoord;
421:
422: final JLabel userTacletsLabel = new JLabel(
423: "User-specific taclets");
424: addJavaDLOption(userTacletsLabel, javaDLOptionsLayout, 1,
425: yCoord, 7);
426: userTacletsLabel
427: .setToolTipText("<html>"
428: + "These options define whether user- and problem-specific taclets<br>"
429: + "are applied automatically by the strategy. Problem-specific taclets<br>"
430: + "can be defined in the \\rules-section of a .key-problem file or be<br>"
431: + "loaded during a proof with \"Load Non-Axiom Lemma ...\". For<br>"
432: + "automatic application, the taclets have to contain a clause<br>"
433: + "\\heuristics(userTaclets1), \\heuristics(userTaclets2), etc."
434: + "</html>");
435:
436: for (int i = 1; i <= StrategyProperties.USER_TACLETS_NUM; ++i) {
437: ++yCoord;
438: addUserTacletsOptions(javaDLOptionsLayout, optListener,
439: userTacletsGroup[i - 1], yCoord, i);
440: }
441:
442: fixVerticalSpace(javaDLOptionsScrollPane);
443:
444: ////////////////////////////////////////////////////////////////////////
445:
446: Box box = Box.createVerticalBox();
447: stratGroup.add(bSimpleFOLStrategy);
448: stratGroup.add(bSimpleJavaCardDLStrategy);
449: stratGroup.add(bSimplificationOfOCLStrategy);
450: stratGroup.add(bVBTStrategy);
451: stratGroup.add(bComputeSpecificationStrategy);
452: javaDLOptionsPanel.setEnabled(bSimpleJavaCardDLStrategy
453: .isSelected());
454: bSimpleJavaCardDLStrategy
455: .addChangeListener(new ChangeListener() {
456: public void stateChanged(ChangeEvent e) {
457: javaDLOptionsPanel
458: .setEnabled(bSimpleJavaCardDLStrategy
459: .isSelected());
460: }
461: });
462:
463: JButton go = new JButton(Main.autoModeAction);
464:
465: JCheckBox resumeAutoMode = createResumeAutoModeCheckBox();
466: JPanel timeout = createTimeoutSpinner();
467:
468: JPanel goPanel = new JPanel();
469: GridBagLayout goLayout = new GridBagLayout();
470: goPanel.setLayout(goLayout);
471: goPanel.setAlignmentX(Component.LEFT_ALIGNMENT);
472:
473: gbcpanel5.gridx = 1;
474: gbcpanel5.gridy = 0;
475: gbcpanel5.gridwidth = 1;
476: gbcpanel5.gridheight = 1;
477: gbcpanel5.fill = GridBagConstraints.NONE;
478: gbcpanel5.weightx = 1;
479: gbcpanel5.weighty = 0;
480: gbcpanel5.anchor = GridBagConstraints.WEST;
481: gbcpanel5.insets = new Insets(4, 4, 4, 4);
482: goLayout.setConstraints(go, gbcpanel5);
483: goPanel.add(go);
484:
485: gbcpanel5.gridx = 1;
486: gbcpanel5.gridy = 1;
487: gbcpanel5.gridwidth = 1;
488: gbcpanel5.gridheight = 1;
489: gbcpanel5.fill = GridBagConstraints.NONE;
490: gbcpanel5.weightx = 1;
491: gbcpanel5.weighty = 0;
492: gbcpanel5.anchor = GridBagConstraints.WEST;
493: gbcpanel5.insets = new Insets(0, 0, 0, 0);
494: goLayout.setConstraints(resumeAutoMode, gbcpanel5);
495: goPanel.add(resumeAutoMode);
496:
497: gbcpanel5.gridx = 2;
498: gbcpanel5.gridy = 0;
499: gbcpanel5.gridwidth = 1;
500: gbcpanel5.gridheight = 1;
501: gbcpanel5.fill = GridBagConstraints.NONE;
502: gbcpanel5.weightx = 0;
503: gbcpanel5.weighty = 0;
504: gbcpanel5.anchor = GridBagConstraints.CENTER;
505: gbcpanel5.insets = new Insets(0, 0, 0, 0);
506: goLayout.setConstraints(timeout, gbcpanel5);
507: goPanel.add(timeout);
508:
509: fixVerticalSpace(goPanel);
510:
511: box.add(Box.createVerticalStrut(4));
512: box.add(goPanel);
513: box.add(Box.createVerticalStrut(8));
514: // box.add(numLabel);
515: // box.add(Box.createVerticalStrut(4));
516: maxSlider.setAlignmentX(Component.LEFT_ALIGNMENT);
517: box.add(maxSlider);
518: box.add(Box.createVerticalStrut(8));
519: bSimpleFOLStrategy.setAlignmentX(Component.LEFT_ALIGNMENT);
520: box.add(bSimpleFOLStrategy);
521: bSimpleJavaCardDLStrategy
522: .setAlignmentX(Component.LEFT_ALIGNMENT);
523: box.add(bSimpleJavaCardDLStrategy);
524: javaDLOptionsScrollPane.setAlignmentX(Component.LEFT_ALIGNMENT);
525: box.add(javaDLOptionsScrollPane);
526: box.add(bVBTStrategy);
527:
528: bSimplificationOfOCLStrategy
529: .setAlignmentX(Component.LEFT_ALIGNMENT);
530: box.add(bSimplificationOfOCLStrategy);
531: bComputeSpecificationStrategy
532: .setAlignmentX(Component.LEFT_ALIGNMENT);
533: box.add(bComputeSpecificationStrategy);
534:
535: // HACK but I really do not know enough about the GridBagLayout :-(
536: // final JPanel verticalGlue = new JPanel();
537: // verticalGlue.setPreferredSize(new Dimension(1, 1024));
538: // box.add(verticalGlue);
539: box.add(Box.createVerticalGlue());
540:
541: this .add(box);
542: // add the ActionListener to the Buttons and ActionCommands
543: // for identifying Buttons
544: bSimpleFOLStrategy.addActionListener(stratListener);
545: bSimpleJavaCardDLStrategy.addActionListener(stratListener);
546: bSimplificationOfOCLStrategy.addActionListener(stratListener);
547: bVBTStrategy.addActionListener(stratListener);
548: bComputeSpecificationStrategy.addActionListener(stratListener);
549: rdBut9.addActionListener(optListener);
550: rdBut10.addActionListener(optListener);
551: rdBut11.addActionListener(optListener);
552: rdBut12.addActionListener(optListener);
553: rdBut13.addActionListener(optListener);
554: rdBut14.addActionListener(optListener);
555: queryExpand.addActionListener(optListener);
556: queryProgramsToRight.addActionListener(optListener);
557: queryNone.addActionListener(optListener);
558: splittingNormal.addActionListener(optListener);
559: splittingDelayed.addActionListener(optListener);
560: splittingOff.addActionListener(optListener);
561: nonLinArithNone.addActionListener(optListener);
562: nonLinArithDefOps.addActionListener(optListener);
563: nonLinArithCompletion.addActionListener(optListener);
564: quantifierNone.addActionListener(optListener);
565: quantifierNonSplitting.addActionListener(optListener);
566: quantifierNonSplittingWithProgs.addActionListener(optListener);
567: quantifierInstantiate.addActionListener(optListener);
568: }
569:
570: private void addUserTacletsOptions(
571: GridBagLayout javaDLOptionsLayout, OptListener optListener,
572: ButtonGroup group, int yCoord, int num) {
573: addJavaDLOption(new JLabel("" + num + ": "),
574: javaDLOptionsLayout, 2, yCoord, 1);
575:
576: final JRadioButtonHashMap userTacletsOff = new JRadioButtonHashMap(
577: "Off", StrategyProperties.USER_TACLETS_OFF + num, true,
578: false);
579: userTacletsOff
580: .setToolTipText("Taclets of the rule set \"userTaclets"
581: + num + "\" are not applied automatically");
582: group.add(userTacletsOff);
583: userTacletsOff.addActionListener(optListener);
584: addJavaDLOption(userTacletsOff, javaDLOptionsLayout, 3, yCoord,
585: 1);
586:
587: final JRadioButtonHashMap userTacletsLow = new JRadioButtonHashMap(
588: "Low prior.",
589: StrategyProperties.USER_TACLETS_LOW + num, true, false);
590: userTacletsLow
591: .setToolTipText("Taclets of the rule set \"userTaclets"
592: + num
593: + "\" are applied automatically with low priority");
594: group.add(userTacletsLow);
595: userTacletsLow.addActionListener(optListener);
596: addJavaDLOption(userTacletsLow, javaDLOptionsLayout, 4, yCoord,
597: 2);
598:
599: final JRadioButtonHashMap userTacletsHigh = new JRadioButtonHashMap(
600: "High prior.", StrategyProperties.USER_TACLETS_HIGH
601: + num, true, false);
602: userTacletsHigh
603: .setToolTipText("Taclets of the rule set \"userTaclets"
604: + num
605: + "\" are applied automatically with high priority");
606: group.add(userTacletsHigh);
607: userTacletsHigh.addActionListener(optListener);
608: addJavaDLOption(userTacletsHigh, javaDLOptionsLayout, 6,
609: yCoord, 2);
610: }
611:
612: private void addJavaDLOptionSpace(
613: GridBagLayout javaDLOptionsLayout, int yCoord) {
614: final GridBagConstraints con = new GridBagConstraints();
615: con.gridx = 0;
616: con.gridy = yCoord;
617: con.gridwidth = 9;
618: con.gridheight = 1;
619: con.fill = GridBagConstraints.HORIZONTAL;
620: con.weightx = 1;
621: con.weighty = 0;
622: con.anchor = GridBagConstraints.CENTER;
623: final Component sep = new JLabel();
624: javaDLOptionsLayout.setConstraints(sep, con);
625: javaDLOptionsPanel.add(sep);
626: addJavaDLOption(Box.createRigidArea(new Dimension(4, 4)),
627: javaDLOptionsLayout, 0, yCoord, 1);
628: addJavaDLOption(Box.createRigidArea(new Dimension(4, 4)),
629: javaDLOptionsLayout, 1, yCoord, 1);
630: }
631:
632: private void addJavaDLOption(Component widget,
633: GridBagLayout javaDLOptionsLayout, int gridx, int gridy,
634: int width) {
635: final GridBagConstraints con = new GridBagConstraints();
636: con.gridx = gridx;
637: con.gridy = gridy;
638: con.gridwidth = width;
639: con.gridheight = 1;
640: con.fill = GridBagConstraints.NONE;
641: con.weightx = 0;
642: con.weighty = 0;
643: con.anchor = GridBagConstraints.WEST;
644: javaDLOptionsLayout.setConstraints(widget, con);
645: javaDLOptionsPanel.add(widget);
646: }
647:
648: private void fixVerticalSpace(JComponent comp) {
649: comp.setMaximumSize(new Dimension(Integer.MAX_VALUE, comp
650: .getPreferredSize().height));
651: }
652:
653: private JPanel createTimeoutSpinner() {
654: final JPanel timeoutPanel = new JPanel();
655: timeoutPanel.setLayout(new FlowLayout());
656: final JLabel timeoutLabel = new JLabel("Time limit (ms)");
657: timeoutPanel.add(timeoutLabel);
658: timeoutPanel
659: .setToolTipText("Interrupt automatic rule application "
660: + "after the specified period of time (-1 disables timeout).");
661:
662: timeoutSpinner = new TimeoutSpinner();
663:
664: timeoutSpinner.addChangeListener(new ChangeListener() {
665:
666: public void stateChanged(ChangeEvent e) {
667: if (e.getSource() == timeoutSpinner) {
668: long timeout = ((Long) ((JSpinner) e.getSource())
669: .getValue()).longValue();
670: mediator.setAutomaticApplicationTimeout(timeout);
671: }
672: }
673: });
674: timeoutPanel.add(timeoutSpinner);
675: return timeoutPanel;
676: }
677:
678: private JCheckBox createResumeAutoModeCheckBox() {
679: JCheckBox resumeAutoMode = new JCheckBox("Autoresume strategy");
680: resumeAutoMode
681: .setToolTipText("Restart strategy after an interactive proof step?");
682: resumeAutoMode.setBorderPaintedFlat(true);
683:
684: /* Sorry, but the icon was concealing the checkbox nature of this
685: thing. People were thinking it was a button.
686: resumeAutoMode.setIcon
687: (IconFactory.resumeDisabledLogo(toolbarIconSize));
688: */
689:
690: resumeAutoMode
691: .setMaximumSize(resumeAutoMode.getPreferredSize());
692: resumeAutoMode.addItemListener(new ItemListener() {
693: public void itemStateChanged(ItemEvent e) {
694: if (e.getStateChange() == ItemEvent.SELECTED) {
695: // resumeAutoMode.
696: // setIcon(IconFactory.resumeLogo(toolbarIconSize));
697: mediator.setResumeAutoMode(true);
698: } else if (e.getStateChange() == ItemEvent.DESELECTED) {
699: // resumeAutoMode.
700: // setIcon(IconFactory.
701: // resumeDisabledLogo(toolbarIconSize));
702: mediator.setResumeAutoMode(false);
703: } else
704: System.err
705: .println("Automode checkbox undefined state: "
706: + e.getStateChange());
707:
708: }
709: });
710: return resumeAutoMode;
711: }
712:
713: public void setMediator(KeYMediator mediator) {
714: this .mediator = mediator;
715: maxSlider.setMediator(mediator);
716:
717: mediator
718: .addKeYSelectionListener(new SelectionChangedListener());
719:
720: final StrategyFactory defaultStrategyFactory = mediator
721: .getProfile().getDefaultStrategyFactory();
722:
723: getStrategyButton(defaultStrategyFactory.name().toString())
724: .setSelected(true);
725: }
726:
727: private final MaxRuleAppSlider maxSlider = new MaxRuleAppSlider(
728: mediator);
729:
730: private final class JavaDLOptionListener implements
731: PropertyChangeListener, ItemListener {
732: public void propertyChange(PropertyChangeEvent evt) {
733: if (evt.getNewValue() instanceof Boolean) {
734: javaDLOptionsPanel
735: .setEnabled(bSimpleJavaCardDLStrategy
736: .isSelected()
737: && ((Boolean) evt.getNewValue())
738: .booleanValue());
739: } else {
740: javaDLOptionsPanel.setEnabled(bSimpleJavaCardDLStrategy
741: .isSelected()
742: && Boolean.getBoolean("" + evt.getNewValue()));
743: }
744: }
745:
746: public void itemStateChanged(ItemEvent e) {
747: if (e.getItem() == bSimpleJavaCardDLStrategy) {
748: javaDLOptionsPanel.setEnabled(bSimpleJavaCardDLStrategy
749: .isSelected()
750: && bSimpleJavaCardDLStrategy.isEnabled());
751: }
752: }
753: }
754:
755: class TimeoutSpinner extends JSpinner {
756: public TimeoutSpinner() {
757: super (new SpinnerNumberModel(new Long(-1), new Long(-1),
758: new Long(Long.MAX_VALUE), new Long(1)));
759: if (this .getEditor() instanceof JSpinner.DefaultEditor) {
760: JFormattedTextField ftf = ((JSpinner.DefaultEditor) this
761: .getEditor()).getTextField();
762: if (ftf != null) {
763: ftf.setColumns(6);
764: ftf.setHorizontalAlignment(JTextField.RIGHT);
765: }
766: }
767: }
768:
769: public void refresh() {
770: setValue(new Long(mediator.getAutomaticApplicationTimeout()));
771: }
772: }
773:
774: /**
775: * TODO: here should be a settings listener listening to strategy setting changes
776: * Therefore we have to wait until ProofSettings have been refactored (see KeY-Wiki)
777: *
778: *(Currently changes made in the old slider are not reported to this view)
779: */
780: private final class SelectionChangedListener implements
781: KeYSelectionListener {
782:
783: public void selectedNodeChanged(KeYSelectionEvent e) {
784: }
785:
786: public void selectedProofChanged(KeYSelectionEvent e) {
787: refresh(e.getSource().getSelectedProof());
788: }
789: }
790:
791: /** performs a refresh of all elements in this tab */
792: public void refresh(Proof proof) {
793: if (proof == null) {
794: enableAll(false);
795: } else {
796: maxSlider.refresh();
797: timeoutSpinner.refresh();
798: enableAll(true);
799: String activeS = proof.getActiveStrategy().name()
800: .toString();
801: JRadioButton bactive = JRadioButtonHashMap
802: .getButton(activeS);
803: bactive.setSelected(true);
804:
805: StrategyProperties p = proof.getSettings()
806: .getStrategySettings()
807: .getActiveStrategyProperties();
808:
809: String activeSplittingOptions = p
810: .getProperty(StrategyProperties.SPLITTING_OPTIONS_KEY);
811: JRadioButton bSplittingActive = getStrategyOptionButton(
812: activeSplittingOptions,
813: StrategyProperties.LOOP_OPTIONS_KEY);
814: bSplittingActive.setSelected(true);
815: String activeLoopOptions = p
816: .getProperty(StrategyProperties.LOOP_OPTIONS_KEY);
817: JRadioButton bLoopActive = getStrategyOptionButton(
818: activeLoopOptions,
819: StrategyProperties.LOOP_OPTIONS_KEY);
820: bLoopActive.setSelected(true);
821: String activeMethodOptions = p
822: .getProperty(StrategyProperties.METHOD_OPTIONS_KEY);
823: JRadioButton bMethodActive = getStrategyOptionButton(
824: activeMethodOptions,
825: StrategyProperties.METHOD_OPTIONS_KEY);
826: bMethodActive.setSelected(true);
827: String activeQueryOptions = p
828: .getProperty(StrategyProperties.QUERY_OPTIONS_KEY);
829: JRadioButton bQueryActive = getStrategyOptionButton(
830: activeQueryOptions,
831: StrategyProperties.QUERY_OPTIONS_KEY);
832: bQueryActive.setSelected(true);
833: String activeNonLinArithOptions = p
834: .getProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY);
835: JRadioButton bNonLinArithActive = getStrategyOptionButton(
836: activeNonLinArithOptions,
837: StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY);
838: bNonLinArithActive.setSelected(true);
839: String quantifierOptions = p
840: .getProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY);
841: JRadioButton bQuantifierActive = getStrategyOptionButton(
842: quantifierOptions,
843: StrategyProperties.QUANTIFIERS_OPTIONS_KEY);
844: bQuantifierActive.setSelected(true);
845: for (int i = 1; i <= StrategyProperties.USER_TACLETS_NUM; ++i) {
846: String userTacletsOptions = p
847: .getProperty(StrategyProperties
848: .USER_TACLETS_OPTIONS_KEY(i));
849: JRadioButton userTacletsActive = getStrategyOptionButton(
850: userTacletsOptions + i,
851: StrategyProperties.USER_TACLETS_OFF);
852: userTacletsActive.setSelected(true);
853: }
854: }
855: }
856:
857: private JRadioButton getStrategyOptionButton(String activeOptions,
858: String category) {
859: JRadioButton bActive = JRadioButtonHashMap
860: .getButton(activeOptions);
861: if (bActive == null) {
862: System.err.println("Unknown option '" + activeOptions
863: + "' falling back to "
864: + StrategyProperties.getDefaultProperty(category));
865: bActive = JRadioButtonHashMap.getButton(StrategyProperties
866: .getDefaultProperty(category));
867: }
868: return bActive;
869: }
870:
871: private JRadioButton getStrategyButton(String name) {
872: return JRadioButtonHashMap.getButton(name);
873: }
874:
875: /**
876: * enables or disables all components
877: * @param enable boolean saying whether to activate or
878: * deactivate the components
879: */
880: private void enableAll(boolean enable) {
881: maxSlider.setEnabled(enable);
882: timeoutSpinner.setEnabled(enable);
883: if (mediator != null) {
884: final IteratorOfStrategyFactory supportedStrategies = mediator
885: .getProfile().supportedStrategies().iterator();
886: while (supportedStrategies.hasNext()) {
887: final StrategyFactory next = supportedStrategies.next();
888: getStrategyButton(next.name().toString()).setEnabled(
889: enable);
890: }
891: }
892: }
893:
894: public Strategy getStrategy(String strategyName, Proof proof,
895: StrategyProperties properties) {
896: if (mediator != null) {
897: final IteratorOfStrategyFactory supportedStrategies = mediator
898: .getProfile().supportedStrategies().iterator();
899: while (supportedStrategies.hasNext()) {
900: final StrategyFactory s = supportedStrategies.next();
901: if (strategyName.equals(s.name().toString())) {
902: return s.create(proof, properties);
903: }
904: }
905: }
906: System.err.println("Selected Strategy '"
907: + strategyName
908: + "' not found falling back to "
909: + mediator.getProfile().getDefaultStrategyFactory()
910: .name());
911: return mediator.getProfile().getDefaultStrategyFactory()
912: .create(proof, properties);
913: }
914:
915: private String removeLast(String str, int num) {
916: return str.substring(0, str.length() - num);
917: }
918:
919: /**
920: * @return
921: */
922: private StrategyProperties getProperties() {
923: StrategyProperties p = new StrategyProperties();
924: p.setProperty(StrategyProperties.SPLITTING_OPTIONS_KEY,
925: splittingGroup.getSelection().getActionCommand());
926: p.setProperty(StrategyProperties.LOOP_OPTIONS_KEY, loopGroup
927: .getSelection().getActionCommand());
928: p.setProperty(StrategyProperties.METHOD_OPTIONS_KEY,
929: methodGroup.getSelection().getActionCommand());
930: p.setProperty(StrategyProperties.QUERY_OPTIONS_KEY, queryGroup
931: .getSelection().getActionCommand());
932: p.setProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY,
933: nonLinArithGroup.getSelection().getActionCommand());
934: p.setProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY,
935: quantifierGroup.getSelection().getActionCommand());
936:
937: for (int i = 1; i <= StrategyProperties.USER_TACLETS_NUM; ++i) {
938: p.setProperty(StrategyProperties
939: .USER_TACLETS_OPTIONS_KEY(i), removeLast(
940: userTacletsGroup[i - 1].getSelection()
941: .getActionCommand(), 1));
942: }
943:
944: return p;
945: }
946:
947: /**
948: *
949: */
950: private void updateStrategySettings(String strategyName) {
951: final Proof proof = mediator.getProof();
952: final StrategyProperties p = getProperties();
953: final Strategy strategy = getStrategy(strategyName, proof, p);
954:
955: ProofSettings.DEFAULT_SETTINGS.getStrategySettings()
956: .setStrategy(strategy.name());
957: ProofSettings.DEFAULT_SETTINGS.getStrategySettings()
958: .setActiveStrategyProperties(p);
959:
960: proof.getSettings().getStrategySettings().setStrategy(
961: strategy.name());
962: proof.getSettings().getStrategySettings()
963: .setActiveStrategyProperties(p);
964:
965: proof.setActiveStrategy(strategy);
966: }
967:
968: public class StratListener implements ActionListener {
969: public void actionPerformed(ActionEvent e) {
970: updateStrategySettings(e.getActionCommand());
971: }
972: }
973:
974: public class OptListener implements ActionListener {
975: public void actionPerformed(ActionEvent e) {
976: updateStrategySettings(mediator.getProof()
977: .getActiveStrategy().name().toString());
978: }
979: }
980:
981: }
|