← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/Colored/Colors.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/Colors.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:   Colors.h
 
9
 * Author: andreas
 
10
 *
 
11
 * Created on February 19, 2018, 8:22 PM
 
12
 */
 
13
 
 
14
#ifndef COLORS_H
 
15
#define COLORS_H
 
16
 
 
17
#include <stdint.h>
 
18
#include <stddef.h>
 
19
#include <string>
 
20
#include <string.h>
 
21
#include <utility>
 
22
#include <vector>
 
23
#include <unordered_map>
 
24
 
 
25
namespace PetriEngine {
 
26
    namespace Colored {
 
27
        class ColorType;
 
28
 
 
29
        class Color {
 
30
        public:
 
31
            friend std::ostream& operator<< (std::ostream& stream, const Color& color);
 
32
            
 
33
        protected:
 
34
            const std::vector<const Color*> _tuple;
 
35
            ColorType* _colorType;
 
36
            std::string _colorName;
 
37
            uint32_t _id;
 
38
            
 
39
        public:
 
40
            Color(ColorType* colorType, uint32_t id, std::vector<const Color*>& colors);
 
41
            Color(ColorType* colorType, uint32_t id, const char* color);
 
42
            ~Color() {}
 
43
            
 
44
            bool isTuple() const {
 
45
                return _tuple.size() > 1;
 
46
            }
 
47
            
 
48
            const std::string& getColorName() const {
 
49
                if (this->isTuple()) {
 
50
                    throw "Cannot get color from a tuple color.";
 
51
                }
 
52
                return _colorName;
 
53
            }
 
54
            
 
55
            ColorType* getColorType() const {
 
56
                return _colorType;
 
57
            }
 
58
            
 
59
            uint32_t getId() const {
 
60
                return _id;
 
61
            }
 
62
            
 
63
            const Color* operator[] (size_t index) const;
 
64
            bool operator< (const Color& other) const;
 
65
            bool operator> (const Color& other) const;
 
66
            bool operator<= (const Color& other) const;
 
67
            bool operator>= (const Color& other) const;
 
68
            
 
69
            bool operator== (const Color& other) const {
 
70
                return _colorType == other._colorType && _id == other._id;
 
71
            }
 
72
            bool operator!= (const Color& other) const {
 
73
                return !((*this) == other);
 
74
            }
 
75
            
 
76
            const Color& operator++ () const;
 
77
            const Color& operator-- () const;
 
78
            
 
79
            std::string toString() const;
 
80
            static std::string toString(const Color* color);
 
81
            static std::string toString(const std::vector<const Color*>& colors);
 
82
        };
 
83
        
 
84
        /*
 
85
         *  Singleton pattern from: 
 
86
         * https://stackoverflow.com/questions/1008019/c-singleton-design-pattern
 
87
         */
 
88
        class DotConstant : public Color {
 
89
        private:
 
90
            DotConstant();
 
91
            
 
92
        public:
 
93
            static const Color* dotConstant() {
 
94
                static DotConstant _instance;
 
95
                
 
96
                return &_instance;
 
97
            }
 
98
            
 
99
            DotConstant(DotConstant const&) = delete;
 
100
            void operator=(DotConstant const&) = delete;
 
101
 
 
102
            bool operator== (const DotConstant& other) {
 
103
                return true;
 
104
            }
 
105
        };
 
106
        
 
107
        class ColorType {
 
108
        public:
 
109
            class iterator {
 
110
            private:
 
111
                ColorType& type;
 
112
                size_t index;
 
113
 
 
114
            public:
 
115
                iterator(ColorType& type, size_t index) : type(type), index(index) {}
 
116
 
 
117
                const Color& operator++() {
 
118
                    return type[++index];
 
119
                }
 
120
 
 
121
                const Color& operator++(int) {
 
122
                    return type[index++];
 
123
                }
 
124
 
 
125
                const Color& operator--() {
 
126
                    return type[--index];
 
127
                }
 
128
                const Color& operator--(int) {
 
129
                    return type[index--];
 
130
                }
 
131
 
 
132
                const Color& operator*() {
 
133
                    return type[index];
 
134
                }
 
135
 
 
136
                const Color* operator->() {
 
137
                    return &type[index];
 
138
                }
 
139
 
 
140
                bool operator==(iterator& other) {
 
141
                    return type == other.type && index == other.index;
 
142
                }
 
143
 
 
144
                bool operator!=(iterator& other) {
 
145
                    return !(type == other.type) || index != other.index;
 
146
                }
 
147
            };
 
148
            
 
149
        private:
 
150
            std::vector<Color> _colors;
 
151
            uintptr_t _id;
 
152
            std::string _name;
 
153
            
 
154
        public:
 
155
            ColorType(std::vector<ColorType*> elements);
 
156
            ColorType(std::string name = "Undefined") : _colors(), _name(std::move(name)) {
 
157
                _id = (uintptr_t)this;
 
158
            }
 
159
            
 
160
            virtual void addColor(const char* colorName);
 
161
            virtual void addColor(std::vector<const Color*>& colors);
 
162
            virtual void addDot() {
 
163
                _colors.push_back(*DotConstant::dotConstant());
 
164
            }
 
165
            
 
166
            virtual size_t size() const {
 
167
                return _colors.size();
 
168
            }
 
169
            
 
170
            virtual const Color& operator[] (size_t index) {
 
171
                return _colors[index];
 
172
            }
 
173
            
 
174
            virtual const Color& operator[] (int index) {
 
175
                return _colors[index];
 
176
            }
 
177
            
 
178
            virtual const Color& operator[] (uint32_t index) {
 
179
                return _colors[index];
 
180
            }
 
181
            
 
182
            virtual const Color* operator[] (const char* index);
 
183
            
 
184
            virtual const Color* operator[] (const std::string& index) {
 
185
                return (*this)[index.c_str()];
 
186
            }
 
187
            
 
188
            bool operator== (const ColorType& other) const {
 
189
                return _id == other._id;
 
190
            }
 
191
 
 
192
            uintptr_t getId() {
 
193
                return _id;
 
194
            }
 
195
 
 
196
            const std::string& getName() const {
 
197
                return _name;
 
198
            }
 
199
            
 
200
            iterator begin() {
 
201
                return {*this, 0};
 
202
            }
 
203
 
 
204
            iterator end() {
 
205
                return {*this, size()};
 
206
            }
 
207
        };
 
208
 
 
209
        class ProductType : public ColorType {
 
210
        private:
 
211
            std::vector<ColorType*> constituents;
 
212
            std::unordered_map<size_t,Color> cache;
 
213
 
 
214
        public:
 
215
            ProductType(const std::string& name = "Undefined") : ColorType(name) {}
 
216
            ~ProductType() {
 
217
                cache.clear();
 
218
            }
 
219
 
 
220
            void addType(ColorType* type) {
 
221
                constituents.push_back(type);
 
222
            }
 
223
 
 
224
            void addColor(const char* colorName) override {}
 
225
            void addColor(std::vector<const Color*>& colors) override {}
 
226
            void addDot() override {}
 
227
 
 
228
            size_t size() const override {
 
229
                size_t product = 1;
 
230
                for (auto ct : constituents) {
 
231
                    product *= ct->size();
 
232
                }
 
233
                return product;
 
234
            }
 
235
 
 
236
            bool containsTypes(const std::vector<const ColorType*>& types) const {
 
237
                if (constituents.size() != types.size()) return false;
 
238
 
 
239
                for (size_t i = 0; i < constituents.size(); ++i) {
 
240
                    if (!(*constituents[i] == *types[i])) {
 
241
                        return false;
 
242
                    }
 
243
                }
 
244
 
 
245
                return true;
 
246
            }
 
247
 
 
248
            const Color* getColor(const std::vector<const Color*>& colors);
 
249
 
 
250
            const Color& operator[](size_t index) override;
 
251
            const Color& operator[](int index) override {
 
252
                return operator[]((size_t)index);
 
253
            }
 
254
            const Color& operator[](uint32_t index) override {
 
255
                return operator[]((size_t)index);
 
256
            }
 
257
 
 
258
            const Color* operator[](const char* index) override;
 
259
            const Color* operator[](const std::string& index) override;
 
260
        };
 
261
        
 
262
        struct Variable {
 
263
            std::string name;
 
264
            ColorType* colorType;
 
265
        };
 
266
        
 
267
        struct Binding {
 
268
            Variable* var;
 
269
            const Color* color;
 
270
            
 
271
            bool operator==(Binding& other) {
 
272
                return var->name.compare(other.var->name);
 
273
            }
 
274
        };
 
275
    }
 
276
}
 
277
 
 
278
#endif /* COLORS_H */
 
279