← Back to branch summary

~tapaal-contributor/tapaal/unselect-objects-after-undo-1894108

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.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/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java
42
42
import pipe.gui.widgets.InclusionPlaces.InclusionPlacesOption;
43
43
 
44
44
public class VerifyTAPNDiscreteVerification implements ModelChecker{
45
 
        
 
45
 
46
46
        private static final String NEED_TO_LOCATE_VERIFYDTAPN_MSG = "TAPAAL needs to know the location of the file verifydtapn.\n\n"
47
47
                        + "Verifydtapn is a part of the TAPAAL distribution and it is\n"
48
48
                        + "normally located in the directory lib.";
49
 
                
50
 
                protected static String verifydtapnpath = "";
51
 
                
52
 
                private FileFinder fileFinder;
53
 
                private Messenger messenger;
54
 
 
55
 
                private ProcessRunner runner;
56
 
                
57
 
                public VerifyTAPNDiscreteVerification(FileFinder fileFinder, Messenger messenger) {
58
 
                        this.fileFinder = fileFinder;
59
 
                        this.messenger = messenger;
60
 
                }
61
 
                
62
 
                public boolean supportsStats(){
 
49
 
 
50
        protected static String verifydtapnpath = "";
 
51
 
 
52
        private FileFinder fileFinder;
 
53
        private Messenger messenger;
 
54
 
 
55
        private ProcessRunner runner;
 
56
 
 
57
        public VerifyTAPNDiscreteVerification(FileFinder fileFinder, Messenger messenger) {
 
58
                this.fileFinder = fileFinder;
 
59
                this.messenger = messenger;
 
60
        }
 
61
 
 
62
        public boolean supportsStats() {
 
63
                return true;
 
64
        }
 
65
 
 
66
        public String getStatsExplanation() {
 
67
                StringBuilder buffer = new StringBuilder("<html>");
 
68
                buffer.append("<b>Discovered markings:</b> The number of found markings (each<br />");
 
69
                buffer.append("time a successor is calculated, this number is incremented)<br/>");
 
70
                buffer.append("<br/>");
 
71
                buffer.append("<b>Explored markings:</b> The number of markings taken out<br/>");
 
72
                buffer.append("of the waiting list during the search.<br />");
 
73
                buffer.append("<br/>");
 
74
                buffer.append("<b>Stored markings:</b> The number of markings found in the<br />");
 
75
                buffer.append("passed/waiting list at the end of verification.<br />");
 
76
                buffer.append("</html>");
 
77
                return buffer.toString();
 
78
        }
 
79
 
 
80
        public String getPath() {
 
81
                return verifydtapnpath;
 
82
        }
 
83
 
 
84
        public String getVersion() {
 
85
                String result = null;
 
86
 
 
87
                if (!isNotSetup()) {
 
88
                        String[] commands;
 
89
                        commands = new String[]{verifydtapnpath, "-v"};
 
90
 
 
91
                        InputStream stream = null;
 
92
                        try {
 
93
                                Process child = Runtime.getRuntime().exec(commands);
 
94
                                stream = child.getInputStream();
 
95
                                if (stream != null) {
 
96
                                        result = readVersionNumberFrom(stream);
 
97
                                }
 
98
                                child.waitFor();
 
99
                        } catch (IOException | InterruptedException e) {
 
100
                        }
 
101
                }
 
102
 
 
103
                return result;
 
104
        }
 
105
 
 
106
        private String readVersionNumberFrom(InputStream stream) {
 
107
                String result = null;
 
108
                BufferedReader bufferedReader = new BufferedReader(new InputStreamReader(stream));
 
109
 
 
110
                String versioninfo = null;
 
111
                try {
 
112
                        versioninfo = bufferedReader.readLine();
 
113
                        while (bufferedReader.readLine() != null) {
 
114
                        }    // Empty buffer
 
115
                } catch (IOException e) {
 
116
                        result = null;
 
117
                }
 
118
 
 
119
                Pattern pattern = Pattern.compile("^VerifyDTAPN (\\d+\\.\\d+\\.\\d+)$");
 
120
                Matcher m = pattern.matcher(versioninfo);
 
121
                m.find();
 
122
                result = m.group(1);
 
123
                return result;
 
124
        }
 
125
 
 
126
        public boolean isCorrectVersion() {
 
127
                if (isNotSetup()) {
 
128
                        return false;
 
129
                }
 
130
 
 
131
                File file = new File(getPath());
 
132
                if (!file.canExecute()) {
 
133
                        messenger.displayErrorMessage("The engine verifydtapn is not executable.\n"
 
134
                                        + "The verifydtapn path will be reset. Please try again, "
 
135
                                        + "to manually set the verifydtapn path.", "Verifydtapn Error");
 
136
                        resetVerifytapn();
 
137
                        return false;
 
138
                }
 
139
 
 
140
                if (getVersion() != null) {
 
141
 
 
142
                        String[] version = getVersion().split("\\.");
 
143
                        String[] targetversion = Pipe.verifydtapnMinRev.split("\\.");
 
144
 
 
145
                        for (int i = 0; i < targetversion.length; i++) {
 
146
                                if (version.length < i + 1) version[i] = "0";
 
147
                                int diff = Integer.parseInt(version[i]) - Integer.parseInt(targetversion[i]);
 
148
                                if (diff > 0) {
 
149
                                        break;
 
150
                                } else if (diff < 0) {
 
151
                                        return false;
 
152
                                }
 
153
                        }
 
154
 
63
155
                        return true;
64
 
                }
65
 
                
66
 
                public String getStatsExplanation(){
67
 
                        StringBuffer buffer = new StringBuffer("<html>");
68
 
                        buffer.append("<b>Discovered markings:</b> The number of found markings (each<br />");
69
 
                        buffer.append("time a successor is calculated, this number is incremented)<br/>");
70
 
                        buffer.append("<br/>");
71
 
                        buffer.append("<b>Explored markings:</b> The number of markings taken out<br/>");
72
 
                        buffer.append("of the waiting list during the search.<br />");
73
 
                        buffer.append("<br/>");
74
 
                        buffer.append("<b>Stored markings:</b> The number of markings found in the<br />");
75
 
                        buffer.append("passed/waiting list at the end of verification.<br />");
76
 
                        buffer.append("</html>");
77
 
                        return buffer.toString();
78
 
                }
79
 
                
80
 
                public String getPath() {
81
 
                        return verifydtapnpath;
82
 
                }
83
 
 
84
 
                public String getVersion() {
85
 
                        String result = null;
86
 
 
87
 
                        if (!isNotSetup()) {
88
 
                                String[] commands;
89
 
                                commands = new String[] { verifydtapnpath, "-v" };
90
 
 
91
 
                                InputStream stream = null;
92
 
                                try {
93
 
                                        Process child = Runtime.getRuntime().exec(commands);
94
 
                                        stream = child.getInputStream();
95
 
                                        if (stream != null) {
96
 
                                                result = readVersionNumberFrom(stream);
97
 
                                        }
98
 
                                        child.waitFor();
99
 
                                } catch (IOException e) {
100
 
                                } catch (InterruptedException e) {
101
 
                                }
102
 
                        }
103
 
 
104
 
                        return result;
105
 
                }
106
 
 
107
 
                private String readVersionNumberFrom(InputStream stream) {
108
 
                        String result = null;
109
 
                        BufferedReader bufferedReader = new BufferedReader(new InputStreamReader(stream));
110
 
 
111
 
                        String versioninfo = null;
 
156
                } else {
 
157
                        return false;
 
158
                }
 
159
        }
 
160
 
 
161
        private void resetVerifytapn() {
 
162
                verifydtapnpath = null;
 
163
                Preferences.getInstance().setVerifydtapnLocation(null);
 
164
        }
 
165
 
 
166
 
 
167
        public void kill() {
 
168
                if (runner != null) {
 
169
                        runner.kill();
 
170
                }
 
171
        }
 
172
 
 
173
        public void setPath(String path) throws IllegalArgumentException {
 
174
                ExecutabilityChecker.check(path);
 
175
                String oldPath = verifydtapnpath;
 
176
                verifydtapnpath = path;
 
177
                Preferences.getInstance().setVerifydtapnLocation(path);
 
178
                if (!isCorrectVersion()) {
 
179
                        messenger.displayErrorMessage("The specified version of the file verifydtapn is too old.", "Verifydtapn Error");
 
180
                        verifydtapnpath = oldPath;
 
181
                        Preferences.getInstance().setVerifydtapnLocation(oldPath);
 
182
                }
 
183
        }
 
184
 
 
185
        public boolean setup() {
 
186
                if (isNotSetup()) {
 
187
                        messenger.displayInfoMessage(NEED_TO_LOCATE_VERIFYDTAPN_MSG, "Locate verifydtapn");
 
188
 
112
189
                        try {
113
 
                                versioninfo = bufferedReader.readLine();
114
 
                                while(bufferedReader.readLine() != null){}      // Empty buffer
115
 
                        } catch (IOException e) {
116
 
                                result = null;
117
 
                        }
118
 
 
119
 
                        Pattern pattern = Pattern.compile("^VerifyDTAPN (\\d+\\.\\d+\\.\\d+)$");
120
 
                        Matcher m = pattern.matcher(versioninfo);
121
 
                        m.find();
122
 
                        result = m.group(1);
123
 
                        return result;
124
 
                }
125
 
 
126
 
                public boolean isCorrectVersion() {
127
 
                        if (isNotSetup()) {
128
 
                                return false;
129
 
                        }
130
 
 
131
 
                        File file = new File(getPath());
132
 
                        if (!file.canExecute()) {
133
 
                                messenger.displayErrorMessage("The engine verifydtapn is not executable.\n"
134
 
                                                + "The verifydtapn path will be reset. Please try again, "
135
 
                                                + "to manually set the verifydtapn path.", "Verifydtapn Error");
136
 
                                resetVerifytapn();
137
 
                                return false;
138
 
                        }
139
 
 
140
 
                        if (getVersion() != null) {
141
 
 
142
 
                                String[] version = getVersion().split("\\.");
143
 
                                String[] targetversion = Pipe.verifydtapnMinRev.split("\\.");
144
 
 
145
 
                                for (int i = 0; i < targetversion.length; i++) {
146
 
                                        if (version.length < i + 1) version[i] = "0";
147
 
                                        int diff = Integer.parseInt(version[i]) - Integer.parseInt(targetversion[i]);
148
 
                                        if (diff > 0) {
149
 
                                                break;
150
 
                                        } else if (diff < 0) {
151
 
                                                return false;
 
190
                                File file = fileFinder.ShowFileBrowserDialog("Verifydtapn", "", System.getProperty("user.home"));
 
191
                                if (file != null) {
 
192
                                        if (file.getName().matches("^verifydtapn.*(?:\\.exe)?$")) {
 
193
                                                setPath(file.getAbsolutePath());
 
194
                                        } else {
 
195
                                                messenger.displayErrorMessage("The selected executable does not seem to be verifydtapn.");
152
196
                                        }
153
197
                                }
154
198
 
 
199
                        } catch (Exception e) {
 
200
                                messenger.displayErrorMessage("There were errors performing the requested action:\n" + e.getMessage(), "Error");
 
201
                        }
 
202
 
 
203
                }
 
204
 
 
205
                return !isNotSetup();
 
206
        }
 
207
 
 
208
        private boolean isNotSetup() {
 
209
                return verifydtapnpath == null || verifydtapnpath.equals("") || !(new File(verifydtapnpath).exists());
 
210
        }
 
211
 
 
212
        public static boolean trySetup() {
 
213
 
 
214
                String verifydtapn;
 
215
 
 
216
                //If env is set, it overwrites the value
 
217
                verifydtapn = System.getenv("verifydtapn");
 
218
                if (verifydtapn != null && !verifydtapn.isEmpty()) {
 
219
                        if (new File(verifydtapn).exists()) {
 
220
                                verifydtapnpath = verifydtapn;
 
221
                                VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinder(), new MessengerImpl());
 
222
                                if (v.isCorrectVersion()) {
 
223
                                        return true;
 
224
                                } else {
 
225
                                        verifydtapnpath = null;
 
226
                                }
 
227
                        }
 
228
                }
 
229
 
 
230
                //If pref is set
 
231
                verifydtapn = Preferences.getInstance().getVerifydtapnLocation();
 
232
                if (verifydtapn != null && !verifydtapn.isEmpty()) {
 
233
                        verifydtapnpath = verifydtapn;
 
234
                        VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinder(), new MessengerImpl());
 
235
                        if (v.isCorrectVersion()) {
155
236
                                return true;
156
237
                        } else {
157
 
                                return false;
158
 
                        }
159
 
                }
160
 
 
161
 
                private void resetVerifytapn() {
162
 
                        verifydtapnpath = null; 
163
 
                        Preferences.getInstance().setVerifydtapnLocation(null);
164
 
                }
165
 
 
166
 
 
167
 
                public void kill() {
168
 
                        if (runner != null) {
169
 
                                runner.kill();
170
 
                        }
171
 
                }
172
 
                
173
 
                public void setPath(String path) throws IllegalArgumentException{
174
 
                        ExecutabilityChecker.check(path);
175
 
                        String oldPath = verifydtapnpath;
176
 
                        verifydtapnpath = path;
177
 
                        Preferences.getInstance().setVerifydtapnLocation(path);
178
 
                        if(!isCorrectVersion()){
179
 
                                messenger
180
 
                                .displayErrorMessage(
181
 
                                                "The specified version of the file verifydtapn is too old.", "Verifydtapn Error");
182
 
                                verifydtapnpath = oldPath;
183
 
                                Preferences.getInstance().setVerifydtapnLocation(oldPath);
184
 
                        }
185
 
                }
186
 
 
187
 
                public boolean setup() {
188
 
                        if (isNotSetup()) {
189
 
                                messenger.displayInfoMessage(NEED_TO_LOCATE_VERIFYDTAPN_MSG, "Locate verifydtapn");
190
 
 
191
 
                                try {
192
 
                                        File file = fileFinder.ShowFileBrowserDialog("Verifydtapn", "",System.getProperty("user.home"));
193
 
                                        if(file != null){
194
 
                                                if(file.getName().matches("^verifydtapn.*(?:\\.exe)?$")){
195
 
                                                        setPath(file.getAbsolutePath());
196
 
                                                }else{
197
 
                                                        messenger.displayErrorMessage("The selected executable does not seem to be verifydtapn.");
198
 
                                                }
199
 
                                        }
200
 
 
201
 
                                } catch (Exception e) {
202
 
                                        messenger.displayErrorMessage("There were errors performing the requested action:\n" + e.getMessage(), "Error");
203
 
                                }
204
 
 
205
 
                        }
206
 
 
207
 
                        return !isNotSetup();
208
 
                }
209
 
 
210
 
                private boolean isNotSetup() {
211
 
                        return verifydtapnpath == null || verifydtapnpath.equals("") || !(new File(verifydtapnpath).exists());
212
 
                }
213
 
                
214
 
                public static boolean trySetup() {
215
 
 
216
 
                                String verifydtapn = null;
217
 
 
218
 
                                //If env is set, it overwrites the value
219
 
                                verifydtapn = System.getenv("verifydtapn");
220
 
                                if (verifydtapn != null && !verifydtapn.isEmpty()) {
221
 
                                        if (new File(verifydtapn).exists()){
222
 
                                                verifydtapnpath = verifydtapn;
223
 
                                                VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinder(), new MessengerImpl());
224
 
                                                if(v.isCorrectVersion()){
225
 
                                                        return true;
226
 
                                                }else{
227
 
                                                        verifydtapn = null;
228
 
                                                        verifydtapnpath = null;
229
 
                                                }
230
 
                                        }
231
 
                                }
232
 
 
233
 
                                //If pref is set
234
 
                                verifydtapn = Preferences.getInstance().getVerifydtapnLocation();
235
 
                                if (verifydtapn != null && !verifydtapn.isEmpty()) {
236
 
                                        verifydtapnpath = verifydtapn;
237
 
                                        VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinder(), new MessengerImpl());
238
 
                                        if(v.isCorrectVersion()){
239
 
                                                return true;
240
 
                                        }else{
241
 
                                                verifydtapn = null;
242
 
                                                verifydtapnpath = null;
243
 
                                        }
244
 
                                }
245
 
 
246
 
                                //Search the installdir for verifytapn
247
 
                                File installdir = TAPAAL.getInstallDir();
248
 
 
249
 
                                String[] paths = {"/bin/verifydtapn", "/bin/verifydtapn64", "/bin/verifydtapn.exe", "/bin/verifydtapn64.exe"};
250
 
                                for (String s : paths) {
251
 
                                        File verifydtapnfile = new File(installdir + s);
252
 
 
253
 
                                        if (verifydtapnfile.exists()){
254
 
 
255
 
                                                verifydtapnpath = verifydtapnfile.getAbsolutePath();
256
 
                                                VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinder(), new MessengerImpl());
257
 
                                                if(v.isCorrectVersion()){
258
 
                                                        return true;
259
 
                                                }else{
260
 
                                                        verifydtapn = null;
261
 
                                                        verifydtapnpath = null;
262
 
                                                }
263
 
 
264
 
                                        }
265
 
                                }
266
 
 
267
 
 
268
 
                                return false;
269
 
 
270
 
                }
271
 
 
272
 
                public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query) throws Exception {    
273
 
                        if(!supportsModel(model.value1(), options)){
274
 
                                throw new UnsupportedModelException("Verifydtapn does not support the given model.");
275
 
                        }
276
 
                        
277
 
            if(!supportsQuery(model.value1(), query, options)){
278
 
                throw new UnsupportedQueryException("Verifydtapn does not support the given query-option combination. ");
279
 
            }
280
 
                        //if(!supportsQuery(model.value1(), query, options))
281
 
                                //throw new UnsupportedQueryException("Verifydtapn does not support the given query.");
282
 
                        
283
 
//                      if(((VerifyTAPNOptions)options).discreteInclusion() && !isQueryUpwardClosed(query))
284
 
//                              throw new UnsupportedQueryException("Discrete inclusion check only supports upward closed queries.");
285
 
                        
286
 
                        if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
287
 
                        
288
 
                        VerifyTAPNExporter exporter = new VerifyTAPNExporter();
289
 
                        ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query);
290
 
 
291
 
                        if (exportedModel == null) {
292
 
                                messenger.displayErrorMessage("There was an error exporting the model");
293
 
                        }
294
 
 
295
 
                        return verify(options, model, exportedModel, query);
296
 
                }
297
 
 
298
 
                private void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
299
 
                        VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions)options;
300
 
                        
301
 
                        if(verificationOptions.inclusionPlaces().inclusionOption() == InclusionPlacesOption.AllPlaces) 
302
 
                                return;
303
 
                        
304
 
                        List<TimedPlace> inclusionPlaces = new ArrayList<TimedPlace>();
305
 
                        for(TimedPlace p : verificationOptions.inclusionPlaces().inclusionPlaces()) {
306
 
                                if(p instanceof LocalTimedPlace) {
307
 
                                        LocalTimedPlace local = (LocalTimedPlace)p;
308
 
                                        if(local.model().isActive()){
309
 
                                                inclusionPlaces.add(model.value1().getPlaceByName(model.value2().map(local.model().name(), local.name())));
310
 
                                        }
311
 
                                }
312
 
                                else // shared place
313
 
                                        inclusionPlaces.add(model.value1().getPlaceByName(model.value2().map("", p.name())));
314
 
                        }
315
 
                        
316
 
                        ((VerifyTAPNOptions)options).setInclusionPlaces(new InclusionPlaces(InclusionPlacesOption.UserSpecified, inclusionPlaces));
317
 
                }
318
 
 
319
 
                private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {
320
 
                        ((VerifyTAPNOptions)options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
321
 
                        runner = new ProcessRunner(verifydtapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
322
 
                        runner.run();
323
 
 
324
 
                        if (runner.error()) {
325
 
                                return null;
 
238
                                verifydtapnpath = null;
 
239
                        }
 
240
                }
 
241
 
 
242
                //Search the installdir for verifytapn
 
243
                File installdir = TAPAAL.getInstallDir();
 
244
 
 
245
                String[] paths = {"/bin/verifydtapn", "/bin/verifydtapn64", "/bin/verifydtapn.exe", "/bin/verifydtapn64.exe"};
 
246
                for (String s : paths) {
 
247
                        File verifydtapnfile = new File(installdir + s);
 
248
 
 
249
                        if (verifydtapnfile.exists()) {
 
250
 
 
251
                                verifydtapnpath = verifydtapnfile.getAbsolutePath();
 
252
                                VerifyTAPNDiscreteVerification v = new VerifyTAPNDiscreteVerification(new FileFinder(), new MessengerImpl());
 
253
                                if (v.isCorrectVersion()) {
 
254
                                        return true;
 
255
                                } else {
 
256
                                        verifydtapnpath = null;
 
257
                                }
 
258
 
 
259
                        }
 
260
                }
 
261
 
 
262
 
 
263
                return false;
 
264
 
 
265
        }
 
266
 
 
267
        public VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, TAPNQuery query) throws Exception {
 
268
                if (!supportsModel(model.value1(), options)) {
 
269
                        throw new UnsupportedModelException("Verifydtapn does not support the given model.");
 
270
                }
 
271
 
 
272
                if (!supportsQuery(model.value1(), query, options)) {
 
273
                        throw new UnsupportedQueryException("Verifydtapn does not support the given query-option combination. ");
 
274
                }
 
275
                //if(!supportsQuery(model.value1(), query, options))
 
276
                //throw new UnsupportedQueryException("Verifydtapn does not support the given query.");
 
277
 
 
278
                //if(((VerifyTAPNOptions)options).discreteInclusion() && !isQueryUpwardClosed(query))
 
279
                //throw new UnsupportedQueryException("Discrete inclusion check only supports upward closed queries.");
 
280
 
 
281
                if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
 
282
 
 
283
                VerifyTAPNExporter exporter = new VerifyTAPNExporter();
 
284
                ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query);
 
285
 
 
286
                if (exportedModel == null) {
 
287
                        messenger.displayErrorMessage("There was an error exporting the model");
 
288
                }
 
289
 
 
290
                return verify(options, model, exportedModel, query);
 
291
        }
 
292
 
 
293
        private void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
 
294
                VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options;
 
295
 
 
296
                if (verificationOptions.inclusionPlaces().inclusionOption() == InclusionPlacesOption.AllPlaces)
 
297
                        return;
 
298
 
 
299
                List<TimedPlace> inclusionPlaces = new ArrayList<TimedPlace>();
 
300
                for (TimedPlace p : verificationOptions.inclusionPlaces().inclusionPlaces()) {
 
301
                        if (p instanceof LocalTimedPlace) {
 
302
                                LocalTimedPlace local = (LocalTimedPlace) p;
 
303
                                if (local.model().isActive()) {
 
304
                                        inclusionPlaces.add(model.value1().getPlaceByName(model.value2().map(local.model().name(), local.name())));
 
305
                                }
 
306
                        } else { // shared place
 
307
                                inclusionPlaces.add(model.value1().getPlaceByName(model.value2().map("", p.name())));
 
308
                        }
 
309
                }
 
310
 
 
311
                ((VerifyTAPNOptions) options).setInclusionPlaces(new InclusionPlaces(InclusionPlacesOption.UserSpecified, inclusionPlaces));
 
312
        }
 
313
 
 
314
        private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {
 
315
                ((VerifyTAPNOptions) options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
 
316
                runner = new ProcessRunner(verifydtapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
 
317
                runner.run();
 
318
 
 
319
                if (runner.error()) {
 
320
                        return null;
 
321
                } else {
 
322
                        String errorOutput = readOutput(runner.errorOutput());
 
323
                        String standardOutput = readOutput(runner.standardOutput());
 
324
 
 
325
                        Tuple<QueryResult, Stats> queryResult = parseQueryResult(standardOutput, model.value1().marking().size() + query.getExtraTokens(), query.getExtraTokens(), query, model.value1());
 
326
 
 
327
                        if (queryResult == null || queryResult.value1() == null) {
 
328
                                return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
326
329
                        } else {
327
 
                                String errorOutput = readOutput(runner.errorOutput());
328
 
                                String standardOutput = readOutput(runner.standardOutput());
329
 
 
330
 
                                Tuple<QueryResult, Stats> queryResult = parseQueryResult(standardOutput, model.value1().marking().size() + query.getExtraTokens(), query.getExtraTokens(), query, model.value1());
331
 
                                
332
 
                                if (queryResult == null || queryResult.value1() == null) {
333
 
                                        return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
 
330
 
 
331
                                // Parse covered trace
 
332
                                TimedArcPetriNetTrace secondaryTrace = null;
 
333
                                if (queryResult.value2().getCoveredMarking() != null) {
 
334
                                        secondaryTrace = parseTrace((errorOutput.split("Trace:")[2]), options, model, exportedModel, query, queryResult.value1());
 
335
                                }
 
336
 
 
337
                                TimedArcPetriNetTrace tapnTrace = parseTrace(!errorOutput.contains("Trace:") ? errorOutput : (errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1());
 
338
                                return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, secondaryTrace, runner.getRunningTime(), queryResult.value2(), false);
 
339
                        }
 
340
                }
 
341
        }
 
342
 
 
343
        private TimedArcPetriNetTrace parseTrace(String output, VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, QueryResult queryResult) {
 
344
                if (((VerifyTAPNOptions) options).trace() == TraceOption.NONE) return null;
 
345
 
 
346
                VerifyTAPNTraceParser traceParser = new VerifyTAPNTraceParser(model.value1());
 
347
                TimedArcPetriNetTrace trace = traceParser.parseTrace(new BufferedReader(new StringReader(output)));
 
348
 
 
349
                if (trace == null) {
 
350
                        if (((VerifyTAPNOptions) options).trace() != TraceOption.NONE) {
 
351
                                if ((query.getProperty() instanceof TCTLEFNode && !queryResult.isQuerySatisfied()) ||
 
352
                                                (query.getProperty() instanceof TCTLAGNode && queryResult.isQuerySatisfied()) ||
 
353
                                                (query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) ||
 
354
                                                (query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied())) {
 
355
                                        return null;
334
356
                                } else {
335
 
                                        
336
 
                                        // Parse covered trace
337
 
                                        TimedArcPetriNetTrace secondaryTrace = null;
338
 
                                        if(queryResult.value2().getCoveredMarking() != null){
339
 
                                                secondaryTrace = parseTrace((errorOutput.split("Trace:")[2]), options, model, exportedModel, query, queryResult.value1());
340
 
                                        }
341
 
                                        
342
 
                                        TimedArcPetriNetTrace tapnTrace = parseTrace(!errorOutput.contains("Trace:")?errorOutput:(errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1());
343
 
                                        return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, secondaryTrace, runner.getRunningTime(), queryResult.value2(), false); 
 
357
                                        messenger.displayErrorMessage("Verifydtapn cannot generate the requested trace for the model. Try another trace option.");
344
358
                                }
345
359
                        }
346
360
                }
347
 
 
348
 
                private TimedArcPetriNetTrace parseTrace(String output, VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, QueryResult queryResult) {
349
 
                        if (((VerifyTAPNOptions) options).trace() == TraceOption.NONE) return null;
350
 
                        
351
 
                        VerifyTAPNTraceParser traceParser = new VerifyTAPNTraceParser(model.value1());
352
 
                        TimedArcPetriNetTrace trace = traceParser.parseTrace(new BufferedReader(new StringReader(output)));
353
 
                        
354
 
                        if (trace == null) {
355
 
                                if (((VerifyTAPNOptions) options).trace() != TraceOption.NONE) {
356
 
                                        if((query.getProperty() instanceof TCTLEFNode && !queryResult.isQuerySatisfied()) || 
357
 
                                                        (query.getProperty() instanceof TCTLAGNode && queryResult.isQuerySatisfied()) || 
358
 
                                                        (query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) || 
359
 
                                                        (query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied())){
360
 
                                                return null;
361
 
                                        } else{
362
 
                                                messenger.displayErrorMessage("Verifydtapn cannot generate the requested trace for the model. Try another trace option.");
363
 
                                        }
364
 
                                }
365
 
                        } 
366
 
                        return trace;
367
 
                }
368
 
 
369
 
                private String createArgumentString(String modelFile, String queryFile, VerificationOptions options) {
370
 
                        StringBuffer buffer = new StringBuffer(options.toString());
 
361
                return trace;
 
362
        }
 
363
 
 
364
        private String createArgumentString(String modelFile, String queryFile, VerificationOptions options) {
 
365
                StringBuilder buffer = new StringBuilder(options.toString());
 
366
                buffer.append(' ');
 
367
                buffer.append(modelFile);
 
368
                VerifyDTAPNOptions opts = (VerifyDTAPNOptions) options;
 
369
                if (opts.getWorkflowMode() == WorkflowMode.NOT_WORKFLOW || opts.getWorkflowMode() == null) {
371
370
                        buffer.append(' ');
372
 
                        buffer.append(modelFile);
373
 
                        VerifyDTAPNOptions opts = (VerifyDTAPNOptions)options;
374
 
                        if(opts.getWorkflowMode() == WorkflowMode.NOT_WORKFLOW || opts.getWorkflowMode() == null) {
375
 
                            buffer.append(' ');
376
 
                            buffer.append(queryFile);
377
 
                        }
378
 
 
379
 
                        return buffer.toString();
 
371
                        buffer.append(queryFile);
380
372
                }
381
 
                
382
 
                private String readOutput(BufferedReader reader) {
383
 
                        try {
384
 
                                if (!reader.ready())
385
 
                                        return "";
386
 
                        } catch (IOException e1) {
 
373
 
 
374
                return buffer.toString();
 
375
        }
 
376
 
 
377
        private String readOutput(BufferedReader reader) {
 
378
                try {
 
379
                        if (!reader.ready())
387
380
                                return "";
388
 
                        }
389
 
                        StringBuffer buffer = new StringBuffer();
390
 
                        String line = null;
391
 
                        try {
392
 
                                while ((line = reader.readLine()) != null) {
393
 
                                        buffer.append(line);
394
 
                                        buffer.append(System.getProperty("line.separator"));
395
 
                                }
396
 
                        } catch (IOException e) {
397
 
                        }
398
 
 
399
 
                        return buffer.toString();
400
 
                }
401
 
                
402
 
                private Tuple<QueryResult, Stats> parseQueryResult(String output, int totalTokens, int extraTokens, TAPNQuery query, TimedArcPetriNet model) {
403
 
                        VerifyDTAPNOutputParser outputParser = new VerifyDTAPNOutputParser(totalTokens, extraTokens, query);
404
 
                        Tuple<QueryResult, Stats> result = outputParser.parseOutput(output);
405
 
                        return result;
406
 
                }
407
 
                
408
 
                
409
 
                public boolean supportsModel(TimedArcPetriNet model, VerificationOptions options) {
410
 
                        if(model.hasUrgentTransitions() && ((VerifyDTAPNOptions)options).timeDarts()){
411
 
                                return false;
412
 
                        }
413
 
                        
414
 
                        return model.isNonStrict();
415
 
                }
416
 
                
417
 
                public boolean supportsQuery(TimedArcPetriNet model, TAPNQuery query, VerificationOptions options) {
418
 
                        // if liveness, has deadlock proposition and uses timedarts, it is not supported
419
 
                        if((query.getProperty() instanceof TCTLEGNode || query.getProperty() instanceof TCTLAFNode)
420
 
                                && query.hasDeadlock() 
421
 
                                && ((VerifyDTAPNOptions)options).timeDarts()){
422
 
                return false;
423
 
            }
424
 
                        
425
 
                        return true;
426
 
                }
427
 
                
428
 
                // JS: this is not used any more
429
 
                //private boolean isQueryUpwardClosed(TAPNQuery query) {
430
 
                //      UpwardsClosedVisitor visitor = new UpwardsClosedVisitor();
431
 
                //      return visitor.isUpwardClosed(query.getProperty());
432
 
                //}
433
 
 
434
 
                
435
 
                public static void reset() {
436
 
                        //Clear value
437
 
                        verifydtapnpath = "";
438
 
                        Preferences.getInstance().setVerifydtapnLocation(null);
439
 
                        //Set the detault
440
 
                        trySetup();
441
 
                }
442
 
 
443
 
                @Override
444
 
                public String toString() {
445
 
                        return "verifydtapn";
446
 
                }
447
 
                
448
 
                public boolean useDiscreteSemantics() {
449
 
                        return true;
450
 
                }
 
381
                } catch (IOException e1) {
 
382
                        return "";
 
383
                }
 
384
                StringBuilder buffer = new StringBuilder();
 
385
                String line = null;
 
386
                try {
 
387
                        while ((line = reader.readLine()) != null) {
 
388
                                buffer.append(line);
 
389
                                buffer.append(System.getProperty("line.separator"));
 
390
                        }
 
391
                } catch (IOException e) {
 
392
                }
 
393
 
 
394
                return buffer.toString();
 
395
        }
 
396
 
 
397
        private Tuple<QueryResult, Stats> parseQueryResult(String output, int totalTokens, int extraTokens, TAPNQuery query, TimedArcPetriNet model) {
 
398
                VerifyDTAPNOutputParser outputParser = new VerifyDTAPNOutputParser(totalTokens, extraTokens, query);
 
399
                return outputParser.parseOutput(output);
 
400
        }
 
401
 
 
402
 
 
403
        public boolean supportsModel(TimedArcPetriNet model, VerificationOptions options) {
 
404
                if (model.hasUrgentTransitions() && ((VerifyDTAPNOptions) options).timeDarts()) {
 
405
                        return false;
 
406
                }
 
407
 
 
408
                return model.isNonStrict();
 
409
        }
 
410
 
 
411
        public boolean supportsQuery(TimedArcPetriNet model, TAPNQuery query, VerificationOptions options) {
 
412
                // if liveness, has deadlock proposition and uses timedarts, it is not supported
 
413
                if ((query.getProperty() instanceof TCTLEGNode || query.getProperty() instanceof TCTLAFNode)
 
414
                                && query.hasDeadlock()
 
415
                                && ((VerifyDTAPNOptions) options).timeDarts()) {
 
416
                        return false;
 
417
                }
 
418
 
 
419
                return true;
 
420
        }
 
421
 
 
422
        public static void reset() {
 
423
                //Clear value
 
424
                verifydtapnpath = "";
 
425
                Preferences.getInstance().setVerifydtapnLocation(null);
 
426
                //Set the detault
 
427
                trySetup();
 
428
        }
 
429
 
 
430
        @Override
 
431
        public String toString() {
 
432
                return "verifydtapn";
 
433
        }
 
434
 
 
435
        public boolean useDiscreteSemantics() {
 
436
                return true;
 
437
        }
451
438
}