← Back to branch summary

~tapaal-contributor/tapaal/autodetect-lens-check2

« back to all changes in this revision

Viewing changes to src/pipe/gui/widgets/CTLQueryDialog.java

merged in  lp:~tapaal-contributor/tapaal/implement-game-ui-1884499 adding implementation of game UI 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/widgets/CTLQueryDialog.java
38
38
import javax.swing.undo.UndoableEdit;
39
39
import javax.swing.undo.UndoableEditSupport;
40
40
 
 
41
import dk.aau.cs.gui.TabContent;
41
42
import net.tapaal.swinghelpers.CustomJSpinner;
42
43
import pipe.dataLayer.DataLayer;
43
44
import pipe.dataLayer.NetWriter;
220
221
        private boolean isNetDegree2;
221
222
        private boolean hasInhibitorArcs;
222
223
        private InclusionPlaces inclusionPlaces;
 
224
    private TabContent.TAPNLens lens;
223
225
 
224
226
        private String name_verifyTAPN = "TAPAAL: Continous Engine (verifytapn)";
225
227
        private String name_COMBI = "UPPAAL: Optimized Broadcast Reduction";
327
329
        private final static String TOOL_TIP_QUERYTYPE = "Choose a query type";
328
330
        
329
331
        public CTLQueryDialog(EscapableDialog me, QueryDialogueOption option,
330
 
                        TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels) {
 
332
                        TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
331
333
                this.tapnNetwork = tapnNetwork;
332
334
                this.guiModels = guiModels;
333
335
                inclusionPlaces = queryToCreateFrom == null ? new InclusionPlaces() : queryToCreateFrom.inclusionPlaces();
334
 
                
 
336
                this.lens = lens;
 
337
 
335
338
                // Attempt to parse and possibly transform the string query using the manual edit parser
336
339
                try {
337
340
                        newProperty = TAPAALCTLQueryParser.parse(queryToCreateFrom.getProperty().toString());
458
461
                        return;
459
462
                }
460
463
 
461
 
                if(queryIsReachability()){
 
464
        if (lens.isGame()) {
 
465
            someTraceRadioButton.setEnabled(false);
 
466
            noTraceRadioButton.setEnabled(true);
 
467
        } else if(queryIsReachability()){
462
468
                        someTraceRadioButton.setEnabled(true);
463
469
                        noTraceRadioButton.setEnabled(true);
464
470
 
490
496
                return new IsReachabilityVisitor().isReachability(newProperty);
491
497
        }
492
498
 
493
 
        public static TAPNQuery showQueryDialogue(QueryDialogueOption option, TAPNQuery queryToRepresent, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels) {
 
499
        public static TAPNQuery showQueryDialogue(QueryDialogueOption option, TAPNQuery queryToRepresent, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
494
500
                if(CreateGui.getCurrentTab().network().hasWeights() && !CreateGui.getCurrentTab().network().isNonStrict()){
495
501
                        JOptionPane.showMessageDialog(CreateGui.getApp(),
496
502
                                        "No reduction option supports both strict intervals and weigthed arcs", 
505
511
                contentPane.setLayout(new GridBagLayout());
506
512
 
507
513
                // 2 Add query editor
508
 
                CTLQueryDialog queryDialogue = new CTLQueryDialog(guiDialog, option, queryToRepresent, tapnNetwork, guiModels);
 
514
                CTLQueryDialog queryDialogue = new CTLQueryDialog(guiDialog, option, queryToRepresent, tapnNetwork, guiModels, lens);
509
515
                contentPane.add(queryDialogue);
510
516
 
511
517
                guiDialog.setResizable(false);
697
703
        
698
704
        private void setEnabledReductionOptions(){
699
705
                reductionOption.removeAllItems();
700
 
                reductionOption.addItem(name_UNTIMED);
 
706
        if (!lens.isGame()) {
 
707
                    reductionOption.addItem(name_UNTIMED);
 
708
        }
701
709
        }
702
710
 
703
711
        private void updateSearchStrategies(){
727
735
                        breadthFirstSearch.setEnabled(false);
728
736
                }
729
737
                 */
730
 
                
 
738
 
 
739
        if (lens.isGame()) {
 
740
            heuristicSearch.setEnabled(false);
 
741
        }
 
742
 
731
743
                if(!currentselected.isEnabled()){
732
744
                        if(depthFirstSearch.isEnabled()){
733
745
                                depthFirstSearch.setSelected(true);
808
820
 
809
821
        }
810
822
 
 
823
    private void enableOnlyForAllBox() {
 
824
        existsBox.setEnabled(false);
 
825
        existsDiamond.setEnabled(false);
 
826
        forAllBox.setEnabled(true);
 
827
        forAllDiamond.setEnabled(false);
 
828
        existsUntil.setEnabled(false);
 
829
        existsNext.setEnabled(false);
 
830
        forAllUntil.setEnabled(false);
 
831
        forAllNext.setEnabled(false);
 
832
 
 
833
        conjunctionButton.setEnabled(true);
 
834
        disjunctionButton.setEnabled(true);
 
835
        negationButton.setEnabled(true);
 
836
        templateBox.setEnabled(true);
 
837
        placesTransitionsBox.setEnabled(true);
 
838
        relationalOperatorBox.setEnabled(true);
 
839
        placeMarking.setEnabled(true);
 
840
        truePredicateButton.setEnabled(true);
 
841
        falsePredicateButton.setEnabled(true);
 
842
        deadLockPredicateButton.setEnabled(true);
 
843
        setEnablednessOfAddPredicateButton();
 
844
        setEnablednessOfOperatorAndMarkingBoxes();
 
845
    }
 
846
 
811
847
        private void setEnablednessOfAddPredicateButton() {
812
848
                if (placesTransitionsBox.getSelectedItem() == null)
813
849
                        addPredicateButton.setEnabled(false);
814
850
                else
815
851
                        addPredicateButton.setEnabled(true);
816
852
        }
817
 
        
 
853
 
818
854
        private void setEnablednessOfOperatorAndMarkingBoxes(){
819
855
                if (transitionIsSelected()){
820
856
                        placeMarking.setVisible(false);
1189
1225
                queryScrollPane.setPreferredSize(d);
1190
1226
                queryScrollPane.setMinimumSize(d);
1191
1227
 
 
1228
                if (lens.isGame()) {
 
1229
                    queryScrollPane.setColumnHeaderView(new JLabel("control:"));
 
1230
        }
 
1231
 
1192
1232
                queryField.addMouseListener(new MouseAdapter() {
1193
1233
                        @Override
1194
1234
                        public void mouseReleased(MouseEvent e) {
1247
1287
                gbc.gridx = 0;
1248
1288
                gbc.gridy = 0;
1249
1289
                gbc.fill = GridBagConstraints.BOTH;
 
1290
                gbc.anchor = GridBagConstraints.CENTER;
1250
1291
                gbc.gridwidth = 4;
1251
1292
 
1252
1293
                queryPanel.add(queryScrollPane, gbc);
2290
2331
 
2291
2332
        private void refreshQueryEditingButtons() {
2292
2333
                if(currentSelection != null) {
2293
 
                        enableOnlyStateButtons();
2294
 
                        updateQueryButtonsAccordingToSelection();
 
2334
            if (lens.isGame()) {
 
2335
                enableOnlyForAllBox();
 
2336
            } else {
 
2337
                enableOnlyStateButtons();
 
2338
                updateQueryButtonsAccordingToSelection();
 
2339
            }
2295
2340
                }
2296
2341
        }
2297
2342
 
2386
2431
 
2387
2432
                                                if(reduction == ReductionOption.VerifyTAPN || reduction == ReductionOption.VerifyTAPNdiscreteVerification) {
2388
2433
                                                        VerifyTAPNExporter exporter = new VerifyTAPNExporter();
2389
 
                                                        exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery);
 
2434
                                                        exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens);
2390
2435
                                                } else if(reduction == ReductionOption.VerifyPN){
2391
2436
                                                        VerifyPNExporter exporter = new VerifyPNExporter();
2392
 
                                                        exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery);
 
2437
                                                        exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens);
2393
2438
                                                } else {
2394
2439
                                                        UppaalExporter exporter = new UppaalExporter();
2395
2440
                                                        try {