Merge lp:~ragusaen/verifypn/verifypn into lp:verifypn

Proposed by Rasmus Tollund
Status: Merged
Merged at revision: 253
Proposed branch: lp:~ragusaen/verifypn/verifypn
Merge into: lp:verifypn
Diff against target: 2104 lines (+1036/-165) (has conflicts)
10 files modified
include/PetriEngine/PQL/BinaryPrinter.h (+71/-0)
include/PetriEngine/PQL/Expressions.h (+15/-62)
include/PetriEngine/PQL/PQL.h (+0/-4)
include/PetriEngine/PQL/Visitor.h (+118/-90)
include/PetriEngine/PQL/XMLPrinter.h (+119/-0)
src/PetriEngine/PQL/BinaryPrinter.cpp (+173/-0)
src/PetriEngine/PQL/CMakeLists.txt (+1/-1)
src/PetriEngine/PQL/Expressions.cpp (+132/-5)
src/PetriEngine/PQL/XMLPrinter.cpp (+399/-0)
src/VerifyPN.cpp (+8/-3)
Text conflict in src/PetriEngine/PQL/Expressions.cpp
To merge this branch: bzr merge lp:~ragusaen/verifypn/verifypn
Reviewer Review Type Date Requested Status
Peter Gjøl Jensen Needs Fixing
Review via email: mp+409484@code.launchpad.net

Description of the change

Changed XML printer for queries to use visitor pattern.

To post a comment you must log in.
Revision history for this message
Peter Gjøl Jensen (peter-gjoel) :
review: Needs Fixing
lp:~ragusaen/verifypn/verifypn updated
253. By Rasmus Tollund

Added options for tab size and printing new lines

254. By Rasmus Tollund

Added a binary printer with visitor pattern. I changed the Visitor class to support overriding base class _accepts. This way the classes will default to the base class's _accept definition.

255. By Rasmus Tollund

Removed toBinary and toXML from expressions.[h/cpp]. Also added a couple of _accept for functions that were defined in the .h file.

256. By Rasmus Tollund

Removed .h file from add_libraries

257. By Rasmus Tollund

Fixed bug with until condition

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== added file 'include/PetriEngine/PQL/BinaryPrinter.h'
2--- include/PetriEngine/PQL/BinaryPrinter.h 1970-01-01 00:00:00 +0000
3+++ include/PetriEngine/PQL/BinaryPrinter.h 2021-10-18 11:40:53 +0000
4@@ -0,0 +1,71 @@
5+/* Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
6+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
7+ * Lars Kærlund Østergaard <larsko@gmail.com>,
8+ * Peter Gjøl Jensen <root@petergjoel.dk>,
9+ * Rasmus Tollund <rtollu18@student.aau.dk>
10+ *
11+ * This program is free software: you can redistribute it and/or modify
12+ * it under the terms of the GNU General Public License as published by
13+ * the Free Software Foundation, either version 3 of the License, or
14+ * (at your option) any later version.
15+ *
16+ * This program is distributed in the hope that it will be useful,
17+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
18+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
19+ * GNU General Public License for more details.
20+ *
21+ * You should have received a copy of the GNU General Public License
22+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
23+ */
24+
25+#ifndef VERIFYPN_BINARYPRINTER_H
26+#define VERIFYPN_BINARYPRINTER_H
27+
28+#include "Visitor.h"
29+
30+namespace PetriEngine::PQL {
31+ class BinaryPrinter : public Visitor {
32+ public:
33+ explicit BinaryPrinter(std::ostream& os) :
34+ os(os) {}
35+
36+ protected:
37+ std::ostream& os;
38+
39+ void _accept(const NotCondition *element) override;
40+
41+ void _accept(const DeadlockCondition *element) override;
42+
43+ void _accept(const CompareConjunction *element) override;
44+
45+ void _accept(const UnfoldedUpperBoundsCondition *element) override;
46+
47+ void _accept(const UntilCondition *condition) override;
48+
49+ void _accept(const BooleanCondition *element) override;
50+
51+ void _accept(const UnfoldedIdentifierExpr *element) override;
52+
53+ void _accept(const LiteralExpr *element) override;
54+
55+ void _accept(const MinusExpr *element) override;
56+
57+ void _accept(const SubtractExpr *element) override;
58+
59+ void _accept(const CommutativeExpr *element) override;
60+
61+ void _accept(const SimpleQuantifierCondition *condition) override;
62+
63+ void _accept(const LogicalCondition *condition) override;
64+
65+ void _accept(const CompareCondition *condition) override;
66+
67+ void _accept(const IdentifierExpr *condition) override;
68+
69+ void _accept(const ShallowCondition *condition) override;
70+
71+ };
72+}
73+
74+
75+#endif //VERIFYPN_BINARYPRINTER_H
76
77=== modified file 'include/PetriEngine/PQL/Expressions.h'
78--- include/PetriEngine/PQL/Expressions.h 2021-08-12 12:35:54 +0000
79+++ include/PetriEngine/PQL/Expressions.h 2021-10-18 11:40:53 +0000
80@@ -62,9 +62,10 @@
81 const Expr_ptr &operator[](size_t i) const {
82 return _exprs[i];
83 }
84+ virtual std::string op() const = 0;
85+
86 protected:
87 virtual int apply(int v1, int v2) const = 0;
88- virtual std::string op() const = 0;
89 std::vector<Expr_ptr> _exprs;
90 virtual int32_t preOp(const EvaluationContext& context) const;
91 };
92@@ -78,7 +79,7 @@
93 friend CompareCondition;
94 virtual void analyze(AnalysisContext& context) override;
95 int evaluate(const EvaluationContext& context) override;
96- void toBinary(std::ostream&) const override;
97+ void visit(Visitor&) const override;
98 int formulaSize() const override{
99 size_t sum = _ids.size();
100 for(auto& e : _exprs) sum += e->formulaSize();
101@@ -87,6 +88,7 @@
102 bool placeFree() const override;
103 auto constant() const { return _constant; }
104 auto& places() const { return _ids; }
105+
106 protected:
107 CommutativeExpr(int constant): _constant(constant) {};
108 void init(std::vector<Expr_ptr>&& exprs);
109@@ -104,7 +106,6 @@
110
111 Expr::Types type() const override;
112 Member constraint(SimplificationContext& context) const override;
113- void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
114 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
115 bool tk = false;
116
117@@ -125,11 +126,9 @@
118 }
119 Expr::Types type() const override;
120 Member constraint(SimplificationContext& context) const override;
121- void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
122 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
123
124
125- void toBinary(std::ostream&) const override;
126 void visit(Visitor& visitor) const override;
127 protected:
128 int apply(int v1, int v2) const override;
129@@ -144,7 +143,6 @@
130 MultiplyExpr(std::vector<Expr_ptr>&& exprs);
131 Expr::Types type() const override;
132 Member constraint(SimplificationContext& context) const override;
133- void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
134 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
135
136
137@@ -166,9 +164,7 @@
138 int evaluate(const EvaluationContext& context) override;
139 Expr::Types type() const override;
140 Member constraint(SimplificationContext& context) const override;
141- void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
142 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
143- void toBinary(std::ostream&) const override;
144
145 void visit(Visitor& visitor) const override;
146 int formulaSize() const override{
147@@ -190,9 +186,7 @@
148 void analyze(AnalysisContext& context) override;
149 int evaluate(const EvaluationContext& context) override;
150 Expr::Types type() const override;
151- void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
152 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
153- void toBinary(std::ostream&) const override;
154
155 void visit(Visitor& visitor) const override;
156 int formulaSize() const override{
157@@ -220,9 +214,6 @@
158 if(_compiled) return _compiled->type();
159 return Expr::IdentifierExpr;
160 }
161- void toXML(std::ostream& os, uint32_t tabs, bool tokencount = false) const override {
162- _compiled->toXML(os, tabs, tokencount);
163- }
164 void toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
165
166 int formulaSize() const override {
167@@ -238,15 +229,12 @@
168 return _compiled->constraint(context);
169 }
170
171- void toBinary(std::ostream& s) const override {
172- _compiled->toBinary(s);
173- }
174 void visit(Visitor& visitor) const override;
175
176 [[nodiscard]] const std::string &name() const {
177 return _name;
178 }
179-
180+
181 [[nodiscard]] const Expr_ptr &compiled() const {
182 return _compiled;
183 }
184@@ -265,15 +253,13 @@
185
186 UnfoldedIdentifierExpr(const std::string& name) : UnfoldedIdentifierExpr(name, -1) {
187 }
188-
189+
190 UnfoldedIdentifierExpr(const UnfoldedIdentifierExpr&) = default;
191
192 void analyze(AnalysisContext& context) override;
193 int evaluate(const EvaluationContext& context) override;
194 Expr::Types type() const override;
195- void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
196 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
197- void toBinary(std::ostream&) const override;
198 int formulaSize() const override{
199 return 1;
200 }
201@@ -305,17 +291,12 @@
202 { return _compiled->distance(context); }
203 void toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const override
204 { _compiled->toTAPAALQuery(out, context); }
205- void toBinary(std::ostream& out) const override
206- { return _compiled->toBinary(out); }
207 Retval simplify(SimplificationContext& context) const override
208 { return _compiled->simplify(context); }
209 Condition_ptr prepareForReachability(bool negated) const override
210 { return _compiled->prepareForReachability(negated); }
211 bool isReachability(uint32_t depth) const override
212 { return _compiled->isReachability(depth); }
213-
214- void toXML(std::ostream& out, uint32_t tabs) const override
215- { _compiled->toXML(out, tabs); }
216 void toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const override{
217 }
218
219@@ -383,8 +364,6 @@
220 bool isReachability(uint32_t depth) const override;
221 Condition_ptr prepareForReachability(bool negated) const override;
222 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
223- void toXML(std::ostream&, uint32_t tabs) const override;
224- void toBinary(std::ostream&) const override;
225 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
226
227
228@@ -427,7 +406,7 @@
229 Result evaluate(const EvaluationContext& context) override;
230 Result evalAndSet(const EvaluationContext& context) override;
231 void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
232- void toBinary(std::ostream& out) const override;
233+ void visit(Visitor&) const override;
234
235
236 virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
237@@ -452,7 +431,6 @@
238 bool isReachability(uint32_t depth) const override;
239 Condition_ptr prepareForReachability(bool negated) const override;
240 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
241- void toXML(std::ostream&, uint32_t tabs) const override;
242 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
243 Quantifier getQuantifier() const override { return Quantifier::E; }
244 Path getPath() const override { return Path::pError; }
245@@ -481,7 +459,6 @@
246 bool isReachability(uint32_t depth) const override;
247 Condition_ptr prepareForReachability(bool negated) const override;
248 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
249- void toXML(std::ostream&, uint32_t tabs) const override;
250 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
251 Quantifier getQuantifier() const override { return Quantifier::A; }
252 Path getPath() const override { return Path::pError; }
253@@ -521,7 +498,6 @@
254
255 Retval simplify(SimplificationContext &context) const override;
256
257- void toXML(std::ostream &, uint32_t tabs) const override;
258 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
259
260 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
261@@ -563,7 +539,6 @@
262 assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
263 }
264 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
265- void toXML(std::ostream&, uint32_t tabs) const override;
266 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
267 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
268 Path getPath() const override { return Path::F; }
269@@ -591,7 +566,6 @@
270 }
271 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
272 Retval simplify(SimplificationContext& context) const override;
273- void toXML(std::ostream&, uint32_t tabs) const override;
274 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
275 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
276 Path getPath() const override { return Path::X; }
277@@ -613,7 +587,6 @@
278 bool isReachability(uint32_t depth) const override;
279 Condition_ptr prepareForReachability(bool negated) const override;
280 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
281- void toXML(std::ostream&, uint32_t tabs) const override;
282 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
283 Quantifier getQuantifier() const override { return Quantifier::E; }
284 Path getPath() const override { return Path::X; }
285@@ -634,7 +607,6 @@
286 bool isReachability(uint32_t depth) const override;
287 Condition_ptr prepareForReachability(bool negated) const override;
288 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
289- void toXML(std::ostream&, uint32_t tabs) const override;
290 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
291 Quantifier getQuantifier() const override { return Quantifier::E; }
292 Path getPath() const override { return Path::G; }
293@@ -656,7 +628,6 @@
294 bool isReachability(uint32_t depth) const override;
295 Condition_ptr prepareForReachability(bool negated) const override;
296 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
297- void toXML(std::ostream&, uint32_t tabs) const override;
298 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
299 Quantifier getQuantifier() const override { return Quantifier::E; }
300 Path getPath() const override { return Path::F; }
301@@ -676,7 +647,6 @@
302 bool isReachability(uint32_t depth) const override;
303 Condition_ptr prepareForReachability(bool negated) const override;
304 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
305- void toXML(std::ostream&, uint32_t tabs) const override;
306 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
307 Quantifier getQuantifier() const override { return Quantifier::A; }
308 Path getPath() const override { return Path::X; }
309@@ -696,7 +666,6 @@
310 bool isReachability(uint32_t depth) const override;
311 Condition_ptr prepareForReachability(bool negated) const override;
312 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
313- void toXML(std::ostream&, uint32_t tabs) const override;
314 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
315 Quantifier getQuantifier() const override { return Quantifier::A; }
316 Path getPath() const override { return Path::G; }
317@@ -716,7 +685,6 @@
318 bool isReachability(uint32_t depth) const override;
319 Condition_ptr prepareForReachability(bool negated) const override;
320 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
321- void toXML(std::ostream&, uint32_t tabs) const override;
322 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
323 Quantifier getQuantifier() const override { return Quantifier::A; }
324 Path getPath() const override { return Path::F; }
325@@ -744,7 +712,6 @@
326 void analyze(AnalysisContext& context) override;
327 Result evaluate(const EvaluationContext& context) override;
328 void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
329- void toBinary(std::ostream& out) const override;
330 bool isReachability(uint32_t depth) const override;
331 Condition_ptr prepareForReachability(bool negated) const override;
332
333@@ -758,12 +725,11 @@
334
335 [[nodiscard]] const Condition_ptr& getCond1() const { return (*this)[0]; }
336 [[nodiscard]] const Condition_ptr& getCond2() const { return (*this)[1]; }
337-
338+
339 Retval simplify(SimplificationContext& context) const override;
340 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
341 void visit(Visitor&) const override;
342 void visit(MutatingVisitor&) override;
343- void toXML(std::ostream&, uint32_t tabs) const override;
344 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
345 uint32_t distance(DistanceContext& context) const override { return (*this)[1]->distance(context); }
346 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
347@@ -785,7 +751,6 @@
348 void visit(MutatingVisitor&) override;
349 uint32_t distance(DistanceContext& context) const override;
350 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
351- void toXML(std::ostream&, uint32_t tabs) const override;
352 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
353
354 private:
355@@ -800,7 +765,6 @@
356 void visit(Visitor&) const override;
357 void visit(MutatingVisitor&) override;
358 uint32_t distance(DistanceContext& context) const override;
359- void toXML(std::ostream&, uint32_t tabs) const override;
360 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
361 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
362 virtual bool isLoopSensitive() const override { return true; }
363@@ -819,7 +783,6 @@
364 std::string getName() const {
365 return _name;
366 }
367- void toXML(std::ostream& out, uint32_t tabs) const override;
368 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
369 protected:
370 void _analyze(AnalysisContext& context) override;
371@@ -859,7 +822,7 @@
372
373 void analyze(AnalysisContext& context) override;
374
375- void toBinary(std::ostream& out) const override;
376+ void visit(Visitor&) const override;
377 void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
378 bool isReachability(uint32_t depth) const override;
379 Condition_ptr prepareForReachability(bool negated) const override;
380@@ -916,7 +879,6 @@
381 Result evalAndSet(const EvaluationContext& context) override;
382 void visit(Visitor&) const override;
383 void visit(MutatingVisitor&) override;
384- void toXML(std::ostream&, uint32_t tabs) const override;
385 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
386 Quantifier getQuantifier() const override { return Quantifier::AND; }
387 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
388@@ -941,7 +903,6 @@
389 Result evalAndSet(const EvaluationContext& context) override;
390 void visit(Visitor&) const override;
391 void visit(MutatingVisitor&) override;
392- void toXML(std::ostream&, uint32_t tabs) const override;
393 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
394
395 Quantifier getQuantifier() const override { return Quantifier::OR; }
396@@ -1024,12 +985,10 @@
397 void analyze(AnalysisContext& context) override;
398 uint32_t distance(DistanceContext& context) const override;
399 void toTAPAALQuery(std::ostream& stream,TAPAALConditionExportContext& context) const override;
400- void toBinary(std::ostream& out) const override;
401 bool isReachability(uint32_t depth) const override { return depth > 0; };
402 Condition_ptr prepareForReachability(bool negated) const override;
403 CTLType getQueryType() const override { return CTLType::LOPERATOR; }
404 Path getPath() const override { return Path::pError; }
405- virtual void toXML(std::ostream& stream, uint32_t tabs) const override;
406 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
407 Retval simplify(SimplificationContext& context) const override;
408 Result evaluate(const EvaluationContext& context) override;
409@@ -1071,7 +1030,7 @@
410 Result evaluate(const EvaluationContext& context) override;
411 Result evalAndSet(const EvaluationContext& context) override;
412 void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
413- void toBinary(std::ostream& out) const override;
414+ void visit(Visitor&) const override;
415 bool isReachability(uint32_t depth) const override;
416 Condition_ptr prepareForReachability(bool negated) const override;
417 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
418@@ -1090,6 +1049,8 @@
419
420 [[nodiscard]] const Expr_ptr &getExpr2() const { return _expr2; }
421
422+ virtual std::string op() const = 0;
423+
424 protected:
425 uint32_t _distance(DistanceContext& c,
426 std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
427@@ -1098,7 +1059,6 @@
428 }
429 private:
430 virtual bool apply(int v1, int v2) const = 0;
431- virtual std::string op() const = 0;
432 /** Operator when exported to TAPAAL */
433 virtual std::string opTAPAAL() const = 0;
434 /** Swapped operator when exported to TAPAAL, e.g. operator when operands are swapped */
435@@ -1119,7 +1079,6 @@
436
437 using CompareCondition::CompareCondition;
438 Retval simplify(SimplificationContext& context) const override;
439- void toXML(std::ostream&, uint32_t tabs) const override;
440 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
441
442 uint32_t distance(DistanceContext& context) const override;
443@@ -1140,7 +1099,6 @@
444 using CompareCondition::CompareCondition;
445 void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
446 Retval simplify(SimplificationContext& context) const override;
447- void toXML(std::ostream&, uint32_t tabs) const override;
448 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
449
450
451@@ -1161,7 +1119,6 @@
452
453 using CompareCondition::CompareCondition;
454 Retval simplify(SimplificationContext& context) const override;
455- void toXML(std::ostream&, uint32_t tabs) const override;
456 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
457
458 uint32_t distance(DistanceContext& context) const override;
459@@ -1181,7 +1138,6 @@
460
461 using CompareCondition::CompareCondition;
462 Retval simplify(SimplificationContext& context) const override;
463- void toXML(std::ostream&, uint32_t tabs) const override;
464 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
465
466 uint32_t distance(DistanceContext& context) const override;
467@@ -1223,8 +1179,6 @@
468 bool isReachability(uint32_t depth) const override;
469 Condition_ptr prepareForReachability(bool negated) const override;
470 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
471- void toXML(std::ostream&, uint32_t tabs) const override;
472- void toBinary(std::ostream&) const override;
473 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
474
475 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
476@@ -1256,8 +1210,6 @@
477 bool isReachability(uint32_t depth) const override;
478 Condition_ptr prepareForReachability(bool negated) const override;
479 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
480- void toXML(std::ostream&, uint32_t tabs) const override;
481- void toBinary(std::ostream&) const override;
482 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
483
484 static Condition_ptr DEADLOCK;
485@@ -1385,12 +1337,10 @@
486 void visit(MutatingVisitor&) override;
487 uint32_t distance(DistanceContext& context) const override;
488 void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
489- void toBinary(std::ostream&) const override;
490 Retval simplify(SimplificationContext& context) const override;
491 bool isReachability(uint32_t depth) const override;
492 Condition_ptr prepareForReachability(bool negated) const override;
493 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
494- void toXML(std::ostream&, uint32_t tabs) const override;
495 void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
496
497 Quantifier getQuantifier() const override { return Quantifier::UPPERBOUNDS; }
498@@ -1410,6 +1360,9 @@
499
500 const std::vector<place_t>& places() const { return _places; }
501
502+ double getMax() const { return _max; }
503+ double getOffset() const { return _offset; }
504+
505 private:
506 std::vector<place_t> _places;
507 size_t _bound = 0;
508
509=== modified file 'include/PetriEngine/PQL/PQL.h'
510--- include/PetriEngine/PQL/PQL.h 2021-06-01 08:40:18 +0000
511+++ include/PetriEngine/PQL/PQL.h 2021-10-18 11:40:53 +0000
512@@ -118,8 +118,6 @@
513 /** Construct left/right side of equations used in query simplification */
514 virtual Simplification::Member constraint(SimplificationContext& context) const = 0;
515 /** Output the expression as it currently is to a file in XML */
516- virtual void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const = 0;
517- virtual void toBinary(std::ostream&) const = 0;
518 virtual void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const = 0;
519
520 /** Count size of the entire formula in number of nodes */
521@@ -231,9 +229,7 @@
522 [[nodiscard]] virtual std::shared_ptr<Condition> pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated = false, bool initrw = true) = 0;
523
524 /** Output the condition as it currently is to a file in XML */
525- virtual void toXML(std::ostream&, uint32_t tabs) const = 0;
526 virtual void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const = 0;
527- virtual void toBinary(std::ostream& out) const = 0;
528
529 /** Checks if the condition is trivially true */
530 [[nodiscard]] bool isTriviallyTrue();
531
532=== modified file 'include/PetriEngine/PQL/Visitor.h'
533--- include/PetriEngine/PQL/Visitor.h 2021-04-29 07:47:52 +0000
534+++ include/PetriEngine/PQL/Visitor.h 2021-10-18 11:40:53 +0000
535@@ -30,101 +30,119 @@
536
537 protected:
538 virtual void _accept(const NotCondition* element) = 0;
539- virtual void _accept(const AndCondition* element) = 0;
540- virtual void _accept(const OrCondition* element) = 0;
541- virtual void _accept(const LessThanCondition* element) = 0;
542- virtual void _accept(const LessThanOrEqualCondition* element) = 0;
543- virtual void _accept(const EqualCondition* element) = 0;
544- virtual void _accept(const NotEqualCondition* element) = 0;
545+
546+ virtual void _accept(const AndCondition* element) {
547+ element->LogicalCondition::visit(*this);
548+ }
549+
550+ virtual void _accept(const OrCondition* element) {
551+ element->LogicalCondition::visit(*this);
552+ }
553+
554+ virtual void _accept(const LessThanCondition* element) {
555+ element->CompareCondition::visit(*this);
556+ }
557+
558+ virtual void _accept(const LessThanOrEqualCondition* element) {
559+ element->CompareCondition::visit(*this);
560+ }
561+
562+ virtual void _accept(const EqualCondition* element) {
563+ element->CompareCondition::visit(*this);
564+ }
565+
566+ virtual void _accept(const NotEqualCondition* element) {
567+ element->CompareCondition::visit(*this);
568+ }
569
570 virtual void _accept(const DeadlockCondition* element) = 0;
571 virtual void _accept(const CompareConjunction* element) = 0;
572 virtual void _accept(const UnfoldedUpperBoundsCondition* element) = 0;
573
574+ // Super classes, the default implementation of subclasses is to call these
575+ virtual void _accept(const CommutativeExpr *element) {
576+ assert(false);
577+ std::cerr << "No accept for CommutativeExpr (may be called from subclass)" << std::endl;
578+ exit(0);
579+ }
580+
581+ virtual void _accept(const SimpleQuantifierCondition *element) {
582+ assert(false);
583+ std::cerr << "No accept for SimpleQuantifierCondition (may be called from subclass)" << std::endl;
584+ exit(0);
585+ }
586+
587+ virtual void _accept(const LogicalCondition *element) {
588+ assert(false);
589+ std::cerr << "No accept for LogicalCondition (may be called from subclass)" << std::endl;
590+ exit(0);
591+ }
592+
593+ virtual void _accept(const CompareCondition *element) {
594+ assert(false);
595+ std::cerr << "No accept for CompareCondition (may be called from subclass)" << std::endl;
596+ exit(0);
597+ }
598+
599+ virtual void _accept(const UntilCondition *element) {
600+ assert(false);
601+ std::cerr << "No accept for UntilCondition (may be called from subclass)" << std::endl;
602+ exit(0);
603+ }
604+
605+
606 // Quantifiers, most uses of the visitor will not use the quantifiers - so we give a default implementation.
607 // default behaviour is error
608- virtual void _accept(const EFCondition *) {
609- assert(false);
610- std::cerr << "No accept for EFCondition" << std::endl;
611- exit(0);
612- };
613-
614- virtual void _accept(const EGCondition *) {
615- assert(false);
616- std::cerr << "No accept for EGCondition" << std::endl;
617- exit(0);
618- };
619-
620- virtual void _accept(const AGCondition *) {
621- assert(false);
622- std::cerr << "No accept for AGCondition" << std::endl;
623- exit(0);
624- };
625-
626- virtual void _accept(const AFCondition *) {
627- assert(false);
628- std::cerr << "No accept for AFCondition" << std::endl;
629- exit(0);
630- };
631-
632- virtual void _accept(const EXCondition *) {
633- assert(false);
634- std::cerr << "No accept for EXCondition" << std::endl;
635- exit(0);
636- };
637-
638- virtual void _accept(const AXCondition *) {
639- assert(false);
640- std::cerr << "No accept for AXCondition" << std::endl;
641- exit(0);
642- };
643-
644- virtual void _accept(const EUCondition *) {
645- assert(false);
646- std::cerr << "No accept for EUCondition" << std::endl;
647- exit(0);
648- };
649-
650- virtual void _accept(const AUCondition *) {
651- assert(false);
652- std::cerr << "No accept for AUCondition" << std::endl;
653- exit(0);
654- };
655-
656- virtual void _accept(const ACondition *) {
657- assert(false);
658- std::cerr << "No accept for ACondition" << std::endl;
659- exit(0);
660- };
661-
662- virtual void _accept(const ECondition *) {
663- assert(false);
664- std::cerr << "No accept for ECondition" << std::endl;
665- exit(0);
666- };
667-
668- virtual void _accept(const GCondition *) {
669- assert(false);
670- std::cerr << "No accept for GCondition" << std::endl;
671- exit(0);
672- };
673-
674- virtual void _accept(const FCondition *) {
675- assert(false);
676- std::cerr << "No accept for FCondition" << std::endl;
677- exit(0);
678- };
679-
680- virtual void _accept(const XCondition *) {
681- assert(false);
682- std::cerr << "No accept for XCondition" << std::endl;
683- exit(0);
684- };
685-
686- virtual void _accept(const UntilCondition *) {
687- assert(false);
688- std::cerr << "No accept for UntilCondition" << std::endl;
689- exit(0);
690+ virtual void _accept(const EFCondition *condition) {
691+ condition->SimpleQuantifierCondition::visit(*this);
692+ };
693+
694+ virtual void _accept(const EGCondition *condition) {
695+ condition->SimpleQuantifierCondition::visit(*this);
696+ };
697+
698+ virtual void _accept(const AGCondition *condition) {
699+ condition->SimpleQuantifierCondition::visit(*this);
700+ };
701+
702+ virtual void _accept(const AFCondition *condition) {
703+ condition->SimpleQuantifierCondition::visit(*this);
704+ };
705+
706+ virtual void _accept(const EXCondition *condition) {
707+ condition->SimpleQuantifierCondition::visit(*this);
708+ };
709+
710+ virtual void _accept(const AXCondition *condition) {
711+ condition->SimpleQuantifierCondition::visit(*this);
712+ };
713+
714+ virtual void _accept(const EUCondition *condition) {
715+ condition->UntilCondition::visit(*this);
716+ };
717+
718+ virtual void _accept(const AUCondition *condition) {
719+ condition->UntilCondition::visit(*this);
720+ };
721+
722+ virtual void _accept(const ACondition *condition) {
723+ condition->SimpleQuantifierCondition::visit(*this);
724+ };
725+
726+ virtual void _accept(const ECondition *condition) {
727+ condition->SimpleQuantifierCondition::visit(*this);
728+ };
729+
730+ virtual void _accept(const GCondition *condition) {
731+ condition->SimpleQuantifierCondition::visit(*this);
732+ };
733+
734+ virtual void _accept(const FCondition *condition) {
735+ condition->SimpleQuantifierCondition::visit(*this);
736+ };
737+
738+ virtual void _accept(const XCondition *condition) {
739+ condition->SimpleQuantifierCondition::visit(*this);
740 };
741
742 // shallow elements, neither of these should exist in a compiled expression
743@@ -176,14 +194,24 @@
744 exit(0);
745 };
746
747+ virtual void _accept(const ShallowCondition *element) {
748+ assert(false);
749+ std::cerr << "No accept for BooleanCondition" << std::endl;
750+ exit(0);
751+ }
752+
753 // Expression
754 virtual void _accept(const UnfoldedIdentifierExpr *element) = 0;
755
756 virtual void _accept(const LiteralExpr *element) = 0;
757
758- virtual void _accept(const PlusExpr *element) = 0;
759+ virtual void _accept(const PlusExpr *element) {
760+ element->CommutativeExpr::visit(*this);
761+ };
762
763- virtual void _accept(const MultiplyExpr *element) = 0;
764+ virtual void _accept(const MultiplyExpr *element) {
765+ element->CommutativeExpr::visit(*this);
766+ };
767
768 virtual void _accept(const MinusExpr *element) = 0;
769
770
771=== added file 'include/PetriEngine/PQL/XMLPrinter.h'
772--- include/PetriEngine/PQL/XMLPrinter.h 1970-01-01 00:00:00 +0000
773+++ include/PetriEngine/PQL/XMLPrinter.h 2021-10-18 11:40:53 +0000
774@@ -0,0 +1,119 @@
775+/* Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
776+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
777+ * Lars Kærlund Østergaard <larsko@gmail.com>,
778+ * Peter Gjøl Jensen <root@petergjoel.dk>,
779+ * Rasmus Tollund <rtollu18@student.aau.dk>
780+ *
781+ * This program is free software: you can redistribute it and/or modify
782+ * it under the terms of the GNU General Public License as published by
783+ * the Free Software Foundation, either version 3 of the License, or
784+ * (at your option) any later version.
785+ *
786+ * This program is distributed in the hope that it will be useful,
787+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
788+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
789+ * GNU General Public License for more details.
790+ *
791+ * You should have received a copy of the GNU General Public License
792+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
793+ */
794+#ifndef VERIFYPN_XMLPRINTER_H
795+#define VERIFYPN_XMLPRINTER_H
796+
797+#include <iostream>
798+#include "Visitor.h"
799+
800+namespace PetriEngine {
801+ namespace PQL {
802+ class XMLPrinter : public Visitor {
803+ public:
804+ XMLPrinter(std::ostream& os, uint32_t init_tabs = 0, uint32_t tab_size = 2, bool print_newlines = true, bool token_count = false) :
805+ os(os), tabs(init_tabs), tab_size(tab_size), single_tab(std::string(tab_size, ' ')), print_newlines(print_newlines), token_count(token_count) {}
806+
807+ protected:
808+ std::ostream& os;
809+ const bool token_count;
810+ uint32_t tabs;
811+ const uint32_t tab_size;
812+ const std::string single_tab;
813+ const bool print_newlines;
814+
815+ std::ostream & generateTabs();
816+
817+ void openXmlTag(const std::string& tag);
818+ void closeXmlTag(const std::string &tag);
819+ void outputLine(const std::string &line);
820+
821+ void _accept(const NotCondition *element) override;
822+
823+ void _accept(const AndCondition *element) override;
824+
825+ void _accept(const OrCondition *element) override;
826+
827+ void _accept(const LessThanCondition *element) override;
828+
829+ void _accept(const LessThanOrEqualCondition *element) override;
830+
831+ void _accept(const EqualCondition *element) override;
832+
833+ void _accept(const NotEqualCondition *element) override;
834+
835+ void _accept(const DeadlockCondition *element) override;
836+
837+ void _accept(const CompareConjunction *element) override;
838+
839+ void _accept(const UnfoldedUpperBoundsCondition *element) override;
840+
841+ void _accept(const EFCondition *condition) override;
842+
843+ void _accept(const EGCondition *condition) override;
844+
845+ void _accept(const AGCondition *condition) override;
846+
847+ void _accept(const AFCondition *condition) override;
848+
849+ void _accept(const EXCondition *condition) override;
850+
851+ void _accept(const AXCondition *condition) override;
852+
853+ void _accept(const EUCondition *condition) override;
854+
855+ void _accept(const AUCondition *condition) override;
856+
857+ void _accept(const ACondition *condition) override;
858+
859+ void _accept(const ECondition *condition) override;
860+
861+ void _accept(const GCondition *condition) override;
862+
863+ void _accept(const FCondition *condition) override;
864+
865+ void _accept(const XCondition *condition) override;
866+
867+ void _accept(const UntilCondition *condition) override;
868+
869+ void _accept(const UnfoldedFireableCondition *element) override;
870+
871+ void _accept(const BooleanCondition *element) override;
872+
873+ void _accept(const ShallowCondition *element) override;
874+
875+ void _accept(const UnfoldedIdentifierExpr *element) override;
876+
877+ void _accept(const LiteralExpr *element) override;
878+
879+ void _accept(const PlusExpr *element) override;
880+
881+ void _accept(const MultiplyExpr *element) override;
882+
883+ void _accept(const MinusExpr *element) override;
884+
885+ void _accept(const SubtractExpr *element) override;
886+
887+ void _accept(const IdentifierExpr *element) override;
888+
889+ };
890+ }
891+}
892+
893+#endif //VERIFYPN_XMLPRINTER_H
894
895=== added file 'src/PetriEngine/PQL/BinaryPrinter.cpp'
896--- src/PetriEngine/PQL/BinaryPrinter.cpp 1970-01-01 00:00:00 +0000
897+++ src/PetriEngine/PQL/BinaryPrinter.cpp 2021-10-18 11:40:53 +0000
898@@ -0,0 +1,173 @@
899+/* Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
900+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
901+ * Lars Kærlund Østergaard <larsko@gmail.com>,
902+ * Peter Gjøl Jensen <root@petergjoel.dk>,
903+ * Rasmus Tollund <rtollu18@student.aau.dk>
904+ *
905+ * This program is free software: you can redistribute it and/or modify
906+ * it under the terms of the GNU General Public License as published by
907+ * the Free Software Foundation, either version 3 of the License, or
908+ * (at your option) any later version.
909+ *
910+ * This program is distributed in the hope that it will be useful,
911+ * but WITHos ANY WARRANTY; withos even the implied warranty of
912+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
913+ * GNU General Public License for more details.
914+ *
915+ * You should have received a copy of the GNU General Public License
916+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
917+ */
918+#include "PetriEngine/PQL/BinaryPrinter.h"
919+
920+namespace PetriEngine::PQL {
921+ void BinaryPrinter::_accept(const LiteralExpr *element){
922+ os.write("l", sizeof(char));
923+ int temp = element->value();
924+ os.write(reinterpret_cast<const char*>(&temp), sizeof(int));
925+ }
926+
927+ void BinaryPrinter::_accept(const UnfoldedIdentifierExpr *element){
928+ os.write("i", sizeof(char));
929+ int temp = element->offset();
930+ os.write(reinterpret_cast<const char*>(&temp), sizeof(int));
931+ }
932+
933+ void BinaryPrinter::_accept(const MinusExpr *element){
934+ auto e1 = std::make_shared<PQL::LiteralExpr>(0);
935+ std::vector<Expr_ptr> exprs;
936+ exprs.push_back(e1);
937+ exprs.push_back((*element)[0]);
938+ PQL::SubtractExpr(std::move(exprs)).visit(*this);
939+ }
940+
941+ void BinaryPrinter::_accept(const SubtractExpr *element){
942+ os.write("-", sizeof(char));
943+ uint32_t size = element->expressions().size();
944+ os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
945+ for(auto& e : element->expressions())
946+ e->visit(*this);
947+ }
948+
949+ void BinaryPrinter::_accept(const CommutativeExpr *element){
950+ auto sop = element->op();
951+ os.write(&sop[0], sizeof(char));
952+ int32_t temp_constant = element->constant();
953+ os.write(reinterpret_cast<const char*>(&temp_constant), sizeof(int32_t));
954+ uint32_t size = element->places().size();
955+ os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
956+ size = element->expressions().size();
957+ os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
958+ for(auto& id : element->places())
959+ os.write(reinterpret_cast<const char*>(&id.first), sizeof(uint32_t));
960+ for(auto& e : element->expressions())
961+ e->visit(*this);
962+ }
963+
964+ void BinaryPrinter::_accept(const SimpleQuantifierCondition *condition){
965+ auto path = condition->getPath();
966+ auto quant = condition->getQuantifier();
967+ os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
968+ os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
969+ condition->getCond()->visit(*this);
970+ }
971+
972+ void BinaryPrinter::_accept(const UntilCondition *condition){
973+ auto path = condition->getPath();
974+ auto quant = condition->getQuantifier();
975+ os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
976+ os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
977+ (*condition)[0]->visit(*this);
978+ (*condition)[1]->visit(*this);
979+ }
980+
981+ void BinaryPrinter::_accept(const LogicalCondition *condition){
982+ auto path = condition->getPath();
983+ auto quant = condition->getQuantifier();
984+ os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
985+ os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
986+ uint32_t size = condition->operands();
987+ os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
988+ for(auto& c : *condition)
989+ c->visit(*this);
990+ }
991+
992+ void BinaryPrinter::_accept(const CompareConjunction *element){
993+ auto path = element->getPath();
994+ auto quant = Quantifier::COMPCONJ;
995+ os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
996+ os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
997+ bool temp = element->isNegated();
998+ os.write(reinterpret_cast<const char*>(&temp), sizeof(bool));
999+ uint32_t size = element->constraints().size();
1000+ os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
1001+ for(auto& c : element->constraints())
1002+ {
1003+ os.write(reinterpret_cast<const char*>(&c._place), sizeof(int32_t));
1004+ os.write(reinterpret_cast<const char*>(&c._lower), sizeof(uint32_t));
1005+ os.write(reinterpret_cast<const char*>(&c._upper), sizeof(uint32_t));
1006+ }
1007+ }
1008+
1009+ void BinaryPrinter::_accept(const CompareCondition *condition){
1010+ auto path = condition->getPath();
1011+ auto quant = condition->getQuantifier();
1012+ os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
1013+ os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1014+ std::string sop = condition->op();
1015+ os.write(sop.data(), sop.size());
1016+ os.write("\0", sizeof(char));
1017+ (*condition)[0]->visit(*this);
1018+ (*condition)[1]->visit(*this);
1019+ }
1020+
1021+ void BinaryPrinter::_accept(const DeadlockCondition *condition){
1022+ auto path = condition->getPath();
1023+ auto quant = Quantifier::DEADLOCK;
1024+ os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
1025+ os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1026+ }
1027+
1028+ void BinaryPrinter::_accept(const BooleanCondition *condition){
1029+ auto path = condition->getPath();
1030+ auto quant = Quantifier::PN_BOOLEAN;
1031+ os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
1032+ os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1033+ os.write(reinterpret_cast<const char*>(&condition->value), sizeof(bool));
1034+ }
1035+
1036+ void BinaryPrinter::_accept(const UnfoldedUpperBoundsCondition *condition){
1037+ auto path = condition->getPath();
1038+ auto quant = Quantifier::UPPERBOUNDS;
1039+ os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
1040+ os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1041+ uint32_t size = condition->places().size();
1042+ os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
1043+ double temp_max = condition->getMax();
1044+ os.write(reinterpret_cast<const char*>(&temp_max), sizeof(double));
1045+ double temp_offset = condition->getOffset();
1046+ os.write(reinterpret_cast<const char*>(&temp_offset), sizeof(double));
1047+ for(auto& b : condition->places())
1048+ {
1049+ os.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t));
1050+ os.write(reinterpret_cast<const char*>(&b._max), sizeof(double));
1051+ }
1052+ }
1053+
1054+ void BinaryPrinter::_accept(const NotCondition *condition){
1055+ auto path = condition->getPath();
1056+ auto quant = condition->getQuantifier();
1057+ os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
1058+ os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1059+ condition->getCond()->visit(*this);
1060+ }
1061+
1062+ void BinaryPrinter::_accept(const IdentifierExpr *condition) {
1063+ condition->compiled()->visit(*this);
1064+ }
1065+
1066+ void BinaryPrinter::_accept(const ShallowCondition *condition) {
1067+ condition->getCompiled()->visit(*this);
1068+ }
1069+
1070+
1071+}
1072
1073=== modified file 'src/PetriEngine/PQL/CMakeLists.txt'
1074--- src/PetriEngine/PQL/CMakeLists.txt 2021-08-11 09:06:51 +0000
1075+++ src/PetriEngine/PQL/CMakeLists.txt 2021-10-18 11:40:53 +0000
1076@@ -8,7 +8,7 @@
1077
1078 add_flex_bison_dependency(pql_lexer pql_parser)
1079
1080-add_library(PQL ${BISON_pql_parser_OUTPUTS} ${FLEX_pql_lexer_OUTPUTS} Expressions.cpp PQL.cpp Contexts.cpp QueryPrinter.cpp CTLVisitor.cpp)
1081+add_library(PQL ${BISON_pql_parser_OUTPUTS} ${FLEX_pql_lexer_OUTPUTS} Expressions.cpp PQL.cpp Contexts.cpp QueryPrinter.cpp CTLVisitor.cpp XMLPrinter.cpp BinaryPrinter.cpp)
1082 add_dependencies(PQL glpk-ext)
1083 target_link_libraries(PQL Simplification Reachability glpk PetriEngine)
1084
1085
1086=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
1087--- src/PetriEngine/PQL/Expressions.cpp 2021-10-03 14:50:33 +0000
1088+++ src/PetriEngine/PQL/Expressions.cpp 2021-10-18 11:40:53 +0000
1089@@ -976,6 +976,10 @@
1090
1091 /******************** Range Contexts ********************/
1092
1093+ void SimpleQuantifierCondition::visit(Visitor& ctx) const {
1094+ ctx.accept<decltype(this)>(this);
1095+ }
1096+
1097 void UntilCondition::visit(Visitor &ctx) const
1098 {
1099 ctx.accept<decltype(this)>(this);
1100@@ -1046,6 +1050,10 @@
1101 ctx.accept<decltype(this)>(this);
1102 }
1103
1104+ void LogicalCondition::visit(Visitor& ctx) const {
1105+ ctx.accept<decltype(this)>(this);
1106+ }
1107+
1108 void AndCondition::visit(Visitor& ctx) const
1109 {
1110 ctx.accept<decltype(this)>(this);
1111@@ -1060,7 +1068,15 @@
1112 {
1113 ctx.accept<decltype(this)>(this);
1114 }
1115-
1116+<<<<<<< TREE
1117+
1118+=======
1119+
1120+ void CompareCondition::visit(Visitor& ctx) const {
1121+ ctx.accept<decltype(this)>(this);
1122+ }
1123+
1124+>>>>>>> MERGE-SOURCE
1125 void EqualCondition::visit(Visitor& ctx) const
1126 {
1127 ctx.accept<decltype(this)>(this);
1128@@ -1176,6 +1192,10 @@
1129 ctx.accept<decltype(this)>(this);
1130 }
1131
1132+ void CommutativeExpr::visit(Visitor& ctx) const {
1133+ ctx.accept<decltype(this)>(this);
1134+ }
1135+
1136 void MinusExpr::visit(Visitor& ctx) const
1137 {
1138 ctx.accept<decltype(this)>(this);
1139@@ -1757,6 +1777,7 @@
1140 }
1141
1142 /******************** BIN output ********************/
1143+<<<<<<< TREE
1144
1145 void LiteralExpr::toBinary(std::ostream& out) const {
1146 out.write("l", sizeof(char));
1147@@ -1908,15 +1929,16 @@
1148 void LiteralExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
1149 generateTabs(out,tabs) << "<integer-constant>" + std::to_string(_value) + "</integer-constant>\n";
1150 }
1151+=======
1152+
1153+
1154+ /******************** CTL Output ********************/
1155+>>>>>>> MERGE-SOURCE
1156
1157 void LiteralExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
1158 out << "<integer-constant>" + std::to_string(_value) + "</integer-constant>\n";
1159 }
1160
1161- void UnfoldedFireableCondition::toXML(std::ostream& out, uint32_t tabs) const{
1162- generateTabs(out, tabs) << "<is-fireable><transition>" + _name << "</transition></is-fireable>\n";
1163- }
1164-
1165 void UnfoldedFireableCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1166 out << "<is-fireable><transition>" + _name << "</transition></is-fireable>\n";
1167 }
1168@@ -1944,6 +1966,7 @@
1169 out << "</is-fireable>";
1170 }
1171 }
1172+<<<<<<< TREE
1173
1174 void UnfoldedIdentifierExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
1175 if (tokencount) {
1176@@ -1956,6 +1979,8 @@
1177 generateTabs(out,tabs) << "</tokens-count>\n";
1178 }
1179 }
1180+=======
1181+>>>>>>> MERGE-SOURCE
1182
1183 void UnfoldedIdentifierExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
1184 if (tokencount) {
1185@@ -1997,6 +2022,7 @@
1186 }
1187 }
1188 }
1189+<<<<<<< TREE
1190
1191 void PlusExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
1192 if (tokencount) {
1193@@ -2022,6 +2048,8 @@
1194 for(auto& e : _exprs) e->toXML(ss,tabs+1, tokencount);
1195 generateTabs(ss,tabs) << "</integer-sum>\n";
1196 }
1197+=======
1198+>>>>>>> MERGE-SOURCE
1199
1200 void PlusExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
1201 if (tokencount) {
1202@@ -2047,30 +2075,37 @@
1203 for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);
1204 out << "</integer-sum>\n";
1205 }
1206+<<<<<<< TREE
1207
1208 void SubtractExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
1209 generateTabs(ss,tabs) << "<integer-difference>\n";
1210 for(auto& e : _exprs) e->toXML(ss,tabs+1);
1211 generateTabs(ss,tabs) << "</integer-difference>\n";
1212 }
1213+=======
1214+>>>>>>> MERGE-SOURCE
1215
1216 void SubtractExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
1217 out << "<integer-difference>\n";
1218 for(auto& e : _exprs) e->toCompactXML(out,tabs, context);
1219 out << "</integer-difference>\n";
1220 }
1221+<<<<<<< TREE
1222
1223 void MultiplyExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
1224 generateTabs(ss,tabs) << "<integer-product>\n";
1225 for(auto& e : _exprs) e->toXML(ss,tabs+1);
1226 generateTabs(ss,tabs) << "</integer-product>\n";
1227 }
1228+=======
1229+>>>>>>> MERGE-SOURCE
1230
1231 void MultiplyExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
1232 out << "<integer-product>\n";
1233 for(auto& e : _exprs) e->toCompactXML(out,tabs, context);
1234 out << "</integer-product>\n";
1235 }
1236+<<<<<<< TREE
1237
1238 void MinusExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
1239
1240@@ -2081,6 +2116,8 @@
1241 "<integer-constant>1</integer-constant>\n" ; generateTabs(out,tabs+1) <<
1242 "</integer-difference>\n" ; generateTabs(out,tabs) << "</integer-product>\n";
1243 }
1244+=======
1245+>>>>>>> MERGE-SOURCE
1246
1247 void MinusExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
1248 out << "<integer-product>\n";
1249@@ -2090,12 +2127,15 @@
1250 "<integer-constant>1</integer-constant>\n" ; out <<
1251 "</integer-difference>\n" ; out << "</integer-product>\n";
1252 }
1253+<<<<<<< TREE
1254
1255 void EXCondition::toXML(std::ostream& out,uint32_t tabs) const {
1256 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<next>\n";
1257 _cond->toXML(out,tabs+2);
1258 generateTabs(out,tabs+1) << "</next>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
1259 }
1260+=======
1261+>>>>>>> MERGE-SOURCE
1262
1263 void EXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1264 out << "<exists-path>\n" ; out << "<next>\n";
1265@@ -2103,6 +2143,7 @@
1266 out << "</next>\n" ; out << "</exists-path>\n";
1267 }
1268
1269+<<<<<<< TREE
1270 void AXCondition::toXML(std::ostream& out,uint32_t tabs) const {
1271 generateTabs(out,tabs) << "<all-paths>\n"; generateTabs(out,tabs+1) << "<next>\n";
1272 _cond->toXML(out,tabs+2);
1273@@ -2110,58 +2151,74 @@
1274 }
1275
1276 void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1277+=======
1278+ void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1279+>>>>>>> MERGE-SOURCE
1280 out << "<all-paths>\n" ;out << "<next>\n";
1281 _cond->toCompactXML(out,tabs+2, context);
1282 out << "</next>\n" ; out << "</all-paths>\n";
1283 }
1284+<<<<<<< TREE
1285
1286 void EFCondition::toXML(std::ostream& out,uint32_t tabs) const {
1287 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
1288 _cond->toXML(out,tabs+2);
1289 generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
1290 }
1291+=======
1292+>>>>>>> MERGE-SOURCE
1293
1294 void EFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1295 out << "<exists-path>\n" ;out << "<finally>\n";
1296 _cond->toCompactXML(out,tabs+2, context);
1297 out << "</finally>\n" ; out << "</exists-path>\n";
1298 }
1299+<<<<<<< TREE
1300
1301 void AFCondition::toXML(std::ostream& out,uint32_t tabs) const {
1302 generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
1303 _cond->toXML(out,tabs+2);
1304 generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
1305 }
1306+=======
1307+>>>>>>> MERGE-SOURCE
1308
1309 void AFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1310 out << "<all-paths>\n" ;out << "<finally>\n";
1311 _cond->toCompactXML(out,tabs+2, context);
1312 out << "</finally>\n" ; out << "</all-paths>\n";
1313 }
1314+<<<<<<< TREE
1315
1316 void EGCondition::toXML(std::ostream& out,uint32_t tabs) const {
1317 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
1318 _cond->toXML(out,tabs+2);
1319 generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
1320 }
1321+=======
1322+>>>>>>> MERGE-SOURCE
1323
1324 void EGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1325 out << "<exists-path>\n" ;out << "<globally>\n";
1326 _cond->toCompactXML(out,tabs+2, context);
1327 out << "</globally>\n" ; out << "</exists-path>\n";
1328 }
1329+<<<<<<< TREE
1330
1331 void AGCondition::toXML(std::ostream& out,uint32_t tabs) const {
1332 generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
1333 _cond->toXML(out,tabs+2);
1334 generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
1335 }
1336+=======
1337+>>>>>>> MERGE-SOURCE
1338
1339 void AGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1340 out << "<all-paths>\n" ;out << "<globally>\n";
1341 _cond->toCompactXML(out,tabs+2, context);
1342 out << "</globally>\n" ; out << "</all-paths>\n";
1343 }
1344+<<<<<<< TREE
1345
1346 void EUCondition::toXML(std::ostream& out,uint32_t tabs) const {
1347 generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
1348@@ -2170,6 +2227,8 @@
1349 _cond2->toXML(out,tabs+3);
1350 generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
1351 }
1352+=======
1353+>>>>>>> MERGE-SOURCE
1354
1355 void EUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1356 out << "<exists-path>\n" ; out << "<until>\n" ; out << "<before>\n";
1357@@ -2178,6 +2237,7 @@
1358 _cond2->toCompactXML(out,tabs+2, context);
1359 out << "</reach>\n" ; out << "</until>\n" ; out << "</exists-path>\n";
1360 }
1361+<<<<<<< TREE
1362
1363 void AUCondition::toXML(std::ostream& out,uint32_t tabs) const {
1364 generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
1365@@ -2186,6 +2246,8 @@
1366 _cond2->toXML(out,tabs+3);
1367 generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
1368 }
1369+=======
1370+>>>>>>> MERGE-SOURCE
1371
1372 void AUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1373 out << "<all-paths>\n" ; out << "<until>\n" ; out << "<before>\n";
1374@@ -2195,6 +2257,7 @@
1375 out << "</reach>\n" ; out << "</until>\n" ; out << "</all-paths>\n";
1376 }
1377
1378+<<<<<<< TREE
1379 void ACondition::toXML(std::ostream& out, uint32_t tabs) const {
1380 generateTabs(out, tabs) << "<all-paths>\n";
1381 _cond->toXML(out, tabs+1);
1382@@ -2202,11 +2265,15 @@
1383 }
1384
1385 void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1386+=======
1387+ void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1388+>>>>>>> MERGE-SOURCE
1389 out << "<all-paths>\n" ;
1390 _cond->toCompactXML(out,tabs+2, context);
1391 out << "</all-paths>\n";
1392 }
1393
1394+<<<<<<< TREE
1395 void ECondition::toXML(std::ostream& out, uint32_t tabs) const {
1396 generateTabs(out, tabs) << "<exists-path>\n";
1397 _cond->toXML(out, tabs+1);
1398@@ -2214,11 +2281,15 @@
1399 }
1400
1401 void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1402+=======
1403+ void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1404+>>>>>>> MERGE-SOURCE
1405 out << "<exists-path>\n" ;
1406 _cond->toCompactXML(out,tabs+2, context);
1407 out << "</exists-path>\n";
1408 }
1409
1410+<<<<<<< TREE
1411 void FCondition::toXML(std::ostream& out, uint32_t tabs) const {
1412 generateTabs(out, tabs) << "<finally>\n";
1413 _cond->toXML(out, tabs+1);
1414@@ -2226,11 +2297,15 @@
1415 }
1416
1417 void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1418+=======
1419+ void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1420+>>>>>>> MERGE-SOURCE
1421 out << "<finally>\n" ;
1422 _cond->toCompactXML(out,tabs+2, context);
1423 out << "</finally>\n";
1424 }
1425
1426+<<<<<<< TREE
1427 void GCondition::toXML(std::ostream& out, uint32_t tabs) const {
1428 generateTabs(out, tabs) << "<globally>\n";
1429 _cond->toXML(out, tabs+1);
1430@@ -2238,11 +2313,15 @@
1431 }
1432
1433 void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1434+=======
1435+ void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1436+>>>>>>> MERGE-SOURCE
1437 out << "<globally>\n" ;
1438 _cond->toCompactXML(out,tabs+2, context);
1439 out << "</globally>\n";
1440 }
1441
1442+<<<<<<< TREE
1443 void XCondition::toXML(std::ostream& out, uint32_t tabs) const {
1444 generateTabs(out, tabs) << "<next>\n";
1445 _cond->toXML(out, tabs+1);
1446@@ -2250,11 +2329,15 @@
1447 }
1448
1449 void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1450+=======
1451+ void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1452+>>>>>>> MERGE-SOURCE
1453 out << "<next>\n" ;
1454 _cond->toCompactXML(out,tabs+2, context);
1455 out << "</next>\n";
1456 }
1457
1458+<<<<<<< TREE
1459 void UntilCondition::toXML(std::ostream& out, uint32_t tabs) const {
1460 generateTabs(out,tabs) << "<until>\n" ; generateTabs(out,tabs+1) << "<before>\n";
1461 _cond1->toXML(out,tabs+2);
1462@@ -2264,6 +2347,9 @@
1463 }
1464
1465 void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1466+=======
1467+ void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1468+>>>>>>> MERGE-SOURCE
1469 out << "<until>\n" ; out << "<before>\n";
1470 _cond1->toCompactXML(out,tabs+2, context);
1471 out << "</before>\n" ; out << "<reach>\n";
1472@@ -2271,6 +2357,7 @@
1473 out << "</reach>\n"; out << "</until>\n" ;
1474 }
1475
1476+<<<<<<< TREE
1477 void AndCondition::toXML(std::ostream& out,uint32_t tabs) const {
1478 if(_conds.size() == 0)
1479 {
1480@@ -2304,6 +2391,9 @@
1481 }
1482
1483 void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1484+=======
1485+ void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1486+>>>>>>> MERGE-SOURCE
1487 if(_conds.size() == 0)
1488 {
1489 BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);
1490@@ -2334,6 +2424,7 @@
1491 }
1492 out << "</conjunction>\n";
1493 }
1494+<<<<<<< TREE
1495
1496 void OrCondition::toXML(std::ostream& out,uint32_t tabs) const {
1497 if(_conds.size() == 0)
1498@@ -2366,6 +2457,8 @@
1499 }
1500 generateTabs(out,tabs) << "</disjunction>\n";
1501 }
1502+=======
1503+>>>>>>> MERGE-SOURCE
1504
1505 void OrCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1506 if(_conds.size() == 0)
1507@@ -2399,6 +2492,7 @@
1508 out << "</disjunction>\n";
1509 }
1510
1511+<<<<<<< TREE
1512 void CompareConjunction::toXML(std::ostream& out, uint32_t tabs) const
1513 {
1514 if(_negated) generateTabs(out,tabs++) << "<negation>";
1515@@ -2438,6 +2532,9 @@
1516 }
1517
1518 void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1519+=======
1520+ void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1521+>>>>>>> MERGE-SOURCE
1522 if(_negated) out << "<negation>";
1523 if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);
1524 else
1525@@ -2474,6 +2571,7 @@
1526 if(_negated) out << "</negation>";
1527 }
1528
1529+<<<<<<< TREE
1530 void EqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
1531 generateTabs(out,tabs) << "<integer-eq>\n";
1532 _expr1->toXML(out,tabs+1);
1533@@ -2482,11 +2580,15 @@
1534 }
1535
1536 void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1537+=======
1538+ void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1539+>>>>>>> MERGE-SOURCE
1540 out << "<integer-eq>\n";
1541 _expr1->toCompactXML(out,tabs, context);
1542 _expr2->toCompactXML(out,tabs, context);
1543 out << "</integer-eq>\n";
1544 }
1545+<<<<<<< TREE
1546
1547 void NotEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
1548 generateTabs(out,tabs) << "<integer-ne>\n";
1549@@ -2494,6 +2596,8 @@
1550 _expr2->toXML(out,tabs+1);
1551 generateTabs(out,tabs) << "</integer-ne>\n";
1552 }
1553+=======
1554+>>>>>>> MERGE-SOURCE
1555
1556 void NotEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1557 out << "<integer-ne>\n";
1558@@ -2501,6 +2605,7 @@
1559 _expr2->toCompactXML(out,tabs, context);
1560 out << "</integer-ne>\n";
1561 }
1562+<<<<<<< TREE
1563
1564 void LessThanCondition::toXML(std::ostream& out,uint32_t tabs) const {
1565 generateTabs(out,tabs) << "<integer-lt>\n";
1566@@ -2508,6 +2613,8 @@
1567 _expr2->toXML(out,tabs+1);
1568 generateTabs(out,tabs) << "</integer-lt>\n";
1569 }
1570+=======
1571+>>>>>>> MERGE-SOURCE
1572
1573 void LessThanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1574 out << "<integer-lt>\n";
1575@@ -2515,6 +2622,7 @@
1576 _expr2->toCompactXML(out,tabs, context);
1577 out << "</integer-lt>\n";
1578 }
1579+<<<<<<< TREE
1580
1581 void LessThanOrEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
1582 generateTabs(out,tabs) << "<integer-le>\n";
1583@@ -2522,6 +2630,8 @@
1584 _expr2->toXML(out,tabs+1);
1585 generateTabs(out,tabs) << "</integer-le>\n";
1586 }
1587+=======
1588+>>>>>>> MERGE-SOURCE
1589
1590 void LessThanOrEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1591 out << "<integer-le>\n";
1592@@ -2529,6 +2639,7 @@
1593 _expr2->toCompactXML(out,tabs, context);
1594 out << "</integer-le>\n";
1595 }
1596+<<<<<<< TREE
1597
1598 void NotCondition::toXML(std::ostream& out,uint32_t tabs) const {
1599
1600@@ -2536,12 +2647,15 @@
1601 _cond->toXML(out,tabs+1);
1602 generateTabs(out,tabs) << "</negation>\n";
1603 }
1604+=======
1605+>>>>>>> MERGE-SOURCE
1606
1607 void NotCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1608 out << "<negation>\n";
1609 _cond->toCompactXML(out,tabs, context);
1610 out << "</negation>\n";
1611 }
1612+<<<<<<< TREE
1613
1614 void BooleanCondition::toXML(std::ostream& out,uint32_t tabs) const {
1615 generateTabs(out,tabs) << "<" <<
1616@@ -2558,10 +2672,19 @@
1617 void DeadlockCondition::toXML(std::ostream& out,uint32_t tabs) const {
1618 generateTabs(out,tabs) << "<deadlock/>\n";
1619 }
1620+=======
1621+
1622+ void BooleanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1623+ out << "<" <<
1624+ (value ? "true" : "false")
1625+ << "/>\n";
1626+ }
1627+>>>>>>> MERGE-SOURCE
1628
1629 void DeadlockCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1630 out << "<deadlock/>\n";
1631 }
1632+<<<<<<< TREE
1633
1634 void UnfoldedUpperBoundsCondition::toXML(std::ostream& out, uint32_t tabs) const {
1635 generateTabs(out, tabs) << "<place-bound>\n";
1636@@ -2569,6 +2692,8 @@
1637 generateTabs(out, tabs + 1) << "<place>" << p._name << "</place>\n";
1638 generateTabs(out, tabs) << "</place-bound>\n";
1639 }
1640+=======
1641+>>>>>>> MERGE-SOURCE
1642
1643 void UnfoldedUpperBoundsCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
1644 out << "<place-bound>\n";
1645@@ -4462,6 +4587,8 @@
1646 return false;
1647 }
1648
1649+
1650+
1651 } // PQL
1652 } // PetriEngine
1653
1654
1655=== added file 'src/PetriEngine/PQL/XMLPrinter.cpp'
1656--- src/PetriEngine/PQL/XMLPrinter.cpp 1970-01-01 00:00:00 +0000
1657+++ src/PetriEngine/PQL/XMLPrinter.cpp 2021-10-18 11:40:53 +0000
1658@@ -0,0 +1,399 @@
1659+/* Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
1660+ * Thomas Søndersø Nielsen <primogens@gmail.com>,
1661+ * Lars Kærlund Østergaard <larsko@gmail.com>,
1662+ * Peter Gjøl Jensen <root@petergjoel.dk>,
1663+ * Rasmus Tollund <rtollu18@student.aau.dk>
1664+ *
1665+ * This program is free software: you can redistribute it and/or modify
1666+ * it under the terms of the GNU General Public License as published by
1667+ * the Free Software Foundation, either version 3 of the License, or
1668+ * (at your option) any later version.
1669+ *
1670+ * This program is distributed in the hope that it will be useful,
1671+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
1672+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
1673+ * GNU General Public License for more details.
1674+ *
1675+ * You should have received a copy of the GNU General Public License
1676+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
1677+ */
1678+#include "PetriEngine/PQL/XMLPrinter.h"
1679+namespace PetriEngine {
1680+ namespace PQL {
1681+ std::ostream& XMLPrinter::generateTabs() {
1682+ for(uint32_t i = 0; i < tabs; i++) {
1683+ os << single_tab;
1684+ }
1685+ return os;
1686+ }
1687+
1688+ void XMLPrinter::openXmlTag(const std::string &tag) {
1689+ generateTabs() << "<" << tag << (print_newlines? ">\n": ">");
1690+ tabs++;
1691+ }
1692+
1693+ void XMLPrinter::closeXmlTag(const std::string &tag) {
1694+ tabs--;
1695+ generateTabs() << "</" << tag << (print_newlines? ">\n": ">");
1696+ }
1697+
1698+ void XMLPrinter::outputLine(const std::string &line) {
1699+ generateTabs() << line << (print_newlines? "\n": "");
1700+
1701+ }
1702+
1703+ void XMLPrinter::_accept(const NotCondition *element) {
1704+ openXmlTag("negation");
1705+ element->getCond()->visit(*this);
1706+ closeXmlTag("negation");
1707+ }
1708+
1709+ void XMLPrinter::_accept(const AndCondition *element) {
1710+ if(element->empty())
1711+ {
1712+ BooleanCondition::TRUE_CONSTANT->visit(*this);
1713+ return;
1714+ }
1715+ if(element->size() == 1)
1716+ {
1717+ (*element)[0]->visit(*this);
1718+ return;
1719+ }
1720+ openXmlTag("conjunction");
1721+ (*element)[0]->visit(*this);
1722+ for(size_t i = 1; i < element->size(); ++i)
1723+ {
1724+ if(i + 1 == element->size())
1725+ {
1726+ (*element)[i]->visit(*this);
1727+ }
1728+ else
1729+ {
1730+ openXmlTag("conjunction");
1731+ (*element)[i]->visit(*this);
1732+ }
1733+ }
1734+ for(size_t i = element->size() - 1; i > 1; --i)
1735+ {
1736+ closeXmlTag("conjunction");
1737+ }
1738+ closeXmlTag("conjunction");
1739+ }
1740+
1741+ void XMLPrinter::_accept(const OrCondition *element) {
1742+ if(element->empty())
1743+ {
1744+ BooleanCondition::FALSE_CONSTANT->visit(*this);
1745+ return;
1746+ }
1747+ if(element->size() == 1)
1748+ {
1749+ (*element)[0]->visit(*this);
1750+ return;
1751+ }
1752+ openXmlTag("disjunction");
1753+ (*element)[0]->visit(*this);
1754+ for(size_t i = 1; i < element->size(); ++i)
1755+ {
1756+ if(i + 1 == element->size())
1757+ {
1758+ (*element)[i]->visit(*this);
1759+ }
1760+ else
1761+ {
1762+ openXmlTag("disjunction");
1763+ (*element)[i]->visit(*this);
1764+ }
1765+ }
1766+ for(size_t i = element->size() - 1; i > 1; --i)
1767+ {
1768+ closeXmlTag("disjunction");
1769+ }
1770+ closeXmlTag("disjunction");
1771+ }
1772+
1773+ void XMLPrinter::_accept(const LessThanCondition *element) {
1774+ openXmlTag("integer-lt");
1775+ (*element)[0]->visit(*this);
1776+ (*element)[1]->visit(*this);
1777+ closeXmlTag("integer-lt");
1778+ }
1779+
1780+ void XMLPrinter::_accept(const LessThanOrEqualCondition *element) {
1781+ openXmlTag("integer-le");
1782+ (*element)[0]->visit(*this);
1783+ (*element)[1]->visit(*this);
1784+ closeXmlTag("integer-le");
1785+ }
1786+
1787+ void XMLPrinter::_accept(const EqualCondition *element) {
1788+ openXmlTag("integer-eq");
1789+ (*element)[0]->visit(*this);
1790+ (*element)[1]->visit(*this);
1791+ closeXmlTag("integer-eq");
1792+ }
1793+
1794+ void XMLPrinter::_accept(const NotEqualCondition *element) {
1795+ openXmlTag("integer-ne");
1796+ (*element)[0]->visit(*this);
1797+ (*element)[1]->visit(*this);
1798+ closeXmlTag("integer-ne");
1799+ }
1800+
1801+ void XMLPrinter::_accept(const DeadlockCondition *element) {
1802+ outputLine("<deadlock/>");
1803+ }
1804+
1805+ void XMLPrinter::_accept(const CompareConjunction *element) {
1806+ if(element->isNegated()) {
1807+ generateTabs() << "<negation>";
1808+ }
1809+
1810+ if(element->constraints().empty()) BooleanCondition::TRUE_CONSTANT->visit(*this);
1811+ else
1812+ {
1813+ bool single = element->constraints().size() == 1 &&
1814+ (element->constraints()[0]._lower == 0 ||
1815+ element->constraints()[0]._upper == std::numeric_limits<uint32_t>::max());
1816+ if(!single)
1817+ openXmlTag("conjunction");
1818+ for(auto& c : element->constraints())
1819+ {
1820+ if(c._lower != 0)
1821+ {
1822+ openXmlTag("integer-ge");
1823+ openXmlTag("tokens-count");
1824+ outputLine("<place>" + c._name + "</place>");
1825+ closeXmlTag("tokens-count");
1826+ outputLine("<integer-constant>" + std::to_string(c._lower) + "</integer-constant>");
1827+ closeXmlTag("integer-ge");
1828+ }
1829+ if(c._upper != std::numeric_limits<uint32_t>::max())
1830+ {
1831+ openXmlTag("integer-le");
1832+ openXmlTag("tokens-count");
1833+ outputLine("<place>" + c._name + "</place>");
1834+ closeXmlTag("tokens-count");
1835+ outputLine("<integer-constant>" + std::to_string(c._upper) + "</integer-constant>");
1836+ closeXmlTag("integer-le");
1837+ }
1838+ }
1839+ if(!single)
1840+ closeXmlTag("conjunction");
1841+ }
1842+ if(element->isNegated()) {
1843+ generateTabs() << "</negation>";
1844+ }
1845+ }
1846+
1847+ void XMLPrinter::_accept(const UnfoldedUpperBoundsCondition *element) {
1848+ openXmlTag("place-bound");
1849+ for(auto& p : element->places()) {
1850+ outputLine("<place>" + p._name + "</place>");
1851+ }
1852+ closeXmlTag("place-bound");
1853+ }
1854+
1855+ void XMLPrinter::_accept(const EFCondition *condition) {
1856+ openXmlTag("exists-path");
1857+ openXmlTag("finally");
1858+ condition->getCond()->visit(*this);
1859+ closeXmlTag("finally");
1860+ closeXmlTag("exists-path");
1861+ }
1862+
1863+ void XMLPrinter::_accept(const EGCondition *condition) {
1864+ openXmlTag("exists-path");
1865+ openXmlTag("globally");
1866+ condition->getCond()->visit(*this);
1867+ closeXmlTag("globally");
1868+ closeXmlTag("exists-path");
1869+ }
1870+
1871+ void XMLPrinter::_accept(const AGCondition *condition) {
1872+ openXmlTag("all-paths");
1873+ openXmlTag("globally");
1874+ condition->getCond()->visit(*this);
1875+ closeXmlTag("globally");
1876+ closeXmlTag("all-paths");
1877+ }
1878+
1879+ void XMLPrinter::_accept(const AFCondition *condition) {
1880+ openXmlTag("all-paths");
1881+ openXmlTag("finally");
1882+ condition->getCond()->visit(*this);
1883+ closeXmlTag("finally");
1884+ closeXmlTag("all-paths");
1885+ }
1886+
1887+ void XMLPrinter::_accept(const EXCondition *condition) {
1888+ openXmlTag("exists-path");
1889+ openXmlTag("next");
1890+ condition->getCond()->visit(*this);
1891+ closeXmlTag("next");
1892+ closeXmlTag("exists-path");
1893+ }
1894+
1895+ void XMLPrinter::_accept(const AXCondition *condition) {
1896+ openXmlTag("all-paths");
1897+ openXmlTag("next");
1898+ condition->getCond()->visit(*this);
1899+ closeXmlTag("next");
1900+ closeXmlTag("all-paths");
1901+ }
1902+
1903+ void XMLPrinter::_accept(const EUCondition *condition) {
1904+ openXmlTag("exists-path");
1905+ openXmlTag("until");
1906+ openXmlTag("before");
1907+ (*condition)[0]->visit(*this);
1908+ closeXmlTag("before");
1909+ openXmlTag("reach");
1910+ (*condition)[1]->visit(*this);
1911+ closeXmlTag("reach");
1912+ closeXmlTag("until");
1913+ closeXmlTag("exists-path");
1914+ }
1915+
1916+ void XMLPrinter::_accept(const AUCondition *condition) {
1917+ openXmlTag("all-paths");
1918+ openXmlTag("until");
1919+ openXmlTag("before");
1920+ (*condition)[0]->visit(*this);
1921+ closeXmlTag("before");
1922+ openXmlTag("reach");
1923+ (*condition)[1]->visit(*this);
1924+ closeXmlTag("reach");
1925+ closeXmlTag("until");
1926+ closeXmlTag("all-paths");
1927+
1928+ }
1929+
1930+ void XMLPrinter::_accept(const ACondition *condition) {
1931+ openXmlTag("all-paths");
1932+ condition->getCond()->visit(*this);
1933+ closeXmlTag("all-paths");
1934+ }
1935+
1936+ void XMLPrinter::_accept(const ECondition *condition) {
1937+ openXmlTag("exists-path");
1938+ condition->getCond()->visit(*this);
1939+ closeXmlTag("exists-path");
1940+ }
1941+
1942+ void XMLPrinter::_accept(const GCondition *condition) {
1943+ openXmlTag("globally");
1944+ condition->getCond()->visit(*this);
1945+ closeXmlTag("globally");
1946+ }
1947+
1948+ void XMLPrinter::_accept(const FCondition *condition) {
1949+ openXmlTag("finally");
1950+ condition->getCond()->visit(*this);
1951+ closeXmlTag("finally");
1952+ }
1953+
1954+ void XMLPrinter::_accept(const XCondition *condition) {
1955+ openXmlTag("next");
1956+ condition->getCond()->visit(*this);
1957+ closeXmlTag("next");
1958+ }
1959+
1960+ void XMLPrinter::_accept(const UntilCondition *condition) {
1961+ openXmlTag("until") ;
1962+ openXmlTag("before");
1963+ (*condition)[0]->visit(*this);
1964+ closeXmlTag("before") ;
1965+ openXmlTag("reach");
1966+ (*condition)[1]->visit(*this);
1967+ closeXmlTag("reach") ;
1968+ closeXmlTag("until") ;
1969+ }
1970+
1971+ void XMLPrinter::_accept(const UnfoldedFireableCondition *element) {
1972+ outputLine("<is-fireable><transition>" + element->getName() + "</transition></is-fireable>");
1973+ }
1974+
1975+ void XMLPrinter::_accept(const BooleanCondition *element) {
1976+ outputLine(element->value? "<true/>": "<false/>");
1977+ }
1978+
1979+ void XMLPrinter::_accept(const UnfoldedIdentifierExpr *element) {
1980+ if (token_count) {
1981+ outputLine("<place>" + element->name() + "</place>");
1982+ }
1983+ else
1984+ {
1985+ openXmlTag("tokens-count");
1986+ outputLine("<place>" + element->name() + "</place>");
1987+ closeXmlTag("tokens-count");
1988+ }
1989+ }
1990+
1991+ void XMLPrinter::_accept(const LiteralExpr *element) {
1992+ outputLine("<integer-constant>" + std::to_string(element->value()) + "</integer-constant>");
1993+ }
1994+
1995+ void XMLPrinter::_accept(const PlusExpr *element) {
1996+ if (token_count) {
1997+ for(auto& e : element->expressions())
1998+ e->visit(*this);
1999+ return;
2000+ }
2001+
2002+ if(element->tk) {
2003+ openXmlTag("tokens-count");
2004+ for(auto& e : element->places())
2005+ outputLine("<place>" + e.second + "</place>");
2006+ for(auto& e : element->expressions())
2007+ e->visit(*this);
2008+ closeXmlTag("tokens-count");
2009+ return;
2010+ }
2011+ openXmlTag("integer-sum");
2012+ outputLine("<integer-constant>" + std::to_string(element->constant()) + "</integer-constant>");
2013+ for(auto& i : element->places())
2014+ {
2015+ openXmlTag("tokens-count");
2016+ outputLine("<place>" + i.second + "</place>");
2017+ closeXmlTag("tokens-count");
2018+ }
2019+ for(auto& e : element->expressions())
2020+ e->visit(*this);
2021+ closeXmlTag("integer-sum");
2022+ }
2023+
2024+ void XMLPrinter::_accept(const MultiplyExpr *element) {
2025+ openXmlTag("integer-product");
2026+ for(auto& e : element->expressions())
2027+ e->visit(*this);
2028+ closeXmlTag("integer-product");
2029+ }
2030+
2031+ void XMLPrinter::_accept(const MinusExpr *element) {
2032+ openXmlTag("integer-product");
2033+ (*element)[0]->visit(*this);
2034+ openXmlTag("integer-difference");
2035+ outputLine("<integer-constant>0</integer-constant>");
2036+ outputLine("<integer-constant>1</integer-constant>");
2037+ closeXmlTag("integer-difference");
2038+ closeXmlTag("integer-product");
2039+ }
2040+
2041+ void XMLPrinter::_accept(const SubtractExpr *element) {
2042+ openXmlTag("integer-difference");
2043+ for(auto& e : element->expressions())
2044+ e->visit(*this);
2045+ closeXmlTag("integer-difference");
2046+ }
2047+
2048+ void XMLPrinter::_accept(const IdentifierExpr *element) {
2049+ element->compiled()->visit(*this);
2050+ }
2051+
2052+ void XMLPrinter::_accept(const ShallowCondition *element) {
2053+ element->getCompiled()->visit(*this);
2054+ }
2055+ }
2056+}
2057+
2058
2059=== modified file 'src/VerifyPN.cpp'
2060--- src/VerifyPN.cpp 2021-10-14 11:37:21 +0000
2061+++ src/VerifyPN.cpp 2021-10-18 11:40:53 +0000
2062@@ -75,6 +75,7 @@
2063 #include "PetriEngine/PetriNetBuilder.h"
2064 #include "PetriEngine/PQL/PQL.h"
2065 #include "PetriEngine/PQL/CTLVisitor.h"
2066+#include <PetriEngine/PQL/XMLPrinter.h>
2067 #include "PetriEngine/options.h"
2068 #include "PetriEngine/errorcodes.h"
2069 #include "PetriEngine/STSolver.h"
2070@@ -90,6 +91,7 @@
2071 #include "LTL/LTLMain.h"
2072
2073 #include <atomic>
2074+#include <PetriEngine/PQL/BinaryPrinter.h>
2075
2076 using namespace PetriEngine;
2077 using namespace PetriEngine::PQL;
2078@@ -940,7 +942,8 @@
2079 continue;
2080 }
2081 ss << " <property>\n <id>" << querynames[i] << "</id>\n <description>Simplified</description>\n <formula>\n";
2082- queries[i]->toXML(ss, 3);
2083+ XMLPrinter xml_printer(ss, 3);
2084+ queries[i]->visit(xml_printer);
2085 ss << " </formula>\n </property>\n";
2086 }
2087
2088@@ -985,12 +988,14 @@
2089 {
2090 out.write(querynames[i].data(), querynames[i].size());
2091 out.write("\0", sizeof(char));
2092- queries[i]->toBinary(out);
2093+ BinaryPrinter binary_printer(out);
2094+ queries[i]->visit(binary_printer);
2095 }
2096 else
2097 {
2098 out << " <property>\n <id>" << querynames[i] << "</id>\n <description>Simplified</description>\n <formula>\n";
2099- queries[i]->toXML(out, 3);
2100+ XMLPrinter xml_printer(out, 3);
2101+ queries[i]->visit(xml_printer);
2102 out << " </formula>\n </property>\n";
2103 }
2104 }

Subscribers

People subscribed via source and target branches