← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/Colored/Multiset.cpp

  • 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:
src/PetriEngine/Colored/Multiset.cpp
 
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:   Multiset.cpp
 
9
 * Author: andreas
 
10
 * 
 
11
 * Created on February 20, 2018, 10:37 AM
 
12
 */
 
13
 
 
14
#include <ios>
 
15
#include <algorithm>
 
16
#include <iostream>
 
17
#include <sstream>
 
18
 
 
19
#include "PetriEngine/Colored/Multiset.h"
 
20
 
 
21
namespace PetriEngine {
 
22
    namespace Colored {
 
23
        Multiset::Multiset() : _set(), type(nullptr) {
 
24
        }
 
25
 
 
26
        Multiset::Multiset(const Multiset& orig) {
 
27
            _set = orig._set;
 
28
            type = orig.type;
 
29
        }
 
30
 
 
31
        Multiset::Multiset(std::vector<std::pair<const Color*,uint32_t>>& colors)
 
32
                : _set(), type(nullptr)
 
33
        {
 
34
            for (auto& c : colors) {
 
35
                (*this)[c.first] += c.second;
 
36
            }
 
37
        }
 
38
 
 
39
        Multiset::~Multiset() = default;
 
40
 
 
41
        Multiset Multiset::operator +(const Multiset& other) const {
 
42
            Multiset ms(*this);
 
43
            ms += other;
 
44
            return ms;
 
45
        }
 
46
 
 
47
        Multiset Multiset::operator -(const Multiset& other) const {
 
48
            Multiset ms(*this);
 
49
            ms -= other;
 
50
            return ms;
 
51
        }
 
52
 
 
53
        Multiset Multiset::operator *(uint32_t scalar) const {
 
54
            Multiset ms(*this);
 
55
            ms *= scalar;
 
56
            return ms;
 
57
        }
 
58
 
 
59
        void Multiset::operator +=(const Multiset& other) {
 
60
            if (type == nullptr) {
 
61
                type = other.type;
 
62
            }
 
63
            if (other.type != nullptr && type->getId() != other.type->getId()) {
 
64
                throw "You cannot add Multisets over different sets";
 
65
            }
 
66
            for (auto c : other._set) {
 
67
                const Color* color = DotConstant::dotConstant();
 
68
                if (type != nullptr)
 
69
                    color = &((*type)[c.first]);
 
70
                (*this)[color] += c.second;
 
71
            }
 
72
        }
 
73
 
 
74
        void Multiset::operator -=(const Multiset& other) {
 
75
            if (type == nullptr) {
 
76
                type = other.type;
 
77
            }
 
78
            if (other.type != nullptr && type->getId() != other.type->getId()) {
 
79
                throw "You cannot add Multisets over different sets";
 
80
            }
 
81
            for (auto c : _set) {
 
82
                const Color* color = DotConstant::dotConstant();
 
83
                if (type != nullptr)
 
84
                    color = &((*type)[c.first]);
 
85
                (*this)[color] = std::min(c.second - other[color], c.second);
 
86
            }
 
87
        }
 
88
 
 
89
        void Multiset::operator *=(uint32_t scalar) {
 
90
            for (auto c : _set) {
 
91
                c.second *= scalar;
 
92
            }
 
93
        }
 
94
 
 
95
        uint32_t Multiset::operator [](const Color* color) const {
 
96
            if (type != nullptr && type->getId() == color->getColorType()->getId()) {
 
97
                for (auto c : _set) {
 
98
                    if (c.first == color->getId())
 
99
                        return c.second;
 
100
                }
 
101
            }
 
102
 
 
103
            return 0;
 
104
        }
 
105
 
 
106
        uint32_t& Multiset::operator [](const Color* color) {
 
107
            if (type == nullptr) {
 
108
                type = color->getColorType();
 
109
            }
 
110
            if (color->getColorType() != nullptr && type->getId() != color->getColorType()->getId()) {
 
111
                throw "You cannot access a Multiset with a color from a different color type";
 
112
            }
 
113
            for (auto & i : _set) {
 
114
                if (i.first == color->getId())
 
115
                    return i.second;
 
116
            }
 
117
 
 
118
            _set.emplace_back(color->getId(), 0);
 
119
            return _set.back().second;
 
120
        }
 
121
 
 
122
        bool Multiset::empty() const {
 
123
            return _set.empty();
 
124
        }
 
125
 
 
126
        void Multiset::clean() {
 
127
            if (std::find_if(_set.begin(), _set.end(), [&](auto elem) { return elem.second == 0; }) == _set.end())
 
128
                return;
 
129
 
 
130
            _set.erase(std::remove_if(_set.begin(), _set.end(), [&](auto elem) {
 
131
                return elem.second == 0;
 
132
            }));
 
133
        }
 
134
 
 
135
        Multiset::Iterator Multiset::begin() {
 
136
            return Iterator(this, 0);
 
137
        }
 
138
 
 
139
        Multiset::Iterator Multiset::end() {
 
140
            return Iterator(this, _set.size());
 
141
        }
 
142
 
 
143
 
 
144
        /** Multiset iterator implementation */
 
145
        bool Multiset::Iterator::operator==(Multiset::Iterator &other) {
 
146
            return ms == other.ms && index == other.index;
 
147
        }
 
148
 
 
149
        bool Multiset::Iterator::operator!=(Multiset::Iterator &other) {
 
150
            return !(*this == other);
 
151
        }
 
152
 
 
153
        Multiset::Iterator &Multiset::Iterator::operator++() {
 
154
            ++index;
 
155
            return *this;
 
156
        }
 
157
 
 
158
        std::pair<const Color *, uint32_t &> Multiset::Iterator::operator++(int) {
 
159
            std::pair<const Color*, uint32_t&> old = **this;
 
160
            ++index;
 
161
            return old;
 
162
        }
 
163
 
 
164
        std::pair<const Color *, uint32_t &> Multiset::Iterator::operator*() {
 
165
            auto& item = ms->_set[index];
 
166
            auto color = DotConstant::dotConstant();
 
167
            if (ms->type != nullptr)
 
168
                color = &(*ms->type)[item.first];
 
169
            return { color, item.second };
 
170
        }
 
171
 
 
172
        std::string Multiset::toString() const {
 
173
            std::ostringstream oss;
 
174
            for (size_t i = 0; i < _set.size(); ++i) {
 
175
                oss << _set[i].second << "'(" << (*type)[_set[i].first].toString() << ")";
 
176
                if (i < _set.size() - 1) {
 
177
                    oss << " + ";
 
178
                }
 
179
            }
 
180
 
 
181
            return oss.str();
 
182
        }
 
183
 
 
184
        size_t Multiset::size() const {
 
185
            size_t res = 0;
 
186
            for (auto item : _set) {
 
187
                res += item.second;
 
188
            }
 
189
            return res;
 
190
        }
 
191
    }
 
192
}
 
193