← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/TAR/TraceSet.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/TAR/TraceSet.cpp
 
1
/*
 
2
 *  Copyright Peter G. Jensen, all rights reserved.
 
3
 */
 
4
 
 
5
/* 
 
6
 * File:   TraceSet.cpp
 
7
 * Author: Peter G. Jensen <root@petergjoel.dk>
 
8
 * 
 
9
 * Created on April 2, 2020, 6:03 PM
 
10
 */
 
11
 
 
12
#include "PetriEngine/TAR/TraceSet.h"
 
13
 
 
14
 
 
15
namespace PetriEngine
 
16
{
 
17
    namespace Reachability
 
18
    {
 
19
 
 
20
        void inline_union(std::vector<size_t>& into, const std::vector<size_t>& other)
 
21
        {
 
22
            into.reserve(into.size() + other.size());
 
23
            auto iit = into.begin();
 
24
            auto oit = other.begin();
 
25
 
 
26
            while (oit != other.end()) {
 
27
                while (iit != into.end() && *iit < *oit) ++iit;
 
28
                if (iit == into.end()) {
 
29
                    into.insert(iit, oit, other.end());
 
30
                    break;
 
31
                }
 
32
                else if (*iit != *oit) {
 
33
                    iit = into.insert(iit, *oit);
 
34
                }
 
35
                ++oit;
 
36
            }
 
37
        }
 
38
 
 
39
        TraceSet::TraceSet(const PetriNet& net)
 
40
        : _net(net)
 
41
        {
 
42
            init();
 
43
        }
 
44
 
 
45
        void TraceSet::init()
 
46
        {
 
47
            prvector_t truerange;
 
48
            prvector_t falserange;
 
49
            {
 
50
                for (size_t v = 0; v < _net.numberOfPlaces(); ++v)
 
51
                    falserange.find_or_add(v) &= 0;
 
52
            }
 
53
            assert(falserange.is_false(_net.numberOfPlaces()));
 
54
            assert(truerange.is_true());
 
55
            assert(!falserange.is_true());
 
56
            assert(falserange.is_false(_net.numberOfPlaces()));
 
57
            assert(truerange.compare(falserange).first);
 
58
            assert(!truerange.compare(falserange).second);
 
59
            assert(falserange.compare(truerange).second);
 
60
            assert(!falserange.compare(truerange).first);
 
61
            _states.emplace_back(falserange); // false
 
62
            _states.emplace_back(truerange); // true
 
63
            computeSimulation(0);
 
64
 
 
65
            assert(_states[1].simulates.size() == 0);
 
66
            assert(_states[1].simulators.size() == 1);
 
67
            assert(_states[0].simulates.size() == 1);
 
68
            assert(_states[0].simulators.size() == 0);
 
69
 
 
70
            assert(_states[1].simulators[0] == 0);
 
71
            assert(_states[0].simulates[0] == 1);
 
72
 
 
73
            _intmap.emplace(falserange, 0);
 
74
            _intmap.emplace(truerange, 1);
 
75
 
 
76
            _initial.insert(1);
 
77
        }
 
78
 
 
79
        void TraceSet::clear()
 
80
        {
 
81
            _initial.clear();
 
82
            _intmap.clear();
 
83
            _states.clear();
 
84
            init();
 
85
        }
 
86
 
 
87
        
 
88
        std::set<size_t> TraceSet::minimize(const std::set<size_t>& org) const
 
89
        {
 
90
            std::set<size_t> minimal = org;
 
91
            for(size_t i : org)
 
92
                for(auto e : _states[i].simulates)
 
93
                    minimal.erase(e);
 
94
            return minimal;
 
95
        }
 
96
 
 
97
        void TraceSet::copyNonChanged(const std::set<size_t>& from, const std::vector<int64_t>& modifiers, std::set<size_t>& to) const
 
98
        {
 
99
            for (auto p : from)
 
100
                if (!_states[p].interpolant.restricts(modifiers))
 
101
                    to.insert(p);
 
102
        }
 
103
 
 
104
        std::set<size_t> TraceSet::maximize(const std::set<size_t>& org) const
 
105
        {
 
106
            auto maximal = org;
 
107
            maximal.insert(1);
 
108
            for (size_t i : org) 
 
109
                maximal.insert(_states[i].simulates.begin(), _states[i].simulates.end());
 
110
            return maximal;
 
111
        }
 
112
 
 
113
        std::pair<bool, size_t> TraceSet::stateForPredicate(prvector_t& predicate)
 
114
        {
 
115
            predicate.compress();
 
116
            assert(predicate.is_compact());
 
117
            if (predicate.is_true()) {
 
118
                return std::make_pair(false, 1);
 
119
            }
 
120
            else if (predicate.is_false(_net.numberOfPlaces())) {
 
121
                return std::make_pair(false, 0);
 
122
            }
 
123
 
 
124
            auto astate = _states.size();
 
125
            auto res = _intmap.emplace(predicate, astate);
 
126
            if (!res.second) {
 
127
#ifndef NDEBUG
 
128
                if (!(_states[res.first->second].interpolant == predicate)) {
 
129
                    assert(!(_states[res.first->second].interpolant < predicate));
 
130
                    assert(!(predicate < _states[res.first->second].interpolant));
 
131
                    assert(false);
 
132
                }
 
133
                for (auto& e : _intmap) {
 
134
                    assert(e.first == _states[e.second].interpolant);
 
135
                }
 
136
#endif
 
137
                return std::make_pair(false, res.first->second);
 
138
            }
 
139
            else {
 
140
                _states.emplace_back(predicate);
 
141
                computeSimulation(astate);
 
142
                res.first->second = astate;
 
143
                assert(_states[astate].interpolant == predicate);
 
144
#ifndef NDEBUG
 
145
                for (auto& s : _states) {
 
146
                    if (s.interpolant == predicate) {
 
147
                        if (&s == &_states[astate]) continue;
 
148
                        assert((s.interpolant < predicate) ||
 
149
                               (predicate < s.interpolant));
 
150
                        assert(false);
 
151
                    }
 
152
                }
 
153
                for (auto& e : _intmap) {
 
154
                    assert(e.first == _states[e.second].interpolant);
 
155
                }
 
156
#endif
 
157
                bool ok = true;
 
158
                for(auto& r : predicate._ranges)
 
159
                {
 
160
 
 
161
                    if(_net.initial()[r._place] > r._range._upper ||
 
162
                       _net.initial()[r._place] < r._range._lower)
 
163
                    {
 
164
                        ok = false;
 
165
                        break;
 
166
                    }
 
167
                }
 
168
                if(ok)
 
169
                {
 
170
                    auto lb = std::lower_bound(_initial.begin(), _initial.end(), astate);
 
171
                    if (lb == std::end(_initial) || *lb != res.second)
 
172
                    {
 
173
                        _initial.insert(lb, astate);
 
174
                    }
 
175
                }
 
176
                // check which edges actually change the predicate, add rest to automata
 
177
                for(size_t t = 0; t < _net.numberOfTransitions(); ++t)
 
178
                {
 
179
                    auto pre = _net.preset(t);
 
180
                    bool ok = true;
 
181
                    bool changes = false;
 
182
                    for(; pre.first != pre.second; ++pre.first)
 
183
                    {
 
184
                        auto it = predicate[pre.first->place];
 
185
                        if(it)
 
186
                        {
 
187
                            changes = true;
 
188
                            auto post = _net.postset(t);
 
189
                            int64_t change = pre.first->tokens;
 
190
                            if(pre.first->tokens > it->_range._upper)
 
191
                                _states[astate].add_edge(t+1, 0);
 
192
                            change *= -1;
 
193
                            for(; post.first != post.second; ++post.first)
 
194
                            {
 
195
                                if(post.first->place == pre.first->place)
 
196
                                {
 
197
                                    change += post.first->tokens;
 
198
                                    break;
 
199
                                }
 
200
                            }
 
201
                            if(change < 0 && !it->_range.no_lower())
 
202
                                ok = false;
 
203
                            else if(change > 0 && !it->_range.no_upper())
 
204
                                ok = false;
 
205
                        }
 
206
                        if(!ok) break;
 
207
                    }
 
208
                    
 
209
                    auto post = _net.postset(t);
 
210
                    for(; post.first != post.second; ++post.first)
 
211
                    {
 
212
                        auto it = predicate[post.first->place];
 
213
                        if(it)
 
214
                        {
 
215
                            changes = true;
 
216
                            auto pre = _net.preset(t);
 
217
                            int64_t change = post.first->tokens;
 
218
                            for(; pre.first != pre.second; ++pre.first)
 
219
                            {
 
220
                                if(pre.first->place == post.first->place)
 
221
                                {
 
222
                                    change -= pre.first->tokens;
 
223
                                    break;
 
224
                                }
 
225
                            }
 
226
                            if(change < 0 && !it->_range.no_lower())
 
227
                                ok = false;
 
228
                            else if(change > 0 && !it->_range.no_upper())
 
229
                                ok = false;
 
230
                        }
 
231
                        if(!ok) break;
 
232
                    }
 
233
                    
 
234
                    if(changes && ok)
 
235
                    {
 
236
                        _states[astate].add_edge(t+1, astate);
 
237
                    }
 
238
                }
 
239
                
 
240
                
 
241
                return std::make_pair(true, astate);
 
242
            }
 
243
        }
 
244
 
 
245
        void TraceSet::computeSimulation(size_t index)
 
246
        {
 
247
            AutomataState& state = _states[index];
 
248
            assert(index == _states.size() - 1 || index == 0);
 
249
            for (size_t i = 0; i < _states.size(); ++i) {
 
250
                if (i == index) continue;
 
251
                AutomataState& other = _states[i];
 
252
                std::pair<bool, bool> res = other.interpolant.compare(state.interpolant);
 
253
                assert(!res.first || !res.second);
 
254
                if (res.first) {
 
255
                    state.simulates.emplace_back(i);
 
256
                    auto lb = std::lower_bound(other.simulators.begin(), other.simulators.end(), index);
 
257
                    if (lb == std::end(other.simulators) || *lb != index)
 
258
                        other.simulators.insert(lb, index);
 
259
                    other.interpolant.compare(state.interpolant);
 
260
                }
 
261
                if (res.second) {
 
262
                    state.simulators.emplace_back(i);
 
263
                    auto lb = std::lower_bound(other.simulates.begin(), other.simulates.end(), index);
 
264
                    if (lb == std::end(other.simulates) || *lb != index)
 
265
                        other.simulates.insert(lb, index);
 
266
                    other.interpolant.compare(state.interpolant);
 
267
                }
 
268
            }
 
269
 
 
270
            assert(_states[1].simulates.size() == 0);
 
271
            assert(_states[0].simulators.size() == 0);
 
272
        }
 
273
 
 
274
        bool TraceSet::follow(const std::set<size_t>& from, std::set<size_t>& nextinter, size_t symbol)
 
275
        {
 
276
            nextinter.insert(1);
 
277
            for (size_t i : from) {
 
278
                if (i == 0) {
 
279
                    assert(false);
 
280
                    continue;
 
281
                }
 
282
                AutomataState& as = _states[i];
 
283
                if (as.is_accepting()) {
 
284
                    assert(false);
 
285
                    break;
 
286
                }
 
287
 
 
288
                auto it = as.first_edge(symbol);
 
289
 
 
290
                while (it != as.get_edges().end()) {
 
291
                    if (it->edge != symbol) {
 
292
                        break;
 
293
                    }
 
294
                    auto& ae = *it;
 
295
                    ++it;
 
296
                    assert(ae.to.size() > 0);
 
297
                    if (ae.to.front() == 0) 
 
298
                        return true;
 
299
                    nextinter.insert(ae.to.begin(), ae.to.end());
 
300
                }
 
301
            }
 
302
            return false;
 
303
        }
 
304
 
 
305
        void TraceSet::removeEdges(size_t edge)
 
306
        {
 
307
            for(auto& s : _states)
 
308
            {
 
309
                s.remove_edge(edge);
 
310
            }
 
311
            // TODO back color here to remove non-accepting end-components.
 
312
        }
 
313
        
 
314
        bool TraceSet::addTrace(std::vector<std::pair<prvector_t, size_t>>& inter)
 
315
        {
 
316
            assert(inter.size() > 0);
 
317
            bool some = false;
 
318
 
 
319
            size_t last = 1;
 
320
            {
 
321
                auto res = stateForPredicate(inter[0].first);
 
322
                some |= res.first;
 
323
                last = res.second;
 
324
                //inter[0].first.print(std::cerr) << std::endl;
 
325
            }
 
326
#ifndef NDEBUG
 
327
            bool added_terminal = false;
 
328
#endif
 
329
            for (size_t i = 0; i < inter.size(); ++i) {
 
330
                size_t j = i + 1;
 
331
//                std::cerr << " >> T" << inter[i].second << " <<" << std::endl;
 
332
                if (j == inter.size()) {
 
333
                    some |= _states[last].add_edge(inter[i].second, 0);
 
334
#ifndef NDEBUG                    
 
335
                    added_terminal = true;
 
336
#endif
 
337
//                    std::cerr << "FALSE" << std::endl;
 
338
                }
 
339
                else {
 
340
//                    inter[j].first.print(std::cerr) << std::endl;
 
341
                    /*if (!inter[i].second)
 
342
                        trace[j].add_interpolant(last);
 
343
                    else*/ {
 
344
                        auto res = stateForPredicate(inter[j].first);
 
345
                        some |= res.first;
 
346
//                        assert(inter[i].second || res.second == last);
 
347
                        some |= _states[last].add_edge(inter[i].second, res.second);
 
348
                        last = res.second;
 
349
                    }
 
350
                }
 
351
            }
 
352
            assert(added_terminal);
 
353
            return some;
 
354
        }
 
355
 
 
356
        std::ostream& TraceSet::print(std::ostream& out) const
 
357
        {
 
358
            out << "digraph graphname {\n";
 
359
            for (size_t i = 0; i < _states.size(); ++i) {
 
360
                auto& s = _states[i];
 
361
                out << "\tS" << i << " [label=\"";
 
362
                if (s.interpolant.is_true()) {
 
363
                    out << "TRUE";
 
364
                }
 
365
                else if (s.interpolant.is_false(_net.numberOfPlaces())) {
 
366
                    out << "FALSE";
 
367
                }
 
368
                else {
 
369
                    s.interpolant.print(out);
 
370
                }
 
371
                out << "\",shape=";
 
372
                auto lb = std::lower_bound(_initial.begin(), _initial.end(), i);
 
373
                if (lb != std::end(_initial) && *lb == i)
 
374
                    out << "box,color=green";
 
375
                else
 
376
                    out << "box";
 
377
                out << "];\n";
 
378
            }
 
379
            for (size_t i = 0; i < _states.size(); ++i) {
 
380
                auto& s = _states[i];
 
381
                for (auto& e : s.get_edges()) {
 
382
                    out << "\tS" << i << "_" << e.edge << " [label=\"" <<
 
383
                            (e.edge == 0 ? "Q" : std::to_string(e.edge - 1))
 
384
                            << "\",shape=diamond,style=dashed];\n";
 
385
                    out << "\tS" << i << " -> S" << i << "_" << e.edge << ";\n";
 
386
                    for (auto& t : e.to) {
 
387
                        out << "\tS" << i << "_" << e.edge << " -> S" << t << ";\n";
 
388
                    }
 
389
                }
 
390
            }
 
391
 
 
392
            out << "}\n";
 
393
            return out;
 
394
        }
 
395
    }
 
396
}
 
397