← Back to branch summary

~verifypn-maintainers/verifypn/emptyTracePrint

« back to all changes in this revision

Viewing changes to PetriParse/QueryXMLParser.cpp

  • Committer: Jiri Srba
  • Date: 2018-04-18 10:58:36 UTC
  • mfrom: (197.3.78 cpn_ctlss)
  • Revision ID: srba.jiri@gmail.com-20180418105836-a5rha272u0om4u77
merged in branch lp:~verifypn-cpn/verifypn/cpn_ctlss/

CPN unfolding
CPN linear overapproximation
Export of reduced queries and model
parallel query simplification
TAR for P/T nets
Improved structural reduction rules

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriParse/QueryXMLParser.cpp
136
136
}
137
137
 
138
138
Condition_ptr QueryXMLParser::parseFormula(rapidxml::xml_node<>*  element) {
139
 
    if (getChildCount(element) != 1) return nullptr;    
 
139
    if (getChildCount(element) != 1) 
 
140
    {
 
141
        assert(false);
 
142
        return nullptr;    
 
143
    }
140
144
    auto child = element->first_node();
141
145
    string childName = child->name();
142
146
    Condition_ptr cond = nullptr;
145
149
    if (childName == "place-bound") {
146
150
        std::vector<std::string> places;
147
151
        for (auto it = child->first_node(); it ; it = it->next_sibling()) {
148
 
            if (strcmp(it->name(), "place") != 0) return nullptr;
 
152
            if (strcmp(it->name(), "place") != 0) 
 
153
            {
 
154
                assert(false);
 
155
                return nullptr;
 
156
            }
149
157
            auto place = parsePlace(it);
150
 
            if (place == "") return nullptr; // invalid place name
151
 
            auto tmp = std::make_shared<LessThanCondition>(
152
 
                            std::make_shared<IdentifierExpr>(place),
153
 
                            std::make_shared<LiteralExpr>(0));
154
 
            if (cond == nullptr) {
155
 
                cond = tmp;
156
 
            } else {
157
 
                cond = std::make_shared<AndCondition>(cond, tmp);
 
158
            if (place == "") 
 
159
            {             
 
160
                assert(false);
 
161
                return nullptr; // invalid place name
158
162
            }
159
163
            places.push_back(place);
160
164
        }
161
 
        cond->setPlaceNameForBounds(places);
162
 
        return std::make_shared<EFCondition>(cond);
 
165
        auto bnds = std::make_shared<UpperBoundsCondition>(places);
 
166
        return std::make_shared<EFCondition>(bnds);
163
167
    } else if ((cond = parseBooleanFormula(child)) != nullptr) {
164
168
        return cond;
165
169
    } else {
 
170
        assert(false);
166
171
        return nullptr;
167
172
    }
168
173
}
192
197
        if ((cond = parseBooleanFormula(element->first_node())) != nullptr)
193
198
            return std::make_shared<EFCondition>(cond);
194
199
    } else if (elementName == "exists-path") {
195
 
        if (getChildCount(element) != 1) return nullptr;
 
200
        if (getChildCount(element) != 1) 
 
201
        {
 
202
            assert(false);
 
203
            return nullptr;
 
204
        }
196
205
        auto child = element->first_node();
197
206
        if (strcmp(child->name(), "next") == 0) {
198
 
            if (getChildCount(child) != 1) return nullptr;
 
207
            if (getChildCount(child) != 1) 
 
208
            {
 
209
                assert(false);
 
210
                return nullptr;
 
211
            }
199
212
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
200
213
                return std::make_shared<EXCondition>(cond);
201
214
        } else if (strcmp(child->name(), "globally") == 0) {
202
 
            if (getChildCount(child) != 1) return nullptr;
 
215
            if (getChildCount(child) != 1) 
 
216
            {
 
217
                assert(false);
 
218
                return nullptr;
 
219
            }
203
220
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
204
221
                return std::make_shared<EGCondition>(cond);
205
222
        } else if (strcmp(child->name(), "finally") == 0) {
206
 
            if (getChildCount(child) != 1) return nullptr;
 
223
            if (getChildCount(child) != 1) 
 
224
            {
 
225
                assert(false);
 
226
                return nullptr;
 
227
            }
207
228
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
208
229
                return std::make_shared<EFCondition>(cond);
209
230
        } else if (strcmp(child->name(), "until") == 0) {
210
 
            if (getChildCount(child) != 2) return nullptr;           
 
231
            if (getChildCount(child) != 2) 
 
232
            {
 
233
                assert(false);
 
234
                return nullptr;
 
235
            }
211
236
            auto before = child->first_node();
212
237
            auto reach = before->next_sibling();
213
238
            if (getChildCount(before) != 1 || getChildCount(reach) != 1 ||
214
 
                    strcmp(before->name(), "before") != 0 || strcmp(reach->name(), "reach") != 0) return nullptr;
 
239
                    strcmp(before->name(), "before") != 0 || strcmp(reach->name(), "reach") != 0) 
 
240
                {
 
241
                    assert(false);
 
242
                    return nullptr;
 
243
                }
215
244
            if ((cond = parseBooleanFormula(before->first_node())) != nullptr) {
216
245
                if ((cond2 = parseBooleanFormula(reach->first_node())) != nullptr) {
217
246
                    return std::make_shared<EUCondition>(cond, cond2);
219
248
            }
220
249
        }
221
250
    } else if (elementName == "all-paths") {
222
 
        if (getChildCount(element) != 1) return nullptr;
 
251
        if (getChildCount(element) != 1) 
 
252
        {
 
253
            assert(false);
 
254
            return nullptr;
 
255
        }
223
256
        auto child = element->first_node();
224
257
        if (strcmp(child->name(), "next") == 0) {
225
 
            if (getChildCount(child) != 1) return nullptr;
 
258
            if (getChildCount(child) != 1) 
 
259
            {
 
260
                assert(false);
 
261
                return nullptr;
 
262
            }
226
263
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
227
264
                return std::make_shared<AXCondition>(cond);
228
265
        } else if (strcmp(child->name(), "globally") == 0) {
229
 
            if (getChildCount(child) != 1) return nullptr;
 
266
            if (getChildCount(child) != 1) 
 
267
            {
 
268
                assert(false);
 
269
                return nullptr;
 
270
            }
230
271
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
231
272
                return std::make_shared<AGCondition>(cond);
232
273
        } else if (strcmp(child->name(), "finally") == 0) {
233
 
            if (getChildCount(child) != 1) return nullptr;
 
274
            if (getChildCount(child) != 1) 
 
275
            {
 
276
                assert(false);
 
277
                return nullptr;
 
278
            }
234
279
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr)
235
280
                return std::make_shared<AFCondition>(cond);
236
281
        } else if (strcmp(child->name(), "until") == 0) {
237
 
            if (getChildCount(child) != 2) return nullptr;           
 
282
            if (getChildCount(child) != 2) 
 
283
            {
 
284
                assert(false);
 
285
                return nullptr;
 
286
            }
238
287
            auto before = child->first_node();
239
288
            auto reach = before->next_sibling();
240
289
            if (getChildCount(before) != 1 || getChildCount(reach) != 1 ||
241
 
                    strcmp(before->name(), "before") != 0 || strcmp(reach->name(), "reach") != 0) return nullptr;
 
290
                    strcmp(before->name(), "before") != 0 || strcmp(reach->name(), "reach") != 0)
 
291
            {
 
292
                assert(false);
 
293
                return nullptr;
 
294
            }
242
295
            if ((cond = parseBooleanFormula(before->first_node())) != nullptr){
243
296
                if ((cond2 = parseBooleanFormula(reach->first_node())) != nullptr) {
244
297
                    return std::make_shared<AUCondition>(cond, cond2);
252
305
    } else if (elementName == "false") {
253
306
        return BooleanCondition::FALSE_CONSTANT;
254
307
    } else if (elementName == "negation") {
255
 
        if (getChildCount(element) != 1) return nullptr;
 
308
        if (getChildCount(element) != 1) 
 
309
        {
 
310
            assert(false);
 
311
            return nullptr;
 
312
        }
256
313
        auto child = element->first_node();
257
314
        if (strcmp(child->name(), "invariant") == 0) {
258
315
            if ((cond = parseBooleanFormula(child->first_node())) != nullptr) {
273
330
        }
274
331
    } else if (elementName == "conjunction") {
275
332
        auto children = element->first_node();
276
 
        if (getChildCount(element) < 2) return nullptr;
 
333
        if (getChildCount(element) < 2) 
 
334
        {
 
335
            assert(false);
 
336
            return nullptr;
 
337
        }
277
338
        auto it = children;
278
339
        cond = parseBooleanFormula(it);
279
340
        // skip a sibling
280
341
        for (it = it->next_sibling(); it; it = it->next_sibling()) {
281
342
            Condition_ptr child = parseBooleanFormula(it);
282
 
            if(child == nullptr || cond == nullptr) return nullptr;
 
343
            if(child == nullptr || cond == nullptr) 
 
344
            {
 
345
                assert(false);
 
346
                return nullptr;
 
347
            }
283
348
            cond = std::make_shared<AndCondition>(cond, child);
284
349
        }
285
350
        return cond;
286
351
    } else if (elementName == "disjunction") {
287
352
        auto children = element->first_node();
288
 
        if (getChildCount(element) < 2) return nullptr;
 
353
        if (getChildCount(element) < 2) 
 
354
        {
 
355
            assert(false);
 
356
            return nullptr;
 
357
        }
289
358
        auto it = children;
290
359
        cond = parseBooleanFormula(it);
291
360
        // skip a sibling
292
361
        for (it = it->next_sibling(); it; it = it->next_sibling()) {
293
362
            Condition_ptr child = parseBooleanFormula(it);
294
 
            if(child == nullptr || cond == nullptr) return nullptr;
 
363
            if(child == nullptr || cond == nullptr) 
 
364
            {
 
365
                assert(false);
 
366
                return nullptr;
 
367
            }
295
368
            cond = std::make_shared<OrCondition>(cond, child);
296
369
        }
297
370
        return cond;
298
371
    } else if (elementName == "exclusive-disjunction") {
299
372
        auto children = element->first_node();
300
 
        if (getChildCount(element) != 2) return nullptr; // we support only two subformulae here
 
373
        if (getChildCount(element) != 2) 
 
374
        {
 
375
            assert(false);
 
376
            return nullptr;
 
377
        }
301
378
        cond = parseBooleanFormula(children);
302
379
        cond2 = parseBooleanFormula(children->next_sibling());
303
 
        if (cond == nullptr || cond2 == nullptr) return nullptr;       
 
380
        if (cond == nullptr || cond2 == nullptr)    
 
381
        {
 
382
            assert(false);
 
383
            return nullptr;
 
384
        }
304
385
        return std::make_shared<OrCondition>(
305
386
                std::make_shared<AndCondition>(cond, std::make_shared<NotCondition>(cond2)),
306
387
                std::make_shared<AndCondition>(std::make_shared<NotCondition>(cond), cond2));
307
388
    } else if (elementName == "implication") {
308
389
        auto children = element->first_node();
309
 
        if (getChildCount(element) != 2) return nullptr; // implication has only two subformulae
 
390
        if (getChildCount(element) != 2)             
 
391
        {
 
392
            assert(false);
 
393
            return nullptr;
 
394
        }
310
395
        cond = parseBooleanFormula(children);
311
396
        cond2 = parseBooleanFormula(children->next_sibling());
312
 
        if (cond == nullptr || cond2 == nullptr) return nullptr;       
 
397
        if (cond == nullptr || cond2 == nullptr)
 
398
        {
 
399
            assert(false);
 
400
            return nullptr;       
 
401
        }
313
402
        return std::make_shared<OrCondition>(std::make_shared<NotCondition>(cond), cond2);
314
403
    } else if (elementName == "equivalence") {
315
404
        auto children = element->first_node();
316
 
        if (getChildCount(element) != 2) return nullptr; // we support only two subformulae here
 
405
        if (getChildCount(element) != 2) 
 
406
        {
 
407
            assert(false);
 
408
            return nullptr;       
 
409
        }
317
410
        cond = parseBooleanFormula(children);
318
411
        cond2 = parseBooleanFormula(children->next_sibling());
319
412
        if (cond == nullptr || cond2 == nullptr) return nullptr;
324
417
            elementName == "integer-lt" || elementName == "integer-le" ||
325
418
            elementName == "integer-gt" || elementName == "integer-ge") {
326
419
        auto children = element->first_node();
327
 
        if (getChildCount(element) != 2) return nullptr; // exactly two integer subformulae are required       
 
420
        if (getChildCount(element) != 2) 
 
421
        {
 
422
            assert(false);
 
423
            return nullptr;       
 
424
        }
328
425
        Expr_ptr expr1 = parseIntegerExpression(children);
329
426
        Expr_ptr expr2 = parseIntegerExpression(children->next_sibling());
330
 
        if(expr1 == nullptr || expr2 == nullptr) return nullptr;
 
427
        if(expr1 == nullptr || expr2 == nullptr) 
 
428
        {
 
429
            assert(false);
 
430
            return nullptr;       
 
431
        }
331
432
        if (elementName == "integer-eq") return std::make_shared<EqualCondition>(expr1, expr2);
332
433
        else if (elementName == "integer-ne") return std::make_shared<NotEqualCondition>(expr1, expr2);
333
434
        else if (elementName == "integer-lt") return std::make_shared<LessThanCondition>(expr1, expr2);
336
437
        else if (elementName == "integer-ge") return std::make_shared<GreaterThanOrEqualCondition>(expr1, expr2);        
337
438
    } else if (elementName == "is-fireable") {
338
439
        size_t nrOfChildren = getChildCount(element);
339
 
        if (nrOfChildren == 0) return nullptr;
 
440
        if (nrOfChildren == 0) 
 
441
        {
 
442
            assert(false);
 
443
            return nullptr;       
 
444
        }
340
445
        std::vector<Condition_ptr> conds;
341
446
        for (auto it = element->first_node(); it; it = it->next_sibling()) {
342
 
            if (strcmp(it->name(), "transition") != 0) return nullptr;            
 
447
            if (strcmp(it->name(), "transition") != 0) 
 
448
            {
 
449
                assert(false);
 
450
                return nullptr;       
 
451
            }
343
452
            conds.emplace_back(std::make_shared<FireableCondition>(it->value()));
344
453
        }
345
454
        return std::make_shared<OrCondition>(conds);
346
455
    }
 
456
    std::cout << elementName << std::endl;
 
457
    assert(false);
347
458
    return nullptr;
348
459
}
349
460
 
351
462
    string elementName = element->name();
352
463
    if (elementName == "integer-constant") {
353
464
        int i;
354
 
        if (sscanf(element->value(), "%d", &i) == EOF) return nullptr; // expected integer at this place
 
465
        if (sscanf(element->value(), "%d", &i) == EOF) 
 
466
        {
 
467
            assert(false);
 
468
            return nullptr;       
 
469
        }
355
470
        return std::make_shared<LiteralExpr>(i);
356
471
    } else if (elementName == "tokens-count") {
357
472
        auto children = element->first_node();
372
487
            ids.emplace_back(id);
373
488
        }
374
489
        
375
 
        if (ids.size() == 0) return nullptr;
 
490
        if (ids.size() == 0) 
 
491
        {
 
492
            assert(false);
 
493
            return nullptr;       
 
494
        }
376
495
        if (ids.size() == 1) return ids[0];
377
496
        
378
497
        return std::make_shared<PlusExpr>(std::move(ids), true);
387
506
       
388
507
        for (; it; it = it->next_sibling()) {
389
508
            els.emplace_back(parseIntegerExpression(it));
390
 
            if(!els.back())  return nullptr;
 
509
            if(!els.back())  
 
510
        {
 
511
            assert(false);
 
512
            return nullptr;       
 
513
        }
391
514
        }
392
515
 
393
 
        if (els.size() < 2)  return nullptr; // at least two integer subexpression are required
 
516
        if (els.size() < 2) 
 
517
        {
 
518
            assert(false);
 
519
            return nullptr;       
 
520
        }
394
521
 
395
522
        return  isMult ? 
396
523
                std::dynamic_pointer_cast<Expr>(std::make_shared<MultiplyExpr>(std::move(els))) :
406
533
            els.emplace(els.begin(), std::make_shared<LiteralExpr>(0));
407
534
        return std::make_shared<SubtractExpr>(std::move(els));
408
535
    }
 
536
    assert(false);
409
537
    return nullptr;
410
538
}
411
539