← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/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:
include/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 "../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
            virtual ~AllExpression() {};
 
459
            std::vector<const Color*> eval(ExpressionContext& context) const {
 
460
                std::vector<const Color*> colors;
 
461
                assert(_sort != nullptr);
 
462
                for (size_t i = 0; i < _sort->size(); i++) {
 
463
                    colors.push_back(&(*_sort)[i]);
 
464
                }
 
465
                return colors;
 
466
            }
 
467
 
 
468
            size_t size() const {
 
469
                return  _sort->size();
 
470
            }
 
471
 
 
472
            std::string toString() const override {
 
473
                return _sort->getName() + ".all";
 
474
            }
 
475
 
 
476
            AllExpression(ColorType* sort) : _sort(sort) 
 
477
            {
 
478
                assert(sort != nullptr);
 
479
            }
 
480
        };
 
481
 
 
482
        typedef std::shared_ptr<AllExpression> AllExpression_ptr;
 
483
        
 
484
        class NumberOfExpression : public ArcExpression {
 
485
        private:
 
486
            uint32_t _number;
 
487
            std::vector<ColorExpression_ptr> _color;
 
488
            AllExpression_ptr _all;
 
489
            
 
490
        public:
 
491
            Multiset eval(ExpressionContext& context) const override {
 
492
                std::vector<const Color*> colors;
 
493
                if (!_color.empty()) {
 
494
                    for (auto elem : _color) {
 
495
                        colors.push_back(elem->eval(context));
 
496
                    }
 
497
                } else if (_all != nullptr) {
 
498
                    colors = _all->eval(context);
 
499
                }
 
500
                std::vector<std::pair<const Color*,uint32_t>> col;
 
501
                for (auto elem : colors) {
 
502
                    col.push_back(std::make_pair(elem, _number));
 
503
                }
 
504
                return Multiset(col);
 
505
            }
 
506
            
 
507
            void getVariables(std::set<Variable*>& variables) const override {
 
508
                if (_all != nullptr)
 
509
                    return;
 
510
                for (auto elem : _color) {
 
511
                    elem->getVariables(variables);
 
512
                }
 
513
            }
 
514
 
 
515
            uint32_t weight() const override {
 
516
                if (_all == nullptr)
 
517
                    return _number * _color.size();
 
518
                else
 
519
                    return _number * _all->size();
 
520
            }
 
521
 
 
522
            bool isAll() const {
 
523
                return (bool)_all;
 
524
            }
 
525
 
 
526
            bool isSingleColor() const {
 
527
                return !isAll() && _color.size() == 1;
 
528
            }
 
529
 
 
530
            uint32_t number() const {
 
531
                return _number;
 
532
            }
 
533
 
 
534
            std::string toString() const override {
 
535
                if (isAll())
 
536
                    return std::to_string(_number) + "'(" + _all->toString() + ")";
 
537
                std::string res = std::to_string(_number) + "'(" + _color[0]->toString() + ")";
 
538
                for (uint32_t i = 1; i < _color.size(); ++i) {
 
539
                    res += " + ";
 
540
                    res += std::to_string(_number) + "'(" + _color[i]->toString() + ")";
 
541
                }
 
542
                return res;
 
543
            }
 
544
 
 
545
            NumberOfExpression(std::vector<ColorExpression_ptr>&& color, uint32_t number = 1)
 
546
                    : _number(number), _color(std::move(color)), _all(nullptr) {}
 
547
            NumberOfExpression(AllExpression_ptr&& all, uint32_t number = 1)
 
548
                    : _number(number), _color(), _all(std::move(all)) {}
 
549
        };
 
550
 
 
551
        typedef std::shared_ptr<NumberOfExpression> NumberOfExpression_ptr;
 
552
        
 
553
        class AddExpression : public ArcExpression {
 
554
        private:
 
555
            std::vector<ArcExpression_ptr> _constituents;
 
556
            
 
557
        public:
 
558
            Multiset eval(ExpressionContext& context) const override {
 
559
                Multiset ms;
 
560
                for (auto expr : _constituents) {
 
561
                    ms += expr->eval(context);
 
562
                }
 
563
                return ms;
 
564
            }
 
565
            
 
566
            void getVariables(std::set<Variable*>& variables) const override {
 
567
                for (auto elem : _constituents) {
 
568
                    elem->getVariables(variables);
 
569
                }
 
570
            }
 
571
 
 
572
            uint32_t weight() const override {
 
573
                uint32_t res = 0;
 
574
                for (auto expr : _constituents) {
 
575
                    res += expr->weight();
 
576
                }
 
577
                return res;
 
578
            }
 
579
 
 
580
            std::string toString() const override {
 
581
                std::string res = _constituents[0]->toString();
 
582
                for (uint32_t i = 1; i < _constituents.size(); ++i) {
 
583
                    res += " + " + _constituents[i]->toString();
 
584
                }
 
585
                return res;
 
586
            }
 
587
 
 
588
            AddExpression(std::vector<ArcExpression_ptr>&& constituents)
 
589
                    : _constituents(std::move(constituents)) {}
 
590
        };
 
591
        
 
592
        class SubtractExpression : public ArcExpression {
 
593
        private:
 
594
            ArcExpression_ptr _left;
 
595
            ArcExpression_ptr _right;
 
596
            
 
597
        public:
 
598
            Multiset eval(ExpressionContext& context) const override {
 
599
                return _left->eval(context) - _right->eval(context);
 
600
            }
 
601
            
 
602
            void getVariables(std::set<Variable*>& variables) const override {
 
603
                _left->getVariables(variables);
 
604
                _right->getVariables(variables);
 
605
            }
 
606
 
 
607
            uint32_t weight() const override {
 
608
                auto* left = dynamic_cast<NumberOfExpression*>(_left.get());
 
609
                if (!left || !left->isAll()) {
 
610
                    throw WeightException("Left constituent of subtract is not an all expression!");
 
611
                }
 
612
                auto* right = dynamic_cast<NumberOfExpression*>(_right.get());
 
613
                if (!right || !right->isSingleColor()) {
 
614
                    throw WeightException("Right constituent of subtract is not a single color number of expression!");
 
615
                }
 
616
 
 
617
                uint32_t val = std::min(left->number(), right->number());
 
618
                return _left->weight() - val;
 
619
            }
 
620
 
 
621
            std::string toString() const override {
 
622
                return _left->toString() + " - " + _right->toString();
 
623
            }
 
624
 
 
625
            SubtractExpression(ArcExpression_ptr&& left, ArcExpression_ptr&& right)
 
626
                    : _left(std::move(left)), _right(std::move(right)) {}
 
627
        };
 
628
        
 
629
        class ScalarProductExpression : public ArcExpression {
 
630
        private:
 
631
            uint32_t _scalar;
 
632
            ArcExpression_ptr _expr;
 
633
            
 
634
        public:
 
635
            Multiset eval(ExpressionContext& context) const override {
 
636
                return _expr->eval(context) * _scalar;
 
637
            }
 
638
            
 
639
            void getVariables(std::set<Variable*>& variables) const override {
 
640
                _expr->getVariables(variables);
 
641
            }
 
642
 
 
643
            uint32_t weight() const override {
 
644
                return _scalar * _expr->weight();
 
645
            }
 
646
 
 
647
            std::string toString() const override {
 
648
                return std::to_string(_scalar) + " * " + _expr->toString();
 
649
            }
 
650
 
 
651
            ScalarProductExpression(ArcExpression_ptr&& expr, uint32_t scalar)
 
652
                    : _scalar(std::move(scalar)), _expr(expr) {}
 
653
        };
 
654
    }
 
655
}
 
656
 
 
657
#endif /* COLORED_EXPRESSIONS_H */
 
658