← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/ReducingSuccessorGenerator.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/ReducingSuccessorGenerator.cpp
 
1
#include "PetriEngine/ReducingSuccessorGenerator.h"
 
2
 
 
3
#include <cassert>
 
4
#include "PetriEngine/PQL/Contexts.h"
 
5
 
 
6
namespace PetriEngine {
 
7
 
 
8
    ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet& net) : SuccessorGenerator(net), _inhibpost(net._nplaces){
 
9
        _current = 0;
 
10
        _enabled = std::make_unique<bool[]>(net._ntransitions);
 
11
        _stubborn = std::make_unique<bool[]>(net._ntransitions);
 
12
        _dependency = std::make_unique<uint32_t[]>(net._ntransitions);
 
13
        _places_seen = std::make_unique<uint8_t[]>(_net.numberOfPlaces());
 
14
        reset();
 
15
        constructPrePost();
 
16
        constructDependency();
 
17
        checkForInhibitor();      
 
18
    }
 
19
 
 
20
    ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries) : ReducingSuccessorGenerator(net) {
 
21
        _queries.reserve(queries.size());
 
22
        for(auto& q : queries)
 
23
            _queries.push_back(q.get());
 
24
    }
 
25
 
 
26
    ReducingSuccessorGenerator::~ReducingSuccessorGenerator() {
 
27
    }
 
28
    
 
29
    void ReducingSuccessorGenerator::checkForInhibitor(){
 
30
        _netContainsInhibitorArcs=false;
 
31
        for (uint32_t t = 0; t < _net._ntransitions; t++) {
 
32
            const TransPtr& ptr = _net._transitions[t];
 
33
            uint32_t finv = ptr.inputs;
 
34
            uint32_t linv = ptr.outputs;
 
35
            for (; finv < linv; finv++) { // Post set of places
 
36
                if (_net._invariants[finv].inhibitor) {
 
37
                    _netContainsInhibitorArcs=true;
 
38
                    return;
 
39
                }
 
40
            }
 
41
        }
 
42
    }
 
43
 
 
44
    void ReducingSuccessorGenerator::constructPrePost() {
 
45
        std::vector<std::pair<std::vector<trans_t>, std::vector < trans_t>>> tmp_places(_net._nplaces);
 
46
                
 
47
        for (uint32_t t = 0; t < _net._ntransitions; t++) {
 
48
            const TransPtr& ptr = _net._transitions[t];
 
49
            uint32_t finv = ptr.inputs;
 
50
            uint32_t linv = ptr.outputs;
 
51
            for (; finv < linv; finv++) { // Post set of places
 
52
                if (_net._invariants[finv].inhibitor) {
 
53
                    _inhibpost[_net._invariants[finv].place].push_back(t);
 
54
                    _netContainsInhibitorArcs=true;
 
55
                } else {
 
56
                    tmp_places[_net._invariants[finv].place].second.emplace_back(t, _net._invariants[finv].direction);
 
57
                }
 
58
            }
 
59
 
 
60
            finv = linv;
 
61
            linv = _net._transitions[t + 1].inputs;
 
62
            for (; finv < linv; finv++) { // Pre set of places
 
63
                if(_net._invariants[finv].direction > 0)
 
64
                    tmp_places[_net._invariants[finv].place].first.emplace_back(t, _net._invariants[finv].direction);
 
65
            }
 
66
        }
 
67
 
 
68
        // flatten
 
69
        size_t ntrans = 0;
 
70
        for (auto p : tmp_places) {
 
71
            ntrans += p.first.size() + p.second.size();
 
72
        }
 
73
        _transitions.reset(new trans_t[ntrans]);
 
74
 
 
75
        _places.reset(new place_t[_net._nplaces + 1]);
 
76
        uint32_t offset = 0;
 
77
        uint32_t p = 0;
 
78
        for (; p < _net._nplaces; ++p) {
 
79
            auto& pre = tmp_places[p].first;
 
80
            auto& post = tmp_places[p].second;
 
81
 
 
82
            // keep things nice for caches
 
83
            std::sort(pre.begin(), pre.end());
 
84
            std::sort(post.begin(), post.end());
 
85
 
 
86
            _places.get()[p].pre = offset;
 
87
            offset += pre.size();
 
88
            _places.get()[p].post = offset;
 
89
            offset += post.size();
 
90
            for (size_t tn = 0; tn < pre.size(); ++tn) {
 
91
                _transitions.get()[tn + _places.get()[p].pre] = pre[tn];
 
92
            }
 
93
 
 
94
            for (size_t tn = 0; tn < post.size(); ++tn) {
 
95
                _transitions.get()[tn + _places.get()[p].post] = post[tn];
 
96
            }
 
97
 
 
98
        }
 
99
        assert(offset == ntrans);
 
100
        _places.get()[p].pre = offset;
 
101
        _places.get()[p].post = offset;
 
102
    }
 
103
 
 
104
    void ReducingSuccessorGenerator::constructDependency() {
 
105
        memset(_dependency.get(), 0, sizeof(uint32_t) * _net._ntransitions);
 
106
 
 
107
        for (uint32_t t = 0; t < _net._ntransitions; t++) {
 
108
            uint32_t finv = _net._transitions[t].inputs;
 
109
            uint32_t linv = _net._transitions[t].outputs;
 
110
 
 
111
            for (; finv < linv; finv++) {
 
112
                const Invariant& inv = _net._invariants[finv];
 
113
                uint32_t p = inv.place;
 
114
                uint32_t ntrans = (_places.get()[p + 1].pre - _places.get()[p].post);
 
115
 
 
116
                for (uint32_t tIndex = 0; tIndex < ntrans; tIndex++) {
 
117
                    ++_dependency[t];
 
118
                }
 
119
            }
 
120
        }
 
121
    }
 
122
 
 
123
    void ReducingSuccessorGenerator::constructEnabled() {
 
124
        _ordering.clear();
 
125
        for (uint32_t p = 0; p < _net._nplaces; ++p) {
 
126
            // orphans are currently under "place 0" as a special case
 
127
            if (p == 0 || (*_parent).marking()[p] > 0) { 
 
128
                uint32_t t = _net._placeToPtrs[p];
 
129
                uint32_t last = _net._placeToPtrs[p + 1];
 
130
 
 
131
                for (; t != last; ++t) {
 
132
                    if (!checkPreset(t)) continue;
 
133
                    _enabled[t] = true;
 
134
                    _ordering.push_back(t);
 
135
                }
 
136
            }
 
137
        }
 
138
    }
 
139
 
 
140
    bool ReducingSuccessorGenerator::seenPre(uint32_t place) const
 
141
    {
 
142
        return (_places_seen.get()[place] & 1) != 0;
 
143
    }
 
144
    
 
145
    bool ReducingSuccessorGenerator::seenPost(uint32_t place) const
 
146
    {
 
147
        return (_places_seen.get()[place] & 2) != 0;
 
148
    }
 
149
    
 
150
    void ReducingSuccessorGenerator::presetOf(uint32_t place, bool make_closure) {
 
151
        if((_places_seen.get()[place] & 1) != 0) return;
 
152
        _places_seen.get()[place] = _places_seen.get()[place] | 1;
 
153
        for (uint32_t t = _places.get()[place].pre; t < _places.get()[place].post; t++)
 
154
        {
 
155
            auto& tr = _transitions.get()[t];
 
156
            addToStub(tr.index);
 
157
        }
 
158
        if(make_closure) closure();            
 
159
    }
 
160
    
 
161
    void ReducingSuccessorGenerator::postsetOf(uint32_t place, bool make_closure) {       
 
162
        if((_places_seen.get()[place] & 2) != 0) return;
 
163
        _places_seen.get()[place] = _places_seen.get()[place] | 2;
 
164
        for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++) {
 
165
            auto tr = _transitions.get()[t];
 
166
            if(tr.direction < 0)
 
167
                addToStub(tr.index);
 
168
        }
 
169
        if(make_closure) closure();
 
170
    }
 
171
    
 
172
    void ReducingSuccessorGenerator::addToStub(uint32_t t)
 
173
    {
 
174
        if(!_stubborn[t])
 
175
        {
 
176
            _stubborn[t] = true;
 
177
            _unprocessed.push_back(t);
 
178
        }
 
179
    }
 
180
    
 
181
    void ReducingSuccessorGenerator::inhibitorPostsetOf(uint32_t place){
 
182
        if((_places_seen.get()[place] & 4) != 0) return;
 
183
        _places_seen.get()[place] = _places_seen.get()[place] | 4;
 
184
        for(uint32_t& newstub : _inhibpost[place])
 
185
            addToStub(newstub);
 
186
    }
 
187
    
 
188
    void ReducingSuccessorGenerator::postPresetOf(uint32_t t, bool make_closure) {
 
189
        const TransPtr& ptr = _net._transitions[t];
 
190
        uint32_t finv = ptr.inputs;
 
191
        uint32_t linv = ptr.outputs;
 
192
        for (; finv < linv; finv++) { // pre-set of t
 
193
            if(_net._invariants[finv].inhibitor){ 
 
194
                presetOf(_net._invariants[finv].place, make_closure);
 
195
            } else {
 
196
                postsetOf(_net._invariants[finv].place, make_closure); 
 
197
            }
 
198
        }        
 
199
    }
 
200
    
 
201
 
 
202
    void ReducingSuccessorGenerator::prepare(const Structures::State* state) {
 
203
        _parent = state;
 
204
        memset(_places_seen.get(), 0, _net.numberOfPlaces());
 
205
        constructEnabled();
 
206
        if(_ordering.size() == 0) return;
 
207
        if(_ordering.size() == 1)
 
208
        {
 
209
            _stubborn[_ordering.front()] = true;
 
210
            return;
 
211
        }
 
212
        for (auto &q : _queries) {
 
213
            q->evalAndSet(PQL::EvaluationContext((*_parent).marking(), &_net));
 
214
            q->findInteresting(*this, false);
 
215
        }
 
216
        
 
217
        closure();
 
218
    }
 
219
    
 
220
    void ReducingSuccessorGenerator::closure()
 
221
    {
 
222
        while (!_unprocessed.empty()) {
 
223
            uint32_t tr = _unprocessed.front();
 
224
            _unprocessed.pop_front();
 
225
            const TransPtr& ptr = _net._transitions[tr];
 
226
            uint32_t finv = ptr.inputs;
 
227
            uint32_t linv = ptr.outputs;
 
228
            if(_enabled[tr]){
 
229
                for (; finv < linv; finv++) {
 
230
                    if(_net._invariants[finv].direction < 0)
 
231
                    {
 
232
                        auto place = _net._invariants[finv].place;
 
233
                        for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++) 
 
234
                            addToStub(_transitions.get()[t].index);
 
235
                    }
 
236
                }
 
237
                if(_netContainsInhibitorArcs){
 
238
                    uint32_t next_finv = _net._transitions[tr+1].inputs;
 
239
                    for (; linv < next_finv; linv++)
 
240
                    {
 
241
                        if(_net._invariants[linv].direction > 0)
 
242
                            inhibitorPostsetOf(_net._invariants[linv].place);
 
243
                    }
 
244
                }
 
245
            } else {
 
246
                bool ok = false;
 
247
                bool inhib = false;
 
248
                uint32_t cand = std::numeric_limits<uint32_t>::max();
 
249
               
 
250
                // Lets try to see if we havent already added sufficient pre/post 
 
251
                // for this transition.
 
252
                for (; finv < linv; ++finv) {
 
253
                    const Invariant& inv = _net._invariants[finv];
 
254
                    if ((*_parent).marking()[inv.place] < inv.tokens && !inv.inhibitor) {
 
255
                        inhib = false;
 
256
                        ok = (_places_seen.get()[inv.place] & 1) != 0;
 
257
                        cand = inv.place;
 
258
                    } else if ((*_parent).marking()[inv.place] >= inv.tokens && inv.inhibitor) {
 
259
                        inhib = true;
 
260
                        ok = (_places_seen.get()[inv.place] & 2) != 0;
 
261
                        cand = inv.place;
 
262
                    }
 
263
                    if(ok) break;
 
264
 
 
265
                }
 
266
                
 
267
                // OK, we didnt have sufficient, we just pick whatever is left
 
268
                // in cand.
 
269
                assert(cand != std::numeric_limits<uint32_t>::max());
 
270
                if(!ok && cand != std::numeric_limits<uint32_t>::max())
 
271
                {
 
272
                    if(!inhib) presetOf(cand);
 
273
                    else       postsetOf(cand);
 
274
                }
 
275
            }
 
276
        }        
 
277
    }
 
278
 
 
279
    bool ReducingSuccessorGenerator::next(Structures::State& write) {
 
280
        while (!_ordering.empty()) {
 
281
            _current = _ordering.front();
 
282
            _ordering.pop_front();
 
283
            if (_stubborn[_current]) {
 
284
                assert(_enabled[_current]);
 
285
                memcpy(write.marking(), (*_parent).marking(), _net._nplaces*sizeof(MarkVal));
 
286
                consumePreset(write, _current);
 
287
                producePostset(write, _current);
 
288
                return true;
 
289
            }
 
290
        }
 
291
        reset();
 
292
        return false;
 
293
    }
 
294
    
 
295
    uint32_t ReducingSuccessorGenerator::leastDependentEnabled() {
 
296
        uint32_t tLeast = -1;
 
297
        bool foundLeast = false;
 
298
        for (uint32_t t = 0; t < _net._ntransitions; t++) {
 
299
            if (_enabled[t]) {
 
300
                if (!foundLeast) {
 
301
                    tLeast = t;
 
302
                    foundLeast = true;
 
303
                } else {
 
304
                    if (_dependency[t] < _dependency[tLeast]) {
 
305
                        tLeast = t;
 
306
                    }
 
307
                }
 
308
            }
 
309
        }
 
310
        return tLeast;
 
311
    }
 
312
 
 
313
    void ReducingSuccessorGenerator::reset() {
 
314
        SuccessorGenerator::reset();
 
315
        memset(_enabled.get(), false, sizeof(bool) * _net._ntransitions);
 
316
        memset(_stubborn.get(), false, sizeof(bool) * _net._ntransitions);
 
317
    }
 
318
}