Merge lp:~tapaal-contributor/tapaal/redirect-game-engine-cpn into lp:~tapaal-contributor/tapaal/cpn-gui-dev
- redirect-game-engine-cpn
- Merge into cpn-gui-dev
Proposed by
Lena Ernstsen
Status: | Merged |
---|---|
Approved by: | Jiri Srba |
Approved revision: | 1554 |
Merged at revision: | 1550 |
Proposed branch: | lp:~tapaal-contributor/tapaal/redirect-game-engine-cpn |
Merge into: | lp:~tapaal-contributor/tapaal/cpn-gui-dev |
Diff against target: |
302 lines (+30/-48) 5 files modified
src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java (+0/-3) src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java (+0/-10) src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java (+1/-6) src/net/tapaal/TAPAAL.java (+1/-1) src/net/tapaal/gui/petrinet/dialog/QueryDialog.java (+28/-28) |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/redirect-game-engine-cpn |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Review via email: mp+414145@code.launchpad.net |
This proposal supersedes a proposal from 2022-01-12.
Commit message
Calls the verifypn engine when the net is untimed and game
Description of the change
Removed ghost node when the net is untimed and game
To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote : Posted in a previous version of this proposal | # |
review:
Needs Fixing
Preview Diff
[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java' | |||
2 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java 2022-01-09 18:33:52 +0000 | |||
3 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java 2022-01-14 07:59:46 +0000 | |||
4 | @@ -31,9 +31,6 @@ | |||
5 | 31 | } | 31 | } |
6 | 32 | 32 | ||
7 | 33 | if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model); | 33 | if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model); |
8 | 34 | if (TAPAALGUI.getCurrentTab().getLens().isGame() && !TAPAALGUI.getCurrentTab().getLens().isTimed() && !TAPAALGUI.getCurrentTab().getLens().isColored()) { | ||
9 | 35 | addGhostPlace(model.value1()); | ||
10 | 36 | } | ||
11 | 37 | 34 | ||
12 | 38 | VerifyTAPNExporter exporter = new VerifyTACPNExporter(); | 35 | VerifyTAPNExporter exporter = new VerifyTACPNExporter(); |
13 | 39 | 36 | ||
14 | 40 | 37 | ||
15 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java' | |||
16 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java 2022-01-09 18:33:52 +0000 | |||
17 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java 2022-01-14 07:59:46 +0000 | |||
18 | @@ -218,9 +218,6 @@ | |||
19 | 218 | } | 218 | } |
20 | 219 | 219 | ||
21 | 220 | if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model); | 220 | if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model); |
22 | 221 | if (TAPAALGUI.getCurrentTab().getLens().isGame() && !TAPAALGUI.getCurrentTab().getLens().isTimed()) { | ||
23 | 222 | addGhostPlace(model.value1()); | ||
24 | 223 | } | ||
25 | 224 | 221 | ||
26 | 225 | VerifyTAPNExporter exporter = new VerifyTAPNExporter(); | 222 | VerifyTAPNExporter exporter = new VerifyTAPNExporter(); |
27 | 226 | 223 | ||
28 | @@ -233,13 +230,6 @@ | |||
29 | 233 | return verify(options, model, exportedModel, query, dataLayerQuery); | 230 | return verify(options, model, exportedModel, query, dataLayerQuery); |
30 | 234 | } | 231 | } |
31 | 235 | 232 | ||
32 | 236 | //An extra place is added before verifying the query so the timed engine is able to mimic the untimed game semantics. | ||
33 | 237 | protected void addGhostPlace(TimedArcPetriNet net) { | ||
34 | 238 | TimedPlace place = new LocalTimedPlace("ghost", new TimeInvariant(true, new IntBound(0)), ColorType.COLORTYPE_DOT); | ||
35 | 239 | net.add(place); | ||
36 | 240 | place.addToken(new TimedToken(place, new BigDecimal(0), ColorType.COLORTYPE_DOT.getFirstColor())); | ||
37 | 241 | } | ||
38 | 242 | |||
39 | 243 | protected void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) { | 233 | protected void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) { |
40 | 244 | VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options; | 234 | VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options; |
41 | 245 | 235 | ||
42 | 246 | 236 | ||
43 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java' | |||
44 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2022-01-09 14:56:00 +0000 | |||
45 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2022-01-14 07:59:46 +0000 | |||
46 | @@ -125,14 +125,9 @@ | |||
47 | 125 | 125 | ||
48 | 126 | protected void outputPlace(TimedPlace p, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) { | 126 | protected void outputPlace(TimedPlace p, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) { |
49 | 127 | //remove the net prefix from the place name | 127 | //remove the net prefix from the place name |
51 | 128 | String placeName; | 128 | String placeName = mapping.map(p.name()).value2(); |
52 | 129 | Place guiPlace = null; | 129 | Place guiPlace = null; |
53 | 130 | 130 | ||
54 | 131 | if (mapping.map(p.name()) == null) { | ||
55 | 132 | placeName = "ghost"; | ||
56 | 133 | } else { | ||
57 | 134 | placeName = mapping.map(p.name()).value2(); | ||
58 | 135 | } | ||
59 | 136 | for (DataLayer guiModel : guiModels ) { | 131 | for (DataLayer guiModel : guiModels ) { |
60 | 137 | guiPlace = guiModel.getPlaceById(placeName); | 132 | guiPlace = guiModel.getPlaceById(placeName); |
61 | 138 | if (guiPlace != null) { | 133 | if (guiPlace != null) { |
62 | 139 | 134 | ||
63 | === modified file 'src/net/tapaal/TAPAAL.java' | |||
64 | --- src/net/tapaal/TAPAAL.java 2022-01-09 19:10:28 +0000 | |||
65 | +++ src/net/tapaal/TAPAAL.java 2022-01-14 07:59:46 +0000 | |||
66 | @@ -120,7 +120,7 @@ | |||
67 | 120 | TAPAALGUI.getApp().setVisible(false); | 120 | TAPAALGUI.getApp().setVisible(false); |
68 | 121 | 121 | ||
69 | 122 | System.out.println("============================================================="); | 122 | System.out.println("============================================================="); |
71 | 123 | System.out.println("Batch Porcessing"); | 123 | System.out.println("Batch Processing"); |
72 | 124 | System.out.println("============================================================="); | 124 | System.out.println("============================================================="); |
73 | 125 | 125 | ||
74 | 126 | System.out.println("Running in batch mode for " + batchFolder.getAbsolutePath()); | 126 | System.out.println("Running in batch mode for " + batchFolder.getAbsolutePath()); |
75 | 127 | 127 | ||
76 | === modified file 'src/net/tapaal/gui/petrinet/dialog/QueryDialog.java' | |||
77 | --- src/net/tapaal/gui/petrinet/dialog/QueryDialog.java 2022-01-10 11:04:27 +0000 | |||
78 | +++ src/net/tapaal/gui/petrinet/dialog/QueryDialog.java 2022-01-14 07:59:46 +0000 | |||
79 | @@ -159,9 +159,6 @@ | |||
80 | 159 | private JRadioButton randomSearch; | 159 | private JRadioButton randomSearch; |
81 | 160 | private JRadioButton heuristicSearch; | 160 | private JRadioButton heuristicSearch; |
82 | 161 | 161 | ||
83 | 162 | |||
84 | 163 | |||
85 | 164 | |||
86 | 165 | // Trace options panel | 162 | // Trace options panel |
87 | 166 | private JPanel traceOptionsPanel; | 163 | private JPanel traceOptionsPanel; |
88 | 167 | 164 | ||
89 | @@ -170,8 +167,6 @@ | |||
90 | 170 | private JRadioButton someTraceRadioButton; | 167 | private JRadioButton someTraceRadioButton; |
91 | 171 | private JRadioButton fastestTraceRadioButton; | 168 | private JRadioButton fastestTraceRadioButton; |
92 | 172 | 169 | ||
93 | 173 | |||
94 | 174 | |||
95 | 175 | // Unfolding options panel | 170 | // Unfolding options panel |
96 | 176 | private JPanel verificationPanel; | 171 | private JPanel verificationPanel; |
97 | 177 | private JPanel unfoldingOptionsPanel; | 172 | private JPanel unfoldingOptionsPanel; |
98 | @@ -416,7 +411,7 @@ | |||
99 | 416 | TAPNQuery.SearchOption searchOption = getSearchOption(); | 411 | TAPNQuery.SearchOption searchOption = getSearchOption(); |
100 | 417 | ReductionOption reductionOptionToSet = getReductionOption(); | 412 | ReductionOption reductionOptionToSet = getReductionOption(); |
101 | 418 | 413 | ||
103 | 419 | if (!lens.isGame() && !lens.isTimed()) { | 414 | if (!lens.isTimed()) { |
104 | 420 | return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet); | 415 | return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet); |
105 | 421 | } else { | 416 | } else { |
106 | 422 | return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet); | 417 | return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet); |
107 | @@ -749,7 +744,7 @@ | |||
108 | 749 | templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate())); | 744 | templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate())); |
109 | 750 | } | 745 | } |
110 | 751 | } | 746 | } |
112 | 752 | if (!lens.isGame() && !lens.isTimed()) { | 747 | if (!lens.isTimed()) { |
113 | 753 | updateUntimedQueryButtons(node); | 748 | updateUntimedQueryButtons(node); |
114 | 754 | } else { | 749 | } else { |
115 | 755 | updateTimedQueryButtons(node); | 750 | updateTimedQueryButtons(node); |
116 | @@ -765,7 +760,7 @@ | |||
117 | 765 | placeTransitionBox.setSelectedItem(transitionNode.getTransition()); | 760 | placeTransitionBox.setSelectedItem(transitionNode.getTransition()); |
118 | 766 | userChangedAtomicPropSelection = true; | 761 | userChangedAtomicPropSelection = true; |
119 | 767 | } | 762 | } |
121 | 768 | if (!lens.isTimed() && !lens.isGame()) { | 763 | if (!lens.isTimed()) { |
122 | 769 | setEnablednessOfOperatorAndMarkingBoxes(); | 764 | setEnablednessOfOperatorAndMarkingBoxes(); |
123 | 770 | } | 765 | } |
124 | 771 | if (current instanceof LTLANode || current instanceof LTLENode || | 766 | if (current instanceof LTLANode || current instanceof LTLENode || |
125 | @@ -956,10 +951,8 @@ | |||
126 | 956 | options.add(engine.nameString); | 951 | options.add(engine.nameString); |
127 | 957 | } | 952 | } |
128 | 958 | } | 953 | } |
130 | 959 | } else if (!lens.isGame()) { | 954 | } else { |
131 | 960 | options.add(name_UNTIMED); | 955 | options.add(name_UNTIMED); |
132 | 961 | } else { | ||
133 | 962 | options.add(name_DISCRETE); | ||
134 | 963 | } | 956 | } |
135 | 964 | 957 | ||
136 | 965 | reductionOption.removeAllItems(); | 958 | reductionOption.removeAllItems(); |
137 | @@ -1307,13 +1300,20 @@ | |||
138 | 1307 | 1300 | ||
139 | 1308 | setEnabledOptionsAccordingToCurrentReduction(); | 1301 | setEnabledOptionsAccordingToCurrentReduction(); |
140 | 1309 | makeShortcuts(); | 1302 | makeShortcuts(); |
141 | 1303 | |||
142 | 1304 | if (lens.isGame() && !lens.isTimed()) { | ||
143 | 1305 | useReduction.setSelected(false); | ||
144 | 1306 | useReduction.setEnabled(false); | ||
145 | 1307 | useSiphonTrap.setSelected(false); | ||
146 | 1308 | useSiphonTrap.setEnabled(false); | ||
147 | 1309 | } | ||
148 | 1310 | } | 1310 | } |
149 | 1311 | 1311 | ||
150 | 1312 | private void setupFromQuery(TAPNQuery queryToCreateFrom) { | 1312 | private void setupFromQuery(TAPNQuery queryToCreateFrom) { |
151 | 1313 | queryName.setText(queryToCreateFrom.getName()); | 1313 | queryName.setText(queryToCreateFrom.getName()); |
152 | 1314 | numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity()); | 1314 | numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity()); |
153 | 1315 | 1315 | ||
155 | 1316 | if (lens.isTimed() || lens.isGame()) { | 1316 | if (lens.isTimed()) { |
156 | 1317 | setupQuantificationFromQuery(queryToCreateFrom); | 1317 | setupQuantificationFromQuery(queryToCreateFrom); |
157 | 1318 | setupApproximationOptionsFromQuery(queryToCreateFrom); | 1318 | setupApproximationOptionsFromQuery(queryToCreateFrom); |
158 | 1319 | } | 1319 | } |
159 | @@ -1382,7 +1382,7 @@ | |||
160 | 1382 | reductionOption.addItem(reduction); | 1382 | reductionOption.addItem(reduction); |
161 | 1383 | reductionOption.setSelectedItem(reduction); | 1383 | reductionOption.setSelectedItem(reduction); |
162 | 1384 | 1384 | ||
164 | 1385 | if (lens.isTimed() || lens.isGame()) { | 1385 | if (lens.isTimed()) { |
165 | 1386 | setupTimedReductionOptions(queryToCreateFrom); | 1386 | setupTimedReductionOptions(queryToCreateFrom); |
166 | 1387 | } else { | 1387 | } else { |
167 | 1388 | setupUntimedReductionOptions(queryToCreateFrom); | 1388 | setupUntimedReductionOptions(queryToCreateFrom); |
168 | @@ -1458,7 +1458,7 @@ | |||
169 | 1458 | } | 1458 | } |
170 | 1459 | 1459 | ||
171 | 1460 | private void setupQueryCategoryFromQuery(TAPNQuery queryToCreateFrom) { | 1460 | private void setupQueryCategoryFromQuery(TAPNQuery queryToCreateFrom) { |
173 | 1461 | if (!lens.isTimed() && !lens.isGame()) { | 1461 | if (!lens.isTimed()) { |
174 | 1462 | TAPNQuery.QueryCategory category = queryToCreateFrom.getCategory(); | 1462 | TAPNQuery.QueryCategory category = queryToCreateFrom.getCategory(); |
175 | 1463 | if (category.equals(TAPNQuery.QueryCategory.CTL)) { | 1463 | if (category.equals(TAPNQuery.QueryCategory.CTL)) { |
176 | 1464 | queryType.setSelectedIndex(0); | 1464 | queryType.setSelectedIndex(0); |
177 | @@ -1605,7 +1605,7 @@ | |||
178 | 1605 | } | 1605 | } |
179 | 1606 | 1606 | ||
180 | 1607 | reductionOptionsPanel.setVisible(advancedView); | 1607 | reductionOptionsPanel.setVisible(advancedView); |
182 | 1608 | if (lens.isTimed() || lens.isGame()) { | 1608 | if (lens.isTimed()) { |
183 | 1609 | saveUppaalXMLButton.setVisible(advancedView); | 1609 | saveUppaalXMLButton.setVisible(advancedView); |
184 | 1610 | // Disabled approximation options for colored models, because they are not supported yet (will generate error) | 1610 | // Disabled approximation options for colored models, because they are not supported yet (will generate error) |
185 | 1611 | overApproximationOptionsPanel.setVisible(advancedView && !lens.isColored()); | 1611 | overApproximationOptionsPanel.setVisible(advancedView && !lens.isColored()); |
186 | @@ -2515,7 +2515,7 @@ | |||
187 | 2515 | }); | 2515 | }); |
188 | 2516 | 2516 | ||
189 | 2517 | negationButton.addActionListener(e -> { | 2517 | negationButton.addActionListener(e -> { |
191 | 2518 | if (lens.isTimed() || lens.isGame()) { | 2518 | if (lens.isTimed()) { |
192 | 2519 | TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject())); | 2519 | TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject())); |
193 | 2520 | addPropertyToQuery(property); | 2520 | addPropertyToQuery(property); |
194 | 2521 | } else { | 2521 | } else { |
195 | @@ -2619,7 +2619,7 @@ | |||
196 | 2619 | placeNames.add(place.name()); | 2619 | placeNames.add(place.name()); |
197 | 2620 | } | 2620 | } |
198 | 2621 | } | 2621 | } |
200 | 2622 | if (!lens.isTimed() && !lens.isGame()) { | 2622 | if (!lens.isTimed()) { |
201 | 2623 | for (TimedTransition transition : tapn.transitions()) { | 2623 | for (TimedTransition transition : tapn.transitions()) { |
202 | 2624 | if (!transition.isShared()) { | 2624 | if (!transition.isShared()) { |
203 | 2625 | placeNames.add(transition.name()); | 2625 | placeNames.add(transition.name()); |
204 | @@ -2641,7 +2641,7 @@ | |||
205 | 2641 | for (SharedPlace place : tapnNetwork.sharedPlaces()) { | 2641 | for (SharedPlace place : tapnNetwork.sharedPlaces()) { |
206 | 2642 | placeNames.add(place.name()); | 2642 | placeNames.add(place.name()); |
207 | 2643 | } | 2643 | } |
209 | 2644 | if (lens.isTimed() || lens.isGame()) { | 2644 | if (lens.isTimed()) { |
210 | 2645 | for (SharedTransition transition : tapnNetwork.sharedTransitions()) { | 2645 | for (SharedTransition transition : tapnNetwork.sharedTransitions()) { |
211 | 2646 | placeNames.add(transition.name()); | 2646 | placeNames.add(transition.name()); |
212 | 2647 | } | 2647 | } |
213 | @@ -2655,7 +2655,7 @@ | |||
214 | 2655 | updateQueryOnAtomicPropositionChange(); | 2655 | updateQueryOnAtomicPropositionChange(); |
215 | 2656 | } | 2656 | } |
216 | 2657 | } | 2657 | } |
218 | 2658 | if (!lens.isTimed() && !lens.isGame()) setEnablednessOfOperatorAndMarkingBoxes(); | 2658 | if (!lens.isTimed()) setEnablednessOfOperatorAndMarkingBoxes(); |
219 | 2659 | 2659 | ||
220 | 2660 | } | 2660 | } |
221 | 2661 | }); | 2661 | }); |
222 | @@ -2692,7 +2692,7 @@ | |||
223 | 2692 | 2692 | ||
224 | 2693 | transitionIsEnabledLabel = new JLabel(" is enabled"); | 2693 | transitionIsEnabledLabel = new JLabel(" is enabled"); |
225 | 2694 | transitionIsEnabledLabel.setPreferredSize(new Dimension(165, 27)); | 2694 | transitionIsEnabledLabel.setPreferredSize(new Dimension(165, 27)); |
227 | 2695 | if (!lens.isTimed() && !lens.isGame()) placeRow.add(transitionIsEnabledLabel); | 2695 | if (!lens.isTimed()) placeRow.add(transitionIsEnabledLabel); |
228 | 2696 | 2696 | ||
229 | 2697 | JPanel addPredicateRow = new JPanel(new FlowLayout(FlowLayout.CENTER)); | 2697 | JPanel addPredicateRow = new JPanel(new FlowLayout(FlowLayout.CENTER)); |
230 | 2698 | gbc.gridy = 2; | 2698 | gbc.gridy = 2; |
231 | @@ -2754,7 +2754,7 @@ | |||
232 | 2754 | String template = templateBox.getSelectedItem().toString(); | 2754 | String template = templateBox.getSelectedItem().toString(); |
233 | 2755 | if(template.equals(SHARED)) template = ""; | 2755 | if(template.equals(SHARED)) template = ""; |
234 | 2756 | 2756 | ||
236 | 2757 | if ((!lens.isTimed() && !lens.isGame()) && transitionIsSelected()) { | 2757 | if ((!lens.isTimed()) && transitionIsSelected()) { |
237 | 2758 | addPropertyToQuery(new TCTLTransitionNode(template, (String) placeTransitionBox.getSelectedItem())); | 2758 | addPropertyToQuery(new TCTLTransitionNode(template, (String) placeTransitionBox.getSelectedItem())); |
238 | 2759 | } else { | 2759 | } else { |
239 | 2760 | TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode( | 2760 | TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode( |
240 | @@ -2791,7 +2791,7 @@ | |||
241 | 2791 | if (userChangedAtomicPropSelection) { | 2791 | if (userChangedAtomicPropSelection) { |
242 | 2792 | updateQueryOnAtomicPropositionChange(); | 2792 | updateQueryOnAtomicPropositionChange(); |
243 | 2793 | } | 2793 | } |
245 | 2794 | if (!lens.isTimed() && !lens.isGame()) { | 2794 | if (!lens.isTimed()) { |
246 | 2795 | setEnablednessOfOperatorAndMarkingBoxes(); | 2795 | setEnablednessOfOperatorAndMarkingBoxes(); |
247 | 2796 | } | 2796 | } |
248 | 2797 | }); | 2797 | }); |
249 | @@ -2913,7 +2913,7 @@ | |||
250 | 2913 | 2913 | ||
251 | 2914 | boolean isResultFalse; | 2914 | boolean isResultFalse; |
252 | 2915 | 2915 | ||
254 | 2916 | if (lens.isTimed() || lens.isGame()) { | 2916 | if (lens.isTimed()) { |
255 | 2917 | isResultFalse = !placeContext.getResult(); | 2917 | isResultFalse = !placeContext.getResult(); |
256 | 2918 | } else { | 2918 | } else { |
257 | 2919 | isResultFalse = !transitionContext.getResult() || !placeContext.getResult(); | 2919 | isResultFalse = !transitionContext.getResult() || !placeContext.getResult(); |
258 | @@ -3027,7 +3027,7 @@ | |||
259 | 3027 | ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>(); | 3027 | ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>(); |
260 | 3028 | for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) { | 3028 | for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) { |
261 | 3029 | for(TimedPlace p : tapn.places()) { | 3029 | for(TimedPlace p : tapn.places()) { |
263 | 3030 | if (lens.isTimed() || !p.isShared() || lens.isGame()) { | 3030 | if (lens.isTimed() || !p.isShared()) { |
264 | 3031 | templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name())); | 3031 | templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name())); |
265 | 3032 | } | 3032 | } |
266 | 3033 | } | 3033 | } |
267 | @@ -3047,7 +3047,7 @@ | |||
268 | 3047 | ArrayList<Tuple<String,String>> templateTransitionNames = new ArrayList<Tuple<String,String>>(); | 3047 | ArrayList<Tuple<String,String>> templateTransitionNames = new ArrayList<Tuple<String,String>>(); |
269 | 3048 | for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) { | 3048 | for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) { |
270 | 3049 | for (TimedTransition t : tapn.transitions()) { | 3049 | for (TimedTransition t : tapn.transitions()) { |
272 | 3050 | if (lens.isTimed() || !t.isShared() || lens.isGame()) { | 3050 | if (lens.isTimed() || !t.isShared()) { |
273 | 3051 | templateTransitionNames.add(new Tuple<>(tapn.name(), t.name())); | 3051 | templateTransitionNames.add(new Tuple<>(tapn.name(), t.name())); |
274 | 3052 | } | 3052 | } |
275 | 3053 | } | 3053 | } |
276 | @@ -3229,7 +3229,7 @@ | |||
277 | 3229 | gridBagConstraints.anchor = GridBagConstraints.WEST; | 3229 | gridBagConstraints.anchor = GridBagConstraints.WEST; |
278 | 3230 | traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints); | 3230 | traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints); |
279 | 3231 | 3231 | ||
281 | 3232 | if (lens.isTimed() || lens.isGame()) { | 3232 | if (lens.isTimed()) { |
282 | 3233 | gridBagConstraints.gridy = 2; | 3233 | gridBagConstraints.gridy = 2; |
283 | 3234 | gridBagConstraints.weightx = 1; | 3234 | gridBagConstraints.weightx = 1; |
284 | 3235 | gridBagConstraints.anchor = GridBagConstraints.WEST; | 3235 | gridBagConstraints.anchor = GridBagConstraints.WEST; |
285 | @@ -3372,7 +3372,7 @@ | |||
286 | 3372 | 3372 | ||
287 | 3373 | useTarjan.addActionListener(e -> updateSearchStrategies()); | 3373 | useTarjan.addActionListener(e -> updateSearchStrategies()); |
288 | 3374 | 3374 | ||
290 | 3375 | if (lens.isTimed() || lens.isGame()) { | 3375 | if (lens.isTimed()) { |
291 | 3376 | initTimedReductionOptions(); | 3376 | initTimedReductionOptions(); |
292 | 3377 | } else { | 3377 | } else { |
293 | 3378 | useReduction.addActionListener(new ActionListener() { | 3378 | useReduction.addActionListener(new ActionListener() { |
294 | @@ -3467,7 +3467,7 @@ | |||
295 | 3467 | protected void setEnabledOptionsAccordingToCurrentReduction() { | 3467 | protected void setEnabledOptionsAccordingToCurrentReduction() { |
296 | 3468 | refreshQueryEditingButtons(); | 3468 | refreshQueryEditingButtons(); |
297 | 3469 | refreshTraceOptions(); | 3469 | refreshTraceOptions(); |
299 | 3470 | if (lens.isTimed() || lens.isGame()) { | 3470 | if (lens.isTimed()) { |
300 | 3471 | refreshSymmetryReduction(); | 3471 | refreshSymmetryReduction(); |
301 | 3472 | refreshStubbornReduction(); | 3472 | refreshStubbornReduction(); |
302 | 3473 | refreshDiscreteOptions(); | 3473 | refreshDiscreteOptions(); |
Approximation options should not be available when the lens is untimed and the state-equation options cannot be enabled and partial-order reduction option is missing.