Merge lp:~tapaal-contributor/tapaal/add-discrete-to-untimed into lp:tapaal

Proposed by Lena Said
Status: Merged
Approved by: Jiri Srba
Approved revision: 1107
Merged at revision: 1110
Proposed branch: lp:~tapaal-contributor/tapaal/add-discrete-to-untimed
Merge into: lp:tapaal
Diff against target: 222 lines (+39/-23)
3 files modified
src/dk/aau/cs/gui/TabContent.java (+4/-0)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java (+15/-5)
src/pipe/gui/widgets/QueryDialog.java (+20/-18)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/add-discrete-to-untimed
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Kenneth Yrke Jørgensen Approve
Lena Said (community) Needs Resubmitting
Review via email: mp+390666@code.launchpad.net

Commit message

Added the discrete engine to untimed, gamed nets

To post a comment you must log in.
Kenneth Yrke Jørgensen (yrke) wrote :

Please check comments for one possible minior issue, just double check that the logic is as intended

review: Needs Fixing
Jiri Srba (srba) wrote :

I create a simple net for untimed and game lens, ask a simple AF query and the verification ends with error in query parsing. When I save the file and open again, the GUI hals and becomes unresponsive.

review: Needs Fixing
1102. By lsaid <email address hidden> on 2020-09-17

Fixed logic

1103. By lsaid <email address hidden> on 2020-09-18

Fixed query issue

1104. By lsaid <email address hidden> on 2020-09-18

clean up

Lena Said (lsaid) wrote :

Fixed some logic that created bugs in the querydialog

review: Needs Resubmitting
Jiri Srba (srba) wrote :

In order to make this work, before the untimed game net is sent to verifydtapn engine
there should be added new isolated place, with one token in it and age invariant <=0.
Then the timed engine will be able to mimick the untimed game semantics.

review: Needs Fixing
1105. By lsaid <email address hidden> on 2020-09-26

Adds an extra place when verifying game/untimed net

1106. By lsaid <email address hidden> on 2020-09-26

Added comment

Lena Said (lsaid) :
review: Needs Resubmitting
1107. By lsaid <email address hidden> on 2020-09-27

Added token to the ghost place

review: Approve
Jiri Srba (srba) :
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/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java 2020-09-16 19:30:40 +0000
+++ src/dk/aau/cs/gui/TabContent.java 2020-09-27 13:29:30 +0000
@@ -680,6 +680,10 @@
680 q.setReductionOption(ReductionOption.VerifyTAPNdiscreteVerification);680 q.setReductionOption(ReductionOption.VerifyTAPNdiscreteVerification);
681 q.setUseOverApproximationEnabled(false);681 q.setUseOverApproximationEnabled(false);
682 q.setUseUnderApproximationEnabled(false);682 q.setUseUnderApproximationEnabled(false);
683 } else if (!tab.lens.isTimed()) {
684 q.setReductionOption(ReductionOption.VerifyPN);
685 q.setUseOverApproximationEnabled(false);
686 q.setUseUnderApproximationEnabled(false);
683 }687 }
684 }688 }
685 String message = "";689 String message = "";
686690
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2020-08-06 13:48:04 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2020-09-27 13:29:30 +0000
@@ -5,10 +5,8 @@
5import dk.aau.cs.TCTL.TCTLAGNode;5import dk.aau.cs.TCTL.TCTLAGNode;
6import dk.aau.cs.TCTL.TCTLEFNode;6import dk.aau.cs.TCTL.TCTLEFNode;
7import dk.aau.cs.TCTL.TCTLEGNode;7import dk.aau.cs.TCTL.TCTLEGNode;
8import dk.aau.cs.model.tapn.LocalTimedPlace;8import dk.aau.cs.gui.TabContent;
9import dk.aau.cs.model.tapn.TAPNQuery;9import dk.aau.cs.model.tapn.*;
10import dk.aau.cs.model.tapn.TimedArcPetriNet;
11import dk.aau.cs.model.tapn.TimedPlace;
12import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;10import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
13import dk.aau.cs.util.ExecutabilityChecker;11import dk.aau.cs.util.ExecutabilityChecker;
14import dk.aau.cs.util.Tuple;12import dk.aau.cs.util.Tuple;
@@ -27,6 +25,7 @@
27import java.io.InputStream;25import java.io.InputStream;
28import java.io.InputStreamReader;26import java.io.InputStreamReader;
29import java.io.StringReader;27import java.io.StringReader;
28import java.math.BigDecimal;
30import java.util.ArrayList;29import java.util.ArrayList;
31import java.util.List;30import java.util.List;
32import java.util.regex.Matcher;31import java.util.regex.Matcher;
@@ -274,6 +273,9 @@
274 //throw new UnsupportedQueryException("Discrete inclusion check only supports upward closed queries.");273 //throw new UnsupportedQueryException("Discrete inclusion check only supports upward closed queries.");
275274
276 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);275 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
276 if (CreateGui.getCurrentTab().getLens().isGame() && !CreateGui.getCurrentTab().getLens().isTimed()) {
277 addGhostPlace(model.value1());
278 }
277279
278 VerifyTAPNExporter exporter = new VerifyTAPNExporter();280 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
279 ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens());281 ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens());
@@ -285,6 +287,13 @@
285 return verify(options, model, exportedModel, query);287 return verify(options, model, exportedModel, query);
286 }288 }
287289
290 //An extra place is added before verifying the query so the timed engine is able to mimic the untimed game semantics.
291 private void addGhostPlace(TimedArcPetriNet net) {
292 TimedPlace place = new LocalTimedPlace("ghost", new TimeInvariant(true, new IntBound(0)));
293 net.add(place);
294 place.addToken(new TimedToken(place, new BigDecimal(0)));
295 }
296
288 private void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {297 private void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
289 VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options;298 VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options;
290299
@@ -308,7 +317,8 @@
308317
309 private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {318 private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {
310 ((VerifyTAPNOptions) options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me319 ((VerifyTAPNOptions) options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
311 runner = new ProcessRunner(verifydtapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));320
321 runner = new ProcessRunner(verifydtapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
312 runner.run();322 runner.run();
313323
314 if (runner.error()) {324 if (runner.error()) {
315325
=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java 2020-09-23 11:37:19 +0000
+++ src/pipe/gui/widgets/QueryDialog.java 2020-09-27 13:29:30 +0000
@@ -371,10 +371,10 @@
371 TAPNQuery.SearchOption searchOption = getSearchOption();371 TAPNQuery.SearchOption searchOption = getSearchOption();
372 ReductionOption reductionOptionToSet = getReductionOption();372 ReductionOption reductionOptionToSet = getReductionOption();
373373
374 if (lens.isTimed()) {374 if (!lens.isGame() && !lens.isTimed()) {
375 return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
376 } else {
375 return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);377 return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
376 } else {
377 return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
378 }378 }
379 }379 }
380380
@@ -690,10 +690,10 @@
690 templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));690 templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));
691 }691 }
692 }692 }
693 if (lens.isTimed()) {693 if (!lens.isGame() && !lens.isTimed()) {
694 updateUntimedQueryButtons(node);
695 } else {
694 updateTimedQueryButtons(node);696 updateTimedQueryButtons(node);
695 } else {
696 updateUntimedQueryButtons(node);
697 }697 }
698 } else if (current instanceof TCTLTransitionNode) {698 } else if (current instanceof TCTLTransitionNode) {
699 TCTLTransitionNode transitionNode = (TCTLTransitionNode) current;699 TCTLTransitionNode transitionNode = (TCTLTransitionNode) current;
@@ -891,6 +891,8 @@
891 }891 }
892 } else if (!lens.isGame()) {892 } else if (!lens.isGame()) {
893 options.add(name_UNTIMED);893 options.add(name_UNTIMED);
894 } else {
895 options.add(name_DISCRETE);
894 }896 }
895897
896 reductionOption.removeAllItems();898 reductionOption.removeAllItems();
@@ -1199,7 +1201,7 @@
1199 queryName.setText(queryToCreateFrom.getName());1201 queryName.setText(queryToCreateFrom.getName());
1200 numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity());1202 numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity());
12011203
1202 if (lens.isTimed()) {1204 if (lens.isTimed() || lens.isGame()) {
1203 setupQuantificationFromQuery(queryToCreateFrom);1205 setupQuantificationFromQuery(queryToCreateFrom);
1204 setupApproximationOptionsFromQuery(queryToCreateFrom);1206 setupApproximationOptionsFromQuery(queryToCreateFrom);
1205 }1207 }
@@ -1252,7 +1254,7 @@
1252 reductionOption.addItem(reduction);1254 reductionOption.addItem(reduction);
1253 reductionOption.setSelectedItem(reduction);1255 reductionOption.setSelectedItem(reduction);
12541256
1255 if (lens.isTimed()) {1257 if (lens.isTimed() || lens.isGame()) {
1256 setupTimedReductionOptions(queryToCreateFrom);1258 setupTimedReductionOptions(queryToCreateFrom);
1257 } else {1259 } else {
1258 setupUntimedReductionOptions(queryToCreateFrom);1260 setupUntimedReductionOptions(queryToCreateFrom);
@@ -1449,7 +1451,7 @@
14491451
1450 searchOptionsPanel.setVisible(advancedView);1452 searchOptionsPanel.setVisible(advancedView);
1451 reductionOptionsPanel.setVisible(advancedView);1453 reductionOptionsPanel.setVisible(advancedView);
1452 if (lens.isTimed()) {1454 if (lens.isTimed() || lens.isGame()) {
1453 saveUppaalXMLButton.setVisible(advancedView);1455 saveUppaalXMLButton.setVisible(advancedView);
1454 overApproximationOptionsPanel.setVisible(advancedView);1456 overApproximationOptionsPanel.setVisible(advancedView);
1455 }1457 }
@@ -1682,7 +1684,7 @@
1682 gbc.fill = GridBagConstraints.VERTICAL;1684 gbc.fill = GridBagConstraints.VERTICAL;
1683 queryPanel.add(quantificationPanel, gbc);1685 queryPanel.add(quantificationPanel, gbc);
16841686
1685 if (lens.isTimed()) {1687 if (lens.isTimed()|| lens.isGame()) {
1686 addTimedQuantificationListeners();1688 addTimedQuantificationListeners();
1687 } else {1689 } else {
1688 addUntimedQuantificationListeners();1690 addUntimedQuantificationListeners();
@@ -1924,7 +1926,7 @@
1924 });1926 });
19251927
1926 negationButton.addActionListener(e -> {1928 negationButton.addActionListener(e -> {
1927 if (lens.isTimed()) {1929 if (lens.isTimed() || lens.isGame()) {
1928 TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));1930 TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));
1929 addPropertyToQuery(property);1931 addPropertyToQuery(property);
1930 } else {1932 } else {
@@ -2045,7 +2047,7 @@
2045 for (SharedPlace place : tapnNetwork.sharedPlaces()) {2047 for (SharedPlace place : tapnNetwork.sharedPlaces()) {
2046 placeNames.add(place.name());2048 placeNames.add(place.name());
2047 }2049 }
2048 if (lens.isTimed()) {2050 if (lens.isTimed() || lens.isGame()) {
2049 for (SharedTransition transition : tapnNetwork.sharedTransitions()) {2051 for (SharedTransition transition : tapnNetwork.sharedTransitions()) {
2050 placeNames.add(transition.name());2052 placeNames.add(transition.name());
2051 }2053 }
@@ -2158,7 +2160,7 @@
2158 String template = templateBox.getSelectedItem().toString();2160 String template = templateBox.getSelectedItem().toString();
2159 if(template.equals(SHARED)) template = "";2161 if(template.equals(SHARED)) template = "";
21602162
2161 if (lens.isTimed() && transitionIsSelected()) {2163 if ((lens.isTimed() || lens.isGame()) && transitionIsSelected()) {
2162 addPropertyToQuery(new TCTLTransitionNode(template, (String) placesBox.getSelectedItem()));2164 addPropertyToQuery(new TCTLTransitionNode(template, (String) placesBox.getSelectedItem()));
2163 } else {2165 } else {
2164 TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(2166 TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(
@@ -2293,7 +2295,7 @@
2293 ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();2295 ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();
2294 for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {2296 for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
2295 for(TimedPlace p : tapn.places()) {2297 for(TimedPlace p : tapn.places()) {
2296 if (lens.isTimed() || !p.isShared()) {2298 if (lens.isTimed() || !p.isShared() || lens.isGame()) {
2297 templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));2299 templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
2298 }2300 }
2299 }2301 }
@@ -2309,7 +2311,7 @@
23092311
2310 boolean isResultFalse;2312 boolean isResultFalse;
23112313
2312 if (lens.isTimed()) {2314 if (lens.isTimed() || lens.isGame()) {
2313 isResultFalse = !c.getResult();2315 isResultFalse = !c.getResult();
2314 } else {2316 } else {
2315 isResultFalse = checkUntimedResult(newQuery) && !c.getResult();2317 isResultFalse = checkUntimedResult(newQuery) && !c.getResult();
@@ -2535,7 +2537,7 @@
2535 gridBagConstraints.anchor = GridBagConstraints.WEST;2537 gridBagConstraints.anchor = GridBagConstraints.WEST;
2536 traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);2538 traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);
25372539
2538 if (lens.isTimed()) {2540 if (lens.isTimed() || lens.isGame()) {
2539 gridBagConstraints.gridy = 2;2541 gridBagConstraints.gridy = 2;
2540 gridBagConstraints.weightx = 1;2542 gridBagConstraints.weightx = 1;
2541 gridBagConstraints.anchor = GridBagConstraints.WEST;2543 gridBagConstraints.anchor = GridBagConstraints.WEST;
@@ -2671,7 +2673,7 @@
2671 usePTrie.setToolTipText(TOOL_TIP_PTRIE);2673 usePTrie.setToolTipText(TOOL_TIP_PTRIE);
2672 useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);2674 useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
26732675
2674 if (lens.isTimed()) {2676 if (lens.isTimed() || lens.isGame()) {
2675 initTimedReductionOptions();2677 initTimedReductionOptions();
2676 } else {2678 } else {
2677 initUntimedReductionOptions();2679 initUntimedReductionOptions();
@@ -2753,7 +2755,7 @@
2753 protected void setEnabledOptionsAccordingToCurrentReduction() {2755 protected void setEnabledOptionsAccordingToCurrentReduction() {
2754 refreshQueryEditingButtons();2756 refreshQueryEditingButtons();
2755 refreshTraceOptions();2757 refreshTraceOptions();
2756 if (lens.isTimed()) {2758 if (lens.isTimed() || lens.isGame()) {
2757 refreshSymmetryReduction();2759 refreshSymmetryReduction();
2758 refreshStubbornReduction();2760 refreshStubbornReduction();
2759 refreshDiscreteOptions();2761 refreshDiscreteOptions();

Subscribers

People subscribed via source and target branches