← Back to branch summary

~tapaal-contributor/tapaal/display-shared-places-transitions-1879126

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/approximation/ApproximationWorker.java

  • Committer: Jiri Srba
  • Date: 2020-04-28 19:15:28 UTC
  • mfrom: (998.2.376 testbranch)
  • Revision ID: srba@cs.aau.dk-20200428191528-3xxjqa1r4jcob5ur
merged in lp:~yrke/tapaal/testbranch doing majour refactoring of the GUI

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/dk/aau/cs/approximation/ApproximationWorker.java
2
2
 
3
3
import java.math.BigDecimal;
4
4
 
5
 
import javax.swing.SwingWorker.StateValue;
6
 
 
7
5
import pipe.dataLayer.TAPNQuery.TraceOption;
8
6
import pipe.gui.RunVerificationBase;
9
7
import pipe.gui.widgets.InclusionPlaces;
29
27
import dk.aau.cs.verification.TAPNTraceDecomposer;
30
28
import dk.aau.cs.verification.VerificationOptions;
31
29
import dk.aau.cs.verification.VerificationResult;
32
 
import dk.aau.cs.verification.UPPAAL.VerifytaOptions;
33
30
import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions;
34
31
import dk.aau.cs.verification.batchProcessing.BatchProcessingWorker;
35
32
 
36
33
public class ApproximationWorker {
37
 
        public VerificationResult<TAPNNetworkTrace> normalWorker(VerificationOptions options, ModelChecker modelChecker,
38
 
                        Tuple<TimedArcPetriNet, NameMapping> transformedModel, ITAPNComposer composer, TAPNQuery clonedQuery,
39
 
                        RunVerificationBase verificationBase, TimedArcPetriNetNetwork model) throws Exception {
 
34
        public VerificationResult<TAPNNetworkTrace> normalWorker(
 
35
                        VerificationOptions options,
 
36
                        ModelChecker modelChecker,
 
37
                        Tuple<TimedArcPetriNet, NameMapping> transformedModel,
 
38
                        ITAPNComposer composer,
 
39
                        TAPNQuery clonedQuery,
 
40
                        RunVerificationBase verificationBase,
 
41
                        TimedArcPetriNetNetwork model
 
42
        ) throws Exception {
40
43
                
41
44
                // If options is of an instance of VerifyTAPNOptions then save the inclusion places before verify alters them
42
45
                InclusionPlaces oldInclusionPlaces = null;
45
48
                
46
49
                // Enable SOME_TRACE if not already
47
50
                TraceOption oldTraceOption = options.traceOption();
48
 
                if ((options.enableOverApproximation() || options.enableUnderApproximation())) {
 
51
                if ((options.enabledOverApproximation() || options.enabledUnderApproximation())) {
49
52
                        options.setTraceOption(TraceOption.SOME);
50
53
                }
51
54
                
52
 
                VerificationResult<TAPNNetworkTrace> value = null;
 
55
                VerificationResult<TAPNNetworkTrace> toReturn = null;
53
56
                VerificationResult<TimedArcPetriNetTrace> result = modelChecker.verify(options, transformedModel, clonedQuery);
54
 
                if (verificationBase.isCancelled()) {
55
 
                        verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
56
 
                }
 
57
 
57
58
                if (result.error()) {
58
59
                        options.setTraceOption(oldTraceOption);
59
60
                        return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), result.verificationTime());
60
61
                }
61
 
                else if (options.enableOverApproximation()) {
 
62
                else if (options.enabledOverApproximation()) {
62
63
                        // Over-approximation
 
64
                        //ApproximationDenominator should not be able to be 1, if its one its the same as an exact analyses. --kyrke 2020-03-25
63
65
                        if (options.approximationDenominator() == 1) {
64
66
                                // If r = 1
65
67
                                // No matter what it answered -> return that answer
66
68
                                QueryResult queryResult = result.getQueryResult();
67
 
                                value =  new VerificationResult<TAPNNetworkTrace>(
 
69
                                toReturn =  new VerificationResult<TAPNNetworkTrace>(
68
70
                                                queryResult,
69
71
                                                decomposeTrace(result.getTrace(), transformedModel.value2(), model),
70
72
                                                decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
71
73
                                                result.verificationTime(),
72
74
                                                result.stats(),
73
 
                                                result.isOverApproximationResult());
74
 
                                value.setNameMapping(transformedModel.value2());
 
75
                                                result.isSolvedUsingStateEquation());
 
76
                                toReturn.setNameMapping(transformedModel.value2());
75
77
                        } else {
76
78
                                // If r > 1
77
79
                                if (result.getTrace() != null && (((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && result.getQueryResult().isQuerySatisfied())
80
82
                                                // The results are inconclusive, but we get a trace and can use trace TAPN for verification.
81
83
                                        
82
84
                                                VerificationResult<TimedArcPetriNetTrace> approxResult = result;
83
 
                                                value = new VerificationResult<TAPNNetworkTrace>(
 
85
                                                toReturn = new VerificationResult<TAPNNetworkTrace>(
84
86
                                                                approxResult.getQueryResult(),
85
87
                                                                decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
86
88
                                                                decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
87
89
                                                                approxResult.verificationTime(),
88
90
                                                                approxResult.stats(),
89
 
                                                                approxResult.isOverApproximationResult());
90
 
                                                value.setNameMapping(transformedModel.value2());
 
91
                                                                approxResult.isSolvedUsingStateEquation());
 
92
                                                toReturn.setNameMapping(transformedModel.value2());
91
93
                                                
92
94
                                                OverApproximation overaprx = new OverApproximation();
93
95
                        
94
96
                                                //Create trace TAPN from the trace
95
97
                                                Tuple<TimedArcPetriNet, NameMapping> transformedOriginalModel = composer.transformModel(model);
96
 
                                                overaprx.makeTraceTAPN(transformedOriginalModel, value, clonedQuery);
 
98
                                                overaprx.makeTraceTAPN(transformedOriginalModel, toReturn, clonedQuery);
97
99
                                                
98
100
                                                // Reset the inclusion places in order to avoid NullPointerExceptions
99
101
                                                if (options instanceof VerifyTAPNOptions && oldInclusionPlaces != null)
102
104
                                                // run model checker again for trace TAPN
103
105
                                                MemoryMonitor.cumulateMemory();
104
106
                                                result = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
105
 
                                                if (verificationBase.isCancelled()) {
106
 
                                                        verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
107
 
                                                }
 
107
 
108
108
                                                if (result.error()) {
109
109
                                                        options.setTraceOption(oldTraceOption);
110
110
                                                        // if the old trace option was none, we need to set the results traces to null so GUI doesn't try to display the traces later
111
 
                                                        if (oldTraceOption == TraceOption.NONE && value != null){
112
 
                                                                value.setTrace(null);
113
 
                                                                value.setSecondaryTrace(null);
 
111
                                                        if (oldTraceOption == TraceOption.NONE && toReturn != null){
 
112
                                                                toReturn.setTrace(null);
 
113
                                                                toReturn.setSecondaryTrace(null);
114
114
                                                        }
115
115
                                                        return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), approxResult.verificationTime() + result.verificationTime());
116
116
                                                }
127
127
                                                
128
128
                                                // If satisfied trace -> Return result
129
129
                                                // This is satisfied for EF and EG and not satisfied for AG and AF
130
 
                                                value = new VerificationResult<TAPNNetworkTrace>(
 
130
                                                toReturn = new VerificationResult<TAPNNetworkTrace>(
131
131
                                                                queryResult,
132
132
                                                                decomposeTrace(result.getTrace(), transformedModel.value2(), model),
133
133
                                                                decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
134
134
                                                                approxResult.verificationTime() + result.verificationTime(),
135
135
                                                                approxResult.stats(),
136
 
                                                                approxResult.isOverApproximationResult());
137
 
                                                value.setNameMapping(transformedModel.value2());
 
136
                                                                approxResult.isSolvedUsingStateEquation());
 
137
                                                toReturn.setNameMapping(transformedModel.value2());
138
138
                                        } 
139
139
                                        else if (((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && !result.getQueryResult().isQuerySatisfied())
140
140
                                                        || ((result.getQueryResult().queryType() == QueryType.AG || result.getQueryResult().queryType() == QueryType.AF) && result.getQueryResult().isQuerySatisfied())) {
147
147
                                                }
148
148
                                                
149
149
                                                VerificationResult<TimedArcPetriNetTrace> approxResult = result;
150
 
                                                value = new VerificationResult<TAPNNetworkTrace>(
 
150
                                                toReturn = new VerificationResult<TAPNNetworkTrace>(
151
151
                                                                approxResult.getQueryResult(),
152
152
                                                                decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
153
153
                                                                decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
154
154
                                                                approxResult.verificationTime(),
155
155
                                                                approxResult.stats(),
156
 
                                                                approxResult.isOverApproximationResult());
157
 
                                                value.setNameMapping(transformedModel.value2());
 
156
                                                                approxResult.isSolvedUsingStateEquation());
 
157
                                                toReturn.setNameMapping(transformedModel.value2());
158
158
                                        } else {
159
159
                                                // We cannot use the result directly, and did not get a trace.
160
160
                                                
162
162
                                                queryResult.setApproximationInconclusive(true);
163
163
                                                
164
164
                                                VerificationResult<TimedArcPetriNetTrace> approxResult = result;
165
 
                                                value = new VerificationResult<TAPNNetworkTrace>(
 
165
                                                toReturn = new VerificationResult<TAPNNetworkTrace>(
166
166
                                                                approxResult.getQueryResult(),
167
167
                                                                decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
168
168
                                                                decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
169
169
                                                                approxResult.verificationTime(),
170
170
                                                                approxResult.stats(),
171
 
                                                                approxResult.isOverApproximationResult());
172
 
                                                value.setNameMapping(transformedModel.value2());
 
171
                                                                approxResult.isSolvedUsingStateEquation());
 
172
                                                toReturn.setNameMapping(transformedModel.value2());
173
173
                                                
174
174
                                        }
175
175
                        }
176
176
                } 
177
 
                else if (options.enableUnderApproximation()) {
 
177
                else if (options.enabledUnderApproximation()) {
178
178
                        // Under-approximation
179
179
                        
180
180
                        if (result.getTrace() != null) {
189
189
                                        }
190
190
                                }
191
191
                        }
192
 
                        
 
192
                        //ApproximationDenominator should not be able to be 1, if its one its the same as an exact analyses. --kyrke 2020-03-25
193
193
                        if (options.approximationDenominator() == 1) { 
194
194
                                // If r = 1
195
195
                                // No matter it answered -> return that answer
196
196
                                QueryResult queryResult= result.getQueryResult();
197
 
                                value =  new VerificationResult<TAPNNetworkTrace>(
 
197
                                toReturn =  new VerificationResult<TAPNNetworkTrace>(
198
198
                                                queryResult,
199
199
                                                decomposeTrace(result.getTrace(), transformedModel.value2(), model),
200
200
                                                decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
201
201
                                                result.verificationTime(),
202
202
                                                result.stats(),
203
 
                                                result.isOverApproximationResult());
204
 
                                value.setNameMapping(transformedModel.value2());
 
203
                                                result.isSolvedUsingStateEquation());
 
204
                                toReturn.setNameMapping(transformedModel.value2());
205
205
                        }
206
206
                        else {
207
207
                                // If r > 1
210
210
                                        // If ((EF OR EG) AND not satisfied) OR ((AG OR AF) and satisfied) -> Inconclusive
211
211
                                        QueryResult queryResult= result.getQueryResult();
212
212
                                        queryResult.setApproximationInconclusive(true);
213
 
                                        value =  new VerificationResult<TAPNNetworkTrace>(
 
213
                                        toReturn =  new VerificationResult<TAPNNetworkTrace>(
214
214
                                                        queryResult,
215
215
                                                        decomposeTrace(result.getTrace(), transformedModel.value2(), model),
216
216
                                                        decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
217
217
                                                        result.verificationTime(),
218
218
                                                        result.stats(),
219
 
                                                        result.isOverApproximationResult());
220
 
                                        value.setNameMapping(transformedModel.value2());
 
219
                                                        result.isSolvedUsingStateEquation());
 
220
                                        toReturn.setNameMapping(transformedModel.value2());
221
221
                                } else if ((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && result.getQueryResult().isQuerySatisfied()
222
222
                                                || ((result.getQueryResult().queryType() == QueryType.AG || result.getQueryResult().queryType() == QueryType.AF) && ! result.getQueryResult().isQuerySatisfied())) {
223
223
                                                                                
225
225
                                                // If query does have deadlock or EG or AF a trace -> create trace TAPN
226
226
                                                //Create the verification satisfied result for the approximation
227
227
                                                VerificationResult<TimedArcPetriNetTrace> approxResult = result;
228
 
                                                value = new VerificationResult<TAPNNetworkTrace>(
 
228
                                                toReturn = new VerificationResult<TAPNNetworkTrace>(
229
229
                                                                approxResult.getQueryResult(),
230
230
                                                                decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
231
231
                                                                decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
232
232
                                                                approxResult.verificationTime(),
233
233
                                                                approxResult.stats(),
234
 
                                                                result.isOverApproximationResult());
235
 
                                                value.setNameMapping(transformedModel.value2());
 
234
                                                                result.isSolvedUsingStateEquation());
 
235
                                                toReturn.setNameMapping(transformedModel.value2());
236
236
                                                
237
237
                                                OverApproximation overaprx = new OverApproximation();
238
238
                                                
239
239
                        
240
240
                                                //Create trace TAPN from the trace
241
241
                                                Tuple<TimedArcPetriNet, NameMapping> transformedOriginalModel = composer.transformModel(model);
242
 
                                                overaprx.makeTraceTAPN(transformedOriginalModel, value, clonedQuery);
 
242
                                                overaprx.makeTraceTAPN(transformedOriginalModel, toReturn, clonedQuery);
243
243
                                                
244
244
                                                // Reset the inclusion places in order to avoid NullPointerExceptions
245
245
                                                if (options instanceof VerifyTAPNOptions && oldInclusionPlaces != null)
248
248
                                                //run model checker again for trace TAPN
249
249
                                                MemoryMonitor.cumulateMemory();
250
250
                                                result = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
251
 
                                                if (verificationBase.isCancelled()) {
252
 
                                                        verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
253
 
                                                }
 
251
 
254
252
                                                if (result.error()) {
255
253
                                                        options.setTraceOption(oldTraceOption);
256
254
                                                        // if the old trace option was none, we need to set the results traces to null so GUI doesn't try to display the traces later
257
 
                                                        if (oldTraceOption == TraceOption.NONE && value != null){
258
 
                                                                value.setTrace(null);
259
 
                                                                value.setSecondaryTrace(null);
 
255
                                                        if (oldTraceOption == TraceOption.NONE && toReturn != null){
 
256
                                                                toReturn.setTrace(null);
 
257
                                                                toReturn.setSecondaryTrace(null);
260
258
                                                        }
261
259
                                                        return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), result.verificationTime() + approxResult.verificationTime());
262
260
                                                }
276
274
                                                
277
275
                                                // If satisfied trace) -> Return result
278
276
                                                // This is satisfied for EF and EG and not satisfied for AG and AF
279
 
                                                value = new VerificationResult<TAPNNetworkTrace>(
 
277
                                                toReturn = new VerificationResult<TAPNNetworkTrace>(
280
278
                                                                queryResult,
281
279
                                                                decomposeTrace(result.getTrace(), transformedModel.value2(), model),
282
280
                                                                decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
283
281
                                                                approxResult.verificationTime() + result.verificationTime(),
284
282
                                                                approxResult.stats(),
285
 
                                                                approxResult.isOverApproximationResult());
286
 
                                                value.setNameMapping(transformedModel.value2());
 
283
                                                                approxResult.isSolvedUsingStateEquation());
 
284
                                                toReturn.setNameMapping(transformedModel.value2());
287
285
                                        }
288
286
                                        else {
289
287
                                                // the query contains deadlock, but we do not have a trace.
291
289
                                                queryResult.setApproximationInconclusive(true);
292
290
                                                
293
291
                                                VerificationResult<TimedArcPetriNetTrace> approxResult = result;
294
 
                                                value = new VerificationResult<TAPNNetworkTrace>(
 
292
                                                toReturn = new VerificationResult<TAPNNetworkTrace>(
295
293
                                                                approxResult.getQueryResult(),
296
294
                                                                decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
297
295
                                                                decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
298
296
                                                                approxResult.verificationTime(),
299
297
                                                                approxResult.stats(),
300
 
                                                                approxResult.isOverApproximationResult());
301
 
                                                value.setNameMapping(transformedModel.value2());
 
298
                                                                approxResult.isSolvedUsingStateEquation());
 
299
                                                toReturn.setNameMapping(transformedModel.value2());
302
300
                                        }
303
301
                                }
304
302
                        }
305
303
                } 
306
304
                else {
307
 
                        value =  new VerificationResult<TAPNNetworkTrace>(
 
305
                        toReturn =  new VerificationResult<TAPNNetworkTrace>(
308
306
                                        result.getQueryResult(),
309
307
                                        decomposeTrace(result.getTrace(), transformedModel.value2(), model),
310
308
                                        decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
311
309
                                        result.verificationTime(),
312
310
                                        result.stats(),
313
 
                                        result.isOverApproximationResult());
314
 
                        value.setNameMapping(transformedModel.value2());
 
311
                                        result.isSolvedUsingStateEquation());
 
312
                        toReturn.setNameMapping(transformedModel.value2());
315
313
                }
316
314
                
317
315
                options.setTraceOption(oldTraceOption);
318
316
                // if the old traceoption was none, we need to set the results traces to null so GUI doesn't try to display the traces later
319
317
                if (oldTraceOption == TraceOption.NONE){
320
 
                        value.setTrace(null);
321
 
                        value.setSecondaryTrace(null);
 
318
                        toReturn.setTrace(null);
 
319
                        toReturn.setSecondaryTrace(null);
322
320
                }
323
321
                
324
 
                return value;
 
322
                return toReturn;
325
323
        }
326
324
 
327
 
        public VerificationResult<TimedArcPetriNetTrace> batchWorker(Tuple<TimedArcPetriNet, NameMapping> composedModel,
328
 
                        VerificationOptions options, pipe.dataLayer.TAPNQuery query, LoadedBatchProcessingModel model,
329
 
                        ModelChecker modelChecker, TAPNQuery queryToVerify, TAPNQuery clonedQuery, BatchProcessingWorker verificationBase) throws Exception {
 
325
        public VerificationResult<TimedArcPetriNetTrace> batchWorker(
 
326
                        Tuple<TimedArcPetriNet, NameMapping> composedModel,
 
327
                        VerificationOptions options,
 
328
                        pipe.dataLayer.TAPNQuery query,
 
329
                        LoadedBatchProcessingModel model,
 
330
                        ModelChecker modelChecker,
 
331
                        TAPNQuery queryToVerify,
 
332
                        TAPNQuery clonedQuery,
 
333
                        BatchProcessingWorker verificationBase
 
334
        ) throws Exception {
330
335
                InclusionPlaces oldInclusionPlaces = null;
331
336
                if (options instanceof VerifyTAPNOptions)
332
337
                        oldInclusionPlaces = ((VerifyTAPNOptions) options).inclusionPlaces();
370
375
                                        verificationResult.getSecondaryTrace(),
371
376
                                        verificationResult.verificationTime(),
372
377
                                        verificationResult.stats(),
373
 
                                        verificationResult.isOverApproximationResult());
 
378
                                        verificationResult.isSolvedUsingStateEquation());
374
379
                                value.setNameMapping(composedModel.value2());
375
380
                } else {
376
381
                    // If r > 1
385
390
                                    decomposeTrace(approxResult.getSecondaryTrace(), composedModel.value2(), model.network()),
386
391
                                    approxResult.verificationTime(),
387
392
                                    approxResult.stats(),
388
 
                                                        verificationResult.isOverApproximationResult());
 
393
                                                        verificationResult.isSolvedUsingStateEquation());
389
394
                        valueNetwork.setNameMapping(composedModel.value2());
390
395
                        
391
396
                        OverApproximation overaprx = new OverApproximation();
401
406
                        //run model checker again for trace TAPN
402
407
                        MemoryMonitor.cumulateMemory();
403
408
                        verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
404
 
                        if (verificationBase.isCancelled()) {
405
 
                                verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
406
 
                        }
 
409
 
407
410
                        if (verificationResult.error()) {
408
411
                                options.setTraceOption(oldTraceOption);
409
412
                            return new VerificationResult<TimedArcPetriNetTrace>(
428
431
                                approxResult.getSecondaryTrace(),
429
432
                                approxResult.verificationTime() + verificationResult.verificationTime(),
430
433
                                approxResult.stats(),
431
 
                                                verificationResult.isOverApproximationResult());
 
434
                                                verificationResult.isSolvedUsingStateEquation());
432
435
                        value.setNameMapping(composedModel.value2());
433
436
                    }
434
437
                                else if (((verificationResult.getQueryResult().queryType() == QueryType.EF || verificationResult.getQueryResult().queryType() == QueryType.EG) && !verificationResult.getQueryResult().isQuerySatisfied())
447
450
                                                verificationResult.getSecondaryTrace(),
448
451
                                                verificationResult.verificationTime(),
449
452
                                                verificationResult.stats(),
450
 
                                                verificationResult.isOverApproximationResult());
 
453
                                                verificationResult.isSolvedUsingStateEquation());
451
454
                                    value.setNameMapping(composedModel.value2());
452
455
                    }
453
456
                                else {
463
466
                                                verificationResult.getSecondaryTrace(),
464
467
                                                verificationResult.verificationTime(),
465
468
                                                verificationResult.stats(),
466
 
                                                verificationResult.isOverApproximationResult());
 
469
                                                verificationResult.isSolvedUsingStateEquation());
467
470
                                    value.setNameMapping(composedModel.value2());
468
471
                                        
469
472
                                }
482
485
                    verificationResult.getSecondaryTrace(),
483
486
                    verificationResult.verificationTime(),
484
487
                    verificationResult.stats(),
485
 
                                        verificationResult.isOverApproximationResult());
 
488
                                        verificationResult.isSolvedUsingStateEquation());
486
489
                value.setNameMapping(composedModel.value2());
487
490
                }
488
491
                else {
499
502
                            verificationResult.getSecondaryTrace(),
500
503
                            verificationResult.verificationTime(),
501
504
                            verificationResult.stats(),
502
 
                                                verificationResult.isOverApproximationResult());
 
505
                                                verificationResult.isSolvedUsingStateEquation());
503
506
                    value.setNameMapping(composedModel.value2());
504
507
                            
505
 
                                } else if ((verificationResult.getQueryResult().queryType() == QueryType.EF || verificationResult.getQueryResult().queryType() == QueryType.EG) && verificationResult.getQueryResult().isQuerySatisfied()
 
508
                                }
 
509
                                else if ((verificationResult.getQueryResult().queryType() == QueryType.EF || verificationResult.getQueryResult().queryType() == QueryType.EG) && verificationResult.getQueryResult().isQuerySatisfied()
506
510
                                                || ((verificationResult.getQueryResult().queryType() == QueryType.AG || verificationResult.getQueryResult().queryType() == QueryType.AF) && ! verificationResult.getQueryResult().isQuerySatisfied())) {
507
511
                                        // ((EF OR EG) AND satisfied) OR ((AG OR AF) and not satisfied) -> Check for deadlock
508
512
                            
516
520
                                decomposeTrace(approxResult.getSecondaryTrace(), composedModel.value2(), model.network()),
517
521
                                approxResult.verificationTime(),
518
522
                                approxResult.stats(),
519
 
                                approxResult.isOverApproximationResult());
 
523
                                approxResult.isSolvedUsingStateEquation());
520
524
                            valueNetwork.setNameMapping(composedModel.value2());
521
525
                            
522
526
                            OverApproximation overaprx = new OverApproximation();
531
535
                            //run model checker again for trace TAPN
532
536
                            MemoryMonitor.cumulateMemory();
533
537
                            verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
534
 
                            if (verificationBase.isCancelled()) {
535
 
                                verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
536
 
                            }
 
538
 
537
539
                            if (verificationResult.error()) {
538
540
                                options.setTraceOption(oldTraceOption);
539
541
                                                return new VerificationResult<TimedArcPetriNetTrace>(
562
564
                                    verificationResult.getSecondaryTrace(),
563
565
                                    verificationResult.verificationTime() + approxResult.verificationTime(),
564
566
                                    verificationResult.stats(),
565
 
                                                        verificationResult.isOverApproximationResult());
 
567
                                                        verificationResult.isSolvedUsingStateEquation());
566
568
                            value.setNameMapping(composedModel.value2());
567
569
                        }
568
570
                        else {
576
578
                                                        verificationResult.getSecondaryTrace(),
577
579
                                                        verificationResult.verificationTime(),
578
580
                                                        verificationResult.stats(),
579
 
                                                        verificationResult.isOverApproximationResult());
 
581
                                                        verificationResult.isSolvedUsingStateEquation());
580
582
                                            value.setNameMapping(composedModel.value2());
581
583
                        }
582
584
                    }
583
585
                }
584
 
            } else {
 
586
            }
 
587
            else {
585
588
                value =  new VerificationResult<TimedArcPetriNetTrace>(
586
589
                        verificationResult.getQueryResult(),
587
590
                        verificationResult.getTrace(),
588
591
                        verificationResult.getSecondaryTrace(),
589
592
                        verificationResult.verificationTime(),
590
593
                        verificationResult.stats(),
591
 
                                        verificationResult.isOverApproximationResult());
 
594
                                        verificationResult.isSolvedUsingStateEquation());
592
595
                value.setNameMapping(composedModel.value2());
593
596
            }
594
597