1
/* TAPAAL untimed verification engine verifypn
2
* Copyright (C) 2011-2019 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>
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>
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>
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.
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.
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/>.
47
#ifdef ENABLE_MC_SIMPLIFICATION
52
#include "PetriEngine/PQL/PQLParser.h"
53
#include "PetriEngine/PQL/Contexts.h"
54
#include "PetriEngine/Reachability/ReachabilitySearch.h"
56
#include "PetriEngine/Reachability/TARReachability.h"
58
#include "PetriEngine/Reducer.h"
59
#include "PetriParse/QueryXMLParser.h"
60
#include "PetriParse/QueryBinaryParser.h"
61
#include "PetriParse/PNMLParser.h"
62
#include "PetriEngine/PetriNetBuilder.h"
63
#include "PetriEngine/PQL/PQL.h"
64
#include "PetriEngine/options.h"
65
#include "PetriEngine/errorcodes.h"
66
#include "PetriEngine/STSolver.h"
67
#include "PetriEngine/Simplification/Member.h"
68
#include "PetriEngine/Simplification/LinearPrograms.h"
69
#include "PetriEngine/Simplification/Retval.h"
71
#include "CTL/CTLEngine.h"
72
#include "PetriEngine/PQL/Expressions.h"
73
#include "PetriEngine/Colored/ColoredPetriNetBuilder.h"
76
using namespace PetriEngine;
77
using namespace PetriEngine::PQL;
78
using namespace PetriEngine::Reachability;
80
#define VERSION "3.0.2"
82
ReturnValue contextAnalysis(ColoredPetriNetBuilder& cpnBuilder, PetriNetBuilder& builder, const PetriNet* net, std::vector<std::shared_ptr<Condition> >& queries)
85
ColoredAnalysisContext context(builder.getPlaceNames(), builder.getTransitionNames(), net, cpnBuilder.getUnfoldedPlaceNames(), cpnBuilder.getUnfoldedTransitionNames(), cpnBuilder.isColored());
86
for(auto& q : queries)
91
if (context.errors().size() > 0) {
92
for (size_t i = 0; i < context.errors().size(); i++) {
93
fprintf(stderr, "Query Context Analysis Error: %s\n", context.errors()[i].toString().c_str());
101
std::vector<std::string> explode(std::string const & s)
103
std::vector<std::string> result;
104
std::istringstream iss(s);
106
for (std::string token; std::getline(iss, token, ','); )
108
result.push_back(std::move(token));
109
if(result.back().empty()) result.pop_back();
115
ReturnValue parseOptions(int argc, char* argv[], options_t& options)
117
for (int i = 1; i < argc; i++) {
118
if (strcmp(argv[i], "-k") == 0 || strcmp(argv[i], "--k-bound") == 0) {
120
fprintf(stderr, "Missing number after \"%s\"\n", argv[i]);
123
if (sscanf(argv[++i], "%d", &options.kbound) != 1 || options.kbound < 0) {
124
fprintf(stderr, "Argument Error: Invalid number of tokens \"%s\"\n", argv[i]);
127
} else if(strcmp(argv[i], "-s") == 0 || strcmp(argv[i], "--search-strategy") == 0){
129
fprintf(stderr, "Missing search strategy after \"%s\"\n\n", argv[i]);
133
if(strcmp(s, "BestFS") == 0)
134
options.strategy = HEUR;
135
else if(strcmp(s, "BFS") == 0)
136
options.strategy = BFS;
137
else if(strcmp(s, "DFS") == 0)
138
options.strategy = DFS;
139
else if(strcmp(s, "RDFS") == 0)
140
options.strategy = RDFS;
141
else if(strcmp(s, "OverApprox") == 0)
142
options.strategy = OverApprox;
144
fprintf(stderr, "Argument Error: Unrecognized search strategy \"%s\"\n", s);
147
} else if (strcmp(argv[i], "-q") == 0 || strcmp(argv[i], "--query-reduction") == 0) {
149
fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
152
if (sscanf(argv[++i], "%d", &options.queryReductionTimeout) != 1 || options.queryReductionTimeout < 0) {
153
fprintf(stderr, "Argument Error: Invalid query reduction timeout argument \"%s\"\n", argv[i]);
156
} else if (strcmp(argv[i], "-l") == 0 || strcmp(argv[i], "--lpsolve-timeout") == 0) {
158
fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
161
if (sscanf(argv[++i], "%d", &options.lpsolveTimeout) != 1 || options.lpsolveTimeout < 0) {
162
fprintf(stderr, "Argument Error: Invalid LPSolve timeout argument \"%s\"\n", argv[i]);
165
} else if (strcmp(argv[i], "-e") == 0 || strcmp(argv[i], "--state-space-exploration") == 0) {
166
options.statespaceexploration = true;
167
} else if (strcmp(argv[i], "-n") == 0 || strcmp(argv[i], "--no-statistics") == 0) {
168
options.printstatistics = false;
169
} else if (strcmp(argv[i], "-t") == 0 || strcmp(argv[i], "--trace") == 0) {
170
options.trace = true;
171
} else if (strcmp(argv[i], "-x") == 0 || strcmp(argv[i], "--xml-queries") == 0) {
173
fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
176
std::vector<std::string> q = explode(argv[++i]);
180
if(sscanf(qn.c_str(), "%d", &n) != 1 || n <= 0)
182
std::cerr << "Error in query numbers : " << qn << std::endl;
186
options.querynumbers.insert(--n);
189
} else if (strcmp(argv[i], "-r") == 0 || strcmp(argv[i], "--reduction") == 0) {
191
fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
194
if (sscanf(argv[++i], "%d", &options.enablereduction) != 1 || options.enablereduction < 0 || options.enablereduction > 2) {
195
fprintf(stderr, "Argument Error: Invalid reduction argument \"%s\"\n", argv[i]);
198
} else if (strcmp(argv[i], "-d") == 0 || strcmp(argv[i], "--reduction-timeout") == 0) {
200
fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
203
if (sscanf(argv[++i], "%d", &options.reductionTimeout) != 1) {
204
fprintf(stderr, "Argument Error: Invalid reduction timeout argument \"%s\"\n", argv[i]);
207
} else if(strcmp(argv[i], "--seed-offset") == 0) {
208
if (sscanf(argv[++i], "%u", &options.seed_offset) != 1) {
209
fprintf(stderr, "Argument Error: Invalid seed offset argument \"%s\"\n", argv[i]);
212
} else if(strcmp(argv[i], "-p") == 0 || strcmp(argv[i], "--partial-order-reduction") == 0) {
213
options.stubbornreduction = false;
214
} else if(strcmp(argv[i], "-a") == 0 || strcmp(argv[i], "--siphon-trap") == 0) {
216
fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
219
if (sscanf(argv[++i], "%u", &options.siphontrapTimeout) != 1) {
220
fprintf(stderr, "Argument Error: Invalid siphon-trap timeout \"%s\"\n", argv[i]);
223
} else if(strcmp(argv[i], "--siphon-depth") == 0) {
225
fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
228
if (sscanf(argv[++i], "%u", &options.siphonDepth) != 1) {
229
fprintf(stderr, "Argument Error: Invalid siphon-depth count \"%s\"\n", argv[i]);
234
else if (strcmp(argv[i], "-tar") == 0)
240
else if (strcmp(argv[i], "--write-simplified") == 0)
242
options.query_out_file = std::string(argv[++i]);
244
else if(strcmp(argv[i], "--binary-query-io") == 0)
246
if (sscanf(argv[++i], "%u", &options.binary_query_io) != 1 || options.binary_query_io > 3) {
247
fprintf(stderr, "Argument Error: Invalid binary-query-io value \"%s\"\n", argv[i]);
251
else if (strcmp(argv[i], "--write-reduced") == 0)
253
options.model_out_file = std::string(argv[++i]);
255
#ifdef ENABLE_MC_SIMPLIFICATION
256
else if (strcmp(argv[i], "-z") == 0)
259
fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
262
if (sscanf(argv[++i], "%u", &options.cores) != 1) {
263
fprintf(stderr, "Argument Error: Invalid cores count \"%s\"\n", argv[i]);
268
else if (strcmp(argv[i], "-ctl") == 0){
270
if(strcmp(argv[i + 1], "local") == 0){
271
options.ctlalgorithm = CTL::Local;
273
else if(strcmp(argv[i + 1], "czero") == 0){
274
options.ctlalgorithm = CTL::CZero;
278
fprintf(stderr, "Argument Error: Invalid ctl-algorithm type \"%s\"\n", argv[i + 1]);
284
} else if (strcmp(argv[i], "-g") == 0 || strcmp(argv[i], "--game-mode") == 0){
285
options.gamemode = true;
286
} else if (strcmp(argv[i], "-c") == 0 || strcmp(argv[i], "--cpn-overapproximation") == 0) {
287
options.cpnOverApprox = true;
288
} else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "--help") == 0) {
289
printf("Usage: verifypn [options] model-file query-file\n"
290
"A tool for answering CTL and reachability queries of place cardinality\n"
291
"deadlock and transition fireability for weighted P/T Petri nets\n"
292
"extended with inhibitor arcs.\n"
295
" -k, --k-bound <number of tokens> Token bound, 0 to ignore (default)\n"
296
" -t, --trace Provide XML-trace to stderr\n"
297
" -s, --search-strategy <strategy> Search strategy:\n"
298
" - BestFS Heuristic search (default)\n"
299
" - BFS Breadth first search\n"
300
" - DFS Depth first search (CTL default)\n"
301
" - RDFS Random depth first search\n"
302
" - OverApprox Linear Over Approx\n"
303
" --seed-offset <number> Extra noise to add to the seed of the random number generation\n"
304
" -e, --state-space-exploration State-space exploration only (query-file is irrelevant)\n"
305
" -x, --xml-query <query index> Parse XML query file and verify query of a given index\n"
306
" -r, --reduction <type> Change structural net reduction:\n"
308
" - 1 aggressive reduction (default)\n"
309
" - 2 reduction preserving k-boundedness\n"
310
" -d, --reduction-timeout <timeout> Timeout for structural reductions in seconds (default 60)\n"
311
" -q, --query-reduction <timeout> Query reduction timeout in seconds (default 30)\n"
312
" write -q 0 to disable query reduction\n"
313
" -l, --lpsolve-timeout <timeout> LPSolve timeout in seconds, default 10\n"
314
" -p, --partial-order-reduction Disable partial order reduction (stubborn sets)\n"
315
" -a, --siphon-trap <timeout> Siphon-Trap analysis timeout in seconds (default 0)\n"
316
" --siphon-depth <place count> Search depth of siphon (default 0, which counts all places)\n"
317
" -n, --no-statistics Do not display any statistics (default is to display it)\n"
318
" -h, --help Display this help message\n"
319
" -v, --version Display version information\n"
320
" -ctl <type> Verify CTL properties\n"
321
" - local Liu and Smolka's on-the-fly algorithm\n"
322
" - czero local with certain zero extension (default)\n"
323
" -c, --cpn-overapproximation Over approximate query on Colored Petri Nets (CPN only)\n"
324
//" -g Enable game mode (CTL Only)" // Feature not yet implemented
325
#ifdef ENABLE_MC_SIMPLIFICATION
326
" -z <number of cores> Number of cores to use (currently only query simplification)\n"
329
" -tar Enables Trace Abstraction Refinement for reachability properties\n"
331
" --write-simplified <filename> Outputs the queries to the given file after simplification\n"
332
" --write-reduced <filename> Outputs the model to the given file after structural reduction\n"
333
" --binary-query-io <0,1,2,3> Determines the input/output format of the query-file\n"
334
" - 0 MCC XML format for Input and Output\n"
335
" - 1 Input is binary, output is XML\n"
336
" - 2 Output is binary, input is XML\n"
337
" - 3 Input and Output is binary\n"
340
" 0 Successful, query satisfiable\n"
341
" 1 Unsuccesful, query not satisfiable\n"
342
" 2 Unknown, algorithm was unable to answer the question\n"
343
" 3 Error, see stderr for error message\n"
345
"VerifyPN is an untimed CTL verification engine for TAPAAL.\n"
346
"TAPAAL project page: <http://www.tapaal.net>\n");
348
} else if (strcmp(argv[i], "-v") == 0 || strcmp(argv[i], "--version") == 0) {
349
printf("VerifyPN (untimed verification engine for TAPAAL) %s\n", VERSION);
350
printf("Copyright (C) 2011-2019\n");
351
printf(" Frederik Meyer Boenneland <sadpantz@gmail.com>\n");
352
printf(" Jakob Dyhr <jakobdyhr@gmail.com>\n");
353
printf(" Peter Fogh <peter.f1992@gmail.com>\n");
354
printf(" Jonas Finnemann Jensen <jopsen@gmail.com>\n");
355
printf(" Lasse Steen Jensen <lassjen88@gmail.com>\n");
356
printf(" Peter Gjøl Jensen <root@petergjoel.dk>\n");
357
printf(" Tobias Skovgaard Jepsen <tobiasj1991@gmail.com>\n");
358
printf(" Mads Johannsen <mads_johannsen@yahoo.com>\n");
359
printf(" Isabella Kaufmann <bellakaufmann93@gmail.com>\n");
360
printf(" Andreas Hairing Klostergaard <kloster92@me.com>\n");
361
printf(" Søren Moss Nielsen <soren_moss@mac.com>\n");
362
printf(" Thomas Søndersø Nielsen <primogens@gmail.com>\n");
363
printf(" Samuel Pastva <daemontus@gmail.com>\n");
364
printf(" Jiri Srba <srba.jiri@gmail.com>\n");
365
printf(" Lars Kærlund Østergaard <larsko@gmail.com>\n");
366
printf("GNU GPLv3 or later <http://gnu.org/licenses/gpl.html>\n");
368
} else if (options.modelfile == NULL) {
369
options.modelfile = argv[i];
370
} else if (options.queryfile == NULL) {
371
options.queryfile = argv[i];
373
fprintf(stderr, "Argument Error: Unrecognized option \"%s\"\n", options.modelfile);
378
if (options.printstatistics) {
379
std::cout << std::endl << "Parameters: ";
380
for (int i = 1; i < argc; i++) {
381
std::cout << argv[i] << " ";
383
std::cout << std::endl;
386
if (options.statespaceexploration) {
387
// for state-space exploration some options are mandatory
388
options.enablereduction = 0;
390
options.queryReductionTimeout = 0;
391
options.lpsolveTimeout = 0;
392
options.siphontrapTimeout = 0;
393
options.stubbornreduction = false;
394
// outputtrace = false;
398
//----------------------- Validate Arguments -----------------------//
400
//Check for model file
401
if (!options.modelfile) {
402
fprintf(stderr, "Argument Error: No model-file provided\n");
406
//Check for query file
407
if (!options.modelfile && !options.statespaceexploration) {
408
fprintf(stderr, "Argument Error: No query-file provided\n");
416
readQueries(options_t& options, std::vector<std::string>& qstrings)
419
std::vector<Condition_ptr > conditions;
420
if (!options.statespaceexploration) {
422
ifstream qfile(options.queryfile, ifstream::in);
424
fprintf(stderr, "Error: Query file \"%s\" couldn't be opened\n", options.queryfile);
425
fprintf(stdout, "CANNOT_COMPUTE\n");
430
if(options.querynumbers.size() == 0)
432
string querystring; // excluding EF and AG
436
buffer << qfile.rdbuf();
437
string querystr = buffer.str(); // including EF and AG
438
//Parse XML the queries and querystr let be the index of xmlquery
440
qstrings.push_back(querystring);
441
//Validate query type
442
if (querystr.substr(0, 2) != "EF" && querystr.substr(0, 2) != "AG") {
443
fprintf(stderr, "Error: Query type \"%s\" not supported, only (EF and AG is supported)\n", querystr.substr(0, 2).c_str());
446
//Check if is invariant
447
bool isInvariant = querystr.substr(0, 2) == "AG";
449
//Wrap in not if isInvariant
450
querystring = querystr.substr(2);
451
std::vector<std::string> tmp;
452
conditions.emplace_back(ParseQuery(querystring, tmp));
453
if(isInvariant) conditions.back() = std::make_shared<AGCondition>(conditions.back());
454
else conditions.back() = std::make_shared<EFCondition>(conditions.back());
458
std::vector<QueryItem> queries;
459
if(options.binary_query_io & 1)
461
QueryBinaryParser parser;
462
if (!parser.parse(qfile, options.querynumbers)) {
463
fprintf(stderr, "Error: Failed parsing binary query file\n");
464
fprintf(stdout, "DO_NOT_COMPETE\n");
468
queries = std::move(parser.queries);
472
QueryXMLParser parser;
473
if (!parser.parse(qfile, options.querynumbers)) {
474
fprintf(stderr, "Error: Failed parsing XML query file\n");
475
fprintf(stdout, "DO_NOT_COMPETE\n");
479
queries = std::move(parser.queries);
483
for(auto& q : queries)
485
if(!options.querynumbers.empty()
486
&& options.querynumbers.count(i) == 0)
493
if (q.parsingResult == QueryItem::UNSUPPORTED_QUERY) {
494
fprintf(stdout, "The selected query in the XML query file is not supported\n");
495
fprintf(stdout, "FORMULA %s CANNOT_COMPUTE\n", q.id.c_str());
498
// fprintf(stdout, "Index of the selected query: %d\n\n", xmlquery);
500
conditions.push_back(q.query);
501
if (conditions.back() == nullptr) {
502
fprintf(stderr, "Error: Failed to parse query \"%s\"\n", q.id.c_str()); //querystr.substr(2).c_str());
503
fprintf(stdout, "FORMULA %s CANNOT_COMPUTE\n", q.id.c_str());
504
conditions.pop_back();
507
qstrings.push_back(q.id);
512
} else { // state-space exploration
513
std::string querystring = "false";
514
std::vector<std::string> empty;
515
conditions.push_back(std::make_shared<EFCondition>(ParseQuery(querystring, empty)));
520
ReturnValue parseModel(AbstractPetriNetBuilder& builder, options_t& options)
523
ifstream mfile(options.modelfile, ifstream::in);
525
fprintf(stderr, "Error: Model file \"%s\" couldn't be opened\n", options.modelfile);
526
fprintf(stdout, "CANNOT_COMPUTE\n");
531
//Parse and build the petri net
533
parser.parse(mfile, &builder);
534
options.isCPN = builder.isColored();
541
void printStats(PetriNetBuilder& builder, options_t& options)
543
if (options.printstatistics) {
544
if (options.enablereduction != 0) {
546
std::cout << "Size of net before structural reductions: " <<
547
builder.numberOfPlaces() << " places, " <<
548
builder.numberOfTransitions() << " transitions" << std::endl;
549
std::cout << "Size of net after structural reductions: " <<
550
builder.numberOfPlaces() - builder.RemovedPlaces() << " places, " <<
551
builder.numberOfTransitions() - builder.RemovedTransitions() << " transitions" << std::endl;
552
std::cout << "Structural reduction finished after " << builder.getReductionTime() <<
553
" seconds" << std::endl;
555
std::cout << "\nNet reduction is enabled.\n";
556
builder.printStats(std::cout);
561
void printUnfoldingStats(ColoredPetriNetBuilder& builder, options_t& options) {
562
if (options.printstatistics) {
563
if (!builder.isColored() && !builder.isUnfolded())
565
std::cout << "\nSize of colored net: " <<
566
builder.getPlaceCount() << " places, " <<
567
builder.getTransitionCount() << " transitions, and " <<
568
builder.getArcCount() << " arcs" << std::endl;
569
std::cout << "Size of unfolded net: " <<
570
builder.getUnfoldedPlaceCount() << " places, " <<
571
builder.getUnfoldedTransitionCount() << " transitions, and " <<
572
builder.getUnfoldedArcCount() << " arcs" << std::endl;
573
std::cout << "Unfolded in " << builder.getUnfoldTime() << " seconds" << std::endl;
577
std::string getXMLQueries(vector<std::shared_ptr<Condition>> queries, vector<std::string> querynames, std::vector<ResultPrinter::Result> results) {
579
for(uint32_t i = 0; i < results.size(); i++) {
580
if (results[i] == ResultPrinter::CTL) {
590
std::stringstream ss;
591
ss << "<?xml version=\"1.0\"?>\n<property-set xmlns=\"http://mcc.lip6.fr/\">\n";
593
for(uint32_t i = 0; i < queries.size(); i++) {
594
if (!(results[i] == ResultPrinter::CTL)) {
597
ss << " <property>\n <id>" << querynames[i] << "</id>\n <description>Simplified</description>\n <formula>\n";
598
queries[i]->toXML(ss, 3);
599
ss << " </formula>\n </property>\n";
602
ss << "</property-set>\n";
607
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)
613
out.open(filename, std::ios::binary | std::ios::out);
615
for(uint32_t j = 0; j < queries.size(); j++) {
616
if(queries[j]->isTriviallyTrue() || queries[j]->isTriviallyFalse()) continue;
619
out.write(reinterpret_cast<const char *>(&cnt), sizeof(uint32_t));
620
cnt = place_names.size();
621
out.write(reinterpret_cast<const char *>(&cnt), sizeof(uint32_t));
622
for(auto& kv : place_names)
624
out.write(reinterpret_cast<const char *>(&kv.second), sizeof(uint32_t));
625
out.write(kv.first.data(), kv.first.size());
626
out.write("\0", sizeof(char));
631
out.open(filename, std::ios::out);
632
out << "<?xml version=\"1.0\"?>\n<property-set xmlns=\"http://mcc.lip6.fr/\">\n";
635
for(uint32_t j = 0; j < queries.size(); j++) {
637
if(queries[i]->isTriviallyTrue() || queries[i]->isTriviallyFalse()) continue;
640
out.write(querynames[i].data(), querynames[i].size());
641
out.write("\0", sizeof(char));
642
queries[i]->toBinary(out);
646
out << " <property>\n <id>" << querynames[i] << "</id>\n <description>Simplified</description>\n <formula>\n";
647
queries[i]->toXML(out, 3);
648
out << " </formula>\n </property>\n";
654
out << "</property-set>\n";
659
int main(int argc, char* argv[]) {
663
ReturnValue v = parseOptions(argc, argv, options);
664
if(v != ContinueCode) return v;
666
srand (time(NULL) xor options.seed_offset);
667
ColoredPetriNetBuilder cpnBuilder;
668
if(parseModel(cpnBuilder, options) != ContinueCode)
670
std::cerr << "Error parsing the model" << std::endl;
673
if(options.cpnOverApprox && !cpnBuilder.isColored())
675
std::cerr << "CPN OverApproximation is only usable on colored models" << std::endl;
678
if (options.printstatistics) {
679
std::cout << "Finished parsing model" << std::endl;
682
//----------------------- Parse Query -----------------------//
683
std::vector<std::string> querynames;
684
auto queries = readQueries(options, querynames);
686
if(options.printstatistics && options.queryReductionTimeout > 0)
689
std::cout << "RWSTATS LEGEND:";
690
stats.printRules(std::cout);
691
std::cout << std::endl;
694
if(cpnBuilder.isColored())
697
EvaluationContext context(nullptr, nullptr);
698
for (ssize_t qid = queries.size() - 1; qid >= 0; --qid) {
699
queries[qid] = queries[qid]->pushNegation(stats, context, false, false, false);
700
if(options.printstatistics)
702
std::cout << "\nQuery before expansion and reduction: ";
703
queries[qid]->toString(std::cout);
704
std::cout << std::endl;
706
std::cout << "RWSTATS COLORED PRE:";
707
stats.print(std::cout);
708
std::cout << std::endl;
713
if (options.cpnOverApprox) {
714
for (ssize_t qid = queries.size() - 1; qid >= 0; --qid) {
716
EvaluationContext context(nullptr, nullptr);
717
auto q = queries[qid]->pushNegation(stats, context, false, false, false);
718
if (!q->isReachability() || q->isLoopSensitive() || q->prepareForReachability()->getQuantifier() == UPPERBOUNDS || stats.negated_fireability) {
719
std::cerr << "Warning: CPN OverApproximation is only available for Reachability queries without deadlock, negated fireability and UpperBounds, skipping " << querynames[qid] << std::endl;
720
queries.erase(queries.begin() + qid);
721
querynames.erase(querynames.begin() + qid);
726
auto builder = options.cpnOverApprox ? cpnBuilder.stripColors() : cpnBuilder.unfold();
727
printUnfoldingStats(cpnBuilder, options);
729
std::vector<ResultPrinter::Result> results(queries.size(), ResultPrinter::Result::Unknown);
730
ResultPrinter printer(&builder, &options, querynames);
732
//----------------------- Query Simplification -----------------------//
733
bool alldone = options.queryReductionTimeout > 0;
734
PetriNetBuilder b2(builder);
735
std::unique_ptr<PetriNet> qnet(b2.makePetriNet(false));
736
MarkVal* qm0 = qnet->makeInitialMarking();
737
ResultPrinter p2(&b2, &options, querynames);
739
if(queries.size() == 0 || contextAnalysis(cpnBuilder, b2, qnet.get(), queries) != ContinueCode)
741
std::cerr << "Could not analyze the queries" << std::endl;
745
if (options.strategy == PetriEngine::Reachability::OverApprox && options.queryReductionTimeout == 0)
747
// Conflicting flags "-s OverApprox" and "-q 0"
748
std::cerr << "Conflicting flags '-s OverApprox' and '-q 0'" << std::endl;
752
// simplification. We always want to do negation-push and initial marking check.
754
// simplification. We always want to do negation-push and initial marking check.
755
std::vector<LPCache> caches(options.cores);
756
std::atomic<uint32_t> to_handle(queries.size());
757
auto begin = std::chrono::high_resolution_clock::now();
758
auto end = std::chrono::high_resolution_clock::now();
759
std::vector<bool> hadTo(queries.size(), true);
763
auto qt = (options.queryReductionTimeout - std::chrono::duration_cast<std::chrono::seconds>(end - begin).count()) / ( 1 + (to_handle / options.cores));
764
if((to_handle <= options.cores || options.cores == 1) && to_handle > 0)
765
qt = (options.queryReductionTimeout - std::chrono::duration_cast<std::chrono::seconds>(end - begin).count()) / to_handle;
766
std::atomic<uint32_t> cnt(0);
767
#ifdef ENABLE_MC_SIMPLIFICATION
769
std::vector<std::thread> threads;
771
std::vector<std::stringstream> tstream(queries.size());
772
uint32_t old = to_handle;
773
for(size_t c = 0; c < std::min<uint32_t>(options.cores, old); ++c)
775
#ifdef ENABLE_MC_SIMPLIFICATION
776
threads.push_back(std::thread([&,c](){
778
auto simplify = [&,c](){
780
auto& out = tstream[c];
781
auto& cache = caches[c];
785
if(i >= queries.size()) return;
786
if(!hadTo[i]) continue;
789
EvaluationContext context(qm0, qnet.get());
790
if(options.printstatistics && options.queryReductionTimeout > 0)
792
out << "\nQuery before reduction: ";
793
queries[i]->toString(out);
797
#ifndef ENABLE_MC_SIMPLIFICATION
798
qt = (options.queryReductionTimeout - std::chrono::duration_cast<std::chrono::seconds>(end - begin).count()) / (queries.size() - i);
800
// this is used later, we already know that this is a plain reachability (or AG)
801
bool wasAGCPNApprox = dynamic_cast<NotCondition*>(queries[i].get()) != nullptr;
802
int preSize=queries[i]->formulaSize();
803
queries[i] = Condition::initialMarkingRW([&](){ return queries[i]; }, stats, context, false, false, true)
804
->pushNegation(stats, context, false, false, true);
805
wasAGCPNApprox |= dynamic_cast<NotCondition*>(queries[i].get()) != nullptr;
807
if(options.queryReductionTimeout > 0 && options.printstatistics)
809
out << "RWSTATS PRE:";
814
if (options.queryReductionTimeout > 0 && qt > 0)
816
SimplificationContext simplificationContext(qm0, qnet.get(), qt,
817
options.lpsolveTimeout, &cache);
820
queries[i] = (queries[i]->simplify(simplificationContext)).formula->pushNegation(stats, context, false, false, true);
821
wasAGCPNApprox |= dynamic_cast<NotCondition*>(queries[i].get()) != nullptr;
822
if(options.printstatistics)
824
out << "RWSTATS POST:";
828
} catch (std::bad_alloc& ba){
829
std::cerr << "Query reduction failed." << std::endl;
830
std::cerr << "Exception information: " << ba.what() << std::endl;
833
std::exit(ErrorCode);
836
if(options.printstatistics)
838
out << "\nQuery after reduction: ";
839
queries[i]->toString(out);
842
if(simplificationContext.timeout()){
843
if(options.printstatistics)
844
out << "Query reduction reached timeout.\n";
847
if(options.printstatistics)
848
out << "Query reduction finished after " << simplificationContext.getReductionTime() << " seconds.\n";
852
else if(options.printstatistics)
854
out << "Skipping linear-programming (-q 0)" << std::endl;
856
if(options.cpnOverApprox && wasAGCPNApprox)
858
if(queries[i]->isTriviallyTrue())
859
queries[i] = std::make_shared<BooleanCondition>(false);
860
else if(queries[i]->isTriviallyFalse())
861
queries[i] = std::make_shared<BooleanCondition>(true);
862
queries[i]->setInvariant(wasAGCPNApprox);
866
if(options.printstatistics)
868
int postSize=queries[i]->formulaSize();
869
double redPerc = preSize-postSize == 0 ? 0 : ((double)(preSize-postSize)/(double)preSize)*100;
870
out << "Query size reduced from " << preSize << " to " << postSize << " nodes ( " << redPerc << " percent reduction).\n";
874
#ifdef ENABLE_MC_SIMPLIFICATION
881
#ifndef ENABLE_MC_SIMPLIFICATION
882
std::cout << tstream[0].str() << std::endl;
885
for(size_t i = 0; i < std::min<uint32_t>(options.cores, old); ++i)
888
std::cout << tstream[i].str();
889
std::cout << std::endl;
892
end = std::chrono::high_resolution_clock::now();
894
} 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);
897
if(options.query_out_file.size() > 0)
899
std::vector<uint32_t> reorder(queries.size());
900
for(uint32_t i = 0; i < queries.size(); ++i) reorder[i] = i;
901
std::sort(reorder.begin(), reorder.end(), [&queries](auto a, auto b){
903
if(queries[a]->isReachability() != queries[b]->isReachability())
904
return queries[a]->isReachability() > queries[b]->isReachability();
905
if(queries[a]->isLoopSensitive() != queries[b]->isLoopSensitive())
906
return queries[a]->isLoopSensitive() < queries[b]->isLoopSensitive();
907
if(queries[a]->containsNext() != queries[b]->containsNext())
908
return queries[a]->containsNext() < queries[b]->containsNext();
909
return queries[a]->formulaSize() < queries[b]->formulaSize();
911
writeQueries(queries, querynames, reorder, options.query_out_file, options.binary_query_io & 2, builder.getPlaceNames());
917
if (!options.statespaceexploration){
918
for(size_t i = 0; i < queries.size(); ++i)
920
if(queries[i]->isTriviallyTrue()){
921
results[i] = p2.printResult(i, queries[i].get(), ResultPrinter::Satisfied);
922
if(results[i] == ResultPrinter::Ignore && options.printstatistics)
924
std::cout << "Unable to decide if query is satisfied." << std::endl << std::endl;
926
else if (options.printstatistics) {
927
std::cout << "Query solved by Query Simplification." << std::endl << std::endl;
929
} else if (queries[i]->isTriviallyFalse()) {
930
results[i] = p2.printResult(i, queries[i].get(), ResultPrinter::NotSatisfied);
931
if(results[i] == ResultPrinter::Ignore && options.printstatistics)
933
std::cout << "Unable to decide if query is satisfied." << std::endl << std::endl;
935
else if (options.printstatistics) {
936
std::cout << "Query solved by Query Simplification." << std::endl << std::endl;
938
} else if (options.strategy == PetriEngine::Reachability::OverApprox){
939
results[i] = p2.printResult(i, queries[i].get(), ResultPrinter::Unknown);
940
if (options.printstatistics) {
941
std::cout << "Unable to decide if query is satisfied." << std::endl << std::endl;
943
} else if (!queries[i]->isReachability()) {
944
results[i] = ResultPrinter::CTL;
947
queries[i] = queries[i]->prepareForReachability();
952
if(alldone && options.model_out_file.size() == 0) return SuccessCode;
955
options.queryReductionTimeout = 0;
957
//--------------------- Apply Net Reduction ---------------//
959
if (options.enablereduction == 1 || options.enablereduction == 2) {
960
// Compute how many times each place appears in the query
961
builder.startTimer();
962
builder.reduce(queries, results, options.enablereduction, options.trace, nullptr, options.reductionTimeout);
963
printer.setReducer(builder.getReducer());
966
printStats(builder, options);
968
auto net = std::unique_ptr<PetriNet>(builder.makePetriNet());
970
if(options.model_out_file.size() > 0)
973
file.open(options.model_out_file, std::ios::out);
977
if(alldone) return SuccessCode;
979
//----------------------- Verify CTL queries -----------------------//
980
std::vector<size_t> ctl_ids;
981
for(size_t i = 0; i < queries.size(); ++i)
983
if(results[i] == ResultPrinter::CTL)
985
ctl_ids.push_back(i);
989
if (ctl_ids.size() > 0) {
991
PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;
994
if(queries.size() == 0 || contextAnalysis(cpnBuilder, builder, net.get(), queries) != ContinueCode)
996
std::cerr << "An error occurred while assigning indexes" << std::endl;
999
if(options.strategy == DEFAULT) options.strategy = PetriEngine::Reachability::DFS;
1000
v = CTLMain(net.get(),
1001
options.ctlalgorithm,
1004
options.printstatistics,
1006
options.stubbornreduction,
1012
if (std::find(results.begin(), results.end(), ResultPrinter::Unknown) == results.end()) {
1015
// go back to previous strategy if the program continues
1016
options.strategy=reachabilityStrategy;
1018
options.isctl=false;
1020
//----------------------- Siphon Trap ------------------------//
1022
if(options.siphontrapTimeout > 0){
1023
for (uint32_t i = 0; i < results.size(); i ++) {
1024
bool isDeadlockQuery = std::dynamic_pointer_cast<DeadlockCondition>(queries[i]) != nullptr;
1026
if (results[i] == ResultPrinter::Unknown && isDeadlockQuery) {
1027
STSolver stSolver(printer, *net, queries[i].get(), options.siphonDepth);
1028
stSolver.Solve(options.siphontrapTimeout);
1029
results[i] = stSolver.PrintResult();
1030
if (results[i] == Reachability::ResultPrinter::NotSatisfied && options.printstatistics) {
1031
std::cout << "Query solved by Siphon-Trap Analysis." << std::endl << std::endl;
1033
if(options.printstatistics){
1034
stSolver.PrintStatistics();
1039
if (std::find(results.begin(), results.end(), ResultPrinter::Unknown) == results.end()) {
1043
options.siphontrapTimeout = 0;
1045
//----------------------- Reachability -----------------------//
1047
//Analyse context again to reindex query
1048
contextAnalysis(cpnBuilder, builder, net.get(), queries);
1050
// Change default place-holder to default strategy
1051
if(options.strategy == DEFAULT) options.strategy = PetriEngine::Reachability::HEUR;
1056
//Create reachability search strategy
1057
TARReachabilitySearch strategy(printer, *net, builder.getReducer(), options.kbound);
1059
// Change default place-holder to default strategy
1060
fprintf(stdout, "Search strategy option was ignored as the TAR engine is called.\n");
1061
options.strategy = PetriEngine::Reachability::DFS;
1063
//Reachability search
1064
strategy.reachable(queries, results,
1065
options.printstatistics,
1071
ReachabilitySearch strategy(printer, *net, options.kbound);
1073
// Change default place-holder to default strategy
1074
if(options.strategy == DEFAULT) options.strategy = PetriEngine::Reachability::HEUR;
1076
//Reachability search
1077
strategy.reachable(queries, results,
1079
options.stubbornreduction,
1080
options.statespaceexploration,
1081
options.printstatistics,
added
removed
VerifyPN.cpp
