← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/pipe/gui/RunVerification.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/RunVerification.java
5
5
 
6
6
import javax.swing.JOptionPane;
7
7
 
8
 
import pipe.dataLayer.DataLayer;
9
 
import pipe.dataLayer.TAPNTrace;
10
8
import pipe.gui.GuiFrame.GUIMode;
11
9
import dk.aau.cs.Messenger;
12
 
import dk.aau.cs.TCTL.TCTLAFNode;
13
 
import dk.aau.cs.TCTL.TCTLAGNode;
14
 
import dk.aau.cs.TCTL.TCTLEFNode;
15
 
import dk.aau.cs.TCTL.TCTLEGNode;
 
10
import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
16
11
import dk.aau.cs.verification.ModelChecker;
17
12
import dk.aau.cs.verification.VerificationResult;
18
13
 
23
18
        }
24
19
 
25
20
        @Override
26
 
        protected void showResult(VerificationResult result, long verificationTime) {   
27
 
                if(result != null && !result.error()){
 
21
        protected void showResult(VerificationResult<TAPNNetworkTrace> result,
 
22
                        long verificationTime) {
 
23
                if (result != null && !result.error()) {
28
24
                        String satisfaction = result.isQuerySatisfied() ? "satisfied" : "not satisfied";
29
25
                        JOptionPane.showMessageDialog(CreateGui.getApp(), 
30
 
                                        String.format("Property is %1$s.\nEstimated verification time: %2$.2fs", satisfaction, verificationTime/1000.0),
 
26
                                        String.format("Property is %1$s.\nEstimated verification time: %2$.2fs", satisfaction, verificationTime / 1000.0),
31
27
                                        "Verification Result", JOptionPane.INFORMATION_MESSAGE);
32
 
                        
33
 
                        if(result.getTrace() != null){
34
 
                                DataLayer model = CreateGui.getModel();
35
 
                                TraceTransformer interpreter =  model.isUsingColors() ? new ColoredTraceTransformer(model) : new TraceTransformer(model);
36
 
                                TAPNTrace trace = interpreter.interpretTrace(result.getTrace());
 
28
 
 
29
                        if (result.getTrace() != null) {
 
30
                                // DataLayer model = CreateGui.getModel();
 
31
                                // TraceTransformer interpreter = model.isUsingColors() ? new
 
32
                                // ColoredTraceTransformer(model) : new TraceTransformer(model);
 
33
                                // TAPNTrace trace =
 
34
                                // interpreter.interpretTrace(result.getTrace());
37
35
                                CreateGui.getApp().setGUIMode(GUIMode.animation);
38
 
                                CreateGui.getAnimator().SetTrace(trace);
39
 
                        }else if(result.getTrace() == null && shouldFindTrace(result)){
40
 
                                messenger.displayErrorMessage("A trace could not be generated by the chosen verification engine.");
 
36
 
 
37
                                CreateGui.getAnimator().SetTrace(result.getTrace());
 
38
 
41
39
                        }
 
40
 
42
41
                }else{
43
42
                        
44
43
                        //Check if the is something like 
70
69
                        message += "UPPAAL output:\n" + result.errorMessage();
71
70
                        
72
71
                        messenger.displayWrappedErrorMessage(message,"Error during verification");
 
72
 
73
73
                }
74
74
        }
75
75
 
76
 
        private boolean shouldFindTrace(VerificationResult result) {
77
 
                boolean askedForTrace = !options.getOption("trace").equalsIgnoreCase("NONE");
78
 
                boolean queryAllowsTrace = (query.getProperty() instanceof TCTLEFNode && result.isQuerySatisfied()) 
79
 
                        || (query.getProperty() instanceof TCTLEGNode && result.isQuerySatisfied())
80
 
                        || (query.getProperty() instanceof TCTLAGNode && !result.isQuerySatisfied())
81
 
                        || (query.getProperty() instanceof TCTLAFNode && !result.isQuerySatisfied());
82
 
                
83
 
                return askedForTrace && queryAllowsTrace;
84
 
        }
85
76
}
 
 
b'\\ No newline at end of file'