← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/TAR/range.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/TAR/range.h
 
1
/*
 
2
 *  Copyright Peter G. Jensen, all rights reserved.
 
3
 */
 
4
 
 
5
/* 
 
6
 * File:   range.h
 
7
 * Author: Peter G. Jensen <root@petergjoel.dk>
 
8
 *
 
9
 * Created on March 31, 2020, 4:32 PM
 
10
 */
 
11
 
 
12
#ifndef RANGE_H
 
13
#define RANGE_H
 
14
 
 
15
#include <cinttypes>
 
16
#include <cassert>
 
17
#include <limits>
 
18
#include <iostream>
 
19
#include <vector>
 
20
 
 
21
namespace PetriEngine {
 
22
    namespace Reachability {
 
23
 
 
24
        struct range_t {
 
25
 
 
26
            static inline uint32_t min() {
 
27
                return std::numeric_limits<uint32_t>::min();
 
28
            }
 
29
 
 
30
            static inline uint32_t max() {
 
31
                return std::numeric_limits<uint32_t>::max();
 
32
            }
 
33
 
 
34
            range_t() {
 
35
            };
 
36
 
 
37
            explicit range_t(uint32_t val) : _lower(val), _upper(val) {
 
38
            }
 
39
 
 
40
            range_t(uint32_t l, uint32_t u) : _lower(l), _upper(u) {
 
41
                assert(_lower <= _upper);
 
42
            }
 
43
 
 
44
            uint32_t _lower = min();
 
45
            uint32_t _upper = max();
 
46
 
 
47
            bool no_upper() const {
 
48
                return _upper == max();
 
49
            }
 
50
 
 
51
            bool no_lower() const {
 
52
                return _lower == min();
 
53
            }
 
54
 
 
55
            bool unbound() const {
 
56
                return no_lower() && no_upper();
 
57
            }
 
58
 
 
59
            void free() {
 
60
                _upper = max();
 
61
                _lower = min();
 
62
            }
 
63
 
 
64
            std::ostream& print(std::ostream& os) const {
 
65
                if (no_lower())
 
66
                    os << "[0";
 
67
                else
 
68
                    os << "[" << _lower;
 
69
                os << ", ";
 
70
                if (no_upper())
 
71
                    os << "inf]";
 
72
                else
 
73
                    os << _upper << "]";
 
74
                return os;
 
75
            }
 
76
 
 
77
            std::pair<bool, bool> compare(const range_t& other) const {
 
78
                return std::make_pair(
 
79
                        _lower <= other._lower && _upper >= other._upper,
 
80
                        _lower >= other._lower && _upper <= other._upper
 
81
                        );
 
82
            }
 
83
 
 
84
            range_t& operator&=(const range_t& other) {
 
85
                _lower = std::max(_lower, other._lower);
 
86
                _upper = std::min(_upper, other._upper);
 
87
                return *this;
 
88
            }
 
89
 
 
90
            range_t& operator|=(const range_t& other) {
 
91
                _lower = std::min(_lower, other._lower);
 
92
                _upper = std::max(_upper, other._upper);
 
93
                return *this;
 
94
            }
 
95
 
 
96
            range_t& operator|=(uint32_t val) {
 
97
                _lower = std::min(val, _lower);
 
98
                _upper = std::max(val, _upper);
 
99
                return *this;
 
100
            }
 
101
 
 
102
            range_t& operator&=(uint32_t val) {
 
103
                _lower = val;
 
104
                _upper = val;
 
105
                return *this;
 
106
            }
 
107
 
 
108
            range_t& operator-=(uint32_t val) {
 
109
                if (_lower < min() + val)
 
110
                    _lower = min();
 
111
                else
 
112
                    _lower -= val;
 
113
                if (_upper != max()) {
 
114
                    if (_upper < min() + val) {
 
115
                        assert(false);
 
116
                    } else {
 
117
                        _upper -= val;
 
118
                    }
 
119
                }
 
120
                return *this;
 
121
            }
 
122
 
 
123
            range_t& operator+=(uint32_t val) {
 
124
                if (_lower != min()) {
 
125
                    if (_lower >= max() - val)
 
126
                        assert(false);
 
127
                    _lower += val;
 
128
                }
 
129
 
 
130
                if (_upper >= max() - val) {
 
131
                    _upper = max();
 
132
                } else
 
133
                    _upper += val;
 
134
                return *this;
 
135
            }
 
136
        };
 
137
 
 
138
        struct placerange_t {
 
139
            range_t _range;
 
140
            uint32_t _place = std::numeric_limits<uint32_t>::max();
 
141
 
 
142
            placerange_t() {
 
143
            }
 
144
 
 
145
            placerange_t(uint32_t place) : _place(place) {
 
146
            };
 
147
 
 
148
            placerange_t(uint32_t place, const range_t& r) : _range(r), _place(place) {
 
149
            };
 
150
 
 
151
            placerange_t(uint32_t place, range_t&& r) : _range(r), _place(place) {
 
152
            };
 
153
 
 
154
            placerange_t(uint32_t place, uint32_t v) : _range(v), _place(place) {
 
155
            };
 
156
 
 
157
            placerange_t(uint32_t place, uint32_t l, uint32_t u) : _range(l, u), _place(place) {
 
158
            };
 
159
 
 
160
            std::ostream& print(std::ostream& os) const {
 
161
                os << "<P" << _place << "> in ";
 
162
                return _range.print(os);
 
163
            }
 
164
 
 
165
            std::pair<bool, bool> compare(const range_t& other) const {
 
166
                return _range.compare(other);
 
167
            }
 
168
 
 
169
            std::pair<bool, bool> compare(const placerange_t& other) const {
 
170
                assert(other._place == _place);
 
171
                if (other._place != _place)
 
172
                    return std::make_pair(false, false);
 
173
                return _range.compare(other._range);
 
174
            }
 
175
 
 
176
            placerange_t& operator|=(uint32_t val) {
 
177
                _range |= val;
 
178
                return *this;
 
179
            }
 
180
 
 
181
            placerange_t& operator&=(uint32_t val) {
 
182
                _range &= val;
 
183
                return *this;
 
184
            }
 
185
 
 
186
            placerange_t& operator-=(uint32_t val) {
 
187
                _range -= val;
 
188
                return *this;
 
189
            }
 
190
 
 
191
            placerange_t& operator+=(uint32_t val) {
 
192
                _range += val;
 
193
                return *this;
 
194
            }
 
195
 
 
196
            placerange_t& operator&=(const placerange_t& other) {
 
197
                assert(other._place == _place);
 
198
                _range &= other._range;
 
199
                return *this;
 
200
            }
 
201
 
 
202
            placerange_t& operator|=(const placerange_t& other) {
 
203
                assert(other._place == _place);
 
204
                _range |= other._range;
 
205
                return *this;
 
206
            }
 
207
 
 
208
            // used for sorting only!
 
209
 
 
210
            bool operator<(const placerange_t& other) const {
 
211
                return _place < other._place;
 
212
            }
 
213
        };
 
214
 
 
215
        struct prvector_t {
 
216
            std::vector<placerange_t> _ranges;
 
217
 
 
218
            const placerange_t* operator[](uint32_t place) const {
 
219
                auto lb = std::lower_bound(_ranges.begin(), _ranges.end(), place);
 
220
                if (lb == _ranges.end() || lb->_place != place) {
 
221
                    return nullptr;
 
222
                } else {
 
223
                    return &(*lb);
 
224
                }
 
225
            }
 
226
 
 
227
            placerange_t* operator[](uint32_t place) {
 
228
                auto lb = std::lower_bound(_ranges.begin(), _ranges.end(), place);
 
229
                if (lb == _ranges.end() || lb->_place != place) {
 
230
                    return nullptr;
 
231
                } else {
 
232
                    return &(*lb);
 
233
                }
 
234
            }
 
235
 
 
236
            placerange_t& find_or_add(uint32_t place) {
 
237
                auto lb = std::lower_bound(_ranges.begin(), _ranges.end(), place);
 
238
                if (lb == _ranges.end() || lb->_place != place) {
 
239
                    lb = _ranges.emplace(lb, place);
 
240
                }
 
241
                return *lb;
 
242
            }
 
243
 
 
244
            uint32_t lower(uint32_t place) const {
 
245
                auto* pr = (*this)[place];
 
246
                if (pr == nullptr)
 
247
                    return range_t::min();
 
248
                return pr->_range._lower;
 
249
            }
 
250
 
 
251
            uint32_t upper(uint32_t place) const {
 
252
                auto* pr = (*this)[place];
 
253
                if (pr == nullptr)
 
254
                    return range_t::max();
 
255
                return pr->_range._upper;
 
256
            }
 
257
 
 
258
            bool unbound(uint32_t place) const {
 
259
                auto* pr = (*this)[place];
 
260
                if (pr == nullptr)
 
261
                    return true;
 
262
                return pr->_range.unbound();
 
263
            }
 
264
 
 
265
            void copy(const prvector_t& other) {
 
266
                _ranges = other._ranges;
 
267
                compact();
 
268
            }
 
269
 
 
270
            void compact() {
 
271
                for (int64_t i = _ranges.size() - 1; i >= 0; --i) {
 
272
                    if (_ranges[i]._range.unbound())
 
273
                        _ranges.erase(_ranges.begin() + i);
 
274
                }
 
275
                assert(is_compact());
 
276
            }
 
277
 
 
278
            bool is_compact() const {
 
279
                for (auto& e : _ranges)
 
280
                    if (e._range.unbound())
 
281
                        return false;
 
282
                return true;
 
283
            }
 
284
 
 
285
            void compress() {
 
286
                int64_t i = _ranges.size();
 
287
                for (--i; i >= 0; --i)
 
288
                    if (_ranges[i]._range.unbound())
 
289
                        _ranges.erase(_ranges.begin() + i);
 
290
            }
 
291
 
 
292
            std::pair<bool, bool> compare(const prvector_t& other) const {
 
293
                assert(is_compact());
 
294
                assert(other.is_compact());
 
295
                auto sit = _ranges.begin();
 
296
                auto oit = other._ranges.begin();
 
297
                std::pair<bool, bool> incl = std::make_pair(true, true);
 
298
 
 
299
                while (true) {
 
300
                    if (sit == _ranges.end()) {
 
301
                        incl.second = incl.second && (oit == other._ranges.end());
 
302
                        break;
 
303
                    } else if (oit == other._ranges.end()) {
 
304
                        incl.first = false;
 
305
                        break;
 
306
                    } else if (sit->_place == oit->_place) {
 
307
                        auto r = sit->compare(*oit);
 
308
                        incl.first = incl.first && r.first;
 
309
                        incl.second &= incl.second && r.second;
 
310
                        ++sit;
 
311
                        ++oit;
 
312
                    } else if (sit->_place < oit->_place) {
 
313
                        incl.first = false;
 
314
                        ++sit;
 
315
                    } else if (sit->_place > oit->_place) {
 
316
                        incl.second = false;
 
317
                        ++oit;
 
318
                    }
 
319
                    if (!incl.first && !incl.second)
 
320
                        return incl;
 
321
                }
 
322
                return incl;
 
323
            }
 
324
 
 
325
            std::ostream& print(std::ostream& os) const {
 
326
 
 
327
                os << "{\n";
 
328
                for (auto& pr : _ranges) {
 
329
                    os << "\t";
 
330
                    pr.print(os) << "\n";
 
331
                }
 
332
                os << "}\n";
 
333
                return os;
 
334
            }
 
335
 
 
336
            bool is_true() const {
 
337
                return _ranges.empty();
 
338
            }
 
339
 
 
340
            bool is_false(size_t nplaces) const {
 
341
                if (_ranges.size() != nplaces) return false;
 
342
                for (auto& p : _ranges) {
 
343
                    if (p._range._lower != 0 ||
 
344
                            p._range._upper != 0)
 
345
                        return false;
 
346
                }
 
347
                return true;
 
348
            }
 
349
 
 
350
            bool operator<(const prvector_t& other) const {
 
351
                if (_ranges.size() != other._ranges.size())
 
352
                    return _ranges.size() < other._ranges.size();
 
353
                for (size_t i = 0; i < _ranges.size(); ++i) {
 
354
                    auto& r = _ranges[i];
 
355
                    auto& otr = other._ranges[i];
 
356
 
 
357
                    if (r._place != otr._place)
 
358
                        return r._place < otr._place;
 
359
                    if (r._range._lower != otr._range._lower)
 
360
                        return r._range._lower < otr._range._lower;
 
361
                    if (r._range._upper != otr._range._upper)
 
362
                        return r._range._upper < otr._range._upper;
 
363
                }
 
364
                return false;
 
365
            }
 
366
 
 
367
            bool operator==(const prvector_t& other) const {
 
368
                auto r = compare(other);
 
369
                return r.first && r.second;
 
370
            }
 
371
 
 
372
            prvector_t& operator&=(const placerange_t& other) {
 
373
                auto lb = std::lower_bound(_ranges.begin(), _ranges.end(), other);
 
374
                if (lb == std::end(_ranges) || lb->_place != other._place) {
 
375
                    _ranges.insert(lb, other);
 
376
                } else {
 
377
                    *lb &= other;
 
378
                }
 
379
                return *this;
 
380
            }
 
381
 
 
382
            prvector_t& operator&=(const prvector_t& other) {
 
383
                auto oit = other._ranges.begin();
 
384
                auto sit = _ranges.begin();
 
385
                while (sit != _ranges.end()) {
 
386
                    while (oit != other._ranges.end() && oit->_place < sit->_place) {
 
387
                        sit = _ranges.insert(sit, *oit);
 
388
                        ++sit;
 
389
                        ++oit;
 
390
                    }
 
391
                    if (oit == other._ranges.end() || oit->_place != sit->_place) {
 
392
                        ++sit;
 
393
                    } else {
 
394
                        *sit &= *oit;
 
395
                        ++sit;
 
396
                    }
 
397
                }
 
398
                if (oit != other._ranges.end()) {
 
399
                    _ranges.insert(_ranges.end(), oit, other._ranges.end());
 
400
                }
 
401
                return *this;
 
402
            }
 
403
 
 
404
            bool restricts(const std::vector<int64_t>& writes) const {
 
405
                auto rit = _ranges.begin();
 
406
                for (auto p : writes) {
 
407
                    while (rit != std::end(_ranges) &&
 
408
                            (rit->_place < p || rit->_range.unbound()))
 
409
                        ++rit;
 
410
                    if (rit == std::end(_ranges)) break;
 
411
                    if (rit->_place == p)
 
412
                        return true;
 
413
                }
 
414
                return false;
 
415
            }
 
416
        };
 
417
    }
 
418
}
 
419
 
 
420
 
 
421
#endif /* RANGE_H */
 
422