← Back to branch summary

~yrke/tapaal/tapaal-fix1764383-java9macoslookandfeel

« back to all changes in this revision

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

merged in branch  lp:~tapaal-contributor/tapaal/reachability-query-dialog-stubborn-reduction adding partial order reduction for verifydtapn

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/widgets/QueryDialog.java
228
228
        private JCheckBox useGCD;
229
229
        private JCheckBox useOverApproximation;
230
230
        private JCheckBox useReduction;
 
231
        private JCheckBox useStubbornReduction;
231
232
        
232
233
        // Approximation options panel
233
234
        private JPanel overApproximationOptionsPanel;
272
273
        private static Boolean advancedView = false;
273
274
        
274
275
        private static boolean hasForcedDisabledTimeDarts = false;
 
276
        private static boolean hasForcedDisabledStubbornReduction = false;
275
277
        private static boolean hasForcedDisabledGCD = false;
276
278
        private static boolean disableSymmetryUpdate = false;
277
279
 
329
331
        private final static String TOOL_TIP_SELECT_INCLUSION_PLACES = "Manually select places considered for the inclusion check.";
330
332
        private final static String TOOL_TIP_TIME_DARTS = "Use the time dart optimization";
331
333
        private final static String TOOL_TIP_PTRIE = "Use the PTrie memory optimization";
 
334
        private final static String TOOL_TIP_STUBBORN_REDUCTION = "Apply partial order reduction (only for EF and AG queries and when Time Darts are disabled).";
332
335
        private final static String TOOL_TIP_GCD = "Calculate greatest common divisor to minimize constants in the model";
333
336
        private final static String TOOL_TIP_OVERAPPROX = "Run linear over-approximation check for EF and AG queries";  // TODO: write tooltip
334
337
 
414
417
                boolean overApproximation = useOverApproximation.isSelected();
415
418
                boolean reduction = useReduction.isSelected();
416
419
 
417
 
                TAPNQuery query = new TAPNQuery(name, capacity, newProperty.copy(), traceOption, searchOption, reductionOptionToSet, symmetry, gcd, timeDarts, pTrie, overApproximation, reduction, /* hashTableSizeToSet */ null, /* extrapolationOptionToSet */null, inclusionPlaces, overApproximationEnable.isSelected(), underApproximationEnable.isSelected(), (Integer) overApproximationDenominator.getValue());
418
 
                
 
420
                TAPNQuery query = new TAPNQuery(
 
421
                                name,
 
422
                                capacity,
 
423
                                newProperty.copy(),
 
424
                                traceOption,
 
425
                                searchOption,
 
426
                                reductionOptionToSet,
 
427
                                symmetry,
 
428
                                gcd,
 
429
                                timeDarts,
 
430
                                pTrie,
 
431
                                overApproximation,
 
432
                                reduction,
 
433
                                /* hashTableSizeToSet */ null,
 
434
                                /* extrapolationOptionToSet */null,
 
435
                                inclusionPlaces,
 
436
                                overApproximationEnable.isSelected(),
 
437
                                underApproximationEnable.isSelected(),
 
438
                                (Integer) overApproximationDenominator.getValue()
 
439
                );
 
440
 
 
441
                query.setUseStubbornReduction(useStubbornReduction.isSelected());
 
442
 
419
443
                if(reductionOptionToSet.equals(ReductionOption.VerifyTAPN)){
420
444
                        query.setDiscreteInclusion(discreteInclusion.isSelected());
421
445
                }
728
752
                        }
729
753
            useTimeDarts.setEnabled(true);     
730
754
        }
 
755
 
 
756
        if(useStubbornReduction != null){
 
757
                        if(hasForcedDisabledStubbornReduction){
 
758
                                hasForcedDisabledStubbornReduction = false;
 
759
                                useStubbornReduction.setSelected(true);
 
760
                        }
 
761
                        useStubbornReduction.setEnabled(true);
 
762
                }
731
763
                
732
764
                if(useGCD != null){
733
765
                        if(hasForcedDisabledGCD){
1080
1112
                symmetryReduction.setSelected(symmetry);
1081
1113
                useTimeDarts.setSelected(queryToCreateFrom.useTimeDarts());
1082
1114
                usePTrie.setSelected(queryToCreateFrom.usePTrie());
 
1115
                useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled());
1083
1116
                useGCD.setSelected(queryToCreateFrom.useGCD());
1084
1117
                useOverApproximation.setSelected(queryToCreateFrom.useOverApproximation());
1085
1118
                useReduction.setSelected(queryToCreateFrom.useReduction());
2324
2357
                reductionOptionsPanel.add(selectInclusionPlacesButton, gbc);
2325
2358
 
2326
2359
                useTimeDarts = new JCheckBox("Use Time Darts");
2327
 
                useTimeDarts.setSelected(true);
 
2360
                useTimeDarts.setSelected(false);
2328
2361
                useTimeDarts.setToolTipText(TOOL_TIP_TIME_DARTS);
 
2362
                useTimeDarts.addActionListener(new ActionListener() {
 
2363
                        public void actionPerformed(ActionEvent e) {
 
2364
                                setEnabledOptionsAccordingToCurrentReduction();
 
2365
                        }
 
2366
                });
2329
2367
 
2330
2368
                gbc = new GridBagConstraints();
2331
 
                gbc.gridx = 2;
2332
 
                gbc.gridy = 1;
 
2369
                gbc.gridx = 3;
 
2370
                gbc.gridy = 2;
2333
2371
                gbc.anchor = GridBagConstraints.WEST;
2334
2372
                gbc.insets = new Insets(0,5,0,5);
2335
2373
                reductionOptionsPanel.add(useTimeDarts, gbc);
2374
2412
                gbc.insets = new Insets(0,5,0,5);
2375
2413
                reductionOptionsPanel.add(usePTrie, gbc);
2376
2414
 
 
2415
                useStubbornReduction = new JCheckBox("Use stubborn reduction");
 
2416
                useStubbornReduction.setSelected(true);
 
2417
                useStubbornReduction.setToolTipText(TOOL_TIP_STUBBORN_REDUCTION);
 
2418
 
 
2419
                gbc = new GridBagConstraints();
 
2420
                gbc.gridx = 2;
 
2421
                gbc.gridy = 1;
 
2422
                gbc.anchor = GridBagConstraints.WEST;
 
2423
                gbc.insets = new Insets(0,5,0,5);
 
2424
                reductionOptionsPanel.add(useStubbornReduction, gbc);
 
2425
 
2377
2426
                useOverApproximation = new JCheckBox("Use untimed state-equations check");
2378
2427
                useOverApproximation.setSelected(true);
2379
2428
                useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
2397
2446
                refreshQueryEditingButtons();
2398
2447
                refreshTraceOptions();
2399
2448
                refreshSymmetryReduction();
 
2449
                refreshStubbornReduction();
2400
2450
                refreshDiscreteOptions();
2401
2451
                refreshDiscreteInclusion();
2402
2452
                refreshOverApproximationOption();
2498
2548
        }
2499
2549
 
2500
2550
        private void refreshDiscreteOptions(){
2501
 
                useTimeDarts.setEnabled(true);
2502
 
                if(hasForcedDisabledTimeDarts){
2503
 
                        hasForcedDisabledTimeDarts = false;
2504
 
                        useTimeDarts.setSelected(true);
2505
 
                }
2506
 
                
2507
2551
                useReduction.setVisible(false);
2508
2552
                
2509
2553
                if(reductionOption.getSelectedItem() == null){
2510
2554
                        useGCD.setVisible(false);
2511
2555
                        usePTrie.setVisible(false);
 
2556
                        useStubbornReduction.setVisible(false);
2512
2557
                        useTimeDarts.setVisible(false);
2513
2558
                } 
2514
2559
                else if(((String)reductionOption.getSelectedItem()).equals(name_DISCRETE)) {
2515
2560
                        useGCD.setVisible(true);
2516
2561
                        usePTrie.setVisible(true);
 
2562
                        useStubbornReduction.setVisible(true);
2517
2563
                        useTimeDarts.setVisible(true);
 
2564
 
2518
2565
                        if(tapnNetwork.hasUrgentTransitions() || fastestTraceRadioButton.isSelected()){
2519
2566
                                hasForcedDisabledTimeDarts = useTimeDarts.isSelected();
2520
2567
                                useTimeDarts.setSelected(false);
2521
2568
                                useTimeDarts.setEnabled(false);
2522
2569
                        }
 
2570
 
 
2571
                        // Disable GCD calculation for EG/AF or deadlock queries
2523
2572
                        if(queryHasDeadlock() || getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")){
2524
2573
                                if(useGCD.isSelected()) hasForcedDisabledGCD = true;
2525
2574
                                useGCD.setSelected(false);
2532
2581
                                useTimeDarts.setSelected(false);
2533
2582
                                useTimeDarts.setEnabled(false);
2534
2583
                        }
 
2584
 
 
2585
                        // Disable stubborn reduction for EG/AF queries
 
2586
                        if(getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")){
 
2587
                                if(useStubbornReduction.isSelected())   hasForcedDisabledStubbornReduction = true;
 
2588
                                useStubbornReduction.setSelected(false);
 
2589
                                useStubbornReduction.setEnabled(false);
 
2590
                        }
2535
2591
                } else {
2536
2592
                        useGCD.setVisible(false);
2537
2593
                        usePTrie.setVisible(false);
 
2594
                        useStubbornReduction.setVisible(false);
2538
2595
                        useTimeDarts.setVisible(false);
2539
2596
 
2540
2597
//                      if(((String)reductionOption.getSelectedItem()).equals(name_UNTIMED)){
2543
2600
                }
2544
2601
        }
2545
2602
 
 
2603
        private void refreshStubbornReduction(){
 
2604
                if(useTimeDarts.isSelected()){
 
2605
                        useStubbornReduction.setSelected(false);
 
2606
                        useStubbornReduction.setEnabled(false);
 
2607
                } else {
 
2608
                        useStubbornReduction.setEnabled(true);
 
2609
                }
 
2610
        }
 
2611
 
2546
2612
 
2547
2613
        private void queryChanged(){
2548
2614
                setEnabledReductionOptions();