← Back to branch summary

~tapaal-contributor/tapaal/change-export-batch-shortcut-1820012

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java

  • Committer: Kenneth Yrke Jørgensen
  • Date: 2019-03-13 07:17:48 UTC
  • mfrom: (989 tapaal)
  • mto: This revision was merged to the branch mainline in revision 991.
  • Revision ID: kenneth@yrke.dk-20190313071748-fm6dc00yy27un3xd
Merged with trunk

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java
5
5
import java.util.List;
6
6
 
7
7
import javax.swing.SwingWorker;
8
 
 
9
8
import pipe.dataLayer.TAPNQuery.SearchOption;
10
9
import pipe.dataLayer.TAPNQuery.TraceOption;
 
10
import pipe.dataLayer.TAPNQuery.WorkflowMode;
11
11
import pipe.gui.CreateGui;
12
12
import pipe.gui.FileFinder;
13
13
import pipe.gui.MessengerImpl;
 
14
import pipe.gui.Verifier;
14
15
import pipe.gui.widgets.QueryPane;
15
16
import dk.aau.cs.Messenger;
16
17
import dk.aau.cs.TCTL.TCTLAGNode;
17
18
import dk.aau.cs.TCTL.TCTLEFNode;
 
19
import dk.aau.cs.TCTL.TCTLEGNode;
 
20
import dk.aau.cs.TCTL.TCTLPlaceNode;
18
21
import dk.aau.cs.TCTL.TCTLAbstractProperty;
 
22
import dk.aau.cs.TCTL.TCTLAtomicPropositionNode;
 
23
import dk.aau.cs.TCTL.TCTLConstNode;
19
24
import dk.aau.cs.TCTL.TCTLTrueNode;
20
25
import dk.aau.cs.TCTL.TCTLDeadlockNode;
21
26
import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor;
24
29
import dk.aau.cs.gui.components.BatchProcessingResultsTableModel;
25
30
import dk.aau.cs.io.batchProcessing.BatchProcessingModelLoader;
26
31
import dk.aau.cs.io.batchProcessing.LoadedBatchProcessingModel;
 
32
import dk.aau.cs.model.tapn.Bound;
27
33
import dk.aau.cs.model.tapn.TAPNQuery;
28
34
import dk.aau.cs.model.tapn.TimedArcPetriNet;
29
35
import dk.aau.cs.model.tapn.TimedPlace;
30
36
import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
31
37
import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
 
38
import dk.aau.cs.model.tapn.simulation.TimedTAPNNetworkTrace;
32
39
import dk.aau.cs.translations.ReductionOption;
33
40
import dk.aau.cs.util.MemoryMonitor;
34
41
import dk.aau.cs.util.Require;
35
42
import dk.aau.cs.util.Tuple;
36
43
import dk.aau.cs.util.UnsupportedModelException;
37
44
import dk.aau.cs.util.UnsupportedQueryException;
 
45
import dk.aau.cs.util.VerificationCallback;
38
46
import dk.aau.cs.verification.ITAPNComposer;
39
47
import dk.aau.cs.verification.ModelChecker;
40
48
import dk.aau.cs.verification.NameMapping;
47
55
import dk.aau.cs.verification.VerificationResult;
48
56
import dk.aau.cs.verification.UPPAAL.Verifyta;
49
57
import dk.aau.cs.verification.UPPAAL.VerifytaOptions;
 
58
import dk.aau.cs.verification.VerifyTAPN.TraceType;
50
59
import dk.aau.cs.verification.VerifyTAPN.VerifyDTAPNOptions;
51
60
import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
52
61
import dk.aau.cs.verification.VerifyTAPN.VerifyPNOptions;
57
66
import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.QueryPropertyOption;
58
67
import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.StubbornReductionOption;
59
68
import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.SymmetryOption;
 
69
import pipe.dataLayer.TAPNQuery.ExtrapolationOption;
60
70
import pipe.dataLayer.TAPNQuery.QueryCategory;
61
71
 
62
72
public class BatchProcessingWorker extends SwingWorker<Void, BatchProcessingVerificationResult> {
71
81
        private boolean oomCurrentVerification = false;
72
82
        private int verificationTasksCompleted;
73
83
        private LoadedBatchProcessingModel model;
 
84
        private boolean isSoundnessCheck;
 
85
        private boolean isModelCheckOnly;
 
86
        private ArrayList<File> filesProcessed;
74
87
        
75
88
        
76
89
        public BatchProcessingWorker(List<File> files, BatchProcessingResultsTableModel tableModel, BatchProcessingVerificationOptions batchProcessingVerificationOptions) {
113
126
        
114
127
        @Override
115
128
        protected Void doInBackground() throws Exception {
 
129
                isSoundnessCheck = false;
 
130
                filesProcessed = new ArrayList<File>();
116
131
                for(File file : files){
117
132
 
118
133
                        fireFileChanged(file.getName());
119
134
                        LoadedBatchProcessingModel model = loadModel(file);
120
135
                        this.model = model;
121
 
                        if(model != null) {                     
 
136
                        if(model != null) {     
 
137
                Tuple<TimedArcPetriNet, NameMapping> composedModel = composeModel(model);
122
138
                                for(pipe.dataLayer.TAPNQuery query : model.queries()) {
123
139
                    if(exiting()) {
124
140
                        return null;
125
 
                    }                   
126
 
                    Tuple<TimedArcPetriNet, NameMapping> composedModel = composeModel(model);
 
141
                    }
 
142
                    //For "Search whole state space", "Existence of deadlock", "Soundness" and "Strong Soundness" 
 
143
                    //the file should only be checked once instead of checking every query
 
144
                    if(isModelCheckOnly && filesProcessed.contains(file)) {
 
145
                        continue;
 
146
                    }
127
147
                                        
128
 
                                        pipe.dataLayer.TAPNQuery queryToVerify = overrideVerificationOptions(composedModel.value1(), query);
 
148
                                        pipe.dataLayer.TAPNQuery queryToVerify = overrideVerificationOptions(composedModel.value1(), query, file);
129
149
                                        
130
150
                                        if (batchProcessingVerificationOptions.isReductionOptionUserdefined()){
131
151
                                                processQueryForUserdefinedReductions(file, composedModel, queryToVerify);
132
152
                                        } else {
133
153
                                                processQuery(file, composedModel, queryToVerify);
134
154
                                        }
135
 
                                        
 
155
                                }
 
156
                                if(model.queries().isEmpty() && batchProcessingVerificationOptions.queryPropertyOption() != QueryPropertyOption.KeepQueryOption) {
 
157
                                        pipe.dataLayer.TAPNQuery queryToVerify = createQueryFromQueryPropertyOption(composedModel.value1(), batchProcessingVerificationOptions.queryPropertyOption(), file);
 
158
                                        processQuery(file, composedModel, queryToVerify);
136
159
                                }
137
160
                        }
138
161
                }
234
257
        }
235
258
 
236
259
        private void processQuery(File file, Tuple<TimedArcPetriNet, NameMapping> composedModel, pipe.dataLayer.TAPNQuery queryToVerify) throws Exception {
237
 
                if(queryToVerify.isActive()) { 
238
 
                        VerificationResult<TimedArcPetriNetTrace> verificationResult = verifyQuery(file, composedModel, queryToVerify);
 
260
                if(queryToVerify.isActive()) {
 
261
 
 
262
                        if(isSoundnessCheck) {
 
263
                                processSoundnessCheck(file, composedModel, queryToVerify);
 
264
                        }
 
265
                        if(!isSoundnessCheck) { 
 
266
                                VerificationResult<TimedArcPetriNetTrace> verificationResult = verifyQuery(file, composedModel, queryToVerify);
239
267
                        
240
 
                        if(verificationResult != null)
241
 
                                processVerificationResult(file, queryToVerify, verificationResult);
 
268
                                if(verificationResult != null)
 
269
                                        processVerificationResult(file, queryToVerify, verificationResult);
 
270
                        }
242
271
                }
243
272
                else
244
273
                        publishResult(file.getName(), queryToVerify, "Skipped - query is disabled because it contains propositions involving places from a deactivated component", 0, new NullStats());
 
274
                
245
275
                fireVerificationTaskComplete();
246
276
        }
247
 
 
248
 
        private pipe.dataLayer.TAPNQuery overrideVerificationOptions(TimedArcPetriNet model, pipe.dataLayer.TAPNQuery query) throws Exception {
 
277
        private void processSoundnessCheck(final File file, Tuple<TimedArcPetriNet, NameMapping> composedModel, final pipe.dataLayer.TAPNQuery queryToVerify) throws Exception{
 
278
                VerificationResult<TimedArcPetriNetTrace> verificationResult;
 
279
                if(queryToVerify.getWorkflowMode() == WorkflowMode.WORKFLOW_SOUNDNESS) {
 
280
                        try {
 
281
                                verificationResult = verifyQuery(file, composedModel, queryToVerify);
 
282
                                if(verificationResult != null)
 
283
                                        processVerificationResult(file, queryToVerify, verificationResult);
 
284
                        } catch (Exception e) {
 
285
                                publishResult(file.getName(), queryToVerify, "Skipped - model not supported by the verification method. Try running workflow analysis from the menu.", 0, new NullStats());
 
286
                        }
 
287
                }
 
288
                if(queryToVerify.getWorkflowMode() == WorkflowMode.WORKFLOW_STRONG_SOUNDNESS) {
 
289
                        //Test for Soundness before Strong Soundness
 
290
                        pipe.dataLayer.TAPNQuery queryToCheckIfSound = new pipe.dataLayer.TAPNQuery(
 
291
                                        "Workflow soundness check", queryToVerify.getCapacity(),
 
292
                                        new TCTLEFNode(new TCTLTrueNode()), TraceOption.SOME,
 
293
                                        SearchOption.DEFAULT,
 
294
                                        ReductionOption.VerifyTAPNdiscreteVerification, true, true,
 
295
                                        false, true, false, null, ExtrapolationOption.AUTOMATIC,
 
296
                                        WorkflowMode.WORKFLOW_SOUNDNESS);
 
297
                        long time = 0;
 
298
                        try {
 
299
                                final VerificationResult<TimedArcPetriNetTrace> resultOfSoundCheck = verifyQuery(file, composedModel, queryToCheckIfSound);
 
300
                                //Strong Soundness check
 
301
                                if(resultOfSoundCheck.isQuerySatisfied()) {
 
302
                                        long m = resultOfSoundCheck.stats().exploredStates();
 
303
                                        long B = 0;
 
304
                                        for (TimedPlace p : composedModel.value1().places()) {
 
305
                                                if (p.invariant().upperBound().equals(Bound.Infinity)) {
 
306
                                                        continue;
 
307
                                                }
 
308
                                                B = Math.max(B, p.invariant().upperBound().value());
 
309
                                        }
 
310
                                        long c  = m*B+1;
 
311
                                        queryToVerify.setStrongSoundnessBound(c);
 
312
                                        Verifier.runVerifyTAPNVerification(model.network(), queryToVerify, new VerificationCallback() {
 
313
                                                
 
314
                                                @Override
 
315
                                                public void run() {                                                     
 
316
                                                }
 
317
                                                
 
318
                                                @Override
 
319
                                                public void run(VerificationResult<TAPNNetworkTrace> result) {
 
320
                                                        TraceType traceType = ((TimedTAPNNetworkTrace) result.getTrace()).getTraceType();
 
321
                                                        if(traceType == TraceType.EG_DELAY_FOREVER || traceType == TraceType.EG_LOOP) {
 
322
                                                                publishResult(file.getName(), queryToVerify, "Not Strongly Sound", result.verificationTime(), result.stats());
 
323
                                                        } else
 
324
                                                                publishResult(file.getName(), queryToVerify, "Strongly Sound", result.verificationTime(), result.stats());
 
325
                                                }
 
326
                                        });
 
327
 
 
328
                                } else
 
329
                                        publishResult(file.getName(), queryToVerify, "Not Strongly Sound", resultOfSoundCheck.verificationTime(), resultOfSoundCheck.stats());
 
330
                                
 
331
                        } catch (Exception e) {
 
332
                                publishResult(file.getName(), queryToVerify, "Skipped - model is not a workflow net. Try running workflow analysis from the menu.", time, new NullStats());
 
333
                        }
 
334
                }
 
335
        }
 
336
 
 
337
        private pipe.dataLayer.TAPNQuery overrideVerificationOptions(TimedArcPetriNet model, pipe.dataLayer.TAPNQuery query, File fileToBeChecked) throws Exception {
249
338
                if(batchProcessingVerificationOptions != null) {
250
 
                        SearchOption search = batchProcessingVerificationOptions.searchOption() == SearchOption.BatchProcessingKeepQueryOption ? query.getSearchOption() : batchProcessingVerificationOptions.searchOption();
251
 
                        ReductionOption option = query.getReductionOption();
252
 
                        TCTLAbstractProperty property;
253
 
                        String name;
254
 
                        if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.ExistDeadlock) {
255
 
                            property = generateExistDeadlock(model);
256
 
                            name = "Existence of a deadlock";
257
 
                        } else if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace) {
258
 
                            property = generateSearchWholeStateSpaceProperty(model);
259
 
                            name = "Search whole state space";
260
 
                        } else {
261
 
                            property = query.getProperty();
262
 
                            name = query.getName();
263
 
                        }
264
 
                        boolean symmetry = batchProcessingVerificationOptions.symmetry() == SymmetryOption.KeepQueryOption ? query.useSymmetry() : getSymmetryFromBatchProcessingOptions();
265
 
                        boolean stubbornReduction = batchProcessingVerificationOptions.stubbornReductionOption() == StubbornReductionOption.KeepQueryOption ? query.isStubbornReductionEnabled() : getStubbornReductionFromBatchProcessingOptions();
266
339
                        int capacity = batchProcessingVerificationOptions.KeepCapacityFromQuery() ? query.getCapacity() : batchProcessingVerificationOptions.capacity();
267
 
                        boolean overApproximation = query.isOverApproximationEnabled();
268
 
                        boolean underApproximation = query.isUnderApproximationEnabled();
269
 
                        int approximationDenominator = query.approximationDenominator();
270
 
                        if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.None) {
271
 
                                overApproximation = false;
272
 
                                underApproximation = false;
273
 
                        } else if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.OverApproximation) {
274
 
                                overApproximation = true;
275
 
                                underApproximation = false;
276
 
                        } else if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.UnderApproximation) {
277
 
                                overApproximation = false;
278
 
                                underApproximation = true;
279
 
                        }
280
 
                        if (batchProcessingVerificationOptions.approximationDenominator() != 0) {
281
 
                                approximationDenominator = batchProcessingVerificationOptions.approximationDenominator();
282
 
                        }
283
 
                        
284
 
                        pipe.dataLayer.TAPNQuery changedQuery = new pipe.dataLayer.TAPNQuery(name, capacity, property, TraceOption.NONE, search, option, symmetry, false, query.useTimeDarts(), query.usePTrie(), query.useOverApproximation(), query.useReduction(),  query.getHashTableSize(), query.getExtrapolationOption(), query.inclusionPlaces(), overApproximation, underApproximation, approximationDenominator);
285
 
                        
286
 
                        if(batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.KeepQueryOption)
287
 
                                changedQuery.setActive(query.isActive());
288
 
 
289
 
                        changedQuery.setCategory(query.getCategory());
290
 
                        changedQuery.setAlgorithmOption(query.getAlgorithmOption());
291
 
                        changedQuery.setUseSiphontrap(query.isSiphontrapEnabled());
292
 
                        changedQuery.setUseQueryReduction(query.isQueryReductionEnabled());
293
 
                        changedQuery.setUseStubbornReduction(stubbornReduction);
294
 
                        return changedQuery;
 
340
                        if(!(batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.StrongSoundness || batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.Soundness)) {
 
341
                                SearchOption search = batchProcessingVerificationOptions.searchOption() == SearchOption.BatchProcessingKeepQueryOption ? query.getSearchOption() : batchProcessingVerificationOptions.searchOption();
 
342
                                ReductionOption option = query.getReductionOption();
 
343
                    TCTLAbstractProperty property;
 
344
                    String name;
 
345
                    if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.ExistDeadlock) {
 
346
                                        property = generateExistDeadlock(model);
 
347
                                        name = "Existence of a deadlock";
 
348
                                        filesProcessed.add(fileToBeChecked);
 
349
                                        isModelCheckOnly = true;
 
350
                    } else if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace) {
 
351
                        property = generateSearchWholeStateSpaceProperty(model);
 
352
                        name = "Search whole state space";
 
353
                        filesProcessed.add(fileToBeChecked);
 
354
                        isModelCheckOnly = true;
 
355
                    } else {
 
356
                        property = query.getProperty();
 
357
                        name = query.getName();
 
358
                    }
 
359
                                boolean symmetry = batchProcessingVerificationOptions.symmetry() == SymmetryOption.KeepQueryOption ? query.useSymmetry() : getSymmetryFromBatchProcessingOptions();
 
360
                                boolean stubbornReduction = batchProcessingVerificationOptions.stubbornReductionOption() == StubbornReductionOption.KeepQueryOption ? query.isStubbornReductionEnabled() : getStubbornReductionFromBatchProcessingOptions();
 
361
                                boolean overApproximation = query.isOverApproximationEnabled();
 
362
                                boolean underApproximation = query.isUnderApproximationEnabled();
 
363
                                int approximationDenominator = query.approximationDenominator();
 
364
                                if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.None) {
 
365
                                        overApproximation = false;
 
366
                                        underApproximation = false;
 
367
                                } else if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.OverApproximation) {
 
368
                                        overApproximation = true;
 
369
                                        underApproximation = false;
 
370
                                } else if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.UnderApproximation) {
 
371
                                        overApproximation = false;
 
372
                                        underApproximation = true;
 
373
                                }
 
374
                                if (batchProcessingVerificationOptions.approximationDenominator() != 0) {
 
375
                                        approximationDenominator = batchProcessingVerificationOptions.approximationDenominator();
 
376
                                }
 
377
                                
 
378
                                pipe.dataLayer.TAPNQuery changedQuery = new pipe.dataLayer.TAPNQuery(name, capacity, property, TraceOption.NONE, search, option, symmetry, false, query.useTimeDarts(), query.usePTrie(), query.useOverApproximation(), query.useReduction(),  query.getHashTableSize(), query.getExtrapolationOption(), query.inclusionPlaces(), overApproximation, underApproximation, approximationDenominator);
 
379
                                
 
380
                                if(batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.KeepQueryOption)
 
381
                                        changedQuery.setActive(query.isActive());
 
382
        
 
383
                                changedQuery.setCategory(query.getCategory());
 
384
                                changedQuery.setAlgorithmOption(query.getAlgorithmOption());
 
385
                                changedQuery.setUseSiphontrap(query.isSiphontrapEnabled());
 
386
                                changedQuery.setUseQueryReduction(query.isQueryReductionEnabled());
 
387
                                changedQuery.setUseStubbornReduction(stubbornReduction);
 
388
                                return changedQuery;
 
389
                        } else if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.Soundness) {
 
390
                                isSoundnessCheck = true;
 
391
                                query = new pipe.dataLayer.TAPNQuery(
 
392
                                        "Workflow soundness check", capacity,
 
393
                                                        new TCTLEFNode(new TCTLTrueNode()), TraceOption.SOME,
 
394
                                                        SearchOption.DEFAULT,
 
395
                                                        ReductionOption.VerifyTAPNdiscreteVerification, true, true,
 
396
                                                        false, true, false, null, ExtrapolationOption.AUTOMATIC,
 
397
                                                        WorkflowMode.WORKFLOW_SOUNDNESS);
 
398
                                filesProcessed.add(fileToBeChecked);
 
399
                                isModelCheckOnly = true;
 
400
                
 
401
                } else if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.StrongSoundness) {
 
402
                        isSoundnessCheck = true;
 
403
                        query = new pipe.dataLayer.TAPNQuery(
 
404
                                                "Workflow soundness check", capacity,
 
405
                                                                new TCTLEGNode(new TCTLTrueNode()), TraceOption.SOME,
 
406
                                                                SearchOption.DEFAULT,
 
407
                                                                ReductionOption.VerifyTAPNdiscreteVerification, true, true,
 
408
                                                                false, true, false, null, ExtrapolationOption.AUTOMATIC,
 
409
                                                                WorkflowMode.WORKFLOW_STRONG_SOUNDNESS);
 
410
                                filesProcessed.add(fileToBeChecked);
 
411
                                isModelCheckOnly = true;
 
412
                        }
295
413
                }
296
414
                
297
415
                return query;
298
416
        }
 
417
        
 
418
        private pipe.dataLayer.TAPNQuery createQueryFromQueryPropertyOption(TimedArcPetriNet model, QueryPropertyOption option, File fileToBeChecked) throws Exception {
 
419
                int capacity = batchProcessingVerificationOptions.capacity();
 
420
                ReductionOption reductionOption = model.isUntimed() ? ReductionOption.VerifyPN : ReductionOption.VerifyTAPN;
 
421
                if(option == QueryPropertyOption.ExistDeadlock) {
 
422
                        filesProcessed.add(fileToBeChecked);
 
423
                        return new pipe.dataLayer.TAPNQuery(
 
424
                                        "Existence of a deadlock", capacity,
 
425
                                                        generateExistDeadlock(model), TraceOption.NONE,
 
426
                                                        SearchOption.DEFAULT,
 
427
                                                        reductionOption, true, true,
 
428
                                                        false, true, false, null, ExtrapolationOption.AUTOMATIC,
 
429
                                                        WorkflowMode.WORKFLOW_SOUNDNESS);
 
430
                }
 
431
                if(option == QueryPropertyOption.SearchWholeStateSpace) {
 
432
                        filesProcessed.add(fileToBeChecked);
 
433
                        return new pipe.dataLayer.TAPNQuery(
 
434
                                        "Search whole state space", capacity,
 
435
                                                        generateSearchWholeStateSpaceProperty(model), TraceOption.NONE,
 
436
                                                        SearchOption.DEFAULT,
 
437
                                                        reductionOption, true, true,
 
438
                                                        false, true, false, null, ExtrapolationOption.AUTOMATIC,
 
439
                                                        WorkflowMode.WORKFLOW_SOUNDNESS);
 
440
                }
 
441
                if (option == QueryPropertyOption.Soundness) {
 
442
                        isSoundnessCheck = true;
 
443
                        filesProcessed.add(fileToBeChecked);
 
444
                        return new pipe.dataLayer.TAPNQuery(
 
445
                                "Workflow soundness check", capacity,
 
446
                                                new TCTLEFNode(new TCTLTrueNode()), TraceOption.SOME,
 
447
                                                SearchOption.DEFAULT,
 
448
                                                ReductionOption.VerifyTAPNdiscreteVerification, true, true,
 
449
                                                false, true, false, null, ExtrapolationOption.AUTOMATIC,
 
450
                                                WorkflowMode.WORKFLOW_SOUNDNESS);
 
451
                }
 
452
                if(option == QueryPropertyOption.StrongSoundness) {
 
453
                        isSoundnessCheck = true;
 
454
                        filesProcessed.add(fileToBeChecked);
 
455
                return new pipe.dataLayer.TAPNQuery(
 
456
                                        "Workflow soundness check", capacity,
 
457
                                                        new TCTLEGNode(new TCTLTrueNode()), TraceOption.SOME,
 
458
                                                        SearchOption.DEFAULT,
 
459
                                                        ReductionOption.VerifyTAPNdiscreteVerification, true, true,
 
460
                                                        false, true, false, null, ExtrapolationOption.AUTOMATIC,
 
461
                                                        WorkflowMode.WORKFLOW_STRONG_SOUNDNESS);
 
462
                }
 
463
                return null;
 
464
        }
299
465
 
300
466
        private boolean getSymmetryFromBatchProcessingOptions() {
301
467
                return batchProcessingVerificationOptions.symmetry() == SymmetryOption.Yes;
325
491
                try {
326
492
                        verificationResult = verify(composedModel, query);
327
493
                } catch(UnsupportedModelException e) {
328
 
                        publishResult(file.getName(), query, "Skipped - model not supported by the verification method", 0, new NullStats());
 
494
                        if(isSoundnessCheck)
 
495
                                publishResult(file.getName(), query, "Skipped - model is not a workflow net. Try running workflow analysis from the menu.", 0, new NullStats());
 
496
                        else
 
497
                                publishResult(file.getName(), query, "Skipped - model not supported by the verification method", 0, new NullStats());
329
498
                        return null;
330
499
                } catch(UnsupportedQueryException e) {
331
500
                        if(e.getMessage().toLowerCase().contains("discrete inclusion"))
333
502
                        else
334
503
                                publishResult(file.getName(), query, "Skipped - query not supported by the verification method", 0, new NullStats());
335
504
                        return null;
336
 
                }
 
505
                } 
337
506
                return verificationResult;
338
507
        }
339
508
 
356
525
                        else
357
526
                        {
358
527
                                queryResult = verificationResult.getQueryResult().isQuerySatisfied() ? "Satisfied" : "Not Satisfied";
 
528
                                if(isSoundnessCheck && !verificationResult.isQuerySatisfied())
 
529
                                        queryResult = "Not Sound";
 
530
                                if(isSoundnessCheck && verificationResult.isQuerySatisfied()) {
 
531
                                        if(query.getWorkflowMode() == WorkflowMode.WORKFLOW_STRONG_SOUNDNESS)
 
532
                                                queryResult = "Strongly Sound";
 
533
                                        else
 
534
                                                queryResult = "Sound";
 
535
                                }
359
536
                        }
360
537
                        if (query.discreteInclusion() && !verificationResult.isBounded() && 
361
538
                                        ((query.queryType().equals(QueryType.EF) && !verificationResult.getQueryResult().isQuerySatisfied())
368
545
                                        queryResult = "Inconclusive";
369
546
                                }
370
547
                        publishResult(file.getName(), query, queryResult,       verificationResult.verificationTime(), verificationResult.stats());
 
548
                } else if(isSoundnessCheck && verificationResult.error()) {
 
549
                        publishResult(file.getName(), query, "Skipped - model is not a workflow net. Try running workflow analysis from the menu.", verificationResult.verificationTime(), new NullStats());
371
550
                } else {
372
551
                        publishResult(file.getName(), query, "Error during verification", verificationResult.verificationTime(), new NullStats());
373
552
                }               
427
606
                return new TCTLAGNode(new TCTLTrueNode());
428
607
        }
429
608
        
430
 
        private TCTLAbstractProperty generateExistDeadlock(TimedArcPetriNet model) throws Exception {
 
609
        private TCTLAbstractProperty generateExistDeadlock(TimedArcPetriNet model) throws Exception {
431
610
                return new TCTLEFNode(new TCTLDeadlockNode()); 
432
611
        }
433
 
 
 
612
        
434
613
        private ModelChecker getModelChecker(pipe.dataLayer.TAPNQuery query) {
435
614
                if(query.getReductionOption() == ReductionOption.VerifyTAPN)
436
615
                        return getVerifyTAPN();