~tapaal-contributor/tapaal/refactor-remove-queries
» Revision
1092
: src/pipe/gui/widgets/QueryDialog.java
« back to all changes in this revision
Viewing changes to src/pipe/gui/widgets/QueryDialog.java
- browse files at revision 1092
- compare with another revision
- download diff
- download tarball
- view history from revision 1092
- Committer: lsaid
- Date: 2020-08-25 12:50:20 UTC
- mfrom: (1068.4.12 merge-query-dialogs)
- Revision ID: lena.said@hotmail.com-20200825125020-ubw6jdrluyt0cayo
Merged with trunk
added
removed
src/pipe/gui/widgets/QueryDialog.java
14
14
import java.util.*;
15
15
16
16
import javax.swing.*;
17
import javax.swing.border.Border;
17
18
import javax.swing.event.DocumentEvent;
18
19
import javax.swing.event.DocumentListener;
19
20
import javax.swing.event.UndoableEditEvent;
30
31
import javax.swing.undo.UndoableEditSupport;
31
32
32
33
import dk.aau.cs.TCTL.*;
34
import dk.aau.cs.TCTL.visitors.*;
33
35
import dk.aau.cs.gui.TabContent;
36
import dk.aau.cs.model.tapn.*;
34
37
import net.tapaal.swinghelpers.CustomJSpinner;
35
38
import pipe.dataLayer.DataLayer;
36
39
import pipe.dataLayer.NetWriter;
40
43
import pipe.dataLayer.TAPNQuery.TraceOption;
41
44
import pipe.gui.*;
42
45
import dk.aau.cs.TCTL.Parsing.TAPAALQueryParser;
43
import dk.aau.cs.TCTL.visitors.FixAbbrivPlaceNames;
44
import dk.aau.cs.TCTL.visitors.HasDeadlockVisitor;
45
import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor;
46
import dk.aau.cs.TCTL.visitors.VerifyPlaceNamesVisitor;
47
46
import dk.aau.cs.approximation.OverApproximation;
48
47
import dk.aau.cs.approximation.UnderApproximation;
49
48
import dk.aau.cs.io.TimedArcPetriNetNetworkWriter;
50
import dk.aau.cs.model.tapn.Constant;
51
import dk.aau.cs.model.tapn.ConstantStore;
52
import dk.aau.cs.model.tapn.SharedPlace;
53
import dk.aau.cs.model.tapn.TimedArcPetriNet;
54
import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
55
import dk.aau.cs.model.tapn.TimedPlace;
56
49
import dk.aau.cs.translations.ReductionOption;
57
50
import dk.aau.cs.util.Tuple;
58
51
import dk.aau.cs.util.UnsupportedModelException;
75
68
private static final String EXPORT_VERIFYTAPN_BTN_TEXT = "Export TAPAAL XML";
76
69
private static final String EXPORT_VERIFYPN_BTN_TEXT = "Export PN XML";
77
70
private static final String EXPORT_COMPOSED_BTN_TEXT = "Merge net components";
78
71
79
72
private static final String UPPAAL_SOME_TRACE_STRING = "Some trace ";
80
73
private static final String SOME_TRACE_STRING = "Some trace ";
81
74
private static final String FASTEST_TRACE_STRING = "Fastest trace ";
103
96
private JPanel queryPanel;
104
97
105
98
private JPanel quantificationPanel;
106
private ButtonGroup quantificationRadioButtonGroup;
107
private JRadioButton existsDiamond;
108
private JRadioButton existsBox;
109
private JRadioButton forAllDiamond;
110
private JRadioButton forAllBox;
99
private ButtonGroup quantificationButtonGroup;
100
private JButton existsDiamond;
101
private JButton existsBox;
102
private JButton existsNext;
103
private JButton existsUntil;
104
private JButton forAllDiamond;
105
private JButton forAllBox;
106
private JButton forAllNext;
107
private JButton forAllUntil;
111
108
112
109
private JTextPane queryField;
113
110
130
127
private JComboBox templateBox;
131
128
private JComboBox<String> placesBox;
132
129
private JComboBox<String> relationalOperatorBox;
133
private CustomJSpinner placeMarking;
130
private JLabel transitionIsEnabledLabel;
131
private CustomJSpinner placeMarking;
134
132
private JButton truePredicateButton;
135
133
private JButton falsePredicateButton;
136
134
private JButton deadLockPredicateButton;
152
150
private JRadioButton noTraceRadioButton;
153
151
private JRadioButton someTraceRadioButton;
154
152
private JRadioButton fastestTraceRadioButton;
155
153
156
154
// Reduction options panel
157
155
private JPanel reductionOptionsPanel;
158
156
private JComboBox<String> reductionOption;
163
161
private JCheckBox usePTrie;
164
162
private JCheckBox useGCD;
165
163
private JCheckBox useOverApproximation;
166
private JCheckBox useReduction;
164
private JCheckBox useSiphonTrap;
165
private JCheckBox useQueryReduction;
166
private JCheckBox useReduction;
167
167
private JCheckBox useStubbornReduction;
168
168
169
169
// Approximation options panel
170
170
private JPanel overApproximationOptionsPanel;
171
171
private ButtonGroup approximationRadioButtonGroup;
173
173
private JRadioButton overApproximationEnable;
174
174
private JRadioButton underApproximationEnable;
175
175
private CustomJSpinner overApproximationDenominator;
176
176
177
177
// Buttons in the bottom of the dialogue
178
178
private JPanel buttonPanel;
179
179
private JButton cancelButton;
349
349
private JTextField queryName;
350
350
351
351
private static Boolean advancedView = false;
352
352
353
353
private static boolean hasForcedDisabledTimeDarts = false;
354
354
private static boolean hasForcedDisabledStubbornReduction = false;
355
355
private static boolean hasForcedDisabledGCD = false;
370
370
private static final String TOOL_TIP_EXISTS_DIAMOND = "Check if the given marking is reachable in the net.";
371
371
private static final String TOOL_TIP_EXISTS_BOX = "Check if there is a trace on which all markings satisfy the given property. (Available only for some verification engines.)";
372
372
private static final String TOOL_TIP_FORALL_DIAMOND = "Check if on any maxiaml trace there is marking that satisfies the given property. (Available only for some verification engines.)";
373
374
373
private static final String TOOL_TIP_FORALL_BOX = "Check if every reachable marking in the net satifies the given property.";
375
374
376
//Tool tips for logic panel
375
private static final String TOOL_TIP_EXISTS_UNTIL = "There is a computation where the first formula holds until the second one holds.";
376
private static final String TOOL_TIP_EXISTS_NEXT = "There is a transition firing after which the reached marking satisfies the given property.";
377
private static final String TOOL_TIP_FORALL_UNTIL = "On every computation the first formula holds until the second one holds";
378
private static final String TOOL_TIP_FORALL_NEXT = "After any transition firing the reached marking satisfies the given property.";
379
380
//Tool tips for logic panel
377
381
private static final String TOOL_TIP_CONJUNCTIONBUTTON = "Expand the currently selected part of the query with a conjunction.";
378
382
private static final String TOOL_TIP_DISJUNCTIONBUTTON = "Expand the currently selected part of the query with a disjunction.";
379
383
private static final String TOOL_TIP_NEGATIONBUTTON = "Negate the currently selected part of the query.";
405
409
//Tool tips for reduction options panel
406
410
private final static String TOOL_TIP_REDUCTION_OPTION = "Choose a verification engine.";
407
411
private final static String TOOL_TIP_SYMMETRY_REDUCTION = "Apply automatic symmetry reduction.";
408
private final static String TOOL_TIP_DISCRETE_INCLUSION = "<html>This optimization will perform a more advanced inclusion check.";
412
private final static String TOOL_TIP_DISCRETE_INCLUSION = "<html>This optimization will perform a more advanced inclusion check.";
409
413
private final static String TOOL_TIP_SELECT_INCLUSION_PLACES = "Manually select places considered for the inclusion check.";
410
414
private final static String TOOL_TIP_TIME_DARTS = "Use the time dart optimization";
411
415
private final static String TOOL_TIP_PTRIE = "Use the PTrie memory optimization";
412
416
private final static String TOOL_TIP_STUBBORN_REDUCTION = "Apply partial order reduction (only for EF and AG queries and when Time Darts are disabled).";
413
417
private final static String TOOL_TIP_GCD = "Calculate greatest common divisor to minimize constants in the model";
414
418
private final static String TOOL_TIP_OVERAPPROX = "Run linear over-approximation check for EF and AG queries"; // TODO: write tooltip
419
private final static String TOOL_TIP_USE_STRUCTURALREDUCTION = "Apply structural reductions to reduce the size of the net.";
420
private final static String TOOL_TIP_USE_SIPHONTRAP = "For a deadlock query, attempt to prove deadlock-freeness by using siphon-trap analysis via linear programming.";
421
private final static String TOOL_TIP_USE_QUERY_REDUCTION = "Use query rewriting rules and linear programming (state equations) to reduce the size of the query.";
415
422
416
423
//Tool tips for search options panel
417
424
private final static String TOOL_TIP_HEURISTIC_SEARCH = "<html>Uses a heuiristic method in state space exploration.<br />" +
433
440
private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Export an xml file of composed net and approximated net if enabled";
434
441
private final static String TOOL_TIP_SAVE_TAPAAL_BUTTON = "Export an xml file that can be used as input for the TAPAAL engine.";
435
442
private final static String TOOL_TIP_SAVE_PN_BUTTON = "Export an xml file that can be used as input for the untimed Petri net engine.";
436
443
437
444
//Tool tips for approximation panel
438
445
private final static String TOOL_TIP_APPROXIMATION_METHOD_NONE = "No approximation method is used.";
439
446
private final static String TOOL_TIP_APPROXIMATION_METHOD_OVER = "Approximate by dividing all intervals with the approximation constant and enlarging the intervals.";
440
447
private final static String TOOL_TIP_APPROXIMATION_METHOD_UNDER = "Approximate by dividing all intervals with the approximation constant and shrinking the intervals.";
441
448
private final static String TOOL_TIP_APPROXIMATION_CONSTANT = "Choose approximation constant";
442
449
443
450
public QueryDialog(EscapableDialog me, QueryDialogueOption option,
444
451
TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
445
452
this.tapnNetwork = tapnNetwork;
486
493
int capacity = getCapacity();
487
494
488
495
TAPNQuery.TraceOption traceOption = getTraceOption();
489
490
496
TAPNQuery.SearchOption searchOption = getSearchOption();
491
492
497
ReductionOption reductionOptionToSet = getReductionOption();
493
boolean symmetry = getSymmetry();
498
499
if (lens.isTimed()) {
500
return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
501
} else {
502
return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
503
}
504
}
505
506
private TAPNQuery getTimedQuery(String name, int capacity, TraceOption traceOption, SearchOption searchOption, ReductionOption reductionOptionToSet) {
507
boolean symmetry = getSymmetry();
494
508
boolean timeDarts = useTimeDarts.isSelected();
495
509
boolean pTrie = usePTrie.isSelected();
496
510
boolean gcd = useGCD.isSelected();
526
540
return query;
527
541
}
528
542
543
private TAPNQuery getUntimedQuery(String name, int capacity, TraceOption traceOption, SearchOption searchOption, ReductionOption reductionOptionToSet) {
544
boolean reduction = useReduction.isSelected();
545
546
TAPNQuery query = new TAPNQuery(
547
name,
548
capacity,
549
newProperty.copy(),
550
traceOption,
551
searchOption,
552
reductionOptionToSet,
553
/* symmetry */false,
554
/* gcd */false,
555
/* timeDart */false,
556
/* pTrie */false,
557
/* overApproximation */false,
558
reduction,
559
/* hashTableSizeToSet */ null,
560
/* extrapolationOptionToSet */null,
561
inclusionPlaces,
562
/* enableOverApproximation */false,
563
/* enableUnderApproximation */false,
564
0
565
);
566
query.setCategory(TAPNQuery.QueryCategory.CTL);
567
query.setUseSiphontrap(useSiphonTrap.isSelected());
568
query.setUseQueryReduction(useQueryReduction.isSelected());
569
query.setUseStubbornReduction(useStubbornReduction.isSelected());
570
return query;
571
}
572
529
573
private boolean getSymmetry() {
530
574
return symmetryReduction.isSelected();
531
575
}
551
595
if(fastestTraceRadioButton.isSelected()){
552
596
return SearchOption.DEFAULT;
553
597
}
554
598
555
599
if(depthFirstSearch.isSelected())
556
600
return SearchOption.DFS;
557
601
else if(randomSearch.isSelected())
580
624
return ReductionOption.VerifyTAPN;
581
625
else if (reductionOptionString.equals(name_DISCRETE))
582
626
return ReductionOption.VerifyTAPNdiscreteVerification;
583
// else if (reductionOptionString.equals(name_UNTIMED))
584
// return ReductionOption.VerifyPN;
627
else if (reductionOptionString.equals(name_UNTIMED))
628
return ReductionOption.VerifyPN;
585
629
else
586
630
return ReductionOption.BROADCAST;
587
631
}
599
643
fastestTraceRadioButton.setEnabled(false);
600
644
someTraceRadioButton.setEnabled(false);
601
645
noTraceRadioButton.setEnabled(true);
646
} else if (lens.isTimed()) {
647
fastestTraceRadioButton.setEnabled(tapnNetwork.isNonStrict() && !queryHasDeadlock() &&
648
!(newProperty instanceof TCTLEGNode || newProperty instanceof TCTLAFNode));
649
someTraceRadioButton.setEnabled(true);
650
noTraceRadioButton.setEnabled(true);
651
} else if (queryIsReachability()) {
652
fastestTraceRadioButton.setEnabled(false);
653
someTraceRadioButton.setEnabled(true);
654
noTraceRadioButton.setEnabled(true);
602
655
} else {
603
fastestTraceRadioButton.setEnabled(tapnNetwork.isNonStrict() && !queryHasDeadlock() && !(newProperty instanceof TCTLEGNode || newProperty instanceof TCTLAFNode));
604
someTraceRadioButton.setEnabled(true);
605
noTraceRadioButton.setEnabled(true);
656
fastestTraceRadioButton.setEnabled(false);
657
someTraceRadioButton.setEnabled(false);
658
noTraceRadioButton.setEnabled(false);
659
noTraceRadioButton.setSelected(true);
606
660
}
607
661
608
662
if(getTraceOption() == TraceOption.FASTEST) {
609
663
if(fastestTraceRadioButton.isEnabled()){
610
664
fastestTraceRadioButton.setSelected(true);
611
} else {
612
someTraceRadioButton.setSelected(true);
613
}
665
} else if (someTraceRadioButton.isEnabled()) {
666
someTraceRadioButton.setSelected(true);
667
} else {
668
noTraceRadioButton.setSelected(true);
669
}
614
670
}
615
671
}
616
672
617
private void resetQuantifierSelectionButtons() {
618
quantificationRadioButtonGroup.clearSelection();
673
private boolean queryIsReachability() {
674
return new IsReachabilityVisitor().isReachability(newProperty);
675
}
676
677
private void resetQuantifierSelectionButtons() {
678
quantificationButtonGroup.clearSelection();
619
679
}
620
680
621
681
private void exit() {
622
682
rootPane.getParent().setVisible(false);
623
683
}
624
684
625
public String getQuantificationSelection() {
626
if (existsDiamond.isSelected()) {
627
return "E<>";
628
} else if (existsBox.isSelected()) {
629
return "E[]";
630
} else if (forAllDiamond.isSelected()) {
631
return "A<>";
632
} else if (forAllBox.isSelected()) {
633
return "A[]";
634
} else {
635
return "";
636
}
637
}
638
639
685
public boolean queryHasDeadlock(){
640
686
return new HasDeadlockVisitor().hasDeadLock(newProperty);
641
687
}
644
690
HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
645
691
if(CreateGui.getCurrentTab().network().hasWeights() && !CreateGui.getCurrentTab().network().isNonStrict()){
646
692
JOptionPane.showMessageDialog(CreateGui.getApp(),
647
"No reduction option supports both strict intervals and weigthed arcs",
693
"No reduction option supports both strict intervals and weigthed arcs",
648
694
"No reduction option", JOptionPane.ERROR_MESSAGE);
649
695
return null;
650
696
}
680
726
}
681
727
}
682
728
729
private TCTLAbstractPathProperty getPathProperty(TCTLAbstractProperty property) {
730
if (property instanceof TCTLAbstractPathProperty) {
731
return (TCTLAbstractPathProperty) property.copy();
732
} else {
733
return new TCTLPathPlaceHolder();
734
}
735
}
736
683
737
private TCTLAbstractStateProperty getSpecificChildOfProperty(int number, TCTLAbstractProperty property) {
684
738
StringPosition[] children = property.getChildren();
685
739
int count = 0;
700
754
private void updateSelection() {
701
755
int index = queryField.getCaretPosition();
702
756
StringPosition position = newProperty.objectAt(index);
757
703
758
if (position == null)
704
759
return;
760
705
761
queryField.select(position.getStart(), position.getEnd());
706
762
currentSelection = position;
707
763
if(currentSelection != null) {
740
796
}
741
797
742
798
private void updateQueryButtonsAccordingToSelection() {
743
if (currentSelection.getObject() instanceof TCTLAtomicPropositionNode) {
799
TCTLAbstractProperty current = currentSelection.getObject();
800
if (current instanceof TCTLStateToPathConverter && !lens.isTimed()) {
801
current = ((TCTLStateToPathConverter) current).getProperty();
802
}
803
if (current instanceof TCTLAtomicPropositionNode) {
744
804
TCTLAtomicPropositionNode node = (TCTLAtomicPropositionNode) currentSelection.getObject();
745
if(!(node.getLeft() instanceof TCTLPlaceNode && node.getRight() instanceof TCTLConstNode)){
746
return;
747
}
748
TCTLPlaceNode placeNode = (TCTLPlaceNode) node.getLeft();
749
TCTLConstNode placeMarkingNode = (TCTLConstNode) node.getRight();
750
805
751
806
// bit of a hack to prevent posting edits to the undo manager when
752
807
// we programmatically change the selection in the atomic proposition comboboxes etc.
753
808
// because a different atomic proposition was selected
754
809
userChangedAtomicPropSelection = false;
755
if(placeNode.getTemplate().equals(""))
756
templateBox.setSelectedItem(SHARED);
757
else
758
templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));
759
placesBox.setSelectedItem(placeNode.getPlace());
760
relationalOperatorBox.setSelectedItem(node.getOp());
761
placeMarking.setValue(placeMarkingNode.getConstant());
762
userChangedAtomicPropSelection = true;
763
} else if (currentSelection.getObject() instanceof TCTLEFNode) {
764
existsDiamond.setSelected(true);
765
} else if (currentSelection.getObject() instanceof TCTLEGNode) {
766
existsBox.setSelected(true);
767
} else if (currentSelection.getObject() instanceof TCTLAGNode) {
768
forAllBox.setSelected(true);
769
} else if (currentSelection.getObject() instanceof TCTLAFNode) {
770
forAllDiamond.setSelected(true);
771
}
810
if (node.getLeft() instanceof TCTLPlaceNode) {
811
TCTLPlaceNode placeNode = (TCTLPlaceNode) node.getLeft();
812
if (placeNode.getTemplate().equals("")) {
813
templateBox.setSelectedItem(SHARED);
814
} else {
815
templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));
816
}
817
}
818
if (lens.isTimed()) {
819
updateTimedQueryButtons(node);
820
} else {
821
updateUntimedQueryButtons(node);
822
}
823
} else if (current instanceof TCTLTransitionNode) {
824
TCTLTransitionNode transitionNode = (TCTLTransitionNode) current;
825
userChangedAtomicPropSelection = false;
826
if (transitionNode.getTemplate().equals("")) {
827
templateBox.setSelectedItem(SHARED);
828
} else {
829
templateBox.setSelectedItem(tapnNetwork.getTAPNByName(transitionNode.getTemplate()));
830
}
831
placesBox.setSelectedItem(transitionNode.getTransition());
832
userChangedAtomicPropSelection = true;
833
}
834
if (!lens.isTimed()) {
835
setEnablednessOfOperatorAndMarkingBoxes();
836
}
772
837
}
773
838
839
private void updateTimedQueryButtons(TCTLAtomicPropositionNode node) {
840
if (!(node.getLeft() instanceof TCTLPlaceNode && node.getRight() instanceof TCTLConstNode)) {
841
return;
842
}
843
TCTLPlaceNode placeNode = (TCTLPlaceNode) node.getLeft();
844
TCTLConstNode placeMarkingNode = (TCTLConstNode) node.getRight();
845
846
placesBox.setSelectedItem(placeNode.getPlace());
847
relationalOperatorBox.setSelectedItem(node.getOp());
848
placeMarking.setValue(placeMarkingNode.getConstant());
849
userChangedAtomicPropSelection = true;
850
}
851
852
private void updateUntimedQueryButtons(TCTLAtomicPropositionNode node) {
853
userChangedAtomicPropSelection = false;
854
if (node.getLeft() instanceof TCTLPlaceNode) {
855
TCTLPlaceNode placeNode = (TCTLPlaceNode) node.getLeft();
856
placesBox.setSelectedItem(placeNode.getPlace());
857
} else {
858
if (placesBox.getItemCount() > 0) {
859
placesBox.setSelectedIndex(0);
860
}
861
}
862
relationalOperatorBox.setSelectedItem(node.getOp());
863
864
if (node.getRight() instanceof TCTLConstNode) {
865
TCTLConstNode placeMarkingNode = (TCTLConstNode) node.getRight();
866
placeMarking.setValue(placeMarkingNode.getConstant());
867
}
868
userChangedAtomicPropSelection = true;
869
}
870
871
private void setEnablednessOfOperatorAndMarkingBoxes() {
872
if (transitionIsSelected()) {
873
placeMarking.setVisible(false);
874
relationalOperatorBox.setVisible(false);
875
transitionIsEnabledLabel.setVisible(true);
876
} else {
877
transitionIsEnabledLabel.setVisible(false);
878
placeMarking.setVisible(true);
879
relationalOperatorBox.setVisible(true);
880
}
881
}
882
883
private boolean transitionIsSelected() {
884
String itemName = (String) placesBox.getSelectedItem();
885
if (itemName == null) return false;
886
boolean transitionSelected = false;
887
boolean sharedTransitionSelected = false;
888
for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
889
if (tapn.getTransitionByName(itemName) != null) {
890
transitionSelected = true;
891
break;
892
}
893
}
894
if (!transitionSelected) {
895
sharedTransitionSelected = tapnNetwork.getSharedTransitionByName(itemName) != null;
896
}
897
return transitionSelected || sharedTransitionSelected;
898
}
899
774
900
private void deleteSelection() {
775
901
if (currentSelection != null) {
776
902
TCTLAbstractProperty replacement = null;
822
948
String reductionOptionString = getReductionOptionAsString();
823
949
824
950
ArrayList<String> options = new ArrayList<String>();
825
951
826
952
disableSymmetryUpdate = true;
827
953
//The order here should be the same as in EngineSupportOptions
828
boolean[] queryOptions = new boolean[]{fastestTraceRadioButton.isSelected(),
829
(queryHasDeadlock() && (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]")) && highestNetDegree <= 2),
830
(queryHasDeadlock() && (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>"))),
954
boolean[] queryOptions = new boolean[]{
955
fastestTraceRadioButton.isSelected(),
956
(queryHasDeadlock() && (newProperty.toString().contains("EF") || newProperty.toString().contains("AG")) && highestNetDegree <= 2),
957
(queryHasDeadlock() && (newProperty.toString().contains("EG") || newProperty.toString().contains("AF"))),
831
958
(queryHasDeadlock() && hasInhibitorArcs),
832
959
tapnNetwork.hasWeights(),
833
960
hasInhibitorArcs,
834
961
tapnNetwork.hasUrgentTransitions(),
835
(getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")),
962
(newProperty.toString().contains("EG") || newProperty.toString().contains("AF")),
836
963
//we want to know if it is strict
837
964
!tapnNetwork.isNonStrict(),
838
965
//we want to know if it is timed
839
966
lens.isTimed(),
840
967
(queryHasDeadlock() && highestNetDegree > 2),
841
968
lens.isGame(),
842
(getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")) && highestNetDegree > 2,
969
(newProperty.toString().contains("EG") || newProperty.toString().contains("AF")) && highestNetDegree > 2,
843
970
newProperty.hasNestedPathQuantifiers()
844
971
};
845
972
846
973
847
974
if(useTimeDarts != null){
848
975
if(hasForcedDisabledTimeDarts){
849
976
hasForcedDisabledTimeDarts = false;
850
977
useTimeDarts.setSelected(true);
851
978
}
852
useTimeDarts.setEnabled(true);
979
useTimeDarts.setEnabled(true);
853
980
}
854
981
855
982
if(useStubbornReduction != null){
859
986
}
860
987
useStubbornReduction.setEnabled(true);
861
988
}
862
989
863
990
if(useGCD != null){
864
991
if(hasForcedDisabledGCD){
865
992
hasForcedDisabledGCD = false;
866
993
useGCD.setSelected(true);
867
994
}
868
useGCD.setEnabled(true);
995
useGCD.setEnabled(true);
869
996
}
870
997
871
998
if (tapnNetwork.isNonStrict()) {
872
999
// disable timedarts if liveness and deadlock prop
873
if((getQuantificationSelection().equals("E[]") ||
874
getQuantificationSelection().equals("A<>"))){
1000
if((newProperty.toString().contains("EG") ||
1001
newProperty.toString().contains("AF"))){
875
1002
if (useTimeDarts != null) {
876
1003
if(useTimeDarts.isSelected()){
877
1004
hasForcedDisabledTimeDarts = true;
881
1008
}
882
1009
}
883
1010
}
884
for(EngineSupportOptions engine : engineSupportOptions){
885
if(engine.areOptionsSupported(queryOptions)){
886
options.add(engine.nameString);
1011
if (lens.isTimed()) {
1012
for (EngineSupportOptions engine : engineSupportOptions) {
1013
if (engine.areOptionsSupported(queryOptions)) {
1014
options.add(engine.nameString);
1015
}
887
1016
}
1017
} else if (!lens.isGame()) {
1018
options.add(name_UNTIMED);
888
1019
}
889
1020
890
1021
reductionOption.removeAllItems();
891
1022
892
boolean selectedOptionStillAvailable = false;
1023
boolean selectedOptionStillAvailable = false;
893
1024
TraceOption trace = getTraceOption();
894
1025
for (String s : options) {
895
1026
reductionOption.addItem(s);
906
1037
fastestTraceRadioButton.setSelected(true);
907
1038
}
908
1039
}
909
1040
910
1041
disableSymmetryUpdate = false;
911
1042
}
912
1043
925
1056
}else{
926
1057
currentselected = randomSearch;
927
1058
}
928
1059
929
1060
if(fastestTraceRadioButton.isSelected()){
930
1061
breadthFirstSearch.setEnabled(false);
931
1062
depthFirstSearch.setEnabled(false);
942
1073
String reductionOptionString = getReductionOptionAsString();
943
1074
if (lens.isGame()) {
944
1075
heuristicSearch.setEnabled(false);
945
} else if(getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")){
1076
} else if (lens.isTimed() && (newProperty.toString().contains("EG") || newProperty.toString().contains("AF"))){
946
1077
breadthFirstSearch.setEnabled(false);
947
1078
if(!(reductionOptionString.equals(name_verifyTAPN) || reductionOptionString.equals(name_DISCRETE))){
948
1079
heuristicSearch.setEnabled(false);
963
1094
existsDiamond.setEnabled(false);
964
1095
forAllBox.setEnabled(false);
965
1096
forAllDiamond.setEnabled(false);
966
conjunctionButton.setEnabled(false);
1097
existsUntil.setEnabled(false);
1098
existsNext.setEnabled(false);
1099
forAllUntil.setEnabled(false);
1100
forAllNext.setEnabled(false);
1101
1102
conjunctionButton.setEnabled(false);
967
1103
disjunctionButton.setEnabled(false);
968
1104
negationButton.setEnabled(false);
969
1105
templateBox.setEnabled(false);
981
1117
existsDiamond.setEnabled(true);
982
1118
forAllBox.setEnabled(true);
983
1119
forAllDiamond.setEnabled(true);
984
conjunctionButton.setEnabled(false);
1120
if (!lens.isTimed()) {
1121
existsUntil.setEnabled(true);
1122
existsNext.setEnabled(true);
1123
forAllUntil.setEnabled(true);
1124
forAllNext.setEnabled(true);
1125
}
1126
1127
conjunctionButton.setEnabled(false);
985
1128
disjunctionButton.setEnabled(false);
986
1129
negationButton.setEnabled(false);
987
1130
templateBox.setEnabled(false);
999
1142
existsDiamond.setEnabled(false);
1000
1143
forAllBox.setEnabled(false);
1001
1144
forAllDiamond.setEnabled(false);
1002
conjunctionButton.setEnabled(true);
1145
existsUntil.setEnabled(false);
1146
existsNext.setEnabled(false);
1147
forAllUntil.setEnabled(false);
1148
forAllNext.setEnabled(false);
1149
1150
conjunctionButton.setEnabled(true);
1003
1151
disjunctionButton.setEnabled(true);
1004
1152
negationButton.setEnabled(true);
1005
1153
templateBox.setEnabled(true);
1012
1160
setEnablednessOfAddPredicateButton();
1013
1161
}
1014
1162
1163
private void enableOnlyUntimedStateButtons() {
1164
existsBox.setEnabled(true);
1165
existsDiamond.setEnabled(true);
1166
forAllBox.setEnabled(true);
1167
forAllDiamond.setEnabled(true);
1168
existsUntil.setEnabled(true);
1169
existsNext.setEnabled(true);
1170
forAllUntil.setEnabled(true);
1171
forAllNext.setEnabled(true);
1172
1173
conjunctionButton.setEnabled(true);
1174
disjunctionButton.setEnabled(true);
1175
negationButton.setEnabled(true);
1176
templateBox.setEnabled(true);
1177
placesBox.setEnabled(true);
1178
relationalOperatorBox.setEnabled(true);
1179
placeMarking.setEnabled(true);
1180
truePredicateButton.setEnabled(true);
1181
falsePredicateButton.setEnabled(true);
1182
deadLockPredicateButton.setEnabled(true);
1183
setEnablednessOfAddPredicateButton();
1184
}
1185
1015
1186
private void enableOnlyForAllBox() {
1016
1187
existsBox.setEnabled(false);
1017
1188
existsDiamond.setEnabled(false);
1018
1189
forAllBox.setEnabled(true);
1019
1190
forAllDiamond.setEnabled(false);
1191
if (!lens.isTimed()) {
1192
existsUntil.setEnabled(false);
1193
existsNext.setEnabled(false);
1194
forAllUntil.setEnabled(false);
1195
forAllNext.setEnabled(false);
1196
}
1197
1020
1198
conjunctionButton.setEnabled(false);
1021
1199
disjunctionButton.setEnabled(false);
1022
1200
negationButton.setEnabled(false);
1076
1254
disableAllQueryButtons();
1077
1255
disableEditingButtons();
1078
1256
setSaveButtonsEnabled();
1079
1257
1080
1258
// Set default caret location to end of query
1081
1259
queryField.setCaretPosition(queryField.getText().length());
1082
1260
}
1083
1261
1084
1262
private void updateQueryOnAtomicPropositionChange() {
1085
if (currentSelection != null && currentSelection.getObject() instanceof TCTLAtomicPropositionNode) {
1086
Object item = templateBox.getSelectedItem();
1263
if (currentSelection != null && (currentSelection.getObject() instanceof TCTLAtomicPropositionNode ||
1264
(!lens.isTimed() && currentSelection.getObject() instanceof TCTLTransitionNode))) {
1265
1266
Object item = templateBox.getSelectedItem();
1087
1267
String template = item.equals(SHARED) ? "" : item.toString();
1088
TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(
1089
new TCTLPlaceNode(template, (String) placesBox.getSelectedItem()),
1090
(String) relationalOperatorBox.getSelectedItem(),
1091
new TCTLConstNode((Integer) placeMarking.getValue()));
1268
TCTLAbstractStateProperty property;
1269
1270
if (!lens.isTimed() && transitionIsSelected()) {
1271
property = new TCTLTransitionNode(template, (String) placesBox.getSelectedItem());
1272
} else {
1273
property = new TCTLAtomicPropositionNode(
1274
new TCTLPlaceNode(template, (String) placesBox.getSelectedItem()),
1275
(String) relationalOperatorBox.getSelectedItem(),
1276
new TCTLConstNode((Integer) placeMarking.getValue()));
1277
}
1278
1092
1279
if (!property.equals(currentSelection.getObject())) {
1093
1280
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
1094
1281
newProperty = newProperty.replace(currentSelection.getObject(), property);
1116
1303
1117
1304
if(queryToCreateFrom != null)
1118
1305
setupFromQuery(queryToCreateFrom);
1119
1306
1120
1307
refreshTraceOptions();
1121
1308
setEnabledReductionOptions();
1122
1309
1123
1310
rootPane.setDefaultButton(saveAndVerifyButton);
1124
1311
disableAllQueryButtons();
1125
1312
setSaveButtonsEnabled();
1137
1324
queryName.setText(queryToCreateFrom.getName());
1138
1325
numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity());
1139
1326
1140
setupQuantificationFromQuery(queryToCreateFrom);
1141
setupSearchOptionsFromQuery(queryToCreateFrom);
1327
if (lens.isTimed()) {
1328
setupQuantificationFromQuery(queryToCreateFrom);
1329
setupApproximationOptionsFromQuery(queryToCreateFrom);
1330
}
1331
setupSearchOptionsFromQuery(queryToCreateFrom);
1142
1332
setupReductionOptionsFromQuery(queryToCreateFrom);
1143
1333
setupTraceOptionsFromQuery(queryToCreateFrom);
1144
setupApproximationOptionsFromQuery(queryToCreateFrom);
1145
1334
}
1146
1335
1147
1336
private void setupApproximationOptionsFromQuery(TAPNQuery queryToCreateFrom) {
1148
1337
if (queryToCreateFrom.isOverApproximationEnabled())
1149
1338
overApproximationEnable.setSelected(true);
1151
1340
underApproximationEnable.setSelected(true);
1152
1341
else
1153
1342
noApproximationEnable.setSelected(true);
1154
1343
1155
1344
if (queryToCreateFrom.approximationDenominator() > 0) {
1156
1345
overApproximationDenominator.setValue(queryToCreateFrom.approximationDenominator());
1157
1346
}
1167
1356
reduction = name_BROADCASTDEG2;
1168
1357
} else if(queryToCreateFrom.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification){
1169
1358
reduction = name_DISCRETE;
1170
// } else if(queryToCreateFrom.getReductionOption() == ReductionOption.VerifyPN){
1171
// reduction = name_UNTIMED;
1359
} else if(queryToCreateFrom.getReductionOption() == ReductionOption.VerifyPN){
1360
reduction = name_UNTIMED;
1172
1361
} else if(queryToCreateFrom.getReductionOption() == ReductionOption.COMBI){
1173
1362
reduction = name_COMBI;
1174
} else if (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]")) {
1363
} else if (newProperty.toString().contains("EF") || newProperty.toString().contains("AG")) {
1175
1364
if (queryToCreateFrom.getReductionOption() == ReductionOption.STANDARD) {
1176
1365
reduction = name_STANDARD;
1177
1366
} else if (queryToCreateFrom.getReductionOption() == ReductionOption.OPTIMIZEDSTANDARD) {
1185
1374
}
1186
1375
}
1187
1376
1188
reductionOption.addItem(reduction);
1189
reductionOption.setSelectedItem(reduction);
1190
symmetryReduction.setSelected(symmetry);
1191
useTimeDarts.setSelected(queryToCreateFrom.useTimeDarts());
1192
usePTrie.setSelected(queryToCreateFrom.usePTrie());
1193
useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled());
1194
useGCD.setSelected(queryToCreateFrom.useGCD());
1195
useOverApproximation.setSelected(queryToCreateFrom.useOverApproximation());
1196
useReduction.setSelected(queryToCreateFrom.useReduction());
1197
discreteInclusion.setSelected(queryToCreateFrom.discreteInclusion());
1198
if(queryToCreateFrom.discreteInclusion()) selectInclusionPlacesButton.setEnabled(true);
1377
reductionOption.addItem(reduction);
1378
reductionOption.setSelectedItem(reduction);
1379
1380
if (lens.isTimed()) {
1381
setupTimedReductionOptions(queryToCreateFrom);
1382
} else {
1383
setupUntimedReductionOptions(queryToCreateFrom);
1384
}
1199
1385
}
1200
1386
1387
private void setupTimedReductionOptions(TAPNQuery queryToCreateFrom) {
1388
symmetryReduction.setSelected(queryToCreateFrom.useSymmetry());
1389
useTimeDarts.setSelected(queryToCreateFrom.useTimeDarts());
1390
usePTrie.setSelected(queryToCreateFrom.usePTrie());
1391
useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled());
1392
useGCD.setSelected(queryToCreateFrom.useGCD());
1393
useOverApproximation.setSelected(queryToCreateFrom.useOverApproximation());
1394
useReduction.setSelected(queryToCreateFrom.useReduction());
1395
discreteInclusion.setSelected(queryToCreateFrom.discreteInclusion());
1396
1397
if (queryToCreateFrom.discreteInclusion()) {
1398
selectInclusionPlacesButton.setEnabled(true);
1399
}
1400
}
1401
1402
private void setupUntimedReductionOptions(TAPNQuery queryToCreateFrom) {
1403
useSiphonTrap.setSelected(queryToCreateFrom.isSiphontrapEnabled());
1404
useQueryReduction.setSelected(queryToCreateFrom.isQueryReductionEnabled());
1405
useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled());
1406
useReduction.setSelected(queryToCreateFrom.useReduction());
1407
}
1408
1201
1409
private void setupTraceOptionsFromQuery(TAPNQuery queryToCreateFrom) {
1202
1410
if (queryToCreateFrom.getTraceOption() == TraceOption.SOME) {
1203
1411
someTraceRadioButton.setSelected(true);
1222
1430
1223
1431
private void setupQuantificationFromQuery(TAPNQuery queryToCreateFrom) {
1224
1432
// bit of a hack, possible because quantifier node is always the first
1225
// node (we cant have nested quantifiers)
1433
// node (we cant have nested quantifiers)
1226
1434
if (queryToCreateFrom.getProperty() instanceof TCTLEFNode) {
1227
1435
existsDiamond.setSelected(true);
1228
1436
} else if (queryToCreateFrom.getProperty() instanceof TCTLEGNode) {
1270
1478
advancedButton.setToolTipText(TOOL_TIP_ADVANCED_VIEW_BUTTON);
1271
1479
advancedButton.addActionListener(arg0 -> toggleAdvancedSimpleView(true));
1272
1480
1273
JButton infoButton = new JButton("Help on the query options");
1481
JButton infoButton = new JButton("Help on the query options");
1274
1482
infoButton.setToolTipText(TOOL_TIP_INFO_BUTTON);
1275
1483
infoButton.addActionListener(new ActionListener(){
1276
1484
public void actionPerformed(ActionEvent arg0) {
1287
1495
pane.removeMouseListener(listener);
1288
1496
}
1289
1497
Dimension dim = new Dimension(500,400);
1290
pane.setPreferredSize(dim);
1291
pane.setMargin(new Insets(5,5,5,5));
1292
JScrollPane scrollPane = new JScrollPane(pane);
1293
scrollPane.setPreferredSize(dim);
1294
return scrollPane;
1498
pane.setPreferredSize(dim);
1499
pane.setMargin(new Insets(5,5,5,5));
1500
JScrollPane scrollPane = new JScrollPane(pane);
1501
scrollPane.setPreferredSize(dim);
1502
return scrollPane;
1295
1503
}
1296
1504
1297
1505
private String getHelpMessage(){
1366
1574
1367
1575
searchOptionsPanel.setVisible(advancedView);
1368
1576
reductionOptionsPanel.setVisible(advancedView);
1369
saveUppaalXMLButton.setVisible(advancedView);
1577
if (lens.isTimed()) {
1578
saveUppaalXMLButton.setVisible(advancedView);
1579
overApproximationOptionsPanel.setVisible(advancedView);
1580
}
1370
1581
mergeNetComponentsButton.setVisible(advancedView);
1371
overApproximationOptionsPanel.setVisible(advancedView);
1372
1582
1373
1583
if(advancedView){
1374
1584
advancedButton.setText("Simple view");
1375
1585
advancedButton.setToolTipText(TOOL_TIP_SIMPLE_VIEW_BUTTON);
1379
1589
}
1380
1590
1381
1591
guiDialog.pack();
1382
guiDialog.setLocation(location);
1592
guiDialog.setLocation(location);
1383
1593
}
1384
1594
1385
1595
private void initBoundednessCheckPanel() {
1390
1600
boundednessCheckPanel.setLayout(new BoxLayout(boundednessCheckPanel, BoxLayout.X_AXIS));
1391
1601
boundednessCheckPanel.add(new JLabel(" Number of extra tokens: "));
1392
1602
1393
numberOfExtraTokensInNet = new CustomJSpinner(4, 0, Integer.MAX_VALUE);
1603
numberOfExtraTokensInNet = new CustomJSpinner(4, 0, Integer.MAX_VALUE);
1394
1604
numberOfExtraTokensInNet.setMaximumSize(new Dimension(65, 30));
1395
1605
numberOfExtraTokensInNet.setMinimumSize(new Dimension(65, 30));
1396
1606
numberOfExtraTokensInNet.setPreferredSize(new Dimension(65, 30));
1454
1664
// Put the text pane in a scroll pane.
1455
1665
JScrollPane queryScrollPane = new JScrollPane(queryField);
1456
1666
queryScrollPane.setVerticalScrollBarPolicy(ScrollPaneConstants.VERTICAL_SCROLLBAR_AS_NEEDED);
1457
Dimension d = new Dimension(750, 80);
1667
Dimension d = new Dimension(900, 80);
1458
1668
queryScrollPane.setPreferredSize(d);
1459
1669
queryScrollPane.setMinimumSize(d);
1460
1670
1520
1730
gbc.gridx = 0;
1521
1731
gbc.gridy = 0;
1522
1732
gbc.fill = GridBagConstraints.BOTH;
1523
gbc.gridwidth = 4;
1733
gbc.anchor = GridBagConstraints.CENTER;
1734
gbc.gridwidth = 4;
1524
1735
queryPanel.add(queryScrollPane, gbc);
1525
1736
}
1526
1737
1527
1738
private void initQuantificationPanel() {
1528
1739
quantificationPanel = new JPanel(new GridBagLayout());
1529
1740
quantificationPanel.setBorder(BorderFactory.createTitledBorder("Quantification"));
1530
quantificationRadioButtonGroup = new ButtonGroup();
1741
quantificationButtonGroup = new ButtonGroup();
1531
1742
approximationRadioButtonGroup = new ButtonGroup();
1532
1743
1533
existsDiamond = new JRadioButton("(EF) There exists some reachable marking that satisifies:");
1534
existsBox = new JRadioButton("(EG) There exists a trace on which every marking satisfies:");
1535
forAllDiamond = new JRadioButton("(AF) On all traces there is eventually a marking that satisfies:");
1536
forAllBox = new JRadioButton("(AG) All reachable markings satisfy:");
1537
1538
//Add tool tips
1539
existsDiamond.setToolTipText(TOOL_TIP_EXISTS_DIAMOND);
1540
existsBox.setToolTipText(TOOL_TIP_EXISTS_BOX);
1541
forAllDiamond.setToolTipText(TOOL_TIP_FORALL_DIAMOND);
1542
forAllBox.setToolTipText(TOOL_TIP_FORALL_BOX);
1543
1544
quantificationRadioButtonGroup.add(existsDiamond);
1545
quantificationRadioButtonGroup.add(existsBox);
1546
quantificationRadioButtonGroup.add(forAllDiamond);
1547
quantificationRadioButtonGroup.add(forAllBox);
1548
1549
GridBagConstraints gbc = new GridBagConstraints();
1550
gbc.gridx = 0;
1551
gbc.gridy = 0;
1552
gbc.anchor = GridBagConstraints.WEST;
1553
quantificationPanel.add(existsDiamond, gbc);
1554
1555
gbc.gridy = 1;
1556
quantificationPanel.add(existsBox, gbc);
1557
1558
gbc.gridy = 2;
1559
quantificationPanel.add(forAllDiamond, gbc);
1560
1561
gbc.gridy = 3;
1562
quantificationPanel.add(forAllBox, gbc);
1563
1744
// Instantiate buttons
1745
existsDiamond = new JButton("EF");
1746
existsBox = new JButton("EG");
1747
forAllDiamond = new JButton("AF");
1748
forAllBox = new JButton("AG");
1749
existsUntil = new JButton("EU");
1750
existsNext = new JButton("EX");
1751
forAllUntil = new JButton("AU");
1752
forAllNext = new JButton("AX");
1753
1754
// Add tool-tips
1755
existsDiamond.setToolTipText(TOOL_TIP_EXISTS_DIAMOND);
1756
existsBox.setToolTipText(TOOL_TIP_EXISTS_BOX);
1757
forAllDiamond.setToolTipText(TOOL_TIP_FORALL_DIAMOND);
1758
forAllBox.setToolTipText(TOOL_TIP_FORALL_BOX);
1759
existsUntil.setToolTipText(TOOL_TIP_EXISTS_UNTIL);
1760
existsNext.setToolTipText(TOOL_TIP_EXISTS_NEXT);
1761
forAllUntil.setToolTipText(TOOL_TIP_FORALL_UNTIL);
1762
forAllNext.setToolTipText(TOOL_TIP_FORALL_NEXT);
1763
1764
// Add buttons to panel
1765
quantificationButtonGroup.add(existsDiamond);
1766
quantificationButtonGroup.add(existsBox);
1767
quantificationButtonGroup.add(forAllDiamond);
1768
quantificationButtonGroup.add(forAllBox);
1769
quantificationButtonGroup.add(existsUntil);
1770
quantificationButtonGroup.add(existsNext);
1771
quantificationButtonGroup.add(forAllUntil);
1772
quantificationButtonGroup.add(forAllNext);
1773
1774
// Place buttons in GUI
1775
GridBagConstraints gbc = new GridBagConstraints();
1776
gbc.gridx = 0;
1777
gbc.anchor = GridBagConstraints.WEST;
1778
1779
// First column of buttons
1780
gbc.gridy = 0;
1781
gbc.insets = new Insets(0, 0, 5, 0);
1782
quantificationPanel.add(existsDiamond, gbc);
1783
gbc.gridy = 1;
1784
quantificationPanel.add(existsBox, gbc);
1785
gbc.gridy = 2;
1786
quantificationPanel.add(existsUntil, gbc);
1787
gbc.gridy = 3;
1788
quantificationPanel.add(existsNext, gbc);
1789
1790
// Second column of buttons
1791
gbc.gridx = 2;
1792
gbc.gridy = 0;
1793
gbc.insets = new Insets(0, 0, 5, 0);
1794
quantificationPanel.add(forAllDiamond, gbc);
1795
gbc.gridy = 1;
1796
quantificationPanel.add(forAllBox, gbc);
1797
gbc.gridy = 2;
1798
quantificationPanel.add(forAllUntil, gbc);
1799
gbc.gridy = 3;
1800
quantificationPanel.add(forAllNext, gbc);
1801
1802
// Add quantification panel to query panel
1564
1803
gbc = new GridBagConstraints();
1565
1804
gbc.gridx = 0;
1566
1805
gbc.gridy = 1;
1568
1807
gbc.fill = GridBagConstraints.VERTICAL;
1569
1808
queryPanel.add(quantificationPanel, gbc);
1570
1809
1810
if (lens.isTimed()) {
1811
addTimedQuantificationListeners();
1812
} else {
1813
addUntimedQuantificationListeners();
1814
}
1815
}
1816
1817
private void addTimedQuantificationListeners() {
1571
1818
// Add action listeners to the query options
1572
1819
existsBox.addActionListener(e -> {
1573
1820
TCTLEGNode property = new TCTLEGNode(getSpecificChildOfProperty(1, currentSelection.getObject()));
1574
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
1575
newProperty = newProperty.replace(currentSelection.getObject(), property);
1576
updateSelection(property);
1577
undoSupport.postEdit(edit);
1578
queryChanged();
1821
existsBox.setSelected(true);
1822
addPropertyToQuery(property);
1823
unselectButtons();
1579
1824
});
1580
1825
1581
1826
existsDiamond.addActionListener(e -> {
1582
1827
TCTLEFNode property = new TCTLEFNode(getSpecificChildOfProperty(1, currentSelection.getObject()));
1583
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
1584
newProperty = newProperty.replace(currentSelection.getObject(), property);
1585
updateSelection(property);
1586
undoSupport.postEdit(edit);
1587
queryChanged();
1828
existsDiamond.setSelected(true);
1829
addPropertyToQuery(property);
1830
unselectButtons();
1588
1831
});
1589
1832
1590
1833
forAllBox.addActionListener(e -> {
1591
1834
TCTLAGNode property = new TCTLAGNode(getSpecificChildOfProperty(1, currentSelection.getObject()));
1592
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
1593
newProperty = newProperty.replace(currentSelection.getObject(), property);
1594
updateSelection(property);
1595
undoSupport.postEdit(edit);
1596
queryChanged();
1835
forAllBox.setSelected(true);
1836
addPropertyToQuery(property);
1837
unselectButtons();
1597
1838
});
1598
1839
1599
1840
forAllDiamond.addActionListener(e -> {
1600
1841
TCTLAFNode property = new TCTLAFNode(getSpecificChildOfProperty(1, currentSelection.getObject()));
1601
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
1602
newProperty = newProperty.replace(currentSelection.getObject(), property);
1603
updateSelection(property);
1604
undoSupport.postEdit(edit);
1605
queryChanged();
1842
forAllDiamond.setSelected(true);
1843
addPropertyToQuery(property);
1844
unselectButtons();
1606
1845
});
1607
1846
}
1608
1847
1848
private void unselectButtons() {
1849
existsDiamond.setSelected(false);
1850
existsBox.setSelected(false);
1851
forAllBox.setSelected(false);
1852
forAllDiamond.setSelected(false);
1853
}
1854
1855
private void addUntimedQuantificationListeners() {
1856
addTimedQuantificationListeners();
1857
1858
existsNext.addActionListener(new ActionListener() {
1859
public void actionPerformed(ActionEvent e) {
1860
TCTLAbstractPathProperty property;
1861
if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
1862
property = new TCTLEXNode((TCTLAbstractStateProperty) currentSelection.getObject());
1863
} else {
1864
property = new TCTLEXNode(getSpecificChildOfProperty(1, currentSelection.getObject()));
1865
}
1866
addPropertyToQuery(property);
1867
}
1868
});
1869
1870
existsUntil.addActionListener(new ActionListener() {
1871
public void actionPerformed(ActionEvent e) {
1872
TCTLAbstractPathProperty property;
1873
if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
1874
property = new TCTLEUNode((TCTLAbstractStateProperty) currentSelection.getObject(),
1875
new TCTLStatePlaceHolder());
1876
} else {
1877
property = new TCTLEUNode(getSpecificChildOfProperty(1, currentSelection.getObject()),
1878
getSpecificChildOfProperty(2, currentSelection.getObject()));
1879
}
1880
addPropertyToQuery(property);
1881
}
1882
});
1883
1884
forAllNext.addActionListener(new ActionListener() {
1885
public void actionPerformed(ActionEvent e) {
1886
TCTLAbstractPathProperty property;
1887
if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
1888
property = new TCTLAXNode((TCTLAbstractStateProperty) currentSelection.getObject());
1889
} else {
1890
property = new TCTLAXNode(getSpecificChildOfProperty(1, currentSelection.getObject()));
1891
}
1892
addPropertyToQuery(property);
1893
}
1894
});
1895
1896
forAllUntil.addActionListener(new ActionListener() {
1897
public void actionPerformed(ActionEvent e) {
1898
TCTLAbstractPathProperty property;
1899
if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
1900
property = new TCTLAUNode((TCTLAbstractStateProperty) currentSelection.getObject(),
1901
new TCTLStatePlaceHolder());
1902
} else {
1903
property = new TCTLAUNode(getSpecificChildOfProperty(1, currentSelection.getObject()),
1904
getSpecificChildOfProperty(2, currentSelection.getObject()));
1905
}
1906
addPropertyToQuery(property);
1907
}
1908
});
1909
}
1910
1911
private void addPropertyToQuery(TCTLAbstractPathProperty property) {
1912
if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
1913
addPropertyToQuery(ConvertToStateProperty(property));
1914
return;
1915
}
1916
1917
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
1918
newProperty = newProperty.replace(currentSelection.getObject(), property);
1919
updateSelection(property);
1920
undoSupport.postEdit(edit);
1921
queryChanged();
1922
}
1923
1924
private void addPropertyToQuery(TCTLAbstractStateProperty property) {
1925
if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
1926
addPropertyToQuery(ConvertToPathProperty(property));
1927
return;
1928
}
1929
1930
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
1931
newProperty = newProperty.replace(currentSelection.getObject(), property);
1932
updateSelection(property);
1933
undoSupport.postEdit(edit);
1934
queryChanged();
1935
}
1936
1937
private TCTLAbstractStateProperty ConvertToStateProperty(TCTLAbstractPathProperty p) {
1938
if (p instanceof TCTLStateToPathConverter) {
1939
return ((TCTLStateToPathConverter) p).getProperty();
1940
} else return new TCTLPathToStateConverter(p);
1941
}
1942
1943
private TCTLAbstractPathProperty ConvertToPathProperty(TCTLAbstractStateProperty p) {
1944
if (p instanceof TCTLPathToStateConverter) {
1945
return ((TCTLPathToStateConverter) p).getProperty();
1946
} else return new TCTLStateToPathConverter(p);
1947
}
1948
1609
1949
private void initLogicPanel() {
1610
1950
logicButtonPanel = new JPanel(new GridBagLayout());
1611
1951
logicButtonPanel.setBorder(BorderFactory.createTitledBorder("Logic"));
1650
1990
if (currentSelection.getObject() instanceof TCTLAndListNode) {
1651
1991
andListNode = new TCTLAndListNode((TCTLAndListNode) currentSelection.getObject());
1652
1992
andListNode.addConjunct(new TCTLStatePlaceHolder());
1653
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), andListNode);
1654
newProperty = newProperty.replace(currentSelection.getObject(), andListNode);
1655
updateSelection(andListNode);
1656
undoSupport.postEdit(edit);
1993
addPropertyToQuery(andListNode);
1657
1994
} else if (currentSelection.getObject() instanceof TCTLOrListNode) {
1658
1995
andListNode = new TCTLAndListNode(((TCTLOrListNode) currentSelection.getObject()).getProperties());
1659
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), andListNode);
1660
newProperty = newProperty.replace(currentSelection.getObject(), andListNode);
1661
updateSelection(andListNode);
1662
undoSupport.postEdit(edit);
1996
addPropertyToQuery(andListNode);
1663
1997
} else if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
1664
1998
TCTLAbstractStateProperty prop = (TCTLAbstractStateProperty) currentSelection
1665
1999
.getObject();
1670
2004
// new placeholder conjunct to it
1671
2005
andListNode = new TCTLAndListNode((TCTLAndListNode) parentNode);
1672
2006
andListNode.addConjunct(new TCTLStatePlaceHolder());
1673
UndoableEdit edit = new QueryConstructionEdit(parentNode, andListNode);
1674
newProperty = newProperty.replace(parentNode, andListNode);
1675
updateSelection(andListNode);
1676
undoSupport.postEdit(edit);
2007
addPropertyToQuery(andListNode);
1677
2008
} else {
1678
2009
TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();
1679
2010
andListNode = new TCTLAndListNode(getStateProperty(currentSelection.getObject()), ph);
1680
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), andListNode);
1681
newProperty = newProperty.replace(currentSelection.getObject(), andListNode);
1682
updateSelection(andListNode);
1683
undoSupport.postEdit(edit);
2011
addPropertyToQuery(andListNode);
1684
2012
}
1685
}
1686
queryChanged();
2013
} else if (!lens.isTimed()) {
2014
checkUntimedAndNode();
2015
}
1687
2016
}
1688
2017
1689
}
1690
1691
);
2018
});
1692
2019
1693
2020
disjunctionButton.addActionListener(new ActionListener() {
1694
2021
public void actionPerformed(ActionEvent e) {
1696
2023
if (currentSelection.getObject() instanceof TCTLOrListNode) {
1697
2024
orListNode = new TCTLOrListNode((TCTLOrListNode) currentSelection.getObject());
1698
2025
orListNode.addDisjunct(new TCTLStatePlaceHolder());
1699
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), orListNode);
1700
newProperty = newProperty.replace(currentSelection.getObject(), orListNode);
1701
updateSelection(orListNode);
1702
undoSupport.postEdit(edit);
1703
} else if (currentSelection.getObject() instanceof TCTLAndListNode) {
2026
addPropertyToQuery(orListNode);
2027
} else if (currentSelection.getObject() instanceof TCTLAndListNode) {
1704
2028
orListNode = new TCTLOrListNode(((TCTLAndListNode) currentSelection.getObject()).getProperties());
1705
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), orListNode);
1706
newProperty = newProperty.replace(currentSelection.getObject(), orListNode);
1707
updateSelection(orListNode);
1708
undoSupport.postEdit(edit);
1709
} else if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
2029
addPropertyToQuery(orListNode);
2030
} else if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
1710
2031
TCTLAbstractStateProperty prop = (TCTLAbstractStateProperty) currentSelection.getObject();
1711
2032
TCTLAbstractProperty parentNode = prop.getParent();
1712
2033
1715
2036
// new placeholder disjunct to it
1716
2037
orListNode = new TCTLOrListNode((TCTLOrListNode) parentNode);
1717
2038
orListNode.addDisjunct(new TCTLStatePlaceHolder());
1718
UndoableEdit edit = new QueryConstructionEdit(parentNode, orListNode);
1719
newProperty = newProperty.replace(parentNode, orListNode);
1720
updateSelection(orListNode);
1721
undoSupport.postEdit(edit);
1722
} else {
2039
addPropertyToQuery(orListNode);
2040
} else {
1723
2041
TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();
1724
2042
orListNode = new TCTLOrListNode(getStateProperty(currentSelection.getObject()), ph);
1725
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), orListNode);
1726
newProperty = newProperty.replace(currentSelection.getObject(), orListNode);
1727
updateSelection(orListNode);
1728
undoSupport.postEdit(edit);
1729
}
1730
}
1731
queryChanged();
2043
addPropertyToQuery(orListNode);
2044
}
2045
} else if (!lens.isTimed()) {
2046
checkUntimedOrNode();
2047
}
1732
2048
}
1733
1734
2049
});
1735
2050
1736
2051
negationButton.addActionListener(e -> {
1737
TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));
1738
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
1739
newProperty = newProperty.replace(currentSelection.getObject(), property);
1740
updateSelection(property);
1741
undoSupport.postEdit(edit);
1742
queryChanged();
2052
if (lens.isTimed()) {
2053
TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));
2054
addPropertyToQuery(property);
2055
} else {
2056
TCTLAbstractStateProperty root;
2057
if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
2058
root = ConvertToStateProperty(getPathProperty(currentSelection.getObject()));
2059
} else {
2060
root = getStateProperty(currentSelection.getObject());
2061
}
2062
TCTLNotNode property = new TCTLNotNode(root);
2063
addPropertyToQuery(property);
2064
}
1743
2065
});
1744
2066
}
1745
2067
2068
private void checkUntimedAndNode() {
2069
TCTLAndListNode andListNode;
2070
if (currentSelection.getObject() instanceof TCTLStateToPathConverter) {
2071
TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();
2072
2073
TCTLAbstractStateProperty prop = ((TCTLStateToPathConverter) currentSelection.getObject()).getProperty();
2074
2075
if (prop instanceof TCTLAndListNode) {
2076
andListNode = new TCTLAndListNode((TCTLAndListNode) prop);
2077
andListNode.addConjunct(new TCTLStatePlaceHolder());
2078
} else if (prop instanceof TCTLOrListNode) {
2079
andListNode = new TCTLAndListNode(((TCTLOrListNode) prop).getProperties());
2080
} else {
2081
andListNode = new TCTLAndListNode(getStateProperty(prop), ph);
2082
}
2083
2084
TCTLAbstractPathProperty property = new TCTLStateToPathConverter(andListNode);
2085
addPropertyToQuery(property);
2086
} else if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
2087
TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();
2088
andListNode = new TCTLAndListNode(getStateProperty(
2089
new TCTLPathToStateConverter((TCTLAbstractPathProperty) currentSelection.getObject())), ph);
2090
2091
TCTLAbstractPathProperty property = new TCTLStateToPathConverter(andListNode);
2092
addPropertyToQuery(property);
2093
}
2094
}
2095
2096
private void checkUntimedOrNode() {
2097
TCTLOrListNode orListNode;
2098
if (currentSelection.getObject() instanceof TCTLStateToPathConverter) {
2099
TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();
2100
2101
TCTLAbstractStateProperty prop = ((TCTLStateToPathConverter) currentSelection.getObject()).getProperty();
2102
2103
if (prop instanceof TCTLOrListNode) {
2104
orListNode = new TCTLOrListNode((TCTLOrListNode) prop);
2105
orListNode.addDisjunct(new TCTLStatePlaceHolder());
2106
} else if (prop instanceof TCTLAndListNode) {
2107
orListNode = new TCTLOrListNode(((TCTLAndListNode) prop).getProperties());
2108
} else {
2109
orListNode = new TCTLOrListNode(getStateProperty(prop), ph);
2110
}
2111
2112
TCTLAbstractPathProperty property = new TCTLStateToPathConverter(orListNode);
2113
addPropertyToQuery(property);
2114
} else if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
2115
TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();
2116
orListNode = new TCTLOrListNode(getStateProperty(
2117
new TCTLPathToStateConverter((TCTLAbstractPathProperty) currentSelection.getObject())), ph);
2118
2119
TCTLAbstractPathProperty property = new TCTLStateToPathConverter(orListNode);
2120
addPropertyToQuery(property);
2121
}
2122
}
2123
1746
2124
private void initPredicationConstructionPanel() {
1747
2125
predicatePanel = new JPanel(new GridBagLayout());
1748
2126
predicatePanel.setBorder(BorderFactory.createTitledBorder("Predicates"));
1752
2130
placesBox.setMaximumSize(d);
1753
2131
placesBox.setPreferredSize(d);
1754
2132
1755
1756
2133
Vector<Object> items = new Vector<Object>(tapnNetwork.activeTemplates().size()+1);
1757
2134
items.addAll(tapnNetwork.activeTemplates());
1758
2135
if(tapnNetwork.numberOfSharedPlaces() > 0) items.add(SHARED);
1771
2148
placeNames.add(place.name());
1772
2149
}
1773
2150
}
2151
if (!lens.isTimed()) {
2152
for (TimedTransition transition : tapn.transitions()) {
2153
if (!transition.isShared()) {
2154
placeNames.add(transition.name());
2155
}
2156
}
2157
}
1774
2158
1775
2159
placeNames.sort(String::compareToIgnoreCase);
1776
2160
placesBox.setModel(new DefaultComboBoxModel<>(placeNames));
1786
2170
for (SharedPlace place : tapnNetwork.sharedPlaces()) {
1787
2171
placeNames.add(place.name());
1788
2172
}
2173
if (lens.isTimed()) {
2174
for (SharedTransition transition : tapnNetwork.sharedTransitions()) {
2175
placeNames.add(transition.name());
2176
}
2177
}
1789
2178
placeNames.sort(String::compareToIgnoreCase);
1790
2179
placesBox.setModel(new DefaultComboBoxModel<>(placeNames));
1791
2180
1795
2184
updateQueryOnAtomicPropositionChange();
1796
2185
}
1797
2186
}
2187
if (!lens.isTimed()) setEnablednessOfOperatorAndMarkingBoxes();
2188
1798
2189
}
1799
2190
});
1800
2191
Dimension dim = new Dimension(235, 27);
1809
2200
gbc.anchor = GridBagConstraints.WEST;
1810
2201
predicatePanel.add(templateBox, gbc);
1811
2202
1812
gbc = new GridBagConstraints();
1813
gbc.gridx = 0;
1814
gbc.gridy = 1;
1815
gbc.anchor = GridBagConstraints.WEST;
1816
predicatePanel.add(placesBox, gbc);
1817
1818
String[] relationalSymbols = { "=", "<=", "<", ">=", ">" };
1819
relationalOperatorBox = new JComboBox<>(new DefaultComboBoxModel<>(relationalSymbols));
1820
1821
gbc.gridx = 1;
1822
predicatePanel.add(relationalOperatorBox, gbc);
1823
1824
placeMarking = new CustomJSpinner(0);
1825
placeMarking.setMaximumSize(new Dimension(60, 30));
1826
placeMarking.setMinimumSize(new Dimension(60, 30));
1827
placeMarking.setPreferredSize(new Dimension(60, 30));
1828
1829
gbc.gridx = 2;
1830
predicatePanel.add(placeMarking, gbc);
1831
1832
addPredicateButton = new JButton("Add predicate to the query");
1833
gbc.gridx = 0;
1834
gbc.gridy = 2;
1835
gbc.gridwidth = 3;
1836
predicatePanel.add(addPredicateButton, gbc);
2203
JPanel templateRow = new JPanel(new FlowLayout(FlowLayout.CENTER));
2204
predicatePanel.add(templateRow, gbc);
2205
templateBox.setPreferredSize(new Dimension(292, 27));
2206
templateRow.add(templateBox);
2207
2208
JPanel placeRow = new JPanel(new FlowLayout(FlowLayout.CENTER));
2209
gbc.gridy = 1;
2210
predicatePanel.add(placeRow, gbc);
2211
placeRow.add(placesBox);
2212
2213
String[] relationalSymbols = { "=", "!=", "<=", "<", ">=", ">" };
2214
relationalOperatorBox = new JComboBox(new DefaultComboBoxModel(relationalSymbols));
2215
relationalOperatorBox.setPreferredSize(new Dimension(80, 27));
2216
placeRow.add(relationalOperatorBox);
2217
2218
placeMarking = new CustomJSpinner(0);
2219
placeMarking.setPreferredSize(new Dimension(80, 27));
2220
placeRow.add(placeMarking);
2221
2222
transitionIsEnabledLabel = new JLabel(" is enabled");
2223
transitionIsEnabledLabel.setPreferredSize(new Dimension(165, 27));
2224
if (!lens.isTimed()) placeRow.add(transitionIsEnabledLabel);
2225
2226
JPanel addPredicateRow = new JPanel(new FlowLayout(FlowLayout.CENTER));
2227
gbc.gridy = 2;
2228
predicatePanel.add(addPredicateRow, gbc);
2229
addPredicateButton = new JButton("Add predicate to the query");
2230
addPredicateButton.setPreferredSize(new Dimension(292, 27));
2231
addPredicateRow.add(addPredicateButton);
1837
2232
1838
2233
JSeparator separator = new JSeparator(SwingConstants.HORIZONTAL);
1839
2234
separator.setEnabled(true);
1845
2240
gbc.fill = GridBagConstraints.HORIZONTAL;
1846
2241
predicatePanel.add(separator,gbc);
1847
2242
1848
truePredicateButton = new JButton("True");
1849
gbc = new GridBagConstraints();
1850
gbc.gridx = 0;
1851
gbc.gridy = 4;
1852
gbc.insets = new Insets(0, -38, 0,0);
1853
predicatePanel.add(truePredicateButton, gbc);
1854
1855
falsePredicateButton = new JButton("False");
1856
gbc = new GridBagConstraints();
1857
gbc.gridx = 1;
1858
gbc.gridy = 4;
1859
gbc.insets = new Insets(0, -88, 0,0);
1860
predicatePanel.add(falsePredicateButton, gbc);
1861
1862
deadLockPredicateButton = new JButton("Deadlock");
1863
gbc = new GridBagConstraints();
1864
gbc.gridx = 2;
1865
gbc.gridy = 4;
1866
gbc.gridwidth = 3;
1867
gbc.insets = new Insets(0, -35, 0,0);
1868
predicatePanel.add(deadLockPredicateButton, gbc);
2243
truePredicateButton = new JButton("True");
2244
truePredicateButton.setPreferredSize(new Dimension(90, 27));
2245
2246
falsePredicateButton = new JButton("False");
2247
falsePredicateButton.setPreferredSize(new Dimension(90, 27));
2248
2249
deadLockPredicateButton = new JButton("Deadlock");
2250
deadLockPredicateButton.setPreferredSize(new Dimension(103, 27));
2251
2252
JPanel trueFalseDeadlock = new JPanel(new FlowLayout(FlowLayout.CENTER));
2253
trueFalseDeadlock.add(truePredicateButton);
2254
trueFalseDeadlock.add(falsePredicateButton);
2255
trueFalseDeadlock.add(deadLockPredicateButton);
2256
2257
gbc = new GridBagConstraints();
2258
gbc.gridx = 2;
2259
gbc.gridy = 4;
2260
gbc.anchor = GridBagConstraints.CENTER;
2261
predicatePanel.add(trueFalseDeadlock, gbc);
1869
2262
1870
2263
gbc = new GridBagConstraints();
1871
2264
gbc.gridx = 2;
1889
2282
public void actionPerformed(ActionEvent e) {
1890
2283
String template = templateBox.getSelectedItem().toString();
1891
2284
if(template.equals(SHARED)) template = "";
1892
TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(
1893
new TCTLPlaceNode(template, (String) placesBox.getSelectedItem()),
1894
(String) relationalOperatorBox.getSelectedItem(),
1895
new TCTLConstNode((Integer) placeMarking.getValue()));
1896
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
1897
newProperty = newProperty.replace(currentSelection.getObject(), property);
1898
updateSelection(property);
1899
undoSupport.postEdit(edit);
1900
queryChanged();
2285
2286
if (lens.isTimed() && transitionIsSelected()) {
2287
addPropertyToQuery(new TCTLTransitionNode(template, (String) placesBox.getSelectedItem()));
2288
} else {
2289
TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(
2290
new TCTLPlaceNode(template, (String) placesBox.getSelectedItem()),
2291
(String) relationalOperatorBox.getSelectedItem(),
2292
new TCTLConstNode((Integer) placeMarking.getValue()));
2293
addPropertyToQuery(property);
2294
}
1901
2295
}
1902
}
1903
1904
);
2296
});
1905
2297
1906
2298
truePredicateButton.addActionListener(new ActionListener() {
1907
2299
public void actionPerformed(ActionEvent e) {
1908
2300
TCTLTrueNode trueNode = new TCTLTrueNode();
1909
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), trueNode);
1910
newProperty = newProperty.replace(currentSelection.getObject(), trueNode);
1911
updateSelection(trueNode);
1912
undoSupport.postEdit(edit);
1913
queryChanged();
1914
}
2301
addPropertyToQuery(trueNode);
2302
}
1915
2303
});
1916
2304
1917
2305
falsePredicateButton.addActionListener(new ActionListener() {
1918
2306
public void actionPerformed(ActionEvent e) {
1919
2307
TCTLFalseNode falseNode = new TCTLFalseNode();
1920
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), falseNode);
1921
newProperty = newProperty.replace(currentSelection.getObject(), falseNode);
1922
updateSelection(falseNode);
1923
undoSupport.postEdit(edit);
1924
queryChanged();
1925
}
2308
addPropertyToQuery(falseNode);
2309
}
1926
2310
});
1927
2311
1928
2312
deadLockPredicateButton.addActionListener(new ActionListener() {
1929
2313
public void actionPerformed(ActionEvent e) {
1930
2314
TCTLDeadlockNode deadLockNode = new TCTLDeadlockNode();
1931
UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), deadLockNode);
1932
newProperty = newProperty.replace(currentSelection.getObject(), deadLockNode);
1933
updateSelection(deadLockNode);
1934
undoSupport.postEdit(edit);
1935
queryChanged();
1936
}
2315
addPropertyToQuery(deadLockNode);
2316
}
1937
2317
});
1938
2318
1939
2319
placesBox.addActionListener(e -> {
1983
2363
editingButtonsGroup.add(redoButton);
1984
2364
editingButtonsGroup.add(editQueryButton);
1985
2365
1986
GridBagConstraints gbc = new GridBagConstraints();
1987
gbc.gridx = 0;
1988
gbc.gridy = 0;
1989
gbc.anchor = GridBagConstraints.WEST;
1990
editingButtonPanel.add(undoButton, gbc);
2366
GridBagConstraints gbc = new GridBagConstraints();
2367
JPanel row = new JPanel(new GridLayout(1, 2));
2368
row.add(undoButton);
2369
row.add(redoButton);
1991
2370
1992
gbc.gridx = 1;
1993
editingButtonPanel.add(redoButton, gbc);
2371
gbc.gridx = 0;
2372
gbc.gridy = 0;
2373
gbc.weightx = 4;
2374
gbc.fill = GridBagConstraints.HORIZONTAL;
2375
editingButtonPanel.add(row, gbc);
1994
2376
1995
2377
gbc.gridx = 0;
1996
2378
gbc.gridy = 1;
1997
gbc.gridwidth = 2;
1998
gbc.fill = GridBagConstraints.HORIZONTAL;
1999
editingButtonPanel.add(deleteButton, gbc);
2379
gbc.weightx = 4;
2380
gbc.fill = GridBagConstraints.HORIZONTAL;
2381
editingButtonPanel.add(deleteButton, gbc);
2000
2382
2001
2383
gbc.gridy = 2;
2002
2384
editingButtonPanel.add(resetButton, gbc);
2036
2418
ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();
2037
2419
for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
2038
2420
for(TimedPlace p : tapn.places()) {
2039
templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
2421
if (lens.isTimed() || !p.isShared()) {
2422
templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
2423
}
2040
2424
}
2041
2425
}
2042
2426
2044
2428
templatePlaceNames.add(new Tuple<String, String>("", p.name()));
2045
2429
}
2046
2430
2047
FixAbbrivPlaceNames.fixAbbrivPlaceNames(templatePlaceNames, newQuery);
2048
2431
FixAbbrivPlaceNames.fixAbbrivPlaceNames(templatePlaceNames, newQuery);
2049
2432
VerifyPlaceNamesVisitor nameChecker = new VerifyPlaceNamesVisitor(templatePlaceNames);
2050
2051
2433
VerifyPlaceNamesVisitor.Context c = nameChecker.verifyPlaceNames(newQuery);
2052
2434
2053
if (!c.getResult()) {
2435
boolean isResultFalse;
2436
2437
if (lens.isTimed()) {
2438
isResultFalse = !c.getResult();
2439
} else {
2440
isResultFalse = checkUntimedResult(newQuery) && !c.getResult();
2441
}
2442
2443
if (isResultFalse) {
2054
2444
StringBuilder s = new StringBuilder();
2055
s.append("The following places were used in the query, but are not present in your model:\n\n");
2445
s.append("The following places" + (lens.isTimed() ? "" : " or transitions") +
2446
"were used in the query, but are not present in your model:\n\n");
2056
2447
2057
2448
for (String placeName : c.getIncorrectPlaceNames()) {
2058
2449
s.append(placeName);
2134
2525
gbc = new GridBagConstraints();
2135
2526
gbc.gridx = 3;
2136
2527
gbc.gridy = 1;
2137
gbc.fill = GridBagConstraints.VERTICAL;
2528
gbc.fill = GridBagConstraints.BOTH;
2529
gbc.anchor = GridBagConstraints.WEST;
2138
2530
queryPanel.add(editingButtonPanel, gbc);
2139
2531
}
2140
2532
2533
private boolean checkUntimedResult(TCTLAbstractProperty newQuery) {
2534
// check correct transition names are used in atomic propositions
2535
ArrayList<Tuple<String, String>> templateTransitionNames = new ArrayList<Tuple<String, String>>();
2536
for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
2537
for (TimedTransition t : tapn.transitions()) {
2538
if (!t.isShared()) {
2539
templateTransitionNames.add(new Tuple<String, String>(tapn.name(), t.name()));
2540
}
2541
}
2542
}
2543
2544
for (SharedTransition t : tapnNetwork.sharedTransitions()) {
2545
templateTransitionNames.add(new Tuple<String, String>("", t.name()));
2546
}
2547
2548
FixAbbrivTransitionNames.fixAbbrivTransitionNames(templateTransitionNames, newQuery);
2549
VerifyTransitionNamesVisitor transitionNameChecker = new VerifyTransitionNamesVisitor(templateTransitionNames);
2550
VerifyTransitionNamesVisitor.Context c2 = transitionNameChecker.verifyTransitionNames(newQuery);
2551
return !c2.getResult();
2552
}
2553
2141
2554
private void initUppaalOptionsPanel() {
2142
2555
2143
2556
uppaalOptionsPanel = new JPanel(new GridBagLayout());
2208
2621
someTraceRadioButton = new JRadioButton(UPPAAL_SOME_TRACE_STRING);
2209
2622
noTraceRadioButton = new JRadioButton("No trace");
2210
2623
fastestTraceRadioButton = new JRadioButton("Fastest trace");
2624
2211
2625
someTraceRadioButton.setToolTipText(TOOL_TIP_SOME_TRACE);
2212
2626
noTraceRadioButton.setToolTipText(TOOL_TIP_NO_TRACE);
2213
2627
fastestTraceRadioButton.setToolTipText(TOOL_TIP_FASTEST_TRACE);
2628
2214
2629
traceRadioButtonGroup.add(fastestTraceRadioButton);
2215
2630
traceRadioButtonGroup.add(someTraceRadioButton);
2216
2631
traceRadioButtonGroup.add(noTraceRadioButton);
2218
2633
fastestTraceRadioButton.setEnabled(false);
2219
2634
someTraceRadioButton.setEnabled(false);
2220
2635
noTraceRadioButton.setSelected(true);
2221
2222
Enumeration<AbstractButton> buttons = traceRadioButtonGroup.getElements();
2223
2636
2637
Enumeration<AbstractButton> buttons = traceRadioButtonGroup.getElements();
2638
2224
2639
while(buttons.hasMoreElements()){
2225
AbstractButton button = buttons.nextElement();
2640
AbstractButton button = buttons.nextElement();
2226
2641
button.addActionListener(e -> {
2227
2642
setEnabledReductionOptions();
2228
2643
setEnabledOptionsAccordingToCurrentReduction();
2239
2654
gridBagConstraints.weightx = 1;
2240
2655
gridBagConstraints.anchor = GridBagConstraints.WEST;
2241
2656
traceOptionsPanel.add(someTraceRadioButton, gridBagConstraints);
2242
2657
2243
2658
gridBagConstraints.gridy = 2;
2244
2659
gridBagConstraints.weightx = 1;
2245
2660
gridBagConstraints.anchor = GridBagConstraints.WEST;
2246
2661
traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);
2247
2662
2663
if (lens.isTimed()) {
2664
gridBagConstraints.gridy = 2;
2665
gridBagConstraints.weightx = 1;
2666
gridBagConstraints.anchor = GridBagConstraints.WEST;
2667
traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);
2668
}
2669
2248
2670
gridBagConstraints = new GridBagConstraints();
2249
2671
gridBagConstraints.anchor = GridBagConstraints.WEST;
2250
2672
gridBagConstraints.gridx = 1;
2254
2676
uppaalOptionsPanel.add(traceOptionsPanel, gridBagConstraints);
2255
2677
2256
2678
}
2257
2258
2259
2260
2261
2679
2262
2680
private void initOverApproximationPanel() {
2263
2681
overApproximationOptionsPanel = new JPanel(new GridBagLayout());
2264
2682
overApproximationOptionsPanel.setVisible(false);
2265
2683
overApproximationOptionsPanel.setBorder(BorderFactory.createTitledBorder("Approximation Options"));
2266
2684
approximationRadioButtonGroup = new ButtonGroup();
2267
2685
2268
2686
noApproximationEnable = new JRadioButton("Exact analysis");
2269
2687
noApproximationEnable.setVisible(true);
2270
2688
noApproximationEnable.setSelected(true);
2271
2689
noApproximationEnable.setToolTipText(TOOL_TIP_APPROXIMATION_METHOD_NONE);
2272
2690
2273
2691
overApproximationEnable = new JRadioButton("Over-approximation");
2274
2692
overApproximationEnable.setVisible(true);
2275
2693
overApproximationEnable.setToolTipText(TOOL_TIP_APPROXIMATION_METHOD_OVER);
2276
2694
2277
2695
underApproximationEnable = new JRadioButton("Under-approximation");
2278
2696
underApproximationEnable.setVisible(true);
2279
2697
underApproximationEnable.setToolTipText(TOOL_TIP_APPROXIMATION_METHOD_UNDER);
2281
2699
approximationRadioButtonGroup.add(noApproximationEnable);
2282
2700
approximationRadioButtonGroup.add(overApproximationEnable);
2283
2701
approximationRadioButtonGroup.add(underApproximationEnable);
2284
2285
Enumeration<AbstractButton> buttons = approximationRadioButtonGroup.getElements();
2286
2702
2703
Enumeration<AbstractButton> buttons = approximationRadioButtonGroup.getElements();
2704
2287
2705
while(buttons.hasMoreElements()){
2288
AbstractButton button = buttons.nextElement();
2706
AbstractButton button = buttons.nextElement();
2289
2707
button.addActionListener(e -> setEnabledOptionsAccordingToCurrentReduction());
2290
2708
}
2291
2709
2292
2710
GridBagConstraints gridBagConstraints = new GridBagConstraints();
2293
2711
gridBagConstraints.gridy = 0;
2294
2712
gridBagConstraints.weightx = 1;
2295
2713
gridBagConstraints.anchor = GridBagConstraints.WEST;
2296
2297
JLabel approximationDenominatorLabel = new JLabel("Approximation constant: ");
2298
2299
overApproximationDenominator = new CustomJSpinner(2, 2, Integer.MAX_VALUE);
2714
2715
JLabel approximationDenominatorLabel = new JLabel("Approximation constant: ");
2716
2717
overApproximationDenominator = new CustomJSpinner(2, 2, Integer.MAX_VALUE);
2300
2718
overApproximationDenominator.setMaximumSize(new Dimension(65, 30));
2301
2719
overApproximationDenominator.setMinimumSize(new Dimension(65, 30));
2302
2720
overApproximationDenominator.setPreferredSize(new Dimension(65, 30));
2303
2721
overApproximationDenominator.setToolTipText(TOOL_TIP_APPROXIMATION_CONSTANT);
2304
2722
2305
2723
overApproximationOptionsPanel.add(noApproximationEnable, gridBagConstraints);
2306
2724
overApproximationOptionsPanel.add(overApproximationEnable, gridBagConstraints);
2307
2725
overApproximationOptionsPanel.add(underApproximationEnable, gridBagConstraints);
2308
2726
overApproximationOptionsPanel.add(approximationDenominatorLabel, gridBagConstraints);
2309
2727
overApproximationOptionsPanel.add(overApproximationDenominator);
2310
2728
2311
2729
gridBagConstraints = new GridBagConstraints();
2312
2730
gridBagConstraints.gridx = 0;
2313
2731
gridBagConstraints.gridy = 5;
2314
2732
gridBagConstraints.anchor = GridBagConstraints.WEST;
2315
2733
gridBagConstraints.insets = new Insets(5,10,5,10);
2316
2734
gridBagConstraints.fill = GridBagConstraints.HORIZONTAL;
2317
2735
2318
2736
add(overApproximationOptionsPanel, gridBagConstraints);
2319
2737
}
2320
2738
2322
2740
reductionOptionsPanel = new JPanel(new GridBagLayout());
2323
2741
reductionOptionsPanel.setVisible(false);
2324
2742
reductionOptionsPanel.setBorder(BorderFactory.createTitledBorder("Verification Options"));
2325
Dimension d = new Dimension(898, 100);
2743
Dimension d = lens.isTimed() ? new Dimension(898, 100) : new Dimension(810, 130);
2326
2744
reductionOptionsPanel.setPreferredSize(d);
2327
2745
reductionOption = new JComboBox<String>();
2328
2746
reductionOption.setToolTipText(TOOL_TIP_REDUCTION_OPTION);
2342
2760
gbc.insets = new Insets(0,5,0,5);
2343
2761
reductionOptionsPanel.add(reductionOption, gbc);
2344
2762
2345
symmetryReduction = new JCheckBox("Use symmetry reduction");
2346
symmetryReduction.setSelected(true);
2347
symmetryReduction.setToolTipText(TOOL_TIP_SYMMETRY_REDUCTION);
2348
2349
gbc = new GridBagConstraints();
2350
gbc.gridx = 2;
2351
gbc.gridy = 0;
2352
gbc.anchor = GridBagConstraints.WEST;
2353
gbc.insets = new Insets(0,5,0,5);
2354
reductionOptionsPanel.add(symmetryReduction, gbc);
2355
2356
discreteInclusion = new JCheckBox("Use discrete inclusion");
2357
discreteInclusion.setVisible(true);
2358
discreteInclusion.setToolTipText(TOOL_TIP_DISCRETE_INCLUSION);
2359
discreteInclusion.addActionListener(new ActionListener() {
2360
public void actionPerformed(ActionEvent e) {
2361
selectInclusionPlacesButton.setEnabled(discreteInclusion.isSelected());
2362
}
2363
});
2364
2365
gbc = new GridBagConstraints();
2366
gbc.gridx = 2;
2367
gbc.gridy = 1;
2368
gbc.anchor = GridBagConstraints.WEST;
2369
gbc.insets = new Insets(0,5,0,5);
2370
reductionOptionsPanel.add(discreteInclusion, gbc);
2371
2372
selectInclusionPlacesButton = new JButton("Select Inclusion Places");
2373
selectInclusionPlacesButton.setEnabled(false);
2374
selectInclusionPlacesButton.setToolTipText(TOOL_TIP_SELECT_INCLUSION_PLACES);
2375
selectInclusionPlacesButton.addActionListener(new ActionListener() {
2376
public void actionPerformed(ActionEvent e) {
2377
inclusionPlaces = ChooseInclusionPlacesDialog.showInclusionPlacesDialog(tapnNetwork, inclusionPlaces);
2378
}
2379
});
2380
2381
gbc = new GridBagConstraints();
2382
gbc.gridx = 3;
2383
gbc.gridy = 1;
2384
gbc.anchor = GridBagConstraints.WEST;
2385
gbc.insets = new Insets(0,5,0,5);
2386
reductionOptionsPanel.add(selectInclusionPlacesButton, gbc);
2387
2388
useTimeDarts = new JCheckBox("Use Time Darts");
2389
useTimeDarts.setSelected(false);
2390
useTimeDarts.setToolTipText(TOOL_TIP_TIME_DARTS);
2391
useTimeDarts.addActionListener(e -> setEnabledOptionsAccordingToCurrentReduction());
2392
2393
gbc = new GridBagConstraints();
2394
gbc.gridx = 3;
2395
gbc.gridy = 2;
2396
gbc.anchor = GridBagConstraints.WEST;
2397
gbc.insets = new Insets(0,5,0,5);
2398
reductionOptionsPanel.add(useTimeDarts, gbc);
2399
2400
useGCD = new JCheckBox("Use GCD");
2401
useGCD.setSelected(true);
2402
useGCD.setToolTipText(TOOL_TIP_GCD);
2403
2404
gbc = new GridBagConstraints();
2405
gbc.gridx = 3;
2406
gbc.gridy = 0;
2407
gbc.anchor = GridBagConstraints.WEST;
2408
gbc.insets = new Insets(0,5,0,5);
2409
reductionOptionsPanel.add(useGCD, gbc);
2410
2411
usePTrie = new JCheckBox("Use PTrie");
2412
usePTrie.setSelected(true);
2413
usePTrie.setToolTipText(TOOL_TIP_PTRIE);
2414
2415
gbc = new GridBagConstraints();
2416
gbc.gridx = 3;
2417
gbc.gridy = 1;
2418
gbc.anchor = GridBagConstraints.WEST;
2419
gbc.insets = new Insets(0,5,0,5);
2420
reductionOptionsPanel.add(selectInclusionPlacesButton, gbc);
2421
2422
useReduction = new JCheckBox("Apply net reductions");
2423
useReduction.setSelected(true);
2424
2425
gbc = new GridBagConstraints();
2426
gbc.gridx = 2;
2427
gbc.gridy = 1;
2428
gbc.anchor = GridBagConstraints.WEST;
2429
gbc.insets = new Insets(0,5,0,5);
2430
reductionOptionsPanel.add(useReduction, gbc);
2431
2432
2433
gbc = new GridBagConstraints();
2434
gbc.gridx = 3;
2435
gbc.gridy = 1;
2436
gbc.anchor = GridBagConstraints.WEST;
2437
gbc.insets = new Insets(0,5,0,5);
2438
reductionOptionsPanel.add(usePTrie, gbc);
2439
2440
useStubbornReduction = new JCheckBox("Use stubborn reduction");
2441
useStubbornReduction.setSelected(true);
2442
useStubbornReduction.setToolTipText(TOOL_TIP_STUBBORN_REDUCTION);
2443
2444
gbc = new GridBagConstraints();
2445
gbc.gridx = 2;
2446
gbc.gridy = 1;
2447
gbc.anchor = GridBagConstraints.WEST;
2448
gbc.insets = new Insets(0,5,0,5);
2449
reductionOptionsPanel.add(useStubbornReduction, gbc);
2450
2451
useOverApproximation = new JCheckBox("Use untimed state-equations check");
2452
useOverApproximation.setSelected(true);
2453
useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
2454
2455
gbc = new GridBagConstraints();
2456
gbc.gridx = 2;
2457
gbc.gridy = 2;
2458
gbc.anchor = GridBagConstraints.WEST;
2459
gbc.insets = new Insets(0,5,0,5);
2460
reductionOptionsPanel.add(useOverApproximation, gbc);
2763
useReduction = new JCheckBox("Apply net reductions");
2764
useSiphonTrap = new JCheckBox("Use siphon-trap analysis");
2765
useQueryReduction = new JCheckBox("Use query reduction");
2766
useStubbornReduction = new JCheckBox("Use stubborn reduction");
2767
symmetryReduction = new JCheckBox("Use symmetry reduction");
2768
discreteInclusion = new JCheckBox("Use discrete inclusion");
2769
selectInclusionPlacesButton = new JButton("Select Inclusion Places");
2770
useTimeDarts = new JCheckBox("Use Time Darts");
2771
useGCD = new JCheckBox("Use GCD");
2772
usePTrie = new JCheckBox("Use PTrie");
2773
useOverApproximation = new JCheckBox("Use untimed state-equations check");
2774
2775
useReduction.setSelected(true);
2776
useSiphonTrap.setSelected(false);
2777
useQueryReduction.setSelected(true);
2778
useStubbornReduction.setSelected(true);
2779
symmetryReduction.setSelected(true);
2780
discreteInclusion.setVisible(true);
2781
selectInclusionPlacesButton.setEnabled(false);
2782
useTimeDarts.setSelected(false);
2783
useGCD.setSelected(true);
2784
usePTrie.setSelected(true);
2785
useOverApproximation.setSelected(true);
2786
2787
useReduction.setToolTipText(TOOL_TIP_USE_STRUCTURALREDUCTION);
2788
useSiphonTrap.setToolTipText(TOOL_TIP_USE_SIPHONTRAP);
2789
useQueryReduction.setToolTipText(TOOL_TIP_USE_QUERY_REDUCTION);
2790
useStubbornReduction.setToolTipText(TOOL_TIP_STUBBORN_REDUCTION);
2791
symmetryReduction.setToolTipText(TOOL_TIP_SYMMETRY_REDUCTION);
2792
discreteInclusion.setToolTipText(TOOL_TIP_DISCRETE_INCLUSION);
2793
selectInclusionPlacesButton.setToolTipText(TOOL_TIP_SELECT_INCLUSION_PLACES);
2794
useTimeDarts.setToolTipText(TOOL_TIP_TIME_DARTS);
2795
useGCD.setToolTipText(TOOL_TIP_GCD);
2796
usePTrie.setToolTipText(TOOL_TIP_PTRIE);
2797
useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
2798
2799
if (lens.isTimed()) {
2800
initTimedReductionOptions();
2801
} else {
2802
initUntimedReductionOptions();
2803
}
2461
2804
2462
2805
gbc = new GridBagConstraints();
2463
2806
gbc.gridx = 0;
2467
2810
add(reductionOptionsPanel, gbc);
2468
2811
}
2469
2812
2813
private void initTimedReductionOptions() {
2814
GridBagConstraints gbc = new GridBagConstraints();
2815
gbc.gridx = 2;
2816
gbc.gridy = 0;
2817
gbc.anchor = GridBagConstraints.WEST;
2818
gbc.insets = new Insets(0,5,0,5);
2819
reductionOptionsPanel.add(symmetryReduction, gbc);
2820
gbc.gridx = 2;
2821
gbc.gridy = 1;
2822
reductionOptionsPanel.add(discreteInclusion, gbc);
2823
gbc.gridx = 2;
2824
gbc.gridy = 1;
2825
reductionOptionsPanel.add(useStubbornReduction, gbc);
2826
gbc.gridx = 2;
2827
gbc.gridy = 2;
2828
reductionOptionsPanel.add(useOverApproximation, gbc);
2829
gbc.gridx = 3;
2830
gbc.gridy = 1;
2831
reductionOptionsPanel.add(selectInclusionPlacesButton, gbc);
2832
gbc.gridx = 3;
2833
gbc.gridy = 2;
2834
reductionOptionsPanel.add(useTimeDarts, gbc);
2835
gbc.gridx = 3;
2836
gbc.gridy = 0;
2837
reductionOptionsPanel.add(useGCD, gbc);
2838
gbc.gridx = 3;
2839
gbc.gridy = 1;
2840
reductionOptionsPanel.add(selectInclusionPlacesButton, gbc);
2841
gbc.gridx = 3;
2842
gbc.gridy = 1;
2843
reductionOptionsPanel.add(usePTrie, gbc);
2844
2845
discreteInclusion.addActionListener(new ActionListener() {
2846
public void actionPerformed(ActionEvent e) {
2847
selectInclusionPlacesButton.setEnabled(discreteInclusion.isSelected());
2848
}
2849
});
2850
2851
selectInclusionPlacesButton.addActionListener(new ActionListener() {
2852
public void actionPerformed(ActionEvent e) {
2853
inclusionPlaces = ChooseInclusionPlacesDialog.showInclusionPlacesDialog(tapnNetwork, inclusionPlaces);
2854
}
2855
});
2856
2857
useTimeDarts.addActionListener(e -> setEnabledOptionsAccordingToCurrentReduction());
2858
}
2859
2860
private void initUntimedReductionOptions() {
2861
GridBagConstraints gbc = new GridBagConstraints();
2862
gbc.gridx = 2;
2863
gbc.gridy = 0;
2864
gbc.anchor = GridBagConstraints.WEST;
2865
gbc.insets = new Insets(0,5,0,5);
2866
reductionOptionsPanel.add(useReduction, gbc);
2867
gbc.gridx = 2;
2868
gbc.gridy = 1;
2869
reductionOptionsPanel.add(useSiphonTrap, gbc);
2870
gbc.gridx = 2;
2871
gbc.gridy = 2;
2872
reductionOptionsPanel.add(useQueryReduction, gbc);
2873
gbc.gridx = 2;
2874
gbc.gridy = 3;
2875
reductionOptionsPanel.add(useStubbornReduction, gbc);
2876
}
2877
2470
2878
protected void setEnabledOptionsAccordingToCurrentReduction() {
2471
2879
refreshQueryEditingButtons();
2472
2880
refreshTraceOptions();
2473
refreshSymmetryReduction();
2474
refreshStubbornReduction();
2475
refreshDiscreteOptions();
2476
refreshDiscreteInclusion();
2477
refreshOverApproximationOption();
2881
if (lens.isTimed()) {
2882
refreshSymmetryReduction();
2883
refreshStubbornReduction();
2884
refreshDiscreteOptions();
2885
refreshDiscreteInclusion();
2886
refreshOverApproximationOption();
2887
}
2478
2888
updateSearchStrategies();
2479
2889
refreshExportButtonText();
2480
2890
}
2507
2917
2508
2918
private void refreshQueryEditingButtons() {
2509
2919
if(currentSelection != null) {
2510
if(currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
2511
if (lens.isGame()) {
2920
if (lens.isGame()) {
2921
if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
2922
forAllBox.setSelected(false);
2512
2923
enableOnlyForAllBox();
2513
} else {
2924
} else if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
2925
enableOnlyStateButtons();
2926
}
2927
} else if (lens.isTimed()) {
2928
if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
2514
2929
enableOnlyPathButtons();
2930
} else if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
2931
enableOnlyStateButtons();
2515
2932
}
2516
} else if(currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
2517
enableOnlyStateButtons();
2518
}
2519
updateQueryButtonsAccordingToSelection();
2933
updateQueryButtonsAccordingToSelection();
2934
} else {
2935
enableOnlyUntimedStateButtons();
2936
updateQueryButtonsAccordingToSelection();
2937
}
2520
2938
}
2521
2939
}
2522
2940
2526
2944
}
2527
2945
else if(reductionOption.getSelectedItem() == null){
2528
2946
symmetryReduction.setVisible(false);
2529
}
2947
}
2530
2948
else if(reductionOption.getSelectedItem().equals(name_DISCRETE) || reductionOption.getSelectedItem().equals(name_UNTIMED)) {
2531
2949
symmetryReduction.setVisible(true);
2532
symmetryReduction.setSelected(true);
2533
2950
symmetryReduction.setEnabled(false);
2534
2951
}
2535
2952
else if((reductionOption.getSelectedItem().equals(name_COMBI) ||
2538
2955
reductionOption.getSelectedItem().equals(name_BROADCAST) ||
2539
2956
reductionOption.getSelectedItem().equals(name_BROADCASTDEG2)) &&
2540
2957
(!noApproximationEnable.isSelected() ||
2541
someTraceRadioButton.isSelected())
2958
someTraceRadioButton.isSelected())
2542
2959
){
2543
2960
symmetryReduction.setVisible(true);
2544
2961
symmetryReduction.setSelected(false);
2551
2968
}
2552
2969
2553
2970
private void refreshOverApproximationOption() {
2554
if (queryHasDeadlock() || getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")){
2971
if (queryHasDeadlock() || newProperty.toString().contains("EG") || newProperty.toString().contains("AF")){
2555
2972
useOverApproximation.setSelected(false);
2556
2973
useOverApproximation.setEnabled(false);
2557
2974
} else {
2583
3000
2584
3001
private void refreshDiscreteOptions(){
2585
3002
useReduction.setVisible(false);
2586
3003
2587
3004
if(reductionOption.getSelectedItem() == null){
2588
3005
useGCD.setVisible(false);
2589
3006
usePTrie.setVisible(false);
2590
3007
useStubbornReduction.setVisible(false);
2591
3008
useTimeDarts.setVisible(false);
2592
}
3009
}
2593
3010
else if(reductionOption.getSelectedItem().equals(name_DISCRETE)) {
2594
3011
useGCD.setVisible(true);
2595
3012
usePTrie.setVisible(true);
2603
3020
}
2604
3021
2605
3022
// Disable GCD calculation for EG/AF or deadlock queries
2606
if(queryHasDeadlock() || getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>") ||
3023
if(queryHasDeadlock() || newProperty.toString().contains("EG") || newProperty.toString().contains("AF") ||
2607
3024
lens.isGame()){
2608
3025
if(useGCD.isSelected()) hasForcedDisabledGCD = true;
2609
3026
useGCD.setSelected(false);
2611
3028
}
2612
3029
2613
3030
// Disable time darts for EG/AF with deadlock
2614
if(queryHasDeadlock() && (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>"))){
3031
if(queryHasDeadlock() && (newProperty.toString().contains("EG") || newProperty.toString().contains("AF"))){
2615
3032
hasForcedDisabledTimeDarts = useTimeDarts.isSelected();
2616
3033
useTimeDarts.setSelected(false);
2617
3034
useTimeDarts.setEnabled(false);
3035
symmetryReduction.setSelected(false);
3036
symmetryReduction.setEnabled(false);
2618
3037
}
2619
3038
2620
3039
// Disable stubborn reduction for EG/AF queries
2621
if(getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")){
3040
if(newProperty.toString().contains("EG") || newProperty.toString().contains("AF")){
2622
3041
if(useStubbornReduction.isSelected()) hasForcedDisabledStubbornReduction = true;
2623
3042
useStubbornReduction.setSelected(false);
2624
3043
useStubbornReduction.setEnabled(false);
2646
3065
2647
3066
2648
3067
private void queryChanged(){
2649
setEnabledReductionOptions();
2650
refreshOverApproximationOption();
3068
setEnabledReductionOptions();
3069
if (lens.isTimed()) refreshOverApproximationOption();
2651
3070
}
2652
3071
2653
3072
2654
3073
private void initButtonPanel(QueryDialogueOption option) {
2655
3074
buttonPanel = new JPanel(new BorderLayout());
2656
3075
if (option == QueryDialogueOption.Save) {
2657
3076
saveButton = new JButton("Save");
2658
3077
saveAndVerifyButton = new JButton("Save and Verify");
2659
3078
cancelButton = new JButton("Cancel");
2660
3079
2661
3080
mergeNetComponentsButton = new JButton(EXPORT_COMPOSED_BTN_TEXT);
2662
3081
mergeNetComponentsButton.setVisible(false);
2663
3082
2664
3083
saveUppaalXMLButton = new JButton(EXPORT_UPPAAL_BTN_TEXT);
2665
3084
//Only show in advanced mode
2666
3085
saveUppaalXMLButton.setVisible(false);
2667
3086
2668
3087
//Add tool tips
2669
3088
saveButton.setToolTipText(TOOL_TIP_SAVE_BUTTON);
2670
3089
saveAndVerifyButton.setToolTipText(TOOL_TIP_SAVE_AND_VERIFY_BUTTON);
2671
3090
cancelButton.setToolTipText(TOOL_TIP_CANCEL_BUTTON);
2672
3091
saveUppaalXMLButton.setToolTipText(TOOL_TIP_SAVE_UPPAAL_BUTTON);
2673
3092
mergeNetComponentsButton.setToolTipText(TOOL_TIP_SAVE_COMPOSED_BUTTON);
2674
3093
2675
3094
saveButton.addActionListener(new ActionListener() {
2676
3095
public void actionPerformed(ActionEvent evt) {
2677
// TODO make save
3096
// TODO make save
2678
3097
// save();
2679
3098
if (checkIfSomeReductionOption()) {
2680
3099
querySaved = true;
2725
3144
if (xmlFile != null && queryFile != null) {
2726
3145
ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), false);
2727
3146
Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(QueryDialog.this.tapnNetwork);
2728
3147
2729
3148
if (overApproximationEnable.isSelected())
2730
3149
{
2731
3150
OverApproximation overaprx = new OverApproximation();
2735
3154
{
2736
3155
UnderApproximation underaprx = new UnderApproximation();
2737
3156
underaprx.modifyTAPN(transformedModel.value1(), getQuery().approximationDenominator());
2738
}
3157
}
2739
3158
2740
3159
TAPNQuery tapnQuery = getQuery();
2741
3160
dk.aau.cs.model.tapn.TAPNQuery clonedQuery = new dk.aau.cs.model.tapn.TAPNQuery(tapnQuery.getProperty().copy(), tapnQuery.getCapacity());
2742
3161
2743
3162
RenameAllPlacesVisitor visitor = new RenameAllPlacesVisitor(transformedModel.value2());
2744
3163
clonedQuery.getProperty().accept(visitor, null);
2745
3164
if (!lens.isTimed()) {
3165
RenameAllTransitionsVisitor transitionVisitor = new RenameAllTransitionsVisitor(transformedModel.value2());
3166
clonedQuery.getProperty().accept(transitionVisitor, null);
3167
}
2746
3168
if(reduction == ReductionOption.VerifyTAPN || reduction == ReductionOption.VerifyTAPNdiscreteVerification) {
2747
3169
VerifyTAPNExporter exporter = new VerifyTAPNExporter();
2748
3170
exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens);
2771
3193
}
2772
3194
}
2773
3195
});
2774
3196
2775
3197
mergeNetComponentsButton.addActionListener(new ActionListener() {
2776
3198
public void actionPerformed(ActionEvent e) {
2777
3199
TAPNComposer composer = new TAPNComposer(new MessengerImpl(), guiModels, true, true);
2778
3200
Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(tapnNetwork);
2779
3201
2780
3202
ArrayList<Template> templates = new ArrayList<Template>(1);
2781
3203
querySaved = true; //Setting this to true will make sure that new values will be used.
2782
3204
if (overApproximationEnable.isSelected())
2790
3212
underaprx.modifyTAPN(transformedModel.value1(), getQuery().approximationDenominator(), composer.getGuiModel());
2791
3213
}
2792
3214
templates.add(new Template(transformedModel.value1(), composer.getGuiModel(), new Zoomer()));
2793
3215
2794
3216
// Create a constant store
2795
3217
ConstantStore newConstantStore = new ConstantStore();
2796
3218
2797
3219
2798
3220
TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork(newConstantStore);
2799
3221
2800
3222
network.add(transformedModel.value1());
2801
3223
2802
3224
NetWriter tapnWriter = new TimedArcPetriNetNetworkWriter(network, templates, new ArrayList<pipe.dataLayer.TAPNQuery>(0), new ArrayList<Constant>(0));
2803
3225
2804
3226
try {
2805
3227
ByteArrayOutputStream outputStream = tapnWriter.savePNML();
2806
3228
String composedName = "composed-" + CreateGui.getApp().getCurrentTabName();
2812
3234
}
2813
3235
}
2814
3236
});
2815
2816
3237
3238
2817
3239
} else if (option == QueryDialogueOption.Export) {
2818
3240
saveButton = new JButton("export");
2819
3241
cancelButton = new JButton("Cancel");
2830
3252
JPanel rightButtomPanel = new JPanel(new FlowLayout());
2831
3253
leftButtomPanel.add(mergeNetComponentsButton, FlowLayout.LEFT);
2832
3254
leftButtomPanel.add(saveUppaalXMLButton, FlowLayout.LEFT);
2833
2834
3255
3256
2835
3257
rightButtomPanel.add(cancelButton);
2836
3258
2837
3259
rightButtomPanel.add(saveButton);
Loggerhead is a web-based interface for Breezy
Version: 2.0.1