← Back to branch summary

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

« back to all changes in this revision

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

  • 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:
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
 
6
 */
 
7
 
 
8
#include "PetriEngine/Stubborn/InterestingTransitionVisitor.h"
 
9
 
 
10
namespace PetriEngine {
 
11
 
 
12
    void InterestingTransitionVisitor::_accept(const PQL::SimpleQuantifierCondition *element) {
 
13
        (*element)[0]->visit(*this);
 
14
    }
 
15
 
 
16
    void InterestingTransitionVisitor::_accept(const PQL::UntilCondition *element) {
 
17
        element->getCond1()->visit(*this);
 
18
        negate();
 
19
        element->getCond1()->visit(*this);
 
20
        negate();
 
21
        element->getCond2()->visit(*this);
 
22
    }
 
23
 
 
24
 
 
25
    void InterestingTransitionVisitor::_accept(const PQL::AndCondition *element) {
 
26
        if (!negated) {               // and
 
27
            for (auto &c : *element) {
 
28
                if (!c->isSatisfied()) {
 
29
                    c->visit(*this);
 
30
                    break;
 
31
                }
 
32
            }
 
33
        } else {                    // or
 
34
            for (auto &c : *element) c->visit(*this);
 
35
        }
 
36
    }
 
37
 
 
38
    void InterestingTransitionVisitor::_accept(const PQL::OrCondition *element) {
 
39
        if (!negated) {               // or
 
40
            for (auto &c : *element) c->visit(*this);
 
41
        } else {                    // and
 
42
            for (auto &c : *element) {
 
43
                if (c->isSatisfied()) {
 
44
                    c->visit(*this);
 
45
                    break;
 
46
                }
 
47
            }
 
48
        }
 
49
    }
 
50
 
 
51
    void InterestingTransitionVisitor::_accept(const PQL::CompareConjunction *element) {
 
52
 
 
53
        auto neg = negated != element->isNegated();
 
54
        int32_t cand = std::numeric_limits<int32_t>::max();
 
55
        bool pre = false;
 
56
        for (auto &c : *element) {
 
57
            auto val = _stubborn.getParent()[c._place];
 
58
            if (c._lower == c._upper) {
 
59
                if (neg) {
 
60
                    if (val != c._lower) continue;
 
61
                    _stubborn.postsetOf(c._place, true);
 
62
                    _stubborn.presetOf(c._place, true);
 
63
                } else {
 
64
                    if (val == c._lower) continue;
 
65
                    if (val > c._lower) {
 
66
                        cand = c._place;
 
67
                        pre = false;
 
68
                    } else {
 
69
                        cand = c._place;
 
70
                        pre = true;
 
71
                    }
 
72
                }
 
73
            } else {
 
74
                if (!neg) {
 
75
                    if (val < c._lower && c._lower != 0) {
 
76
                        assert(!neg);
 
77
                        cand = c._place;
 
78
                        pre = true;
 
79
                    }
 
80
 
 
81
                    if (val > c._upper && c._upper != std::numeric_limits<uint32_t>::max()) {
 
82
                        assert(!neg);
 
83
                        cand = c._place;
 
84
                        pre = false;
 
85
                    }
 
86
                } else {
 
87
                    if (val >= c._lower && c._lower != 0) {
 
88
                        _stubborn.postsetOf(c._place, true);
 
89
                    }
 
90
 
 
91
                    if (val <= c._upper && c._upper != std::numeric_limits<uint32_t>::max()) {
 
92
                        _stubborn.presetOf(c._place, true);
 
93
                    }
 
94
                }
 
95
            }
 
96
            if (cand != std::numeric_limits<int32_t>::max()) {
 
97
                if (pre && _stubborn.seenPre(cand))
 
98
                    return;
 
99
                else if (!pre && _stubborn.seenPost(cand))
 
100
                    return;
 
101
            }
 
102
        }
 
103
        if (cand != std::numeric_limits<int32_t>::max()) {
 
104
            if (pre) {
 
105
                _stubborn.presetOf(cand, true);
 
106
            } else if (!pre) {
 
107
                _stubborn.postsetOf(cand, true);
 
108
            }
 
109
        }
 
110
    }
 
111
 
 
112
    void InterestingTransitionVisitor::_accept(const PQL::EqualCondition *element) {
 
113
        if (!negated) {               // equal
 
114
            if (element->getExpr1()->getEval() == element->getExpr2()->getEval()) { return; }
 
115
            if (element->getExpr1()->getEval() > element->getExpr2()->getEval()) {
 
116
                element->getExpr1()->visit(decr);
 
117
                element->getExpr2()->visit(incr);
 
118
            } else {
 
119
                element->getExpr1()->visit(incr);
 
120
                element->getExpr2()->visit(decr);
 
121
            }
 
122
        } else {                    // not equal
 
123
            if (element->getExpr1()->getEval() != element->getExpr2()->getEval()) { return; }
 
124
            element->getExpr1()->visit(incr);
 
125
            element->getExpr1()->visit(decr);
 
126
            element->getExpr2()->visit(incr);
 
127
            element->getExpr2()->visit(decr);
 
128
        }
 
129
    }
 
130
 
 
131
    void InterestingTransitionVisitor::_accept(const PQL::NotEqualCondition *element) {
 
132
        if (!negated) {               // not equal
 
133
            if (element->getExpr1()->getEval() != element->getExpr2()->getEval()) { return; }
 
134
            element->getExpr1()->visit(incr);
 
135
            element->getExpr1()->visit(decr);
 
136
            element->getExpr2()->visit(incr);
 
137
            element->getExpr2()->visit(decr);
 
138
        } else {                    // equal
 
139
            if (element->getExpr1()->getEval() == element->getExpr2()->getEval()) { return; }
 
140
            if (element->getExpr1()->getEval() > element->getExpr2()->getEval()) {
 
141
                element->getExpr1()->visit(decr);
 
142
                element->getExpr2()->visit(incr);
 
143
            } else {
 
144
                element->getExpr1()->visit(incr);
 
145
                element->getExpr2()->visit(decr);
 
146
            }
 
147
        }
 
148
    }
 
149
 
 
150
    void InterestingTransitionVisitor::_accept(const PQL::LessThanCondition *element) {
 
151
        if (!negated) {               // less than
 
152
            if (element->getExpr1()->getEval() < element->getExpr2()->getEval()) { return; }
 
153
            element->getExpr1()->visit(decr);
 
154
            element->getExpr2()->visit(incr);
 
155
        } else {                    // greater than or equal
 
156
            if (element->getExpr1()->getEval() >= element->getExpr2()->getEval()) { return; }
 
157
            element->getExpr1()->visit(incr);
 
158
            element->getExpr2()->visit(decr);
 
159
        }
 
160
    }
 
161
 
 
162
    void InterestingTransitionVisitor::_accept(const PQL::LessThanOrEqualCondition *element) {
 
163
        if (!negated) {               // less than or equal
 
164
            if (element->getExpr1()->getEval() <= element->getExpr2()->getEval()) { return; }
 
165
            element->getExpr1()->visit(decr);
 
166
            element->getExpr2()->visit(incr);
 
167
        } else {                    // greater than
 
168
            if (element->getExpr1()->getEval() > element->getExpr2()->getEval()) { return; }
 
169
            element->getExpr1()->visit(incr);
 
170
            element->getExpr2()->visit(decr);
 
171
        }
 
172
    }
 
173
 
 
174
    void InterestingTransitionVisitor::_accept(const PQL::NotCondition *element) {
 
175
        negate();
 
176
        (*element)[0]->visit(*this);
 
177
        negate();
 
178
    }
 
179
 
 
180
    void InterestingTransitionVisitor::_accept(const PQL::BooleanCondition *element) {
 
181
        // Add nothing
 
182
    }
 
183
 
 
184
    void InterestingTransitionVisitor::_accept(const PQL::DeadlockCondition *element) {
 
185
        if (!element->isSatisfied()) {
 
186
            _stubborn.postPresetOf(_stubborn.leastDependentEnabled(), true);
 
187
        } // else add nothing
 
188
    }
 
189
 
 
190
    void
 
191
    InterestingTransitionVisitor::_accept(const PQL::UnfoldedUpperBoundsCondition *element) {
 
192
        for (auto &p : element->places())
 
193
            if (!p._maxed_out)
 
194
                _stubborn.presetOf(p._place);
 
195
    }
 
196
 
 
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) {
 
248
        bool first = true;
 
249
        for(auto& e : element->expressions())
 
250
        {
 
251
            if(first)
 
252
                e->visit(*this);
 
253
            else
 
254
                e->visit(*decr);
 
255
            first = false;
 
256
        }
 
257
    }
 
258
 
 
259
    void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::SubtractExpr *element) {
 
260
        bool first = true;
 
261
        for(auto& e : element->expressions())
 
262
        {
 
263
            if(first)
 
264
                e->visit(*this);
 
265
            else
 
266
                e->visit(*incr);
 
267
            first = false;
 
268
        }
 
269
    }
 
270
 
 
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);
 
283
            }
 
284
            for(auto& e : element->expressions())
 
285
            {
 
286
                e->visit(*this);
 
287
                e->visit(*decr);
 
288
            }
 
289
        }
 
290
    }
 
291
 
 
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
 
299
            element->visit(*incr);
 
300
    }
 
301
 
 
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);
 
324
    }
 
325
 
 
326
}
 
 
b'\\ No newline at end of file'