← Back to branch summary

~tapaal-contributor/verifypn/unfoldTACPN

« back to all changes in this revision

Viewing changes to include/PetriEngine/TAR/TARAutomata.h

  • Committer: tpede16 at aau
  • Date: 2020-11-20 12:40:58 UTC
  • Revision ID: tpede16@student.aau.dk-20201120124058-a21zlqk70r4l753c
Merge with trunk

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/PetriEngine/TAR/TARAutomata.h
 
1
/*
 
2
 * To change this license header, choose License Headers in Project Properties.
 
3
 * To change this template file, choose Tools | Templates
 
4
 * and open the template in the editor.
 
5
 */
 
6
 
 
7
/* 
 
8
 * File:   TARAutomata.h
 
9
 * Author: petko
 
10
 *
 
11
 * Created on January 2, 2018, 10:06 AM
 
12
 */
 
13
 
 
14
 
 
15
#ifndef TARAUTOMATA_H
 
16
#define TARAUTOMATA_H
 
17
#include <cassert>
 
18
#include <algorithm>
 
19
#include <vector>
 
20
#include <string>
 
21
#include <set>
 
22
 
 
23
#include "range.h"
 
24
#include "PetriEngine/PetriNet.h"
 
25
 
 
26
namespace PetriEngine {
 
27
    namespace Reachability {
 
28
        class AutomataState;
 
29
 
 
30
        struct AutomataEdge
 
31
        {
 
32
            size_t edge;
 
33
            std::vector<size_t> to;
 
34
 
 
35
            bool operator == (const AutomataEdge& other) const
 
36
            {
 
37
                return edge == other.edge;
 
38
            }
 
39
 
 
40
            bool operator != (const AutomataEdge& other) const
 
41
            {
 
42
                return !(*this == other);
 
43
            }
 
44
 
 
45
 
 
46
            bool operator < ( const AutomataEdge& other) const
 
47
            {
 
48
                return edge < other.edge;
 
49
            };
 
50
 
 
51
            AutomataEdge(size_t e)
 
52
                : edge(e) {};
 
53
 
 
54
            AutomataEdge(const AutomataEdge& other) = default;
 
55
            AutomataEdge(AutomataEdge&&) = default;
 
56
            AutomataEdge& operator=(const AutomataEdge& other) = default;
 
57
            AutomataEdge& operator=(AutomataEdge&& other) = default;
 
58
            
 
59
            bool has_to(size_t i)
 
60
            {
 
61
                if(to.size() > 0 && to[0] == 0) return true;
 
62
                auto lb = std::lower_bound(to.begin(), to.end(), i);
 
63
                return lb != to.end() && *lb == i;
 
64
            }
 
65
 
 
66
            bool add(size_t i)
 
67
            {
 
68
                if(to.size() > 0 && to[0] == 0) return false;
 
69
                if(i == 0) { to.clear(); to.push_back(0); return true; }
 
70
 
 
71
                auto lb = std::lower_bound(to.begin(), to.end(), i);
 
72
                if(lb != to.end() && *lb == i)
 
73
                {
 
74
                    return false;
 
75
                }
 
76
                else
 
77
                {
 
78
                    to.insert(lb, i);
 
79
                    return true;
 
80
                }
 
81
            }
 
82
 
 
83
            bool remove(size_t i)
 
84
            {
 
85
                auto lb = std::lower_bound(to.begin(), to.end(), i);
 
86
                if(lb == to.end() || *lb != i)
 
87
                {
 
88
                    return false;
 
89
                }
 
90
                else
 
91
                {
 
92
                    to.erase(lb);
 
93
                    return true;
 
94
                }
 
95
            }
 
96
            
 
97
            std::ostream& operator<<(std::ostream& os) const
 
98
            {
 
99
                os << edge << " ==> ";
 
100
                for(size_t i : to) os << i << ", ";
 
101
                return os;
 
102
            }
 
103
        };        
 
104
        class TraceSet;
 
105
        struct AutomataState
 
106
        {
 
107
        private:
 
108
            std::vector<AutomataEdge> edges;
 
109
            bool accept = false;
 
110
            std::vector<size_t> simulates;
 
111
            std::vector<size_t> simulators;
 
112
            friend class TraceSet;
 
113
        public:
 
114
            prvector_t interpolant;
 
115
            AutomataState(prvector_t interpol) : interpolant(interpol) {};
 
116
            inline bool is_accepting() const
 
117
            {
 
118
                return accept;
 
119
            }
 
120
 
 
121
            inline void set_accepting(bool val = true)
 
122
            {
 
123
                accept = val;
 
124
            }
 
125
 
 
126
            inline bool has_edge(const size_t& e, size_t to)
 
127
            {
 
128
                AutomataEdge edge(e);
 
129
                auto lb = std::lower_bound(edges.begin(), edges.end(), edge);
 
130
                if(lb == edges.end() || *lb != edge)
 
131
                {
 
132
                    return false;
 
133
                }
 
134
                return lb->has_to(to);
 
135
            }
 
136
 
 
137
            inline bool has_any_edge(size_t prod, const size_t& e)
 
138
            {
 
139
                AutomataEdge edge(e);
 
140
                auto lb = std::lower_bound(edges.begin(), edges.end(), edge);
 
141
                if(lb == edges.end() || *lb != edge)
 
142
                {
 
143
                    return false;
 
144
                }
 
145
                return lb->to.size() > 0;
 
146
            }
 
147
 
 
148
            inline bool add_edge(const size_t& e, size_t to)
 
149
            {
 
150
                AutomataEdge edge(e);
 
151
                auto lb = std::lower_bound(edges.begin(), edges.end(), edge);
 
152
#ifndef NDEBUG
 
153
                bool isnew = false;
 
154
#endif
 
155
                if(lb == edges.end() || *lb != edge)
 
156
                {
 
157
                    assert(lb == edges.end() || *lb != edge);
 
158
                    lb = edges.insert(lb, edge);
 
159
#ifndef NDEBUG
 
160
                    isnew = true;
 
161
#endif
 
162
                }
 
163
                assert(*lb == edge);
 
164
                assert(is_sorted(edges.begin(), edges.end()));
 
165
                bool res = lb->add(to);
 
166
                assert(!isnew || res);
 
167
                assert(lb->to.size() >= 0);
 
168
                return res;
 
169
            }
 
170
 
 
171
            inline bool remove_edge(size_t e)
 
172
            {
 
173
                AutomataEdge edge(e);
 
174
                auto lb = std::lower_bound(edges.begin(), edges.end(), edge);
 
175
                if(lb == edges.end() || *lb != edge)
 
176
                    return false;
 
177
                edges.erase(lb);
 
178
                return true;
 
179
            }
 
180
            
 
181
            inline bool remove_edge(size_t e, size_t to)
 
182
            {
 
183
                AutomataEdge edge(e);
 
184
                auto lb = std::lower_bound(edges.begin(), edges.end(), edge);
 
185
                if(lb == edges.end() || *lb != edge)
 
186
                {
 
187
                    assert(lb == edges.end() || *lb != edge);
 
188
                    assert(is_sorted(edges.begin(), edges.end()));
 
189
                    return false;
 
190
                }
 
191
                assert(*lb == edge);
 
192
                assert(is_sorted(edges.begin(), edges.end()));
 
193
                bool removed = lb->remove(to);
 
194
                if(removed && lb->to.size() == 0)
 
195
                {
 
196
                    edges.erase(lb);
 
197
                }
 
198
                else
 
199
                {
 
200
                    assert(lb->to.size() >= 0);
 
201
                }
 
202
                return removed;
 
203
            }
 
204
 
 
205
            inline auto first_edge(size_t& e) const
 
206
            {
 
207
                AutomataEdge edge(e);
 
208
                auto lb = std::lower_bound(edges.begin(), edges.end(), edge);        
 
209
                return lb;
 
210
            }
 
211
 
 
212
            inline auto last_edge() const
 
213
            {
 
214
                return edges.end();
 
215
            }
 
216
 
 
217
            inline auto& get_edges() const
 
218
            {
 
219
                return edges;
 
220
            }
 
221
            
 
222
            std::ostream& print(std::ostream& os) const {
 
223
                os << "\t PREDICATE\n";
 
224
                interpolant.print(os);
 
225
                os << "\n";
 
226
                os << "\tSIMS [ ";
 
227
                for(auto s : simulates)
 
228
                    os << s << ", ";
 
229
                os << "]\n\tSIMED [";
 
230
                for(auto s : simulators)
 
231
                    os << s << ", ";
 
232
                os << "]\n";
 
233
                os << "\t EDGES\n";
 
234
                for(auto& e : edges)
 
235
                {
 
236
                    os << "\t\t<" << (e.edge ? std::to_string(e.edge-1) : "Q") << "> --> [";
 
237
                    for(auto t : e.to)
 
238
                        os << t << ", ";
 
239
                    os << "]\n";
 
240
                }
 
241
                return os;
 
242
            }
 
243
        };
 
244
 
 
245
 
 
246
        struct state_t 
 
247
        {
 
248
 
 
249
        private:
 
250
            size_t offset = 0;
 
251
            size_t size = std::numeric_limits<size_t>::max();
 
252
            size_t edgecnt = 0; 
 
253
            std::set<size_t> interpolant;
 
254
        public:
 
255
            bool operator == (const state_t& other)
 
256
            {
 
257
//                if((get_edge_cnt() == 0) != (other.get_edge_cnt() == 0)) return false;
 
258
                if( interpolant.size() == other.interpolant.size() &&
 
259
                    std::equal( interpolant.begin(),        interpolant.end(), 
 
260
                                other.interpolant.begin(),  other.interpolant.end()))
 
261
                {
 
262
                    return true;
 
263
                }
 
264
                return false;
 
265
            }
 
266
 
 
267
            bool operator != (const state_t& other)
 
268
            {
 
269
                return !(*this == other);
 
270
            }
 
271
 
 
272
            bool operator <= (const state_t& other)
 
273
            {
 
274
//                if((get_edge_cnt() == 0) != (other.get_edge_cnt() == 0)) return false;
 
275
                if( interpolant.size() <= other.interpolant.size() &&
 
276
                    std::includes(other.interpolant.begin(), other.interpolant.end(),
 
277
                                  interpolant.begin(), interpolant.end()))
 
278
                {
 
279
                    return true;
 
280
                }
 
281
                return false;
 
282
            }
 
283
 
 
284
            size_t get_edge_cnt()
 
285
            {
 
286
                if(edgecnt == 0)
 
287
                    return 0;
 
288
                else
 
289
                    return 1 + (((edgecnt-1) + offset) % size);
 
290
            }
 
291
 
 
292
            void set_edge(size_t edge)
 
293
            {
 
294
                edgecnt = edge;
 
295
                offset = 0;
 
296
            }
 
297
            
 
298
            bool next_edge(const PetriNet& net)
 
299
            {
 
300
                ++edgecnt;
 
301
                return done(net);
 
302
            }
 
303
            
 
304
            bool done(const PetriNet& net) const {
 
305
                return edgecnt > net.numberOfTransitions();
 
306
            }
 
307
 
 
308
            bool reset_edges(const PetriNet& net)
 
309
            {
 
310
                size = net.numberOfTransitions();
 
311
                edgecnt = 0;
 
312
                offset = std::rand();// % (net.numberOfTransitions());
 
313
                return edgecnt > net.numberOfTransitions();
 
314
            }
 
315
 
 
316
            inline void add_interpolant(size_t ninter)
 
317
            {
 
318
                interpolant.insert(ninter);
 
319
            }
 
320
 
 
321
            inline std::set<size_t>& get_interpolants()
 
322
            {
 
323
                return interpolant;
 
324
            }
 
325
 
 
326
            inline void set_interpolants(const std::set<size_t>& interpolants)
 
327
            {
 
328
                interpolant = interpolants;
 
329
            }
 
330
        };
 
331
        
 
332
        typedef std::vector<state_t> trace_t;
 
333
    }
 
334
}
 
335
 
 
336
 
 
337
#endif /* TARAUTOMATA_H */