Merge lp:~tapaal-contributor/tapaal/redirect-game-engine-cpn into lp:~tapaal-contributor/tapaal/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
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

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.

review: Needs Fixing
Revision history for this message
Jiri Srba (srba) wrote :

Works as expected.

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java 2022-01-09 18:33:52 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java 2022-01-14 07:59:46 +0000
@@ -31,9 +31,6 @@
31 }31 }
3232
33 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);33 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
34 if (TAPAALGUI.getCurrentTab().getLens().isGame() && !TAPAALGUI.getCurrentTab().getLens().isTimed() && !TAPAALGUI.getCurrentTab().getLens().isColored()) {
35 addGhostPlace(model.value1());
36 }
3734
38 VerifyTAPNExporter exporter = new VerifyTACPNExporter();35 VerifyTAPNExporter exporter = new VerifyTACPNExporter();
3936
4037
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java 2022-01-09 18:33:52 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java 2022-01-14 07:59:46 +0000
@@ -218,9 +218,6 @@
218 }218 }
219219
220 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);220 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
221 if (TAPAALGUI.getCurrentTab().getLens().isGame() && !TAPAALGUI.getCurrentTab().getLens().isTimed()) {
222 addGhostPlace(model.value1());
223 }
224221
225 VerifyTAPNExporter exporter = new VerifyTAPNExporter();222 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
226223
@@ -233,13 +230,6 @@
233 return verify(options, model, exportedModel, query, dataLayerQuery);230 return verify(options, model, exportedModel, query, dataLayerQuery);
234 }231 }
235232
236 //An extra place is added before verifying the query so the timed engine is able to mimic the untimed game semantics.
237 protected void addGhostPlace(TimedArcPetriNet net) {
238 TimedPlace place = new LocalTimedPlace("ghost", new TimeInvariant(true, new IntBound(0)), ColorType.COLORTYPE_DOT);
239 net.add(place);
240 place.addToken(new TimedToken(place, new BigDecimal(0), ColorType.COLORTYPE_DOT.getFirstColor()));
241 }
242
243 protected void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {233 protected void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
244 VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options;234 VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options;
245235
246236
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2022-01-09 14:56:00 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2022-01-14 07:59:46 +0000
@@ -125,14 +125,9 @@
125125
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) {
127 //remove the net prefix from the place name127 //remove the net prefix from the place name
128 String placeName;128 String placeName = mapping.map(p.name()).value2();
129 Place guiPlace = null;129 Place guiPlace = null;
130130
131 if (mapping.map(p.name()) == null) {
132 placeName = "ghost";
133 } else {
134 placeName = mapping.map(p.name()).value2();
135 }
136 for (DataLayer guiModel : guiModels ) {131 for (DataLayer guiModel : guiModels ) {
137 guiPlace = guiModel.getPlaceById(placeName);132 guiPlace = guiModel.getPlaceById(placeName);
138 if (guiPlace != null) {133 if (guiPlace != null) {
139134
=== modified file 'src/net/tapaal/TAPAAL.java'
--- src/net/tapaal/TAPAAL.java 2022-01-09 19:10:28 +0000
+++ src/net/tapaal/TAPAAL.java 2022-01-14 07:59:46 +0000
@@ -120,7 +120,7 @@
120 TAPAALGUI.getApp().setVisible(false);120 TAPAALGUI.getApp().setVisible(false);
121121
122 System.out.println("=============================================================");122 System.out.println("=============================================================");
123 System.out.println("Batch Porcessing");123 System.out.println("Batch Processing");
124 System.out.println("=============================================================");124 System.out.println("=============================================================");
125125
126 System.out.println("Running in batch mode for " + batchFolder.getAbsolutePath());126 System.out.println("Running in batch mode for " + batchFolder.getAbsolutePath());
127127
=== modified file 'src/net/tapaal/gui/petrinet/dialog/QueryDialog.java'
--- src/net/tapaal/gui/petrinet/dialog/QueryDialog.java 2022-01-10 11:04:27 +0000
+++ src/net/tapaal/gui/petrinet/dialog/QueryDialog.java 2022-01-14 07:59:46 +0000
@@ -159,9 +159,6 @@
159 private JRadioButton randomSearch;159 private JRadioButton randomSearch;
160 private JRadioButton heuristicSearch;160 private JRadioButton heuristicSearch;
161161
162
163
164
165 // Trace options panel162 // Trace options panel
166 private JPanel traceOptionsPanel;163 private JPanel traceOptionsPanel;
167164
@@ -170,8 +167,6 @@
170 private JRadioButton someTraceRadioButton;167 private JRadioButton someTraceRadioButton;
171 private JRadioButton fastestTraceRadioButton;168 private JRadioButton fastestTraceRadioButton;
172169
173
174
175 // Unfolding options panel170 // Unfolding options panel
176 private JPanel verificationPanel;171 private JPanel verificationPanel;
177 private JPanel unfoldingOptionsPanel;172 private JPanel unfoldingOptionsPanel;
@@ -416,7 +411,7 @@
416 TAPNQuery.SearchOption searchOption = getSearchOption();411 TAPNQuery.SearchOption searchOption = getSearchOption();
417 ReductionOption reductionOptionToSet = getReductionOption();412 ReductionOption reductionOptionToSet = getReductionOption();
418413
419 if (!lens.isGame() && !lens.isTimed()) {414 if (!lens.isTimed()) {
420 return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);415 return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
421 } else {416 } else {
422 return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);417 return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
@@ -749,7 +744,7 @@
749 templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));744 templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));
750 }745 }
751 }746 }
752 if (!lens.isGame() && !lens.isTimed()) {747 if (!lens.isTimed()) {
753 updateUntimedQueryButtons(node);748 updateUntimedQueryButtons(node);
754 } else {749 } else {
755 updateTimedQueryButtons(node);750 updateTimedQueryButtons(node);
@@ -765,7 +760,7 @@
765 placeTransitionBox.setSelectedItem(transitionNode.getTransition());760 placeTransitionBox.setSelectedItem(transitionNode.getTransition());
766 userChangedAtomicPropSelection = true;761 userChangedAtomicPropSelection = true;
767 }762 }
768 if (!lens.isTimed() && !lens.isGame()) {763 if (!lens.isTimed()) {
769 setEnablednessOfOperatorAndMarkingBoxes();764 setEnablednessOfOperatorAndMarkingBoxes();
770 }765 }
771 if (current instanceof LTLANode || current instanceof LTLENode ||766 if (current instanceof LTLANode || current instanceof LTLENode ||
@@ -956,10 +951,8 @@
956 options.add(engine.nameString);951 options.add(engine.nameString);
957 }952 }
958 }953 }
959 } else if (!lens.isGame()) {954 } else {
960 options.add(name_UNTIMED);955 options.add(name_UNTIMED);
961 } else {
962 options.add(name_DISCRETE);
963 }956 }
964957
965 reductionOption.removeAllItems();958 reductionOption.removeAllItems();
@@ -1307,13 +1300,20 @@
13071300
1308 setEnabledOptionsAccordingToCurrentReduction();1301 setEnabledOptionsAccordingToCurrentReduction();
1309 makeShortcuts();1302 makeShortcuts();
1303
1304 if (lens.isGame() && !lens.isTimed()) {
1305 useReduction.setSelected(false);
1306 useReduction.setEnabled(false);
1307 useSiphonTrap.setSelected(false);
1308 useSiphonTrap.setEnabled(false);
1309 }
1310 }1310 }
13111311
1312 private void setupFromQuery(TAPNQuery queryToCreateFrom) {1312 private void setupFromQuery(TAPNQuery queryToCreateFrom) {
1313 queryName.setText(queryToCreateFrom.getName());1313 queryName.setText(queryToCreateFrom.getName());
1314 numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity());1314 numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity());
13151315
1316 if (lens.isTimed() || lens.isGame()) {1316 if (lens.isTimed()) {
1317 setupQuantificationFromQuery(queryToCreateFrom);1317 setupQuantificationFromQuery(queryToCreateFrom);
1318 setupApproximationOptionsFromQuery(queryToCreateFrom);1318 setupApproximationOptionsFromQuery(queryToCreateFrom);
1319 }1319 }
@@ -1382,7 +1382,7 @@
1382 reductionOption.addItem(reduction);1382 reductionOption.addItem(reduction);
1383 reductionOption.setSelectedItem(reduction);1383 reductionOption.setSelectedItem(reduction);
13841384
1385 if (lens.isTimed() || lens.isGame()) {1385 if (lens.isTimed()) {
1386 setupTimedReductionOptions(queryToCreateFrom);1386 setupTimedReductionOptions(queryToCreateFrom);
1387 } else {1387 } else {
1388 setupUntimedReductionOptions(queryToCreateFrom);1388 setupUntimedReductionOptions(queryToCreateFrom);
@@ -1458,7 +1458,7 @@
1458 }1458 }
14591459
1460 private void setupQueryCategoryFromQuery(TAPNQuery queryToCreateFrom) {1460 private void setupQueryCategoryFromQuery(TAPNQuery queryToCreateFrom) {
1461 if (!lens.isTimed() && !lens.isGame()) {1461 if (!lens.isTimed()) {
1462 TAPNQuery.QueryCategory category = queryToCreateFrom.getCategory();1462 TAPNQuery.QueryCategory category = queryToCreateFrom.getCategory();
1463 if (category.equals(TAPNQuery.QueryCategory.CTL)) {1463 if (category.equals(TAPNQuery.QueryCategory.CTL)) {
1464 queryType.setSelectedIndex(0);1464 queryType.setSelectedIndex(0);
@@ -1605,7 +1605,7 @@
1605 }1605 }
16061606
1607 reductionOptionsPanel.setVisible(advancedView);1607 reductionOptionsPanel.setVisible(advancedView);
1608 if (lens.isTimed() || lens.isGame()) {1608 if (lens.isTimed()) {
1609 saveUppaalXMLButton.setVisible(advancedView);1609 saveUppaalXMLButton.setVisible(advancedView);
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)
1611 overApproximationOptionsPanel.setVisible(advancedView && !lens.isColored());1611 overApproximationOptionsPanel.setVisible(advancedView && !lens.isColored());
@@ -2515,7 +2515,7 @@
2515 });2515 });
25162516
2517 negationButton.addActionListener(e -> {2517 negationButton.addActionListener(e -> {
2518 if (lens.isTimed() || lens.isGame()) {2518 if (lens.isTimed()) {
2519 TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));2519 TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));
2520 addPropertyToQuery(property);2520 addPropertyToQuery(property);
2521 } else {2521 } else {
@@ -2619,7 +2619,7 @@
2619 placeNames.add(place.name());2619 placeNames.add(place.name());
2620 }2620 }
2621 }2621 }
2622 if (!lens.isTimed() && !lens.isGame()) {2622 if (!lens.isTimed()) {
2623 for (TimedTransition transition : tapn.transitions()) {2623 for (TimedTransition transition : tapn.transitions()) {
2624 if (!transition.isShared()) {2624 if (!transition.isShared()) {
2625 placeNames.add(transition.name());2625 placeNames.add(transition.name());
@@ -2641,7 +2641,7 @@
2641 for (SharedPlace place : tapnNetwork.sharedPlaces()) {2641 for (SharedPlace place : tapnNetwork.sharedPlaces()) {
2642 placeNames.add(place.name());2642 placeNames.add(place.name());
2643 }2643 }
2644 if (lens.isTimed() || lens.isGame()) {2644 if (lens.isTimed()) {
2645 for (SharedTransition transition : tapnNetwork.sharedTransitions()) {2645 for (SharedTransition transition : tapnNetwork.sharedTransitions()) {
2646 placeNames.add(transition.name());2646 placeNames.add(transition.name());
2647 }2647 }
@@ -2655,7 +2655,7 @@
2655 updateQueryOnAtomicPropositionChange();2655 updateQueryOnAtomicPropositionChange();
2656 }2656 }
2657 }2657 }
2658 if (!lens.isTimed() && !lens.isGame()) setEnablednessOfOperatorAndMarkingBoxes();2658 if (!lens.isTimed()) setEnablednessOfOperatorAndMarkingBoxes();
26592659
2660 }2660 }
2661 });2661 });
@@ -2692,7 +2692,7 @@
26922692
2693 transitionIsEnabledLabel = new JLabel(" is enabled");2693 transitionIsEnabledLabel = new JLabel(" is enabled");
2694 transitionIsEnabledLabel.setPreferredSize(new Dimension(165, 27));2694 transitionIsEnabledLabel.setPreferredSize(new Dimension(165, 27));
2695 if (!lens.isTimed() && !lens.isGame()) placeRow.add(transitionIsEnabledLabel);2695 if (!lens.isTimed()) placeRow.add(transitionIsEnabledLabel);
26962696
2697 JPanel addPredicateRow = new JPanel(new FlowLayout(FlowLayout.CENTER));2697 JPanel addPredicateRow = new JPanel(new FlowLayout(FlowLayout.CENTER));
2698 gbc.gridy = 2;2698 gbc.gridy = 2;
@@ -2754,7 +2754,7 @@
2754 String template = templateBox.getSelectedItem().toString();2754 String template = templateBox.getSelectedItem().toString();
2755 if(template.equals(SHARED)) template = "";2755 if(template.equals(SHARED)) template = "";
27562756
2757 if ((!lens.isTimed() && !lens.isGame()) && transitionIsSelected()) {2757 if ((!lens.isTimed()) && transitionIsSelected()) {
2758 addPropertyToQuery(new TCTLTransitionNode(template, (String) placeTransitionBox.getSelectedItem()));2758 addPropertyToQuery(new TCTLTransitionNode(template, (String) placeTransitionBox.getSelectedItem()));
2759 } else {2759 } else {
2760 TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(2760 TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(
@@ -2791,7 +2791,7 @@
2791 if (userChangedAtomicPropSelection) {2791 if (userChangedAtomicPropSelection) {
2792 updateQueryOnAtomicPropositionChange();2792 updateQueryOnAtomicPropositionChange();
2793 }2793 }
2794 if (!lens.isTimed() && !lens.isGame()) {2794 if (!lens.isTimed()) {
2795 setEnablednessOfOperatorAndMarkingBoxes();2795 setEnablednessOfOperatorAndMarkingBoxes();
2796 }2796 }
2797 });2797 });
@@ -2913,7 +2913,7 @@
29132913
2914 boolean isResultFalse;2914 boolean isResultFalse;
29152915
2916 if (lens.isTimed() || lens.isGame()) {2916 if (lens.isTimed()) {
2917 isResultFalse = !placeContext.getResult();2917 isResultFalse = !placeContext.getResult();
2918 } else {2918 } else {
2919 isResultFalse = !transitionContext.getResult() || !placeContext.getResult();2919 isResultFalse = !transitionContext.getResult() || !placeContext.getResult();
@@ -3027,7 +3027,7 @@
3027 ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();3027 ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();
3028 for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {3028 for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
3029 for(TimedPlace p : tapn.places()) {3029 for(TimedPlace p : tapn.places()) {
3030 if (lens.isTimed() || !p.isShared() || lens.isGame()) {3030 if (lens.isTimed() || !p.isShared()) {
3031 templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));3031 templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
3032 }3032 }
3033 }3033 }
@@ -3047,7 +3047,7 @@
3047 ArrayList<Tuple<String,String>> templateTransitionNames = new ArrayList<Tuple<String,String>>();3047 ArrayList<Tuple<String,String>> templateTransitionNames = new ArrayList<Tuple<String,String>>();
3048 for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {3048 for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
3049 for (TimedTransition t : tapn.transitions()) {3049 for (TimedTransition t : tapn.transitions()) {
3050 if (lens.isTimed() || !t.isShared() || lens.isGame()) {3050 if (lens.isTimed() || !t.isShared()) {
3051 templateTransitionNames.add(new Tuple<>(tapn.name(), t.name()));3051 templateTransitionNames.add(new Tuple<>(tapn.name(), t.name()));
3052 }3052 }
3053 }3053 }
@@ -3229,7 +3229,7 @@
3229 gridBagConstraints.anchor = GridBagConstraints.WEST;3229 gridBagConstraints.anchor = GridBagConstraints.WEST;
3230 traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);3230 traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);
32313231
3232 if (lens.isTimed() || lens.isGame()) {3232 if (lens.isTimed()) {
3233 gridBagConstraints.gridy = 2;3233 gridBagConstraints.gridy = 2;
3234 gridBagConstraints.weightx = 1;3234 gridBagConstraints.weightx = 1;
3235 gridBagConstraints.anchor = GridBagConstraints.WEST;3235 gridBagConstraints.anchor = GridBagConstraints.WEST;
@@ -3372,7 +3372,7 @@
33723372
3373 useTarjan.addActionListener(e -> updateSearchStrategies());3373 useTarjan.addActionListener(e -> updateSearchStrategies());
33743374
3375 if (lens.isTimed() || lens.isGame()) {3375 if (lens.isTimed()) {
3376 initTimedReductionOptions();3376 initTimedReductionOptions();
3377 } else {3377 } else {
3378 useReduction.addActionListener(new ActionListener() {3378 useReduction.addActionListener(new ActionListener() {
@@ -3467,7 +3467,7 @@
3467 protected void setEnabledOptionsAccordingToCurrentReduction() {3467 protected void setEnabledOptionsAccordingToCurrentReduction() {
3468 refreshQueryEditingButtons();3468 refreshQueryEditingButtons();
3469 refreshTraceOptions();3469 refreshTraceOptions();
3470 if (lens.isTimed() || lens.isGame()) {3470 if (lens.isTimed()) {
3471 refreshSymmetryReduction();3471 refreshSymmetryReduction();
3472 refreshStubbornReduction();3472 refreshStubbornReduction();
3473 refreshDiscreteOptions();3473 refreshDiscreteOptions();

Subscribers

People subscribed via source and target branches

to all changes: