← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/PetriEngine/PQL/CTLVisitor.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/PQL/CTLVisitor.cpp
 
1
/* Copyright (C) 2020  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/>.
 
16
 */
 
17
#include "PetriEngine/PQL/CTLVisitor.h"
 
18
 
 
19
#include <memory>
 
20
 
 
21
namespace PetriEngine::PQL {
 
22
    void IsCTLVisitor::_accept(const NotCondition *element) {
 
23
        (*element)[0]->visit(*this);
 
24
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
25
            isCTL = false;
 
26
    }
 
27
 
 
28
    void IsCTLVisitor::_accept(const LogicalCondition *element) {
 
29
        for (size_t i = 0; i < element->operands(); i++){
 
30
            (*element)[i]->visit(*this);
 
31
            if (_cur_type != CTLSyntaxType::BOOLEAN){
 
32
                isCTL = false;
 
33
                break;
 
34
            }
 
35
        }
 
36
    }
 
37
 
 
38
    void IsCTLVisitor::_accept(const AndCondition *element) {
 
39
        _accept((const LogicalCondition *) element);
 
40
    }
 
41
 
 
42
    void IsCTLVisitor::_accept(const OrCondition *element) {
 
43
        _accept((const LogicalCondition *) element);
 
44
    }
 
45
 
 
46
    void IsCTLVisitor::_accept(const CompareCondition *element) {
 
47
        //We are an atom. No need to check children as they are the same as CTL*
 
48
        _cur_type = CTLSyntaxType::BOOLEAN;
 
49
    }
 
50
 
 
51
    void IsCTLVisitor::_accept(const LessThanCondition *element) {
 
52
        _accept((const CompareCondition *) element);
 
53
    }
 
54
 
 
55
    void IsCTLVisitor::_accept(const LessThanOrEqualCondition *element) {
 
56
        _accept((const CompareCondition *) element);
 
57
    }
 
58
 
 
59
    void IsCTLVisitor::_accept(const EqualCondition *element) {
 
60
        _accept((const CompareCondition *) element);
 
61
    }
 
62
 
 
63
    void IsCTLVisitor::_accept(const NotEqualCondition *element) {
 
64
        _accept((const CompareCondition *) element);
 
65
    }
 
66
 
 
67
    void IsCTLVisitor::_accept(const DeadlockCondition *element) {
 
68
        _cur_type = CTLSyntaxType::BOOLEAN;
 
69
    }
 
70
 
 
71
    void IsCTLVisitor::_accept(const CompareConjunction *element) {
 
72
        _cur_type = CTLSyntaxType::BOOLEAN;
 
73
    }
 
74
 
 
75
    void IsCTLVisitor::_accept(const UnfoldedUpperBoundsCondition *element) {
 
76
        _cur_type = CTLSyntaxType::BOOLEAN;
 
77
    }
 
78
 
 
79
    void IsCTLVisitor::_accept(const EFCondition *condition) {
 
80
        (*condition)[0]->visit(*this);
 
81
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
82
            isCTL = false;
 
83
    }
 
84
 
 
85
    void IsCTLVisitor::_accept(const EGCondition *condition) {
 
86
        (*condition)[0]->visit(*this);
 
87
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
88
            isCTL = false;
 
89
    }
 
90
 
 
91
    void IsCTLVisitor::_accept(const AGCondition *condition) {
 
92
        (*condition)[0]->visit(*this);
 
93
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
94
            isCTL = false;
 
95
    }
 
96
 
 
97
    void IsCTLVisitor::_accept(const AFCondition *condition) {
 
98
        (*condition)[0]->visit(*this);
 
99
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
100
            isCTL = false;
 
101
    }
 
102
 
 
103
    void IsCTLVisitor::_accept(const EXCondition *condition) {
 
104
        (*condition)[0]->visit(*this);
 
105
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
106
            isCTL = false;
 
107
    }
 
108
 
 
109
    void IsCTLVisitor::_accept(const AXCondition *condition) {
 
110
        (*condition)[0]->visit(*this);
 
111
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
112
            isCTL = false;
 
113
    }
 
114
 
 
115
    void IsCTLVisitor::_accept(const EUCondition *condition) {
 
116
        (*condition)[0]->visit(*this);
 
117
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
118
            isCTL = false;
 
119
    }
 
120
 
 
121
    void IsCTLVisitor::_accept(const AUCondition *condition) {
 
122
        (*condition)[0]->visit(*this);
 
123
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
124
            isCTL = false;
 
125
    }
 
126
 
 
127
    void IsCTLVisitor::_accept(const ACondition *condition) {
 
128
        (*condition)[0]->visit(*this);
 
129
        if (_cur_type != CTLSyntaxType::PATH)
 
130
            isCTL = false;
 
131
        _cur_type = CTLSyntaxType::BOOLEAN;
 
132
    }
 
133
 
 
134
    void IsCTLVisitor::_accept(const ECondition *condition) {
 
135
        (*condition)[0]->visit(*this);
 
136
        if (_cur_type != CTLSyntaxType::PATH)
 
137
            isCTL = false;
 
138
        _cur_type = CTLSyntaxType::BOOLEAN;
 
139
    }
 
140
 
 
141
    void IsCTLVisitor::_accept(const GCondition *condition) {
 
142
        (*condition)[0]->visit(*this);
 
143
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
144
            isCTL = false;
 
145
        _cur_type = CTLSyntaxType::PATH;
 
146
    }
 
147
 
 
148
    void IsCTLVisitor::_accept(const FCondition *condition) {
 
149
        (*condition)[0]->visit(*this);
 
150
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
151
            isCTL = false;
 
152
        _cur_type = CTLSyntaxType::PATH;
 
153
    }
 
154
 
 
155
    void IsCTLVisitor::_accept(const XCondition *condition) {
 
156
        (*condition)[0]->visit(*this);
 
157
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
158
            isCTL = false;
 
159
        _cur_type = CTLSyntaxType::PATH;
 
160
    }
 
161
 
 
162
    void IsCTLVisitor::_accept(const UntilCondition *condition) {
 
163
        (*condition)[0]->visit(*this);
 
164
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
165
            isCTL = false;
 
166
        (*condition)[1]->visit(*this);
 
167
        if (_cur_type != CTLSyntaxType::BOOLEAN)
 
168
            isCTL = false;
 
169
        _cur_type = CTLSyntaxType::PATH;
 
170
    }
 
171
 
 
172
    void IsCTLVisitor::_accept(const UnfoldedFireableCondition *element) {
 
173
        _cur_type = CTLSyntaxType::BOOLEAN;
 
174
    }
 
175
 
 
176
    void IsCTLVisitor::_accept(const FireableCondition *element) {
 
177
        _cur_type = CTLSyntaxType::BOOLEAN;
 
178
    }
 
179
 
 
180
    void IsCTLVisitor::_accept(const UpperBoundsCondition *element) {
 
181
        _cur_type = CTLSyntaxType::BOOLEAN;
 
182
    }
 
183
 
 
184
    void IsCTLVisitor::_accept(const LivenessCondition *element) {
 
185
        _cur_type = CTLSyntaxType::BOOLEAN;
 
186
    }
 
187
 
 
188
    void IsCTLVisitor::_accept(const KSafeCondition *element) {
 
189
        _cur_type = CTLSyntaxType::BOOLEAN;
 
190
    }
 
191
 
 
192
    void IsCTLVisitor::_accept(const QuasiLivenessCondition *element) {
 
193
        _cur_type = CTLSyntaxType::BOOLEAN;
 
194
    }
 
195
 
 
196
    void IsCTLVisitor::_accept(const StableMarkingCondition *element) {
 
197
        _cur_type = CTLSyntaxType::BOOLEAN;
 
198
    }
 
199
 
 
200
    void IsCTLVisitor::_accept(const BooleanCondition *element) {
 
201
        _cur_type = CTLSyntaxType::BOOLEAN;
 
202
    }
 
203
 
 
204
    void IsCTLVisitor::_accept(const UnfoldedIdentifierExpr *element) {
 
205
        _cur_type = CTLSyntaxType::BOOLEAN;
 
206
    }
 
207
 
 
208
    void IsCTLVisitor::_accept(const LiteralExpr *element) {
 
209
        _cur_type = CTLSyntaxType::BOOLEAN;
 
210
    }
 
211
 
 
212
    void IsCTLVisitor::_accept(const PlusExpr *element) {
 
213
        _cur_type = CTLSyntaxType::BOOLEAN;
 
214
    }
 
215
 
 
216
    void IsCTLVisitor::_accept(const MultiplyExpr *element) {
 
217
        _cur_type = CTLSyntaxType::BOOLEAN;
 
218
    }
 
219
 
 
220
    void IsCTLVisitor::_accept(const MinusExpr *element) {
 
221
        _cur_type = CTLSyntaxType::BOOLEAN;
 
222
    }
 
223
 
 
224
    void IsCTLVisitor::_accept(const SubtractExpr *element) {
 
225
        _cur_type = CTLSyntaxType::BOOLEAN;
 
226
    }
 
227
 
 
228
    void IsCTLVisitor::_accept(const IdentifierExpr *element) {
 
229
        _cur_type = CTLSyntaxType::BOOLEAN;
 
230
    }
 
231
 
 
232
 
 
233
    void AsCTL::_accept(const NotCondition *element) {
 
234
        (*element)[0]->visit(*this);
 
235
        _ctl_query = std::make_shared<NotCondition>(_ctl_query);
 
236
    }
 
237
 
 
238
    template<typename T>
 
239
    void AsCTL::_acceptNary(const T *element) {
 
240
        std::vector<Condition_ptr> children;
 
241
        for (auto operand : *element){
 
242
            operand->visit(*this);
 
243
            children.push_back(_ctl_query);
 
244
        }
 
245
        _ctl_query = std::make_shared<T>(children);
 
246
    }
 
247
 
 
248
    void AsCTL::_accept(const AndCondition *element) {
 
249
        AsCTL::_acceptNary(element);
 
250
    }
 
251
 
 
252
    void AsCTL::_accept(const OrCondition *element) {
 
253
        AsCTL::_acceptNary(element);
 
254
    }
 
255
 
 
256
    template<typename T>
 
257
    std::shared_ptr<T> AsCTL::copy_compare_condition(const T *element) {
 
258
        // we copy of sharedptr for now, but this is not safe!
 
259
        // copy_narry_expr needs fixing.
 
260
        return std::make_shared<T>((*element)[0], (*element)[1]);
 
261
    }
 
262
 
 
263
    void AsCTL::_accept(const LessThanCondition *element) {
 
264
        _ctl_query = copy_compare_condition(element);
 
265
    }
 
266
 
 
267
    void AsCTL::_accept(const LessThanOrEqualCondition *element) {
 
268
        _ctl_query = copy_compare_condition(element);
 
269
    }
 
270
 
 
271
    void AsCTL::_accept(const EqualCondition *element) {
 
272
        _ctl_query = copy_compare_condition(element);
 
273
    }
 
274
 
 
275
    void AsCTL::_accept(const NotEqualCondition *element) {
 
276
        _ctl_query = copy_compare_condition(element);
 
277
    }
 
278
 
 
279
    void AsCTL::_accept(const DeadlockCondition *element) {
 
280
        _ctl_query = std::make_shared<DeadlockCondition>();
 
281
    }
 
282
 
 
283
    void AsCTL::_accept(const CompareConjunction *element) {
 
284
        _ctl_query = std::make_shared<CompareConjunction>(*element);
 
285
    }
 
286
 
 
287
    void AsCTL::_accept(const UnfoldedUpperBoundsCondition *element) {
 
288
        _ctl_query = std::make_shared<UnfoldedUpperBoundsCondition>(*element);
 
289
    }
 
290
 
 
291
    void AsCTL::_accept(const EFCondition *condition) {
 
292
        (*condition)[0]->visit(*this);
 
293
        _ctl_query = std::make_shared<EFCondition>(_ctl_query);
 
294
    }
 
295
 
 
296
    void AsCTL::_accept(const EGCondition *condition) {
 
297
        (*condition)[0]->visit(*this);
 
298
        _ctl_query = std::make_shared<EGCondition>(_ctl_query);
 
299
    }
 
300
 
 
301
    void AsCTL::_accept(const AGCondition *condition) {
 
302
        (*condition)[0]->visit(*this);
 
303
        _ctl_query = std::make_shared<AGCondition>(_ctl_query);
 
304
    }
 
305
 
 
306
    void AsCTL::_accept(const AFCondition *condition) {
 
307
        (*condition)[0]->visit(*this);
 
308
        _ctl_query = std::make_shared<AFCondition>(_ctl_query);
 
309
    }
 
310
 
 
311
    void AsCTL::_accept(const EXCondition *condition) {
 
312
        (*condition)[0]->visit(*this);
 
313
        _ctl_query = std::make_shared<EXCondition>(_ctl_query);
 
314
    }
 
315
 
 
316
    void AsCTL::_accept(const AXCondition *condition) {
 
317
        (*condition)[0]->visit(*this);
 
318
        _ctl_query = std::make_shared<AXCondition>(_ctl_query);
 
319
    }
 
320
 
 
321
    void AsCTL::_accept(const EUCondition *condition) {
 
322
        (*condition)[0]->visit(*this);
 
323
        auto first = _ctl_query;
 
324
        (*condition)[1]->visit(*this);
 
325
        _ctl_query = std::make_shared<EUCondition>(first, _ctl_query);
 
326
    }
 
327
 
 
328
    void AsCTL::_accept(const AUCondition *condition) {
 
329
        (*condition)[0]->visit(*this);
 
330
        auto first = _ctl_query;
 
331
        (*condition)[1]->visit(*this);
 
332
        _ctl_query = std::make_shared<AUCondition>(first, _ctl_query);
 
333
    }
 
334
 
 
335
    void AsCTL::_accept(const ACondition *condition) {
 
336
        auto child = dynamic_cast<QuantifierCondition*>((*condition)[0].get());
 
337
        switch (child->getPath()) {
 
338
            case Path::G:
 
339
                (*child)[0]->visit(*this);
 
340
                _ctl_query = std::make_shared<AGCondition>(_ctl_query);
 
341
                break;
 
342
            case Path::X:
 
343
                (*child)[0]->visit(*this);
 
344
                _ctl_query = std::make_shared<AXCondition>(_ctl_query);
 
345
                break;
 
346
            case Path::F:
 
347
                (*child)[0]->visit(*this);
 
348
                _ctl_query = std::make_shared<AFCondition>(_ctl_query);
 
349
                break;
 
350
            case Path::U: {
 
351
                (*child)[0]->visit(*this);
 
352
                auto first = _ctl_query;
 
353
                (*child)[1]->visit(*this);
 
354
                _ctl_query = std::make_shared<AUCondition>(first, _ctl_query);
 
355
                break;
 
356
            }
 
357
            case Path::pError:
 
358
                assert(false);
 
359
                _ctl_query = nullptr;
 
360
                break;
 
361
        }
 
362
    }
 
363
 
 
364
    void AsCTL::_accept(const ECondition *condition) {
 
365
        auto child = dynamic_cast<QuantifierCondition*>((*condition)[0].get());
 
366
        switch (child->getPath()) {
 
367
            case Path::G:
 
368
                (*child)[0]->visit(*this);
 
369
                _ctl_query = std::make_shared<EGCondition>(_ctl_query);
 
370
                break;
 
371
            case Path::X:
 
372
                (*child)[0]->visit(*this);
 
373
                _ctl_query = std::make_shared<EXCondition>(_ctl_query);
 
374
                break;
 
375
            case Path::F:
 
376
                (*child)[0]->visit(*this);
 
377
                _ctl_query = std::make_shared<EFCondition>(_ctl_query);
 
378
                break;
 
379
            case Path::U: {
 
380
                (*child)[0]->visit(*this);
 
381
                auto first = _ctl_query;
 
382
                (*child)[1]->visit(*this);
 
383
                _ctl_query = std::make_shared<EUCondition>(first, _ctl_query);
 
384
                break;
 
385
            }
 
386
            case Path::pError:
 
387
                assert(false);
 
388
                _ctl_query = nullptr;
 
389
                break;
 
390
        }
 
391
    }
 
392
 
 
393
    void AsCTL::_accept(const GCondition *condition) {
 
394
        std::cerr << "Direct call to path quantifier in AsCTL GCondition" << std::endl;
 
395
        assert(false);
 
396
        _ctl_query = nullptr;
 
397
    }
 
398
 
 
399
    void AsCTL::_accept(const FCondition *condition) {
 
400
        std::cerr << "Direct call to path quantifier in AsCTL FCondition" << std::endl;
 
401
        assert(false);
 
402
        _ctl_query = nullptr;
 
403
    }
 
404
 
 
405
    void AsCTL::_accept(const XCondition *condition) {
 
406
        std::cerr << "Direct call to path quantifier in AsCTL XCondition" << std::endl;
 
407
        assert(false);
 
408
        _ctl_query = nullptr;
 
409
    }
 
410
 
 
411
    void AsCTL::_accept(const UntilCondition *condition) {
 
412
        std::cerr << "Direct call to path quantifier in AsCTL UntilCondition" << std::endl;
 
413
        assert(false);
 
414
        _ctl_query = nullptr;
 
415
    }
 
416
 
 
417
    void AsCTL::_accept(const UnfoldedFireableCondition *element) {
 
418
        _ctl_query = std::make_shared<UnfoldedFireableCondition>(*element);
 
419
    }
 
420
 
 
421
    template<typename T>
 
422
    Condition_ptr copy_condition(const T* el)
 
423
    {
 
424
        return std::make_shared<T>(*el);
 
425
    }
 
426
 
 
427
    void AsCTL::_accept(const FireableCondition *element) {
 
428
        _ctl_query = copy_condition(element);
 
429
    }
 
430
 
 
431
    void AsCTL::_accept(const UpperBoundsCondition *element) {
 
432
        _ctl_query = copy_condition(element);
 
433
    }
 
434
 
 
435
    void AsCTL::_accept(const LivenessCondition *element) {
 
436
        _ctl_query = copy_condition(element);
 
437
    }
 
438
 
 
439
    void AsCTL::_accept(const KSafeCondition *element) {
 
440
        _ctl_query = copy_condition(element);
 
441
    }
 
442
 
 
443
    void AsCTL::_accept(const QuasiLivenessCondition *element) {
 
444
        _ctl_query = copy_condition(element);
 
445
    }
 
446
 
 
447
    void AsCTL::_accept(const StableMarkingCondition *element) {
 
448
        _ctl_query = copy_condition(element);
 
449
    }
 
450
 
 
451
    void AsCTL::_accept(const BooleanCondition *element) {
 
452
        _ctl_query = element->value ? BooleanCondition::TRUE_CONSTANT : BooleanCondition::FALSE_CONSTANT;
 
453
    }
 
454
 
 
455
    template<typename T>
 
456
    Expr_ptr AsCTL::copy_narry_expr(const T* el)
 
457
    {
 
458
        assert(false);
 
459
        // TODO: fix
 
460
        return nullptr;
 
461
    }
 
462
 
 
463
    void AsCTL::_accept(const PlusExpr *element) {
 
464
        _expression = copy_narry_expr(element);
 
465
    }
 
466
 
 
467
    void AsCTL::_accept(const MultiplyExpr *element) {
 
468
        _expression = copy_narry_expr(element);
 
469
    }
 
470
 
 
471
    void AsCTL::_accept(const SubtractExpr *element) {
 
472
        _expression = copy_narry_expr(element);
 
473
    }
 
474
 
 
475
    void AsCTL::_accept(const MinusExpr *element) {
 
476
        (*element)[0]->visit(*this);
 
477
        _expression = std::make_shared<MinusExpr>(_expression);
 
478
    }
 
479
 
 
480
    void AsCTL::_accept(const LiteralExpr *element) {
 
481
        _expression = std::make_shared<LiteralExpr>(element->value());
 
482
    }
 
483
 
 
484
    void AsCTL::_accept(const IdentifierExpr *element) {
 
485
        _expression = std::make_shared<IdentifierExpr>(*element);
 
486
    }
 
487
 
 
488
    void AsCTL::_accept(const UnfoldedIdentifierExpr *element) {
 
489
        _expression = std::make_shared<UnfoldedIdentifierExpr>(*element);
 
490
    }
 
491
 
 
492
}
 
 
b'\\ No newline at end of file'