← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/Colored/ColoredPetriNetBuilder.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/ColoredPetriNetBuilder.cpp
 
1
/*
 
2
 * File:   ColoredPetriNetBuilder.cpp
 
3
 * Author: Klostergaard
 
4
 * 
 
5
 * Created on 17. februar 2018, 16:25
 
6
 */
 
7
 
 
8
#include "PetriEngine/Colored/ColoredPetriNetBuilder.h"
 
9
#include <chrono>
 
10
 
 
11
namespace PetriEngine {
 
12
    ColoredPetriNetBuilder::ColoredPetriNetBuilder() {
 
13
    }
 
14
 
 
15
    ColoredPetriNetBuilder::ColoredPetriNetBuilder(const ColoredPetriNetBuilder& orig) {
 
16
    }
 
17
 
 
18
    ColoredPetriNetBuilder::~ColoredPetriNetBuilder() {
 
19
    }
 
20
 
 
21
    void ColoredPetriNetBuilder::addPlace(const std::string& name, int tokens, double x, double y) {
 
22
        if (!_isColored) {
 
23
            _ptBuilder.addPlace(name, tokens, x, y);
 
24
        }
 
25
    }
 
26
 
 
27
    void ColoredPetriNetBuilder::addPlace(const std::string& name, Colored::ColorType* type, Colored::Multiset&& tokens, double x, double y) {
 
28
        if(_placenames.count(name) == 0)
 
29
        {
 
30
            uint32_t next = _placenames.size();
 
31
            _places.emplace_back(Colored::Place {name, type, tokens});
 
32
            _placenames[name] = next;
 
33
        }
 
34
    }
 
35
 
 
36
    void ColoredPetriNetBuilder::addTransition(const std::string& name, double x, double y) {
 
37
        if (!_isColored) {
 
38
            _ptBuilder.addTransition(name, x, y);
 
39
        }
 
40
    }
 
41
 
 
42
    void ColoredPetriNetBuilder::addTransition(const std::string& name, const Colored::GuardExpression_ptr& guard, double x, double y) {
 
43
        if(_transitionnames.count(name) == 0)
 
44
        {
 
45
            uint32_t next = _transitionnames.size();
 
46
            _transitions.emplace_back(Colored::Transition {name, guard});
 
47
            _transitionnames[name] = next;
 
48
        }
 
49
    }
 
50
 
 
51
    void ColoredPetriNetBuilder::addInputArc(const std::string& place, const std::string& transition, bool inhibitor, int weight) {
 
52
        if (!_isColored) {
 
53
            _ptBuilder.addInputArc(place, transition, inhibitor, weight);
 
54
        }
 
55
    }
 
56
 
 
57
    void ColoredPetriNetBuilder::addInputArc(const std::string& place, const std::string& transition, const Colored::ArcExpression_ptr& expr) {
 
58
        addArc(place, transition, expr, true);
 
59
    }
 
60
 
 
61
    void ColoredPetriNetBuilder::addOutputArc(const std::string& transition, const std::string& place, int weight) {
 
62
        if (!_isColored) {
 
63
            _ptBuilder.addOutputArc(transition, place, weight);
 
64
        }
 
65
    }
 
66
 
 
67
    void ColoredPetriNetBuilder::addOutputArc(const std::string& transition, const std::string& place, const Colored::ArcExpression_ptr& expr) {
 
68
        addArc(place, transition, expr, false);
 
69
    }
 
70
 
 
71
    void ColoredPetriNetBuilder::addArc(const std::string& place, const std::string& transition, const Colored::ArcExpression_ptr& expr, bool input) {
 
72
        if(_transitionnames.count(transition) == 0)
 
73
        {
 
74
            std::cout << "Transition '" << transition << "' not found. Adding it." << std::endl;
 
75
            addTransition(transition,0.0,0.0);
 
76
        }
 
77
        if(_placenames.count(place) == 0)
 
78
        {
 
79
            std::cout << "Place '" << place << "' not found. Adding it." << std::endl;
 
80
            addPlace(place,0,0,0);
 
81
        }
 
82
        uint32_t p = _placenames[place];
 
83
        uint32_t t = _transitionnames[transition];
 
84
 
 
85
        assert(t < _transitions.size());
 
86
        assert(p < _places.size());
 
87
 
 
88
        Colored::Arc arc;
 
89
        arc.place = p;
 
90
        arc.transition = t;
 
91
        assert(expr != nullptr);
 
92
        arc.expr = std::move(expr);
 
93
        arc.input = input;
 
94
        _transitions[t].arcs.push_back(std::move(arc));
 
95
    }
 
96
 
 
97
    void ColoredPetriNetBuilder::addColorType(const std::string& id, Colored::ColorType* type) {
 
98
        _colors[id] = type;
 
99
    }
 
100
 
 
101
    void ColoredPetriNetBuilder::sort() {
 
102
 
 
103
    }
 
104
 
 
105
    PetriNetBuilder& ColoredPetriNetBuilder::unfold() {
 
106
        if (_stripped) assert(false);
 
107
        if (_isColored && !_unfolded) {
 
108
            auto start = std::chrono::high_resolution_clock::now();
 
109
            for (auto& place : _places) {
 
110
                unfoldPlace(place);
 
111
            }
 
112
 
 
113
            for (auto& transition : _transitions) {
 
114
                unfoldTransition(transition);
 
115
            }
 
116
 
 
117
            _unfolded = true;
 
118
            auto end = std::chrono::high_resolution_clock::now();
 
119
            _time = (std::chrono::duration_cast<std::chrono::microseconds>(end - start).count())*0.000001;
 
120
        }
 
121
 
 
122
        return _ptBuilder;
 
123
    }
 
124
 
 
125
    void ColoredPetriNetBuilder::unfoldPlace(Colored::Place& place) {
 
126
        for (size_t i = 0; i < place.type->size(); ++i) {
 
127
            std::string name = place.name + ";" + std::to_string(i);
 
128
            const Colored::Color* color = &place.type->operator[](i);
 
129
            _ptBuilder.addPlace(name, place.marking[color], 0.0, 0.0);
 
130
            _ptplacenames[place.name][color->getId()] = std::move(name);
 
131
            ++_nptplaces;
 
132
        }
 
133
    }
 
134
 
 
135
    void ColoredPetriNetBuilder::unfoldTransition(Colored::Transition& transition) {
 
136
        BindingGenerator gen(transition, _arcs, _colors);
 
137
        size_t i = 0;
 
138
        for (auto& b : gen) {
 
139
            std::string name = transition.name + ";" + std::to_string(i++);
 
140
            _ptBuilder.addTransition(name, 0.0, 0.0);
 
141
            _pttransitionnames[transition.name].push_back(name);
 
142
            ++_npttransitions;
 
143
            for (auto& arc : transition.arcs) {
 
144
                unfoldArc(arc, b, name);
 
145
            }
 
146
        }
 
147
    }
 
148
 
 
149
    void ColoredPetriNetBuilder::unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& tName) {
 
150
        Colored::ExpressionContext context {binding, _colors};
 
151
        auto ms = arc.expr->eval(context);
 
152
 
 
153
        for (const auto& color : ms) {
 
154
            if (color.second == 0) {
 
155
                continue;
 
156
            }
 
157
            const std::string& pName = _ptplacenames[_places[arc.place].name][color.first->getId()];
 
158
            if (arc.input) {
 
159
                _ptBuilder.addInputArc(pName, tName, false, color.second);
 
160
            } else {
 
161
                _ptBuilder.addOutputArc(tName, pName, color.second);
 
162
            }
 
163
            ++_nptarcs;
 
164
        }
 
165
    }
 
166
 
 
167
    PetriNetBuilder& ColoredPetriNetBuilder::stripColors() {
 
168
        if (_unfolded) assert(false);
 
169
        if (_isColored && !_stripped) {
 
170
            for (auto& place : _places) {
 
171
                _ptBuilder.addPlace(place.name, place.marking.size(), 0.0, 0.0);
 
172
            }
 
173
 
 
174
            for (auto& transition : _transitions) {
 
175
                _ptBuilder.addTransition(transition.name, 0.0, 0.0);
 
176
                for (auto& arc : transition.arcs) {
 
177
                    try {
 
178
                        if (arc.input) {
 
179
                            _ptBuilder.addInputArc(_places[arc.place].name, _transitions[arc.transition].name, false,
 
180
                                                   arc.expr->weight());
 
181
                        } else {
 
182
                            _ptBuilder.addOutputArc(_transitions[arc.transition].name, _places[arc.place].name,
 
183
                                                    arc.expr->weight());
 
184
                        }
 
185
                    } catch (Colored::WeightException& e) {
 
186
                        std::cerr << "Exception on arc: " << arcToString(arc) << std::endl;
 
187
                        std::cerr << "In expression: " << arc.expr->toString() << std::endl;
 
188
                        std::cerr << e.what() << std::endl;
 
189
                        exit(ErrorCode);
 
190
                    }
 
191
                }
 
192
            }
 
193
 
 
194
            _stripped = true;
 
195
            _isColored = false;
 
196
        }
 
197
 
 
198
        return _ptBuilder;
 
199
    }
 
200
 
 
201
    std::string ColoredPetriNetBuilder::arcToString(Colored::Arc& arc) const {
 
202
        return !arc.input ? "(" + _transitions[arc.transition].name + ", " + _places[arc.place].name + ")" :
 
203
               "(" + _places[arc.place].name + ", " + _transitions[arc.transition].name + ")";
 
204
    }
 
205
 
 
206
    BindingGenerator::Iterator::Iterator(BindingGenerator* generator)
 
207
            : _generator(generator)
 
208
    {
 
209
    }
 
210
 
 
211
    bool BindingGenerator::Iterator::operator==(Iterator& other) {
 
212
        return _generator == other._generator;
 
213
    }
 
214
 
 
215
    bool BindingGenerator::Iterator::operator!=(Iterator& other) {
 
216
        return _generator != other._generator;
 
217
    }
 
218
 
 
219
    BindingGenerator::Iterator& BindingGenerator::Iterator::operator++() {
 
220
        _generator->nextBinding();
 
221
        if (_generator->isInitial()) _generator = nullptr;
 
222
        return *this;
 
223
    }
 
224
 
 
225
    const Colored::ExpressionContext::BindingMap BindingGenerator::Iterator::operator++(int) {
 
226
        auto prev = _generator->currentBinding();
 
227
        ++*this;
 
228
        return prev;
 
229
    }
 
230
 
 
231
    Colored::ExpressionContext::BindingMap& BindingGenerator::Iterator::operator*() {
 
232
        return _generator->currentBinding();
 
233
    }
 
234
 
 
235
    BindingGenerator::BindingGenerator(Colored::Transition& transition,
 
236
            const std::vector<Colored::Arc>& arcs,
 
237
            ColoredPetriNetBuilder::ColorTypeMap& colorTypes)
 
238
        : _colorTypes(colorTypes)
 
239
    {
 
240
        _expr = transition.guard;
 
241
        std::set<Colored::Variable*> variables;
 
242
        if (_expr != nullptr) {
 
243
            _expr->getVariables(variables);
 
244
        }
 
245
        for (auto arc : transition.arcs) {
 
246
            assert(arc.expr != nullptr);
 
247
            arc.expr->getVariables(variables);
 
248
        }
 
249
        for (auto var : variables) {
 
250
            _bindings[var->name] = &var->colorType->operator[](0);
 
251
        }
 
252
        
 
253
        if (!eval())
 
254
            nextBinding();
 
255
    }
 
256
 
 
257
    bool BindingGenerator::eval() {
 
258
        if (_expr == nullptr)
 
259
            return true;
 
260
 
 
261
        Colored::ExpressionContext context {_bindings, _colorTypes};
 
262
        return _expr->eval(context);
 
263
    }
 
264
 
 
265
    Colored::ExpressionContext::BindingMap& BindingGenerator::nextBinding() {
 
266
        bool test = false;
 
267
        while (!test) {
 
268
            for (auto& _binding : _bindings) {
 
269
                _binding.second = &_binding.second->operator++();
 
270
                if (_binding.second->getId() != 0) {
 
271
                    break;
 
272
                }
 
273
            }
 
274
 
 
275
            if (isInitial())
 
276
                break;
 
277
 
 
278
            test = eval();
 
279
        }
 
280
        return _bindings;
 
281
    }
 
282
 
 
283
    Colored::ExpressionContext::BindingMap& BindingGenerator::currentBinding() {
 
284
        return _bindings;
 
285
    }
 
286
 
 
287
    bool BindingGenerator::isInitial() const {
 
288
        for (auto& b : _bindings) {
 
289
            if (b.second->getId() != 0) return false;
 
290
        }
 
291
        return true;
 
292
    }
 
293
 
 
294
    BindingGenerator::Iterator BindingGenerator::begin() {
 
295
        return {this};
 
296
    }
 
297
 
 
298
    BindingGenerator::Iterator BindingGenerator::end() {
 
299
        return {nullptr};
 
300
    }
 
301
}
 
302