← Back to branch summary

~tapaal-ltl/verifypn/answer-for-gui

« back to all changes in this revision

Viewing changes to include/PetriEngine/Structures/StateSet.h

  • Committer: srba.jiri at gmail
  • Date: 2021-04-02 18:13:50 UTC
  • mfrom: (230.1.28 mcc2021)
  • Revision ID: srba.jiri@gmail.com-20210402181350-k71xtjut3r48l1o5
merged in lp:~tapaal-ltl/verifypn/mcc2021 adding LTL, colored fixed-point unfolding for CPN and other performance improvements

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/PetriEngine/Structures/StateSet.h
32
32
        class StateSetInterface
33
33
        {
34
34
        public:
35
 
            StateSetInterface(const PetriNet& net, uint32_t kbound) :
36
 
            _encoder(net.numberOfPlaces(), kbound), _net(net)
 
35
            StateSetInterface(const PetriNet& net, uint32_t kbound, int nplaces = -1) :
 
36
            _nplaces(nplaces == -1 ? net.numberOfPlaces() : nplaces),
 
37
            _encoder(_nplaces, kbound), _net(net)
37
38
            {
38
39
                _discovered = 0;
39
40
                _kbound = kbound;
40
41
                _maxTokens = 0;
41
 
                _maxPlaceBound = std::vector<uint32_t>(_net.numberOfPlaces(), 0);
42
 
                _sp = binarywrapper_t(sizeof(uint32_t)*_net.numberOfPlaces()*8);
 
42
                _maxPlaceBound = std::vector<uint32_t>(net.numberOfPlaces(), 0);
 
43
                _sp = binarywrapper_t(sizeof(uint32_t) * _nplaces * 8);
43
44
            }
44
45
 
45
 
            ~StateSetInterface()
 
46
            virtual ~StateSetInterface()
46
47
            {
47
48
                _sp.release();
48
49
            }
50
51
            virtual std::pair<bool, size_t> add(State& state) = 0;
51
52
            
52
53
            virtual void decode(State& state, size_t id) = 0;
53
 
            
 
54
 
 
55
            virtual std::pair<bool, size_t> lookup(State &state) = 0;
 
56
 
54
57
            const PetriNet& net() { return _net;}
55
58
            
56
59
            virtual void setHistory(size_t id, size_t transition) = 0;
57
60
            
58
61
            virtual std::pair<size_t, size_t> getHistory(size_t markingid) = 0;
 
62
 
 
63
            virtual void setHistory2(size_t id, size_t transition) = 0;
 
64
 
 
65
            virtual std::pair<size_t, size_t> getHistory2(size_t markingid) = 0;
59
66
            
60
67
        protected:
61
68
            size_t _discovered;
62
69
            uint32_t _kbound;
63
70
            uint32_t _maxTokens;
 
71
            size_t _nplaces;
64
72
            std::vector<uint32_t> _maxPlaceBound;
65
73
            AlignedEncoder _encoder;
66
74
            const PetriNet& _net;
105
113
 
106
114
 
107
115
                size_t length = _encoder.encode(state.marking(), type);
 
116
                if(length*8 >= std::numeric_limits<uint16_t>::max())
 
117
                {
 
118
                    std::cerr << "error: Marking could not be encoded into less than 2^16 bytes, current limit of PTries" << std::endl;
 
119
                    std::exit(-1);
 
120
                }
108
121
                binarywrapper_t w = binarywrapper_t(_encoder.scratchpad().raw(), length*8);
109
122
                auto tit = _trie.insert(w.raw(), w.size());
110
 
            
 
123
 
111
124
                
112
125
                if(!tit.first)
113
126
                {
114
 
                    return std::pair<bool, size_t>(false, std::numeric_limits<size_t>::max());
 
127
                    return std::pair<bool, size_t>(false, tit.second);
115
128
                }
116
129
                
117
130
#ifdef DEBUG
133
146
                return std::pair<bool, size_t>(true, tit.second);
134
147
            }
135
148
 
 
149
            template <typename T>
 
150
            std::pair<bool, size_t> _lookup(const State& state, T& _trie) {
 
151
                MarkVal sum = 0;
 
152
                bool allsame = true;
 
153
                uint32_t val = 0;
 
154
                uint32_t active = 0;
 
155
                uint32_t last = 0;
 
156
                markingStats(state.marking(), sum, allsame, val, active, last);
 
157
 
 
158
                unsigned char type = _encoder.getType(sum, active, allsame, val);
 
159
 
 
160
                size_t length = _encoder.encode(state.marking(), type);
 
161
                binarywrapper_t w = binarywrapper_t(_encoder.scratchpad().raw(), length*8);
 
162
                auto tit = _trie.exists(w.raw(), w.size());
 
163
 
 
164
                if (tit.first) {
 
165
                    return tit;
 
166
                }
 
167
                else return std::make_pair(false, std::numeric_limits<size_t>::max());
 
168
            }
 
169
 
 
170
 
 
171
 
136
172
        public:
137
173
            size_t discovered() const {
138
174
                return _discovered;
152
188
            {
153
189
                uint32_t cnt = 0;
154
190
                
155
 
                for (uint32_t i = 0; i < _net.numberOfPlaces(); i++)
 
191
                for (uint32_t i = 0; i < _nplaces; i++)
156
192
                {
157
193
                    uint32_t old = val;
158
194
                    if(marking[i] != 0)
186
222
            {
187
223
                _decode(state, id, _trie);
188
224
            }
189
 
            
190
 
            
 
225
 
 
226
            virtual std::pair<bool, size_t> lookup(State& state) override
 
227
            {
 
228
                return _lookup(state, _trie);
 
229
            }
 
230
 
191
231
            virtual void setHistory(size_t id, size_t transition) override {}
192
232
 
193
233
            virtual std::pair<size_t, size_t> getHistory(size_t markingid) override
195
235
                assert(false); 
196
236
                return std::make_pair(0,0); 
197
237
            }
 
238
 
 
239
            virtual void setHistory2(size_t id, size_t transition) override {}
 
240
 
 
241
            virtual std::pair<size_t, size_t> getHistory2(size_t markingid) override
 
242
            {
 
243
                assert(false);
 
244
                return std::make_pair(std::numeric_limits<std::size_t>::max(), std::numeric_limits<std::size_t>::max());
 
245
            }
198
246
            
199
247
        private:
200
248
            ptrie_t _trie;
206
254
            struct traceable_t
207
255
            {
208
256
                ptrie::uint parent;
209
 
                ptrie::uint transition;
 
257
                ptrie::uint transition = std::numeric_limits<ptrie::uint>::max();
 
258
                ptrie::uint parent2;
 
259
                ptrie::uint transition2 = std::numeric_limits<ptrie::uint>::max();
210
260
            };
211
261
            
212
262
        private:
232
282
                _parent = id;
233
283
                _decode(state, id, _trie);
234
284
            }
235
 
                       
236
 
            virtual void setHistory(size_t id, size_t transition) override 
 
285
 
 
286
            virtual std::pair<bool, size_t> lookup(State& state) override
 
287
            {
 
288
                return _lookup(state, _trie);
 
289
            }
 
290
 
 
291
 
 
292
            virtual void setHistory(size_t id, size_t transition) override
237
293
            {
238
294
                traceable_t& t = _trie.get_data(id);
239
295
                t.parent = _parent;
245
301
                traceable_t& t = _trie.get_data(markingid);
246
302
                return std::pair<size_t, size_t>(t.parent, t.transition);
247
303
            }
 
304
 
 
305
            virtual void setHistory2(size_t id, size_t transition) override {
 
306
                traceable_t &t = _trie.get_data(id);
 
307
                t.parent2 = _parent;
 
308
                t.transition2 = transition;
 
309
            }
 
310
 
 
311
            virtual std::pair<size_t, size_t> getHistory2(size_t markingid) override {
 
312
                traceable_t &t = _trie.get_data(markingid);
 
313
                return std::pair<size_t, size_t>(t.parent2, t.transition2);
 
314
            }
 
315
 
 
316
            void setParent(size_t id) {
 
317
                _parent = id;
 
318
            }
248
319
            
249
320
        private:
250
321
            ptrie_t _trie;