← Back to branch summary

~tapaal-contributor/verifypn/Fix-partition-id-clash-1939939

« back to all changes in this revision

Viewing changes to src/PetriParse/PNMLParser.cpp

  • Committer: srba.jiri at gmail
  • Date: 2021-07-07 12:02:50 UTC
  • mfrom: (233.1.63 update-parser)
  • Revision ID: srba.jiri@gmail.com-20210707120250-f86fv0m9ycbge3qs
merged in lp:~tapaal-contributor/verifypn/update-parser improving CPN unfodling and refactoring the code, fixing parser

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/PetriParse/PNMLParser.cpp
38
38
    id2name.clear();
39
39
    arcs.clear();
40
40
    transitions.clear();
41
 
    inhibarcs.clear();
42
41
    colorTypes.clear();
43
42
 
44
43
    //Set the builder
57
56
        exit(ErrorCode);
58
57
    }
59
58
    
60
 
    auto declarations = root->first_node("net")->first_node("declaration");
 
59
    auto declarations = root->first_node("declaration");
 
60
    if(declarations == nullptr){
 
61
        declarations = root->first_node("net")->first_node("declaration");
 
62
    }
 
63
 
61
64
    isColored = declarations != nullptr;
62
65
    if (isColored) {
63
66
        builder->enableColors();
64
67
        parseDeclarations(declarations);
65
68
    }
 
69
 
66
70
    parseElement(root);
67
71
 
68
72
    //Add all the transition
97
101
 
98
102
        if (source.isPlace && !target.isPlace) {
99
103
            if (!isColored) {
100
 
                builder->addInputArc(source.id, target.id, false, arc.weight);
 
104
                builder->addInputArc(source.id, target.id, arc.inhib, arc.weight);
101
105
            } else {
102
 
                builder->addInputArc(source.id, target.id, arc.expr);
 
106
                builder->addInputArc(source.id, target.id, arc.expr, arc.inhib, arc.weight);
103
107
            }
104
108
 
105
109
        } else if (!source.isPlace && target.isPlace) {
115
119
                    target.id.c_str());
116
120
        }
117
121
    }
118
 
 
119
 
    for(Arc& inhibitor : inhibarcs)
120
 
    {
121
 
        NodeName source = id2name[inhibitor.source];
122
 
        NodeName target = id2name[inhibitor.target];
123
 
        if (source.isPlace && !target.isPlace) {
124
 
            builder->addInputArc(source.id, target.id, true, inhibitor.weight);
125
 
        }
126
 
        else
127
 
        {
128
 
            fprintf(stderr,
129
 
                    "XML Parsing error: Inhibitor from \"%s\" to \"%s\" is not valid!\n",
130
 
                    source.id.c_str(),
131
 
                    target.id.c_str());
132
 
        }
133
 
    }
134
122
    
135
123
    //Unset the builder
136
124
    this->builder = nullptr;
139
127
    id2name.clear();
140
128
    arcs.clear();
141
129
    transitions.clear();
142
 
    inhibarcs.clear();
143
130
    colorTypes.clear();
144
131
    builder->sort();
145
132
}
195
182
 
196
183
void PNMLParser::parseNamedSort(rapidxml::xml_node<>* element) {
197
184
    auto type = element->first_node();
198
 
    auto ct = strcmp(type->name(), "productsort") == 0 ?
199
 
              new PetriEngine::Colored::ProductType(std::string(element->first_attribute("id")->value())) :
200
 
              new PetriEngine::Colored::ColorType(std::string(element->first_attribute("id")->value()));
201
 
    
 
185
    const PetriEngine::Colored::ColorType* fct = nullptr;
202
186
    if (strcmp(type->name(), "dot") == 0) {
203
 
        ct->addDot();
204
 
    } else if (strcmp(type->name(), "productsort") == 0) {
205
 
        bool missingType = false;
206
 
        for (auto it = type->first_node(); it; it = it->next_sibling()) {
207
 
            if (strcmp(it->name(), "usersort") == 0) {
208
 
                auto ctName = it->first_attribute("declaration")->value();
209
 
                if(!missingType && colorTypes.count(ctName)){
210
 
                    ((PetriEngine::Colored::ProductType*)ct)->addType(colorTypes[ctName]);
211
 
                } else {
212
 
                    missingType = true;
213
 
                    missingCTs.push_back(std::make_pair(ctName, (PetriEngine::Colored::ProductType*)ct));
214
 
                }                
215
 
            }
216
 
        }
217
 
    } else if (strcmp(type->name(), "finiteintrange") == 0) {   
218
 
                uint32_t start = (uint32_t)atoll(type->first_attribute("start")->value());      
219
 
                uint32_t end = (uint32_t)atoll(type->first_attribute("end")->value());  
220
 
        
221
 
                for (uint32_t i = start; i<=end;i++) {  
222
 
                        ct->addColor(std::to_string(i).c_str());        
223
 
                }       
224
 
        } else {
225
 
        for (auto it = type->first_node(); it; it = it->next_sibling()) {
226
 
            auto id = it->first_attribute("id");
227
 
            assert(id != nullptr);
228
 
            ct->addColor(id->value());
 
187
        fct = Colored::ColorType::dotInstance();
 
188
    } 
 
189
    else
 
190
    {
 
191
        if (strcmp(type->name(), "productsort") == 0) {
 
192
            auto ct = new PetriEngine::Colored::ProductType(std::string(element->first_attribute("id")->value()));
 
193
            bool missingType = false;
 
194
            for (auto it = type->first_node(); it; it = it->next_sibling()) {
 
195
                if (strcmp(it->name(), "usersort") == 0) {
 
196
                    auto ctName = it->first_attribute("declaration")->value();
 
197
                    if(!missingType && colorTypes.count(ctName)){
 
198
                        ct->addType(colorTypes[ctName]);
 
199
                    } else {
 
200
                        missingType = true;
 
201
                        missingCTs.push_back(std::make_pair(ctName, ct));
 
202
                    }                
 
203
                }
 
204
            }
 
205
            fct = ct;
 
206
        } 
 
207
        else
 
208
        {
 
209
            auto ct = new PetriEngine::Colored::ColorType(std::string(element->first_attribute("id")->value()));
 
210
            if (strcmp(type->name(), "finiteintrange") == 0) {
 
211
 
 
212
                uint32_t start = (uint32_t)atoll(type->first_attribute("start")->value());
 
213
                uint32_t end = (uint32_t)atoll(type->first_attribute("end")->value());
 
214
 
 
215
                for (uint32_t i = start; i<=end;i++) {
 
216
                    ct->addColor(std::to_string(i).c_str());
 
217
                }
 
218
                fct = ct;
 
219
            } else {
 
220
                for (auto it = type->first_node(); it; it = it->next_sibling()) {
 
221
                    auto id = it->first_attribute("id");
 
222
                    assert(id != nullptr);
 
223
                    ct->addColor(id->value());
 
224
                }
 
225
            }
 
226
            fct = ct;
229
227
        }
230
228
    }
231
229
 
232
230
    std::string id = element->first_attribute("id")->value();
233
 
    colorTypes[id] = ct;
234
 
    builder->addColorType(id, ct);
 
231
    colorTypes[id] = fct;
 
232
    builder->addColorType(id, fct);
235
233
}
236
234
 
237
235
PetriEngine::Colored::ArcExpression_ptr PNMLParser::parseArcExpression(rapidxml::xml_node<>* element) {
272
270
}
273
271
 
274
272
PetriEngine::Colored::ArcExpression_ptr PNMLParser::constructAddExpressionFromTupleExpression(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors, uint32_t numberof){    
275
 
        auto initCartesianSet = cartesianProduct(collectedColors[0], collectedColors[1]);       
276
 
        for(uint32_t i = 2; i < collectedColors.size(); i++){   
277
 
                initCartesianSet = cartesianProduct(initCartesianSet, collectedColors[i]);      
278
 
        }       
279
 
        std::vector<PetriEngine::Colored::NumberOfExpression_ptr> numberOfExpressions;  
280
 
        for(auto set : initCartesianSet){       
281
 
                std::vector<PetriEngine::Colored::ColorExpression_ptr> colors;  
282
 
                for (auto color : set) {        
283
 
                        colors.push_back(color);        
284
 
                }       
285
 
                std::shared_ptr<PetriEngine::Colored::TupleExpression> tupleExpr = std::make_shared<PetriEngine::Colored::TupleExpression>(std::move(colors));  
286
 
                tupleExpr->setColorType(tupleExpr->getColorType(colorTypes));   
287
 
                std::vector<PetriEngine::Colored::ColorExpression_ptr> placeholderVector;       
288
 
                placeholderVector.push_back(tupleExpr); 
289
 
                numberOfExpressions.push_back(std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(placeholderVector),numberof));       
290
 
        }       
291
 
        std::vector<PetriEngine::Colored::ArcExpression_ptr> constituents;      
292
 
        for (auto expr : numberOfExpressions) { 
293
 
                constituents.push_back(expr);   
294
 
        }       
295
 
        return std::make_shared<PetriEngine::Colored::AddExpression>(std::move(constituents));  
 
273
    std::vector<PetriEngine::Colored::ArcExpression_ptr> numberOfExpressions;   
 
274
    if(collectedColors.size() < 2){
 
275
        for(auto exp : collectedColors[0]){
 
276
            std::vector<PetriEngine::Colored::ColorExpression_ptr> colors;      
 
277
                        colors.push_back(exp);
 
278
            numberOfExpressions.push_back(std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(colors),numberof));      
 
279
        }
 
280
    }else{
 
281
         auto initCartesianSet = cartesianProduct(collectedColors[0], collectedColors[1]);      
 
282
        for(uint32_t i = 2; i < collectedColors.size(); i++){   
 
283
            initCartesianSet = cartesianProduct(initCartesianSet, collectedColors[i]);  
 
284
        }       
 
285
        for(auto set : initCartesianSet){       
 
286
            std::vector<PetriEngine::Colored::ColorExpression_ptr> colors;      
 
287
            for (auto color : set) {    
 
288
                colors.push_back(color);        
 
289
            }   
 
290
            std::shared_ptr<PetriEngine::Colored::TupleExpression> tupleExpr = std::make_shared<PetriEngine::Colored::TupleExpression>(std::move(colors));      
 
291
            tupleExpr->setColorType(tupleExpr->getColorType(colorTypes));       
 
292
            std::vector<PetriEngine::Colored::ColorExpression_ptr> placeholderVector;   
 
293
            placeholderVector.push_back(tupleExpr);     
 
294
            numberOfExpressions.push_back(std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(placeholderVector),numberof));   
 
295
        }       
 
296
    }
 
297
        return std::make_shared<PetriEngine::Colored::AddExpression>(std::move(numberOfExpressions));   
296
298
}       
297
299
        
298
300
std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> PNMLParser::cartesianProduct(std::vector<PetriEngine::Colored::ColorExpression_ptr> rightSet, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftSet){      
511
513
    return nullptr;
512
514
}
513
515
 
514
 
PetriEngine::Colored::ColorType* PNMLParser::parseUserSort(rapidxml::xml_node<>* element) {
 
516
const PetriEngine::Colored::ColorType* PNMLParser::parseUserSort(rapidxml::xml_node<>* element) {
515
517
    if (element) {
516
518
        for (auto it = element->first_node(); it; it = it->next_sibling()) {
517
519
            if (strcmp(it->name(), "usersort") == 0) {
537
539
        number = 1;
538
540
        first = num;
539
541
    }
 
542
 
540
543
    auto allExpr = parseAllExpression(first);
541
544
    if (allExpr) {
542
545
        return std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(allExpr), number);
565
568
        } else if (strcmp(it->name(),"inhibitorArc") == 0) {
566
569
            parseArc(it, true);
567
570
        } else if (strcmp(it->name(), "variable") == 0) {
568
 
            std::cerr << "variable not supported" << std::endl;
 
571
            std::cerr << "ERROR: variable not supported" << std::endl;
569
572
            exit(ErrorCode);
570
573
        } else if (strcmp(it->name(),"queries") == 0) {
571
574
            parseQueries(it);
572
575
        } else if (strcmp(it->name(), "k-bound") == 0) {
573
 
            std::cerr << "k-bound should be given as command line option -k" << std::endl;
 
576
            std::cerr << "ERROR: k-bound should be given as command line option -k" << std::endl;
574
577
            exit(ErrorCode);
575
578
        } else if (strcmp(it->name(),"query") == 0) {
576
 
            std::cerr << "query tag not supported, please use PQL or XML-style queries instead" << std::endl;
 
579
            std::cerr << "ERROR: query tag not supported, please use PQL or XML-style queries instead" << std::endl;
577
580
            exit(ErrorCode);            
578
581
        }
579
582
        else
603
606
    auto initial = element->first_attribute("initialMarking");
604
607
    long long initialMarking = 0;
605
608
    PetriEngine::Colored::Multiset hlinitialMarking;
606
 
    PetriEngine::Colored::ColorType* type = nullptr;
 
609
    const PetriEngine::Colored::ColorType* type = nullptr;
607
610
    if(initial)
608
611
         initialMarking = atoll(initial->value());
609
612
 
619
622
            std::unordered_map<const PetriEngine::Colored::Variable*, const PetriEngine::Colored::Color*> binding;
620
623
            PetriEngine::Colored::EquivalenceVec placePartition;
621
624
                        PetriEngine::Colored::ExpressionContext context {binding, colorTypes, placePartition};
622
 
            for(auto ct : colorTypes){
623
 
            }
624
625
            hlinitialMarking = parseArcExpression(it->first_node("structure"))->eval(context);
625
626
        } else if (strcmp(it->name(), "type") == 0) {
626
627
            type = parseUserSort(it);
668
669
    }
669
670
 
670
671
    bool first = true;
671
 
    for (auto it = element->first_node("inscription"); it; it = it->next_sibling("inscription")) {
672
 
        std::string text;
673
 
        parseValue(it, text);
674
 
        weight = atoi(text.c_str());
675
 
        if(std::find_if(text.begin(), text.end(), [](char c) { return !std::isdigit(c) && !std::isblank(c); }) != text.end())
676
 
        {
677
 
            std::cerr << "ERROR: Found non-integer-text in inscription-tag (weight) on arc from " << source << " to " << target << " with value \"" << text << "\". An integer was expected." << std::endl;
678
 
            exit(ErrorCode);
679
 
        }
 
672
    auto weightTag = element->first_attribute("weight");
 
673
    if(weightTag != nullptr){
 
674
        weight = atoi(weightTag->value());
680
675
        assert(weight > 0);
681
 
        if(!first)
682
 
        {
683
 
            std::cerr << "ERROR: Multiple inscription tags in xml of a arc from " << source << " to " << target << "." << std::endl;
684
 
            exit(ErrorCode);
 
676
    } else {
 
677
        for (auto it = element->first_node("inscription"); it; it = it->next_sibling("inscription")) {
 
678
            std::string text;
 
679
            parseValue(it, text);
 
680
            weight = atoi(text.c_str());
 
681
            if(std::find_if(text.begin(), text.end(), [](char c) { return !std::isdigit(c) && !std::isblank(c); }) != text.end())
 
682
            {
 
683
                std::cerr << "ERROR: Found non-integer-text in inscription-tag (weight) on arc from " << source << " to " << target << " with value \"" << text << "\". An integer was expected." << std::endl;
 
684
                exit(ErrorCode);
 
685
            }
 
686
            assert(weight > 0);
 
687
            if(!first)
 
688
            {
 
689
                std::cerr << "ERROR: Multiple inscription tags in xml of a arc from " << source << " to " << target << "." << std::endl;
 
690
                exit(ErrorCode);
 
691
            }
 
692
            first = false;
685
693
        }
686
 
        first = false;
687
694
    }
688
695
    
689
696
    PetriEngine::Colored::ArcExpression_ptr expr;
698
705
        first = false;
699
706
    }
700
707
    
701
 
    if (isColored)
 
708
    if (isColored && !inhibitor)
702
709
        assert(expr != nullptr);
703
710
    Arc arc;
704
711
    arc.source = source;
705
712
    arc.target = target;
706
713
    arc.weight = weight;
707
 
    arc.expr = expr;
 
714
    arc.inhib = inhibitor;
 
715
    if(!inhibitor)
 
716
        arc.expr = expr;
708
717
    assert(weight > 0);
709
718
    
710
 
    if (inhibitor && isColored) {
711
 
        std::cerr << "inhibitor arcs are not supported in colored Petri nets" << std::endl;
712
 
        exit(ErrorCode);
713
 
    }
714
 
    
715
719
    if(weight != 0)
716
720
    {
717
 
        if(inhibitor)
718
 
        {
719
 
            inhibarcs.push_back(arc);   
720
 
        }
721
 
        else
722
 
        {
723
 
            arcs.push_back(arc);
724
 
        }
 
721
        arcs.push_back(arc);
725
722
    }
726
723
    else
727
724
    {