← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Colored/Expressions.h

  • 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:
PetriEngine/Colored/Expressions.h
1
 
/*
2
 
 * To change this license header, choose License Headers in Project Properties.
3
 
 * To change this template file, choose Tools | Templates
4
 
 * and open the template in the editor.
5
 
 */
6
 
 
7
 
/* 
8
 
 * File:   Expressions.h
9
 
 * Author: andreas
10
 
 *
11
 
 * Created on February 19, 2018, 7:00 PM
12
 
 */
13
 
 
14
 
#ifndef COLORED_EXPRESSIONS_H
15
 
#define COLORED_EXPRESSIONS_H
16
 
 
17
 
#include <string>
18
 
#include <unordered_map>
19
 
#include <set>
20
 
#include <stdlib.h>
21
 
#include <iostream>
22
 
#include <cassert>
23
 
#include <memory>
24
 
 
25
 
 
26
 
#include "Colors.h"
27
 
#include "Multiset.h"
28
 
#include "PetriEngine/errorcodes.h"
29
 
 
30
 
namespace PetriEngine {
31
 
    class ColoredPetriNetBuilder;
32
 
    
33
 
    namespace Colored {
34
 
        struct ExpressionContext {
35
 
            typedef std::unordered_map<std::string, const Color*> BindingMap;
36
 
 
37
 
            BindingMap& binding;
38
 
            std::unordered_map<std::string, ColorType*>& colorTypes;
39
 
            
40
 
            const Color* findColor(const std::string& color) const {
41
 
                if (color.compare("dot") == 0)
42
 
                    return DotConstant::dotConstant();
43
 
                for (auto& elem : colorTypes) {
44
 
                    auto col = (*elem.second)[color];
45
 
                    if (col)
46
 
                        return col;
47
 
                }
48
 
                printf("Could not find color: %s\nCANNOT_COMPUTE\n", color.c_str());
49
 
                exit(ErrorCode);
50
 
            }
51
 
 
52
 
            ProductType* findProductColorType(const std::vector<const ColorType*>& types) const {
53
 
                for (auto& elem : colorTypes) {
54
 
                    auto* pt = dynamic_cast<ProductType*>(elem.second);
55
 
                    if (pt && pt->containsTypes(types)) {
56
 
                        return pt;
57
 
                    }
58
 
                }
59
 
                return nullptr;
60
 
            }
61
 
        };
62
 
 
63
 
        class WeightException : public std::exception {
64
 
        private:
65
 
            std::string _message;
66
 
        public:
67
 
            explicit WeightException(std::string message) : _message(message) {}
68
 
 
69
 
            const char* what() const noexcept override {
70
 
                return ("Undefined weight: " + _message).c_str();
71
 
            }
72
 
        };
73
 
        
74
 
        class Expression {
75
 
        public:
76
 
            Expression() {}
77
 
            
78
 
            virtual void getVariables(std::set<Variable*>& variables) const {
79
 
            }
80
 
            
81
 
            virtual void expressionType() {
82
 
                std::cout << "Expression" << std::endl;
83
 
            }
84
 
 
85
 
            virtual std::string toString() const {
86
 
                return "Unsupported";
87
 
            }
88
 
        };
89
 
        
90
 
        class ColorExpression : public Expression {
91
 
        public:
92
 
            ColorExpression() {}
93
 
            virtual ~ColorExpression() {}
94
 
            
95
 
            virtual const Color* eval(ExpressionContext& context) const = 0;
96
 
        };
97
 
        
98
 
        class DotConstantExpression : public ColorExpression {
99
 
        public:
100
 
            const Color* eval(ExpressionContext& context) const override {
101
 
                return DotConstant::dotConstant();
102
 
            }
103
 
        };
104
 
 
105
 
        typedef std::shared_ptr<ColorExpression> ColorExpression_ptr;
106
 
        
107
 
        class VariableExpression : public ColorExpression {
108
 
        private:
109
 
            Variable* _variable;
110
 
            
111
 
        public:
112
 
            const Color* eval(ExpressionContext& context) const override {
113
 
                return context.binding[_variable->name];
114
 
            }
115
 
            
116
 
            void getVariables(std::set<Variable*>& variables) const override {
117
 
                variables.insert(_variable);
118
 
            }
119
 
 
120
 
            std::string toString() const override {
121
 
                return _variable->name;
122
 
            }
123
 
 
124
 
            VariableExpression(Variable* variable)
125
 
                    : _variable(variable) {}
126
 
        };
127
 
        
128
 
        class UserOperatorExpression : public ColorExpression {
129
 
        private:
130
 
            const Color* _userOperator;
131
 
            
132
 
        public:
133
 
            const Color* eval(ExpressionContext& context) const override {
134
 
                return _userOperator;
135
 
            }
136
 
 
137
 
            std::string toString() const override {
138
 
                return _userOperator->toString();
139
 
            }
140
 
 
141
 
            UserOperatorExpression(const Color* userOperator)
142
 
                    : _userOperator(userOperator) {}
143
 
        };
144
 
        
145
 
        class UserSortExpression : public Expression {
146
 
        private:
147
 
            ColorType* _userSort;
148
 
            
149
 
        public:
150
 
            ColorType* eval(ExpressionContext& context) const {
151
 
                return _userSort;
152
 
            }
153
 
 
154
 
            std::string toString() const override {
155
 
                return _userSort->getName();
156
 
            }
157
 
 
158
 
            UserSortExpression(ColorType* userSort)
159
 
                    : _userSort(userSort) {}
160
 
        };
161
 
 
162
 
        typedef std::shared_ptr<UserSortExpression> UserSortExpression_ptr;
163
 
        
164
 
        class NumberConstantExpression : public Expression {
165
 
        private:
166
 
            uint32_t _number;
167
 
            
168
 
        public:
169
 
            uint32_t eval(ExpressionContext& context) const {
170
 
                return _number;
171
 
            }
172
 
            
173
 
            NumberConstantExpression(uint32_t number)
174
 
                    : _number(number) {}
175
 
        };
176
 
 
177
 
        typedef std::shared_ptr<NumberConstantExpression> NumberConstantExpression_ptr;
178
 
        
179
 
        class SuccessorExpression : public ColorExpression {
180
 
        private:
181
 
            ColorExpression_ptr _color;
182
 
            
183
 
        public:
184
 
            const Color* eval(ExpressionContext& context) const override {
185
 
                return &++(*_color->eval(context));
186
 
            }
187
 
            
188
 
            void getVariables(std::set<Variable*>& variables) const override {
189
 
                _color->getVariables(variables);
190
 
            }
191
 
 
192
 
            std::string toString() const override {
193
 
                return _color->toString() + "++";
194
 
            }
195
 
 
196
 
            SuccessorExpression(ColorExpression_ptr&& color)
197
 
                    : _color(std::move(color)) {}
198
 
        };
199
 
        
200
 
        class PredecessorExpression : public ColorExpression {
201
 
        private:
202
 
            ColorExpression_ptr _color;
203
 
            
204
 
        public:
205
 
            const Color* eval(ExpressionContext& context) const override {
206
 
                return &--(*_color->eval(context));
207
 
            }
208
 
            
209
 
            void getVariables(std::set<Variable*>& variables) const override {
210
 
                _color->getVariables(variables);
211
 
            }
212
 
 
213
 
            std::string toString() const override {
214
 
                return _color->toString() + "--";
215
 
            }
216
 
 
217
 
            PredecessorExpression(ColorExpression_ptr&& color)
218
 
                    : _color(std::move(color)) {}
219
 
        };
220
 
        
221
 
        class TupleExpression : public ColorExpression {
222
 
        private:
223
 
            std::vector<ColorExpression_ptr> _colors;
224
 
            
225
 
        public:
226
 
            const Color* eval(ExpressionContext& context) const override {
227
 
                std::vector<const Color*> colors;
228
 
                std::vector<const ColorType*> types;
229
 
                for (auto color : _colors) {
230
 
                    colors.push_back(color->eval(context));
231
 
                    types.push_back(colors.back()->getColorType());
232
 
                }
233
 
                ProductType* pt = context.findProductColorType(types);
234
 
 
235
 
                const Color* col = pt->getColor(colors);
236
 
                assert(col != nullptr);
237
 
                return col;
238
 
            }
239
 
            
240
 
            void getVariables(std::set<Variable*>& variables) const override {
241
 
                for (auto elem : _colors) {
242
 
                    elem->getVariables(variables);
243
 
                }
244
 
            }
245
 
 
246
 
            std::string toString() const override {
247
 
                std::string res = "(" + _colors[0]->toString();
248
 
                for (uint32_t i = 1; i < _colors.size(); ++i) {
249
 
                    res += "," + _colors[i]->toString();
250
 
                }
251
 
                res += ")";
252
 
                return res;
253
 
            }
254
 
 
255
 
            TupleExpression(std::vector<ColorExpression_ptr>&& colors)
256
 
                    : _colors(std::move(colors)) {}
257
 
        };
258
 
        
259
 
        class GuardExpression : public Expression {
260
 
        public:
261
 
            GuardExpression() {}
262
 
            virtual ~GuardExpression() {}
263
 
            
264
 
            virtual bool eval(ExpressionContext& context) const = 0;
265
 
        };
266
 
 
267
 
        typedef std::shared_ptr<GuardExpression> GuardExpression_ptr;
268
 
        
269
 
        class LessThanExpression : public GuardExpression {
270
 
        private:
271
 
            ColorExpression_ptr _left;
272
 
            ColorExpression_ptr _right;
273
 
            
274
 
        public:
275
 
            bool eval(ExpressionContext& context) const override {
276
 
                return _left->eval(context) < _right->eval(context);
277
 
            }
278
 
            
279
 
            void getVariables(std::set<Variable*>& variables) const override {
280
 
                _left->getVariables(variables);
281
 
                _right->getVariables(variables);
282
 
            }
283
 
            
284
 
            LessThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
285
 
                    : _left(std::move(left)), _right(std::move(right)) {}
286
 
        };
287
 
        
288
 
        class GreaterThanExpression : public GuardExpression {
289
 
        private:
290
 
            ColorExpression_ptr _left;
291
 
            ColorExpression_ptr _right;
292
 
            
293
 
        public:
294
 
            bool eval(ExpressionContext& context) const override {
295
 
                return _left->eval(context) > _right->eval(context);
296
 
            }
297
 
            
298
 
            void getVariables(std::set<Variable*>& variables) const override {
299
 
                _left->getVariables(variables);
300
 
                _right->getVariables(variables);
301
 
            }
302
 
            
303
 
            GreaterThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
304
 
                    : _left(std::move(left)), _right(std::move(right)) {}
305
 
        };
306
 
        
307
 
        class LessThanEqExpression : public GuardExpression {
308
 
        private:
309
 
            ColorExpression_ptr _left;
310
 
            ColorExpression_ptr _right;
311
 
            
312
 
        public:
313
 
            bool eval(ExpressionContext& context) const override {
314
 
                return _left->eval(context) <= _right->eval(context);
315
 
            }
316
 
            
317
 
            void getVariables(std::set<Variable*>& variables) const override {
318
 
                _left->getVariables(variables);
319
 
                _right->getVariables(variables);
320
 
            }
321
 
            
322
 
            LessThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
323
 
                    : _left(std::move(left)), _right(std::move(right)) {}
324
 
        };
325
 
        
326
 
        class GreaterThanEqExpression : public GuardExpression {
327
 
        private:
328
 
            ColorExpression_ptr _left;
329
 
            ColorExpression_ptr _right;
330
 
            
331
 
        public:
332
 
            bool eval(ExpressionContext& context) const override {
333
 
                return _left->eval(context) >= _right->eval(context);
334
 
            }
335
 
            
336
 
            void getVariables(std::set<Variable*>& variables) const override {
337
 
                _left->getVariables(variables);
338
 
                _right->getVariables(variables);
339
 
            }
340
 
            
341
 
            GreaterThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
342
 
                    : _left(std::move(left)), _right(std::move(right)) {}
343
 
        };
344
 
        
345
 
        class EqualityExpression : public GuardExpression {
346
 
        private:
347
 
            ColorExpression_ptr _left;
348
 
            ColorExpression_ptr _right;
349
 
            
350
 
        public:
351
 
            bool eval(ExpressionContext& context) const override {
352
 
                return _left->eval(context) == _right->eval(context);
353
 
            }
354
 
            
355
 
            void getVariables(std::set<Variable*>& variables) const override {
356
 
                _left->getVariables(variables);
357
 
                _right->getVariables(variables);
358
 
            }
359
 
            
360
 
            EqualityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
361
 
                    : _left(std::move(left)), _right(std::move(right)) {}
362
 
        };
363
 
        
364
 
        class InequalityExpression : public GuardExpression {
365
 
        private:
366
 
            ColorExpression_ptr _left;
367
 
            ColorExpression_ptr _right;
368
 
            
369
 
        public:
370
 
            bool eval(ExpressionContext& context) const override {
371
 
                return _left->eval(context) != _right->eval(context);
372
 
            }
373
 
            
374
 
            void getVariables(std::set<Variable*>& variables) const override {
375
 
                _left->getVariables(variables);
376
 
                _right->getVariables(variables);
377
 
            }
378
 
            
379
 
            InequalityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
380
 
                    : _left(std::move(left)), _right(std::move(right)) {}
381
 
        };
382
 
        
383
 
        class NotExpression : public GuardExpression {
384
 
        private:
385
 
            GuardExpression_ptr _expr;
386
 
            
387
 
        public:
388
 
            bool eval(ExpressionContext& context) const override {
389
 
                return !_expr->eval(context);
390
 
            }
391
 
            
392
 
            void getVariables(std::set<Variable*>& variables) const override {
393
 
                _expr->getVariables(variables);
394
 
            }
395
 
            
396
 
            NotExpression(GuardExpression_ptr&& expr) : _expr(std::move(expr)) {}
397
 
        };
398
 
        
399
 
        class AndExpression : public GuardExpression {
400
 
        private:
401
 
            GuardExpression_ptr _left;
402
 
            GuardExpression_ptr _right;
403
 
            
404
 
        public:
405
 
            bool eval(ExpressionContext& context) const override {
406
 
                return _left->eval(context) && _right->eval(context);
407
 
            }
408
 
            
409
 
            void getVariables(std::set<Variable*>& variables) const override {
410
 
                _left->getVariables(variables);
411
 
                _right->getVariables(variables);
412
 
            }
413
 
            
414
 
            AndExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right)
415
 
                    : _left(left), _right(right) {}
416
 
        };
417
 
        
418
 
        class OrExpression : public GuardExpression {
419
 
        private:
420
 
            GuardExpression_ptr _left;
421
 
            GuardExpression_ptr _right;
422
 
            
423
 
        public:
424
 
            bool eval(ExpressionContext& context) const override {
425
 
                return _left->eval(context) || _right->eval(context);
426
 
            }
427
 
            
428
 
            void getVariables(std::set<Variable*>& variables) const override {
429
 
                _left->getVariables(variables);
430
 
                _right->getVariables(variables);
431
 
            }
432
 
            
433
 
            OrExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right)
434
 
                    : _left(std::move(left)), _right(std::move(right)) {}
435
 
        };
436
 
        
437
 
        class ArcExpression : public Expression {
438
 
        public:
439
 
            ArcExpression() {}
440
 
            virtual ~ArcExpression() {}
441
 
            
442
 
            virtual Multiset eval(ExpressionContext& context) const = 0;
443
 
 
444
 
            virtual void expressionType() override {
445
 
                std::cout << "ArcExpression" << std::endl;
446
 
            }
447
 
 
448
 
            virtual uint32_t weight() const = 0;
449
 
        };
450
 
 
451
 
        typedef std::shared_ptr<ArcExpression> ArcExpression_ptr;
452
 
        
453
 
        class AllExpression : public Expression {
454
 
        private:
455
 
            ColorType* _sort;
456
 
            
457
 
        public:
458
 
            std::vector<const Color*> eval(ExpressionContext& context) const {
459
 
                std::vector<const Color*> colors;
460
 
                assert(_sort != nullptr);
461
 
                for (size_t i = 0; i < _sort->size(); i++) {
462
 
                    colors.push_back(&(*_sort)[i]);
463
 
                }
464
 
                return colors;
465
 
            }
466
 
 
467
 
            size_t size() const {
468
 
                return  _sort->size();
469
 
            }
470
 
 
471
 
            std::string toString() const override {
472
 
                return _sort->getName() + ".all";
473
 
            }
474
 
 
475
 
            AllExpression(ColorType* sort) : _sort(sort) 
476
 
            {
477
 
                assert(sort != nullptr);
478
 
            }
479
 
        };
480
 
 
481
 
        typedef std::shared_ptr<AllExpression> AllExpression_ptr;
482
 
        
483
 
        class NumberOfExpression : public ArcExpression {
484
 
        private:
485
 
            uint32_t _number;
486
 
            std::vector<ColorExpression_ptr> _color;
487
 
            AllExpression_ptr _all;
488
 
            
489
 
        public:
490
 
            Multiset eval(ExpressionContext& context) const override {
491
 
                std::vector<const Color*> colors;
492
 
                if (!_color.empty()) {
493
 
                    for (auto elem : _color) {
494
 
                        colors.push_back(elem->eval(context));
495
 
                    }
496
 
                } else if (_all != nullptr) {
497
 
                    colors = _all->eval(context);
498
 
                }
499
 
                std::vector<std::pair<const Color*,uint32_t>> col;
500
 
                for (auto elem : colors) {
501
 
                    col.push_back(std::make_pair(elem, _number));
502
 
                }
503
 
                return Multiset(col);
504
 
            }
505
 
            
506
 
            void getVariables(std::set<Variable*>& variables) const override {
507
 
                if (_all != nullptr)
508
 
                    return;
509
 
                for (auto elem : _color) {
510
 
                    elem->getVariables(variables);
511
 
                }
512
 
            }
513
 
 
514
 
            uint32_t weight() const override {
515
 
                if (_all == nullptr)
516
 
                    return _number * _color.size();
517
 
                else
518
 
                    return _number * _all->size();
519
 
            }
520
 
 
521
 
            bool isAll() const {
522
 
                return (bool)_all;
523
 
            }
524
 
 
525
 
            bool isSingleColor() const {
526
 
                return !isAll() && _color.size() == 1;
527
 
            }
528
 
 
529
 
            uint32_t number() const {
530
 
                return _number;
531
 
            }
532
 
 
533
 
            std::string toString() const override {
534
 
                if (isAll())
535
 
                    return std::to_string(_number) + "'(" + _all->toString() + ")";
536
 
                std::string res = std::to_string(_number) + "'(" + _color[0]->toString() + ")";
537
 
                for (uint32_t i = 1; i < _color.size(); ++i) {
538
 
                    res += " + ";
539
 
                    res += std::to_string(_number) + "'(" + _color[i]->toString() + ")";
540
 
                }
541
 
                return res;
542
 
            }
543
 
 
544
 
            NumberOfExpression(std::vector<ColorExpression_ptr>&& color, uint32_t number = 1)
545
 
                    : _number(number), _color(std::move(color)), _all(nullptr) {}
546
 
            NumberOfExpression(AllExpression_ptr&& all, uint32_t number = 1)
547
 
                    : _number(number), _color(), _all(std::move(all)) {}
548
 
        };
549
 
 
550
 
        typedef std::shared_ptr<NumberOfExpression> NumberOfExpression_ptr;
551
 
        
552
 
        class AddExpression : public ArcExpression {
553
 
        private:
554
 
            std::vector<ArcExpression_ptr> _constituents;
555
 
            
556
 
        public:
557
 
            Multiset eval(ExpressionContext& context) const override {
558
 
                Multiset ms;
559
 
                for (auto expr : _constituents) {
560
 
                    ms += expr->eval(context);
561
 
                }
562
 
                return ms;
563
 
            }
564
 
            
565
 
            void getVariables(std::set<Variable*>& variables) const override {
566
 
                for (auto elem : _constituents) {
567
 
                    elem->getVariables(variables);
568
 
                }
569
 
            }
570
 
 
571
 
            uint32_t weight() const override {
572
 
                uint32_t res = 0;
573
 
                for (auto expr : _constituents) {
574
 
                    res += expr->weight();
575
 
                }
576
 
                return res;
577
 
            }
578
 
 
579
 
            std::string toString() const override {
580
 
                std::string res = _constituents[0]->toString();
581
 
                for (uint32_t i = 1; i < _constituents.size(); ++i) {
582
 
                    res += " + " + _constituents[i]->toString();
583
 
                }
584
 
                return res;
585
 
            }
586
 
 
587
 
            AddExpression(std::vector<ArcExpression_ptr>&& constituents)
588
 
                    : _constituents(std::move(constituents)) {}
589
 
        };
590
 
        
591
 
        class SubtractExpression : public ArcExpression {
592
 
        private:
593
 
            ArcExpression_ptr _left;
594
 
            ArcExpression_ptr _right;
595
 
            
596
 
        public:
597
 
            Multiset eval(ExpressionContext& context) const override {
598
 
                return _left->eval(context) - _right->eval(context);
599
 
            }
600
 
            
601
 
            void getVariables(std::set<Variable*>& variables) const override {
602
 
                _left->getVariables(variables);
603
 
                _right->getVariables(variables);
604
 
            }
605
 
 
606
 
            uint32_t weight() const override {
607
 
                auto* left = dynamic_cast<NumberOfExpression*>(_left.get());
608
 
                if (!left || !left->isAll()) {
609
 
                    throw WeightException("Left constituent of subtract is not an all expression!");
610
 
                }
611
 
                auto* right = dynamic_cast<NumberOfExpression*>(_right.get());
612
 
                if (!right || !right->isSingleColor()) {
613
 
                    throw WeightException("Right constituent of subtract is not a single color number of expression!");
614
 
                }
615
 
 
616
 
                uint32_t val = std::min(left->number(), right->number());
617
 
                return _left->weight() - val;
618
 
            }
619
 
 
620
 
            std::string toString() const override {
621
 
                return _left->toString() + " - " + _right->toString();
622
 
            }
623
 
 
624
 
            SubtractExpression(ArcExpression_ptr&& left, ArcExpression_ptr&& right)
625
 
                    : _left(std::move(left)), _right(std::move(right)) {}
626
 
        };
627
 
        
628
 
        class ScalarProductExpression : public ArcExpression {
629
 
        private:
630
 
            uint32_t _scalar;
631
 
            ArcExpression_ptr _expr;
632
 
            
633
 
        public:
634
 
            Multiset eval(ExpressionContext& context) const override {
635
 
                return _expr->eval(context) * _scalar;
636
 
            }
637
 
            
638
 
            void getVariables(std::set<Variable*>& variables) const override {
639
 
                _expr->getVariables(variables);
640
 
            }
641
 
 
642
 
            uint32_t weight() const override {
643
 
                return _scalar * _expr->weight();
644
 
            }
645
 
 
646
 
            std::string toString() const override {
647
 
                return std::to_string(_scalar) + " * " + _expr->toString();
648
 
            }
649
 
 
650
 
            ScalarProductExpression(ArcExpression_ptr&& expr, uint32_t scalar)
651
 
                    : _scalar(std::move(scalar)), _expr(expr) {}
652
 
        };
653
 
    }
654
 
}
655
 
 
656
 
#endif /* COLORED_EXPRESSIONS_H */
657