← Back to branch summary

~verifypn-maintainers/verifypn/emptyTracePrint

« back to all changes in this revision

Viewing changes to PetriEngine/Colored/ColoredPetriNetBuilder.cpp

  • Committer: Jiri Srba
  • Date: 2018-04-18 10:58:36 UTC
  • mfrom: (197.3.78 cpn_ctlss)
  • Revision ID: srba.jiri@gmail.com-20180418105836-a5rha272u0om4u77
merged in branch lp:~verifypn-cpn/verifypn/cpn_ctlss/

CPN unfolding
CPN linear overapproximation
Export of reduced queries and model
parallel query simplification
TAR for P/T nets
Improved structural reduction rules

Show diffs side-by-side

added added

removed removed

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