- Just some generification.
[speedith:speedith.git] / devel / Speedith / src / speedith / ui / SpeedithMainForm.java
1 /*
2  *   Project: Speedith
3  * 
4  * File name: SpeedithMainForm.java
5  *    Author: Matej Urbas [matej.urbas@gmail.com]
6  * 
7  *  Copyright © 2011 Matej Urbas
8  * 
9  * Permission is hereby granted, free of charge, to any person obtaining a copy
10  * of this software and associated documentation files (the "Software"), to deal
11  * in the Software without restriction, including without limitation the rights
12  * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13  * copies of the Software, and to permit persons to whom the Software is
14  * furnished to do so, subject to the following conditions:
15  * 
16  * The above copyright notice and this permission notice shall be included in
17  * all copies or substantial portions of the Software.
18  * 
19  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24  * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
25  * THE SOFTWARE.
26  */
27
28 /*
29  * SpeedithMainForm.java
30  *
31  * Created on 07-Nov-2011, 10:47:11
32  */
33 package speedith.ui;
34
35 import java.awt.Image;
36 import java.io.IOException;
37 import java.io.InputStream;
38 import java.util.ArrayList;
39 import java.util.Arrays;
40 import java.util.Set;
41 import java.util.logging.Level;
42 import java.util.logging.Logger;
43 import javax.imageio.ImageIO;
44 import javax.swing.*;
45 import speedith.core.lang.*;
46 import speedith.core.lang.reader.SpiderDiagramsReader;
47 import speedith.core.reasoning.*;
48 import speedith.core.reasoning.args.RuleArg;
49 import speedith.core.reasoning.args.SpiderRegionArg;
50 import speedith.core.reasoning.args.SubgoalIndexArg;
51 import speedith.core.reasoning.rules.AddFeet;
52 import speedith.core.reasoning.rules.SplitSpiders;
53 import speedith.ui.selection.SelectionDialog;
54 import static speedith.i18n.Translations.*;
55 import speedith.ui.rules.InteractiveRuleApplication;
56
57 /**
58  * The main application window of Speedith.
59  *
60  * @author Matej Urbas [matej.urbas@gmail.com]
61  */
62 public class SpeedithMainForm extends javax.swing.JFrame {
63
64     // <editor-fold defaultstate="collapsed" desc="Constants">
65     private static final String[] SpeedithIcons = {
66         "SpeedithIconVennDiagram-16.png",
67         "SpeedithIconVennDiagram-32.png",
68         "SpeedithIconVennDiagram-48.png",
69         "SpeedithIconVennDiagram-64.png",
70         "SpeedithIconVennDiagram-128.png"
71     };
72     /**
73      * The height of the particular goals panels in this form.
74      */
75     private static final int GoalsHeight = 250;
76     // </editor-fold>
77
78     // <editor-fold defaultstate="collapsed" desc="Constructor">
79     /**
80      * Creates new form SpeedithMainForm
81      */
82     public SpeedithMainForm() {
83         initComponents();
84         try {
85             ArrayList<Image> icons = new ArrayList<Image>();
86             // Set the icon of this window:
87             for (String path : SpeedithIcons) {
88                 InputStream imgStream = this.getClass().getResourceAsStream(path);
89                 icons.add(ImageIO.read(imgStream));
90             }
91             setIconImages(icons);
92         } catch (IOException ex) {
93             Logger.getLogger(SpeedithMainForm.class.getName()).log(Level.WARNING, "Speedith's icons could not have been loaded.", ex);
94         }
95     }
96     // </editor-fold>
97
98     // <editor-fold defaultstate="collapsed" desc="Auto-generated code">
99     /**
100      * This method is called from within the constructor to initialize the form.
101      * WARNING: Do NOT modify this code. The content of this method is always
102      * regenerated by the Form Editor.
103      */
104     @SuppressWarnings("unchecked")
105     // <editor-fold defaultstate="collapsed" desc="Generated Code">//GEN-BEGIN:initComponents
106     private void initComponents() {
107         java.awt.GridBagConstraints gridBagConstraints;
108
109         javax.swing.JSplitPane mainSplitPane = new javax.swing.JSplitPane();
110         proofPanel1 = new speedith.ui.ProofPanel();
111         pnlRulesSidePane = new javax.swing.JPanel();
112         lblAppliedRules = new javax.swing.JLabel();
113         scrlPnlAppliedRules = new javax.swing.JScrollPane();
114         lstAppliedRules = new javax.swing.JList();
115         menuBar = new javax.swing.JMenuBar();
116         fileMenu = new javax.swing.JMenu();
117         exitMenuItem = new javax.swing.JMenuItem();
118         drawMenu = new javax.swing.JMenu();
119         jMenuItem1 = new javax.swing.JMenuItem();
120         jMenuItem2 = new javax.swing.JMenuItem();
121         jMenuItem3 = new javax.swing.JMenuItem();
122         rulesMenu = new javax.swing.JMenu();
123
124         setDefaultCloseOperation(javax.swing.WindowConstants.EXIT_ON_CLOSE);
125         setTitle("Speedith");
126
127         proofPanel1.setMinimumSize(new java.awt.Dimension(750, 300));
128         proofPanel1.setPreferredSize(new java.awt.Dimension(750, 300));
129         mainSplitPane.setLeftComponent(proofPanel1);
130
131         pnlRulesSidePane.setMinimumSize(new java.awt.Dimension(100, 300));
132         pnlRulesSidePane.setPreferredSize(new java.awt.Dimension(100, 300));
133         pnlRulesSidePane.setLayout(new java.awt.GridBagLayout());
134
135         lblAppliedRules.setLabelFor(lstAppliedRules);
136         lblAppliedRules.setText(i18n("MAIN_FORM_RULE_LIST")); // NOI18N
137         gridBagConstraints = new java.awt.GridBagConstraints();
138         gridBagConstraints.gridx = 0;
139         gridBagConstraints.gridy = 0;
140         gridBagConstraints.fill = java.awt.GridBagConstraints.HORIZONTAL;
141         gridBagConstraints.anchor = java.awt.GridBagConstraints.NORTHWEST;
142         gridBagConstraints.weightx = 1.0;
143         gridBagConstraints.insets = new java.awt.Insets(0, 3, 0, 0);
144         pnlRulesSidePane.add(lblAppliedRules, gridBagConstraints);
145
146         lstAppliedRules.setModel(getRulesList());
147         lstAppliedRules.addMouseListener(new java.awt.event.MouseAdapter() {
148             public void mouseClicked(java.awt.event.MouseEvent evt) {
149                 onRuleItemClicked(evt);
150             }
151         });
152         scrlPnlAppliedRules.setViewportView(lstAppliedRules);
153
154         gridBagConstraints = new java.awt.GridBagConstraints();
155         gridBagConstraints.gridx = 0;
156         gridBagConstraints.gridy = 1;
157         gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH;
158         gridBagConstraints.anchor = java.awt.GridBagConstraints.NORTHWEST;
159         gridBagConstraints.weightx = 1.0;
160         gridBagConstraints.weighty = 1.0;
161         gridBagConstraints.insets = new java.awt.Insets(6, 0, 0, 0);
162         pnlRulesSidePane.add(scrlPnlAppliedRules, gridBagConstraints);
163
164         mainSplitPane.setRightComponent(pnlRulesSidePane);
165
166         fileMenu.setMnemonic('F');
167         fileMenu.setText("File");
168
169         exitMenuItem.setAccelerator(javax.swing.KeyStroke.getKeyStroke(java.awt.event.KeyEvent.VK_Q, java.awt.event.InputEvent.CTRL_MASK));
170         exitMenuItem.setMnemonic('x');
171         exitMenuItem.setText("Exit");
172         exitMenuItem.addActionListener(new java.awt.event.ActionListener() {
173             public void actionPerformed(java.awt.event.ActionEvent evt) {
174                 exitMenuItemActionPerformed(evt);
175             }
176         });
177         fileMenu.add(exitMenuItem);
178
179         menuBar.add(fileMenu);
180
181         drawMenu.setMnemonic('D');
182         drawMenu.setText("Draw");
183
184         jMenuItem1.setAccelerator(javax.swing.KeyStroke.getKeyStroke(java.awt.event.KeyEvent.VK_1, java.awt.event.InputEvent.CTRL_MASK));
185         jMenuItem1.setMnemonic(i18n("MAIN_FORM_USE_EXAMPLE1_MNEMONIC").charAt(0));
186         jMenuItem1.setText(i18n("MAIN_FORM_USE_EXAMPLE1")); // NOI18N
187         jMenuItem1.addActionListener(new java.awt.event.ActionListener() {
188             public void actionPerformed(java.awt.event.ActionEvent evt) {
189                 jMenuItem1ActionPerformed(evt);
190             }
191         });
192         drawMenu.add(jMenuItem1);
193
194         jMenuItem2.setAccelerator(javax.swing.KeyStroke.getKeyStroke(java.awt.event.KeyEvent.VK_2, java.awt.event.InputEvent.CTRL_MASK));
195         jMenuItem2.setMnemonic(i18n("MAIN_FORM_USE_EXAMPLE2_MNEMONIC").charAt(0));
196         jMenuItem2.setText(i18n("MAIN_FORM_USE_EXAMPLE2")); // NOI18N
197         jMenuItem2.addActionListener(new java.awt.event.ActionListener() {
198             public void actionPerformed(java.awt.event.ActionEvent evt) {
199                 jMenuItem2ActionPerformed(evt);
200             }
201         });
202         drawMenu.add(jMenuItem2);
203
204         jMenuItem3.setAccelerator(javax.swing.KeyStroke.getKeyStroke(java.awt.event.KeyEvent.VK_3, java.awt.event.InputEvent.CTRL_MASK));
205         jMenuItem3.setMnemonic(i18n("MAIN_FORM_USE_EXAMPLE3_MNEMONIC").charAt(0));
206         jMenuItem3.setText(i18n("MAIN_FORM_USE_EXAMPLE3")); // NOI18N
207         jMenuItem3.addActionListener(new java.awt.event.ActionListener() {
208             public void actionPerformed(java.awt.event.ActionEvent evt) {
209                 jMenuItem3ActionPerformed(evt);
210             }
211         });
212         drawMenu.add(jMenuItem3);
213
214         menuBar.add(drawMenu);
215
216         rulesMenu.setMnemonic('R');
217         rulesMenu.setText("Rules");
218         menuBar.add(rulesMenu);
219
220         setJMenuBar(menuBar);
221
222         javax.swing.GroupLayout layout = new javax.swing.GroupLayout(getContentPane());
223         getContentPane().setLayout(layout);
224         layout.setHorizontalGroup(
225             layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
226             .addComponent(mainSplitPane, javax.swing.GroupLayout.Alignment.TRAILING, javax.swing.GroupLayout.DEFAULT_SIZE, 995, Short.MAX_VALUE)
227         );
228         layout.setVerticalGroup(
229             layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
230             .addComponent(mainSplitPane, javax.swing.GroupLayout.Alignment.TRAILING, javax.swing.GroupLayout.DEFAULT_SIZE, 406, Short.MAX_VALUE)
231         );
232
233         pack();
234     }// </editor-fold>//GEN-END:initComponents
235
236     private void exitMenuItemActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_exitMenuItemActionPerformed
237         this.dispose();
238     }//GEN-LAST:event_exitMenuItemActionPerformed
239
240     private void jMenuItem1ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jMenuItem1ActionPerformed
241         proofPanel1.newProof(Goals.createGoalsFrom(getExampleA()));
242     }//GEN-LAST:event_jMenuItem1ActionPerformed
243
244     private void jMenuItem2ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jMenuItem2ActionPerformed
245         proofPanel1.newProof(Goals.createGoalsFrom(getExampleB()));
246     }//GEN-LAST:event_jMenuItem2ActionPerformed
247
248     private void jMenuItem3ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jMenuItem3ActionPerformed
249         proofPanel1.newProof(Goals.createGoalsFrom(getExampleC()));
250     }//GEN-LAST:event_jMenuItem3ActionPerformed
251
252     private void onRuleItemClicked(java.awt.event.MouseEvent evt) {//GEN-FIRST:event_onRuleItemClicked
253         if (evt.getClickCount() == 2) {
254             if (!proofPanel1.isFinished()) {
255                 int index = lstAppliedRules.locationToIndex(evt.getPoint());
256                 DefaultComboBoxModel model = (DefaultComboBoxModel) lstAppliedRules.getModel();
257                 InfRuleListItem selectedRule = (InfRuleListItem) model.getElementAt(index);
258                 applyRule(selectedRule);
259             }
260         }
261     }//GEN-LAST:event_onRuleItemClicked
262
263     /**
264      * @param args the command line arguments
265      */
266     public static void main(String args[]) {
267         /*
268          * Set the Nimbus look and feel
269          */
270         //<editor-fold defaultstate="collapsed" desc=" Look and feel setting code (optional) ">
271         /*
272          * If Nimbus (introduced in Java SE 6) is not available, stay with the
273          * default look and feel. For details see
274          * http://download.oracle.com/javase/tutorial/uiswing/lookandfeel/plaf.html
275          */
276         try {
277             for (javax.swing.UIManager.LookAndFeelInfo info : javax.swing.UIManager.getInstalledLookAndFeels()) {
278                 if ("Nimbus".equals(info.getName())) {
279                     javax.swing.UIManager.setLookAndFeel(info.getClassName());
280                     break;
281                 }
282             }
283         } catch (ClassNotFoundException ex) {
284             java.util.logging.Logger.getLogger(SpeedithMainForm.class.getName()).log(java.util.logging.Level.SEVERE, null, ex);
285         } catch (InstantiationException ex) {
286             java.util.logging.Logger.getLogger(SpeedithMainForm.class.getName()).log(java.util.logging.Level.SEVERE, null, ex);
287         } catch (IllegalAccessException ex) {
288             java.util.logging.Logger.getLogger(SpeedithMainForm.class.getName()).log(java.util.logging.Level.SEVERE, null, ex);
289         } catch (javax.swing.UnsupportedLookAndFeelException ex) {
290             java.util.logging.Logger.getLogger(SpeedithMainForm.class.getName()).log(java.util.logging.Level.SEVERE, null, ex);
291         }
292         //</editor-fold>
293
294         /*
295          * Create and display the form
296          */
297         java.awt.EventQueue.invokeLater(new Runnable() {
298
299             public void run() {
300                 new SpeedithMainForm().setVisible(true);
301             }
302         });
303     }
304     // Variables declaration - do not modify//GEN-BEGIN:variables
305     private javax.swing.JMenu drawMenu;
306     private javax.swing.JMenuItem exitMenuItem;
307     private javax.swing.JMenu fileMenu;
308     private javax.swing.JMenuItem jMenuItem1;
309     private javax.swing.JMenuItem jMenuItem2;
310     private javax.swing.JMenuItem jMenuItem3;
311     private javax.swing.JLabel lblAppliedRules;
312     private javax.swing.JList lstAppliedRules;
313     private javax.swing.JMenuBar menuBar;
314     private javax.swing.JPanel pnlRulesSidePane;
315     private speedith.ui.ProofPanel proofPanel1;
316     private javax.swing.JMenu rulesMenu;
317     private javax.swing.JScrollPane scrlPnlAppliedRules;
318     // End of variables declaration//GEN-END:variables
319     // </editor-fold>
320
321     // <editor-fold defaultstate="collapsed" desc="Spider Diagram Examples">
322     /**
323      * The first main example used in most of our papers. Useful for testing the
324      * rules: split spider, add feet, idempotency, and tautology of implication.
325      *
326      * @return
327      */
328     public static CompoundSpiderDiagram getExampleA() {
329         PrimarySpiderDiagram psd1 = getSDExample1();
330         PrimarySpiderDiagram psd2 = getSDExample7();
331         CompoundSpiderDiagram csd = SpiderDiagrams.createCompoundSD(Operator.Implication, psd1, psd2);
332         return csd;
333     }
334
335     /**
336      * The second example. Useful for testing the rule: idempotency.
337      *
338      * @return
339      */
340     public static SpiderDiagram getExampleB() {
341         try {
342             return SpiderDiagramsReader.readSpiderDiagram("BinarySD {arg1 = PrimarySD { spiders = [\"s\", \"s'\"], sh_zones = [], habitats = [(\"s\", [([\"A\", \"B\"], [])]), (\"s'\", [([\"A\"], [\"B\"]), ([\"B\"], [\"A\"])])]}, arg2 = PrimarySD { spiders = [\"s\", \"s'\"], sh_zones = [], habitats = [(\"s'\", [([\"A\", \"B\"], [])]), (\"s\", [([\"A\"], [\"B\"]), ([\"B\"], [\"A\"])])]}, operator = \"op &\" }");
343         } catch (Exception ex) {
344             throw new RuntimeException();
345         }
346     }
347
348     /**
349      * The third example. Useful for testing the rule: implication tautology.
350      *
351      * @return
352      */
353     public static SpiderDiagram getExampleC() {
354         try {
355             return SpiderDiagramsReader.readSpiderDiagram("BinarySD {arg1 = PrimarySD { spiders = [\"s\", \"s'\"], sh_zones = [], habitats = [(\"s\", [([\"A\", \"B\"], [])]), (\"s'\", [([\"A\"], [\"B\"]), ([\"B\"], [\"A\"])])]}, arg2 = PrimarySD { spiders = [\"s\", \"s'\"], sh_zones = [], habitats = [(\"s'\", [([\"A\", \"B\"], [])]), (\"s\", [([\"A\"], [\"B\"]), ([\"B\"], [\"A\"])])]}, operator = \"op -->\" }");
356         } catch (Exception ex) {
357             throw new RuntimeException();
358         }
359     }
360
361     /**
362      * s1: A, B s2: AB
363      *
364      * @return
365      */
366     public static PrimarySpiderDiagram getSDExample1() {
367         PrimarySpiderDiagram emptyPSD = SpiderDiagrams.createPrimarySD(null, null, null, null);
368         Region s1Region = regionA_B__B_A();
369         Region s2Region = regionAB();
370         emptyPSD = emptyPSD.addSpider("t1", s1Region);
371         return emptyPSD.addSpider("t2", s2Region);
372     }
373
374     /**
375      * s1: A s2: AB
376      *
377      * @return
378      */
379     public static PrimarySpiderDiagram getSDExample5() {
380         PrimarySpiderDiagram emptyPSD = SpiderDiagrams.createPrimarySD(null, null, null, null);
381         Region s1Region = regionA_B();
382         Region s2Region = regionAB();
383         emptyPSD = emptyPSD.addSpider("s1", s1Region);
384         return emptyPSD.addSpider("s2", s2Region);
385     }
386
387     /**
388      * s1: B s2: AB
389      *
390      * @return
391      */
392     public static PrimarySpiderDiagram getSDExample6() {
393         PrimarySpiderDiagram emptyPSD = SpiderDiagrams.createPrimarySD(null, null, null, null);
394         Region s1Region = regionB_A();
395         Region s2Region = regionAB();
396         emptyPSD = emptyPSD.addSpider("s1", s1Region);
397         return emptyPSD.addSpider("s2", s2Region);
398     }
399
400     /**
401      * s1: A, AB s2: B, AB
402      *
403      * @return
404      */
405     public static PrimarySpiderDiagram getSDExample7() {
406         PrimarySpiderDiagram emptyPSD = SpiderDiagrams.createPrimarySD(null, null, null, null);
407         Region s1Region = regionA_B__AB();
408         Region s2Region = regionB_A__AB();
409         emptyPSD = emptyPSD.addSpider("u1", s1Region);
410         return emptyPSD.addSpider("u2", s2Region);
411     }
412
413     /**
414      * s1: B, AB s2: AB
415      *
416      * @return
417      */
418     public static PrimarySpiderDiagram getSDExample8() {
419         PrimarySpiderDiagram emptyPSD = SpiderDiagrams.createPrimarySD(null, null, null, null);
420         Region s1Region = regionB_A__AB();
421         Region s2Region = regionAB();
422         emptyPSD = emptyPSD.addSpider("s1", s1Region);
423         return emptyPSD.addSpider("s2", s2Region);
424     }
425
426     /**
427      * s1: B, AB s2: A, AB
428      *
429      * @return
430      */
431     public static PrimarySpiderDiagram getSDExample9() {
432         PrimarySpiderDiagram emptyPSD = SpiderDiagrams.createPrimarySD(null, null, null, null);
433         Region s1Region = regionB_A__AB();
434         Region s2Region = regionA_B__AB();
435         emptyPSD = emptyPSD.addSpider("s1", s1Region);
436         return emptyPSD.addSpider("s2", s2Region);
437     }
438
439     /**
440      * s1: A, AB s2: AB
441      *
442      * @return
443      */
444     public static PrimarySpiderDiagram getSDExample10() {
445         PrimarySpiderDiagram emptyPSD = SpiderDiagrams.createPrimarySD(null, null, null, null);
446         Region s1Region = regionA_B__AB();
447         Region s2Region = regionAB();
448         emptyPSD = emptyPSD.addSpider("s1", s1Region);
449         return emptyPSD.addSpider("s2", s2Region);
450     }
451
452     public static Goals getStep0() {
453         CompoundSpiderDiagram csd = getExampleA();
454         return Goals.createGoalsFrom(csd);
455     }
456
457     public static Goals getStep1() {
458         RuleArg ruleArg = new SpiderRegionArg(0, 1, "s1", regionA_B());
459         return applyInferenceRule(SplitSpiders.InferenceRuleName, ruleArg, getStep0());
460 //        PrimarySpiderDiagram psd1 = getSDExample5();
461 //        PrimarySpiderDiagram psd2 = getSDExample6();
462 //        PrimarySpiderDiagram psd3 = getSDExample7();
463 //        CompoundSpiderDiagram csd1 = SpiderDiagrams.createCompoundSD(Operator.Disjunction, psd1, psd2);
464 //        CompoundSpiderDiagram csd2 = SpiderDiagrams.createCompoundSD(Operator.Implication, csd1, psd3);
465 //        return csd2;
466     }
467
468     public static Goals getStep2() {
469         RuleArg ruleArg = new SpiderRegionArg(0, 2, "s1", regionAB());
470         return applyInferenceRule(AddFeet.InferenceRuleName, ruleArg, getStep1());
471 //        PrimarySpiderDiagram psd1 = getSDExample10();
472 //        PrimarySpiderDiagram psd2 = getSDExample6();
473 //        PrimarySpiderDiagram psd3 = getSDExample7();
474 //        CompoundSpiderDiagram csd1 = SpiderDiagrams.createCompoundSD(Operator.Disjunction, psd1, psd2);
475 //        CompoundSpiderDiagram csd2 = SpiderDiagrams.createCompoundSD(Operator.Implication, csd1, psd3);
476 //        return csd2;
477     }
478
479     public static Goals getStep3() {
480         RuleArg ruleArg = new SpiderRegionArg(0, 3, "s1", regionAB());
481         return applyInferenceRule(AddFeet.InferenceRuleName, ruleArg, getStep2());
482 //        PrimarySpiderDiagram psd1 = getSDExample10();
483 //        PrimarySpiderDiagram psd2 = getSDExample8();
484 //        PrimarySpiderDiagram psd3 = getSDExample7();
485 //        CompoundSpiderDiagram csd1 = SpiderDiagrams.createCompoundSD(Operator.Disjunction, psd1, psd2);
486 //        CompoundSpiderDiagram csd2 = SpiderDiagrams.createCompoundSD(Operator.Implication, csd1, psd3);
487 //        return csd2;
488     }
489
490     public static Goals getStep4() {
491         RuleArg ruleArg = new SpiderRegionArg(0, 2, "s2", regionB_A());
492         return applyInferenceRule(AddFeet.InferenceRuleName, ruleArg, getStep3());
493 //        PrimarySpiderDiagram psd1 = getSDExample7();
494 //        PrimarySpiderDiagram psd2 = getSDExample8();
495 //        PrimarySpiderDiagram psd3 = getSDExample7();
496 //        CompoundSpiderDiagram csd1 = SpiderDiagrams.createCompoundSD(Operator.Disjunction, psd1, psd2);
497 //        CompoundSpiderDiagram csd2 = SpiderDiagrams.createCompoundSD(Operator.Implication, csd1, psd3);
498 //        return csd2;
499     }
500
501     public static CompoundSpiderDiagram getSDExample2() {
502         PrimarySpiderDiagram psd1 = getSDExample1();
503         PrimarySpiderDiagram psd2 = getSDExample1();
504         CompoundSpiderDiagram csd = SpiderDiagrams.createCompoundSD(Operator.Equivalence, psd1, psd2);
505         return csd;
506     }
507
508     public static NullSpiderDiagram getSDExample3() {
509         return SpiderDiagrams.createNullSD();
510     }
511
512     public static CompoundSpiderDiagram getSDExample4() {
513         PrimarySpiderDiagram sd1 = getSDExample1();
514         SpiderDiagram sd2 = getSDExample2();
515         CompoundSpiderDiagram csd = SpiderDiagrams.createCompoundSD(Operator.Conjunction, sd1, sd2);
516         return csd;
517     }
518
519     public static CompoundSpiderDiagram getSDExample11() {
520         SpiderDiagram sd1 = getSDExample4();
521         SpiderDiagram sd2 = SpiderDiagrams.createNullSD();
522         CompoundSpiderDiagram csd = SpiderDiagrams.createCompoundSD(Operator.Equivalence, sd1, sd2);
523         return csd;
524     }
525     // </editor-fold>
526
527     //<editor-fold defaultstate="collapsed" desc="UI Refresh Methods">
528     private ComboBoxModel<InfRuleListItem> getRulesComboList() {
529         Set<String> knownInferenceRules = InferenceRules.getKnownInferenceRules();
530         InfRuleListItem[] infRules = new InfRuleListItem[knownInferenceRules.size()];
531         int i = 0;
532         for (String providerName : knownInferenceRules) {
533             infRules[i++] = new InfRuleListItem(InferenceRules.getProvider(providerName));
534         }
535         Arrays.sort(infRules);
536         return new DefaultComboBoxModel<InfRuleListItem>(infRules);
537     }
538
539     private ListModel<InfRuleListItem> getRulesList() {
540         Set<String> knownInferenceRules = InferenceRules.getKnownInferenceRules();
541         InfRuleListItem[] infRules = new InfRuleListItem[knownInferenceRules.size()];
542         int i = 0;
543         for (String providerName : knownInferenceRules) {
544             infRules[i++] = new InfRuleListItem(InferenceRules.getProvider(providerName));
545         }
546         Arrays.sort(infRules);
547         return new DefaultComboBoxModel<InfRuleListItem>(infRules);
548
549     }
550
551     private static class InfRuleListItem implements Comparable<InfRuleListItem> {
552
553         private final InferenceRuleProvider<? extends RuleArg> infRuleProvider;
554
555         public InfRuleListItem(InferenceRuleProvider<? extends RuleArg> infRuleProvider) {
556             if (infRuleProvider == null) {
557                 throw new IllegalArgumentException(speedith.core.i18n.Translations.i18n("GERR_NULL_ARGUMENT", "infRuleProvider"));
558             }
559             this.infRuleProvider = infRuleProvider;
560         }
561
562         public InferenceRuleProvider<? extends RuleArg> getInfRuleProvider() {
563             return infRuleProvider;
564         }
565
566         @Override
567         public String toString() {
568             return infRuleProvider.getPrettyName();
569         }
570
571         public int compareTo(InfRuleListItem o) {
572             return infRuleProvider.toString().compareToIgnoreCase(o.toString());
573         }
574     }
575     //</editor-fold>
576
577     // <editor-fold defaultstate="collapsed" desc="Helper Methods">
578     private static Goals applyInferenceRule(String infRuleName, RuleArg ruleArg, Goals goals0) {
579         InferenceRule<? extends RuleArg> infRule = InferenceRules.getInferenceRule(infRuleName);
580         try {
581             RuleApplicationResult rar = infRule.apply(ruleArg, goals0);
582             goals0 = rar.getGoals();
583         } catch (RuleApplicationException ex) {
584             throw new RuntimeException(ex);
585         }
586         return goals0;
587     }
588
589     private static Region regionA_B() {
590         return new Region(zoneA_B());
591     }
592
593     private static Region regionA_B__AB() {
594         return new Region(zoneA_B(), zoneAB());
595     }
596
597     private static Region regionA_B__B_A() {
598         return new Region(zoneA_B(), zoneB_A());
599     }
600
601     private static Region regionB_A() {
602         return new Region(zoneB_A());
603     }
604
605     private static Region regionB_A__AB() {
606         return new Region(zoneB_A(), zoneAB());
607     }
608
609     private static Region regionAB() {
610         return new Region(zoneAB());
611     }
612
613     private static Zone zoneAB() {
614         return Zone.fromInContours("A", "B");
615     }
616
617     private static Zone zoneA_B() {
618         return Zone.fromInContours("A").withOutContours("B");
619     }
620
621     private static Zone zoneB_A() {
622         return Zone.fromInContours("B").withOutContours("A");
623     }
624
625     private void applyRule(InfRuleListItem selectedRule) {
626         Proof proof = proofPanel1;
627         int subgoalIndex = 0;
628         try {
629             InteractiveRuleApplication.applyRuleInteractively(this, selectedRule.getInfRuleProvider().getInferenceRule(), subgoalIndex, proof);
630         } catch (Exception ex) {
631             JOptionPane.showMessageDialog(this, ex.getLocalizedMessage());
632         }
633     }
634     // </editor-fold>
635 }