← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/pipe/gui/Verifier.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/pipe/gui/Verifier.java
1
1
package pipe.gui;
2
2
 
3
 
import java.util.HashMap;
4
 
 
5
3
import javax.swing.JOptionPane;
6
4
import javax.swing.JSpinner;
7
5
 
8
6
import dk.aau.cs.verification.VerifyTAPN.*;
9
 
import pipe.dataLayer.DataLayer;
10
7
import pipe.dataLayer.TAPNQuery;
11
8
import pipe.gui.widgets.RunningVerificationDialog;
12
9
import dk.aau.cs.TCTL.TCTLAbstractProperty;
13
 
import dk.aau.cs.model.tapn.TimedArcPetriNet;
14
10
import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
15
11
import dk.aau.cs.translations.ReductionOption;
16
12
import dk.aau.cs.util.VerificationCallback;
33
29
                verifyta.setup();
34
30
                return verifyta;
35
31
        }
36
 
        
 
32
 
37
33
        private static VerifyTAPN getVerifyTAPN() {
38
34
                VerifyTAPN verifytapn = new VerifyTAPN(new FileFinder(), new MessengerImpl());
39
35
                verifytapn.setup();
52
48
                return verifypn;
53
49
        }
54
50
 
55
 
        private static ModelChecker getModelChecker(TAPNQuery query) {
 
51
        public static ModelChecker getModelChecker(TAPNQuery query) {
56
52
                if(query.getReductionOption() == ReductionOption.VerifyTAPN){
57
53
                        return getVerifyTAPN();
58
54
                } else if(query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification){
65
61
                }
66
62
        }
67
63
 
68
 
        public static void analyzeKBound(
69
 
                        TimedArcPetriNetNetwork tapnNetwork, int k, JSpinner tokensControl) {
 
64
        public static void analyzeKBound(TimedArcPetriNetNetwork tapnNetwork, int k, JSpinner tokensControl) {
70
65
                ModelChecker modelChecker;
71
66
                
72
67
                if(tapnNetwork.isUntimed()){
88
83
 
89
84
 
90
85
        public static void runUppaalVerification(TimedArcPetriNetNetwork timedArcPetriNetNetwork, TAPNQuery input) {
91
 
                runUppaalVerification(timedArcPetriNetNetwork, input, false);
92
 
        }
93
 
 
94
 
        private static void runUppaalVerification(TimedArcPetriNetNetwork timedArcPetriNetNetwork, TAPNQuery input,     boolean untimedTrace) {
95
86
                Verifyta verifyta = getVerifyta();
96
87
                if (!verifyta.isCorrectVersion()) {
97
88
                        System.err.println("Verifyta not found, or you are running an old version of Verifyta.\n"
104
95
                VerifytaOptions verifytaOptions = new VerifytaOptions(
105
96
                                input.getTraceOption(),
106
97
                                input.getSearchOption(),
107
 
                                untimedTrace,
 
98
                                false,
108
99
                                input.getReductionOption(),
109
100
                                input.useSymmetry(),
110
101
                                input.useOverApproximation(),
119
110
 
120
111
                if (timedArcPetriNetNetwork != null) {
121
112
                        RunVerificationBase thread = new RunVerification(verifyta, new UppaalIconSelector(), new MessengerImpl());
122
 
                        RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp());
123
 
                        dialog.setupListeners(thread);
 
113
                        RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), thread);
124
114
                        thread.execute(
125
115
                                        verifytaOptions,
126
116
                                        timedArcPetriNetNetwork,
134
124
                                        "Conversion error", JOptionPane.ERROR_MESSAGE);
135
125
                }
136
126
 
137
 
                return;
138
 
        }
139
 
        
140
 
        public static void runVerifyTAPNVerification(TimedArcPetriNetNetwork tapnNetwork, TAPNQuery query) {
141
 
                runVerifyTAPNVerification(tapnNetwork, query, null);            
142
 
        }
143
 
        
144
 
        public static void runVerifyTAPNVerification(TimedArcPetriNetNetwork tapnNetwork, TAPNQuery query, VerificationCallback callback) {
145
 
                runVerifyTAPNVerification(tapnNetwork, query, callback, null);
146
127
        }
147
128
 
148
129
        public static void runVerifyTAPNVerification(
149
130
                        TimedArcPetriNetNetwork tapnNetwork,
150
131
                        TAPNQuery query,
151
 
                        VerificationCallback callback,
152
 
                        HashMap<TimedArcPetriNet, DataLayer> guiModels) {
 
132
                        VerificationCallback callback
 
133
        ) {
153
134
                ModelChecker verifytapn = getModelChecker(query);
154
135
 
155
136
                if (!verifytapn.isCorrectVersion()) {
219
200
                }
220
201
                
221
202
                if (tapnNetwork != null) {
222
 
                        RunVerificationBase thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback, guiModels);
223
 
                        RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp());
224
 
                        dialog.setupListeners(thread);
 
203
                        RunVerificationBase thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback);
 
204
                        RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), thread);
225
205
                        thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound), query);
226
206
                        dialog.setVisible(true);
227
207
                } else {