TAPAAL

Merge lp:~tapaal-contributor/tapaal/redirect-game-engine-cpn into lp:~tapaal-contributor/tapaal/cpn-gui-dev

  1. redirect-game-engine-cpn
  2. 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
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
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 }
6
7 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
8- if (TAPAALGUI.getCurrentTab().getLens().isGame() && !TAPAALGUI.getCurrentTab().getLens().isTimed() && !TAPAALGUI.getCurrentTab().getLens().isColored()) {
9- addGhostPlace(model.value1());
10- }
11
12 VerifyTAPNExporter exporter = new VerifyTACPNExporter();
13
14
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 }
20
21 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
22- if (TAPAALGUI.getCurrentTab().getLens().isGame() && !TAPAALGUI.getCurrentTab().getLens().isTimed()) {
23- addGhostPlace(model.value1());
24- }
25
26 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
27
28@@ -233,13 +230,6 @@
29 return verify(options, model, exportedModel, query, dataLayerQuery);
30 }
31
32- //An extra place is added before verifying the query so the timed engine is able to mimic the untimed game semantics.
33- protected void addGhostPlace(TimedArcPetriNet net) {
34- TimedPlace place = new LocalTimedPlace("ghost", new TimeInvariant(true, new IntBound(0)), ColorType.COLORTYPE_DOT);
35- net.add(place);
36- place.addToken(new TimedToken(place, new BigDecimal(0), ColorType.COLORTYPE_DOT.getFirstColor()));
37- }
38-
39 protected void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
40 VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options;
41
42
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
48 protected void outputPlace(TimedPlace p, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) {
49 //remove the net prefix from the place name
50- String placeName;
51+ String placeName = mapping.map(p.name()).value2();
52 Place guiPlace = null;
53
54- if (mapping.map(p.name()) == null) {
55- placeName = "ghost";
56- } else {
57- placeName = mapping.map(p.name()).value2();
58- }
59 for (DataLayer guiModel : guiModels ) {
60 guiPlace = guiModel.getPlaceById(placeName);
61 if (guiPlace != null) {
62
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 TAPAALGUI.getApp().setVisible(false);
68
69 System.out.println("=============================================================");
70- System.out.println("Batch Porcessing");
71+ System.out.println("Batch Processing");
72 System.out.println("=============================================================");
73
74 System.out.println("Running in batch mode for " + batchFolder.getAbsolutePath());
75
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 private JRadioButton randomSearch;
81 private JRadioButton heuristicSearch;
82
83-
84-
85-
86 // Trace options panel
87 private JPanel traceOptionsPanel;
88
89@@ -170,8 +167,6 @@
90 private JRadioButton someTraceRadioButton;
91 private JRadioButton fastestTraceRadioButton;
92
93-
94-
95 // Unfolding options panel
96 private JPanel verificationPanel;
97 private JPanel unfoldingOptionsPanel;
98@@ -416,7 +411,7 @@
99 TAPNQuery.SearchOption searchOption = getSearchOption();
100 ReductionOption reductionOptionToSet = getReductionOption();
101
102- if (!lens.isGame() && !lens.isTimed()) {
103+ if (!lens.isTimed()) {
104 return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
105 } else {
106 return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
107@@ -749,7 +744,7 @@
108 templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));
109 }
110 }
111- if (!lens.isGame() && !lens.isTimed()) {
112+ if (!lens.isTimed()) {
113 updateUntimedQueryButtons(node);
114 } else {
115 updateTimedQueryButtons(node);
116@@ -765,7 +760,7 @@
117 placeTransitionBox.setSelectedItem(transitionNode.getTransition());
118 userChangedAtomicPropSelection = true;
119 }
120- if (!lens.isTimed() && !lens.isGame()) {
121+ if (!lens.isTimed()) {
122 setEnablednessOfOperatorAndMarkingBoxes();
123 }
124 if (current instanceof LTLANode || current instanceof LTLENode ||
125@@ -956,10 +951,8 @@
126 options.add(engine.nameString);
127 }
128 }
129- } else if (!lens.isGame()) {
130+ } else {
131 options.add(name_UNTIMED);
132- } else {
133- options.add(name_DISCRETE);
134 }
135
136 reductionOption.removeAllItems();
137@@ -1307,13 +1300,20 @@
138
139 setEnabledOptionsAccordingToCurrentReduction();
140 makeShortcuts();
141+
142+ if (lens.isGame() && !lens.isTimed()) {
143+ useReduction.setSelected(false);
144+ useReduction.setEnabled(false);
145+ useSiphonTrap.setSelected(false);
146+ useSiphonTrap.setEnabled(false);
147+ }
148 }
149
150 private void setupFromQuery(TAPNQuery queryToCreateFrom) {
151 queryName.setText(queryToCreateFrom.getName());
152 numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity());
153
154- if (lens.isTimed() || lens.isGame()) {
155+ if (lens.isTimed()) {
156 setupQuantificationFromQuery(queryToCreateFrom);
157 setupApproximationOptionsFromQuery(queryToCreateFrom);
158 }
159@@ -1382,7 +1382,7 @@
160 reductionOption.addItem(reduction);
161 reductionOption.setSelectedItem(reduction);
162
163- if (lens.isTimed() || lens.isGame()) {
164+ if (lens.isTimed()) {
165 setupTimedReductionOptions(queryToCreateFrom);
166 } else {
167 setupUntimedReductionOptions(queryToCreateFrom);
168@@ -1458,7 +1458,7 @@
169 }
170
171 private void setupQueryCategoryFromQuery(TAPNQuery queryToCreateFrom) {
172- if (!lens.isTimed() && !lens.isGame()) {
173+ if (!lens.isTimed()) {
174 TAPNQuery.QueryCategory category = queryToCreateFrom.getCategory();
175 if (category.equals(TAPNQuery.QueryCategory.CTL)) {
176 queryType.setSelectedIndex(0);
177@@ -1605,7 +1605,7 @@
178 }
179
180 reductionOptionsPanel.setVisible(advancedView);
181- if (lens.isTimed() || lens.isGame()) {
182+ if (lens.isTimed()) {
183 saveUppaalXMLButton.setVisible(advancedView);
184 // Disabled approximation options for colored models, because they are not supported yet (will generate error)
185 overApproximationOptionsPanel.setVisible(advancedView && !lens.isColored());
186@@ -2515,7 +2515,7 @@
187 });
188
189 negationButton.addActionListener(e -> {
190- if (lens.isTimed() || lens.isGame()) {
191+ if (lens.isTimed()) {
192 TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));
193 addPropertyToQuery(property);
194 } else {
195@@ -2619,7 +2619,7 @@
196 placeNames.add(place.name());
197 }
198 }
199- if (!lens.isTimed() && !lens.isGame()) {
200+ if (!lens.isTimed()) {
201 for (TimedTransition transition : tapn.transitions()) {
202 if (!transition.isShared()) {
203 placeNames.add(transition.name());
204@@ -2641,7 +2641,7 @@
205 for (SharedPlace place : tapnNetwork.sharedPlaces()) {
206 placeNames.add(place.name());
207 }
208- if (lens.isTimed() || lens.isGame()) {
209+ if (lens.isTimed()) {
210 for (SharedTransition transition : tapnNetwork.sharedTransitions()) {
211 placeNames.add(transition.name());
212 }
213@@ -2655,7 +2655,7 @@
214 updateQueryOnAtomicPropositionChange();
215 }
216 }
217- if (!lens.isTimed() && !lens.isGame()) setEnablednessOfOperatorAndMarkingBoxes();
218+ if (!lens.isTimed()) setEnablednessOfOperatorAndMarkingBoxes();
219
220 }
221 });
222@@ -2692,7 +2692,7 @@
223
224 transitionIsEnabledLabel = new JLabel(" is enabled");
225 transitionIsEnabledLabel.setPreferredSize(new Dimension(165, 27));
226- if (!lens.isTimed() && !lens.isGame()) placeRow.add(transitionIsEnabledLabel);
227+ if (!lens.isTimed()) placeRow.add(transitionIsEnabledLabel);
228
229 JPanel addPredicateRow = new JPanel(new FlowLayout(FlowLayout.CENTER));
230 gbc.gridy = 2;
231@@ -2754,7 +2754,7 @@
232 String template = templateBox.getSelectedItem().toString();
233 if(template.equals(SHARED)) template = "";
234
235- if ((!lens.isTimed() && !lens.isGame()) && transitionIsSelected()) {
236+ if ((!lens.isTimed()) && transitionIsSelected()) {
237 addPropertyToQuery(new TCTLTransitionNode(template, (String) placeTransitionBox.getSelectedItem()));
238 } else {
239 TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(
240@@ -2791,7 +2791,7 @@
241 if (userChangedAtomicPropSelection) {
242 updateQueryOnAtomicPropositionChange();
243 }
244- if (!lens.isTimed() && !lens.isGame()) {
245+ if (!lens.isTimed()) {
246 setEnablednessOfOperatorAndMarkingBoxes();
247 }
248 });
249@@ -2913,7 +2913,7 @@
250
251 boolean isResultFalse;
252
253- if (lens.isTimed() || lens.isGame()) {
254+ if (lens.isTimed()) {
255 isResultFalse = !placeContext.getResult();
256 } else {
257 isResultFalse = !transitionContext.getResult() || !placeContext.getResult();
258@@ -3027,7 +3027,7 @@
259 ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();
260 for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
261 for(TimedPlace p : tapn.places()) {
262- if (lens.isTimed() || !p.isShared() || lens.isGame()) {
263+ if (lens.isTimed() || !p.isShared()) {
264 templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
265 }
266 }
267@@ -3047,7 +3047,7 @@
268 ArrayList<Tuple<String,String>> templateTransitionNames = new ArrayList<Tuple<String,String>>();
269 for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
270 for (TimedTransition t : tapn.transitions()) {
271- if (lens.isTimed() || !t.isShared() || lens.isGame()) {
272+ if (lens.isTimed() || !t.isShared()) {
273 templateTransitionNames.add(new Tuple<>(tapn.name(), t.name()));
274 }
275 }
276@@ -3229,7 +3229,7 @@
277 gridBagConstraints.anchor = GridBagConstraints.WEST;
278 traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);
279
280- if (lens.isTimed() || lens.isGame()) {
281+ if (lens.isTimed()) {
282 gridBagConstraints.gridy = 2;
283 gridBagConstraints.weightx = 1;
284 gridBagConstraints.anchor = GridBagConstraints.WEST;
285@@ -3372,7 +3372,7 @@
286
287 useTarjan.addActionListener(e -> updateSearchStrategies());
288
289- if (lens.isTimed() || lens.isGame()) {
290+ if (lens.isTimed()) {
291 initTimedReductionOptions();
292 } else {
293 useReduction.addActionListener(new ActionListener() {
294@@ -3467,7 +3467,7 @@
295 protected void setEnabledOptionsAccordingToCurrentReduction() {
296 refreshQueryEditingButtons();
297 refreshTraceOptions();
298- if (lens.isTimed() || lens.isGame()) {
299+ if (lens.isTimed()) {
300 refreshSymmetryReduction();
301 refreshStubbornReduction();
302 refreshDiscreteOptions();

Subscribers

People subscribed via source and target branches

to all changes: