← Back to branch summary

~verifypn-maintainers/verifypn/u3.1

« back to all changes in this revision

Viewing changes to src/VerifyPN.cpp

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/VerifyPN.cpp
 
1
/* TAPAAL untimed verification engine verifypn 
 
2
 * Copyright (C) 2011-2018  Jonas Finnemann Jensen <jopsen@gmail.com>,
 
3
 *                          Thomas Søndersø Nielsen <primogens@gmail.com>,
 
4
 *                          Lars Kærlund Østergaard <larsko@gmail.com>,
 
5
 *                          Jiri Srba <srba.jiri@gmail.com>,
 
6
 *                          Peter Gjøl Jensen <root@petergjoel.dk>
 
7
 *
 
8
 * CTL Extension
 
9
 *                          Peter Fogh <peter.f1992@gmail.com>
 
10
 *                          Isabella Kaufmann <bellakaufmann93@gmail.com>
 
11
 *                          Tobias Skovgaard Jepsen <tobiasj1991@gmail.com>
 
12
 *                          Lasse Steen Jensen <lassjen88@gmail.com>
 
13
 *                          Søren Moss Nielsen <soren_moss@mac.com>
 
14
 *                          Samuel Pastva <daemontus@gmail.com>
 
15
 *                          Jiri Srba <srba.jiri@gmail.com>
 
16
 *
 
17
 * Stubborn sets, query simplification, siphon-trap property
 
18
 *                          Frederik Meyer Boenneland <sadpantz@gmail.com>
 
19
 *                          Jakob Dyhr <jakobdyhr@gmail.com>
 
20
 *                          Peter Gjøl Jensen <root@petergjoel.dk>
 
21
 *                          Mads Johannsen <mads_johannsen@yahoo.com>
 
22
 *                          Jiri Srba <srba.jiri@gmail.com>
 
23
 * 
 
24
 * This program is free software: you can redistribute it and/or modify
 
25
 * it under the terms of the GNU General Public License as published by
 
26
 * the Free Software Foundation, either version 3 of the License, or
 
27
 * (at your option) any later version.
 
28
 * 
 
29
 * This program is distributed in the hope that it will be useful,
 
30
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
31
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
32
 * GNU General Public License for more details.
 
33
 * 
 
34
 * You should have received a copy of the GNU General Public License
 
35
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
36
 */
 
37
#include <stdio.h>
 
38
#include <string>
 
39
#include <string.h>
 
40
#include <iostream>
 
41
#include <fstream>
 
42
#include <sstream>
 
43
#include <map>
 
44
#include <memory>
 
45
#include <utility>
 
46
#include <functional>
 
47
#ifdef VERIFYPN_MC_Simplification
 
48
#include <thread>
 
49
#include <iso646.h>
 
50
#endif
 
51
 
 
52
#include "PetriEngine/PQL/PQLParser.h"
 
53
#include "PetriEngine/PQL/Contexts.h"
 
54
#include "PetriEngine/Reachability/ReachabilitySearch.h"
 
55
#include "PetriEngine/TAR/TARReachability.h"
 
56
#include "PetriEngine/Reducer.h"
 
57
#include "PetriParse/QueryXMLParser.h"
 
58
#include "PetriParse/QueryBinaryParser.h"
 
59
#include "PetriParse/PNMLParser.h"
 
60
#include "PetriEngine/PetriNetBuilder.h"
 
61
#include "PetriEngine/PQL/PQL.h"
 
62
#include "PetriEngine/options.h"
 
63
#include "PetriEngine/errorcodes.h"
 
64
#include "PetriEngine/STSolver.h"
 
65
#include "PetriEngine/Simplification/Member.h"
 
66
#include "PetriEngine/Simplification/LinearPrograms.h"
 
67
#include "PetriEngine/Simplification/Retval.h"
 
68
 
 
69
#include "CTL/CTLEngine.h"
 
70
#include "PetriEngine/PQL/Expressions.h"
 
71
#include "PetriEngine/Colored/ColoredPetriNetBuilder.h"
 
72
 
 
73
using namespace std;
 
74
using namespace PetriEngine;
 
75
using namespace PetriEngine::PQL;
 
76
using namespace PetriEngine::Reachability;
 
77
 
 
78
ReturnValue contextAnalysis(ColoredPetriNetBuilder& cpnBuilder, PetriNetBuilder& builder, const PetriNet* net, std::vector<std::shared_ptr<Condition> >& queries)
 
79
{
 
80
    //Context analysis
 
81
    ColoredAnalysisContext context(builder.getPlaceNames(), builder.getTransitionNames(), net, cpnBuilder.getUnfoldedPlaceNames(), cpnBuilder.getUnfoldedTransitionNames(), cpnBuilder.isColored());
 
82
    for(auto& q : queries)
 
83
    {
 
84
        q->analyze(context);
 
85
 
 
86
        //Print errors if any
 
87
        if (context.errors().size() > 0) {
 
88
            for (size_t i = 0; i < context.errors().size(); i++) {
 
89
                fprintf(stderr, "Query Context Analysis Error: %s\n", context.errors()[i].toString().c_str());
 
90
            }
 
91
            return ErrorCode;
 
92
        }
 
93
    }
 
94
    return ContinueCode;
 
95
}
 
96
 
 
97
std::vector<std::string> explode(std::string const & s)
 
98
{
 
99
    std::vector<std::string> result;
 
100
    std::istringstream iss(s);
 
101
 
 
102
    for (std::string token; std::getline(iss, token, ','); )
 
103
    {
 
104
        result.push_back(std::move(token));
 
105
        if(result.back().empty()) result.pop_back();
 
106
    }
 
107
 
 
108
    return result;
 
109
}
 
110
 
 
111
ReturnValue parseOptions(int argc, char* argv[], options_t& options)
 
112
{
 
113
    for (int i = 1; i < argc; i++) {
 
114
        if (strcmp(argv[i], "-k") == 0 || strcmp(argv[i], "--k-bound") == 0) {  
 
115
            if (i == argc - 1) {
 
116
                fprintf(stderr, "Missing number after \"%s\"\n", argv[i]);
 
117
                return ErrorCode;
 
118
            }
 
119
            if (sscanf(argv[++i], "%d", &options.kbound) != 1 || options.kbound < 0) {
 
120
                fprintf(stderr, "Argument Error: Invalid number of tokens \"%s\"\n", argv[i]);
 
121
                return ErrorCode;
 
122
            }
 
123
        } else if(strcmp(argv[i], "-s") == 0 || strcmp(argv[i], "--search-strategy") == 0){
 
124
                        if (i==argc-1) {
 
125
                fprintf(stderr, "Missing search strategy after \"%s\"\n\n", argv[i]);
 
126
                                return ErrorCode;                           
 
127
            }
 
128
            char* s = argv[++i];
 
129
            if(strcmp(s, "BestFS") == 0)
 
130
                                options.strategy = HEUR;
 
131
                        else if(strcmp(s, "BFS") == 0)
 
132
                                options.strategy = BFS;
 
133
                        else if(strcmp(s, "DFS") == 0)
 
134
                                options.strategy = DFS;
 
135
                        else if(strcmp(s, "RDFS") == 0)
 
136
                                options.strategy = RDFS;
 
137
                        else if(strcmp(s, "OverApprox") == 0)
 
138
                                options.strategy = OverApprox;
 
139
                        else{
 
140
                                fprintf(stderr, "Argument Error: Unrecognized search strategy \"%s\"\n", s);
 
141
                                return ErrorCode;
 
142
                        }
 
143
        } else if (strcmp(argv[i], "-q") == 0 || strcmp(argv[i], "--query-reduction") == 0) {
 
144
            if (i == argc - 1) {
 
145
                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
 
146
                return ErrorCode;
 
147
            }
 
148
            if (sscanf(argv[++i], "%d", &options.queryReductionTimeout) != 1 || options.queryReductionTimeout < 0) {
 
149
                fprintf(stderr, "Argument Error: Invalid query reduction timeout argument \"%s\"\n", argv[i]);
 
150
                return ErrorCode;
 
151
            }
 
152
        } else if (strcmp(argv[i], "-l") == 0 || strcmp(argv[i], "--lpsolve-timeout") == 0) {
 
153
            if (i == argc - 1) {
 
154
                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
 
155
                return ErrorCode;
 
156
            }
 
157
            if (sscanf(argv[++i], "%d", &options.lpsolveTimeout) != 1 || options.lpsolveTimeout < 0) {
 
158
                fprintf(stderr, "Argument Error: Invalid LPSolve timeout argument \"%s\"\n", argv[i]);
 
159
                return ErrorCode;
 
160
            }
 
161
        } else if (strcmp(argv[i], "-e") == 0 || strcmp(argv[i], "--state-space-exploration") == 0) {
 
162
            options.statespaceexploration = true;
 
163
        } else if (strcmp(argv[i], "-n") == 0 || strcmp(argv[i], "--no-statistics") == 0) {
 
164
            options.printstatistics = false;
 
165
        } else if (strcmp(argv[i], "-t") == 0 || strcmp(argv[i], "--trace") == 0) {
 
166
            options.trace = true;
 
167
        } else if (strcmp(argv[i], "-x") == 0 || strcmp(argv[i], "--xml-queries") == 0) {
 
168
            if (i == argc - 1) {
 
169
                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
 
170
                return ErrorCode;
 
171
            }
 
172
            std::vector<std::string> q = explode(argv[++i]);
 
173
            for(auto& qn : q)
 
174
            {
 
175
                int32_t n;
 
176
                if(sscanf(qn.c_str(), "%d", &n) != 1 || n <= 0)
 
177
                {
 
178
                    std::cerr << "Error in query numbers : " << qn << std::endl;
 
179
                }
 
180
                else
 
181
                {
 
182
                    options.querynumbers.insert(--n);
 
183
                }
 
184
            }
 
185
        } else if (strcmp(argv[i], "-r") == 0 || strcmp(argv[i], "--reduction") == 0) {
 
186
            if (i == argc - 1) {
 
187
                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
 
188
                return ErrorCode;
 
189
            }
 
190
            if (sscanf(argv[++i], "%d", &options.enablereduction) != 1 || options.enablereduction < 0 || options.enablereduction > 3) {
 
191
                fprintf(stderr, "Argument Error: Invalid reduction argument \"%s\"\n", argv[i]);
 
192
                return ErrorCode;
 
193
            }
 
194
            if(options.enablereduction == 3)
 
195
            {
 
196
                options.reductions.clear();
 
197
                std::vector<std::string> q = explode(argv[++i]);
 
198
                for(auto& qn : q)
 
199
                {
 
200
                    int32_t n;
 
201
                    if(sscanf(qn.c_str(), "%d", &n) != 1 || n < 0 || n > 9)
 
202
                    {
 
203
                        std::cerr << "Error in reduction rule choice : " << qn << std::endl;
 
204
                        return ErrorCode;
 
205
                    }
 
206
                    else
 
207
                    {
 
208
                        options.reductions.push_back(n);
 
209
                    }
 
210
                }                
 
211
            }
 
212
        } else if (strcmp(argv[i], "-d") == 0 || strcmp(argv[i], "--reduction-timeout") == 0) {
 
213
            if (i == argc - 1) {
 
214
                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
 
215
                return ErrorCode;
 
216
            }
 
217
            if (sscanf(argv[++i], "%d", &options.reductionTimeout) != 1) {
 
218
                fprintf(stderr, "Argument Error: Invalid reduction timeout argument \"%s\"\n", argv[i]);
 
219
                return ErrorCode;
 
220
            }
 
221
        } else if(strcmp(argv[i], "--seed-offset") == 0) {
 
222
            if (sscanf(argv[++i], "%u", &options.seed_offset) != 1) {
 
223
                fprintf(stderr, "Argument Error: Invalid seed offset argument \"%s\"\n", argv[i]);
 
224
                return ErrorCode;
 
225
            }
 
226
        }  else if(strcmp(argv[i], "-p") == 0 || strcmp(argv[i], "--partial-order-reduction") == 0) {
 
227
            options.stubbornreduction = false;
 
228
        } else if(strcmp(argv[i], "-a") == 0 || strcmp(argv[i], "--siphon-trap") == 0) {
 
229
            if (i == argc - 1) {
 
230
                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
 
231
                return ErrorCode;
 
232
            }
 
233
            if (sscanf(argv[++i], "%u", &options.siphontrapTimeout) != 1) {
 
234
                fprintf(stderr, "Argument Error: Invalid siphon-trap timeout \"%s\"\n", argv[i]);
 
235
                return ErrorCode;
 
236
            }
 
237
        } else if(strcmp(argv[i], "--siphon-depth") == 0) {
 
238
            if (i == argc - 1) {
 
239
                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
 
240
                return ErrorCode;
 
241
            }
 
242
            if (sscanf(argv[++i], "%u", &options.siphonDepth) != 1) {
 
243
                fprintf(stderr, "Argument Error: Invalid siphon-depth count \"%s\"\n", argv[i]);
 
244
                return ErrorCode;
 
245
            }
 
246
        } 
 
247
        else if (strcmp(argv[i], "-tar") == 0)
 
248
        {
 
249
            options.tar = true;
 
250
            
 
251
        }
 
252
        else if (strcmp(argv[i], "--write-simplified") == 0)
 
253
        {
 
254
            options.query_out_file = std::string(argv[++i]);
 
255
        }
 
256
        else if(strcmp(argv[i], "--binary-query-io") == 0)
 
257
        {
 
258
            if (sscanf(argv[++i], "%u", &options.binary_query_io) != 1 || options.binary_query_io > 3) {
 
259
                fprintf(stderr, "Argument Error: Invalid binary-query-io value \"%s\"\n", argv[i]);
 
260
                return ErrorCode;
 
261
            }
 
262
        }
 
263
        else if (strcmp(argv[i], "--write-reduced") == 0)
 
264
        {
 
265
            options.model_out_file = std::string(argv[++i]);
 
266
        }
 
267
#ifdef VERIFYPN_MC_Simplification
 
268
        else if (strcmp(argv[i], "-z") == 0)
 
269
        {
 
270
            if (i == argc - 1) {
 
271
                fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
 
272
                return ErrorCode;
 
273
            }
 
274
            if (sscanf(argv[++i], "%u", &options.cores) != 1) {
 
275
                fprintf(stderr, "Argument Error: Invalid cores count \"%s\"\n", argv[i]);
 
276
                return ErrorCode;
 
277
            }
 
278
        }
 
279
#endif
 
280
        else if (strcmp(argv[i], "-ctl") == 0){
 
281
            if(argc > i + 1){
 
282
                if(strcmp(argv[i + 1], "local") == 0){
 
283
                    options.ctlalgorithm = CTL::Local;
 
284
                }
 
285
                else if(strcmp(argv[i + 1], "czero") == 0){
 
286
                    options.ctlalgorithm = CTL::CZero;
 
287
                }
 
288
                else
 
289
                {
 
290
                    fprintf(stderr, "Argument Error: Invalid ctl-algorithm type \"%s\"\n", argv[i + 1]);
 
291
                    return ErrorCode;
 
292
                }
 
293
                i++;
 
294
 
 
295
            }
 
296
        } else if (strcmp(argv[i], "-g") == 0 || strcmp(argv[i], "--game-mode") == 0){
 
297
            options.gamemode = true;
 
298
        } else if (strcmp(argv[i], "-c") == 0 || strcmp(argv[i], "--cpn-overapproximation") == 0) {
 
299
            options.cpnOverApprox = true;
 
300
        } else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "--help") == 0) {
 
301
            printf("Usage: verifypn [options] model-file query-file\n"
 
302
                    "A tool for answering CTL and reachability queries of place cardinality\n" 
 
303
                    "deadlock and transition fireability for weighted P/T Petri nets\n" 
 
304
                    "extended with inhibitor arcs.\n"
 
305
                    "\n"
 
306
                    "Options:\n"
 
307
                    "  -k, --k-bound <number of tokens>   Token bound, 0 to ignore (default)\n"
 
308
                    "  -t, --trace                        Provide XML-trace to stderr\n"
 
309
                    "  -s, --search-strategy <strategy>   Search strategy:\n"
 
310
                    "                                     - BestFS       Heuristic search (default)\n"
 
311
                    "                                     - BFS          Breadth first search\n"
 
312
                    "                                     - DFS          Depth first search (CTL default)\n"
 
313
                    "                                     - RDFS         Random depth first search\n"
 
314
                    "                                     - OverApprox   Linear Over Approx\n"
 
315
                    "  --seed-offset <number>             Extra noise to add to the seed of the random number generation\n"
 
316
                    "  -e, --state-space-exploration      State-space exploration only (query-file is irrelevant)\n"
 
317
                    "  -x, --xml-query <query index>      Parse XML query file and verify query of a given index\n"
 
318
                    "  -r, --reduction <type>             Change structural net reduction:\n"
 
319
                    "                                     - 0  disabled\n"
 
320
                    "                                     - 1  aggressive reduction (default)\n"
 
321
                    "                                     - 2  reduction preserving k-boundedness\n"
 
322
                    "                                     - 3  user defined reduction sequence, eg -r 3 0,1,2,3 to use rules A,B,C,D only, and in that order\n"
 
323
                    "  -d, --reduction-timeout <timeout>  Timeout for structural reductions in seconds (default 60)\n"
 
324
                    "  -q, --query-reduction <timeout>    Query reduction timeout in seconds (default 30)\n"
 
325
                    "                                     write -q 0 to disable query reduction\n"
 
326
                    "  -l, --lpsolve-timeout <timeout>    LPSolve timeout in seconds, default 10\n"
 
327
                    "  -p, --partial-order-reduction      Disable partial order reduction (stubborn sets)\n"
 
328
                    "  -a, --siphon-trap <timeout>        Siphon-Trap analysis timeout in seconds (default 0)\n"
 
329
                    "      --siphon-depth <place count>   Search depth of siphon (default 0, which counts all places)\n"
 
330
                    "  -n, --no-statistics                Do not display any statistics (default is to display it)\n"
 
331
                    "  -h, --help                         Display this help message\n"
 
332
                    "  -v, --version                      Display version information\n"
 
333
                    "  -ctl <type>                        Verify CTL properties\n"
 
334
                    "                                     - local     Liu and Smolka's on-the-fly algorithm\n"
 
335
                    "                                     - czero     local with certain zero extension (default)\n"
 
336
                    "  -c, --cpn-overapproximation        Over approximate query on Colored Petri Nets (CPN only)\n"
 
337
                    //"  -g                                 Enable game mode (CTL Only)" // Feature not yet implemented
 
338
#ifdef VERIFYPN_MC_Simplification
 
339
                    "  -z <number of cores>               Number of cores to use (currently only query simplification)\n"
 
340
#endif
 
341
                    "  -tar                               Enables Trace Abstraction Refinement for reachability properties\n"
 
342
                    "  --write-simplified <filename>      Outputs the queries to the given file after simplification\n"
 
343
                    "  --write-reduced <filename>         Outputs the model to the given file after structural reduction\n"
 
344
                    "  --binary-query-io <0,1,2,3>        Determines the input/output format of the query-file\n"
 
345
                    "                                     - 0 MCC XML format for Input and Output\n"
 
346
                    "                                     - 1 Input is binary, output is XML\n"
 
347
                    "                                     - 2 Output is binary, input is XML\n"
 
348
                    "                                     - 3 Input and Output is binary\n"
 
349
                    "\n"
 
350
                    "Return Values:\n"
 
351
                    "  0   Successful, query satisfiable\n"
 
352
                    "  1   Unsuccesful, query not satisfiable\n"
 
353
                    "  2   Unknown, algorithm was unable to answer the question\n"
 
354
                    "  3   Error, see stderr for error message\n"
 
355
                    "\n"
 
356
                    "VerifyPN is an untimed CTL verification engine for TAPAAL.\n"
 
357
                    "TAPAAL project page: <http://www.tapaal.net>\n");
 
358
            return SuccessCode;
 
359
        } else if (strcmp(argv[i], "-v") == 0 || strcmp(argv[i], "--version") == 0) {
 
360
            printf("VerifyPN (untimed verification engine for TAPAAL) %s\n", VERIFYPN_VERSION);
 
361
            printf("Copyright (C) 2011-2020\n");
 
362
            printf("                        Frederik Meyer Boenneland <sadpantz@gmail.com>\n");
 
363
            printf("                        Jakob Dyhr <jakobdyhr@gmail.com>\n");
 
364
            printf("                        Peter Fogh <peter.f1992@gmail.com>\n");
 
365
            printf("                        Jonas Finnemann Jensen <jopsen@gmail.com>\n");
 
366
            printf("                        Lasse Steen Jensen <lassjen88@gmail.com>\n");
 
367
            printf("                        Peter Gjøl Jensen <root@petergjoel.dk>\n");
 
368
            printf("                        Tobias Skovgaard Jepsen <tobiasj1991@gmail.com>\n");
 
369
            printf("                        Mads Johannsen <mads_johannsen@yahoo.com>\n");
 
370
            printf("                        Isabella Kaufmann <bellakaufmann93@gmail.com>\n");
 
371
            printf("                        Andreas Hairing Klostergaard <kloster92@me.com>\n");
 
372
            printf("                        Søren Moss Nielsen <soren_moss@mac.com>\n");
 
373
            printf("                        Thomas Søndersø Nielsen <primogens@gmail.com>\n");
 
374
            printf("                        Samuel Pastva <daemontus@gmail.com>\n");
 
375
            printf("                        Jiri Srba <srba.jiri@gmail.com>\n");
 
376
            printf("                        Lars Kærlund Østergaard <larsko@gmail.com>\n");
 
377
            printf("GNU GPLv3 or later <http://gnu.org/licenses/gpl.html>\n");
 
378
            return SuccessCode;
 
379
        } else if (options.modelfile == NULL) {
 
380
            options.modelfile = argv[i];
 
381
        } else if (options.queryfile == NULL) {
 
382
            options.queryfile = argv[i];
 
383
        } else {
 
384
                        fprintf(stderr, "Argument Error: Unrecognized option \"%s\"\n", options.modelfile);
 
385
                        return ErrorCode;
 
386
        }
 
387
    }
 
388
    //Print parameters
 
389
    if (options.printstatistics) {
 
390
        std::cout << std::endl << "Parameters: ";
 
391
        for (int i = 1; i < argc; i++) {
 
392
            std::cout << argv[i] << " ";
 
393
        }
 
394
        std::cout << std::endl;
 
395
    }
 
396
    
 
397
    if (options.statespaceexploration) {
 
398
        // for state-space exploration some options are mandatory
 
399
        options.enablereduction = 0;
 
400
        options.kbound = 0;
 
401
        options.queryReductionTimeout = 0;
 
402
        options.lpsolveTimeout = 0;
 
403
        options.siphontrapTimeout = 0;
 
404
        options.stubbornreduction = false;
 
405
//        outputtrace = false;
 
406
    }
 
407
 
 
408
 
 
409
    //----------------------- Validate Arguments -----------------------//
 
410
 
 
411
    //Check for model file
 
412
    if (!options.modelfile) {
 
413
        fprintf(stderr, "Argument Error: No model-file provided\n");
 
414
        return ErrorCode;
 
415
    }
 
416
 
 
417
    //Check for query file
 
418
    if (!options.modelfile && !options.statespaceexploration) {
 
419
        fprintf(stderr, "Argument Error: No query-file provided\n");
 
420
        return ErrorCode;
 
421
    }
 
422
    
 
423
    return ContinueCode;
 
424
}
 
425
 
 
426
auto
 
427
readQueries(options_t& options, std::vector<std::string>& qstrings)
 
428
{
 
429
 
 
430
    std::vector<Condition_ptr > conditions;
 
431
    if (!options.statespaceexploration) {
 
432
        //Open query file
 
433
        ifstream qfile(options.queryfile, ifstream::in);
 
434
        if (!qfile) {
 
435
            fprintf(stderr, "Error: Query file \"%s\" couldn't be opened\n", options.queryfile);
 
436
            fprintf(stdout, "CANNOT_COMPUTE\n");
 
437
            conditions.clear();
 
438
            return conditions;
 
439
        }
 
440
 
 
441
        if(options.querynumbers.size() == 0)
 
442
        {
 
443
            string querystring; // excluding EF and AG
 
444
 
 
445
            //Read everything
 
446
            stringstream buffer;
 
447
            buffer << qfile.rdbuf();
 
448
            string querystr = buffer.str(); // including EF and AG
 
449
            //Parse XML the queries and querystr let be the index of xmlquery 
 
450
        
 
451
            qstrings.push_back(querystring);
 
452
            //Validate query type
 
453
            if (querystr.substr(0, 2) != "EF" && querystr.substr(0, 2) != "AG") {
 
454
                    fprintf(stderr, "Error: Query type \"%s\" not supported, only (EF and AG is supported)\n", querystr.substr(0, 2).c_str());
 
455
                    return conditions;
 
456
            }
 
457
            //Check if is invariant
 
458
            bool isInvariant = querystr.substr(0, 2) == "AG";
 
459
 
 
460
            //Wrap in not if isInvariant
 
461
            querystring = querystr.substr(2);
 
462
            std::vector<std::string> tmp;
 
463
            conditions.emplace_back(ParseQuery(querystring, tmp));
 
464
            if(isInvariant) conditions.back() = std::make_shared<AGCondition>(conditions.back());
 
465
            else            conditions.back() = std::make_shared<EFCondition>(conditions.back());
 
466
        }
 
467
        else
 
468
        {
 
469
            std::vector<QueryItem> queries;
 
470
            if(options.binary_query_io & 1)
 
471
            {
 
472
                QueryBinaryParser parser;
 
473
                if (!parser.parse(qfile, options.querynumbers)) {
 
474
                    fprintf(stderr, "Error: Failed parsing binary query file\n");
 
475
                    fprintf(stdout, "DO_NOT_COMPETE\n");
 
476
                    conditions.clear();
 
477
                    return conditions;
 
478
                }     
 
479
                queries = std::move(parser.queries);
 
480
            }
 
481
            else
 
482
            {
 
483
                QueryXMLParser parser;
 
484
                if (!parser.parse(qfile, options.querynumbers)) {
 
485
                    fprintf(stderr, "Error: Failed parsing XML query file\n");
 
486
                    fprintf(stdout, "DO_NOT_COMPETE\n");
 
487
                    conditions.clear();
 
488
                    return conditions;
 
489
                }
 
490
                queries = std::move(parser.queries);
 
491
            }
 
492
 
 
493
            size_t i = 0;
 
494
            for(auto& q : queries)
 
495
            {
 
496
                if(!options.querynumbers.empty()
 
497
                        && options.querynumbers.count(i) == 0)
 
498
                {
 
499
                    ++i;
 
500
                    continue;
 
501
                }
 
502
                ++i;
 
503
 
 
504
                if (q.parsingResult == QueryItem::UNSUPPORTED_QUERY) {
 
505
                    fprintf(stdout, "The selected query in the XML query file is not supported\n");
 
506
                    fprintf(stdout, "FORMULA %s CANNOT_COMPUTE\n", q.id.c_str());
 
507
                    continue;
 
508
                }
 
509
                // fprintf(stdout, "Index of the selected query: %d\n\n", xmlquery);
 
510
 
 
511
                conditions.push_back(q.query);
 
512
                if (conditions.back() == nullptr) {
 
513
                    fprintf(stderr, "Error: Failed to parse query \"%s\"\n", q.id.c_str()); //querystr.substr(2).c_str());
 
514
                    fprintf(stdout, "FORMULA %s CANNOT_COMPUTE\n", q.id.c_str());
 
515
                    conditions.pop_back();
 
516
                }
 
517
                
 
518
                qstrings.push_back(q.id);
 
519
            }
 
520
        }
 
521
        qfile.close();
 
522
        return conditions;
 
523
    } else { // state-space exploration
 
524
        std::string querystring = "false";
 
525
        std::vector<std::string> empty;
 
526
        conditions.push_back(std::make_shared<EFCondition>(ParseQuery(querystring, empty)));
 
527
        return conditions;
 
528
    } 
 
529
 }
 
530
 
 
531
ReturnValue parseModel(AbstractPetriNetBuilder& builder, options_t& options)
 
532
{
 
533
    //Load the model
 
534
    ifstream mfile(options.modelfile, ifstream::in);
 
535
    if (!mfile) {
 
536
        fprintf(stderr, "Error: Model file \"%s\" couldn't be opened\n", options.modelfile);
 
537
        fprintf(stdout, "CANNOT_COMPUTE\n");
 
538
        return ErrorCode;
 
539
    }
 
540
 
 
541
 
 
542
    //Parse and build the petri net
 
543
    PNMLParser parser;
 
544
    parser.parse(mfile, &builder);
 
545
    options.isCPN = builder.isColored();
 
546
 
 
547
    // Close the file
 
548
    mfile.close();
 
549
    return ContinueCode;
 
550
}
 
551
 
 
552
void printStats(PetriNetBuilder& builder, options_t& options)
 
553
{
 
554
    if (options.printstatistics) {
 
555
        if (options.enablereduction != 0) {
 
556
 
 
557
            std::cout << "Size of net before structural reductions: " <<
 
558
                    builder.numberOfPlaces() << " places, " <<
 
559
                    builder.numberOfTransitions() << " transitions" << std::endl;             
 
560
            std::cout << "Size of net after structural reductions: " <<
 
561
                    builder.numberOfPlaces() - builder.RemovedPlaces() << " places, " <<
 
562
                    builder.numberOfTransitions() - builder.RemovedTransitions() << " transitions" << std::endl;
 
563
            std::cout << "Structural reduction finished after " << builder.getReductionTime() <<
 
564
                    " seconds" << std::endl;
 
565
            
 
566
            std::cout   << "\nNet reduction is enabled.\n";
 
567
            builder.printStats(std::cout);
 
568
        }
 
569
    }
 
570
}
 
571
 
 
572
void printUnfoldingStats(ColoredPetriNetBuilder& builder, options_t& options) {
 
573
    if (options.printstatistics) {
 
574
        if (!builder.isColored() && !builder.isUnfolded())
 
575
            return;
 
576
        std::cout << "\nSize of colored net: " <<
 
577
                builder.getPlaceCount() << " places, " <<
 
578
                builder.getTransitionCount() << " transitions, and " <<
 
579
                builder.getArcCount() << " arcs" << std::endl;
 
580
        std::cout << "Size of unfolded net: " <<
 
581
                builder.getUnfoldedPlaceCount() << " places, " <<
 
582
                builder.getUnfoldedTransitionCount() << " transitions, and " <<
 
583
                builder.getUnfoldedArcCount() << " arcs" << std::endl;
 
584
        std::cout << "Unfolded in " << builder.getUnfoldTime() << " seconds" << std::endl;
 
585
    }
 
586
}
 
587
 
 
588
std::string getXMLQueries(vector<std::shared_ptr<Condition>> queries, vector<std::string> querynames, std::vector<ResultPrinter::Result> results) {
 
589
    bool cont = false;    
 
590
    for(uint32_t i = 0; i < results.size(); i++) {
 
591
        if (results[i] == ResultPrinter::CTL) {
 
592
            cont = true;
 
593
            break;
 
594
        }
 
595
    }
 
596
    
 
597
    if (!cont) {
 
598
        return "";
 
599
    }
 
600
       
 
601
    std::stringstream ss;
 
602
    ss << "<?xml version=\"1.0\"?>\n<property-set xmlns=\"http://mcc.lip6.fr/\">\n";
 
603
    
 
604
    for(uint32_t i = 0; i < queries.size(); i++) {
 
605
        if (!(results[i] == ResultPrinter::CTL)) {
 
606
            continue;
 
607
        }
 
608
        ss << "  <property>\n    <id>" << querynames[i] << "</id>\n    <description>Simplified</description>\n    <formula>\n";
 
609
        queries[i]->toXML(ss, 3);
 
610
        ss << "    </formula>\n  </property>\n";
 
611
    }
 
612
            
 
613
    ss << "</property-set>\n";
 
614
    
 
615
    return ss.str();
 
616
}
 
617
 
 
618
void writeQueries(vector<std::shared_ptr<Condition>>& queries, vector<std::string>& querynames, std::vector<uint32_t>& order, std::string& filename, bool binary, const std::unordered_map<std::string, uint32_t>& place_names) 
 
619
{
 
620
    fstream out;
 
621
    
 
622
    if(binary)
 
623
    {
 
624
        out.open(filename, std::ios::binary | std::ios::out);
 
625
        uint32_t cnt = 0;
 
626
        for(uint32_t j = 0; j < queries.size(); j++) {
 
627
            if(queries[j]->isTriviallyTrue() || queries[j]->isTriviallyFalse()) continue;
 
628
            ++cnt;
 
629
        }
 
630
        out.write(reinterpret_cast<const char *>(&cnt), sizeof(uint32_t));
 
631
        cnt = place_names.size();
 
632
        out.write(reinterpret_cast<const char *>(&cnt), sizeof(uint32_t));
 
633
        for(auto& kv : place_names)
 
634
        {
 
635
            out.write(reinterpret_cast<const char *>(&kv.second), sizeof(uint32_t));
 
636
            out.write(kv.first.data(), kv.first.size());
 
637
            out.write("\0", sizeof(char));
 
638
        }
 
639
    }
 
640
    else
 
641
    {
 
642
        out.open(filename, std::ios::out);
 
643
        out << "<?xml version=\"1.0\"?>\n<property-set xmlns=\"http://mcc.lip6.fr/\">\n";
 
644
    }
 
645
    
 
646
    for(uint32_t j = 0; j < queries.size(); j++) {
 
647
        auto i = order[j];
 
648
        if(queries[i]->isTriviallyTrue() || queries[i]->isTriviallyFalse()) continue;
 
649
        if(binary)
 
650
        {
 
651
            out.write(querynames[i].data(), querynames[i].size());
 
652
            out.write("\0", sizeof(char));
 
653
            queries[i]->toBinary(out);
 
654
        }
 
655
        else
 
656
        {
 
657
            out << "  <property>\n    <id>" << querynames[i] << "</id>\n    <description>Simplified</description>\n    <formula>\n";
 
658
            queries[i]->toXML(out, 3);
 
659
            out << "    </formula>\n  </property>\n";
 
660
        }
 
661
    }
 
662
        
 
663
    if(binary == 0)
 
664
    {
 
665
        out << "</property-set>\n";
 
666
    }
 
667
    out.close();
 
668
}
 
669
 
 
670
int main(int argc, char* argv[]) {
 
671
 
 
672
    options_t options;
 
673
    
 
674
    ReturnValue v = parseOptions(argc, argv, options);
 
675
    if(v != ContinueCode) return v;
 
676
    options.print();
 
677
    srand (time(NULL) xor options.seed_offset);  
 
678
    ColoredPetriNetBuilder cpnBuilder;
 
679
    if(parseModel(cpnBuilder, options) != ContinueCode) 
 
680
    {
 
681
        std::cerr << "Error parsing the model" << std::endl;
 
682
        return ErrorCode;
 
683
    }
 
684
    if(options.cpnOverApprox && !cpnBuilder.isColored())
 
685
    {
 
686
        std::cerr << "CPN OverApproximation is only usable on colored models" << std::endl;
 
687
        return UnknownCode;
 
688
    }
 
689
    if (options.printstatistics) {
 
690
        std::cout << "Finished parsing model" << std::endl;
 
691
    }
 
692
 
 
693
    //----------------------- Parse Query -----------------------//
 
694
    std::vector<std::string> querynames;
 
695
    auto queries = readQueries(options, querynames);
 
696
    
 
697
    if(options.printstatistics && options.queryReductionTimeout > 0)
 
698
    {
 
699
        negstat_t stats;            
 
700
        std::cout << "RWSTATS LEGEND:";
 
701
        stats.printRules(std::cout);            
 
702
        std::cout << std::endl;
 
703
    }
 
704
 
 
705
    if(cpnBuilder.isColored())
 
706
    {
 
707
        negstat_t stats;            
 
708
        EvaluationContext context(nullptr, nullptr);
 
709
        for (ssize_t qid = queries.size() - 1; qid >= 0; --qid) {
 
710
            queries[qid] = queries[qid]->pushNegation(stats, context, false, false, false);
 
711
            if(options.printstatistics)
 
712
            {
 
713
                std::cout << "\nQuery before expansion and reduction: ";
 
714
                queries[qid]->toString(std::cout);
 
715
                std::cout << std::endl;
 
716
 
 
717
                std::cout << "RWSTATS COLORED PRE:";
 
718
                stats.print(std::cout);
 
719
                std::cout << std::endl;
 
720
            }
 
721
        }
 
722
    }
 
723
 
 
724
    if (options.cpnOverApprox) {
 
725
        for (ssize_t qid = queries.size() - 1; qid >= 0; --qid) {
 
726
            negstat_t stats;            
 
727
            EvaluationContext context(nullptr, nullptr);
 
728
            auto q = queries[qid]->pushNegation(stats, context, false, false, false);
 
729
            if (!q->isReachability() || q->isLoopSensitive() || stats.negated_fireability) {
 
730
                std::cerr << "Warning: CPN OverApproximation is only available for Reachability queries without deadlock, negated fireability and UpperBounds, skipping " << querynames[qid] << std::endl;
 
731
                queries.erase(queries.begin() + qid);
 
732
                querynames.erase(querynames.begin() + qid);
 
733
            }
 
734
        }
 
735
    }
 
736
    
 
737
    auto builder = options.cpnOverApprox ? cpnBuilder.stripColors() : cpnBuilder.unfold();
 
738
    printUnfoldingStats(cpnBuilder, options);
 
739
    builder.sort();
 
740
    std::vector<ResultPrinter::Result> results(queries.size(), ResultPrinter::Result::Unknown);
 
741
    ResultPrinter printer(&builder, &options, querynames);
 
742
    
 
743
    //----------------------- Query Simplification -----------------------//
 
744
    bool alldone = options.queryReductionTimeout > 0;
 
745
    PetriNetBuilder b2(builder);
 
746
    std::unique_ptr<PetriNet> qnet(b2.makePetriNet(false));
 
747
    MarkVal* qm0 = qnet->makeInitialMarking();
 
748
    ResultPrinter p2(&b2, &options, querynames);
 
749
 
 
750
    if(queries.size() == 0 || contextAnalysis(cpnBuilder, b2, qnet.get(), queries) != ContinueCode)
 
751
    {
 
752
        std::cerr << "Could not analyze the queries" << std::endl;
 
753
        return ErrorCode;
 
754
    }
 
755
 
 
756
    if (options.strategy == PetriEngine::Reachability::OverApprox && options.queryReductionTimeout == 0)
 
757
    { 
 
758
        // Conflicting flags "-s OverApprox" and "-q 0"
 
759
        std::cerr << "Conflicting flags '-s OverApprox' and '-q 0'" << std::endl;
 
760
        return ErrorCode;
 
761
    }
 
762
 
 
763
    // simplification. We always want to do negation-push and initial marking check.
 
764
    {
 
765
        // simplification. We always want to do negation-push and initial marking check.
 
766
        std::vector<LPCache> caches(options.cores);
 
767
        std::atomic<uint32_t> to_handle(queries.size());
 
768
        auto begin = std::chrono::high_resolution_clock::now();
 
769
        auto end = std::chrono::high_resolution_clock::now();
 
770
        std::vector<bool> hadTo(queries.size(), true);
 
771
        
 
772
        do
 
773
        {
 
774
            auto qt = (options.queryReductionTimeout - std::chrono::duration_cast<std::chrono::seconds>(end - begin).count()) / ( 1 + (to_handle / options.cores));
 
775
            if((to_handle <= options.cores || options.cores == 1) && to_handle > 0)
 
776
                qt = (options.queryReductionTimeout - std::chrono::duration_cast<std::chrono::seconds>(end - begin).count()) / to_handle;
 
777
            std::atomic<uint32_t> cnt(0);
 
778
#ifdef VERIFYPN_MC_Simplification
 
779
 
 
780
            std::vector<std::thread> threads;
 
781
#endif
 
782
            std::vector<std::stringstream> tstream(queries.size());
 
783
            uint32_t old = to_handle;
 
784
            for(size_t c = 0; c < std::min<uint32_t>(options.cores, old); ++c)
 
785
            {
 
786
#ifdef VERIFYPN_MC_Simplification
 
787
                threads.push_back(std::thread([&,c](){ 
 
788
#else
 
789
                auto simplify = [&,c](){ 
 
790
#endif
 
791
                    auto& out = tstream[c];
 
792
                    auto& cache = caches[c];
 
793
                    while(true)
 
794
                    {
 
795
                    auto i = cnt++;
 
796
                    if(i >= queries.size()) return;                
 
797
                    if(!hadTo[i]) continue;
 
798
                    hadTo[i] = false;
 
799
                    negstat_t stats;            
 
800
                    EvaluationContext context(qm0, qnet.get());
 
801
                    if(options.printstatistics && options.queryReductionTimeout > 0)
 
802
                    {
 
803
                        out << "\nQuery before reduction: ";
 
804
                        queries[i]->toString(out);
 
805
                        out << std::endl;
 
806
                    }
 
807
 
 
808
#ifndef VERIFYPN_MC_Simplification
 
809
                    qt = (options.queryReductionTimeout - std::chrono::duration_cast<std::chrono::seconds>(end - begin).count()) / (queries.size() - i);              
 
810
#endif
 
811
                    // this is used later, we already know that this is a plain reachability (or AG)
 
812
                    bool wasAGCPNApprox = dynamic_cast<NotCondition*>(queries[i].get()) != nullptr;
 
813
                    int preSize=queries[i]->formulaSize(); 
 
814
                    queries[i] = Condition::initialMarkingRW([&](){ return queries[i]; }, stats,  context, false, false, true)
 
815
                                            ->pushNegation(stats, context, false, false, true);
 
816
                    wasAGCPNApprox |= dynamic_cast<NotCondition*>(queries[i].get()) != nullptr;
 
817
 
 
818
                    if(options.queryReductionTimeout > 0 && options.printstatistics)
 
819
                    {
 
820
                        out << "RWSTATS PRE:";
 
821
                        stats.print(out);
 
822
                        out << std::endl;
 
823
                    }
 
824
 
 
825
                    if (options.queryReductionTimeout > 0 && qt > 0)
 
826
                    {
 
827
                        SimplificationContext simplificationContext(qm0, qnet.get(), qt,
 
828
                                options.lpsolveTimeout, &cache);
 
829
                        try {
 
830
                            negstat_t stats;            
 
831
                            queries[i] = (queries[i]->simplify(simplificationContext)).formula->pushNegation(stats, context, false, false, true);
 
832
                            wasAGCPNApprox |= dynamic_cast<NotCondition*>(queries[i].get()) != nullptr;
 
833
                            if(options.printstatistics)
 
834
                            {
 
835
                                out << "RWSTATS POST:";
 
836
                                stats.print(out);
 
837
                                out << std::endl;
 
838
                            }
 
839
                        } catch (std::bad_alloc& ba){
 
840
                            std::cerr << "Query reduction failed." << std::endl;
 
841
                            std::cerr << "Exception information: " << ba.what() << std::endl;
 
842
 
 
843
                            delete[] qm0;
 
844
                            std::exit(ErrorCode);
 
845
                        }
 
846
 
 
847
                        if(options.printstatistics)
 
848
                        {
 
849
                            out << "\nQuery after reduction: ";
 
850
                            queries[i]->toString(out);
 
851
                            out << std::endl;
 
852
                        }
 
853
                        if(simplificationContext.timeout()){
 
854
                            if(options.printstatistics)
 
855
                                out << "Query reduction reached timeout.\n";
 
856
                            hadTo[i] = true;
 
857
                        } else {
 
858
                            if(options.printstatistics)
 
859
                                out << "Query reduction finished after " << simplificationContext.getReductionTime() << " seconds.\n";
 
860
                            --to_handle;
 
861
                        }
 
862
                    }
 
863
                    else if(options.printstatistics)
 
864
                    {
 
865
                        out << "Skipping linear-programming (-q 0)" << std::endl;
 
866
                    }
 
867
                    if(options.cpnOverApprox && wasAGCPNApprox)
 
868
                    {
 
869
                        if(queries[i]->isTriviallyTrue())
 
870
                            queries[i] = std::make_shared<BooleanCondition>(false);
 
871
                        else if(queries[i]->isTriviallyFalse())
 
872
                            queries[i] = std::make_shared<BooleanCondition>(true);
 
873
                        queries[i]->setInvariant(wasAGCPNApprox);
 
874
                    }
 
875
                   
 
876
 
 
877
                    if(options.printstatistics)
 
878
                    {
 
879
                        int postSize=queries[i]->formulaSize();
 
880
                        double redPerc = preSize-postSize == 0 ? 0 : ((double)(preSize-postSize)/(double)preSize)*100;
 
881
                        out << "Query size reduced from " << preSize << " to " << postSize << " nodes ( " << redPerc << " percent reduction).\n";
 
882
                    }
 
883
                    }
 
884
                }
 
885
#ifdef VERIFYPN_MC_Simplification
 
886
                ));
 
887
#else
 
888
                ;
 
889
                simplify();
 
890
#endif
 
891
            }
 
892
#ifndef VERIFYPN_MC_Simplification
 
893
            std::cout << tstream[0].str() << std::endl;
 
894
            break;
 
895
#else
 
896
            for(size_t i = 0; i < std::min<uint32_t>(options.cores, old); ++i)
 
897
            {
 
898
                threads[i].join();
 
899
                std::cout << tstream[i].str();
 
900
                std::cout << std::endl;
 
901
            }
 
902
#endif
 
903
            end = std::chrono::high_resolution_clock::now();
 
904
 
 
905
        } while(std::any_of(hadTo.begin(), hadTo.end(), [](auto a) { return a;}) && std::chrono::duration_cast<std::chrono::seconds>(end - begin).count() < options.queryReductionTimeout && to_handle > 0);
 
906
    } 
 
907
    
 
908
    if(options.query_out_file.size() > 0)
 
909
    {
 
910
        std::vector<uint32_t> reorder(queries.size());
 
911
        for(uint32_t i = 0; i < queries.size(); ++i) reorder[i] = i;
 
912
        std::sort(reorder.begin(), reorder.end(), [&queries](auto a, auto b){
 
913
 
 
914
            if(queries[a]->isReachability() != queries[b]->isReachability())
 
915
                return queries[a]->isReachability() > queries[b]->isReachability();
 
916
            if(queries[a]->isLoopSensitive() != queries[b]->isLoopSensitive())
 
917
                return queries[a]->isLoopSensitive() < queries[b]->isLoopSensitive();
 
918
            if(queries[a]->containsNext() != queries[b]->containsNext())
 
919
                return queries[a]->containsNext() < queries[b]->containsNext();
 
920
            return queries[a]->formulaSize() < queries[b]->formulaSize();
 
921
        });
 
922
        writeQueries(queries, querynames, reorder, options.query_out_file, options.binary_query_io & 2, builder.getPlaceNames());
 
923
    }
 
924
    
 
925
    qnet = nullptr;
 
926
    delete[] qm0;
 
927
 
 
928
    if (!options.statespaceexploration){
 
929
        for(size_t i = 0; i < queries.size(); ++i)
 
930
        {
 
931
            if(queries[i]->isTriviallyTrue()){
 
932
                results[i] = p2.handle(i, queries[i].get(), ResultPrinter::Satisfied).first;
 
933
                if(results[i] == ResultPrinter::Ignore && options.printstatistics)
 
934
                {
 
935
                    std::cout << "Unable to decide if query is satisfied." << std::endl << std::endl;
 
936
                }
 
937
                else if (options.printstatistics) {
 
938
                    std::cout << "Query solved by Query Simplification." << std::endl << std::endl;
 
939
                }
 
940
            } else if (queries[i]->isTriviallyFalse()) {
 
941
                results[i] = p2.handle(i, queries[i].get(), ResultPrinter::NotSatisfied).first;
 
942
                if(results[i] == ResultPrinter::Ignore &&  options.printstatistics)
 
943
                {
 
944
                    std::cout << "Unable to decide if query is satisfied." << std::endl << std::endl;
 
945
                }
 
946
                else if (options.printstatistics) {
 
947
                    std::cout << "Query solved by Query Simplification." << std::endl << std::endl;
 
948
                }
 
949
            } else if (options.strategy == PetriEngine::Reachability::OverApprox){
 
950
                results[i] = p2.handle(i, queries[i].get(), ResultPrinter::Unknown).first;
 
951
                if (options.printstatistics) {
 
952
                    std::cout << "Unable to decide if query is satisfied." << std::endl << std::endl;
 
953
                }
 
954
            } else if (!queries[i]->isReachability()) {
 
955
                results[i] = ResultPrinter::CTL;
 
956
                alldone = false;
 
957
            } else {
 
958
                queries[i] = queries[i]->prepareForReachability();
 
959
                alldone = false;
 
960
            }
 
961
        }
 
962
 
 
963
        if(alldone && options.model_out_file.size() == 0) return SuccessCode;
 
964
    }
 
965
    
 
966
    options.queryReductionTimeout = 0;
 
967
    
 
968
    //--------------------- Apply Net Reduction ---------------//
 
969
        
 
970
    if (options.enablereduction > 0) {
 
971
        // Compute how many times each place appears in the query
 
972
        builder.startTimer();
 
973
        builder.reduce(queries, results, options.enablereduction, options.trace, nullptr, options.reductionTimeout, options.reductions);
 
974
        printer.setReducer(builder.getReducer());        
 
975
    }
 
976
    
 
977
    printStats(builder, options);
 
978
    
 
979
    auto net = std::unique_ptr<PetriNet>(builder.makePetriNet());
 
980
    
 
981
    if(options.model_out_file.size() > 0)
 
982
    {
 
983
        fstream file;
 
984
        file.open(options.model_out_file, std::ios::out);
 
985
        net->toXML(file);
 
986
    }
 
987
    
 
988
    if(alldone) return SuccessCode;
 
989
    
 
990
    //----------------------- Verify CTL queries -----------------------//
 
991
    std::vector<size_t> ctl_ids;
 
992
    for(size_t i = 0; i < queries.size(); ++i)
 
993
    {
 
994
        if(results[i] == ResultPrinter::CTL)
 
995
        {
 
996
            ctl_ids.push_back(i);
 
997
        }
 
998
    }
 
999
    
 
1000
    if (ctl_ids.size() > 0) {
 
1001
        options.isctl=true;
 
1002
        PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;
 
1003
 
 
1004
        // Assign indexes
 
1005
        if(queries.size() == 0 || contextAnalysis(cpnBuilder, builder, net.get(), queries) != ContinueCode)
 
1006
        {
 
1007
            std::cerr << "An error occurred while assigning indexes" << std::endl;
 
1008
            return ErrorCode;
 
1009
        }
 
1010
        if(options.strategy == DEFAULT) options.strategy = PetriEngine::Reachability::DFS;
 
1011
        v = CTLMain(net.get(),
 
1012
            options.ctlalgorithm,
 
1013
            options.strategy,
 
1014
            options.gamemode,
 
1015
            options.printstatistics,
 
1016
            true,
 
1017
            options.stubbornreduction,
 
1018
            querynames,
 
1019
            queries,
 
1020
            ctl_ids,
 
1021
            options);
 
1022
 
 
1023
        if (std::find(results.begin(), results.end(), ResultPrinter::Unknown) == results.end()) {
 
1024
            return v;
 
1025
        }
 
1026
        // go back to previous strategy if the program continues
 
1027
        options.strategy=reachabilityStrategy;
 
1028
    }
 
1029
    options.isctl=false;
 
1030
    
 
1031
    //----------------------- Siphon Trap ------------------------//
 
1032
    
 
1033
    if(options.siphontrapTimeout > 0){
 
1034
        for (uint32_t i = 0; i < results.size(); i ++) {
 
1035
            bool isDeadlockQuery = std::dynamic_pointer_cast<DeadlockCondition>(queries[i]) != nullptr;
 
1036
 
 
1037
            if (results[i] == ResultPrinter::Unknown && isDeadlockQuery) {    
 
1038
                STSolver stSolver(printer, *net, queries[i].get(), options.siphonDepth);
 
1039
                stSolver.solve(options.siphontrapTimeout);
 
1040
                results[i] = stSolver.printResult();
 
1041
                if (results[i] == Reachability::ResultPrinter::NotSatisfied && options.printstatistics) {
 
1042
                    std::cout << "Query solved by Siphon-Trap Analysis." << std::endl << std::endl;
 
1043
                }
 
1044
            }
 
1045
        }
 
1046
        
 
1047
        if (std::find(results.begin(), results.end(), ResultPrinter::Unknown) == results.end()) {
 
1048
            return SuccessCode;
 
1049
        }
 
1050
    }
 
1051
    options.siphontrapTimeout = 0;
 
1052
    
 
1053
    //----------------------- Reachability -----------------------//
 
1054
 
 
1055
    //Analyse context again to reindex query
 
1056
    contextAnalysis(cpnBuilder, builder, net.get(), queries);
 
1057
 
 
1058
    // Change default place-holder to default strategy
 
1059
    if(options.strategy == DEFAULT) options.strategy = PetriEngine::Reachability::HEUR;
 
1060
    
 
1061
    if(options.tar && net->numberOfPlaces() > 0)
 
1062
    {
 
1063
        //Create reachability search strategy
 
1064
        TARReachabilitySearch strategy(printer, *net, builder.getReducer(), options.kbound);
 
1065
 
 
1066
        // Change default place-holder to default strategy
 
1067
        fprintf(stdout, "Search strategy option was ignored as the TAR engine is called.\n");
 
1068
        options.strategy = PetriEngine::Reachability::DFS;
 
1069
 
 
1070
        //Reachability search
 
1071
        strategy.reachable(queries, results, 
 
1072
                options.printstatistics,
 
1073
                options.trace);
 
1074
    }
 
1075
    else
 
1076
    {
 
1077
        ReachabilitySearch strategy(*net, printer, options.kbound);
 
1078
 
 
1079
        // Change default place-holder to default strategy
 
1080
        if(options.strategy == DEFAULT) options.strategy = PetriEngine::Reachability::HEUR;
 
1081
 
 
1082
        //Reachability search
 
1083
        strategy.reachable(queries, results,
 
1084
                           options.strategy,
 
1085
                           options.stubbornreduction,
 
1086
                           options.statespaceexploration,
 
1087
                           options.printstatistics,
 
1088
                           options.trace);
 
1089
    }
 
1090
       
 
1091
    return SuccessCode;
 
1092
}
 
1093