← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/PetriNetBuilder.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/PetriNetBuilder.cpp
 
1
/* PeTe - Petri Engine exTremE
 
2
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
 
3
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
 
4
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
 
5
 *                     Peter Gjøl Jensen <root@petergjoel.dk>
 
6
 * 
 
7
 * This program is free software: you can redistribute it and/or modify
 
8
 * it under the terms of the GNU General Public License as published by
 
9
 * the Free Software Foundation, either version 3 of the License, or
 
10
 * (at your option) any later version.
 
11
 * 
 
12
 * This program is distributed in the hope that it will be useful,
 
13
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
15
 * GNU General Public License for more details.
 
16
 * 
 
17
 * You should have received a copy of the GNU General Public License
 
18
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
19
 */
 
20
 
 
21
#include <assert.h>
 
22
#include <algorithm>
 
23
 
 
24
#include "PetriEngine/PetriNetBuilder.h"
 
25
#include "PetriEngine/PetriNet.h"
 
26
#include "PetriEngine/PQL/PQLParser.h"
 
27
#include "PetriEngine/PQL/PQL.h"
 
28
#include "PetriEngine/PQL/Contexts.h"
 
29
#include "PetriEngine/Reducer.h"
 
30
#include "PetriEngine/PQL/Expressions.h"
 
31
 
 
32
using namespace std;
 
33
 
 
34
namespace PetriEngine {
 
35
 
 
36
    PetriNetBuilder::PetriNetBuilder() : AbstractPetriNetBuilder(), 
 
37
    reducer(this){
 
38
    }
 
39
    PetriNetBuilder::PetriNetBuilder(const PetriNetBuilder& other)
 
40
    : _placenames(other._placenames), _transitionnames(other._transitionnames),
 
41
       _transitions(other._transitions), _places(other._places), 
 
42
       initialMarking(other.initialMarking), reducer(this)
 
43
    {
 
44
 
 
45
    }
 
46
 
 
47
    void PetriNetBuilder::addPlace(const string &name, int tokens, double, double) {
 
48
        if(_placenames.count(name) == 0)
 
49
        {
 
50
            uint32_t next = _placenames.size();
 
51
            _places.emplace_back();
 
52
            _placenames[name] = next;
 
53
        }
 
54
        
 
55
        uint32_t id = _placenames[name];
 
56
        
 
57
        while(initialMarking.size() <= id) initialMarking.emplace_back();
 
58
        initialMarking[id] = tokens;
 
59
        
 
60
    }
 
61
 
 
62
    void PetriNetBuilder::addTransition(const string &name,
 
63
            double, double) {
 
64
        if(_transitionnames.count(name) == 0)
 
65
        {
 
66
            uint32_t next = _transitionnames.size();
 
67
            _transitions.emplace_back();
 
68
            _transitionnames[name] = next;
 
69
        }
 
70
    }
 
71
 
 
72
    void PetriNetBuilder::addInputArc(const string &place, const string &transition, bool inhibitor, int weight) {
 
73
        if(_transitionnames.count(transition) == 0)
 
74
        {
 
75
            addTransition(transition,0.0,0.0);
 
76
        }
 
77
        if(_placenames.count(place) == 0)
 
78
        {
 
79
            addPlace(place,0,0,0);
 
80
        }
 
81
        uint32_t p = _placenames[place];
 
82
        uint32_t t = _transitionnames[transition];
 
83
 
 
84
        Arc arc;
 
85
        arc.place = p;
 
86
        arc.weight = weight;
 
87
        arc.skip = false;
 
88
        arc.inhib = inhibitor;
 
89
        assert(t < _transitions.size());
 
90
        assert(p < _places.size());
 
91
        _transitions[t].pre.push_back(arc);
 
92
        _transitions[t].inhib |= inhibitor;
 
93
        _places[p].consumers.push_back(t);
 
94
        _places[p].inhib |= inhibitor;
 
95
    }
 
96
 
 
97
    void PetriNetBuilder::addOutputArc(const string &transition, const string &place, int weight) {
 
98
        if(_transitionnames.count(transition) == 0)
 
99
        {
 
100
            addTransition(transition,0,0);
 
101
        }
 
102
        if(_placenames.count(place) == 0)
 
103
        {
 
104
            addPlace(place,0,0,0);
 
105
        }
 
106
        uint32_t p = _placenames[place];
 
107
        uint32_t t = _transitionnames[transition];
 
108
 
 
109
        assert(t < _transitions.size());
 
110
        assert(p < _places.size());
 
111
        
 
112
        Arc arc;
 
113
        arc.place = p;
 
114
        arc.weight = weight;
 
115
        arc.skip = false;
 
116
        _transitions[t].post.push_back(arc);
 
117
        _places[p].producers.push_back(t);
 
118
    }
 
119
 
 
120
    uint32_t PetriNetBuilder::nextPlaceId(std::vector<uint32_t>& counts, std::vector<uint32_t>& pcounts, std::vector<uint32_t>& ids, bool reorder)
 
121
    {
 
122
        uint32_t cand = std::numeric_limits<uint32_t>::max();
 
123
        uint32_t cnt =  std::numeric_limits<uint32_t>::max();
 
124
        for(uint32_t i = 0; i < _places.size(); ++i)
 
125
        {
 
126
            uint32_t nnum = (pcounts[i] == 0 ? 0 : (counts[0] == 0 ? 0 : std::max(counts[i], pcounts[i])));
 
127
            if( ids[i] == std::numeric_limits<uint32_t>::max() &&
 
128
                nnum < cnt &&
 
129
                !_places[i].skip)
 
130
            {
 
131
                if(!reorder) return i;
 
132
                cand = i;
 
133
                cnt = nnum;
 
134
            }
 
135
        }        
 
136
        return cand;
 
137
    }
 
138
    
 
139
    PetriNet* PetriNetBuilder::makePetriNet(bool reorder) {
 
140
        
 
141
        /*
 
142
         * The basic idea is to construct three arrays, the first array, 
 
143
         * _invariants points to "arcs" - they are triplets (weight, place, inhibitor)
 
144
         * _transitions are pairs, (input, output) are indexes in the _invariants array
 
145
         * _placeToPtrs is an indirection going from a place-index to the FIRST transition
 
146
         *              with a non-inhibitor arc consuming from the given place.
 
147
         * 
 
148
         * For all the indexes and indirections, notice that we only track the 
 
149
         * beginning. We can naturally use the "next" value as the end. eg. the 
 
150
         * inputs of a transition are between "input" and "output". The outputs 
 
151
         * are between "output" and the "input" of the next transition.
 
152
         * 
 
153
         * This allows us to quickly skip a lot of checks when generating successors
 
154
         * Beware that currently "orphans" and "inhibitor orphans" are special-cases
 
155
         * and currently handled as "consuming" from place id=0.
 
156
         * 
 
157
         * If anybody wants to spend time on it, this is the first step towards
 
158
         * a decision-tree like construction, possibly improving successor generation. 
 
159
         */
 
160
        
 
161
        uint32_t nplaces = _places.size() - reducer.RemovedPlaces();
 
162
        uint32_t ntrans = _transitions.size() - reducer.RemovedTransitions();
 
163
        
 
164
        std::vector<uint32_t> place_cons_count = std::vector<uint32_t>(_places.size());
 
165
        std::vector<uint32_t> place_prod_count = std::vector<uint32_t>(_places.size());
 
166
        std::vector<uint32_t> place_idmap = std::vector<uint32_t>(_places.size());
 
167
        std::vector<uint32_t> trans_idmap = std::vector<uint32_t>(_transitions.size());
 
168
        
 
169
        uint32_t invariants = 0;
 
170
        
 
171
        for(uint32_t i = 0; i < _places.size(); ++i)
 
172
        {
 
173
            place_idmap[i] = std::numeric_limits<uint32_t>::max();
 
174
            if(!_places[i].skip)
 
175
            {
 
176
                place_cons_count[i] = _places[i].consumers.size();
 
177
                place_prod_count[i] = _places[i].producers.size();
 
178
                invariants += _places[i].consumers.size() + _places[i].producers.size();
 
179
            }
 
180
        }
 
181
 
 
182
        for(uint32_t i = 0; i < _transitions.size(); ++i)
 
183
        {
 
184
            trans_idmap[i] = std::numeric_limits<uint32_t>::max();
 
185
        }
 
186
        
 
187
        PetriNet* net = new PetriNet(ntrans, invariants, nplaces);
 
188
        
 
189
        uint32_t next = nextPlaceId(place_cons_count, place_prod_count, place_idmap, reorder);
 
190
        uint32_t free = 0;
 
191
        uint32_t freeinv = 0;
 
192
        uint32_t freetrans = 0;
 
193
        
 
194
        // first handle orphans
 
195
        
 
196
        if(place_idmap.size() > next) place_idmap[next] = free;
 
197
        net->_placeToPtrs[free] = freetrans;
 
198
        for(size_t t = 0; t < _transitions.size(); ++t)
 
199
        {
 
200
            Transition& trans = _transitions[t]; 
 
201
            if (std::all_of(trans.pre.begin(), trans.pre.end(), [](Arc& a){return a.inhib;}))
 
202
            {
 
203
                // ALL have to be inhibitor, if any. Otherwise not orphan
 
204
                
 
205
                if(trans.skip) continue;
 
206
                net->_transitions[freetrans].inputs = freeinv;
 
207
                
 
208
                // add inhibitors
 
209
                for(auto pre : trans.pre)
 
210
                {
 
211
                    Invariant& iv = net->_invariants[freeinv];
 
212
                    iv.place = pre.place;
 
213
                    iv.tokens = pre.weight;
 
214
                    iv.inhibitor = pre.inhib;
 
215
                    assert(pre.inhib);
 
216
                    assert(place_cons_count[pre.place] > 0);
 
217
                    --place_cons_count[pre.place];
 
218
                    ++freeinv;
 
219
                }
 
220
                
 
221
                net->_transitions[freetrans].outputs = freeinv;
 
222
                
 
223
                for(auto post : trans.post)
 
224
                {
 
225
                    assert(freeinv < net->_ninvariants);
 
226
                    net->_invariants[freeinv].place = post.place;
 
227
                    net->_invariants[freeinv].tokens = post.weight;                    
 
228
                    ++freeinv;
 
229
                }
 
230
                
 
231
                trans_idmap[t] = freetrans;
 
232
                
 
233
                ++freetrans;
 
234
            }
 
235
        }
 
236
        
 
237
        
 
238
        bool first = true;
 
239
        while(next != std::numeric_limits<uint32_t>::max())
 
240
        {
 
241
            if(first) // already set for first iteration to handle orphans
 
242
            {
 
243
                first = false;
 
244
            }
 
245
            else
 
246
            {
 
247
                place_idmap[next] = free;
 
248
                net->_placeToPtrs[free] = freetrans;
 
249
            }
 
250
            
 
251
            for(auto t : _places[next].consumers)
 
252
            {
 
253
                Transition& trans = _transitions[t]; 
 
254
                if(trans.skip) continue;
 
255
 
 
256
                net->_transitions[freetrans].inputs = freeinv;
 
257
 
 
258
                // check first, we are going to change state later, but we can 
 
259
                // break here, so no statechange inside loop!
 
260
                bool ok = true;
 
261
                bool all_inhib = true;
 
262
                uint32_t cnt = 0;
 
263
                for(const Arc& pre : trans.pre)
 
264
                {
 
265
                    all_inhib &= pre.inhib;
 
266
                    
 
267
                    // if transition belongs to previous place
 
268
                    if(     (!pre.inhib && place_idmap[pre.place] < free) || 
 
269
                            freeinv + cnt >= net->_ninvariants)
 
270
                    {
 
271
                        ok = false;
 
272
                        break;
 
273
                    }  
 
274
                    
 
275
                    // or arc from place is an inhibitor
 
276
                    if(pre.place == next &&  pre.inhib)
 
277
                    {
 
278
                        ok = false;
 
279
                        break;
 
280
                    }
 
281
                    ++cnt;
 
282
                }
 
283
 
 
284
                // skip for now, either T-a->P is inhibitor, or was allready added for other P'
 
285
                // or all a's are inhibitors. 
 
286
                if(!ok || all_inhib) continue; 
 
287
                
 
288
                trans_idmap[t] = freeinv;
 
289
                
 
290
                // everything is good, change state!.
 
291
                for(auto pre : trans.pre)
 
292
                {
 
293
                    Invariant& iv = net->_invariants[freeinv];
 
294
                    iv.place = pre.place;
 
295
                    iv.tokens = pre.weight;
 
296
                    iv.inhibitor = pre.inhib;
 
297
                    ++freeinv;
 
298
                    assert(place_cons_count[pre.place] > 0);
 
299
                    --place_cons_count[pre.place];
 
300
                }
 
301
                
 
302
                net->_transitions[freetrans].outputs = freeinv;
 
303
                for(auto post : trans.post)
 
304
                {
 
305
                    assert(freeinv < net->_ninvariants);
 
306
                    auto& post_inv = net->_invariants[freeinv];
 
307
                    post_inv.place = post.place;
 
308
                    post_inv.tokens = post.weight;    
 
309
                    --place_prod_count[post.place];
 
310
                    ++freeinv;
 
311
                }
 
312
                
 
313
                trans_idmap[t] = freetrans;
 
314
                
 
315
                ++freetrans;
 
316
                assert(freeinv <= invariants);
 
317
            }
 
318
            ++free;
 
319
            next = nextPlaceId(place_cons_count, place_prod_count, place_idmap, reorder);
 
320
        }
 
321
        
 
322
        // Reindex for great justice!
 
323
        for(uint32_t i = 0; i < freeinv; i++)
 
324
        {
 
325
            net->_invariants[i].place = place_idmap[net->_invariants[i].place];
 
326
            assert(net->_invariants[i].place < nplaces);
 
327
            assert(net->_invariants[i].tokens > 0);
 
328
        }
 
329
        
 
330
//        std::cout << "init" << std::endl;
 
331
        for(uint32_t i = 0; i < _places.size(); ++i)
 
332
        {
 
333
            if(place_idmap[i] != std::numeric_limits<uint32_t>::max())
 
334
            {
 
335
                net->_initialMarking[place_idmap[i]] = initialMarking[i];
 
336
//                std::cout << place_idmap[i] << " : " << initialMarking[i] << std::endl;
 
337
            }
 
338
        }
 
339
        
 
340
        // reindex place-names
 
341
 
 
342
        net->_placenames.resize(_placenames.size());
 
343
        int rindex = _placenames.size() - 1;
 
344
        for(auto& i : _placenames)
 
345
        {
 
346
            i.second = place_idmap[i.second];
 
347
            if(i.second != std::numeric_limits<uint32_t>::max())
 
348
            {
 
349
                net->_placenames[i.second] = i.first;
 
350
                assert(_placenames[net->_placenames[i.second]] == i.second);
 
351
            }
 
352
            else
 
353
            {
 
354
                net->_placenames[rindex] = i.first;
 
355
                --rindex;
 
356
            }
 
357
        }
 
358
 
 
359
        net->_transitionnames.resize(_transitionnames.size());
 
360
        int trindex = _transitionnames.size() - 1;
 
361
        for(auto& i : _transitionnames)
 
362
        {
 
363
            i.second = trans_idmap[i.second];
 
364
            if(i.second != std::numeric_limits<uint32_t>::max())
 
365
            {
 
366
                net->_transitionnames[i.second] = i.first;
 
367
            }
 
368
            else
 
369
            {
 
370
                net->_transitionnames[trindex] = i.first;
 
371
                --trindex;
 
372
            }
 
373
        }
 
374
        net->sort();
 
375
        
 
376
        for(size_t t = 0; t < net->numberOfTransitions(); ++t)
 
377
        {
 
378
            {
 
379
                auto tiv = std::make_pair(&net->_invariants[net->_transitions[t].inputs], &net->_invariants[net->_transitions[t].outputs]);
 
380
                for(; tiv.first != tiv.second; ++tiv.first)
 
381
                {
 
382
                    tiv.first->direction = tiv.first->inhibitor ? 0 : -1;
 
383
                    bool found = false;
 
384
                    auto tov = std::make_pair(&net->_invariants[net->_transitions[t].outputs], &net->_invariants[net->_transitions[t + 1].inputs]);                    
 
385
                    for(; tov.first != tov.second; ++tov.first)
 
386
                    {
 
387
                        if(tov.first->place == tiv.first->place)
 
388
                        {
 
389
                            found = true;
 
390
                            if(tiv.first->inhibitor)                        tiv.first->direction = tov.first->direction = 1;
 
391
                            else if(tiv.first->tokens < tov.first->tokens)  tiv.first->direction = tov.first->direction = 1;
 
392
                            else if(tiv.first->tokens == tov.first->tokens) tiv.first->direction = tov.first->direction = 0;
 
393
                            else if(tiv.first->tokens > tov.first->tokens)  tiv.first->direction = tov.first->direction = -1;
 
394
                            break;
 
395
                        }
 
396
                    }
 
397
                    if(!found) assert(tiv.first->direction < 0 || tiv.first->inhibitor);
 
398
                }
 
399
            }
 
400
            {
 
401
                auto tiv = std::make_pair(&net->_invariants[net->_transitions[t].outputs], &net->_invariants[net->_transitions[t + 1].inputs]);
 
402
                for(; tiv.first != tiv.second; ++tiv.first)
 
403
                {
 
404
                    tiv.first->direction = 1;
 
405
                    bool found = false;
 
406
                    auto tov = std::make_pair(&net->_invariants[net->_transitions[t].inputs], &net->_invariants[net->_transitions[t].outputs]);
 
407
                    for(; tov.first != tov.second; ++tov.first)
 
408
                    {
 
409
                        found = true;
 
410
                        if(tov.first->place == tiv.first->place)
 
411
                        {
 
412
                            if     (tov.first->inhibitor)                   tiv.first->direction = tov.first->direction = 1;
 
413
                            else if(tiv.first->tokens > tov.first->tokens)  tiv.first->direction = tov.first->direction = 1;
 
414
                            else if(tiv.first->tokens == tov.first->tokens) tiv.first->direction = tov.first->direction = 0;
 
415
                            else if(tiv.first->tokens < tov.first->tokens)  tiv.first->direction = tov.first->direction = -1;
 
416
                            break;
 
417
                        }
 
418
                    }
 
419
                    if(!found) assert(tiv.first->direction > 0);
 
420
                }
 
421
            }
 
422
        }
 
423
        
 
424
        return net;
 
425
    }
 
426
    
 
427
    void PetriNetBuilder::sort()
 
428
    {
 
429
        for(Place& p : _places)
 
430
        {
 
431
            std::sort(p.consumers.begin(), p.consumers.end());
 
432
            std::sort(p.producers.begin(), p.producers.end());
 
433
        }
 
434
        
 
435
        for(Transition& t : _transitions)
 
436
        {
 
437
            std::sort(t.pre.begin(), t.pre.end());
 
438
            std::sort(t.post.begin(), t.post.end());
 
439
        }
 
440
    }
 
441
    
 
442
    void PetriNetBuilder::reduce(   std::vector<std::shared_ptr<PQL::Condition> >& queries,
 
443
                                    std::vector<Reachability::ResultPrinter::Result>& results, 
 
444
                                    int reductiontype, bool reconstructTrace, const PetriNet* net, int timeout, std::vector<uint32_t>& reductions)
 
445
    {
 
446
        QueryPlaceAnalysisContext placecontext(getPlaceNames(), getTransitionNames(), net);
 
447
        bool all_reach = true;
 
448
        bool remove_loops = true;
 
449
        bool contains_next = false;
 
450
        for(uint32_t i = 0; i < queries.size(); ++i)
 
451
        {
 
452
            if(results[i] == Reachability::ResultPrinter::Unknown ||
 
453
               results[i] == Reachability::ResultPrinter::CTL )
 
454
            {
 
455
                queries[i]->analyze(placecontext);
 
456
                all_reach &= (results[i] != Reachability::ResultPrinter::CTL);
 
457
                remove_loops &= !queries[i]->isLoopSensitive();
 
458
                // There is a deadlock somewhere, if it is not alone, we cannot reduce.
 
459
                // this has similar problems as nested next.                        
 
460
                contains_next |= queries[i]->containsNext() || queries[i]->nestedDeadlock();                        
 
461
            }
 
462
        }
 
463
        reducer.Reduce(placecontext, reductiontype, reconstructTrace, timeout, remove_loops, all_reach, contains_next, reductions);
 
464
    }
 
465
 
 
466
 
 
467
} // PetriEngine