~tapaal-ltl/verifypn/answer-for-gui

« back to all changes in this revision

Viewing changes to src/PetriParse/PNMLParser.cpp

  • Committer: srba.jiri at gmail
  • Date: 2021-04-02 18:13:50 UTC
  • mfrom: (230.1.28 mcc2021)
  • Revision ID: srba.jiri@gmail.com-20210402181350-k71xtjut3r48l1o5
merged in lp:~tapaal-ltl/verifypn/mcc2021 adding LTL, colored fixed-point unfolding for CPN and other performance improvements

Show diffs side-by-side

added added

removed removed

Lines of Context:
30
30
#include "PetriEngine/errorcodes.h"
31
31
 
32
32
using namespace PetriEngine;
33
 
using namespace std;
34
33
using namespace PetriEngine::PQL;
35
34
 
36
 
void PNMLParser::parse(ifstream& xml,
 
35
void PNMLParser::parse(std::ifstream& xml,
37
36
        AbstractPetriNetBuilder* builder) {
38
37
    //Clear any left overs
39
38
    id2name.clear();
47
46
 
48
47
    //Parser the xml
49
48
    rapidxml::xml_document<> doc;
50
 
    vector<char> buffer((istreambuf_iterator<char>(xml)), istreambuf_iterator<char>());
 
49
    std::vector<char> buffer((std::istreambuf_iterator<char>(xml)), std::istreambuf_iterator<char>());
51
50
    buffer.push_back('\0');
52
51
    doc.parse<0>(&buffer[0]);
53
52
    
183
182
                ((PetriEngine::Colored::ProductType*)ct)->addType(colorTypes[it->first_attribute("declaration")->value()]);
184
183
            }
185
184
        }
186
 
    } else {
 
185
    } else if (strcmp(type->name(), "finiteintrange") == 0) {   
 
186
                uint32_t start = (uint32_t)atoll(type->first_attribute("start")->value());      
 
187
                uint32_t end = (uint32_t)atoll(type->first_attribute("end")->value());  
 
188
        
 
189
                for (uint32_t i = start; i<=end;i++) {  
 
190
                        ct->addColor(std::to_string(i).c_str());        
 
191
                }       
 
192
        } else {
187
193
        for (auto it = type->first_node(); it; it = it->next_sibling()) {
188
194
            auto id = it->first_attribute("id");
189
195
            assert(id != nullptr);
222
228
        return parseNumberOfExpression(element->parent());
223
229
    } else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {
224
230
        return parseArcExpression(element->first_node());
225
 
    }
 
231
    } else if (strcmp(element->name(), "tuple") == 0) { 
 
232
                std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors;    
 
233
                collectColorsInTuple(element, collectedColors); 
 
234
                auto expr = constructAddExpressionFromTupleExpression(element, collectedColors);        
 
235
                std::cout << expr->toString() << std::endl;     
 
236
                return expr;    
 
237
        }
226
238
    printf("Could not parse '%s' as an arc expression\n", element->name());
227
239
    assert(false);
228
240
    return nullptr;
229
241
}
230
242
 
231
 
PetriEngine::Colored::GuardExpression_ptr PNMLParser::parseGuardExpression(rapidxml::xml_node<>* element) {
232
 
    if (strcmp(element->name(), "lt") == 0 || strcmp(element->name(), "lessthan") == 0) {
233
 
        auto left = element->first_node();
234
 
        auto right = left->next_sibling();
235
 
        return std::make_shared<PetriEngine::Colored::LessThanExpression>(parseColorExpression(left), parseColorExpression(right));
236
 
    } else if (strcmp(element->name(), "gt") == 0 || strcmp(element->name(), "greaterthan") == 0) {
237
 
        auto left = element->first_node();
238
 
        auto right = left->next_sibling();
239
 
        return std::make_shared<PetriEngine::Colored::GreaterThanExpression>(parseColorExpression(left), parseColorExpression(right));
240
 
    } else if (strcmp(element->name(), "leq") == 0 || strcmp(element->name(), "lessthanorequal") == 0) {
241
 
        auto left = element->first_node();
242
 
        auto right = left->next_sibling();
243
 
        return std::make_shared<PetriEngine::Colored::LessThanEqExpression>(parseColorExpression(left), parseColorExpression(right));
244
 
    } else if (strcmp(element->name(), "geq") == 0 || strcmp(element->name(), "greaterthanorequal") == 0) {
245
 
        auto left = element->first_node();
246
 
        auto right = left->next_sibling();
247
 
        return std::make_shared<PetriEngine::Colored::GreaterThanEqExpression>(parseColorExpression(left), parseColorExpression(right));
248
 
    } else if (strcmp(element->name(), "eq") == 0 || strcmp(element->name(), "equality") == 0) {
249
 
        auto left = element->first_node();
250
 
        auto right = left->next_sibling();
251
 
        return std::make_shared<PetriEngine::Colored::EqualityExpression>(parseColorExpression(left), parseColorExpression(right));
252
 
    } else if (strcmp(element->name(), "neq") == 0 || strcmp(element->name(), "inequality") == 0) {
253
 
        auto left = element->first_node();
254
 
        auto right = left->next_sibling();
255
 
        return std::make_shared<PetriEngine::Colored::InequalityExpression>(parseColorExpression(left), parseColorExpression(right));
256
 
    } else if (strcmp(element->name(), "not") == 0) {
257
 
        return std::make_shared<PetriEngine::Colored::NotExpression>(parseGuardExpression(element->first_node()));
258
 
    } else if (strcmp(element->name(), "and") == 0) {
259
 
        auto left = element->first_node();
260
 
        auto right = left->next_sibling();
261
 
        return std::make_shared<PetriEngine::Colored::AndExpression>(parseGuardExpression(left), parseGuardExpression(right));
262
 
    } else if (strcmp(element->name(), "or") == 0) {
263
 
        auto left = element->first_node();
264
 
        auto right = left->next_sibling();
265
 
        return std::make_shared<PetriEngine::Colored::OrExpression>(parseGuardExpression(left), parseGuardExpression(right));
266
 
    } else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {
267
 
        return parseGuardExpression(element->first_node());
268
 
    }
269
 
    
270
 
    printf("Could not parse '%s' as a guard expression\n", element->name());
271
 
    assert(false);
272
 
    return nullptr;
 
243
PetriEngine::Colored::ArcExpression_ptr PNMLParser::constructAddExpressionFromTupleExpression(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors){       
 
244
        auto initCartesianSet = cartesianProduct(collectedColors[0], collectedColors[1]);       
 
245
        for(uint32_t i = 2; i < collectedColors.size(); i++){   
 
246
                initCartesianSet = cartesianProduct(initCartesianSet, collectedColors[i]);      
 
247
        }       
 
248
        std::vector<PetriEngine::Colored::NumberOfExpression_ptr> numberOfExpressions;  
 
249
        for(auto set : initCartesianSet){       
 
250
                std::vector<PetriEngine::Colored::ColorExpression_ptr> colors;  
 
251
                for (auto color : set) {        
 
252
                        colors.push_back(color);        
 
253
                }       
 
254
                std::shared_ptr<PetriEngine::Colored::TupleExpression> tupleExpr = std::make_shared<PetriEngine::Colored::TupleExpression>(std::move(colors));  
 
255
                tupleExpr->setColorType(tupleExpr->getColorType(colorTypes));   
 
256
                std::vector<PetriEngine::Colored::ColorExpression_ptr> placeholderVector;       
 
257
                placeholderVector.push_back(tupleExpr); 
 
258
                numberOfExpressions.push_back(std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(placeholderVector),1));      
 
259
        }       
 
260
        std::vector<PetriEngine::Colored::ArcExpression_ptr> constituents;      
 
261
        for (auto expr : numberOfExpressions) { 
 
262
                constituents.push_back(expr);   
 
263
        }       
 
264
        return std::make_shared<PetriEngine::Colored::AddExpression>(std::move(constituents));  
 
265
}       
 
266
        
 
267
std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> PNMLParser::cartesianProduct(std::vector<PetriEngine::Colored::ColorExpression_ptr> rightSet, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftSet){      
 
268
        std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> returnSet;  
 
269
        for(auto expr : rightSet){      
 
270
                for(auto expr2 : leftSet){      
 
271
                        std::vector<PetriEngine::Colored::ColorExpression_ptr> toAdd;   
 
272
                        toAdd.push_back(expr);  
 
273
                        toAdd.push_back(expr2); 
 
274
                        returnSet.push_back(toAdd);     
 
275
                }       
 
276
        }       
 
277
        return returnSet;       
 
278
}       
 
279
std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> PNMLParser::cartesianProduct(std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> rightSet, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftSet){ 
 
280
        std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> returnSet;  
 
281
        for(auto set : rightSet){       
 
282
                for(auto expr2 : leftSet){      
 
283
                        set.push_back(expr2);   
 
284
                        returnSet.push_back(set);       
 
285
                }       
 
286
        }       
 
287
        return returnSet;       
 
288
}       
 
289
        
 
290
void PNMLParser::collectColorsInTuple(rapidxml::xml_node<>* element, std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>>& collectedColors){     
 
291
        if (strcmp(element->name(), "tuple") == 0) {    
 
292
                for (auto it = element->first_node(); it; it = it->next_sibling()) {    
 
293
                        collectColorsInTuple(it->first_node(), collectedColors);        
 
294
                }       
 
295
        } else if (strcmp(element->name(), "all") == 0) {       
 
296
                std::vector<PetriEngine::Colored::ColorExpression_ptr> expressionsToAdd;        
 
297
                auto expr = parseAllExpression(element);        
 
298
                std::unordered_map<uint32_t, std::vector<const PetriEngine::Colored::Color *>> constantMap;     
 
299
                uint32_t index = 0;     
 
300
                expr->getConstants(constantMap, index); 
 
301
                for(auto positionColors : constantMap){ 
 
302
                        for(auto color : positionColors.second){        
 
303
                                expressionsToAdd.push_back(std::make_shared<PetriEngine::Colored::UserOperatorExpression>(color));      
 
304
                        }               
 
305
                }       
 
306
                collectedColors.push_back(expressionsToAdd);    
 
307
                return; 
 
308
        } else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {      
 
309
                collectColorsInTuple(element->first_node(), collectedColors);   
 
310
        } else if (strcmp(element->name(), "userOperator") == 0 || strcmp(element->name(), "dotconstant") == 0 || strcmp(element->name(), "variable") == 0      
 
311
                                        || strcmp(element->name(), "successor") == 0 || strcmp(element->name(), "predecessor") == 0) {  
 
312
                std::vector<PetriEngine::Colored::ColorExpression_ptr> expressionsToAdd;        
 
313
                auto color = parseColorExpression(element);     
 
314
                expressionsToAdd.push_back(color);      
 
315
                collectedColors.push_back(expressionsToAdd);    
 
316
                return; 
 
317
        } else{ 
 
318
                printf("Could not parse '%s' as an arc expression\n", element->name()); 
 
319
                return; 
 
320
        }       
 
321
}       
 
322
        
 
323
PetriEngine::Colored::GuardExpression_ptr PNMLParser::parseGuardExpression(rapidxml::xml_node<>* element, bool notFlag) {       
 
324
        if (strcmp(element->name(), "lt") == 0 || strcmp(element->name(), "lessthan") == 0) {   
 
325
                auto left = element->first_node();      
 
326
                auto right = left->next_sibling();      
 
327
                if(notFlag){
 
328
                        return std::make_shared<PetriEngine::Colored::GreaterThanEqExpression>(parseColorExpression(left), parseColorExpression(right));
 
329
                } else {
 
330
                        return std::make_shared<PetriEngine::Colored::LessThanExpression>(parseColorExpression(left), parseColorExpression(right));
 
331
                }                       
 
332
        } else if (strcmp(element->name(), "gt") == 0 || strcmp(element->name(), "greaterthan") == 0) { 
 
333
                auto left = element->first_node();      
 
334
                auto right = left->next_sibling();
 
335
 
 
336
                if(notFlag){
 
337
                        return std::make_shared<PetriEngine::Colored::LessThanEqExpression>(parseColorExpression(left), parseColorExpression(right));
 
338
                } else {
 
339
                        return std::make_shared<PetriEngine::Colored::GreaterThanExpression>(parseColorExpression(left), parseColorExpression(right));
 
340
                }                       
 
341
        } else if (strcmp(element->name(), "leq") == 0 || strcmp(element->name(), "lessthanorequal") == 0) {    
 
342
                auto left = element->first_node();      
 
343
                auto right = left->next_sibling();      
 
344
 
 
345
                if(notFlag){
 
346
                        return std::make_shared<PetriEngine::Colored::GreaterThanExpression>(parseColorExpression(left), parseColorExpression(right));
 
347
                } else {
 
348
                        return std::make_shared<PetriEngine::Colored::LessThanEqExpression>(parseColorExpression(left), parseColorExpression(right));
 
349
                }                       
 
350
        } else if (strcmp(element->name(), "geq") == 0 || strcmp(element->name(), "greaterthanorequal") == 0) { 
 
351
                auto left = element->first_node();      
 
352
                auto right = left->next_sibling();
 
353
 
 
354
                if(notFlag){
 
355
                        return std::make_shared<PetriEngine::Colored::LessThanExpression>(parseColorExpression(left), parseColorExpression(right));
 
356
                } else {
 
357
                        return std::make_shared<PetriEngine::Colored::GreaterThanEqExpression>(parseColorExpression(left), parseColorExpression(right));
 
358
                }       
 
359
        } else if (strcmp(element->name(), "eq") == 0 || strcmp(element->name(), "equality") == 0) {    
 
360
                auto left = element->first_node();      
 
361
                auto right = left->next_sibling();      
 
362
                if(notFlag) {
 
363
                        return std::make_shared<PetriEngine::Colored::InequalityExpression>(parseColorExpression(left), parseColorExpression(right));
 
364
                } else {
 
365
                        return std::make_shared<PetriEngine::Colored::EqualityExpression>(parseColorExpression(left), parseColorExpression(right));
 
366
                }       
 
367
        } else if (strcmp(element->name(), "neq") == 0 || strcmp(element->name(), "inequality") == 0) { 
 
368
                auto left = element->first_node();      
 
369
                auto right = left->next_sibling();      
 
370
 
 
371
                if(notFlag){
 
372
                        return std::make_shared<PetriEngine::Colored::EqualityExpression>(parseColorExpression(left), parseColorExpression(right));
 
373
                } else {
 
374
                        return std::make_shared<PetriEngine::Colored::InequalityExpression>(parseColorExpression(left), parseColorExpression(right));
 
375
                }                       
 
376
        } else if (strcmp(element->name(), "not") == 0) {       
 
377
                return parseGuardExpression(element->first_node(), true);       
 
378
        } else if (strcmp(element->name(), "and") == 0) {       
 
379
                auto left = element->first_node();      
 
380
                auto right = left->next_sibling();
 
381
                if(notFlag){
 
382
                        return std::make_shared<PetriEngine::Colored::OrExpression>(parseGuardExpression(left, true), parseGuardExpression(right, true));
 
383
                } else {
 
384
                        return std::make_shared<PetriEngine::Colored::AndExpression>(parseGuardExpression(left, false), parseGuardExpression(right, false));
 
385
                }                       
 
386
        } else if (strcmp(element->name(), "or") == 0) {        
 
387
                auto left = element->first_node();      
 
388
                auto right = left->next_sibling();      
 
389
                //There must only be one constituent
 
390
                if(right == nullptr){
 
391
                        return parseGuardExpression(left, notFlag);
 
392
                }
 
393
                if(notFlag) {
 
394
                        auto parentAnd = std::make_shared<PetriEngine::Colored::AndExpression>(parseGuardExpression(left, true), parseGuardExpression(right, true));    
 
395
                        for (auto it = right->next_sibling(); it; it = it->next_sibling()) {    
 
396
                                parentAnd = std::make_shared<PetriEngine::Colored::AndExpression>(parentAnd, parseGuardExpression(it, true));   
 
397
                        }       
 
398
                        return parentAnd;
 
399
                } else {
 
400
                        auto parentOr = std::make_shared<PetriEngine::Colored::OrExpression>(parseGuardExpression(left, false), parseGuardExpression(right, false));    
 
401
                        for (auto it = right->next_sibling(); it; it = it->next_sibling()) {    
 
402
                                parentOr = std::make_shared<PetriEngine::Colored::OrExpression>(parentOr, parseGuardExpression(it, false));     
 
403
                        }       
 
404
                        return parentOr;
 
405
                }                       
 
406
        } else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {      
 
407
                return parseGuardExpression(element->first_node(), notFlag);    
 
408
        }       
 
409
                
 
410
        printf("Could not parse '%s' as a guard expression\n", element->name());        
 
411
        assert(false);  
 
412
        return nullptr; 
273
413
}
274
414
 
275
415
PetriEngine::Colored::ColorExpression_ptr PNMLParser::parseColorExpression(rapidxml::xml_node<>* element) {
283
423
        return std::make_shared<PetriEngine::Colored::SuccessorExpression>(parseColorExpression(element->first_node()));
284
424
    } else if (strcmp(element->name(), "predecessor") == 0) {
285
425
        return std::make_shared<PetriEngine::Colored::PredecessorExpression>(parseColorExpression(element->first_node()));
286
 
    } else if (strcmp(element->name(), "tuple") == 0) {
 
426
    } else if (strcmp(element->name(), "finiteintrangeconstant") == 0){ 
 
427
                auto value = element->first_attribute("value")->value();        
 
428
                auto intRangeElement = element->first_node("finiteintrange");   
 
429
                uint32_t start = (uint32_t)atoll(intRangeElement->first_attribute("start")->value());   
 
430
                uint32_t end = (uint32_t)atoll(intRangeElement->first_attribute("end")->value());       
 
431
                return std::make_shared<PetriEngine::Colored::UserOperatorExpression>(findColorForIntRange(value, start,end));  
 
432
        
 
433
        } else if (strcmp(element->name(), "tuple") == 0) {
287
434
        std::vector<PetriEngine::Colored::ColorExpression_ptr> colors;
288
435
        for (auto it = element->first_node(); it; it = it->next_sibling()) {
289
436
            colors.push_back(parseColorExpression(it));
290
437
        }
291
 
        return std::make_shared<PetriEngine::Colored::TupleExpression>(std::move(colors));
 
438
        std::shared_ptr<PetriEngine::Colored::TupleExpression> tupleExpr = std::make_shared<PetriEngine::Colored::TupleExpression>(std::move(colors));  
 
439
                tupleExpr->setColorType(tupleExpr->getColorType(colorTypes));   
 
440
                return tupleExpr;
292
441
    } else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {
293
442
        return parseColorExpression(element->first_node());
294
443
    }
379
528
}
380
529
 
381
530
void PNMLParser::parseQueries(rapidxml::xml_node<>* element) {
382
 
    string query;
 
531
    std::string query;
383
532
 
384
533
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
385
 
        string name(element->first_attribute("name")->value());
 
534
        std::string name(element->first_attribute("name")->value());
386
535
        parseValue(element, query);
387
536
        Query q;
388
537
        q.name = name;
393
542
 
394
543
void PNMLParser::parsePlace(rapidxml::xml_node<>* element) {
395
544
    double x = 0, y = 0;
396
 
    string id(element->first_attribute("id")->value());
 
545
    std::string id(element->first_attribute("id")->value());
397
546
    
398
547
    auto initial = element->first_attribute("initialMarking");
399
548
    long long initialMarking = 0;
407
556
        if (strcmp(it->name(), "graphics") == 0) {
408
557
            parsePosition(it, x, y);
409
558
        } else if (strcmp(it->name(),"initialMarking") == 0) {
410
 
            string text;
 
559
            std::string text;
411
560
            parseValue(it, text);
412
561
            initialMarking = atoll(text.c_str());
413
562
        } else if (strcmp(it->name(),"hlinitialMarking") == 0) {
414
 
            std::unordered_map<std::string, const PetriEngine::Colored::Color*> binding;
 
563
            std::unordered_map<const PetriEngine::Colored::Variable*, const PetriEngine::Colored::Color*> binding;
415
564
            PetriEngine::Colored::ExpressionContext context {binding, colorTypes};
416
565
            hlinitialMarking = parseArcExpression(it->first_node("structure"))->eval(context);
417
566
        } else if (strcmp(it->name(), "type") == 0) {
445
594
}
446
595
 
447
596
void PNMLParser::parseArc(rapidxml::xml_node<>* element, bool inhibitor) {
448
 
    string source = element->first_attribute("source")->value(),
 
597
    std::string source = element->first_attribute("source")->value(),
449
598
            target = element->first_attribute("target")->value();
450
599
    int weight = 1;
451
600
    auto type = element->first_attribute("type");
461
610
 
462
611
    bool first = true;
463
612
    for (auto it = element->first_node("inscription"); it; it = it->next_sibling("inscription")) {
464
 
        string text;
 
613
        std::string text;
465
614
        parseValue(it, text);
466
615
        weight = atoi(text.c_str());
467
616
        if(std::find_if(text.begin(), text.end(), [](char c) { return !std::isdigit(c) && !std::isblank(c); }) != text.end())
523
672
}
524
673
 
525
674
void PNMLParser::parseTransportArc(rapidxml::xml_node<>* element){
526
 
    string source       = element->first_attribute("source")->value(),
 
675
    std::string source  = element->first_attribute("source")->value(),
527
676
           transiton    = element->first_attribute("transition")->value(),
528
677
           target       = element->first_attribute("target")->value();
529
678
    int weight = 1;
530
679
 
531
680
    for(auto it = element->first_node("inscription"); it; it = it->next_sibling("inscription")){
532
 
        string text;
 
681
        std::string text;
533
682
        parseValue(it, text);
534
683
        weight = atoi(text.c_str());
535
684
    }
560
709
        if (strcmp(it->name(), "graphics") == 0) {
561
710
            parsePosition(it, t.x, t.y);
562
711
        } else if (strcmp(it->name(), "condition") == 0) {
563
 
            t.expr = parseGuardExpression(it->first_node("structure"));
 
712
            t.expr = parseGuardExpression(it->first_node("structure"), false);
564
713
        } else if (strcmp(it->name(), "conditions") == 0) {
565
714
            std::cerr << "conditions not supported" << std::endl;
566
715
            exit(ErrorCode);
578
727
    id2name[t.id] = nn;
579
728
}
580
729
 
581
 
void PNMLParser::parseValue(rapidxml::xml_node<>* element, string& text) {
 
730
void PNMLParser::parseValue(rapidxml::xml_node<>* element, std::string& text) {
582
731
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
583
732
        if (strcmp(it->name(), "value") == 0 || strcmp(it->name(), "text") == 0) {
584
733
            text = it->value();
618
767
    printf("Could not find color: %s\nCANNOT_COMPUTE\n", name);
619
768
    exit(ErrorCode);
620
769
}
 
770
 
 
771
const PetriEngine::Colored::Color* PNMLParser::findColorForIntRange(const char* value, uint32_t start, uint32_t end) const{     
 
772
        for (const auto& elem : colorTypes) {   
 
773
                auto col = (*elem.second)[value];       
 
774
                if (col){       
 
775
                        if((*elem.second).operator[](0).getId() == (start -1) && (*elem.second).operator[]((*elem.second).size()-1).getId() == end -1)  
 
776
                                return col;     
 
777
                }       
 
778
        }       
 
779
        printf("Could not find color: %s\nCANNOT_COMPUTE\n", value);    
 
780
        exit(ErrorCode);        
 
781
}
 
 
b'\\ No newline at end of file'