← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/Reducer.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/Reducer.cpp
 
1
/* 
 
2
 * File:   Reducer.cpp
 
3
 * Author: srba
 
4
 *
 
5
 * Created on 15 February 2014, 10:50
 
6
 */
 
7
 
 
8
#include "PetriEngine/Reducer.h"
 
9
#include "PetriEngine/PetriNet.h"
 
10
#include "PetriEngine/PetriNetBuilder.h"
 
11
#include "PetriParse/PNMLParser.h"
 
12
#include <queue>
 
13
#include <set>
 
14
#include <algorithm>
 
15
 
 
16
namespace PetriEngine {
 
17
 
 
18
    Reducer::Reducer(PetriNetBuilder* p) 
 
19
    : parent(p) {
 
20
    }
 
21
 
 
22
    Reducer::~Reducer() {
 
23
 
 
24
    }
 
25
 
 
26
    void Reducer::Print(QueryPlaceAnalysisContext& context) {
 
27
        std::cout   << "\nNET INFO:\n" 
 
28
                    << "Number of places: " << parent->numberOfPlaces() << std::endl
 
29
                    << "Number of transitions: " << parent->numberOfTransitions() 
 
30
                    << std::endl << std::endl;
 
31
        for (uint32_t t = 0; t < parent->numberOfTransitions(); t++) {
 
32
            std::cout << "Transition " << t << " :\n";
 
33
            if(parent->_transitions[t].skip)
 
34
            {
 
35
                std::cout << "\tSKIPPED" << std::endl;
 
36
            }
 
37
            for(auto& arc : parent->_transitions[t].pre)
 
38
            {
 
39
                if (arc.weight > 0) 
 
40
                    std::cout   << "\tInput place " << arc.place  
 
41
                                << " (" << getPlaceName(arc.place) << ")"
 
42
                                << " with arc-weight " << arc.weight << std::endl;
 
43
            }
 
44
            for(auto& arc : parent->_transitions[t].post)
 
45
            {
 
46
                if (arc.weight > 0) 
 
47
                    std::cout   << "\tOutput place " << arc.place 
 
48
                                << " (" << getPlaceName(arc.place) << ")" 
 
49
                                << " with arc-weight " << arc.weight << std::endl;
 
50
            }
 
51
            std::cout << std::endl;
 
52
        }
 
53
        for (uint32_t i = 0; i < parent->numberOfPlaces(); i++) {
 
54
            std::cout <<    "Marking at place "<< i << 
 
55
                            " is: " << parent->initMarking()[i] << std::endl;
 
56
        }
 
57
        for (uint32_t i = 0; i < parent->numberOfPlaces(); i++) {
 
58
            std::cout   << "Query count for place " << i 
 
59
                        << " is: " << context.getQueryPlaceCount()[i] << std::endl;
 
60
        }
 
61
    }
 
62
    
 
63
    std::string Reducer::getTransitionName(uint32_t transition)
 
64
    {
 
65
        for(auto t : parent->_transitionnames)
 
66
        {
 
67
            if(t.second == transition) return t.first;
 
68
        }
 
69
        assert(false);
 
70
        return "";
 
71
    }
 
72
    
 
73
    std::string Reducer::newTransName()
 
74
    {
 
75
        auto prefix = "CT";
 
76
        auto tmp = prefix + std::to_string(_tnameid);
 
77
        while(parent->_transitionnames.count(tmp) >= 1)
 
78
        {
 
79
            ++_tnameid;
 
80
            tmp = prefix + std::to_string(_tnameid);
 
81
        }
 
82
        ++_tnameid;
 
83
        return tmp;
 
84
    }
 
85
    
 
86
    std::string Reducer::getPlaceName(uint32_t place)
 
87
    {
 
88
        for(auto t : parent->_placenames)
 
89
        {
 
90
            if(t.second == place) return t.first;
 
91
        }
 
92
        assert(false);
 
93
        return "";
 
94
    }
 
95
    
 
96
    Transition& Reducer::getTransition(uint32_t transition)
 
97
    {
 
98
        return parent->_transitions[transition];
 
99
    }
 
100
    
 
101
    ArcIter Reducer::getOutArc(Transition& trans, uint32_t place)
 
102
    {
 
103
        Arc a;
 
104
        a.place = place;
 
105
        auto ait = std::lower_bound(trans.post.begin(), trans.post.end(), a);
 
106
        if(ait != trans.post.end() && ait->place == place)
 
107
        {
 
108
            return ait;
 
109
        }
 
110
        else 
 
111
        {
 
112
            return trans.post.end();
 
113
        }
 
114
    }
 
115
    
 
116
    ArcIter Reducer::getInArc(uint32_t place, Transition& trans)
 
117
    {
 
118
        Arc a;
 
119
        a.place = place;
 
120
        auto ait = std::lower_bound(trans.pre.begin(), trans.pre.end(), a);
 
121
        if(ait != trans.pre.end() && ait->place == place)
 
122
        {
 
123
            return ait;
 
124
        }
 
125
        else 
 
126
        {
 
127
            return trans.pre.end();
 
128
        }
 
129
    }
 
130
    
 
131
    void Reducer::eraseTransition(std::vector<uint32_t>& set, uint32_t el)
 
132
    {
 
133
        auto lb = std::lower_bound(set.begin(), set.end(), el);
 
134
        assert(lb != set.end());
 
135
        assert(*lb == el);
 
136
        set.erase(lb);
 
137
    }
 
138
    
 
139
    void Reducer::skipTransition(uint32_t t)
 
140
    {
 
141
        ++_removedTransitions;
 
142
        Transition& trans = getTransition(t);
 
143
        assert(!trans.skip);
 
144
        for(auto p : trans.post)
 
145
        {
 
146
            eraseTransition(parent->_places[p.place].producers, t);
 
147
        }
 
148
        for(auto p : trans.pre)
 
149
        {
 
150
            eraseTransition(parent->_places[p.place].consumers, t);
 
151
        }
 
152
        trans.post.clear();
 
153
        trans.pre.clear();
 
154
        trans.skip = true;
 
155
        assert(consistent());
 
156
        _skipped_trans.push_back(t);
 
157
    }
 
158
    
 
159
    void Reducer::skipPlace(uint32_t place)
 
160
    {
 
161
        ++_removedPlaces;
 
162
        Place& pl = parent->_places[place];
 
163
        assert(!pl.skip);
 
164
        pl.skip = true;
 
165
        for(auto& t : pl.consumers)
 
166
        {
 
167
            Transition& trans = getTransition(t);
 
168
            auto ait = getInArc(place, trans);
 
169
            if(ait != trans.pre.end() && ait->place == place)
 
170
                trans.pre.erase(ait);
 
171
        }
 
172
 
 
173
        for(auto& t : pl.producers)
 
174
        {
 
175
            Transition& trans = getTransition(t);
 
176
            auto ait = getOutArc(trans, place);
 
177
            if(ait != trans.post.end() && ait->place == place)
 
178
                trans.post.erase(ait);
 
179
        }
 
180
        pl.consumers.clear();
 
181
        pl.producers.clear();
 
182
        assert(consistent());
 
183
    }
 
184
    
 
185
    
 
186
    bool Reducer::consistent()
 
187
    {
 
188
#ifndef NDEBUG
 
189
        size_t strans = 0;
 
190
        for(size_t i = 0; i < parent->numberOfTransitions(); ++i)
 
191
        {
 
192
            Transition& t = parent->_transitions[i];
 
193
            if(t.skip) ++strans;
 
194
            assert(std::is_sorted(t.pre.begin(), t.pre.end()));
 
195
            assert(std::is_sorted(t.post.end(), t.post.end()));
 
196
            assert(!t.skip || (t.pre.size() == 0 && t.post.size() == 0));
 
197
            for(Arc& a : t.pre)
 
198
            {
 
199
                assert(a.weight > 0);
 
200
                Place& p = parent->_places[a.place];
 
201
                assert(!p.skip);
 
202
                assert(std::find(p.consumers.begin(), p.consumers.end(), i) != p.consumers.end());
 
203
            }
 
204
            for(Arc& a : t.post)
 
205
            {
 
206
                assert(a.weight > 0);
 
207
                Place& p = parent->_places[a.place];
 
208
                assert(!p.skip);
 
209
                assert(std::find(p.producers.begin(), p.producers.end(), i) != p.producers.end());
 
210
            }
 
211
        }
 
212
        
 
213
        assert(strans == _removedTransitions);
 
214
 
 
215
        size_t splaces = 0;
 
216
        for(size_t i = 0; i < parent->numberOfPlaces(); ++i)
 
217
        {
 
218
            Place& p = parent->_places[i];
 
219
            if(p.skip) ++splaces;
 
220
            assert(std::is_sorted(p.consumers.begin(), p.consumers.end()));
 
221
            assert(std::is_sorted(p.producers.begin(), p.producers.end()));
 
222
            assert(!p.skip || (p.consumers.size() == 0 && p.producers.size() == 0));
 
223
            
 
224
            for(uint c : p.consumers)
 
225
            {
 
226
                Transition& t = parent->_transitions[c];
 
227
                assert(!t.skip);
 
228
                auto a = getInArc(i, t);
 
229
                assert(a != t.pre.end());
 
230
                assert(a->place == i);
 
231
            }
 
232
            
 
233
            for(uint prod : p.producers)
 
234
            {
 
235
                Transition& t = parent->_transitions[prod];
 
236
                assert(!t.skip);
 
237
                auto a = getOutArc(t, i);
 
238
                assert(a != t.post.end());
 
239
                assert(a->place == i);
 
240
            }
 
241
        }
 
242
        assert(splaces == _removedPlaces);
 
243
#endif
 
244
        return true;
 
245
    }
 
246
 
 
247
    bool Reducer::ReducebyRuleA(uint32_t* placeInQuery) {
 
248
        // Rule A  - find transition t that has exactly one place in pre and post and remove one of the places (and t)  
 
249
        bool continueReductions = false;
 
250
        const size_t numberoftransitions = parent->numberOfTransitions();
 
251
        for (uint32_t t = 0; t < numberoftransitions; t++) {
 
252
            if(hasTimedout()) return false;
 
253
            Transition& trans = getTransition(t);
 
254
                        
 
255
            // we have already removed
 
256
            if(trans.skip) continue;
 
257
 
 
258
            // A2. we have more/less than one arc in pre or post
 
259
            // checked first to avoid out-of-bounds when looking up indexes.
 
260
            if(trans.pre.size() != 1) continue;
 
261
 
 
262
            uint32_t pPre = trans.pre[0].place;
 
263
                        
 
264
            // A2. Check that pPre goes only to t
 
265
            if(parent->_places[pPre].consumers.size() != 1) continue;
 
266
            
 
267
            // A3. We have weight of more than one on input
 
268
            // and is empty on output (should not happen).
 
269
            auto w = trans.pre[0].weight;
 
270
            bool ok = true;
 
271
            for(auto t : parent->_places[pPre].producers)
 
272
            {
 
273
                if((getOutArc(parent->_transitions[t], trans.pre[0].place)->weight % w) != 0)
 
274
                {
 
275
                    ok = false;
 
276
                    break;
 
277
                }
 
278
            }
 
279
            if(!ok)
 
280
                continue;
 
281
                        
 
282
            // A4. Do inhibitor check, neither T, pPre or pPost can be involved with any inhibitor
 
283
            if(parent->_places[pPre].inhib|| trans.inhib) continue;
 
284
            
 
285
            // A5. dont mess with query!
 
286
            if(placeInQuery[pPre] > 0) continue;
 
287
            // check A1, A4 and A5 for post
 
288
            for(auto& pPost : trans.post)
 
289
            {
 
290
                if(parent->_places[pPost.place].inhib || pPre == pPost.place || placeInQuery[pPost.place] > 0)
 
291
                {
 
292
                    ok = false;
 
293
                    break;
 
294
                }
 
295
            }
 
296
            if(!ok) continue;
 
297
            
 
298
            continueReductions = true;
 
299
            _ruleA++;
 
300
            
 
301
            // here we need to remember when a token is created in pPre (some 
 
302
            // transition with an output in P is fired), t is fired instantly!.
 
303
            if(reconstructTrace) {
 
304
                Place& pre = parent->_places[pPre];
 
305
                std::string tname = getTransitionName(t);
 
306
                for(size_t pp : pre.producers)
 
307
                {
 
308
                    std::string prefire = getTransitionName(pp);
 
309
                    _postfire[prefire].push_back(tname);
 
310
                }
 
311
                _extraconsume[tname].emplace_back(getPlaceName(pPre), w);
 
312
                for(size_t i = 0; i < parent->initMarking()[pPre]; ++i)
 
313
                {
 
314
                    _initfire.push_back(tname);
 
315
                }                
 
316
            }
 
317
            
 
318
            for(auto& pPost : trans.post)
 
319
            {
 
320
                // UA2. move the token for the initial marking, makes things simpler.
 
321
                parent->initialMarking[pPost.place] += ((parent->initialMarking[pPre]/w) * pPost.weight);
 
322
            }
 
323
            parent->initialMarking[pPre] = 0;
 
324
 
 
325
            // Remove transition t and the place that has no tokens in m0
 
326
            // UA1. remove transition
 
327
            auto toMove = trans.post;
 
328
            skipTransition(t);
 
329
 
 
330
            // UA2. update arcs
 
331
            for(auto& _t : parent->_places[pPre].producers)
 
332
            {
 
333
                assert(_t != t);
 
334
                // move output-arcs to post.
 
335
                Transition& src = getTransition(_t);
 
336
                auto source = *getOutArc(src, pPre);
 
337
                for(auto& pPost : toMove)
 
338
                {
 
339
                    Arc a;
 
340
                    a.place = pPost.place;
 
341
                    a.weight = (source.weight/w) * pPost.weight;
 
342
                    assert(a.weight > 0);
 
343
                    a.inhib = false;
 
344
                    auto dest = std::lower_bound(src.post.begin(), src.post.end(), a);
 
345
                    if(dest == src.post.end() || dest->place != pPost.place)
 
346
                    {
 
347
                        dest = src.post.insert(dest, a);
 
348
                        auto& prod = parent->_places[pPost.place].producers;
 
349
                        auto lb = std::lower_bound(prod.begin(), prod.end(), _t);
 
350
                        prod.insert(lb, _t);
 
351
                    }
 
352
                    else
 
353
                    {
 
354
                        dest->weight += ((source.weight/w) * pPost.weight);
 
355
                    }
 
356
                    assert(dest->weight > 0);
 
357
                }
 
358
            }                
 
359
            // UA1. remove place
 
360
            skipPlace(pPre);
 
361
        } // end of Rule A main for-loop
 
362
        return continueReductions;
 
363
    }
 
364
 
 
365
    bool Reducer::ReducebyRuleB(uint32_t* placeInQuery, bool remove_deadlocks, bool remove_consumers) {
 
366
 
 
367
        // Rule B - find place p that has exactly one transition in pre and exactly one in post and remove the place
 
368
        bool continueReductions = false;
 
369
        const size_t numberofplaces = parent->numberOfPlaces();
 
370
        for (uint32_t p = 0; p < numberofplaces; p++) {
 
371
            if(hasTimedout()) return false;            
 
372
            Place& place = parent->_places[p];
 
373
            
 
374
            if(place.skip) continue;    // already removed    
 
375
            // B5. dont mess up query
 
376
            if(placeInQuery[p] > 0)
 
377
                continue;
 
378
                        
 
379
            // B2. Only one consumer/producer
 
380
            if( place.consumers.size() != 1 || 
 
381
                place.producers.size() < 1)
 
382
                continue; // no orphan removal
 
383
            
 
384
            auto tIn = place.consumers[0];
 
385
            
 
386
            // B1. producer is not consumer
 
387
            bool ok = true;
 
388
            for(auto& tOut : place.producers)
 
389
            {
 
390
                if (tOut == tIn) 
 
391
                {
 
392
                    ok = false;
 
393
                    continue; // cannot remove this kind either
 
394
                }
 
395
            }
 
396
            if(!ok)
 
397
                continue;
 
398
            auto prod = place.producers;
 
399
            Transition& in = getTransition(tIn);
 
400
            for(auto tOut : prod)
 
401
            {
 
402
                Transition& out = getTransition(tOut);
 
403
 
 
404
                if(out.post.size() != 1 && in.pre.size() != 1)
 
405
                    continue; // at least one has to be singular for this to work
 
406
 
 
407
                if((!remove_deadlocks || !remove_consumers) && in.pre.size() != 1)
 
408
                    // the buffer can mean deadlocks and other interesting things
 
409
                    // also we can "hide" tokens, so we need to make sure not
 
410
                    // to remove consumers.
 
411
                    continue;
 
412
 
 
413
                if(parent->initMarking()[p] > 0 && in.pre.size() != 1)
 
414
                    continue;
 
415
 
 
416
                auto inArc = getInArc(p, in);
 
417
                auto outArc = getOutArc(out, p);
 
418
 
 
419
                // B3. Output is a multiple of input and nonzero.
 
420
                if(outArc->weight < inArc->weight) 
 
421
                    continue;            
 
422
                if((outArc->weight % inArc->weight) != 0)
 
423
                    continue;            
 
424
 
 
425
                size_t multiplier = outArc->weight / inArc->weight;
 
426
 
 
427
                // B4. Do inhibitor check, neither In, out or place can be involved with any inhibitor
 
428
                if(place.inhib || in.inhib || out.inhib)
 
429
                    continue;
 
430
 
 
431
                // B6. also, none of the places in the post-set of consuming transition can be participating in inhibitors.
 
432
                // B7. nor can they appear in the query.
 
433
                {
 
434
                    bool post_ok = false;
 
435
                    for(const Arc& a : in.post)
 
436
                    {
 
437
                        post_ok |= parent->_places[a.place].inhib;
 
438
                        post_ok |= placeInQuery[a.place];
 
439
                        if(post_ok) break;
 
440
                    }
 
441
                    if(post_ok) 
 
442
                        continue;
 
443
                }
 
444
                {
 
445
                    bool pre_ok = false;
 
446
                    for(const Arc& a : in.pre)
 
447
                    {
 
448
                        pre_ok |= parent->_places[a.place].inhib;
 
449
                        pre_ok |= placeInQuery[a.place];
 
450
                        if(pre_ok) break;
 
451
                    }
 
452
                    if(pre_ok) 
 
453
                        continue;
 
454
                }
 
455
                
 
456
                bool ok = true;  
 
457
                if(in.pre.size() > 1)
 
458
                    for(const Arc& arc : out.pre)
 
459
                        ok &= placeInQuery[arc.place] == 0;
 
460
                if(!ok)
 
461
                    continue;
 
462
 
 
463
                // B2.a Check that there is no other place than p that gives to tPost, 
 
464
                // tPre can give to other places
 
465
                auto& arcs = in.pre.size() < out.post.size() ? in.pre : out.post;
 
466
                for (auto& arc : arcs) {
 
467
                    if (arc.weight > 0 && arc.place != p) {
 
468
                        ok = false;
 
469
                        break;
 
470
                    }
 
471
                }
 
472
 
 
473
                if (!ok)
 
474
                    continue;
 
475
 
 
476
                // UB2. we need to remember initial marking
 
477
                uint initm = parent->initMarking()[p];
 
478
                initm /= inArc->weight; // integer-devision is floor by default
 
479
 
 
480
                if(reconstructTrace)
 
481
                {
 
482
                    // remember reduction for recreation of trace
 
483
                    std::string toutname    = getTransitionName(tOut);
 
484
                    std::string tinname     = getTransitionName(tIn);
 
485
                    std::string pname       = getPlaceName(p);
 
486
                    Arc& a = *getInArc(p, in);
 
487
                    _extraconsume[tinname].emplace_back(pname, a.weight);
 
488
                    for(size_t i = 0; i < multiplier; ++i)
 
489
                    {
 
490
                        _postfire[toutname].push_back(tinname);
 
491
                    }
 
492
 
 
493
                    for(size_t i = 0; initm > 0 && i < initm / inArc->weight; ++i )
 
494
                    {
 
495
                        _initfire.push_back(tinname);
 
496
                    }
 
497
                }
 
498
 
 
499
                continueReductions = true;
 
500
                _ruleB++;
 
501
                 // UB1. Remove place p
 
502
                parent->initialMarking[p] = 0;
 
503
                // We need to remember that when tOut fires, tIn fires just after.
 
504
                // this should fix the trace
 
505
 
 
506
                // UB3. move arcs from t' to t
 
507
                for (auto& arc : in.post) { // remove tPost
 
508
                    auto _arc = getOutArc(out, arc.place);
 
509
                    // UB2. Update initial marking
 
510
                    parent->initialMarking[arc.place] += initm*arc.weight;
 
511
                    if(_arc != out.post.end())
 
512
                    {
 
513
                        _arc->weight += arc.weight*multiplier;
 
514
                    }
 
515
                    else
 
516
                    {
 
517
                        out.post.push_back(arc);
 
518
                        out.post.back().weight *= multiplier;
 
519
                        parent->_places[arc.place].producers.push_back(tOut);
 
520
 
 
521
                        std::sort(out.post.begin(), out.post.end());
 
522
                        std::sort(parent->_places[arc.place].producers.begin(),
 
523
                                  parent->_places[arc.place].producers.end());
 
524
                    }
 
525
                }
 
526
                for (auto& arc : in.pre) { // remove tPost
 
527
                    if(arc.place == p)
 
528
                        continue;
 
529
                    auto _arc = getInArc(arc.place, out);
 
530
                    // UB2. Update initial marking
 
531
                    parent->initialMarking[arc.place] += initm*arc.weight;
 
532
                    if(_arc != out.pre.end())
 
533
                    {
 
534
                        _arc->weight += arc.weight*multiplier;
 
535
                    }
 
536
                    else
 
537
                    {
 
538
                        out.pre.push_back(arc);
 
539
                        out.pre.back().weight *= multiplier;
 
540
                        parent->_places[arc.place].consumers.push_back(tOut);
 
541
 
 
542
                        std::sort(out.pre.begin(), out.pre.end());
 
543
                        std::sort(parent->_places[arc.place].consumers.begin(),
 
544
                                  parent->_places[arc.place].consumers.end());
 
545
                    }
 
546
                }
 
547
 
 
548
                for(auto it = out.post.begin(); it != out.post.end(); ++it)
 
549
                {
 
550
                    if(it->place == p)
 
551
                    {
 
552
                        out.post.erase(it);
 
553
                        break;
 
554
                    }
 
555
                }
 
556
                for(auto it = place.producers.begin(); it != place.producers.end(); ++it)
 
557
                {
 
558
                    if(*it == tOut)
 
559
                    {
 
560
                        place.producers.erase(it);
 
561
                        break;
 
562
                    }
 
563
                }
 
564
            }
 
565
            // UB1. remove transition
 
566
            if(place.producers.size() == 0)
 
567
            {
 
568
                skipPlace(p);
 
569
                skipTransition(tIn);
 
570
            }
 
571
        } // end of Rule B main for-loop
 
572
        assert(consistent());
 
573
        return continueReductions;
 
574
    }
 
575
 
 
576
    bool Reducer::ReducebyRuleC(uint32_t* placeInQuery) {
 
577
        // Rule C - Places with same input and output-transitions which a modulo each other
 
578
        bool continueReductions = false;
 
579
        
 
580
        _pflags.resize(parent->_places.size(), 0);
 
581
        std::fill(_pflags.begin(), _pflags.end(), 0);
 
582
        
 
583
        for(uint32_t touter = 0; touter < parent->numberOfTransitions(); ++touter)
 
584
        for(size_t outer = 0; outer < parent->_transitions[touter].post.size(); ++outer)
 
585
        {                        
 
586
            auto pouter = parent->_transitions[touter].post[outer].place;
 
587
            if(_pflags[pouter] > 0) continue;
 
588
            _pflags[pouter] = 1;
 
589
            if(hasTimedout()) return false;
 
590
            if(parent->_places[pouter].skip) continue;
 
591
            
 
592
            // C4. No inhib
 
593
            if(parent->_places[pouter].inhib) continue;
 
594
            
 
595
            for (size_t inner = outer + 1; inner < parent->_transitions[touter].post.size(); ++inner) 
 
596
            {
 
597
                auto pinner = parent->_transitions[touter].post[inner].place;
 
598
                if(parent->_places[pinner].skip) continue;
 
599
 
 
600
                // C4. No inhib
 
601
                if(parent->_places[pinner].inhib) continue;
 
602
 
 
603
                for(size_t swp = 0; swp < 2; ++swp)
 
604
                {
 
605
                    if(hasTimedout()) return false;
 
606
                    if( parent->_places[pinner].skip ||
 
607
                        parent->_places[pouter].skip) break;
 
608
                    
 
609
                    uint p1 = pouter;
 
610
                    uint p2 = pinner;
 
611
                    
 
612
                    if(swp == 1) std::swap(p1, p2);
 
613
                    
 
614
                    Place& place1 = parent->_places[p1];
 
615
 
 
616
                    // C1. Not same place
 
617
                    if(p1 == p2) break;
 
618
 
 
619
                    // C5. Dont mess with query
 
620
                    if(placeInQuery[p2] > 0)
 
621
                        continue;
 
622
 
 
623
                    Place& place2 = parent->_places[p2];
 
624
 
 
625
                    // C2, C3. Consumer and producer-sets must match
 
626
                    if(place1.consumers.size() < place2.consumers.size() ||
 
627
                       place1.producers.size() > place2.producers.size())
 
628
                        break;
 
629
 
 
630
                    long double mult = 1;
 
631
 
 
632
                    // C8. Consumers must match with weights
 
633
                    int ok = 0;
 
634
                    size_t j = 0;
 
635
                    for(size_t i = 0; i < place2.consumers.size(); ++i)
 
636
                    {
 
637
                        while(j < place1.consumers.size() && place1.consumers[j] < place2.consumers[i] ) ++j;
 
638
                        if(place1.consumers.size() <= j || place1.consumers[j] != place2.consumers[i])
 
639
                        {
 
640
                            ok = 2;
 
641
                            break;
 
642
                        }
 
643
 
 
644
                        Transition& trans = getTransition(place1.consumers[j]);
 
645
                        auto a1 = getInArc(p1, trans);
 
646
                        auto a2 = getInArc(p2, trans);
 
647
                        assert(a1 != trans.pre.end());
 
648
                        assert(a2 != trans.pre.end());
 
649
                        mult = std::max(mult, ((long double)a2->weight) / ((long double)a1->weight));
 
650
                    }
 
651
 
 
652
                    if(ok == 2) break;
 
653
 
 
654
                    // C6. We do not care about excess markings in p2.
 
655
                    if(mult != std::numeric_limits<long double>::max() &&
 
656
                            (((long double)parent->initialMarking[p1]) * mult) > ((long double)parent->initialMarking[p2]))
 
657
                    {
 
658
                        continue;
 
659
                    }
 
660
 
 
661
                    
 
662
                    // C7. Producers must match with weights
 
663
                    j = 0;
 
664
                    for(size_t i = 0; i < place1.producers.size(); ++i)
 
665
                    {
 
666
                        while(j < place2.producers.size() && place2.producers[j] < place1.producers[i]) ++j;
 
667
                        if(j == place2.producers.size() || place1.producers[i] != place2.producers[j])
 
668
                        {
 
669
                            ok = 2;
 
670
                            break;
 
671
                        }
 
672
 
 
673
                        Transition& trans = getTransition(place1.producers[i]);
 
674
                        auto a1 = getOutArc(trans, p1);
 
675
                        auto a2 = getOutArc(trans, p2);
 
676
                        assert(a1 != trans.post.end());
 
677
                        assert(a2 != trans.post.end());
 
678
 
 
679
                        if(((long double)a1->weight)*mult > ((long double)a2->weight))
 
680
                        {
 
681
                            ok = 1;
 
682
                            break;
 
683
                        }
 
684
                    }
 
685
 
 
686
                    if(ok == 2) break;
 
687
                    else if(ok == 1) continue;
 
688
 
 
689
                    parent->initialMarking[p2] = 0;
 
690
 
 
691
                    if(reconstructTrace)
 
692
                    {
 
693
                        for(auto t : place2.consumers)
 
694
                        {
 
695
                            std::string tname = getTransitionName(t);
 
696
                            const ArcIter arc = getInArc(p2, getTransition(t));
 
697
                            _extraconsume[tname].emplace_back(getPlaceName(p2), arc->weight);
 
698
                        }
 
699
                    }
 
700
 
 
701
                    continueReductions = true;
 
702
                    _ruleC++;
 
703
                    // UC1. Remove p2
 
704
                    skipPlace(p2);
 
705
                    _pflags[pouter] = 0;
 
706
                    break;
 
707
                }
 
708
            }
 
709
        }
 
710
        assert(consistent());
 
711
        return continueReductions;
 
712
    }
 
713
 
 
714
    bool Reducer::ReducebyRuleD(uint32_t* placeInQuery) {
 
715
        // Rule D - two transitions with the same pre and post and same inhibitor arcs 
 
716
        // This does not alter the trace.
 
717
        bool continueReductions = false;
 
718
        _tflags.resize(parent->_transitions.size(), 0);
 
719
        std::fill(_tflags.begin(), _tflags.end(), 0);
 
720
        bool has_empty_trans = false;
 
721
        for(size_t t = 0; t < parent->_transitions.size(); ++t)
 
722
        {
 
723
            auto& trans = parent->_transitions[t];
 
724
            if(!trans.skip && trans.pre.size() == 0 && trans.post.size() == 0)
 
725
            {
 
726
                if(has_empty_trans)
 
727
                {
 
728
                    ++_ruleD;
 
729
                    skipTransition(t);
 
730
                }
 
731
                has_empty_trans = true;
 
732
            }
 
733
            
 
734
        }
 
735
        for(auto& op : parent->_places)
 
736
        for(size_t outer = 0; outer < op.consumers.size(); ++outer)
 
737
        {            
 
738
            auto touter = op.consumers[outer];
 
739
            if(hasTimedout()) return false;
 
740
            if(_tflags[touter] != 0) continue;
 
741
            _tflags[touter] = 1;
 
742
            Transition& tout = getTransition(touter);
 
743
            if (tout.skip) continue;
 
744
 
 
745
            // D2. No inhibitors
 
746
            if (tout.inhib) continue;
 
747
 
 
748
            for(size_t inner = outer + 1; inner < op.consumers.size(); ++inner) {
 
749
                auto tinner = op.consumers[inner];
 
750
                Transition& tin = getTransition(tinner);
 
751
                if (tin.skip || tout.skip) continue;
 
752
 
 
753
                // D2. No inhibitors
 
754
                if (tin.inhib) continue;
 
755
 
 
756
                for (size_t swp = 0; swp < 2; ++swp) {
 
757
                    if(hasTimedout()) return false;
 
758
 
 
759
                    if (tin.skip || tout.skip) break;
 
760
                    
 
761
                    uint t1 = touter;
 
762
                    uint t2 = tinner;
 
763
                    if (swp == 1) std::swap(t1, t2);
 
764
 
 
765
                    // D1. not same transition
 
766
                    assert(t1 != t2);
 
767
 
 
768
                    Transition& trans1 = getTransition(t1);
 
769
                    Transition& trans2 = getTransition(t2);
 
770
 
 
771
                    // From D3, and D4 we have that pre and post-sets are the same
 
772
                    if (trans1.post.size() != trans2.post.size()) break;
 
773
                    if (trans1.pre.size() != trans2.pre.size()) break;
 
774
 
 
775
                    int ok = 0;
 
776
                    uint mult = std::numeric_limits<uint>::max();
 
777
                    // D4. postsets must match
 
778
                    for (int i = trans1.post.size() - 1; i >= 0; --i) {
 
779
                        Arc& arc = trans1.post[i];
 
780
                        Arc& arc2 = trans2.post[i];
 
781
                        if (arc2.place != arc.place) {
 
782
                            ok = 2;
 
783
                            break;
 
784
                        }
 
785
 
 
786
                        if (mult == std::numeric_limits<uint>::max()) {
 
787
                            if (arc2.weight < arc.weight || (arc2.weight % arc.weight) != 0) {
 
788
                                ok = 1;
 
789
                                break;
 
790
                            } else {
 
791
                                mult = arc2.weight / arc.weight;
 
792
                            }
 
793
                        } else if (arc2.weight != arc.weight * mult) {
 
794
                            ok = 2;
 
795
                            break;
 
796
                        }
 
797
                    }
 
798
 
 
799
                    if (ok == 2) break;
 
800
                    else if (ok == 1) continue;
 
801
 
 
802
                    // D3. Presets must match
 
803
                    for (int i = trans1.pre.size() - 1; i >= 0; --i) {
 
804
                        Arc& arc = trans1.pre[i];
 
805
                        Arc& arc2 = trans2.pre[i];
 
806
                        if (arc2.place != arc.place) {
 
807
                            ok = 2;
 
808
                            break;
 
809
                        }
 
810
 
 
811
                        if (mult == std::numeric_limits<uint>::max()) {
 
812
                            if (arc2.weight < arc.weight || (arc2.weight % arc.weight) != 0) {
 
813
                                ok = 1;
 
814
                                break;
 
815
                            } else {
 
816
                                mult = arc2.weight / arc.weight;
 
817
                            }
 
818
                        } else if (arc2.weight != arc.weight * mult) {
 
819
                            ok = 2;
 
820
                            break;
 
821
                        }
 
822
                    }
 
823
 
 
824
                    if (ok == 2) break;
 
825
                    else if (ok == 1) continue;
 
826
 
 
827
                    // UD1. Remove transition t2
 
828
                    continueReductions = true;
 
829
                    _ruleD++;
 
830
                    skipTransition(t2);
 
831
                    _tflags[touter] = 0;
 
832
                    break; // break the swap loop
 
833
                }
 
834
            }
 
835
        } // end of main for loop for rule D
 
836
        assert(consistent());
 
837
        return continueReductions;
 
838
    }
 
839
    
 
840
    bool Reducer::ReducebyRuleE(uint32_t* placeInQuery) {
 
841
        bool continueReductions = false;
 
842
        const size_t numberofplaces = parent->numberOfPlaces();
 
843
        for(uint32_t p = 0; p < numberofplaces; ++p)
 
844
        {
 
845
            if(hasTimedout()) return false;
 
846
            Place& place = parent->_places[p];
 
847
            if(place.skip) continue;
 
848
            if(place.inhib) continue;
 
849
            if(place.producers.size() > place.consumers.size()) continue;
 
850
            
 
851
            std::set<uint32_t> notenabled;
 
852
            bool ok = true;
 
853
            for(uint cons : place.consumers)
 
854
            {
 
855
                Transition& t = getTransition(cons);
 
856
                auto in = getInArc(p, t);
 
857
                if(in->weight <= parent->initialMarking[p])
 
858
                {
 
859
                    auto out = getOutArc(t, p);
 
860
                    if(out == t.post.end() || out->place != p || out->weight >= in->weight)
 
861
                    {
 
862
                        ok = false;
 
863
                        break;
 
864
                    }
 
865
                }               
 
866
                else
 
867
                {
 
868
                    notenabled.insert(cons);
 
869
                }
 
870
            }
 
871
            
 
872
            if(!ok || notenabled.size() == 0) continue;
 
873
 
 
874
            for(uint prod : place.producers)
 
875
            {
 
876
                if(notenabled.count(prod) == 0)
 
877
                {
 
878
                    ok = false;
 
879
                    break;
 
880
                }
 
881
                // check that producing arcs originate from transition also 
 
882
                // consuming. If so, we know it will never fire.
 
883
                Transition& t = getTransition(prod);
 
884
                ArcIter it = getInArc(p, t);
 
885
                if(it == t.pre.end())
 
886
                {
 
887
                    ok = false;
 
888
                    break;
 
889
                }
 
890
            }
 
891
            
 
892
            if(!ok) continue;
 
893
 
 
894
            _ruleE++;
 
895
            continueReductions = true;
 
896
          
 
897
            if(placeInQuery[p] == 0) 
 
898
                parent->initialMarking[p] = 0;
 
899
            
 
900
            bool skipplace = (notenabled.size() == place.consumers.size()) && (placeInQuery[p] == 0);
 
901
            for(uint cons : notenabled)
 
902
                skipTransition(cons);
 
903
 
 
904
            if(skipplace)
 
905
                skipPlace(p);
 
906
            
 
907
        }
 
908
        assert(consistent());
 
909
        return continueReductions;
 
910
    }
 
911
   
 
912
    bool Reducer::ReducebyRuleI(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers) {
 
913
        bool reduced = false;
 
914
        if(remove_loops)
 
915
        {
 
916
            std::vector<uint32_t> wtrans;
 
917
            std::vector<bool> tseen(parent->numberOfTransitions(), false);
 
918
 
 
919
            for(uint32_t p = 0; p < parent->numberOfPlaces(); ++p)
 
920
            {
 
921
                if(hasTimedout()) return false;
 
922
                if(placeInQuery[p] > 0)
 
923
                {
 
924
                    const Place& place = parent->_places[p];
 
925
                    for(auto t : place.consumers)
 
926
                    {
 
927
                        if(!tseen[t])
 
928
                        {
 
929
                            wtrans.push_back(t);
 
930
                            tseen[t] = true;
 
931
                        }
 
932
                    }
 
933
                    for(auto t : place.producers)
 
934
                    {
 
935
                        if(!tseen[t])
 
936
                        {
 
937
                            wtrans.push_back(t);
 
938
                            tseen[t] = true;
 
939
                        }
 
940
                    }
 
941
                }
 
942
            }
 
943
 
 
944
            std::vector<bool> pseen(parent->numberOfPlaces(), false);        
 
945
            while(!wtrans.empty())
 
946
            {
 
947
                if(hasTimedout()) return false;
 
948
                auto t = wtrans.back();
 
949
                wtrans.pop_back();
 
950
                const Transition& trans = parent->_transitions[t];
 
951
                for(const Arc& arc : trans.pre)
 
952
                {
 
953
                    const Place& place = parent->_places[arc.place];
 
954
                    if(arc.inhib)
 
955
                    {
 
956
                        for(auto pt : place.consumers)
 
957
                        {
 
958
                            if(!tseen[pt])
 
959
                            {
 
960
                                Transition& trans = parent->_transitions[pt];
 
961
                                auto it = trans.post.begin();
 
962
                                for(; it != trans.post.end(); ++it)
 
963
                                    if(it->place >= arc.place) break;
 
964
                                if(it != trans.post.end() && it->place == arc.place)
 
965
                                {
 
966
                                    auto it2 = trans.pre.begin();
 
967
                                    for(; it2 != trans.pre.end(); ++it2)
 
968
                                        if(it2->place >= arc.place || it2->inhib) break;
 
969
                                    if(it->weight <= it2->weight) continue;
 
970
                                }
 
971
                                tseen[pt] = true;
 
972
                                wtrans.push_back(pt);                                    
 
973
                            }
 
974
                        }                        
 
975
                    }
 
976
                    else
 
977
                    {
 
978
                        for(auto pt : place.producers)
 
979
                        {
 
980
                            if(!tseen[pt])
 
981
                            {                                    
 
982
                                Transition& trans = parent->_transitions[pt];
 
983
                                auto it = trans.pre.begin();
 
984
                                for(; it != trans.pre.end(); ++it)
 
985
                                    if(it->place >= arc.place) break;
 
986
 
 
987
                                if(it != trans.pre.end() && it->place == arc.place && !it->inhib)
 
988
                                {
 
989
                                    auto it2 = trans.post.begin();
 
990
                                    for(; it2 != trans.post.end(); ++it2)
 
991
                                        if(it2->place >= arc.place) break;
 
992
                                    if(it->weight >= it2->weight) continue;
 
993
                                }
 
994
 
 
995
                                tseen[pt] = true;
 
996
                                wtrans.push_back(pt);
 
997
                            }
 
998
                        }
 
999
 
 
1000
                        for(auto pt : place.consumers)
 
1001
                        {
 
1002
                            if(!tseen[pt] && (!remove_consumers || placeInQuery[arc.place] > 0))
 
1003
                            {
 
1004
                                tseen[pt] = true;
 
1005
                                wtrans.push_back(pt);                                    
 
1006
                            }
 
1007
                        }
 
1008
                    }
 
1009
                    pseen[arc.place] = true;
 
1010
                }
 
1011
            }
 
1012
 
 
1013
            for(size_t t = 0; t < parent->numberOfTransitions(); ++t)
 
1014
            {
 
1015
                if(!tseen[t] && !parent->_transitions[t].skip)
 
1016
                {
 
1017
                    skipTransition(t);
 
1018
                    reduced = true;
 
1019
                }
 
1020
            }
 
1021
 
 
1022
            for(size_t p = 0; p < parent->numberOfPlaces(); ++p)
 
1023
            {
 
1024
                if(!pseen[p] && !parent->_places[p].skip && placeInQuery[p] == 0)
 
1025
                {
 
1026
                    assert(placeInQuery[p] == 0);
 
1027
                    skipPlace(p);
 
1028
                    reduced = true;
 
1029
                }
 
1030
            }
 
1031
            
 
1032
            if(reduced)
 
1033
                ++_ruleI;
 
1034
        }
 
1035
        else
 
1036
        {            
 
1037
            const size_t numberofplaces = parent->numberOfPlaces();
 
1038
            for(uint32_t p = 0; p < numberofplaces; ++p)
 
1039
            {
 
1040
                if(hasTimedout()) return false;
 
1041
                Place& place = parent->_places[p];
 
1042
                if(place.skip) continue;
 
1043
                if(place.inhib) continue;
 
1044
                if(placeInQuery[p] > 0) continue;
 
1045
                if(place.consumers.size() > 0) continue;
 
1046
 
 
1047
                ++_ruleI;
 
1048
                reduced = true;
 
1049
 
 
1050
                std::vector<uint32_t> torem;
 
1051
                if(remove_consumers)
 
1052
                {
 
1053
                    for(auto& t : place.producers)
 
1054
                    {
 
1055
                        auto& trans = parent->_transitions[t];
 
1056
                        if(trans.post.size() != 1) // place will be removed later
 
1057
                            continue;
 
1058
                        bool ok = true;
 
1059
                        for(auto& a : trans.pre)
 
1060
                        {
 
1061
                            if(placeInQuery[a.place] > 0)
 
1062
                            {
 
1063
                                ok = false;
 
1064
                            }
 
1065
                        }
 
1066
                        if(ok) torem.push_back(t);
 
1067
                    }
 
1068
                }
 
1069
                skipPlace(p);
 
1070
                for(auto t : torem)
 
1071
                    skipTransition(t);
 
1072
                assert(consistent());
 
1073
            }
 
1074
        }
 
1075
        
 
1076
        return reduced;
 
1077
    }
 
1078
   
 
1079
    bool Reducer::ReducebyRuleF(uint32_t* placeInQuery) {
 
1080
        bool continueReductions = false;
 
1081
        const size_t numberofplaces = parent->numberOfPlaces();
 
1082
        for(uint32_t p = 0; p < numberofplaces; ++p)
 
1083
        {
 
1084
            if(hasTimedout()) return false;
 
1085
            Place& place = parent->_places[p];
 
1086
            if(place.skip) continue;
 
1087
            if(place.inhib) continue;
 
1088
            if(place.producers.size() < place.consumers.size()) continue;
 
1089
            if(placeInQuery[p] != 0) continue; 
 
1090
            
 
1091
            bool ok = true;
 
1092
            for(uint cons : place.consumers)
 
1093
            {
 
1094
                Transition& t = getTransition(cons);
 
1095
                auto w = getInArc(p, t)->weight;
 
1096
                if(w > parent->initialMarking[p])
 
1097
                {
 
1098
                    ok = false;
 
1099
                    break;
 
1100
                }               
 
1101
                else
 
1102
                {
 
1103
                    auto it = getOutArc(t, p);
 
1104
                    if(it == t.post.end() || 
 
1105
                       it->place != p     ||
 
1106
                       it->weight < w)
 
1107
                    {
 
1108
                        ok = false;
 
1109
                        break;
 
1110
                    }
 
1111
                }
 
1112
            }
 
1113
            
 
1114
            if(!ok) continue;
 
1115
            
 
1116
            ++_ruleF;
 
1117
            
 
1118
            if((numberofplaces - _removedPlaces) > 1)
 
1119
            {
 
1120
                if(reconstructTrace)
 
1121
                {
 
1122
                    for(auto t : place.consumers)
 
1123
                    {
 
1124
                        std::string tname = getTransitionName(t);
 
1125
                        const ArcIter arc = getInArc(p, getTransition(t));
 
1126
                        _extraconsume[tname].emplace_back(getPlaceName(p), arc->weight);
 
1127
                    }
 
1128
                }
 
1129
                skipPlace(p);
 
1130
                continueReductions = true;
 
1131
            }
 
1132
            
 
1133
        }
 
1134
        assert(consistent());
 
1135
        return continueReductions;
 
1136
    }
 
1137
    
 
1138
    
 
1139
    bool Reducer::ReducebyRuleG(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers) {
 
1140
        if(!remove_loops) return false;
 
1141
        bool continueReductions = false;
 
1142
        for(uint32_t t = 0; t < parent->numberOfTransitions(); ++t)
 
1143
        {
 
1144
            if(hasTimedout()) return false;
 
1145
            Transition& trans = parent->_transitions[t];
 
1146
            if(trans.skip) continue;
 
1147
            if(trans.inhib) continue;
 
1148
            if(trans.pre.size() < trans.post.size()) continue;
 
1149
            if(!remove_loops && trans.pre.size() == 0) continue;
 
1150
            
 
1151
            auto postit = trans.post.begin();
 
1152
            auto preit = trans.pre.begin();
 
1153
            
 
1154
            bool ok = true;
 
1155
            while(true)
 
1156
            {
 
1157
                if(preit == trans.pre.end() && postit == trans.post.end())
 
1158
                    break;
 
1159
                if(preit == trans.pre.end())
 
1160
                {
 
1161
                    ok = false;
 
1162
                    break;
 
1163
                }
 
1164
                if(preit->inhib || parent->_places[preit->place].inhib)
 
1165
                {
 
1166
                    ok = false;
 
1167
                    break;
 
1168
                }
 
1169
                if(postit != trans.post.end() && preit->place == postit->place)
 
1170
                {
 
1171
                    if(!remove_consumers && preit->weight != postit->weight)
 
1172
                    {
 
1173
                        ok = false;
 
1174
                        break;
 
1175
                    }
 
1176
                    if((placeInQuery[preit->place] > 0 && preit->weight != postit->weight) ||
 
1177
                       (placeInQuery[preit->place] == 0 && preit->weight < postit->weight))
 
1178
                    {
 
1179
                        ok = false;
 
1180
                        break;
 
1181
                    }
 
1182
                    ++preit;
 
1183
                    ++postit;
 
1184
                }
 
1185
                else if(postit == trans.post.end() || preit->place < postit->place) 
 
1186
                {
 
1187
                    if(placeInQuery[preit->place] > 0 || !remove_consumers)
 
1188
                    {
 
1189
                        ok = false;
 
1190
                        break;
 
1191
                    }
 
1192
                    ++preit;
 
1193
                }
 
1194
                else
 
1195
                {
 
1196
                    // could not match a post with a pre
 
1197
                    ok = false;
 
1198
                    break;
 
1199
                }
 
1200
            }
 
1201
            if(ok)
 
1202
            {
 
1203
                for(preit = trans.pre.begin();preit != trans.pre.end(); ++preit)
 
1204
                {
 
1205
                    if(preit->inhib || parent->_places[preit->place].inhib)
 
1206
                    {
 
1207
                        ok = false;
 
1208
                        break;
 
1209
                    }
 
1210
                }
 
1211
            }
 
1212
                        
 
1213
            if(!ok) continue;
 
1214
            ++_ruleG;
 
1215
            skipTransition(t);
 
1216
        }
 
1217
        assert(consistent());
 
1218
        return continueReductions;
 
1219
    }
 
1220
    
 
1221
    bool Reducer::ReducebyRuleH(uint32_t* placeInQuery)
 
1222
    {
 
1223
        if(reconstructTrace) 
 
1224
            return false; // we don't know where in the loop the tokens are needed
 
1225
        auto transok = [this](uint32_t t) -> uint32_t {
 
1226
            auto& trans = parent->_transitions[t];
 
1227
            if(_tflags[t] != 0) 
 
1228
                return _tflags[t];
 
1229
            _tflags[t] = 1;
 
1230
            if(trans.inhib || 
 
1231
               trans.pre.size() != 1 ||
 
1232
               trans.post.size() != 1) 
 
1233
            {
 
1234
                return 2;
 
1235
            }
 
1236
            
 
1237
            auto p1 = trans.pre[0].place;
 
1238
            auto p2 = trans.post[0].place;
 
1239
            
 
1240
            // we actually do not need weights to be 1 here.
 
1241
            // there is a special case when the places are always "inputting"
 
1242
            // and "outputting" with a GCD that is equal to the weight of the
 
1243
            // specific transition.
 
1244
            // Ie, the place always have a number of tokens (disregarding
 
1245
            // initial tokens) that is dividable with the transition weight
 
1246
            
 
1247
            if(trans.pre[0].weight != 1 ||
 
1248
               trans.post[0].weight != 1 ||
 
1249
               p1 == p2 ||
 
1250
               parent->_places[p1].inhib ||
 
1251
               parent->_places[p2].inhib)
 
1252
            {
 
1253
                return 2;
 
1254
            }
 
1255
            return 1;
 
1256
        };
 
1257
        
 
1258
        auto removeLoop = [this,placeInQuery](std::vector<uint32_t>& loop) -> bool {
 
1259
            size_t i = 0;
 
1260
            for(; i < loop.size(); ++i)
 
1261
                if(loop[i] == loop.back())
 
1262
                    break;
 
1263
            
 
1264
            assert(_tflags[loop.back()]== 1);
 
1265
            if(i == loop.size() - 1)
 
1266
                return false;
 
1267
 
 
1268
            auto p1 = parent->_transitions[loop[i]].pre[0].place;
 
1269
            bool removed = false;
 
1270
            
 
1271
            for(size_t j = i + 1; j < loop.size() - 1; ++j)
 
1272
            {
 
1273
                if(hasTimedout()) 
 
1274
                    return removed;
 
1275
                auto p2 = parent->_transitions[loop[j]].pre[0].place;
 
1276
                if(placeInQuery[p2] > 0 || placeInQuery[p1] > 0)
 
1277
                {
 
1278
                    p1 = p2;
 
1279
                    continue;
 
1280
                }
 
1281
                if(p1 == p2)
 
1282
                {
 
1283
                    continue;
 
1284
                }
 
1285
                removed = true;
 
1286
                ++_ruleH;
 
1287
                skipTransition(loop[j-1]);
 
1288
                auto& place1 = parent->_places[p1];
 
1289
                auto& place2 = parent->_places[p2];
 
1290
 
 
1291
                {
 
1292
 
 
1293
                    for(auto p2it : place2.consumers)
 
1294
                    {
 
1295
                        auto& t = parent->_transitions[p2it];
 
1296
                        auto arc = getInArc(p2, t);
 
1297
                        assert(arc != t.pre.end());
 
1298
                        assert(arc->place == p2);
 
1299
                        auto a = *arc;
 
1300
                        a.place = p1;
 
1301
                        auto dest = std::lower_bound(t.pre.begin(), t.pre.end(), a);
 
1302
                        if(dest == t.pre.end() || dest->place != p1)
 
1303
                        {
 
1304
                            t.pre.insert(dest, a);
 
1305
                            auto lb = std::lower_bound(place1.consumers.begin(), place1.consumers.end(), p2it);
 
1306
                            place1.consumers.insert(lb, p2it);
 
1307
                        }
 
1308
                        else
 
1309
                        {
 
1310
                            dest->weight += a.weight;
 
1311
                        }
 
1312
                        consistent();
 
1313
                    }
 
1314
                }
 
1315
                
 
1316
                {
 
1317
                    auto p2it = place2.producers.begin();
 
1318
 
 
1319
                    for(;p2it != place2.producers.end(); ++p2it)
 
1320
                    {
 
1321
                        auto& t = parent->_transitions[*p2it];
 
1322
                        Arc a = *getOutArc(t, p2);
 
1323
                        a.place = p1;
 
1324
                        auto dest = std::lower_bound(t.post.begin(), t.post.end(), a);
 
1325
                        if(dest == t.post.end() || dest->place != p1)
 
1326
                        {
 
1327
                            t.post.insert(dest, a);
 
1328
                            auto lb = std::lower_bound(place1.producers.begin(), place1.producers.end(), *p2it);
 
1329
                            place1.producers.insert(lb, *p2it);
 
1330
                        }
 
1331
                        else
 
1332
                        {
 
1333
                            dest->weight += a.weight;
 
1334
                        }
 
1335
                        consistent();
 
1336
                    }
 
1337
                }
 
1338
                parent->initialMarking[p1] += parent->initialMarking[p2];
 
1339
                skipPlace(p2);
 
1340
                assert(placeInQuery[p2] == 0);
 
1341
            }
 
1342
            return removed;
 
1343
        };
 
1344
        
 
1345
        bool continueReductions = false;
 
1346
        for(uint32_t t = 0; t < parent->numberOfTransitions(); ++t)
 
1347
        {
 
1348
            if(hasTimedout())
 
1349
                return continueReductions;
 
1350
            _tflags.resize(parent->_transitions.size(), 0);
 
1351
            std::fill(_tflags.begin(), _tflags.end(), 0);
 
1352
            std::vector<uint32_t> stack;
 
1353
            {
 
1354
                if(_tflags[t] != 0) continue;
 
1355
                auto& trans = parent->_transitions[t];
 
1356
                if(trans.skip) continue;
 
1357
                _tflags[t] = transok(t);
 
1358
                if(_tflags[t] != 1) continue;
 
1359
                stack.push_back(t);
 
1360
            }
 
1361
            bool outer = true;
 
1362
            while(stack.size() > 0 && outer)
 
1363
            {
 
1364
                if(hasTimedout())
 
1365
                    return continueReductions;
 
1366
                auto it = stack.back();
 
1367
                auto post = parent->_transitions[it].post[0].place;
 
1368
                bool found = false;
 
1369
                for(auto& nt : parent->_places[post].consumers)
 
1370
                {
 
1371
                    if(hasTimedout())
 
1372
                        return continueReductions;
 
1373
                    auto& nexttrans = parent->_transitions[nt];
 
1374
                    if(nt == it || nexttrans.skip) 
 
1375
                        continue; // handled elsewhere
 
1376
                    if(_tflags[nt] == 1 && stack.size() > 1) 
 
1377
                    {
 
1378
                        stack.push_back(nt);
 
1379
                        bool found = removeLoop(stack);
 
1380
                        continueReductions |= found;
 
1381
    
 
1382
                        if(found)
 
1383
                        {
 
1384
                            outer = false;
 
1385
                            break;
 
1386
                        }
 
1387
                        else
 
1388
                        {
 
1389
                            stack.pop_back();
 
1390
                        }
 
1391
                    }
 
1392
                    else if(_tflags[nt] == 0)
 
1393
                    {
 
1394
                        _tflags[nt] = transok(nt);
 
1395
                        if(_tflags[nt] == 2)
 
1396
                        {
 
1397
                            continue;
 
1398
                        }
 
1399
                        else
 
1400
                        {
 
1401
                            assert(_tflags[nt] == 1);
 
1402
                            stack.push_back(nt);
 
1403
                            found = true;
 
1404
                            break;
 
1405
                        }
 
1406
                    }
 
1407
                    else
 
1408
                    {
 
1409
                        continue;
 
1410
                    }
 
1411
                }
 
1412
                if(!found && outer)
 
1413
                {
 
1414
                    _tflags[it] = 2;
 
1415
                    stack.pop_back();
 
1416
                }
 
1417
            }
 
1418
        }   
 
1419
        return continueReductions;
 
1420
    }
 
1421
    
 
1422
    bool Reducer::ReducebyRuleJ(uint32_t* placeInQuery)
 
1423
    {
 
1424
        bool continueReductions = false;
 
1425
        for(uint32_t t = 0; t < parent->numberOfTransitions(); ++t)
 
1426
        {
 
1427
            if(hasTimedout())
 
1428
                return continueReductions;
 
1429
 
 
1430
            if(parent->_transitions[t].skip ||
 
1431
               parent->_transitions[t].inhib ||
 
1432
               parent->_transitions[t].pre.size() != 1)
 
1433
                continue;
 
1434
            auto p = parent->_transitions[t].pre[0].place;
 
1435
            if(placeInQuery[p] > 0)
 
1436
            {
 
1437
                continue; // can be relaxed
 
1438
            }
 
1439
            if(parent->initialMarking[p] > 0) 
 
1440
            {
 
1441
                continue; // can be relaxed
 
1442
            }
 
1443
            const Place& place = parent->_places[p];
 
1444
            if(place.skip) continue;
 
1445
            if(place.inhib) continue;
 
1446
            if(place.consumers.size() < 1) continue;
 
1447
            if(place.producers.size() < 1) continue;
 
1448
            
 
1449
            // check that prod and cons are not overlapping
 
1450
            const auto presize = place.producers.size(); // can be relaxed >= 2
 
1451
            const auto postsize = place.consumers.size(); // can be relaxed >= 2
 
1452
            bool ok = true;
 
1453
            for(size_t i = 0; i < postsize; ++i)
 
1454
            {   // this can be done smarter than a quadratic loop!
 
1455
                for(size_t j = 0; j < presize; ++j)
 
1456
                {
 
1457
                    ok &= place.consumers[i] != place.producers[j];                        
 
1458
                }
 
1459
            }
 
1460
            if(!ok) continue;
 
1461
            // check that post of consumer is not messing with query or inhib
 
1462
            // if either all pre or all post are query-free, we are ok.
 
1463
            bool inquery = false;
 
1464
            for(auto t : place.consumers)
 
1465
            {
 
1466
                Transition& trans = parent->_transitions[t];
 
1467
                if(trans.pre.size() == 1) // can be relaxed
 
1468
                {
 
1469
                    // check that weights match
 
1470
                    // can be relaxed
 
1471
                    ok &= trans.pre[0].weight == 1;
 
1472
                    ok &= !trans.pre[0].inhib;
 
1473
                }
 
1474
                else 
 
1475
                {
 
1476
                    ok = false;
 
1477
                    break;
 
1478
                }
 
1479
                for(auto& pp : trans.post)
 
1480
                {
 
1481
                    ok &= !parent->_places[pp.place].inhib;
 
1482
                    inquery |= placeInQuery[pp.place] > 0;
 
1483
                    ok &= pp.weight == 1; // can be relaxed
 
1484
                }
 
1485
                if(!ok) 
 
1486
                    break;
 
1487
            }
 
1488
            if(!ok) continue;
 
1489
            // check that pre of producing do not mess with query or inhib
 
1490
            for(auto& t : place.producers)
 
1491
            {
 
1492
                Transition& trans = parent->_transitions[t];
 
1493
                for(const auto& arc : trans.post)
 
1494
                {
 
1495
                    ok &= !inquery || placeInQuery[arc.place] == 0;
 
1496
                    ok &= !parent->_places[arc.place].inhib;
 
1497
                }
 
1498
            }
 
1499
            if(!ok) continue;
 
1500
            ++_ruleJ;
 
1501
            continueReductions = true;
 
1502
            // otherwise we can skip the place by merging up the two transitions
 
1503
            // constructing 4 new transitions, one for each combination.  
 
1504
            // In the binary case, we want to achieve the following four transitions
 
1505
            // post[n] = pre[n] + post[n]
 
1506
            // pre[0] = pre[0] + post[1]
 
1507
            // pre[1] = pre[1] + post[0]
 
1508
            
 
1509
            // start by copying out the post of each of the posts
 
1510
            Place pp = place;
 
1511
            skipPlace(p);
 
1512
            std::vector<std::vector<Arc>> posts;
 
1513
            std::vector<Transition> pres;
 
1514
            
 
1515
            for(auto t : pp.consumers)
 
1516
                posts.push_back(parent->_transitions[t].post);
 
1517
            
 
1518
            for(auto t : pp.producers)
 
1519
                pres.push_back(parent->_transitions[t]);
 
1520
            
 
1521
            // remove old transitions, we will create new ones
 
1522
            for(auto t : pp.consumers)
 
1523
                skipTransition(t);
 
1524
            
 
1525
            for(auto t : pp.producers)
 
1526
                skipTransition(t);      
 
1527
 
 
1528
            // compute all permutations
 
1529
            for(auto& trans : pres)
 
1530
            {
 
1531
                for(auto& postset : posts)
 
1532
                {
 
1533
                    auto id = parent->_transitions.size();
 
1534
                    if(!_skipped_trans.empty())
 
1535
                        id = _skipped_trans.back();
 
1536
                    else
 
1537
                    {
 
1538
                        continue;
 
1539
                        parent->_transitions.emplace_back();
 
1540
                    }
 
1541
                    parent->_transitions[id] = trans;
 
1542
                    auto& target = parent->_transitions[id];
 
1543
                    for(auto& arc : postset)
 
1544
                        target.addPostArc(arc);
 
1545
 
 
1546
                    // add to places
 
1547
                    if(_skipped_trans.empty())
 
1548
                        parent->_transitionnames[newTransName()] = id;
 
1549
                    
 
1550
                    for(auto& arc : target.pre)
 
1551
                        parent->_places[arc.place].addConsumer(id);
 
1552
                    for(auto& arc : target.post)
 
1553
                        parent->_places[arc.place].addProducer(id); 
 
1554
                    if(!_skipped_trans.empty())
 
1555
                    {
 
1556
                        --_removedTransitions; // recycling
 
1557
                        _skipped_trans.pop_back();
 
1558
                    }
 
1559
                    parent->_transitions[id].skip = false;
 
1560
                    parent->_transitions[id].inhib = false;
 
1561
                    consistent();
 
1562
                }
 
1563
            }
 
1564
            consistent();
 
1565
        }
 
1566
        return continueReductions;
 
1567
    }
 
1568
        
 
1569
    void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool next_safe, std::vector<uint32_t>& reduction) {
 
1570
        this->_timeout = timeout;
 
1571
        _timer = std::chrono::high_resolution_clock::now();
 
1572
        assert(consistent());
 
1573
        this->reconstructTrace = reconstructTrace;
 
1574
        if(reconstructTrace && enablereduction >= 1 && enablereduction <= 2)
 
1575
            std::cout << "Rule H disabled when a trace is requested." << std::endl;
 
1576
        if (enablereduction == 2) { // for k-boundedness checking only rules A, D and H are applicable
 
1577
            bool changed = true;
 
1578
            while (changed && !hasTimedout()) {
 
1579
                changed = false;
 
1580
                if(!next_safe)
 
1581
                {
 
1582
                    while(ReducebyRuleA(context.getQueryPlaceCount())) changed = true;
 
1583
                    while(ReducebyRuleD(context.getQueryPlaceCount())) changed = true;
 
1584
                    while(ReducebyRuleH(context.getQueryPlaceCount())) changed = true;
 
1585
                }
 
1586
            }
 
1587
        }
 
1588
        else if (enablereduction == 1) { // in the aggressive reduction all four rules are used as long as they remove something
 
1589
            bool changed = false;
 
1590
            do
 
1591
            {
 
1592
                if(remove_loops && !next_safe)
 
1593
                    while(ReducebyRuleI(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
 
1594
                do{
 
1595
                    do { // start by rules that do not move tokens
 
1596
                        changed = false;
 
1597
                        while(ReducebyRuleE(context.getQueryPlaceCount())) changed = true;
 
1598
                        while(ReducebyRuleC(context.getQueryPlaceCount())) changed = true;
 
1599
                        if(!next_safe) 
 
1600
                        {
 
1601
                            while(ReducebyRuleF(context.getQueryPlaceCount())) changed = true;
 
1602
                            while(ReducebyRuleG(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
 
1603
                            if(!remove_loops) 
 
1604
                                while(ReducebyRuleI(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
 
1605
                            while(ReducebyRuleD(context.getQueryPlaceCount())) changed = true;
 
1606
                        }
 
1607
                    } while(changed && !hasTimedout());
 
1608
                    if(!next_safe) 
 
1609
                    { // then apply tokens moving rules
 
1610
                        //while(ReducebyRuleJ(context.getQueryPlaceCount())) changed = true;
 
1611
                        while(ReducebyRuleB(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
 
1612
                        while(ReducebyRuleA(context.getQueryPlaceCount())) changed = true;
 
1613
                    }    
 
1614
                } while(changed && !hasTimedout());
 
1615
                if(!next_safe && !changed)
 
1616
                {
 
1617
                    // Only try RuleH last. It can reduce applicability of other rules.
 
1618
                    while(ReducebyRuleH(context.getQueryPlaceCount())) changed = true;
 
1619
                }
 
1620
            } while(!hasTimedout() && changed);
 
1621
 
 
1622
        }
 
1623
        else
 
1624
        {
 
1625
            const char* rnames = "ABCDEFGHIJ";
 
1626
            for(int i = reduction.size() - 1; i > 0; --i)
 
1627
            {
 
1628
                if(next_safe)
 
1629
                {
 
1630
                    if(reduction[i] != 2 && reduction[i] != 4)
 
1631
                    {
 
1632
                        std::cerr << "Skipping Rule" << rnames[reduction[i]] << " due to NEXT operator in proposition" << std::endl;
 
1633
                        reduction.erase(reduction.begin() + i);
 
1634
                        continue;
 
1635
                    }
 
1636
                }
 
1637
                if(!remove_loops && reduction[i] == 5)
 
1638
                {
 
1639
                    std::cerr << "Skipping Rule" << rnames[reduction[i]] << " as proposition is loop sensitive" << std::endl;
 
1640
                    reduction.erase(reduction.begin() + i);
 
1641
                }
 
1642
            }
 
1643
            bool changed = true;
 
1644
            while(changed && !hasTimedout())
 
1645
            {
 
1646
                changed = false;
 
1647
                for(auto r : reduction)
 
1648
                {
 
1649
#ifndef NDEBUG
 
1650
                    auto c = std::chrono::high_resolution_clock::now();
 
1651
                    auto op = _removedPlaces;
 
1652
                    auto ot = _removedTransitions;
 
1653
#endif
 
1654
                    switch(r)
 
1655
                    {
 
1656
                        case 0:
 
1657
                            while(ReducebyRuleA(context.getQueryPlaceCount())) changed = true;
 
1658
                            break;
 
1659
                        case 1:
 
1660
                            while(ReducebyRuleB(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
 
1661
                            break;
 
1662
                        case 2:
 
1663
                            while(ReducebyRuleC(context.getQueryPlaceCount())) changed = true;
 
1664
                            break;
 
1665
                        case 3:
 
1666
                            while(ReducebyRuleD(context.getQueryPlaceCount())) changed = true;
 
1667
                            break;              
 
1668
                        case 4:
 
1669
                            while(ReducebyRuleE(context.getQueryPlaceCount())) changed = true;
 
1670
                            break;              
 
1671
                        case 5:
 
1672
                            while(ReducebyRuleF(context.getQueryPlaceCount())) changed = true;
 
1673
                            break;             
 
1674
                        case 6:
 
1675
                            while(ReducebyRuleG(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
 
1676
                            break;             
 
1677
                        case 7:
 
1678
                            while(ReducebyRuleH(context.getQueryPlaceCount())) changed = true;
 
1679
                            break;             
 
1680
                        case 8:
 
1681
                            while(ReducebyRuleI(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
 
1682
                            break;                            
 
1683
                        case 9:
 
1684
                            while(ReducebyRuleJ(context.getQueryPlaceCount())) changed = true;
 
1685
                            break;
 
1686
                    }
 
1687
#ifndef NDEBUG
 
1688
                    auto end = std::chrono::high_resolution_clock::now();
 
1689
                    auto diff = std::chrono::duration_cast<std::chrono::seconds>(end - c);
 
1690
                    std::cout << "SPEND " << diff.count()  << " ON " << rnames[r] << std::endl;
 
1691
                    std::cout << "REM " << ((int)_removedPlaces-(int)op) << " " << ((int)_removedTransitions-(int)ot) << std::endl;
 
1692
#endif
 
1693
                    if(hasTimedout())
 
1694
                        break;
 
1695
                }
 
1696
            }
 
1697
        }
 
1698
    }
 
1699
    
 
1700
    void Reducer::postFire(std::ostream& out, const std::string& transition)
 
1701
    {
 
1702
        if(_postfire.count(transition) > 0)
 
1703
        {
 
1704
            std::queue<std::string> tofire;
 
1705
            
 
1706
            for(auto& el : _postfire[transition]) tofire.push(el);
 
1707
            
 
1708
            for(auto& el : _postfire[transition])
 
1709
            {
 
1710
                tofire.pop();
 
1711
                out << "\t<transition id=\"" << el << "\">\n";
 
1712
                extraConsume(out, el);
 
1713
                out << "\t</transition>\n";               
 
1714
                postFire(out, el);
 
1715
            }
 
1716
        }
 
1717
    }
 
1718
    
 
1719
    void Reducer::initFire(std::ostream& out)
 
1720
    {
 
1721
        for(std::string& init : _initfire)
 
1722
        {
 
1723
            out << "\t<transition id=\"" << init << "\">\n";
 
1724
            extraConsume(out, init);            
 
1725
            out << "\t</transition>\n";
 
1726
            postFire(out, init);
 
1727
        }
 
1728
    }
 
1729
    
 
1730
    void Reducer::extraConsume(std::ostream& out, const std::string& transition)
 
1731
    {
 
1732
        if(_extraconsume.count(transition) > 0)
 
1733
        {
 
1734
            for(auto& ec : _extraconsume[transition])
 
1735
            {
 
1736
                out << ec;
 
1737
            }
 
1738
        }
 
1739
    }
 
1740
 
 
1741
} //PetriNet namespace