TAPAAL

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

  1. add-discrete-to-untimed
  2. Merge into trunk
Proposed by Lena Said on 2020-09-14
Status: Merged
Approved by: Jiri Srba on 2020-10-30
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 on 2020-10-30
Kenneth Yrke Jørgensen 2020-09-14 Approve on 2020-10-30
Lena Said (community) Needs Resubmitting on 2020-09-26
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
lp:~tapaal-contributor/tapaal/add-discrete-to-untimed updated on 2020-09-20
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
lp:~tapaal-contributor/tapaal/add-discrete-to-untimed updated on 2020-09-26
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
lp:~tapaal-contributor/tapaal/add-discrete-to-untimed updated on 2020-09-27
1107. By lsaid <email address hidden> on 2020-09-27

Added token to the ghost place

Kenneth Yrke Jørgensen (yrke) :
review: Approve
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/gui/TabContent.java'
2--- src/dk/aau/cs/gui/TabContent.java 2020-09-16 19:30:40 +0000
3+++ src/dk/aau/cs/gui/TabContent.java 2020-09-27 13:29:30 +0000
4@@ -680,6 +680,10 @@
5 q.setReductionOption(ReductionOption.VerifyTAPNdiscreteVerification);
6 q.setUseOverApproximationEnabled(false);
7 q.setUseUnderApproximationEnabled(false);
8+ } else if (!tab.lens.isTimed()) {
9+ q.setReductionOption(ReductionOption.VerifyPN);
10+ q.setUseOverApproximationEnabled(false);
11+ q.setUseUnderApproximationEnabled(false);
12 }
13 }
14 String message = "";
15
16=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java'
17--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2020-08-06 13:48:04 +0000
18+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2020-09-27 13:29:30 +0000
19@@ -5,10 +5,8 @@
20 import dk.aau.cs.TCTL.TCTLAGNode;
21 import dk.aau.cs.TCTL.TCTLEFNode;
22 import dk.aau.cs.TCTL.TCTLEGNode;
23-import dk.aau.cs.model.tapn.LocalTimedPlace;
24-import dk.aau.cs.model.tapn.TAPNQuery;
25-import dk.aau.cs.model.tapn.TimedArcPetriNet;
26-import dk.aau.cs.model.tapn.TimedPlace;
27+import dk.aau.cs.gui.TabContent;
28+import dk.aau.cs.model.tapn.*;
29 import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
30 import dk.aau.cs.util.ExecutabilityChecker;
31 import dk.aau.cs.util.Tuple;
32@@ -27,6 +25,7 @@
33 import java.io.InputStream;
34 import java.io.InputStreamReader;
35 import java.io.StringReader;
36+import java.math.BigDecimal;
37 import java.util.ArrayList;
38 import java.util.List;
39 import java.util.regex.Matcher;
40@@ -274,6 +273,9 @@
41 //throw new UnsupportedQueryException("Discrete inclusion check only supports upward closed queries.");
42
43 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
44+ if (CreateGui.getCurrentTab().getLens().isGame() && !CreateGui.getCurrentTab().getLens().isTimed()) {
45+ addGhostPlace(model.value1());
46+ }
47
48 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
49 ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens());
50@@ -285,6 +287,13 @@
51 return verify(options, model, exportedModel, query);
52 }
53
54+ //An extra place is added before verifying the query so the timed engine is able to mimic the untimed game semantics.
55+ private void addGhostPlace(TimedArcPetriNet net) {
56+ TimedPlace place = new LocalTimedPlace("ghost", new TimeInvariant(true, new IntBound(0)));
57+ net.add(place);
58+ place.addToken(new TimedToken(place, new BigDecimal(0)));
59+ }
60+
61 private void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
62 VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options;
63
64@@ -308,7 +317,8 @@
65
66 private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {
67 ((VerifyTAPNOptions) options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
68- runner = new ProcessRunner(verifydtapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
69+
70+ runner = new ProcessRunner(verifydtapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
71 runner.run();
72
73 if (runner.error()) {
74
75=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
76--- src/pipe/gui/widgets/QueryDialog.java 2020-09-23 11:37:19 +0000
77+++ src/pipe/gui/widgets/QueryDialog.java 2020-09-27 13:29:30 +0000
78@@ -371,10 +371,10 @@
79 TAPNQuery.SearchOption searchOption = getSearchOption();
80 ReductionOption reductionOptionToSet = getReductionOption();
81
82- if (lens.isTimed()) {
83+ if (!lens.isGame() && !lens.isTimed()) {
84+ return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
85+ } else {
86 return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
87- } else {
88- return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
89 }
90 }
91
92@@ -690,10 +690,10 @@
93 templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));
94 }
95 }
96- if (lens.isTimed()) {
97+ if (!lens.isGame() && !lens.isTimed()) {
98+ updateUntimedQueryButtons(node);
99+ } else {
100 updateTimedQueryButtons(node);
101- } else {
102- updateUntimedQueryButtons(node);
103 }
104 } else if (current instanceof TCTLTransitionNode) {
105 TCTLTransitionNode transitionNode = (TCTLTransitionNode) current;
106@@ -891,6 +891,8 @@
107 }
108 } else if (!lens.isGame()) {
109 options.add(name_UNTIMED);
110+ } else {
111+ options.add(name_DISCRETE);
112 }
113
114 reductionOption.removeAllItems();
115@@ -1199,7 +1201,7 @@
116 queryName.setText(queryToCreateFrom.getName());
117 numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity());
118
119- if (lens.isTimed()) {
120+ if (lens.isTimed() || lens.isGame()) {
121 setupQuantificationFromQuery(queryToCreateFrom);
122 setupApproximationOptionsFromQuery(queryToCreateFrom);
123 }
124@@ -1252,7 +1254,7 @@
125 reductionOption.addItem(reduction);
126 reductionOption.setSelectedItem(reduction);
127
128- if (lens.isTimed()) {
129+ if (lens.isTimed() || lens.isGame()) {
130 setupTimedReductionOptions(queryToCreateFrom);
131 } else {
132 setupUntimedReductionOptions(queryToCreateFrom);
133@@ -1449,7 +1451,7 @@
134
135 searchOptionsPanel.setVisible(advancedView);
136 reductionOptionsPanel.setVisible(advancedView);
137- if (lens.isTimed()) {
138+ if (lens.isTimed() || lens.isGame()) {
139 saveUppaalXMLButton.setVisible(advancedView);
140 overApproximationOptionsPanel.setVisible(advancedView);
141 }
142@@ -1682,7 +1684,7 @@
143 gbc.fill = GridBagConstraints.VERTICAL;
144 queryPanel.add(quantificationPanel, gbc);
145
146- if (lens.isTimed()) {
147+ if (lens.isTimed()|| lens.isGame()) {
148 addTimedQuantificationListeners();
149 } else {
150 addUntimedQuantificationListeners();
151@@ -1924,7 +1926,7 @@
152 });
153
154 negationButton.addActionListener(e -> {
155- if (lens.isTimed()) {
156+ if (lens.isTimed() || lens.isGame()) {
157 TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));
158 addPropertyToQuery(property);
159 } else {
160@@ -2045,7 +2047,7 @@
161 for (SharedPlace place : tapnNetwork.sharedPlaces()) {
162 placeNames.add(place.name());
163 }
164- if (lens.isTimed()) {
165+ if (lens.isTimed() || lens.isGame()) {
166 for (SharedTransition transition : tapnNetwork.sharedTransitions()) {
167 placeNames.add(transition.name());
168 }
169@@ -2158,7 +2160,7 @@
170 String template = templateBox.getSelectedItem().toString();
171 if(template.equals(SHARED)) template = "";
172
173- if (lens.isTimed() && transitionIsSelected()) {
174+ if ((lens.isTimed() || lens.isGame()) && transitionIsSelected()) {
175 addPropertyToQuery(new TCTLTransitionNode(template, (String) placesBox.getSelectedItem()));
176 } else {
177 TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(
178@@ -2293,7 +2295,7 @@
179 ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();
180 for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
181 for(TimedPlace p : tapn.places()) {
182- if (lens.isTimed() || !p.isShared()) {
183+ if (lens.isTimed() || !p.isShared() || lens.isGame()) {
184 templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
185 }
186 }
187@@ -2309,7 +2311,7 @@
188
189 boolean isResultFalse;
190
191- if (lens.isTimed()) {
192+ if (lens.isTimed() || lens.isGame()) {
193 isResultFalse = !c.getResult();
194 } else {
195 isResultFalse = checkUntimedResult(newQuery) && !c.getResult();
196@@ -2535,7 +2537,7 @@
197 gridBagConstraints.anchor = GridBagConstraints.WEST;
198 traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);
199
200- if (lens.isTimed()) {
201+ if (lens.isTimed() || lens.isGame()) {
202 gridBagConstraints.gridy = 2;
203 gridBagConstraints.weightx = 1;
204 gridBagConstraints.anchor = GridBagConstraints.WEST;
205@@ -2671,7 +2673,7 @@
206 usePTrie.setToolTipText(TOOL_TIP_PTRIE);
207 useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
208
209- if (lens.isTimed()) {
210+ if (lens.isTimed() || lens.isGame()) {
211 initTimedReductionOptions();
212 } else {
213 initUntimedReductionOptions();
214@@ -2753,7 +2755,7 @@
215 protected void setEnabledOptionsAccordingToCurrentReduction() {
216 refreshQueryEditingButtons();
217 refreshTraceOptions();
218- if (lens.isTimed()) {
219+ if (lens.isTimed() || lens.isGame()) {
220 refreshSymmetryReduction();
221 refreshStubbornReduction();
222 refreshDiscreteOptions();

Subscribers

People subscribed via source and target branches