TAPAAL

Merge lp:~tapaal-contributor/tapaal/cpn-trace into lp:~tapaal-contributor/tapaal/cpn-gui-dev

  1. cpn-trace
  2. Merge into cpn-gui-dev
Proposed by Kenneth Yrke Jørgensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1570
Merged at revision: 1566
Proposed branch: lp:~tapaal-contributor/tapaal/cpn-trace
Merge into: lp:~tapaal-contributor/tapaal/cpn-gui-dev
Diff against target: 601 lines (+74/-108)
14 files modified
src/dk/aau/cs/approximation/ApproximationWorker.java (+13/-9)
src/dk/aau/cs/verification/ModelChecker.java (+2/-1)
src/dk/aau/cs/verification/UPPAAL/Verifyta.java (+2/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java (+0/-45)
src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java (+14/-9)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+6/-6)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java (+2/-1)
src/net/tapaal/TAPAAL.java (+1/-1)
src/net/tapaal/gui/petrinet/TabTransformer.java (+2/-2)
src/net/tapaal/gui/petrinet/dialog/QueryDialog.java (+3/-4)
src/net/tapaal/gui/petrinet/verification/RunVerificationBase.java (+13/-8)
src/net/tapaal/gui/petrinet/verification/Verifier.java (+14/-19)
src/net/tapaal/gui/petrinet/widgets/QueryPane.java (+1/-1)
src/resources/Example nets/intro-example.tapn (+1/-1)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/cpn-trace
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+414726@code.launchpad.net
To post a comment you must log in.
lp:~tapaal-contributor/tapaal/cpn-trace updated
1570. By Kenneth Yrke Jørgensen

Fixed issue when running query from QueryList insted of dialog

When running intro example, or intro example converted to colored, we got an error when using the QueryPane.
Running from the query dialog worked

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

Tested and fixes the issues nicely.

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/approximation/ApproximationWorker.java'
2--- src/dk/aau/cs/approximation/ApproximationWorker.java 2022-01-07 17:05:54 +0000
3+++ src/dk/aau/cs/approximation/ApproximationWorker.java 2022-01-28 13:31:23 +0000
4@@ -1,6 +1,8 @@
5 package dk.aau.cs.approximation;
6
7 import java.math.BigDecimal;
8+
9+import pipe.gui.petrinet.PetriNetTab;
10 import pipe.gui.petrinet.dataLayer.DataLayer;
11 import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
12 import pipe.gui.TAPAALGUI;
13@@ -41,7 +43,8 @@
14 RunVerificationBase verificationBase,
15 TimedArcPetriNetNetwork model,
16 DataLayer guiModel,
17- net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery
18+ net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery,
19+ PetriNetTab.TAPNLens lens
20 ) throws Exception {
21
22 // If options is of an instance of VerifyTAPNOptions then save the inclusion places before verify alters them
23@@ -58,7 +61,7 @@
24 VerificationResult<TAPNNetworkTrace> toReturn = null;
25 VerificationResult<TimedArcPetriNetTrace> result;
26
27- result = modelChecker.verify(options, transformedModel, clonedQuery, guiModel, dataLayerQuery);
28+ result = modelChecker.verify(options, transformedModel, clonedQuery, guiModel, dataLayerQuery, lens);
29
30 if (result.error()) {
31 options.setTraceOption(oldTraceOption);
32@@ -118,7 +121,7 @@
33
34 // run model checker again for trace TAPN
35 MemoryMonitor.cumulateMemory();
36- result = modelChecker.verify(options, transformedOriginalModel, clonedQuery, guiModel, dataLayerQuery);
37+ result = modelChecker.verify(options, transformedOriginalModel, clonedQuery, guiModel, dataLayerQuery, null);
38
39 if (result.error()) {
40 options.setTraceOption(oldTraceOption);
41@@ -287,7 +290,7 @@
42
43 //run model checker again for trace TAPN
44 MemoryMonitor.cumulateMemory();
45- result = modelChecker.verify(options, transformedOriginalModel, clonedQuery, guiModel, dataLayerQuery);
46+ result = modelChecker.verify(options, transformedOriginalModel, clonedQuery, guiModel, dataLayerQuery, null);
47
48 if (result.error()) {
49 options.setTraceOption(oldTraceOption);
50@@ -347,8 +350,9 @@
51 }
52 }
53 else {
54- NameMapping nameMapping = model.isColored()? result.getUnfoldedModel().value2(): transformedModel.value2();
55- TimedArcPetriNetNetwork netNetwork = model.isColored()? result.getUnfoldedModel().value1().parentNetwork(): model;
56+ boolean isColored = (lens != null && lens.isColored() || model.isColored());
57+ NameMapping nameMapping = isColored? result.getUnfoldedModel().value2(): transformedModel.value2();
58+ TimedArcPetriNetNetwork netNetwork = isColored? result.getUnfoldedModel().value1().parentNetwork(): model;
59 toReturn = new VerificationResult<TAPNNetworkTrace>(
60 result.getQueryResult(),
61 decomposeTrace(result.getTrace(), nameMapping, netNetwork),
62@@ -402,7 +406,7 @@
63 options.setTraceOption(TraceOption.SOME);
64 }
65
66- VerificationResult<TimedArcPetriNetTrace> verificationResult = modelChecker.verify(options, composedModel, queryToVerify, TAPAALGUI.getModel(), query);
67+ VerificationResult<TimedArcPetriNetTrace> verificationResult = modelChecker.verify(options, composedModel, queryToVerify, TAPAALGUI.getModel(), query, null);
68
69 VerificationResult<TAPNNetworkTrace> valueNetwork = null; //The final result is meant to be a PetriNetTrace but to make traceTAPN we make a networktrace
70 VerificationResult<TimedArcPetriNetTrace> value = null;
71@@ -458,7 +462,7 @@
72
73 //run model checker again for trace TAPN
74 MemoryMonitor.cumulateMemory();
75- verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery, TAPAALGUI.getModel(), query);
76+ verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery, TAPAALGUI.getModel(), query, null);
77
78 if (verificationResult.error()) {
79 options.setTraceOption(oldTraceOption);
80@@ -597,7 +601,7 @@
81
82 //run model checker again for trace TAPN
83 MemoryMonitor.cumulateMemory();
84- verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery, TAPAALGUI.getModel(), query);
85+ verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery, TAPAALGUI.getModel(), query, null);
86
87 if (verificationResult.error()) {
88 options.setTraceOption(oldTraceOption);
89
90=== modified file 'src/dk/aau/cs/verification/ModelChecker.java'
91--- src/dk/aau/cs/verification/ModelChecker.java 2022-01-07 17:05:54 +0000
92+++ src/dk/aau/cs/verification/ModelChecker.java 2022-01-28 13:31:23 +0000
93@@ -4,6 +4,7 @@
94 import dk.aau.cs.model.tapn.TimedArcPetriNet;
95 import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
96 import dk.aau.cs.util.Tuple;
97+import pipe.gui.petrinet.PetriNetTab;
98 import pipe.gui.petrinet.dataLayer.DataLayer;
99
100 // TODO: MJ -- This interface is getting somewhat bloated -- Try to fix it
101@@ -18,7 +19,7 @@
102
103 String getPath(); // TODO: MJ -- Delete me when refactoring is done
104
105- VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) throws Exception;
106+ VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery, PetriNetTab.TAPNLens lens) throws Exception;
107
108
109 void kill();
110
111=== modified file 'src/dk/aau/cs/verification/UPPAAL/Verifyta.java'
112--- src/dk/aau/cs/verification/UPPAAL/Verifyta.java 2022-01-09 18:09:13 +0000
113+++ src/dk/aau/cs/verification/UPPAAL/Verifyta.java 2022-01-28 13:31:23 +0000
114@@ -7,6 +7,7 @@
115
116 import dk.aau.cs.verification.*;
117 import net.tapaal.Preferences;
118+import pipe.gui.petrinet.PetriNetTab;
119 import pipe.gui.petrinet.dataLayer.DataLayer;
120 import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
121 import pipe.gui.FileFinder;
122@@ -251,7 +252,7 @@
123 return true;
124 }
125
126- public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) throws Exception {
127+ public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery, PetriNetTab.TAPNLens lens) throws Exception {
128
129 if(!model.value1().isDegree2() && new HasDeadlockVisitor().hasDeadLock(query.getProperty()))
130 throw new UnsupportedModelException("\nBecause the query contains a deadlock proposition, the selected engine\nsupports only nets where transitions have at most two input places.");
131
132=== removed file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java'
133--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java 2022-01-12 06:44:58 +0000
134+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java 1970-01-01 00:00:00 +0000
135@@ -1,45 +0,0 @@
136-package dk.aau.cs.verification.VerifyTAPN;
137-
138-import dk.aau.cs.Messenger;
139-import dk.aau.cs.model.tapn.TAPNQuery;
140-import dk.aau.cs.model.tapn.TimedArcPetriNet;
141-import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
142-import dk.aau.cs.util.Tuple;
143-import dk.aau.cs.util.UnsupportedModelException;
144-import dk.aau.cs.util.UnsupportedQueryException;
145-import dk.aau.cs.verification.NameMapping;
146-import dk.aau.cs.verification.VerificationOptions;
147-import dk.aau.cs.verification.VerificationResult;
148-import pipe.gui.petrinet.dataLayer.DataLayer;
149-import pipe.gui.TAPAALGUI;
150-import pipe.gui.FileFinder;
151-
152-public class VerifyDTACPN extends VerifyDTAPN {
153-
154- public VerifyDTACPN(FileFinder fileFinder, Messenger messenger) {
155- super(fileFinder, messenger);
156- }
157-
158- @Override
159- public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) throws Exception {
160- if (!supportsModel(model.value1(), options)) {
161- throw new UnsupportedModelException("Verifydtapn does not support the given model.");
162- }
163-
164- if (!supportsQuery(model.value1(), query, options)) {
165- throw new UnsupportedQueryException("Verifydtapn does not support the given query-option combination. ");
166- }
167-
168- if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
169-
170- VerifyTAPNExporter exporter = new VerifyTACPNExporter();
171-
172- ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, TAPAALGUI.getCurrentTab().getLens(),model.value2(), guiModel, dataLayerQuery);
173-
174- if (exportedModel == null) {
175- messenger.displayErrorMessage("There was an error exporting the model");
176- }
177-
178- return verify(options, model, exportedModel, query, dataLayerQuery);
179- }
180-}
181
182=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java'
183--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java 2022-01-12 06:44:58 +0000
184+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java 2022-01-28 13:31:23 +0000
185@@ -8,7 +8,6 @@
186 import pipe.gui.petrinet.PetriNetTab;
187 import dk.aau.cs.io.LoadedModel;
188 import dk.aau.cs.io.TapnEngineXmlLoader;
189-import dk.aau.cs.model.CPN.ColorType;
190 import dk.aau.cs.model.tapn.*;
191 import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
192 import dk.aau.cs.util.*;
193@@ -18,7 +17,6 @@
194 import java.io.File;
195 import java.io.IOException;
196 import java.io.StringReader;
197-import java.math.BigDecimal;
198 import java.util.ArrayList;
199 import java.util.List;
200
201@@ -208,7 +206,7 @@
202
203 }
204
205- public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) throws Exception {
206+ public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery, PetriNetTab.TAPNLens lens) throws Exception {
207 if (!supportsModel(model.value1(), options)) {
208 throw new UnsupportedModelException("Verifydtapn does not support the given model.");
209 }
210@@ -219,15 +217,20 @@
211
212 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
213
214- VerifyTAPNExporter exporter = new VerifyTAPNExporter();
215-
216- ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, TAPAALGUI.getCurrentTab().getLens(),model.value2(), guiModel, dataLayerQuery);
217+ ExportedVerifyTAPNModel exportedModel;
218+ if ((lens != null && lens.isColored() || model.value1().parentNetwork().isColored())) {
219+ VerifyTAPNExporter exporter = new VerifyTACPNExporter();
220+ exportedModel = exporter.export(model.value1(), query, TAPAALGUI.getCurrentTab().getLens(),model.value2(), guiModel, dataLayerQuery);
221+ } else {
222+ VerifyTAPNExporter exporter = new VerifyTAPNExporter();
223+ exportedModel = exporter.export(model.value1(), query, TAPAALGUI.getCurrentTab().getLens(),model.value2(), guiModel, dataLayerQuery);
224+ }
225
226 if (exportedModel == null) {
227 messenger.displayErrorMessage("There was an error exporting the model");
228 }
229
230- return verify(options, model, exportedModel, query, dataLayerQuery);
231+ return verify(options, model, exportedModel, query, dataLayerQuery, lens);
232 }
233
234 protected void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
235@@ -251,7 +254,7 @@
236 ((VerifyTAPNOptions) options).setInclusionPlaces(new InclusionPlaces(InclusionPlacesOption.UserSpecified, inclusionPlaces));
237 }
238
239- protected VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) {
240+ protected VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery, PetriNetTab.TAPNLens lens) {
241 ((VerifyTAPNOptions) options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
242
243 runner = new ProcessRunner(verifydtapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
244@@ -271,7 +274,9 @@
245
246 TimedArcPetriNetTrace tapnTrace = null;
247
248- if(options.traceOption() != TraceOption.NONE && model.value1().isColored() && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) {
249+
250+ boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored());
251+ if(options.traceOption() != TraceOption.NONE && isColored && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) {
252 TapnEngineXmlLoader tapnLoader = new TapnEngineXmlLoader();
253 File fileOut = new File(options.unfoldedModelPath());
254 File queriesOut = new File(options.unfoldedQueriesPath());
255
256=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
257--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2022-01-23 11:10:27 +0000
258+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2022-01-28 13:31:23 +0000
259@@ -223,7 +223,7 @@
260 return false;
261 }
262
263- public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) throws Exception {
264+ public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery, PetriNetTab.TAPNLens lens) throws Exception {
265 if (!supportsModel(model.value1(), options)) {
266 throw new UnsupportedModelException("Verifypn does not support the given model.");
267 }
268@@ -235,7 +235,7 @@
269 if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
270
271 VerifyTAPNExporter exporter;
272- if (model.value1().parentNetwork().isColored()) {
273+ if ((lens != null && lens.isColored() || model.value1().parentNetwork().isColored())) {
274 exporter = new VerifyCPNExporter();
275 } else {
276 exporter = new VerifyPNExporter();
277@@ -246,7 +246,7 @@
278 messenger.displayErrorMessage("There was an error exporting the model");
279 }
280
281- return verify(options, model, exportedModel, query, dataLayerQuery);
282+ return verify(options, model, exportedModel, query, dataLayerQuery, lens);
283 }
284
285 private void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
286@@ -272,7 +272,7 @@
287 ((VerifyTAPNOptions) options).setInclusionPlaces(new InclusionPlaces(InclusionPlacesOption.UserSpecified, inclusionPlaces));
288 }
289
290- private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) throws IOException {
291+ private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery, PetriNetTab.TAPNLens lens) throws IOException {
292 ((VerifyTAPNOptions) options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
293
294 runner = new ProcessRunner(verifypnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
295@@ -287,7 +287,8 @@
296
297 Tuple<QueryResult, Stats> queryResult = parseQueryResult(standardOutput, model.value1().marking().size() + query.getExtraTokens(), query.getExtraTokens(), query);
298
299- if (options.traceOption() != TraceOption.NONE && model.value1().isColored() && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) {
300+ boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored());
301+ if (options.traceOption() != TraceOption.NONE && isColored && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) {
302 PNMLoader tapnLoader = new PNMLoader();
303 File fileOut = new File(options.unfoldedModelPath());
304 File queriesOut = new File(options.unfoldedQueriesPath());
305@@ -298,7 +299,6 @@
306 TAPNComposer newComposer = new TAPNComposer(new MessengerImpl(), true);
307 model = newComposer.transformModel(loadedModel.network());
308
309-
310 if (queryResult != null && queryResult.value1() != null) {
311 tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1(), true);
312 }
313
314=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java'
315--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2022-01-09 18:33:52 +0000
316+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2022-01-28 13:31:23 +0000
317@@ -10,6 +10,7 @@
318 import dk.aau.cs.verification.*;
319 import net.tapaal.Preferences;
320 import net.tapaal.TAPAAL;
321+import pipe.gui.petrinet.PetriNetTab;
322 import pipe.gui.petrinet.dataLayer.DataLayer;
323 import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
324 import pipe.gui.FileFinder;
325@@ -206,7 +207,7 @@
326
327 }
328
329- public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) throws Exception {
330+ public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query, DataLayer guiModel, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery, PetriNetTab.TAPNLens lens) throws Exception {
331 if(!supportsModel(model.value1(), options)) {
332 throw new UnsupportedModelException("Verifytapn does not support the given model.");
333 }
334
335=== modified file 'src/net/tapaal/TAPAAL.java'
336--- src/net/tapaal/TAPAAL.java 2022-01-24 10:42:42 +0000
337+++ src/net/tapaal/TAPAAL.java 2022-01-28 13:31:23 +0000
338@@ -154,7 +154,7 @@
339 ));
340 }
341
342- }, tab.getGuiModels(),false);
343+ }, tab.getGuiModels(),false, null);
344 } else {
345 System.out.println(" | Skipped");
346 //Verifier.runUppaalVerification(network, query);
347
348=== modified file 'src/net/tapaal/gui/petrinet/TabTransformer.java'
349--- src/net/tapaal/gui/petrinet/TabTransformer.java 2022-01-24 09:16:26 +0000
350+++ src/net/tapaal/gui/petrinet/TabTransformer.java 2022-01-28 13:31:23 +0000
351@@ -2,6 +2,7 @@
352
353 import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor;
354 import dk.aau.cs.TCTL.visitors.RenameAllTransitionsVisitor;
355+import dk.aau.cs.verification.VerifyTAPN.VerifyDTAPN;
356 import net.tapaal.gui.petrinet.smartdraw.SmartDrawDialog;
357 import dk.aau.cs.model.CPN.ColorType;
358 import dk.aau.cs.model.CPN.ColoredTimeInterval;
359@@ -10,7 +11,6 @@
360 import dk.aau.cs.model.tapn.*;
361 import dk.aau.cs.verification.*;
362 import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
363-import dk.aau.cs.verification.VerifyTAPN.VerifyDTACPN;
364 import net.tapaal.gui.petrinet.verification.TAPNQuery;
365 import pipe.gui.petrinet.dataLayer.DataLayer;
366 import pipe.gui.*;
367@@ -297,7 +297,7 @@
368
369 ModelChecker engine;
370 if(oldTab.getLens().isTimed()){
371- engine = new VerifyDTACPN(new FileFinder(), new MessengerImpl());
372+ engine = new VerifyDTAPN(new FileFinder(), new MessengerImpl());
373 } else {
374 engine = new VerifyPN(new FileFinder(), new MessengerImpl());
375 }
376
377=== modified file 'src/net/tapaal/gui/petrinet/dialog/QueryDialog.java'
378--- src/net/tapaal/gui/petrinet/dialog/QueryDialog.java 2022-01-24 10:42:42 +0000
379+++ src/net/tapaal/gui/petrinet/dialog/QueryDialog.java 2022-01-28 13:31:23 +0000
380@@ -3751,9 +3751,8 @@
381 TAPNQuery query = getQuery();
382
383 if (query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyDTAPN || query.getReductionOption() == ReductionOption.VerifyPN) {
384- Verifier.runVerifyTAPNVerification(tapnNetwork, query, null, guiModels,false);
385- }
386- else{
387+ Verifier.runVerifyTAPNVerification(tapnNetwork, query, null, guiModels,false, lens);
388+ } else{
389 Verifier.runUppaalVerification(tapnNetwork, query);
390 }
391 }}
392@@ -3899,7 +3898,7 @@
393
394 exit();
395
396- Verifier.runVerifyTAPNVerification(tapnNetwork, query,null, guiModels, true);
397+ Verifier.runVerifyTAPNVerification(tapnNetwork, query,null, guiModels, true, null);
398
399 File reducedNetFile = new File(Verifier.getReducedNetFilePath());
400
401
402=== modified file 'src/net/tapaal/gui/petrinet/verification/RunVerificationBase.java'
403--- src/net/tapaal/gui/petrinet/verification/RunVerificationBase.java 2022-01-23 12:36:41 +0000
404+++ src/net/tapaal/gui/petrinet/verification/RunVerificationBase.java 2022-01-28 13:31:23 +0000
405@@ -62,13 +62,18 @@
406 this.spinner = spinner;
407 }
408
409- public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) {
410+ public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery, PetriNetTab.TAPNLens lens) {
411 this.model = model;
412 this.options = options;
413 this.query = query;
414 this.dataLayerQuery = dataLayerQuery;
415+ this.lens = lens;
416 execute();
417 }
418+ public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery) {
419+ execute(options, model, query, dataLayerQuery, null);
420+ }
421+
422
423 @Override
424 protected VerificationResult<TAPNNetworkTrace> doInBackground() throws Exception {
425@@ -107,7 +112,7 @@
426 overapprox_result = verifypn.verify(
427 new VerifyPNOptions(
428 options.extraTokens(),
429- options.traceOption(),
430+ net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption.NONE,
431 SearchOption.OVERAPPROXIMATE,
432 true,
433 ModelReduction.AGGRESSIVE,
434@@ -131,13 +136,13 @@
435 transformedModel,
436 clonedQuery,
437 composer.getGuiModel(),
438- dataLayerQuery
439- );
440+ dataLayerQuery,
441+ null);
442 } else { // TODO: FIX! If datalayer is null then we can't check datalayer's values...
443 overapprox_result = verifypn.verify(
444 new VerifyPNOptions(
445 options.extraTokens(),
446- options.traceOption(),
447+ net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption.NONE,
448 SearchOption.OVERAPPROXIMATE,
449 true,
450 ModelReduction.AGGRESSIVE,
451@@ -161,8 +166,8 @@
452 transformedModel,
453 clonedQuery,
454 composer.getGuiModel(),
455- dataLayerQuery
456- );
457+ dataLayerQuery,
458+ null);
459 }
460
461 if (overapprox_result.getQueryResult() != null) {
462@@ -186,7 +191,7 @@
463 }
464 ApproximationWorker worker = new ApproximationWorker();
465
466- return worker.normalWorker(options, modelChecker, transformedModel, composer, clonedQuery, this, model, guiModel, dataLayerQuery);
467+ return worker.normalWorker(options, modelChecker, transformedModel, composer, clonedQuery, this, model, guiModel, dataLayerQuery, lens);
468 }
469
470 private TAPNNetworkTrace decomposeTrace(TimedArcPetriNetTrace trace, NameMapping mapping) {
471
472=== modified file 'src/net/tapaal/gui/petrinet/verification/Verifier.java'
473--- src/net/tapaal/gui/petrinet/verification/Verifier.java 2022-01-24 10:42:42 +0000
474+++ src/net/tapaal/gui/petrinet/verification/Verifier.java 2022-01-28 13:31:23 +0000
475@@ -52,23 +52,17 @@
476 return verifydtapn;
477 }
478
479- private static VerifyDTAPN getVerifydTACPN() {
480- VerifyDTAPN verifydtacpn = new VerifyDTACPN(new FileFinder(), new MessengerImpl());
481- verifydtacpn.setup();
482- return verifydtacpn;
483- }
484-
485 private static VerifyPN getVerifyPN() {
486 VerifyPN verifypn = new VerifyPN(new FileFinder(), new MessengerImpl());
487 verifypn.setup();
488 return verifypn;
489 }
490
491- public static ModelChecker getModelChecker(TAPNQuery query, boolean isColored) {
492+ public static ModelChecker getModelChecker(TAPNQuery query) {
493 if (query.getReductionOption() == ReductionOption.VerifyTAPN) {
494 return getVerifyTAPN();
495 } else if (query.getReductionOption() == ReductionOption.VerifyDTAPN) {
496- return isColored? getVerifydTACPN(): getVerifydTAPN();
497+ return getVerifydTAPN();
498 } else if (query.getReductionOption() == ReductionOption.VerifyPN) {
499 return getVerifyPN();
500 } else {
501@@ -86,7 +80,7 @@
502 if (tapnNetwork.isUntimed()) {
503 modelChecker = getVerifyPN();
504 } else if (tapnNetwork.isColored()) {
505- modelChecker = getVerifydTACPN();
506+ modelChecker = getVerifydTAPN();
507 }else if (tapnNetwork.hasWeights() || tapnNetwork.hasUrgentTransitions() || tapnNetwork.hasUncontrollableTransitions()) {
508 modelChecker = getVerifydTAPN();
509 } else {
510@@ -153,7 +147,7 @@
511 }
512
513 public static void runVerifyTAPNVerification(TimedArcPetriNetNetwork tapnNetwork, TAPNQuery query, VerificationCallback callback) {
514- runVerifyTAPNVerification(tapnNetwork, query, callback, null, false);
515+ runVerifyTAPNVerification(tapnNetwork, query, callback, null, false, null);
516 }
517
518 public static void runVerifyTAPNVerification(
519@@ -161,9 +155,9 @@
520 TAPNQuery query,
521 VerificationCallback callback,
522 HashMap<TimedArcPetriNet, DataLayer> guiModels,
523- boolean onlyCreateReducedNet
524- ) {
525- ModelChecker verifytapn = getModelChecker(query, tapnNetwork.isColored());
526+ boolean onlyCreateReducedNet,
527+ PetriNetTab.TAPNLens lens) {
528+ ModelChecker verifytapn = getModelChecker(query);
529
530
531 try {
532@@ -185,9 +179,9 @@
533 TCTLAbstractProperty inputQuery = query.getProperty();
534
535 int bound = query.getCapacity();
536-
537+ boolean isColored = (lens != null && lens.isColored() || tapnNetwork.isColored());
538 VerifyTAPNOptions verifytapnOptions;
539- if (query.getReductionOption() == ReductionOption.VerifyDTAPN || (tapnNetwork != null && tapnNetwork.isColored() && !tapnNetwork.isUntimed())) {
540+ if (query.getReductionOption() == ReductionOption.VerifyDTAPN) {
541 verifytapnOptions = new VerifyDTAPNOptions(
542 bound,
543 query.getTraceOption(),
544@@ -208,9 +202,10 @@
545 reducedNetTempFile.getAbsolutePath(),
546 query.usePartitioning(),
547 query.useColorFixpoint(),
548- query.isColored()
549+ isColored // Unfold net
550 );
551 } else if (query.getReductionOption() == ReductionOption.VerifyPN) {
552+
553 verifytapnOptions = new VerifyPNOptions(
554 bound,
555 query.getTraceOption(),
556@@ -228,8 +223,8 @@
557 reducedNetTempFile.getAbsolutePath(),
558 query.isTarOptionEnabled(),
559 query.isTarjan(),
560- tapnNetwork.isColored(),
561- tapnNetwork.isColored() && (!tapnNetwork.isUntimed() || query.getTraceOption() != TAPNQuery.TraceOption.NONE),
562+ isColored,
563+ isColored && query.getTraceOption() != TAPNQuery.TraceOption.NONE,
564 query.usePartitioning(),
565 query.useColorFixpoint(),
566 query.useSymmetricVars()
567@@ -265,7 +260,7 @@
568 if(tapnNetwork.isColored() && query.getTraceOption() != TAPNQuery.TraceOption.NONE){
569 SmartDrawDialog.setupWorkerListener(thread);
570 }
571- thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound), query);
572+ thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound), query, lens);
573 dialog.setVisible(true);
574 } else {
575 JOptionPane.showMessageDialog(TAPAALGUI.getApp(),
576
577=== modified file 'src/net/tapaal/gui/petrinet/widgets/QueryPane.java'
578--- src/net/tapaal/gui/petrinet/widgets/QueryPane.java 2022-01-24 10:42:42 +0000
579+++ src/net/tapaal/gui/petrinet/widgets/QueryPane.java 2022-01-28 13:31:23 +0000
580@@ -456,7 +456,7 @@
581
582 if(NumberOfSelectedElements == 1) {
583 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyDTAPN || query.getReductionOption() == ReductionOption.VerifyPN)
584- Verifier.runVerifyTAPNVerification(tabContent.network(), query, null, tabContent.getGuiModels(), false);
585+ Verifier.runVerifyTAPNVerification(tabContent.network(), query, null, tabContent.getGuiModels(), false, tabContent.lens);
586 else
587 Verifier.runUppaalVerification(tabContent.network(), query);
588 }
589
590=== modified file 'src/resources/Example nets/intro-example.tapn'
591--- src/resources/Example nets/intro-example.tapn 2021-12-04 23:19:33 +0000
592+++ src/resources/Example nets/intro-example.tapn 2022-01-28 13:31:23 +0000
593@@ -92,7 +92,7 @@
594 <arcpath arcPointType="false" id="1" xCoord="59" yCoord="390"/>
595 </arc>
596 </net>
597- <query active="true" approximationDenominator="2" capacity="3" discreteInclusion="false" enableOverApproximation="false" enableUnderApproximation="false" extrapolationOption="AUTOMATIC" gcd="true" hashTableSize="MB_16" inclusionPlaces="*NONE*" name="Target Reachable" overApproximation="true" pTrie="true" query="EF IntroExample.Target = 1" reduction="true" reductionOption="VerifyTAPNdiscreteVerification" searchOption="BFS" symmetry="true" timeDarts="false" traceOption="SOME" useStubbornReduction="true" useTarOption="false"/>
598+ <query active="true" approximationDenominator="2" capacity="3" colorFixpoint="false" discreteInclusion="false" enableOverApproximation="false" enableUnderApproximation="false" extrapolationOption="null" gcd="true" hashTableSize="null" inclusionPlaces="*NONE*" name="Target Reachable" overApproximation="true" pTrie="true" partitioning="false" query="EF IntroExample.Target = 1" reduction="true" reductionOption="VerifyDTAPN" searchOption="BFS" symmetricVars="false" symmetry="true" timeDarts="false" traceOption="SOME" useStubbornReduction="true" useTarOption="false"/>
599 <k-bound bound="3"/>
600 <feature isGame="false" isTimed="true" isColored="false"/>
601 </pnml>

Subscribers

People subscribed via source and target branches