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: Superseded
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 Needs Fixing
Review via email: mp+414017@code.launchpad.net

This proposal has been superseded by a proposal from 2022-01-14.

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 :

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
lp:~tapaal-contributor/tapaal/redirect-game-engine-cpn updated
1552. By Lena Ernstsen

Changed visibility of some query options for game nets

1553. By Lena Ernstsen

Corrected minor spelling mistake

1554. By Lena Ernstsen

Disabled some options for untimed game net queries

Unmerged revisions

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:07 +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:07 +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:07 +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:07 +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:07 +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: