← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Structures/StateSet.h

  • 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:
PetriEngine/Structures/StateSet.h
1
 
/* VerifyPN - TAPAAL Petri Net Engine
2
 
 * Copyright (C) 2016  Peter Gjøl Jensen <root@petergjoel.dk>
3
 
 * 
4
 
 * This program is free software: you can redistribute it and/or modify
5
 
 * it under the terms of the GNU General Public License as published by
6
 
 * the Free Software Foundation, either version 3 of the License, or
7
 
 * (at your option) any later version.
8
 
 * 
9
 
 * This program is distributed in the hope that it will be useful,
10
 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11
 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12
 
 * GNU General Public License for more details.
13
 
 * 
14
 
 * You should have received a copy of the GNU General Public License
15
 
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
16
 
 */
17
 
#ifndef STATESET_H
18
 
#define STATESET_H
19
 
#include <unordered_map>
20
 
#include <iostream>
21
 
#include "State.h"
22
 
#include "AlignedEncoder.h"
23
 
#include "ptrie_stable.h"
24
 
#include "ptrie_map.h"
25
 
#include "binarywrapper.h"
26
 
#include "../errorcodes.h"
27
 
 
28
 
 
29
 
namespace PetriEngine {
30
 
    namespace Structures {
31
 
        
32
 
        class StateSetInterface
33
 
        {
34
 
        public:
35
 
            StateSetInterface(const PetriNet& net, uint32_t kbound) :
36
 
            _encoder(net.numberOfPlaces(), kbound), _net(net)
37
 
            {
38
 
                _discovered = 0;
39
 
                _kbound = kbound;
40
 
                _maxTokens = 0;
41
 
                _maxPlaceBound = std::vector<uint32_t>(_net.numberOfPlaces(), 0);
42
 
                _sp = binarywrapper_t(sizeof(uint32_t)*_net.numberOfPlaces()*8);
43
 
            }
44
 
            
45
 
            virtual std::pair<bool, size_t> add(State& state) = 0;
46
 
            
47
 
            virtual void decode(State& state, size_t id) = 0;
48
 
            
49
 
            const PetriNet& net() { return _net;}
50
 
            
51
 
            virtual void setHistory(size_t id, size_t transition) = 0;
52
 
            
53
 
            virtual std::pair<size_t, size_t> getHistory(size_t markingid) = 0;
54
 
            
55
 
        protected:
56
 
            size_t _discovered;
57
 
            uint32_t _kbound;
58
 
            uint32_t _maxTokens;
59
 
            std::vector<uint32_t> _maxPlaceBound;
60
 
            AlignedEncoder _encoder;
61
 
            const PetriNet& _net;
62
 
            binarywrapper_t _sp;     
63
 
#ifdef DEBUG
64
 
            std::vector<uint32_t*> _dbg;
65
 
#endif
66
 
            template<typename T>
67
 
            void _decode(State& state, size_t id, T& _trie)
68
 
            {
69
 
                    _trie.unpack(id, _encoder.scratchpad().raw());
70
 
                    _encoder.decode(state.marking(), _encoder.scratchpad().raw());
71
 
 
72
 
#ifdef DEBUG
73
 
                    assert(memcmp(state.marking(), _dbg[id], sizeof(uint32_t)*_net.numberOfPlaces()) == 0);
74
 
#endif
75
 
            }             
76
 
            
77
 
            template<typename T>
78
 
            std::pair<bool, size_t> _add(State& state, T& _trie) {
79
 
                _discovered++;
80
 
                
81
 
#ifdef DEBUG
82
 
                if(_discovered % 1000000 == 0) std::cout << "Found number " << _discovered << std::endl;
83
 
#endif
84
 
                
85
 
                MarkVal sum = 0;
86
 
                bool allsame = true;
87
 
                uint32_t val = 0;
88
 
                uint32_t active = 0;
89
 
                uint32_t last = 0;
90
 
                markingStats(state.marking(), sum, allsame, val, active, last);               
91
 
 
92
 
                if (_maxTokens < sum)
93
 
                    _maxTokens = sum;
94
 
 
95
 
                //Check that we're within k-bound
96
 
                if (_kbound != 0 && sum > _kbound)
97
 
                    return std::pair<bool, size_t>(false, std::numeric_limits<size_t>::max());
98
 
                    
99
 
                unsigned char type = _encoder.getType(sum, active, allsame, val);
100
 
 
101
 
 
102
 
                size_t length = _encoder.encode(state.marking(), type);
103
 
                binarywrapper_t w = binarywrapper_t(_encoder.scratchpad().raw(), length*8);
104
 
                auto tit = _trie.insert(w);
105
 
            
106
 
                
107
 
                if(!tit.first)
108
 
                {
109
 
                    return std::pair<bool, size_t>(false, std::numeric_limits<size_t>::max());
110
 
                }
111
 
                
112
 
#ifdef DEBUG
113
 
                _dbg.push_back(new uint32_t[_net.numberOfPlaces()]);
114
 
                memcpy(_dbg.back(), state.marking(), _net.numberOfPlaces()*sizeof(uint32_t));
115
 
                decode(state, _trie.size() - 1);
116
 
#endif
117
 
           
118
 
                // update the max token bound for each place in the net (only for newly discovered markings)
119
 
                for (uint32_t i = 0; i < _net.numberOfPlaces(); i++) 
120
 
                {
121
 
                    _maxPlaceBound[i] = std::max<MarkVal>( state.marking()[i],
122
 
                                                            _maxPlaceBound[i]);
123
 
                }
124
 
 
125
 
#ifdef DEBUG    
126
 
                if(_trie.size() % 100000 == 0) std::cout << "Inserted " << _trie.size() << std::endl;
127
 
#endif     
128
 
                return std::pair<bool, size_t>(true, tit.second);
129
 
            }
130
 
 
131
 
        public:
132
 
            size_t discovered() const {
133
 
                return _discovered;
134
 
            }
135
 
 
136
 
            uint32_t maxTokens() const {
137
 
                return _maxTokens;
138
 
            }
139
 
            
140
 
            std::vector<MarkVal> maxPlaceBound() const {
141
 
                return _maxPlaceBound;
142
 
            }
143
 
            
144
 
        protected:
145
 
            
146
 
            void markingStats(const uint32_t* marking, MarkVal& sum, bool& allsame, uint32_t& val, uint32_t& active, uint32_t& last)
147
 
            {
148
 
                uint32_t cnt = 0;
149
 
                
150
 
                for (uint32_t i = 0; i < _net.numberOfPlaces(); i++)
151
 
                {
152
 
                    uint32_t old = val;
153
 
                    if(marking[i] != 0)
154
 
                    {
155
 
                        ++cnt;
156
 
                        last = std::max(last, i);
157
 
                        val = std::max(marking[i], val);
158
 
                        if(old != 0 && marking[i] != old) allsame = false;
159
 
                        ++active;
160
 
                        sum += marking[i];
161
 
                    }
162
 
                }
163
 
            }
164
 
        };
165
 
        
166
 
#define STATESET_BUCKETS 1000000
167
 
        class StateSet : public StateSetInterface {
168
 
        private:
169
 
            using wrapper_t = ptrie::binarywrapper_t;
170
 
            using ptrie_t = ptrie::set_stable<>;
171
 
            
172
 
        public:
173
 
            using StateSetInterface::StateSetInterface;
174
 
             
175
 
            virtual std::pair<bool, size_t> add(State& state) override
176
 
            {
177
 
                return _add(state, _trie);
178
 
            }
179
 
            
180
 
            virtual void decode(State& state, size_t id) override
181
 
            {
182
 
                _decode(state, id, _trie);
183
 
            }
184
 
            
185
 
            
186
 
            virtual void setHistory(size_t id, size_t transition) override {}
187
 
 
188
 
            virtual std::pair<size_t, size_t> getHistory(size_t markingid) override
189
 
            { 
190
 
                assert(false); 
191
 
                return std::make_pair(0,0); 
192
 
            }
193
 
            
194
 
        private:               
195
 
            ptrie_t _trie;
196
 
        };
197
 
 
198
 
        class TracableStateSet : public StateSetInterface
199
 
        {
200
 
        public:
201
 
            struct traceable_t
202
 
            {
203
 
                ptrie::uint parent;
204
 
                ptrie::uint transition;
205
 
            };
206
 
            
207
 
        private:
208
 
            using ptrie_t = ptrie::map<traceable_t>;
209
 
            
210
 
        public:
211
 
            using StateSetInterface::StateSetInterface;
212
 
 
213
 
            virtual std::pair<bool, size_t> add(State& state) override
214
 
            {
215
 
#ifdef DEBUG
216
 
                size_t tmppar = _parent; // we might change this while debugging.
217
 
#endif
218
 
                auto res = _add(state, _trie);
219
 
#ifdef DEBUG
220
 
                _parent = tmppar;
221
 
#endif
222
 
                return res;
223
 
            }
224
 
            
225
 
            virtual void decode(State& state, size_t id) override
226
 
            {
227
 
                _parent = id;
228
 
                _decode(state, id, _trie);
229
 
            }
230
 
                       
231
 
            virtual void setHistory(size_t id, size_t transition) override 
232
 
            {
233
 
                traceable_t& t = _trie.get_data(id);
234
 
                t.parent = _parent;
235
 
                t.transition = transition;
236
 
            }
237
 
            
238
 
            virtual std::pair<size_t, size_t> getHistory(size_t markingid) override
239
 
            {
240
 
                traceable_t& t = _trie.get_data(markingid);
241
 
                return std::pair<size_t, size_t>(t.parent, t.transition);
242
 
            }
243
 
            
244
 
        private:
245
 
            ptrie_t _trie;
246
 
            size_t _parent = 0;
247
 
        };
248
 
        
249
 
    }
250
 
}
251
 
 
252
 
 
253
 
#endif // STATESET_H