← Back to branch summary

~yrke/verifypn/github-automation

« back to all changes in this revision

Viewing changes to src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp

  • Committer: srba.jiri at gmail
  • Date: 2021-04-16 20:59:15 UTC
  • mfrom: (231.1.16 random-fix)
  • Revision ID: srba.jiri@gmail.com-20210416205915-8d22jkkj14aff05i
merged in lp:~tapaal-ltl/verifypn/random-fix adding LTL heuristic, fixing random search and adding partitioning to CPN unfodling

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp
1
 
/*
2
 
 * File:   InterestingTransitionVisitor.cpp.cc
3
 
 * Author: Nikolaj J. Ulrik <nikolaj@njulrik.dk>
4
 
 *
5
 
 * Created on 03/02/2021
 
1
/* Copyright (C) 2021  Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
 
2
 *                     Simon M. Virenfeldt <simon@simwir.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/>.
6
16
 */
7
17
 
8
18
#include "PetriEngine/Stubborn/InterestingTransitionVisitor.h"
9
19
 
10
20
namespace PetriEngine {
11
21
 
12
 
    void InterestingTransitionVisitor::_accept(const PQL::SimpleQuantifierCondition *element) {
 
22
    void InterestingTransitionVisitor::_accept(const PQL::SimpleQuantifierCondition *element)
 
23
    {
13
24
        (*element)[0]->visit(*this);
14
25
    }
15
26
 
16
 
    void InterestingTransitionVisitor::_accept(const PQL::UntilCondition *element) {
 
27
    void InterestingTransitionVisitor::_accept(const PQL::UntilCondition *element)
 
28
    {
17
29
        element->getCond1()->visit(*this);
18
30
        negate();
19
31
        element->getCond1()->visit(*this);
22
34
    }
23
35
 
24
36
 
25
 
    void InterestingTransitionVisitor::_accept(const PQL::AndCondition *element) {
 
37
    void InterestingTransitionVisitor::_accept(const PQL::AndCondition *element)
 
38
    {
26
39
        if (!negated) {               // and
27
40
            for (auto &c : *element) {
28
41
                if (!c->isSatisfied()) {
35
48
        }
36
49
    }
37
50
 
38
 
    void InterestingTransitionVisitor::_accept(const PQL::OrCondition *element) {
 
51
    void InterestingTransitionVisitor::_accept(const PQL::OrCondition *element)
 
52
    {
39
53
        if (!negated) {               // or
40
54
            for (auto &c : *element) c->visit(*this);
41
55
        } else {                    // and
48
62
        }
49
63
    }
50
64
 
51
 
    void InterestingTransitionVisitor::_accept(const PQL::CompareConjunction *element) {
 
65
    void InterestingTransitionVisitor::_accept(const PQL::CompareConjunction *element)
 
66
    {
52
67
 
53
68
        auto neg = negated != element->isNegated();
54
69
        int32_t cand = std::numeric_limits<int32_t>::max();
58
73
            if (c._lower == c._upper) {
59
74
                if (neg) {
60
75
                    if (val != c._lower) continue;
61
 
                    _stubborn.postsetOf(c._place, true);
62
 
                    _stubborn.presetOf(c._place, true);
 
76
                    _stubborn.postsetOf(c._place, closure);
 
77
                    _stubborn.presetOf(c._place, closure);
63
78
                } else {
64
79
                    if (val == c._lower) continue;
65
80
                    if (val > c._lower) {
85
100
                    }
86
101
                } else {
87
102
                    if (val >= c._lower && c._lower != 0) {
88
 
                        _stubborn.postsetOf(c._place, true);
 
103
                        _stubborn.postsetOf(c._place, closure);
89
104
                    }
90
105
 
91
106
                    if (val <= c._upper && c._upper != std::numeric_limits<uint32_t>::max()) {
92
 
                        _stubborn.presetOf(c._place, true);
 
107
                        _stubborn.presetOf(c._place, closure);
93
108
                    }
94
109
                }
95
110
            }
102
117
        }
103
118
        if (cand != std::numeric_limits<int32_t>::max()) {
104
119
            if (pre) {
105
 
                _stubborn.presetOf(cand, true);
 
120
                _stubborn.presetOf(cand, closure);
106
121
            } else if (!pre) {
107
 
                _stubborn.postsetOf(cand, true);
 
122
                _stubborn.postsetOf(cand, closure);
108
123
            }
109
124
        }
110
125
    }
111
126
 
112
 
    void InterestingTransitionVisitor::_accept(const PQL::EqualCondition *element) {
 
127
    void InterestingTransitionVisitor::_accept(const PQL::EqualCondition *element)
 
128
    {
113
129
        if (!negated) {               // equal
114
130
            if (element->getExpr1()->getEval() == element->getExpr2()->getEval()) { return; }
115
131
            if (element->getExpr1()->getEval() > element->getExpr2()->getEval()) {
128
144
        }
129
145
    }
130
146
 
131
 
    void InterestingTransitionVisitor::_accept(const PQL::NotEqualCondition *element) {
 
147
    void InterestingTransitionVisitor::_accept(const PQL::NotEqualCondition *element)
 
148
    {
132
149
        if (!negated) {               // not equal
133
150
            if (element->getExpr1()->getEval() != element->getExpr2()->getEval()) { return; }
134
151
            element->getExpr1()->visit(incr);
147
164
        }
148
165
    }
149
166
 
150
 
    void InterestingTransitionVisitor::_accept(const PQL::LessThanCondition *element) {
 
167
    void InterestingTransitionVisitor::_accept(const PQL::LessThanCondition *element)
 
168
    {
151
169
        if (!negated) {               // less than
152
170
            if (element->getExpr1()->getEval() < element->getExpr2()->getEval()) { return; }
153
171
            element->getExpr1()->visit(decr);
159
177
        }
160
178
    }
161
179
 
162
 
    void InterestingTransitionVisitor::_accept(const PQL::LessThanOrEqualCondition *element) {
 
180
    void InterestingTransitionVisitor::_accept(const PQL::LessThanOrEqualCondition *element)
 
181
    {
163
182
        if (!negated) {               // less than or equal
164
183
            if (element->getExpr1()->getEval() <= element->getExpr2()->getEval()) { return; }
165
184
            element->getExpr1()->visit(decr);
171
190
        }
172
191
    }
173
192
 
174
 
    void InterestingTransitionVisitor::_accept(const PQL::NotCondition *element) {
 
193
    void InterestingTransitionVisitor::_accept(const PQL::NotCondition *element)
 
194
    {
175
195
        negate();
176
196
        (*element)[0]->visit(*this);
177
197
        negate();
178
198
    }
179
199
 
180
 
    void InterestingTransitionVisitor::_accept(const PQL::BooleanCondition *element) {
 
200
    void InterestingTransitionVisitor::_accept(const PQL::BooleanCondition *element)
 
201
    {
181
202
        // Add nothing
182
203
    }
183
204
 
184
 
    void InterestingTransitionVisitor::_accept(const PQL::DeadlockCondition *element) {
 
205
    void InterestingTransitionVisitor::_accept(const PQL::DeadlockCondition *element)
 
206
    {
185
207
        if (!element->isSatisfied()) {
186
 
            _stubborn.postPresetOf(_stubborn.leastDependentEnabled(), true);
 
208
            _stubborn.postPresetOf(_stubborn.leastDependentEnabled(), closure);
187
209
        } // else add nothing
188
210
    }
189
211
 
190
212
    void
191
 
    InterestingTransitionVisitor::_accept(const PQL::UnfoldedUpperBoundsCondition *element) {
 
213
    InterestingTransitionVisitor::_accept(const PQL::UnfoldedUpperBoundsCondition *element)
 
214
    {
192
215
        for (auto &p : element->places())
193
216
            if (!p._maxed_out)
194
217
                _stubborn.presetOf(p._place);
195
218
    }
196
219
 
197
 
    void InterestingTransitionVisitor::_accept(const PQL::EFCondition *condition)
198
 
    {
199
 
        _accept((PetriEngine::PQL::SimpleQuantifierCondition*) condition);
200
 
    }
201
 
 
202
 
    void InterestingTransitionVisitor::_accept(const PQL::EGCondition *condition)
203
 
    {
204
 
        _accept((PetriEngine::PQL::SimpleQuantifierCondition*) condition);
205
 
    }
206
 
 
207
 
    void InterestingTransitionVisitor::_accept(const PQL::AGCondition *condition)
208
 
    {
209
 
        _accept((PetriEngine::PQL::SimpleQuantifierCondition*) condition);
210
 
    }
211
 
 
212
 
    void InterestingTransitionVisitor::_accept(const PQL::AFCondition *condition)
213
 
    {
214
 
        _accept((PetriEngine::PQL::SimpleQuantifierCondition*) condition);
215
 
    }
216
 
 
217
 
    void InterestingTransitionVisitor::_accept(const PQL::EXCondition *condition)
218
 
    {
219
 
        _accept((PetriEngine::PQL::SimpleQuantifierCondition*) condition);
220
 
    }
221
 
 
222
 
    void InterestingTransitionVisitor::_accept(const PQL::AXCondition *condition)
223
 
    {
224
 
        _accept((PetriEngine::PQL::SimpleQuantifierCondition*) condition);
225
 
    }
226
 
 
227
 
    void InterestingTransitionVisitor::_accept(const PQL::EUCondition *condition)
228
 
    {
229
 
        _accept((PetriEngine::PQL::SimpleQuantifierCondition*) condition);
230
 
    }
231
 
 
232
 
    void InterestingTransitionVisitor::_accept(const PQL::AUCondition *condition)
233
 
    {
234
 
        _accept((PetriEngine::PQL::SimpleQuantifierCondition*) condition);
235
 
    }
236
 
 
237
 
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::PlusExpr *element) {
238
 
        for(auto& i : element->places()) _stubborn.presetOf(i.first, true);
239
 
        for(auto& e : element->expressions()) e->visit(*this);
240
 
    }
241
 
 
242
 
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::PlusExpr *element) {
243
 
        for(auto& i : element->places()) _stubborn.postsetOf(i.first, true);
244
 
        for(auto& e : element->expressions()) e->visit(*this);
245
 
    }
246
 
 
247
 
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::SubtractExpr *element) {
 
220
    void InterestingTransitionVisitor::_accept(const PQL::GCondition *element)
 
221
    {
 
222
        negate();
 
223
        (*element)[0]->visit(*this);
 
224
        negate();
 
225
    }
 
226
 
 
227
    void InterestingTransitionVisitor::_accept(const PQL::FCondition *element)
 
228
    {
 
229
        (*element)[0]->visit(*this);
 
230
    }
 
231
 
 
232
    void InterestingTransitionVisitor::_accept(const PQL::EFCondition *condition) {
 
233
        _accept(static_cast<const PQL::SimpleQuantifierCondition*>(condition));
 
234
    }
 
235
 
 
236
    void InterestingTransitionVisitor::_accept(const PQL::EGCondition *condition) {
 
237
        _accept(static_cast<const PQL::SimpleQuantifierCondition*>(condition));
 
238
    }
 
239
 
 
240
    void InterestingTransitionVisitor::_accept(const PQL::AGCondition *condition) {
 
241
        _accept(static_cast<const PQL::SimpleQuantifierCondition*>(condition));
 
242
    }
 
243
 
 
244
    void InterestingTransitionVisitor::_accept(const PQL::AFCondition *condition) {
 
245
        _accept(static_cast<const PQL::SimpleQuantifierCondition*>(condition));
 
246
    }
 
247
 
 
248
    void InterestingTransitionVisitor::_accept(const PQL::EXCondition *condition) {
 
249
        _accept(static_cast<const PQL::SimpleQuantifierCondition*>(condition));
 
250
    }
 
251
 
 
252
    void InterestingTransitionVisitor::_accept(const PQL::AXCondition *condition) {
 
253
        _accept(static_cast<const PQL::SimpleQuantifierCondition*>(condition));
 
254
    }
 
255
 
 
256
    void InterestingTransitionVisitor::_accept(const PQL::ACondition *condition) {
 
257
        _accept(static_cast<const PQL::SimpleQuantifierCondition*>(condition));
 
258
    }
 
259
 
 
260
    void InterestingTransitionVisitor::_accept(const PQL::ECondition *condition) {
 
261
        _accept(static_cast<const PQL::SimpleQuantifierCondition*>(condition));
 
262
    }
 
263
 
 
264
    void InterestingTransitionVisitor::_accept(const PQL::XCondition *condition) {
 
265
        _accept(static_cast<const PQL::SimpleQuantifierCondition*>(condition));
 
266
    }
 
267
 
 
268
    void InterestingTransitionVisitor::_accept(const PQL::AUCondition *condition) {
 
269
        _accept(static_cast<const PQL::UntilCondition*>(condition));
 
270
    }
 
271
 
 
272
    void InterestingTransitionVisitor::_accept(const PQL::EUCondition *condition) {
 
273
        _accept(static_cast<const PQL::UntilCondition*>(condition));
 
274
    }
 
275
 
 
276
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::PlusExpr *element)
 
277
    {
 
278
        for (auto &i : element->places()) _stubborn.presetOf(i.first, closure);
 
279
        for (auto &e : element->expressions()) e->visit(*this);
 
280
    }
 
281
 
 
282
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::PlusExpr *element)
 
283
    {
 
284
        for (auto &i : element->places()) _stubborn.postsetOf(i.first, closure);
 
285
        for (auto &e : element->expressions()) e->visit(*this);
 
286
    }
 
287
 
 
288
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::SubtractExpr *element)
 
289
    {
248
290
        bool first = true;
249
 
        for(auto& e : element->expressions())
250
 
        {
251
 
            if(first)
 
291
        for (auto &e : element->expressions()) {
 
292
            if (first)
252
293
                e->visit(*this);
253
294
            else
254
295
                e->visit(*decr);
256
297
        }
257
298
    }
258
299
 
259
 
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::SubtractExpr *element) {
 
300
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::SubtractExpr *element)
 
301
    {
260
302
        bool first = true;
261
 
        for(auto& e : element->expressions())
262
 
        {
263
 
            if(first)
 
303
        for (auto &e : element->expressions()) {
 
304
            if (first)
264
305
                e->visit(*this);
265
306
            else
266
307
                e->visit(*incr);
268
309
        }
269
310
    }
270
311
 
271
 
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::MultiplyExpr *element) {
272
 
        if((element->places().size() + element->expressions().size()) == 1)
273
 
        {
274
 
            for(auto& i : element->places()) _stubborn.presetOf(i.first, true);
275
 
            for(auto& e : element->expressions()) e->visit(*this);
276
 
        }
277
 
        else
278
 
        {
279
 
            for(auto& i : element->places())
280
 
            {
281
 
                _stubborn.presetOf(i.first, true);
282
 
                _stubborn.postsetOf(i.first, true);
 
312
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::MultiplyExpr *element)
 
313
    {
 
314
        if ((element->places().size() + element->expressions().size()) == 1) {
 
315
            for (auto &i : element->places()) _stubborn.presetOf(i.first, closure);
 
316
            for (auto &e : element->expressions()) e->visit(*this);
 
317
        } else {
 
318
            for (auto &i : element->places()) {
 
319
                _stubborn.presetOf(i.first, closure);
 
320
                _stubborn.postsetOf(i.first, closure);
283
321
            }
284
 
            for(auto& e : element->expressions())
285
 
            {
 
322
            for (auto &e : element->expressions()) {
286
323
                e->visit(*this);
287
324
                e->visit(*decr);
288
325
            }
289
326
        }
290
327
    }
291
328
 
292
 
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::MultiplyExpr *element) {
293
 
        if((element->places().size() + element->expressions().size()) == 1)
294
 
        {
295
 
            for(auto& i : element->places()) _stubborn.postsetOf(i.first, true);
296
 
            for(auto& e : element->expressions()) e->visit(*this);
297
 
        }
298
 
        else
 
329
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::MultiplyExpr *element)
 
330
    {
 
331
        if ((element->places().size() + element->expressions().size()) == 1) {
 
332
            for (auto &i : element->places()) _stubborn.postsetOf(i.first, closure);
 
333
            for (auto &e : element->expressions()) e->visit(*this);
 
334
        } else
299
335
            element->visit(*incr);
300
336
    }
301
337
 
302
 
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::MinusExpr *element) {
303
 
        // TODO not implemented
304
 
    }
305
 
 
306
 
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::MinusExpr *element) {
307
 
        // TODO not implemented
308
 
    }
309
 
 
310
 
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::LiteralExpr *element) {
311
 
        // Add nothing
312
 
    }
313
 
 
314
 
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::LiteralExpr *element) {
315
 
        // Add nothing
316
 
    }
317
 
 
318
 
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::UnfoldedIdentifierExpr *element) {
319
 
        _stubborn.presetOf(element->offset(), true);
320
 
    }
321
 
 
322
 
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::UnfoldedIdentifierExpr *element) {
323
 
        _stubborn.postsetOf(element->offset(), true);
 
338
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::MinusExpr *element)
 
339
    {
 
340
        // TODO not implemented
 
341
    }
 
342
 
 
343
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::MinusExpr *element)
 
344
    {
 
345
        // TODO not implemented
 
346
    }
 
347
 
 
348
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::LiteralExpr *element)
 
349
    {
 
350
        // Add nothing
 
351
    }
 
352
 
 
353
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::LiteralExpr *element)
 
354
    {
 
355
        // Add nothing
 
356
    }
 
357
 
 
358
    void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::UnfoldedIdentifierExpr *element)
 
359
    {
 
360
        _stubborn.presetOf(element->offset(), closure);
 
361
    }
 
362
 
 
363
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::UnfoldedIdentifierExpr *element)
 
364
    {
 
365
        _stubborn.postsetOf(element->offset(), closure);
 
366
    }
 
367
 
 
368
    void InterestingLTLTransitionVisitor::_accept(const PQL::LessThanCondition *element)
 
369
    {
 
370
        negate_if_satisfied<PQL::LessThanCondition>(element);
 
371
    }
 
372
 
 
373
    void InterestingLTLTransitionVisitor::_accept(const PQL::LessThanOrEqualCondition *element)
 
374
    {
 
375
        negate_if_satisfied<PQL::LessThanOrEqualCondition>(element);
 
376
    }
 
377
 
 
378
    void InterestingLTLTransitionVisitor::_accept(const PQL::EqualCondition *element)
 
379
    {
 
380
        negate_if_satisfied<PQL::EqualCondition>(element);
 
381
    }
 
382
 
 
383
    void InterestingLTLTransitionVisitor::_accept(const PQL::NotEqualCondition *element)
 
384
    {
 
385
        negate_if_satisfied<PQL::NotEqualCondition>(element);
 
386
    }
 
387
 
 
388
    void InterestingLTLTransitionVisitor::_accept(const PQL::CompareConjunction *element)
 
389
    {
 
390
        negate_if_satisfied<PQL::CompareConjunction>(element);
 
391
    }
 
392
 
 
393
    template<typename Condition>
 
394
    void InterestingLTLTransitionVisitor::negate_if_satisfied(const Condition *element)
 
395
    {
 
396
        // TODO: There may be leftover information in isSatisfied that has not been updated in this marking. It is most like needed to evalAndSet the entire tree everytime instead of as now where it may gain a result in a node and therefore not explore the remaining children.
 
397
        auto isSatisfied = element->getSatisfied();
 
398
        assert(isSatisfied != PQL::Condition::RUNKNOWN);
 
399
        if ((isSatisfied == PQL::Condition::RTRUE) != negated) {
 
400
            negate();
 
401
            InterestingTransitionVisitor::_accept(element);
 
402
            negate();
 
403
        } else
 
404
            InterestingTransitionVisitor::_accept(element);
324
405
    }
325
406
 
326
407
}
 
 
b'\\ No newline at end of file'