← Back to branch summary

~tapaal-contributor/tapaal/disappearing-tokens-1940098

« back to all changes in this revision

Viewing changes to src/pipe/gui/RunVerificationBase.java

  • Committer: Kenneth Yrke Jørgensen
  • Date: 2011-04-12 09:50:16 UTC
  • mfrom: (329.1.188 tapaal-1.5)
  • Revision ID: mail@yrke.dk-20110412095016-e4hqdgab5596ja09
Merged with branch addning support for new 1.5 features

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/RunVerificationBase.java
5
5
import javax.swing.SwingWorker;
6
6
 
7
7
import dk.aau.cs.Messenger;
8
 
import dk.aau.cs.petrinet.TAPNQuery;
9
 
import dk.aau.cs.petrinet.TimedArcPetriNet;
 
8
import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor;
 
9
import dk.aau.cs.model.tapn.TAPNQuery;
 
10
import dk.aau.cs.model.tapn.TimedArcPetriNet;
 
11
import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
 
12
import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
 
13
import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
 
14
import dk.aau.cs.util.Tuple;
10
15
import dk.aau.cs.verification.ModelChecker;
 
16
import dk.aau.cs.verification.NameMapping;
 
17
import dk.aau.cs.verification.TAPNComposer;
 
18
import dk.aau.cs.verification.TAPNTraceDecomposer;
11
19
import dk.aau.cs.verification.VerificationOptions;
12
20
import dk.aau.cs.verification.VerificationResult;
13
21
 
14
 
public abstract class RunVerificationBase extends
15
 
                SwingWorker<VerificationResult, Void> {
 
22
public abstract class RunVerificationBase extends SwingWorker<VerificationResult<TAPNNetworkTrace>, Void> {
16
23
 
17
24
        private ModelChecker modelChecker;
18
 
        protected VerificationOptions options;
19
 
        private TimedArcPetriNet model;
20
 
        protected TAPNQuery query;
 
25
 
 
26
        private VerificationOptions options;
 
27
        private TimedArcPetriNetNetwork model;
 
28
        private TAPNQuery query;
 
29
 
21
30
        protected Messenger messenger;
22
 
        
 
31
 
23
32
        public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) {
24
33
                super();
25
34
                this.modelChecker = modelChecker;
26
35
                this.messenger = messenger;
27
36
        }
28
 
        
29
 
        public void execute(VerificationOptions options, TimedArcPetriNet model, TAPNQuery query){
 
37
 
 
38
        public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query) {
30
39
                this.model = model;
31
40
                this.options = options;
32
41
                this.query = query;
33
42
                execute();
34
43
        }
35
 
        
36
 
        @Override
37
 
        protected VerificationResult doInBackground() throws Exception {
38
 
                VerificationResult result = modelChecker.verify(options, model, query);
39
 
                return result;
40
 
        }
41
 
        
42
 
        @Override
43
 
        protected void done() {                                         
44
 
                if(!isCancelled()){
45
 
                        VerificationResult result = null;
 
44
 
 
45
        @Override
 
46
        protected VerificationResult<TAPNNetworkTrace> doInBackground() throws Exception {
 
47
                TAPNComposer composer = new TAPNComposer();
 
48
                Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(model);
 
49
 
 
50
                TAPNQuery clonedQuery = new TAPNQuery(query.getProperty().copy(), query.getExtraTokens());
 
51
                MapQueryToNewNames(clonedQuery, transformedModel.value2());
 
52
 
 
53
                VerificationResult<TimedArcPetriNetTrace> result = modelChecker.verify(options, transformedModel, clonedQuery);
 
54
                if (result.error()) {
 
55
                        return new VerificationResult<TAPNNetworkTrace>(result.errorMessage());
 
56
                } else {
 
57
                        return new VerificationResult<TAPNNetworkTrace>(
 
58
                                        result.getQueryResult(),
 
59
                                        decomposeTrace(result.getTrace(), transformedModel.value2()),
 
60
                                        result.verificationTime());
 
61
                }
 
62
        }
 
63
 
 
64
        private TAPNNetworkTrace decomposeTrace(TimedArcPetriNetTrace trace, NameMapping mapping) {
 
65
                if (trace == null)
 
66
                        return null;
 
67
 
 
68
                TAPNTraceDecomposer decomposer = new TAPNTraceDecomposer(trace, model, mapping);
 
69
                return decomposer.decompose();
 
70
        }
 
71
 
 
72
        private void MapQueryToNewNames(TAPNQuery query, NameMapping mapping) {
 
73
                RenameAllPlacesVisitor visitor = new RenameAllPlacesVisitor(mapping);
 
74
                query.getProperty().accept(visitor, null);
 
75
        }
 
76
 
 
77
        @Override
 
78
        protected void done() {
 
79
                if (!isCancelled()) {
 
80
                        VerificationResult<TAPNNetworkTrace> result = null;
 
81
 
46
82
                        try {
47
83
                                result = get();
48
84
                        } catch (InterruptedException e) {
50
86
                        } catch (ExecutionException e) {
51
87
                                e.printStackTrace();
52
88
                        }
53
 
                        
 
89
 
54
90
                        showResult(result, result.verificationTime());
55
 
                }else{
56
 
                        modelChecker.kill();                    
57
 
                        messenger.displayInfoMessage("Verification was interupted by the user. No result found!",
58
 
                                        "Verification Cancelled");
 
91
 
 
92
                } else {
 
93
                        modelChecker.kill();
 
94
                        messenger.displayInfoMessage("Verification was interupted by the user. No result found!", "Verification Cancelled");
 
95
 
59
96
                }
60
97
        }
61
98
 
62
 
        protected abstract void showResult(VerificationResult result, long verificationTime);
 
99
        protected abstract void showResult(VerificationResult<TAPNNetworkTrace> result, long verificationTime);
63
100
}
 
 
b'\\ No newline at end of file'