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: package de.uka.ilkd.key.gui;
009:
010: import de.uka.ilkd.key.unittest.*;
011: import de.uka.ilkd.key.unittest.simplify.*;
012: import de.uka.ilkd.key.util.ExtList;
013: import de.uka.ilkd.key.logic.op.*;
014: import de.uka.ilkd.key.gui.configuration.ProofSettings;
015: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
016:
017: import java.awt.event.ActionListener;
018: import java.awt.event.ActionEvent;
019: import java.awt.*;
020: import javax.swing.*;
021: import javax.swing.border.TitledBorder;
022:
023: public class MethodSelectionDialog extends JDialog {
024:
025: private UnitTestBuilder testBuilder;
026: private KeYMediator mediator;
027: private JList methodList;
028: private final JCheckBox simplify = new JCheckBox("Simplify");
029: private final JCheckBox cogent = new JCheckBox("Cogent");
030: private final JCheckBox completeEx = new JCheckBox(
031: "Only completely " + "executed traces");
032: private static MethodSelectionDialog instance = null;
033: private StringBuffer latestTests = new StringBuffer();
034:
035: private MethodSelectionDialog(KeYMediator mediator) {
036: this .mediator = mediator;
037: testBuilder = new UnitTestBuilder(mediator.getServices(),
038: mediator.getProof());
039: layoutMethodSelectionDialog();
040: pack();
041: setLocation(70, 70);
042: setVisible(true);
043: }
044:
045: public static MethodSelectionDialog getInstance(KeYMediator mediator) {
046: if (instance != null) {
047: instance.setVisible(false);
048: instance.dispose();
049: }
050: instance = new MethodSelectionDialog(mediator);
051: instance.cogent
052: .setSelected(ModelGenerator.decProdForTestGen == ModelGenerator.COGENT);
053: instance.simplify
054: .setSelected(ModelGenerator.decProdForTestGen == ModelGenerator.SIMPLIFY);
055: instance.completeEx
056: .setSelected(UnitTestBuilder.requireCompleteExecution);
057: return instance;
058: }
059:
060: private void layoutMethodSelectionDialog() {
061: getContentPane().setLayout(
062: new BoxLayout(getContentPane(), BoxLayout.Y_AXIS));
063: final MethodSelectionDialog this Ref = this ;
064: final JTextField simplifyDataTupleNumber = new JTextField(""
065: + SimplifyModelGenerator.modelLimit, 2);
066: simplifyDataTupleNumber
067: .setToolTipText("Minimal number of data tuples"
068: + "per test method");
069: // methodlist
070: methodList = new JList();
071: methodList.setCellRenderer(new DefaultListCellRenderer() {
072: public Component getListCellRendererComponent(JList list,
073: Object value, int index, boolean isSelected,
074: boolean cellHasFocus) {
075: if (value != null) {
076: ProgramMethod pm = (ProgramMethod) value;
077: MethodDeclaration md = pm.getMethodDeclaration();
078: String params = md.getParameters().toString();
079: setText((md.getTypeReference() == null ? "void"
080: : md.getTypeReference().getName())
081: + " "
082: + md.getFullName()
083: + "("
084: + params.substring(1, params.length() - 1)
085: + ")");
086: if (isSelected) {
087: setBackground(list.getSelectionBackground());
088: setForeground(list.getSelectionForeground());
089: } else {
090: setBackground(list.getBackground());
091: setForeground(list.getForeground());
092: }
093: setEnabled(list.isEnabled());
094: setFont(list.getFont());
095: setOpaque(true);
096: }
097: return this ;
098: }
099: });
100: SetOfProgramMethod pms = testBuilder.getProgramMethods(mediator
101: .getProof());
102: methodList.setListData(pms.toArray());
103: JScrollPane methodListScroll = new JScrollPane(
104: JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED,
105: JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
106: methodListScroll.getViewport().setView(methodList);
107: methodListScroll.setBorder(new TitledBorder(
108: "Methods occuring in Proof"));
109: methodListScroll
110: .setMinimumSize(new java.awt.Dimension(250, 400));
111: getContentPane().add(methodListScroll);
112:
113: //buttons
114: final JPanel buttonPanel = new JPanel();
115: buttonPanel.setLayout(new BoxLayout(buttonPanel,
116: BoxLayout.X_AXIS));
117: JButton testAll = new JButton("Create Test For Proof");
118: testAll.addActionListener(new ActionListener() {
119: public void actionPerformed(ActionEvent e) {
120: setSimplifyCount(simplifyDataTupleNumber.getText());
121: createTest(null);
122: }
123: });
124: buttonPanel.add(testAll);
125: JButton testSel = new JButton(
126: "Create Test For Selected Method(s)");
127: testSel.addActionListener(new ActionListener() {
128: public void actionPerformed(ActionEvent e) {
129: if (methodList.getSelectedValues().length == 0) {
130: JOptionPane.showMessageDialog(null,
131: "Please select the method(s) first!",
132: "No Methods Selected",
133: JOptionPane.ERROR_MESSAGE);
134: } else {
135: setSimplifyCount(simplifyDataTupleNumber.getText());
136: createTest(methodList.getSelectedValues());
137: }
138: }
139: });
140: buttonPanel.add(testSel);
141: simplify.addActionListener(new ActionListener() {
142: public void actionPerformed(ActionEvent e) {
143: if (simplify.isSelected()) {
144: ModelGenerator.decProdForTestGen = ModelGenerator.SIMPLIFY;
145: ProofSettings.DEFAULT_SETTINGS
146: .getDecisionProcedureSettings()
147: .setDecisionProcedureForTest(
148: DecisionProcedureSettings.SIMPLIFY);
149: buttonPanel.add(simplifyDataTupleNumber,
150: buttonPanel.getComponentCount() - 1);
151: simplifyDataTupleNumber.setText(""
152: + SimplifyModelGenerator.modelLimit);
153: cogent.setSelected(false);
154: this Ref.pack();
155: } else {
156: ModelGenerator.decProdForTestGen = ModelGenerator.COGENT;
157: ProofSettings.DEFAULT_SETTINGS
158: .getDecisionProcedureSettings()
159: .setDecisionProcedureForTest(
160: DecisionProcedureSettings.COGENT);
161: buttonPanel.remove(simplifyDataTupleNumber);
162: simplify.setSelected(false);
163: cogent.setSelected(true);
164: this Ref.pack();
165: }
166: }
167: });
168: cogent.addActionListener(new ActionListener() {
169: public void actionPerformed(ActionEvent e) {
170: if (cogent.isSelected()) {
171: ModelGenerator.decProdForTestGen = ModelGenerator.COGENT;
172: buttonPanel.remove(simplifyDataTupleNumber);
173: simplify.setSelected(false);
174: this Ref.pack();
175: } else {
176: ModelGenerator.decProdForTestGen = ModelGenerator.SIMPLIFY;
177: buttonPanel.add(simplifyDataTupleNumber,
178: buttonPanel.getComponentCount() - 1);
179: simplifyDataTupleNumber.setText(""
180: + SimplifyModelGenerator.modelLimit);
181: cogent.setSelected(false);
182: simplify.setSelected(true);
183: this Ref.pack();
184: }
185: }
186: });
187: completeEx.addActionListener(new ActionListener() {
188: public void actionPerformed(ActionEvent e) {
189: UnitTestBuilder.requireCompleteExecution = completeEx
190: .isSelected();
191: }
192: });
193: JButton exit = new JButton("Exit");
194: exit.addActionListener(new ActionListener() {
195: public void actionPerformed(ActionEvent e) {
196: setSimplifyCount(simplifyDataTupleNumber.getText());
197: setVisible(false);
198: dispose();
199: instance = null;
200: }
201: });
202: buttonPanel.add(completeEx);
203: buttonPanel.add(cogent);
204: buttonPanel.add(simplify);
205: if (ModelGenerator.decProdForTestGen == ModelGenerator.SIMPLIFY) {
206: buttonPanel.add(simplifyDataTupleNumber);
207: }
208: buttonPanel.add(exit);
209: getContentPane().add(buttonPanel);
210: }
211:
212: public void setSimplifyCount(String s) {
213: try {
214: SimplifyModelGenerator.modelLimit = Integer.parseInt(s);
215: } catch (NumberFormatException ex) {
216: System.out.println(ex);
217: // do nothing
218: }
219: }
220:
221: public StringBuffer getLatestTests() {
222: return latestTests;
223: }
224:
225: public void setLatestTests(StringBuffer latest) {
226: latestTests = latest;
227: }
228:
229: private void createTest(Object[] pms) {
230: try {
231: String test;
232: if (pms == null) {
233: test = testBuilder.createTestForProof(mediator
234: .getProof());
235: latestTests.append(test + " ");
236: mediator.testCaseConfirmation(test);
237: } else {
238: SetOfProgramMethod pmSet = SetAsListOfProgramMethod.EMPTY_SET;
239: for (int i = 0; i < pms.length; i++) {
240: pmSet = pmSet.add((ProgramMethod) pms[i]);
241: }
242: test = testBuilder.createTestForProof(mediator
243: .getProof(), pmSet);
244: latestTests.append(test + " ");
245: mediator.testCaseConfirmation(test);
246: }
247: } catch (Exception e) {
248: ExtList l = new ExtList();
249: l.add(e);
250: new ExceptionDialog(Main.getInstance(), l);
251: }
252: }
253:
254: }
|