← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriParse/PNMLParser.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:
PetriParse/PNMLParser.cpp
1
 
/* PeTe - Petri Engine exTremE
2
 
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
3
 
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
4
 
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
5
 
 *                     Peter Gjøl Jensen <root@petergjoel.dk>
6
 
 * 
7
 
 * This program is free software: you can redistribute it and/or modify
8
 
 * it under the terms of the GNU General Public License as published by
9
 
 * the Free Software Foundation, either version 3 of the License, or
10
 
 * (at your option) any later version.
11
 
 * 
12
 
 * This program is distributed in the hope that it will be useful,
13
 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14
 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15
 
 * GNU General Public License for more details.
16
 
 * 
17
 
 * You should have received a copy of the GNU General Public License
18
 
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
19
 
 */
20
 
 
21
 
#include <string>
22
 
#include <stdio.h>
23
 
#include <stdlib.h>
24
 
#include <iostream>
25
 
#include <limits>
26
 
#include <fstream>
27
 
#include <string.h>
28
 
 
29
 
 
30
 
#include "PNMLParser.h"
31
 
#include "../PetriEngine/errorcodes.h"
32
 
#include "PetriEngine/PQL/Expressions.h"
33
 
 
34
 
using namespace PetriEngine;
35
 
using namespace std;
36
 
using namespace PetriEngine::PQL;
37
 
 
38
 
void PNMLParser::parse(ifstream& xml,
39
 
        AbstractPetriNetBuilder* builder) {
40
 
    //Clear any left overs
41
 
    id2name.clear();
42
 
    arcs.clear();
43
 
    transitions.clear();
44
 
    inhibarcs.clear();
45
 
    colorTypes.clear();
46
 
 
47
 
    //Set the builder
48
 
    this->builder = builder;
49
 
 
50
 
    //Parser the xml
51
 
    rapidxml::xml_document<> doc;
52
 
    vector<char> buffer((istreambuf_iterator<char>(xml)), istreambuf_iterator<char>());
53
 
    buffer.push_back('\0');
54
 
    doc.parse<0>(&buffer[0]);
55
 
    
56
 
    rapidxml::xml_node<>* root = doc.first_node();
57
 
    if(strcmp(root->name(), "pnml") != 0)
58
 
    {
59
 
        std::cerr << "expecting <pnml> tag as root-node in xml tree." << std::endl;
60
 
        exit(ErrorCode);
61
 
    }
62
 
    
63
 
    auto declarations = root->first_node("net")->first_node("declaration");
64
 
    isColored = declarations != nullptr;
65
 
    if (isColored) {
66
 
        builder->enableColors();
67
 
        parseDeclarations(declarations);
68
 
    }
69
 
    parseElement(root);
70
 
 
71
 
    //Add all the transition
72
 
    for (TransitionIter it = transitions.begin(); it != transitions.end(); ++it)
73
 
        if (!isColored) {
74
 
            builder->addTransition(it->id, it->x, it->y);
75
 
        } else {
76
 
            builder->addTransition(it->id, it->expr, it->x, it->y);
77
 
        }
78
 
 
79
 
    //Add all the arcs
80
 
    for (ArcIter it = arcs.begin(); it != arcs.end(); it++) {
81
 
        auto a = *it;
82
 
        
83
 
        //Check that source id exists
84
 
        if (id2name.find(it->source) == id2name.end()) {
85
 
            fprintf(stderr,
86
 
                    "XML Parsing error: Arc source with id=\"%s\" wasn't found!\n",
87
 
                    it->source.c_str());
88
 
            continue;
89
 
        }
90
 
        //Check that target id exists
91
 
        if (id2name.find(it->target) == id2name.end()) {
92
 
            fprintf(stderr,
93
 
                    "XML Parsing error: Arc target with id=\"%s\" wasn't found!\n",
94
 
                    it->target.c_str());
95
 
            continue;
96
 
        }
97
 
        //Find source and target
98
 
        NodeName source = id2name[it->source];
99
 
        NodeName target = id2name[it->target];
100
 
 
101
 
        if (source.isPlace && !target.isPlace) {
102
 
            if (!isColored) {
103
 
                builder->addInputArc(source.id, target.id, false, it->weight);
104
 
            } else {
105
 
                builder->addInputArc(source.id, target.id, it->expr);
106
 
            }
107
 
 
108
 
        } else if (!source.isPlace && target.isPlace) {
109
 
            if (!isColored) {
110
 
                builder->addOutputArc(source.id, target.id, it->weight);
111
 
            } else {
112
 
                builder->addOutputArc(source.id, target.id, it->expr);
113
 
            }
114
 
        } else {
115
 
            fprintf(stderr,
116
 
                    "XML Parsing error: Arc from \"%s\" to \"%s\" is neither input nor output!\n",
117
 
                    source.id.c_str(),
118
 
                    target.id.c_str());
119
 
        }
120
 
    }
121
 
 
122
 
    for(Arc& inhibitor : inhibarcs)
123
 
    {
124
 
        NodeName source = id2name[inhibitor.source];
125
 
        NodeName target = id2name[inhibitor.target];
126
 
        if (source.isPlace && !target.isPlace) {
127
 
            builder->addInputArc(source.id, target.id, true, inhibitor.weight);
128
 
        }
129
 
        else
130
 
        {
131
 
            fprintf(stderr,
132
 
                    "XML Parsing error: Inhibitor from \"%s\" to \"%s\" is not valid!\n",
133
 
                    source.id.c_str(),
134
 
                    target.id.c_str());
135
 
        }
136
 
    }
137
 
    
138
 
    //Unset the builder
139
 
    this->builder = NULL;
140
 
 
141
 
    //Cleanup
142
 
    id2name.clear();
143
 
    arcs.clear();
144
 
    transitions.clear();
145
 
    inhibarcs.clear();
146
 
    colorTypes.clear();
147
 
    builder->sort();
148
 
}
149
 
 
150
 
void PNMLParser::parseDeclarations(rapidxml::xml_node<>* element) {
151
 
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
152
 
        if (strcmp(it->name(), "namedsort") == 0) {
153
 
            parseNamedSort(it);
154
 
        } else if (strcmp(it->name(), "variabledecl") == 0) {
155
 
            auto var = new PetriEngine::Colored::Variable {
156
 
                it->first_attribute("id")->value(),
157
 
                parseUserSort(it)
158
 
            };
159
 
            variables[it->first_attribute("id")->value()] = var;
160
 
        } else {
161
 
            parseDeclarations(element->first_node());
162
 
        }
163
 
    }
164
 
}
165
 
 
166
 
bool isInitialBinding(std::vector<const PetriEngine::Colored::Color*>& binding) {
167
 
    for (auto color : binding) {
168
 
        if (color->getId() != 0)
169
 
            return false;
170
 
    }
171
 
    return true;
172
 
}
173
 
 
174
 
void PNMLParser::parseNamedSort(rapidxml::xml_node<>* element) {
175
 
    auto type = element->first_node();
176
 
    auto ct = strcmp(type->name(), "productsort") == 0 ?
177
 
              new PetriEngine::Colored::ProductType(std::string(element->first_attribute("id")->value())) :
178
 
              new PetriEngine::Colored::ColorType(std::string(element->first_attribute("id")->value()));
179
 
    
180
 
    if (strcmp(type->name(), "dot") == 0) {
181
 
        ct->addDot();
182
 
    } else if (strcmp(type->name(), "productsort") == 0) {
183
 
        for (auto it = type->first_node(); it; it = it->next_sibling()) {
184
 
            if (strcmp(it->name(), "usersort") == 0) {
185
 
                ((PetriEngine::Colored::ProductType*)ct)->addType(colorTypes[it->first_attribute("declaration")->value()]);
186
 
            }
187
 
        }
188
 
    } else {
189
 
        for (auto it = type->first_node(); it; it = it->next_sibling()) {
190
 
            auto id = it->first_attribute("id");
191
 
            assert(id != 0);
192
 
            ct->addColor(id->value());
193
 
        }
194
 
    }
195
 
 
196
 
    std::string id = element->first_attribute("id")->value();
197
 
    colorTypes[id] = ct;
198
 
    builder->addColorType(id, ct);
199
 
}
200
 
 
201
 
PetriEngine::Colored::ArcExpression_ptr PNMLParser::parseArcExpression(rapidxml::xml_node<>* element) {
202
 
    if (strcmp(element->name(), "numberof") == 0) {
203
 
        return parseNumberOfExpression(element);
204
 
    } else if (strcmp(element->name(), "add") == 0) {
205
 
        std::vector<PetriEngine::Colored::ArcExpression_ptr> constituents;
206
 
        for (auto it = element->first_node(); it; it = it->next_sibling()) {
207
 
            constituents.push_back(parseArcExpression(it));
208
 
        }
209
 
        return std::make_shared<PetriEngine::Colored::AddExpression>(std::move(constituents));
210
 
    } else if (strcmp(element->name(), "subtract") == 0) {
211
 
        auto left = element->first_node();
212
 
        auto right = left->next_sibling();
213
 
        auto res = std::make_shared<PetriEngine::Colored::SubtractExpression>(parseArcExpression(left), parseArcExpression(right));
214
 
        auto next = right;
215
 
        while ((next = next->next_sibling())) {
216
 
            res = std::make_shared<PetriEngine::Colored::SubtractExpression>(res, parseArcExpression(next));
217
 
        }
218
 
        return res;
219
 
    } else if (strcmp(element->name(), "scalarproduct") == 0) {
220
 
        auto scalar = element->first_node();
221
 
        auto ms = scalar->next_sibling();
222
 
        return std::make_shared<PetriEngine::Colored::ScalarProductExpression>(parseArcExpression(ms), parseNumberConstant(scalar));
223
 
    } else if (strcmp(element->name(), "all") == 0) {
224
 
        return parseNumberOfExpression(element->parent());
225
 
    } else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {
226
 
        return parseArcExpression(element->first_node());
227
 
    }
228
 
    printf("Could not parse '%s' as an arc expression\n", element->name());
229
 
    assert(false);
230
 
    return nullptr;
231
 
}
232
 
 
233
 
PetriEngine::Colored::GuardExpression_ptr PNMLParser::parseGuardExpression(rapidxml::xml_node<>* element) {
234
 
    if (strcmp(element->name(), "lt") == 0 || strcmp(element->name(), "lessthan") == 0) {
235
 
        auto left = element->first_node();
236
 
        auto right = left->next_sibling();
237
 
        return std::make_shared<PetriEngine::Colored::LessThanExpression>(parseColorExpression(left), parseColorExpression(right));
238
 
    } else if (strcmp(element->name(), "gt") == 0 || strcmp(element->name(), "greaterthan") == 0) {
239
 
        auto left = element->first_node();
240
 
        auto right = left->next_sibling();
241
 
        return std::make_shared<PetriEngine::Colored::GreaterThanExpression>(parseColorExpression(left), parseColorExpression(right));
242
 
    } else if (strcmp(element->name(), "leq") == 0 || strcmp(element->name(), "lessthanorequal") == 0) {
243
 
        auto left = element->first_node();
244
 
        auto right = left->next_sibling();
245
 
        return std::make_shared<PetriEngine::Colored::LessThanEqExpression>(parseColorExpression(left), parseColorExpression(right));
246
 
    } else if (strcmp(element->name(), "geq") == 0 || strcmp(element->name(), "greaterthanorequal") == 0) {
247
 
        auto left = element->first_node();
248
 
        auto right = left->next_sibling();
249
 
        return std::make_shared<PetriEngine::Colored::GreaterThanEqExpression>(parseColorExpression(left), parseColorExpression(right));
250
 
    } else if (strcmp(element->name(), "eq") == 0 || strcmp(element->name(), "equality") == 0) {
251
 
        auto left = element->first_node();
252
 
        auto right = left->next_sibling();
253
 
        return std::make_shared<PetriEngine::Colored::EqualityExpression>(parseColorExpression(left), parseColorExpression(right));
254
 
    } else if (strcmp(element->name(), "neq") == 0 || strcmp(element->name(), "inequality") == 0) {
255
 
        auto left = element->first_node();
256
 
        auto right = left->next_sibling();
257
 
        return std::make_shared<PetriEngine::Colored::InequalityExpression>(parseColorExpression(left), parseColorExpression(right));
258
 
    } else if (strcmp(element->name(), "not") == 0) {
259
 
        return std::make_shared<PetriEngine::Colored::NotExpression>(parseGuardExpression(element->first_node()));
260
 
    } else if (strcmp(element->name(), "and") == 0) {
261
 
        auto left = element->first_node();
262
 
        auto right = left->next_sibling();
263
 
        return std::make_shared<PetriEngine::Colored::AndExpression>(parseGuardExpression(left), parseGuardExpression(right));
264
 
    } else if (strcmp(element->name(), "or") == 0) {
265
 
        auto left = element->first_node();
266
 
        auto right = left->next_sibling();
267
 
        return std::make_shared<PetriEngine::Colored::OrExpression>(parseGuardExpression(left), parseGuardExpression(right));
268
 
    } else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {
269
 
        return parseGuardExpression(element->first_node());
270
 
    }
271
 
    
272
 
    printf("Could not parse '%s' as a guard expression\n", element->name());
273
 
    assert(false);
274
 
    return nullptr;
275
 
}
276
 
 
277
 
PetriEngine::Colored::ColorExpression_ptr PNMLParser::parseColorExpression(rapidxml::xml_node<>* element) {
278
 
    if (strcmp(element->name(), "dotconstant") == 0) {
279
 
        return std::make_shared<PetriEngine::Colored::DotConstantExpression>();
280
 
    } else if (strcmp(element->name(), "variable") == 0) {
281
 
        return std::make_shared<PetriEngine::Colored::VariableExpression>(variables[element->first_attribute("refvariable")->value()]);
282
 
    } else if (strcmp(element->name(), "useroperator") == 0) {
283
 
        return std::make_shared<PetriEngine::Colored::UserOperatorExpression>(findColor(element->first_attribute("declaration")->value()));
284
 
    } else if (strcmp(element->name(), "successor") == 0) {
285
 
        return std::make_shared<PetriEngine::Colored::SuccessorExpression>(parseColorExpression(element->first_node()));
286
 
    } else if (strcmp(element->name(), "predecessor") == 0) {
287
 
        return std::make_shared<PetriEngine::Colored::PredecessorExpression>(parseColorExpression(element->first_node()));
288
 
    } else if (strcmp(element->name(), "tuple") == 0) {
289
 
        std::vector<PetriEngine::Colored::ColorExpression_ptr> colors;
290
 
        for (auto it = element->first_node(); it; it = it->next_sibling()) {
291
 
            colors.push_back(parseColorExpression(it));
292
 
        }
293
 
        return std::make_shared<PetriEngine::Colored::TupleExpression>(std::move(colors));
294
 
    } else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {
295
 
        return parseColorExpression(element->first_node());
296
 
    }
297
 
    assert(false);
298
 
    return nullptr;
299
 
}
300
 
 
301
 
PetriEngine::Colored::AllExpression_ptr PNMLParser::parseAllExpression(rapidxml::xml_node<>* element) {
302
 
    if (strcmp(element->name(), "all") == 0) {
303
 
        return std::make_shared<PetriEngine::Colored::AllExpression>(parseUserSort(element));
304
 
    } else if (strcmp(element->name(), "subterm") == 0) {
305
 
        return parseAllExpression(element->first_node());
306
 
    }
307
 
    
308
 
    return nullptr;
309
 
}
310
 
 
311
 
PetriEngine::Colored::ColorType* PNMLParser::parseUserSort(rapidxml::xml_node<>* element) {
312
 
    if (element) {
313
 
        for (auto it = element->first_node(); it; it = it->next_sibling()) {
314
 
            if (strcmp(it->name(), "usersort") == 0) {
315
 
                return colorTypes[it->first_attribute("declaration")->value()];
316
 
            } else if (strcmp(it->name(), "structure") == 0
317
 
                    || strcmp(it->name(), "type") == 0
318
 
                    || strcmp(it->name(), "subterm") == 0) {
319
 
                return parseUserSort(it);
320
 
            }
321
 
        }
322
 
    }
323
 
    assert(false);
324
 
    return nullptr;
325
 
}
326
 
 
327
 
PetriEngine::Colored::NumberOfExpression_ptr PNMLParser::parseNumberOfExpression(rapidxml::xml_node<>* element) {
328
 
    auto num = element->first_node();
329
 
    uint32_t number = parseNumberConstant(num);
330
 
    rapidxml::xml_node<>* first;
331
 
    if (number) {
332
 
        first = num->next_sibling();
333
 
    } else {
334
 
        number = 1;
335
 
        first = num;
336
 
    }
337
 
    auto allExpr = parseAllExpression(first);
338
 
    if (allExpr) {
339
 
        return std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(allExpr), number);
340
 
    } else {
341
 
        std::vector<PetriEngine::Colored::ColorExpression_ptr> colors;
342
 
        for (auto it = first; it; it = it->next_sibling()) {
343
 
            colors.push_back(parseColorExpression(it));
344
 
        }
345
 
        return std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(colors), number);
346
 
    }
347
 
}
348
 
 
349
 
void PNMLParser::parseElement(rapidxml::xml_node<>* element) {
350
 
    
351
 
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
352
 
        if (strcmp(it->name(), "place") == 0) {
353
 
            parsePlace(it);
354
 
        } else if (strcmp(it->name(),"transition") == 0) {
355
 
            parseTransition(it);
356
 
        } else if ( strcmp(it->name(),"arc") == 0 ||
357
 
                    strcmp(it->name(), "inputArc") == 0 ||
358
 
                    strcmp(it->name(), "outputArc") == 0) {
359
 
            parseArc(it);
360
 
        } else if (strcmp(it->name(),"transportArc") == 0) {
361
 
            parseTransportArc(it);
362
 
        } else if (strcmp(it->name(),"inhibitorArc") == 0) {
363
 
            parseArc(it, true);
364
 
        } else if (strcmp(it->name(), "variable") == 0) {
365
 
            std::cerr << "variable not supported" << std::endl;
366
 
            exit(ErrorCode);
367
 
        } else if (strcmp(it->name(),"queries") == 0) {
368
 
            parseQueries(it);
369
 
        } else if (strcmp(it->name(), "k-bound") == 0) {
370
 
            std::cerr << "k-bound should be given as command line option -k" << std::endl;
371
 
            exit(ErrorCode);
372
 
        } else if (strcmp(it->name(),"query") == 0) {
373
 
            std::cerr << "query tag not supported, please use PQL or XML-style queries instead" << std::endl;
374
 
            exit(ErrorCode);            
375
 
        }
376
 
        else
377
 
        {
378
 
            parseElement(it);
379
 
        }
380
 
    }
381
 
}
382
 
 
383
 
void PNMLParser::parseQueries(rapidxml::xml_node<>* element) {
384
 
    string query;
385
 
 
386
 
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
387
 
        string name(element->first_attribute("name")->value());
388
 
        parseValue(element, query);
389
 
        Query q;
390
 
        q.name = name;
391
 
        q.text = query;
392
 
        this->queries.push_back(q);
393
 
    }
394
 
}
395
 
 
396
 
void PNMLParser::parsePlace(rapidxml::xml_node<>* element) {
397
 
    double x = 0, y = 0;
398
 
    string id(element->first_attribute("id")->value());
399
 
    
400
 
    auto initial = element->first_attribute("initialMarking");
401
 
    long long initialMarking = 0;
402
 
    PetriEngine::Colored::Multiset hlinitialMarking;
403
 
    PetriEngine::Colored::ColorType* type = nullptr;
404
 
    if(initial)
405
 
         initialMarking = atoll(initial->value());
406
 
 
407
 
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
408
 
        // name element is ignored
409
 
        if (strcmp(it->name(), "graphics") == 0) {
410
 
            parsePosition(it, x, y);
411
 
        } else if (strcmp(it->name(),"initialMarking") == 0) {
412
 
            string text;
413
 
            parseValue(it, text);
414
 
            initialMarking = atoll(text.c_str());
415
 
        } else if (strcmp(it->name(),"hlinitialMarking") == 0) {
416
 
            std::unordered_map<std::string, const PetriEngine::Colored::Color*> binding;
417
 
            PetriEngine::Colored::ExpressionContext context {binding, colorTypes};
418
 
            hlinitialMarking = parseArcExpression(it->first_node("structure"))->eval(context);
419
 
        } else if (strcmp(it->name(), "type") == 0) {
420
 
            type = parseUserSort(it);
421
 
        }
422
 
    }
423
 
    
424
 
    if(initialMarking > std::numeric_limits<int>::max())
425
 
    {
426
 
        std::cerr << "Number of tokens in " << id << " exceeded " << std::numeric_limits<int>::max() << std::endl;
427
 
        exit(ErrorCode);
428
 
    }
429
 
    //Create place
430
 
    if (!isColored) {
431
 
        builder->addPlace(id, initialMarking, x, y);
432
 
    } else {
433
 
        if (!type) {
434
 
            std::cerr << "Place '" << id << "' is missing color type" << std::endl;
435
 
            exit(ErrorCode);
436
 
        }
437
 
        else
438
 
        {
439
 
            builder->addPlace(id, type, std::move(hlinitialMarking), x, y);
440
 
        }
441
 
    }
442
 
    //Map id to name
443
 
    NodeName nn;
444
 
    nn.id = id;
445
 
    nn.isPlace = true;
446
 
    id2name[id] = nn;
447
 
}
448
 
 
449
 
void PNMLParser::parseArc(rapidxml::xml_node<>* element, bool inhibitor) {
450
 
    string source = element->first_attribute("source")->value(),
451
 
            target = element->first_attribute("target")->value();
452
 
    int weight = 1;
453
 
    auto type = element->first_attribute("type");
454
 
    if(type && strcmp(type->value(), "timed") == 0)
455
 
    {
456
 
        std::cerr << "timed arcs are not supported" << std::endl;
457
 
        exit(ErrorCode);
458
 
    }
459
 
    else if(type && strcmp(type->value(), "inhibitor") == 0)
460
 
    {
461
 
        inhibitor = true;
462
 
    }
463
 
 
464
 
    bool first = true;
465
 
    for (auto it = element->first_node("inscription"); it; it = it->next_sibling("inscription")) {
466
 
        string text;
467
 
        parseValue(it, text);
468
 
        weight = atoi(text.c_str());
469
 
        if(std::find_if(text.begin(), text.end(), [](char c) { return !std::isdigit(c) && !std::isblank(c); }) != text.end())
470
 
        {
471
 
            if(weight == 0) weight = 1;
472
 
            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;
473
 
            exit(ErrorCode);
474
 
        }
475
 
        assert(weight > 0);
476
 
        if(!first)
477
 
        {
478
 
            std::cerr << "ERROR: Multiple inscription tags in xml of a arc from " << source << " to " << target << "." << std::endl;
479
 
            exit(ErrorCode);
480
 
        }
481
 
        first = false;
482
 
    }
483
 
    
484
 
    PetriEngine::Colored::ArcExpression_ptr expr;
485
 
    first = true;
486
 
    for (auto it = element->first_node("hlinscription"); it; it = it->next_sibling("hlinscription")) {
487
 
        expr = parseArcExpression(it->first_node("structure"));
488
 
        if(!first)
489
 
        {
490
 
            std::cerr << "ERROR: Multiple hlinscription tags in xml of a arc from " << source << " to " << target << "." << std::endl;
491
 
            exit(ErrorCode);            
492
 
        }
493
 
        first = false;
494
 
    }
495
 
    
496
 
    if (isColored)
497
 
        assert(expr != nullptr);
498
 
    Arc arc;
499
 
    arc.source = source;
500
 
    arc.target = target;
501
 
    arc.weight = weight;
502
 
    arc.expr = expr;
503
 
    assert(weight > 0);
504
 
    
505
 
    if (inhibitor && isColored) {
506
 
        std::cerr << "inhibitor arcs are not supported in colored Petri nets" << std::endl;
507
 
        exit(ErrorCode);
508
 
    }
509
 
    
510
 
    if(weight != 0)
511
 
    {
512
 
        if(inhibitor)
513
 
        {
514
 
            inhibarcs.push_back(arc);   
515
 
        }
516
 
        else
517
 
        {
518
 
            arcs.push_back(arc);
519
 
        }
520
 
    }
521
 
    else
522
 
    {
523
 
        std::cerr << "ERROR: Arc from " << source << " to " << target << " has non-sensible weight 0." << std::endl;         
524
 
        exit(ErrorCode);
525
 
    }
526
 
}
527
 
 
528
 
void PNMLParser::parseTransportArc(rapidxml::xml_node<>* element){
529
 
    string source       = element->first_attribute("source")->value(),
530
 
           transiton    = element->first_attribute("transition")->value(),
531
 
           target       = element->first_attribute("target")->value();
532
 
    int weight = 1;
533
 
 
534
 
    for(auto it = element->first_node("inscription"); it; it = it->next_sibling("inscription")){
535
 
        string text;
536
 
        parseValue(it, text);
537
 
        weight = atoi(text.c_str());
538
 
    }
539
 
 
540
 
    Arc inArc;
541
 
    inArc.source = source;
542
 
    inArc.target = transiton;
543
 
    inArc.weight = weight;
544
 
    arcs.push_back(inArc);
545
 
 
546
 
    Arc outArc;
547
 
    outArc.source = transiton;
548
 
    outArc.target = target;
549
 
    outArc.weight = weight;
550
 
    arcs.push_back(outArc);
551
 
}
552
 
 
553
 
void PNMLParser::parseTransition(rapidxml::xml_node<>* element) {
554
 
    Transition t;
555
 
    t.x = 0;
556
 
    t.y = 0;
557
 
    t.id = element->first_attribute("id")->value();
558
 
    t.expr = nullptr;
559
 
 
560
 
 
561
 
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
562
 
        // name element is ignored
563
 
        if (strcmp(it->name(), "graphics") == 0) {
564
 
            parsePosition(it, t.x, t.y);
565
 
        } else if (strcmp(it->name(), "condition") == 0) {
566
 
            t.expr = parseGuardExpression(it->first_node("structure"));
567
 
        } else if (strcmp(it->name(), "conditions") == 0) {
568
 
            std::cerr << "conditions not supported" << std::endl;
569
 
            exit(ErrorCode);
570
 
        } else if (strcmp(it->name(), "assignments") == 0) {
571
 
            std::cerr << "assignments not supported" << std::endl;
572
 
            exit(ErrorCode);
573
 
        }
574
 
    }
575
 
    //Add transition to list
576
 
    transitions.push_back(t);
577
 
    //Map id to name
578
 
    NodeName nn;
579
 
    nn.id = t.id;
580
 
    nn.isPlace = false;
581
 
    id2name[t.id] = nn;
582
 
}
583
 
 
584
 
void PNMLParser::parseValue(rapidxml::xml_node<>* element, string& text) {
585
 
    for (auto it = element->first_node(); it; it = it->next_sibling()) {
586
 
        if (strcmp(it->name(), "value") == 0 || strcmp(it->name(), "text") == 0) {
587
 
            text = it->value();
588
 
        } else
589
 
            parseValue(it, text);
590
 
    }
591
 
}
592
 
 
593
 
uint32_t PNMLParser::parseNumberConstant(rapidxml::xml_node<>* element) {
594
 
    if (strcmp(element->name(), "numberconstant") == 0) {
595
 
        auto value = element->first_attribute("value")->value();
596
 
        return (uint32_t)atoll(value);
597
 
    } else if (strcmp(element->name(), "subterm") == 0) {
598
 
        return parseNumberConstant(element->first_node());
599
 
    }
600
 
    return 0;
601
 
}
602
 
 
603
 
void PNMLParser::parsePosition(rapidxml::xml_node<>* element, double& x, double& y) {
604
 
    for (auto it = element->first_node(); it; it = it->first_node()) {
605
 
        if (strcmp(it->name(), "position") == 0) {
606
 
            x = atof(it->first_attribute("x")->value());
607
 
            y = atof(it->first_attribute("y")->value());
608
 
        } else
609
 
        {
610
 
            parsePosition(it, x, y);
611
 
        }
612
 
    }
613
 
}
614
 
 
615
 
const PetriEngine::Colored::Color* PNMLParser::findColor(const char* name) const {
616
 
    for (auto elem : colorTypes) {
617
 
        auto col = (*elem.second)[name];
618
 
        if (col)
619
 
            return col;
620
 
    }
621
 
    printf("Could not find color: %s\nCANNOT_COMPUTE\n", name);
622
 
    exit(ErrorCode);
623
 
}