← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/PetriEngine/PQL/QueryPrinter.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/QueryPrinter.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
 
 
18
#include "PetriEngine/PQL/QueryPrinter.h"
 
19
 
 
20
namespace PetriEngine {
 
21
    namespace PQL {
 
22
        void QueryPrinter::_accept(const NotCondition *element) {
 
23
            os << "(not ";
 
24
            element->operator[](0)->visit(*this);
 
25
            os << ")";
 
26
        }
 
27
 
 
28
 
 
29
        void QueryPrinter::_accept(const LogicalCondition *element, const std::string &op) {
 
30
            os << "(";
 
31
            (*element)[0]->visit(*this);
 
32
            for (size_t i = 1; i < element->operands(); ++i) {
 
33
                os << " " << op << " ";
 
34
                (*element)[i]->visit(*this);
 
35
            }
 
36
            os << ")";
 
37
        }
 
38
 
 
39
        void QueryPrinter::_accept(const CompareCondition *element, const std::string &op) {
 
40
            os << "(";
 
41
            element->getExpr1()->visit(*this);
 
42
            os << " " << op << " ";
 
43
            element->getExpr2()->visit(*this);
 
44
            os << ")";
 
45
        }
 
46
 
 
47
        void QueryPrinter::_accept(const AndCondition *element) {
 
48
            _accept(element, "and");
 
49
        }
 
50
 
 
51
        void QueryPrinter::_accept(const OrCondition *element) {
 
52
            _accept(element, "or");
 
53
        }
 
54
 
 
55
        void QueryPrinter::_accept(const LessThanCondition *element) {
 
56
            _accept(element, "<");
 
57
        }
 
58
 
 
59
        void QueryPrinter::_accept(const LessThanOrEqualCondition *element) {
 
60
            _accept(element, "<=");
 
61
        }
 
62
 
 
63
        void QueryPrinter::_accept(const EqualCondition *element) {
 
64
            _accept(element, "==");
 
65
        }
 
66
 
 
67
        void QueryPrinter::_accept(const NotEqualCondition *element) {
 
68
            _accept(element, "!=");
 
69
        }
 
70
 
 
71
        void QueryPrinter::_accept(const DeadlockCondition *element) {
 
72
            os << "deadlock";
 
73
        }
 
74
 
 
75
        void QueryPrinter::_accept(const CompareConjunction *element) {
 
76
            os << "(";
 
77
            if (element->isNegated()) os << "not";
 
78
            bool first = true;
 
79
            for (const auto &cons : *element) {
 
80
                if (!first) os << " and ";
 
81
                if (cons._lower != 0)
 
82
                    os << "(" << cons._lower << " <= " << cons._name << ")";
 
83
                if (cons._lower != 0 && cons._upper != std::numeric_limits<uint32_t>::max())
 
84
                    os << " and ";
 
85
                if (cons._upper != std::numeric_limits<uint32_t>::max())
 
86
                    os << "(" << cons._upper << " >= " << cons._name << ")";
 
87
                first = false;
 
88
            }
 
89
            os << ")";
 
90
        }
 
91
 
 
92
        void QueryPrinter::_accept(const UnfoldedUpperBoundsCondition *element) {
 
93
            os << "bounds (";
 
94
            auto places = element->places();
 
95
            for (size_t i = 0; i < places.size(); ++i) {
 
96
                if (i != 0) os << ", ";
 
97
                os << places[i]._name;
 
98
            }
 
99
            os << ")";
 
100
        }
 
101
 
 
102
        void QueryPrinter::_accept(const EFCondition *condition) {
 
103
            os << "EF ";
 
104
            (*condition)[0]->visit(*this);
 
105
        }
 
106
 
 
107
        void QueryPrinter::_accept(const EGCondition *condition) {
 
108
            os << "EG ";
 
109
            (*condition)[0]->visit(*this);
 
110
        }
 
111
 
 
112
        void QueryPrinter::_accept(const AGCondition *condition) {
 
113
            os << "AG ";
 
114
            (*condition)[0]->visit(*this);
 
115
        }
 
116
 
 
117
        void QueryPrinter::_accept(const AFCondition *condition) {
 
118
            os << "AF ";
 
119
            (*condition)[0]->visit(*this);
 
120
        }
 
121
 
 
122
        void QueryPrinter::_accept(const EXCondition *condition) {
 
123
            os << "AF ";
 
124
            (*condition)[0]->visit(*this);
 
125
        }
 
126
 
 
127
        void QueryPrinter::_accept(const AXCondition *condition) {
 
128
            os << "AX ";
 
129
            (*condition)[0]->visit(*this);
 
130
        }
 
131
 
 
132
        void QueryPrinter::_accept(const EUCondition *condition) {
 
133
            os << "E ";
 
134
            _accept((UntilCondition*) condition);
 
135
        }
 
136
 
 
137
        void QueryPrinter::_accept(const AUCondition *condition) {
 
138
            os << "A ";
 
139
            _accept((UntilCondition*) condition);
 
140
        }
 
141
 
 
142
        void QueryPrinter::_accept(const ACondition *condition) {
 
143
            os << "A ";
 
144
            (*condition)[0]->visit(*this);
 
145
        }
 
146
 
 
147
        void QueryPrinter::_accept(const ECondition *condition) {
 
148
            os << "E ";
 
149
            (*condition)[0]->visit(*this);
 
150
        }
 
151
 
 
152
        void QueryPrinter::_accept(const GCondition *condition) {
 
153
            os << "G ";
 
154
            (*condition)[0]->visit(*this);
 
155
        }
 
156
 
 
157
        void QueryPrinter::_accept(const FCondition *condition) {
 
158
            os << "F ";
 
159
            (*condition)[0]->visit(*this);
 
160
        }
 
161
 
 
162
        void QueryPrinter::_accept(const XCondition *condition) {
 
163
            os << "X ";
 
164
            (*condition)[0]->visit(*this);
 
165
        }
 
166
 
 
167
        void QueryPrinter::_accept(const UntilCondition *condition) {
 
168
            os << "(";
 
169
            condition->getCond1()->visit(*this);
 
170
            os << " U ";
 
171
            condition->getCond2()->visit(*this);
 
172
            os << ")";
 
173
        }
 
174
 
 
175
        void QueryPrinter::_accept(const UnfoldedFireableCondition *element) {
 
176
            os << "is-fireable(" << element->getName() << ")";
 
177
        }
 
178
 
 
179
        void QueryPrinter::_accept(const FireableCondition *element) {
 
180
            os << "is-fireable(" << element->getName() << ")";
 
181
 
 
182
        }
 
183
 
 
184
        void QueryPrinter::_accept(const UpperBoundsCondition *element) {
 
185
            os << "bounds (";
 
186
            auto places = element->getPlaces();
 
187
            for(size_t i = 0; i < places.size(); ++i)
 
188
            {
 
189
                if(i != 0) os << ", ";
 
190
                os << places[i];
 
191
            }
 
192
            os << ")";
 
193
        }
 
194
 
 
195
        void QueryPrinter::_accept(const LivenessCondition *element) {
 
196
            const Condition_ptr& cond = element->getCompiled();
 
197
            if (cond) {
 
198
                cond->visit(*this);
 
199
            }
 
200
            else {
 
201
                os << "liveness";
 
202
            }
 
203
        }
 
204
 
 
205
        void QueryPrinter::_accept(const KSafeCondition *element) {
 
206
            if (element->getCompiled()) {
 
207
                element->getCompiled()->visit(*this);
 
208
            }
 
209
            else {
 
210
                os << "k-safe(";
 
211
                element->getBound()->visit(*this);
 
212
                os << ")";
 
213
            }
 
214
        }
 
215
 
 
216
        void QueryPrinter::_accept(const QuasiLivenessCondition *element) {
 
217
            const Condition_ptr& cond = element->getCompiled();
 
218
            if (cond) {
 
219
                cond->visit(*this);
 
220
            }
 
221
            else {
 
222
                os << "liveness";
 
223
            }
 
224
        }
 
225
 
 
226
        void QueryPrinter::_accept(const StableMarkingCondition *element) {
 
227
            const Condition_ptr& cond = element->getCompiled();
 
228
            if (cond) {
 
229
                cond->visit(*this);
 
230
            }
 
231
            else {
 
232
                os << "stable-marking";
 
233
            }
 
234
        }
 
235
 
 
236
        void QueryPrinter::_accept(const BooleanCondition *element) {
 
237
            os << (element->value ? "true" : "false");
 
238
        }
 
239
 
 
240
        void QueryPrinter::_accept(const UnfoldedIdentifierExpr *element) {
 
241
            os << element->name();
 
242
        }
 
243
 
 
244
        void QueryPrinter::_accept(const LiteralExpr *element) {
 
245
            os << element->value();
 
246
        }
 
247
 
 
248
        void QueryPrinter::_accept(const CommutativeExpr *element, const std::string &op) {
 
249
            os << "(" << element->constant();
 
250
            for (const auto &id: element->places()) {
 
251
                os << " " << op << " " << id.second;
 
252
            }
 
253
            for (const auto &expr : element->expressions()) {
 
254
                os << " " << op << " ";
 
255
                expr->visit(*this);
 
256
            }
 
257
            os << ")";
 
258
        }
 
259
 
 
260
        void QueryPrinter::_accept(const NaryExpr *element, const std::string &op) {
 
261
            os << "(";
 
262
            (*element)[0]->visit(*this);
 
263
            for(size_t i = 1; i < element->operands(); ++i)
 
264
            {
 
265
                os << " " << op << " ";
 
266
                (*element)[i]->visit(*this);
 
267
            }
 
268
            os << ")";
 
269
        }
 
270
 
 
271
        void QueryPrinter::_accept(const PlusExpr *element) {
 
272
            _accept((const CommutativeExpr *)element, "+");
 
273
        }
 
274
 
 
275
        void QueryPrinter::_accept(const MultiplyExpr *element) {
 
276
            _accept((const CommutativeExpr*)element, "*");
 
277
        }
 
278
 
 
279
        void QueryPrinter::_accept(const MinusExpr *element) {
 
280
            os << "-";
 
281
            (*element)[0]->visit(*this);
 
282
        }
 
283
 
 
284
        void QueryPrinter::_accept(const SubtractExpr *element) {
 
285
            _accept((const NaryExpr *)element, "-");
 
286
        }
 
287
 
 
288
        void QueryPrinter::_accept(const IdentifierExpr *element) {
 
289
            os << element->name();
 
290
        }
 
291
    }
 
292
}
 
 
b'\\ No newline at end of file'