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

[Rasmus Tollund]

Changed XML printer for queries to use visitor pattern.

[Peter Gjøl Jensen (peter-gjoel)]

review: Needs Fixing

[lp:~ragusaen/verifypn/verifypn]

253. By Rasmus Tollund on 2021-10-02

Added options for tab size and printing new lines

254. By Rasmus Tollund on 2021-10-02

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 on 2021-10-02

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 on 2021-10-04

Removed .h file from add_libraries

257. By Rasmus Tollund on 2021-10-18

Fixed bug with until condition

=== added file 'include/PetriEngine/PQL/BinaryPrinter.h'
--- include/PetriEngine/PQL/BinaryPrinter.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PQL/BinaryPrinter.h	2021-10-18 11:40:53 +0000
@@ -0,0 +1,71 @@
+/* Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>,
+ *                     Rasmus Tollund <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_BINARYPRINTER_H
+#define VERIFYPN_BINARYPRINTER_H
+
+#include "Visitor.h"
+
+namespace PetriEngine::PQL {
+    class BinaryPrinter : public Visitor {
+    public:
+        explicit BinaryPrinter(std::ostream& os) :
+            os(os) {}
+
+    protected:
+        std::ostream& os;
+
+        void _accept(const NotCondition *element) override;
+
+        void _accept(const DeadlockCondition *element) override;
+
+        void _accept(const CompareConjunction *element) override;
+
+        void _accept(const UnfoldedUpperBoundsCondition *element) override;
+
+        void _accept(const UntilCondition *condition) override;
+
+        void _accept(const BooleanCondition *element) override;
+
+        void _accept(const UnfoldedIdentifierExpr *element) override;
+
+        void _accept(const LiteralExpr *element) override;
+
+        void _accept(const MinusExpr *element) override;
+
+        void _accept(const SubtractExpr *element) override;
+
+        void _accept(const CommutativeExpr *element) override;
+
+        void _accept(const SimpleQuantifierCondition *condition) override;
+
+        void _accept(const LogicalCondition *condition) override;
+
+        void _accept(const CompareCondition *condition) override;
+
+        void _accept(const IdentifierExpr *condition) override;
+
+        void _accept(const ShallowCondition *condition) override;
+
+    };
+}
+
+
+#endif //VERIFYPN_BINARYPRINTER_H
 
=== modified file 'include/PetriEngine/PQL/Expressions.h'
--- include/PetriEngine/PQL/Expressions.h	2021-08-12 12:35:54 +0000
+++ include/PetriEngine/PQL/Expressions.h	2021-10-18 11:40:53 +0000
@@ -62,9 +62,10 @@
             const Expr_ptr &operator[](size_t i) const {
                 return _exprs[i];
             }
+            virtual std::string op() const = 0;
+
         protected:
             virtual int apply(int v1, int v2) const = 0;
-            virtual std::string op() const = 0;
             std::vector<Expr_ptr> _exprs;
             virtual int32_t preOp(const EvaluationContext& context) const;
         };
@@ -78,7 +79,7 @@
             friend CompareCondition;
             virtual void analyze(AnalysisContext& context) override;
             int evaluate(const EvaluationContext& context) override;
-            void toBinary(std::ostream&) const override;
+            void visit(Visitor&) const override;
             int formulaSize() const override{
                 size_t sum = _ids.size();
                 for(auto& e : _exprs) sum += e->formulaSize();
@@ -87,6 +88,7 @@
             bool placeFree() const override;
             auto constant() const { return _constant; }
             auto& places() const { return _ids; }
+
         protected:
             CommutativeExpr(int constant): _constant(constant) {};
             void init(std::vector<Expr_ptr>&& exprs);
@@ -104,7 +106,6 @@
 
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
             bool tk = false;
 
@@ -125,11 +126,9 @@
             }
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
 
 
-            void toBinary(std::ostream&) const override;
             void visit(Visitor& visitor) const override;
         protected:
             int apply(int v1, int v2) const override;
@@ -144,7 +143,6 @@
             MultiplyExpr(std::vector<Expr_ptr>&& exprs);
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
 
 
@@ -166,9 +164,7 @@
             int evaluate(const EvaluationContext& context) override;
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
-            void toBinary(std::ostream&) const override;
 
             void visit(Visitor& visitor) const override;
             int formulaSize() const override{
@@ -190,9 +186,7 @@
             void analyze(AnalysisContext& context) override;
             int evaluate(const EvaluationContext& context) override;
             Expr::Types type() const override;
-            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
-            void toBinary(std::ostream&) const override;
 
             void visit(Visitor& visitor) const override;
             int formulaSize() const override{
@@ -220,9 +214,6 @@
                 if(_compiled) return _compiled->type();
                 return Expr::IdentifierExpr;
             }
-            void toXML(std::ostream& os, uint32_t tabs, bool tokencount = false) const override {
-                _compiled->toXML(os, tabs, tokencount);
-            }
             void toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
 
             int formulaSize() const override {
@@ -238,15 +229,12 @@
                 return _compiled->constraint(context);
             }
 
-            void toBinary(std::ostream& s) const override {
-                _compiled->toBinary(s);
-            }
             void visit(Visitor& visitor) const override;
 
             [[nodiscard]] const std::string &name() const {
                 return _name;
             }
-            
+
             [[nodiscard]] const Expr_ptr &compiled() const {
                 return _compiled;
             }
@@ -265,15 +253,13 @@
 
             UnfoldedIdentifierExpr(const std::string& name) : UnfoldedIdentifierExpr(name, -1) {
             }
-            
+
             UnfoldedIdentifierExpr(const UnfoldedIdentifierExpr&) = default;
 
             void analyze(AnalysisContext& context) override;
             int evaluate(const EvaluationContext& context) override;
             Expr::Types type() const override;
-            void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
-            void toBinary(std::ostream&) const override;
             int formulaSize() const override{
                 return 1;
             }
@@ -305,17 +291,12 @@
             { return _compiled->distance(context); }
             void toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const override
             { _compiled->toTAPAALQuery(out, context); }
-            void toBinary(std::ostream& out) const override
-            { return _compiled->toBinary(out); }
             Retval simplify(SimplificationContext& context) const override
             { return _compiled->simplify(context); }
             Condition_ptr prepareForReachability(bool negated) const override
             { return _compiled->prepareForReachability(negated); }
             bool isReachability(uint32_t depth) const override
             { return _compiled->isReachability(depth); }
-
-            void toXML(std::ostream& out, uint32_t tabs) const override
-            { _compiled->toXML(out, tabs); }
             void toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const override{
             }
 
@@ -383,8 +364,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
-            void toBinary(std::ostream&) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
 
@@ -427,7 +406,7 @@
             Result evaluate(const EvaluationContext& context) override;
             Result evalAndSet(const EvaluationContext& context) override;
             void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
-            void toBinary(std::ostream& out) const override;
+            void visit(Visitor&) const override;
 
 
             virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
@@ -452,7 +431,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::pError; }
@@ -481,7 +459,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
             Path getPath() const override             { return Path::pError; }
@@ -521,7 +498,6 @@
 
           Retval simplify(SimplificationContext &context) const override;
 
-          void toXML(std::ostream &, uint32_t tabs) const override;
           void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
           Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
@@ -563,7 +539,6 @@
                 assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
             }
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
             Path getPath() const override             { return Path::F; }
@@ -591,7 +566,6 @@
             }
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             Retval simplify(SimplificationContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
             Path getPath() const override             { return Path::X; }
@@ -613,7 +587,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::X; }
@@ -634,7 +607,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::G; }
@@ -656,7 +628,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::F; }
@@ -676,7 +647,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
             Path getPath() const override             { return Path::X; }
@@ -696,7 +666,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
             Path getPath() const override             { return Path::G; }
@@ -716,7 +685,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
             Path getPath() const override             { return Path::F; }
@@ -744,7 +712,6 @@
             void analyze(AnalysisContext& context) override;
             Result evaluate(const EvaluationContext& context) override;
             void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
-            void toBinary(std::ostream& out) const override;
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
 
@@ -758,12 +725,11 @@
 
             [[nodiscard]] const Condition_ptr& getCond1() const { return (*this)[0]; }
             [[nodiscard]] const Condition_ptr& getCond2() const { return (*this)[1]; }
-            
+
             Retval simplify(SimplificationContext& context) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void visit(Visitor&) const override;
             void visit(MutatingVisitor&) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             uint32_t distance(DistanceContext& context) const override { return (*this)[1]->distance(context); }
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
@@ -785,7 +751,6 @@
             void visit(MutatingVisitor&) override;
             uint32_t distance(DistanceContext& context) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
         private:
@@ -800,7 +765,6 @@
             void visit(Visitor&) const override;
             void visit(MutatingVisitor&) override;
             uint32_t distance(DistanceContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             virtual bool isLoopSensitive() const override { return true; }
@@ -819,7 +783,6 @@
             std::string getName() const {
                 return _name;
             }
-            void toXML(std::ostream& out, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
         protected:
             void _analyze(AnalysisContext& context) override;
@@ -859,7 +822,7 @@
 
             void analyze(AnalysisContext& context) override;
 
-            void toBinary(std::ostream& out) const override;
+            void visit(Visitor&) const override;
             void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
@@ -916,7 +879,6 @@
             Result evalAndSet(const EvaluationContext& context) override;
             void visit(Visitor&) const override;
             void visit(MutatingVisitor&) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::AND; }
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
@@ -941,7 +903,6 @@
             Result evalAndSet(const EvaluationContext& context) override;
             void visit(Visitor&) const override;
             void visit(MutatingVisitor&) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             Quantifier getQuantifier() const override { return Quantifier::OR; }
@@ -1024,12 +985,10 @@
             void analyze(AnalysisContext& context) override;
             uint32_t distance(DistanceContext& context) const override;
             void toTAPAALQuery(std::ostream& stream,TAPAALConditionExportContext& context) const override;
-            void toBinary(std::ostream& out) const override;
             bool isReachability(uint32_t depth) const override { return depth > 0; };
             Condition_ptr prepareForReachability(bool negated) const override;
             CTLType getQueryType() const override { return CTLType::LOPERATOR; }
             Path getPath() const override         { return Path::pError; }
-            virtual void toXML(std::ostream& stream, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Retval simplify(SimplificationContext& context) const override;
             Result evaluate(const EvaluationContext& context) override;
@@ -1071,7 +1030,7 @@
             Result evaluate(const EvaluationContext& context) override;
             Result evalAndSet(const EvaluationContext& context) override;
             void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
-            void toBinary(std::ostream& out) const override;
+            void visit(Visitor&) const override;
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
@@ -1090,6 +1049,8 @@
 
             [[nodiscard]] const Expr_ptr &getExpr2() const { return _expr2; }
 
+            virtual std::string op() const = 0;
+
         protected:
             uint32_t _distance(DistanceContext& c,
                     std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
@@ -1098,7 +1059,6 @@
             }
         private:
             virtual bool apply(int v1, int v2) const = 0;
-            virtual std::string op() const = 0;
             /** Operator when exported to TAPAAL */
             virtual std::string opTAPAAL() const = 0;
             /** Swapped operator when exported to TAPAAL, e.g. operator when operands are swapped */
@@ -1119,7 +1079,6 @@
 
             using CompareCondition::CompareCondition;
             Retval simplify(SimplificationContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             uint32_t distance(DistanceContext& context) const override;
@@ -1140,7 +1099,6 @@
             using CompareCondition::CompareCondition;
             void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
             Retval simplify(SimplificationContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
 
@@ -1161,7 +1119,6 @@
 
             using CompareCondition::CompareCondition;
             Retval simplify(SimplificationContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             uint32_t distance(DistanceContext& context) const override;
@@ -1181,7 +1138,6 @@
 
             using CompareCondition::CompareCondition;
             Retval simplify(SimplificationContext& context) const override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             uint32_t distance(DistanceContext& context) const override;
@@ -1223,8 +1179,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
-            void toBinary(std::ostream&) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
@@ -1256,8 +1210,6 @@
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
-            void toBinary(std::ostream&) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             static Condition_ptr DEADLOCK;
@@ -1385,12 +1337,10 @@
             void visit(MutatingVisitor&) override;
             uint32_t distance(DistanceContext& context) const override;
             void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
-            void toBinary(std::ostream&) const override;
             Retval simplify(SimplificationContext& context) const override;
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
-            void toXML(std::ostream&, uint32_t tabs) const override;
             void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             Quantifier getQuantifier() const override { return Quantifier::UPPERBOUNDS; }
@@ -1410,6 +1360,9 @@
 
             const std::vector<place_t>& places() const { return _places; }
 
+            double getMax() const { return _max; }
+            double getOffset() const { return _offset; }
+
         private:
             std::vector<place_t> _places;
             size_t _bound = 0;
 
=== modified file 'include/PetriEngine/PQL/PQL.h'
--- include/PetriEngine/PQL/PQL.h	2021-06-01 08:40:18 +0000
+++ include/PetriEngine/PQL/PQL.h	2021-10-18 11:40:53 +0000
@@ -118,8 +118,6 @@
             /** Construct left/right side of equations used in query simplification */
             virtual Simplification::Member constraint(SimplificationContext& context) const = 0;
             /** Output the expression as it currently is to a file in XML */
-            virtual void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const = 0;
-            virtual void toBinary(std::ostream&) const = 0;
             virtual void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const = 0;
 
             /** Count size of the entire formula in number of nodes */
@@ -231,9 +229,7 @@
             [[nodiscard]] virtual std::shared_ptr<Condition> pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated = false, bool initrw = true) = 0;
             
             /** Output the condition as it currently is to a file in XML */
-            virtual void toXML(std::ostream&, uint32_t tabs) const = 0;
             virtual void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const = 0;
-            virtual void toBinary(std::ostream& out) const = 0;
 
             /** Checks if the condition is trivially true */
             [[nodiscard]] bool isTriviallyTrue();
 
=== modified file 'include/PetriEngine/PQL/Visitor.h'
--- include/PetriEngine/PQL/Visitor.h	2021-04-29 07:47:52 +0000
+++ include/PetriEngine/PQL/Visitor.h	2021-10-18 11:40:53 +0000
@@ -30,101 +30,119 @@
 
         protected:
             virtual void _accept(const NotCondition* element) = 0;
-            virtual void _accept(const AndCondition* element) = 0;
-            virtual void _accept(const OrCondition* element) = 0;
-            virtual void _accept(const LessThanCondition* element) = 0;
-            virtual void _accept(const LessThanOrEqualCondition* element) = 0;
-            virtual void _accept(const EqualCondition* element) = 0;
-            virtual void _accept(const NotEqualCondition* element) = 0;
+
+            virtual void _accept(const AndCondition* element) {
+                element->LogicalCondition::visit(*this);
+            }
+
+            virtual void _accept(const OrCondition* element) {
+                element->LogicalCondition::visit(*this);
+            }
+
+            virtual void _accept(const LessThanCondition* element) {
+                element->CompareCondition::visit(*this);
+            }
+
+            virtual void _accept(const LessThanOrEqualCondition* element) {
+                element->CompareCondition::visit(*this);
+            }
+
+            virtual void _accept(const EqualCondition* element) {
+                element->CompareCondition::visit(*this);
+            }
+
+            virtual void _accept(const NotEqualCondition* element) {
+                element->CompareCondition::visit(*this);
+            }
 
             virtual void _accept(const DeadlockCondition* element) = 0;
             virtual void _accept(const CompareConjunction* element) = 0;
             virtual void _accept(const UnfoldedUpperBoundsCondition* element) = 0;
 
+            // Super classes, the default implementation of subclasses is to call these
+            virtual void _accept(const CommutativeExpr *element) {
+                assert(false);
+                std::cerr << "No accept for CommutativeExpr (may be called from subclass)" << std::endl;
+                exit(0);
+            }
+
+            virtual void _accept(const SimpleQuantifierCondition *element) {
+                assert(false);
+                std::cerr << "No accept for SimpleQuantifierCondition (may be called from subclass)" << std::endl;
+                exit(0);
+            }
+
+            virtual void _accept(const LogicalCondition *element) {
+                assert(false);
+                std::cerr << "No accept for LogicalCondition (may be called from subclass)" << std::endl;
+                exit(0);
+            }
+
+            virtual void _accept(const CompareCondition *element) {
+                assert(false);
+                std::cerr << "No accept for CompareCondition (may be called from subclass)" << std::endl;
+                exit(0);
+            }
+
+            virtual void _accept(const UntilCondition *element) {
+                assert(false);
+                std::cerr << "No accept for UntilCondition (may be called from subclass)" << std::endl;
+                exit(0);
+            }
+
+
             // Quantifiers, most uses of the visitor will not use the quantifiers - so we give a default implementation.
             // default behaviour is error
-            virtual void _accept(const EFCondition *) {
-                assert(false);
-                std::cerr << "No accept for EFCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const EGCondition *) {
-                assert(false);
-                std::cerr << "No accept for EGCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const AGCondition *) {
-                assert(false);
-                std::cerr << "No accept for AGCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const AFCondition *) {
-                assert(false);
-                std::cerr << "No accept for AFCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const EXCondition *) {
-                assert(false);
-                std::cerr << "No accept for EXCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const AXCondition *) {
-                assert(false);
-                std::cerr << "No accept for AXCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const EUCondition *) {
-                assert(false);
-                std::cerr << "No accept for EUCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const AUCondition *) {
-                assert(false);
-                std::cerr << "No accept for AUCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const ACondition *) {
-                assert(false);
-                std::cerr << "No accept for ACondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const ECondition *) {
-                assert(false);
-                std::cerr << "No accept for ECondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const GCondition *) {
-                assert(false);
-                std::cerr << "No accept for GCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const FCondition *) {
-                assert(false);
-                std::cerr << "No accept for FCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const XCondition *) {
-                assert(false);
-                std::cerr << "No accept for XCondition" << std::endl;
-                exit(0);
-            };
-
-            virtual void _accept(const UntilCondition *) {
-                assert(false);
-                std::cerr << "No accept for UntilCondition" << std::endl;
-                exit(0);
+            virtual void _accept(const EFCondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const EGCondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const AGCondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const AFCondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const EXCondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const AXCondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const EUCondition *condition) {
+                condition->UntilCondition::visit(*this);
+            };
+
+            virtual void _accept(const AUCondition *condition) {
+                condition->UntilCondition::visit(*this);
+            };
+
+            virtual void _accept(const ACondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const ECondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const GCondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const FCondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
+            };
+
+            virtual void _accept(const XCondition *condition) {
+                condition->SimpleQuantifierCondition::visit(*this);
             };
 
             // shallow elements, neither of these should exist in a compiled expression
@@ -176,14 +194,24 @@
                 exit(0);
             };
 
+            virtual void _accept(const ShallowCondition *element) {
+                assert(false);
+                std::cerr << "No accept for BooleanCondition" << std::endl;
+                exit(0);
+            }
+
             // Expression
             virtual void _accept(const UnfoldedIdentifierExpr *element) = 0;
 
             virtual void _accept(const LiteralExpr *element) = 0;
 
-            virtual void _accept(const PlusExpr *element) = 0;
+            virtual void _accept(const PlusExpr *element) {
+                element->CommutativeExpr::visit(*this);
+            };
 
-            virtual void _accept(const MultiplyExpr *element) = 0;
+            virtual void _accept(const MultiplyExpr *element) {
+                element->CommutativeExpr::visit(*this);
+            };
 
             virtual void _accept(const MinusExpr *element) = 0;
 
 
=== added file 'include/PetriEngine/PQL/XMLPrinter.h'
--- include/PetriEngine/PQL/XMLPrinter.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PQL/XMLPrinter.h	2021-10-18 11:40:53 +0000
@@ -0,0 +1,119 @@
+/* Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>,
+ *                     Rasmus Tollund <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#ifndef VERIFYPN_XMLPRINTER_H
+#define VERIFYPN_XMLPRINTER_H
+
+#include <iostream>
+#include "Visitor.h"
+
+namespace PetriEngine {
+    namespace PQL {
+        class XMLPrinter : public Visitor {
+        public:
+            XMLPrinter(std::ostream& os, uint32_t init_tabs = 0, uint32_t tab_size = 2, bool print_newlines = true, bool token_count = false) :
+                os(os), tabs(init_tabs), tab_size(tab_size), single_tab(std::string(tab_size, ' ')), print_newlines(print_newlines), token_count(token_count) {}
+
+        protected:
+            std::ostream& os;
+            const bool token_count;
+            uint32_t tabs;
+            const uint32_t tab_size;
+            const std::string single_tab;
+            const bool print_newlines;
+
+            std::ostream & generateTabs();
+
+            void openXmlTag(const std::string& tag);
+            void closeXmlTag(const std::string &tag);
+            void outputLine(const std::string &line);
+
+            void _accept(const NotCondition *element) override;
+
+            void _accept(const AndCondition *element) override;
+
+            void _accept(const OrCondition *element) override;
+
+            void _accept(const LessThanCondition *element) override;
+
+            void _accept(const LessThanOrEqualCondition *element) override;
+
+            void _accept(const EqualCondition *element) override;
+
+            void _accept(const NotEqualCondition *element) override;
+
+            void _accept(const DeadlockCondition *element) override;
+
+            void _accept(const CompareConjunction *element) override;
+
+            void _accept(const UnfoldedUpperBoundsCondition *element) override;
+
+            void _accept(const EFCondition *condition) override;
+
+            void _accept(const EGCondition *condition) override;
+
+            void _accept(const AGCondition *condition) override;
+
+            void _accept(const AFCondition *condition) override;
+
+            void _accept(const EXCondition *condition) override;
+
+            void _accept(const AXCondition *condition) override;
+
+            void _accept(const EUCondition *condition) override;
+
+            void _accept(const AUCondition *condition) override;
+
+            void _accept(const ACondition *condition) override;
+
+            void _accept(const ECondition *condition) override;
+
+            void _accept(const GCondition *condition) override;
+
+            void _accept(const FCondition *condition) override;
+
+            void _accept(const XCondition *condition) override;
+
+            void _accept(const UntilCondition *condition) override;
+
+            void _accept(const UnfoldedFireableCondition *element) override;
+
+            void _accept(const BooleanCondition *element) override;
+
+            void _accept(const ShallowCondition *element) override;
+
+            void _accept(const UnfoldedIdentifierExpr *element) override;
+
+            void _accept(const LiteralExpr *element) override;
+
+            void _accept(const PlusExpr *element) override;
+
+            void _accept(const MultiplyExpr *element) override;
+
+            void _accept(const MinusExpr *element) override;
+
+            void _accept(const SubtractExpr *element) override;
+
+            void _accept(const IdentifierExpr *element) override;
+
+        };
+    }
+}
+
+#endif //VERIFYPN_XMLPRINTER_H
 
=== added file 'src/PetriEngine/PQL/BinaryPrinter.cpp'
--- src/PetriEngine/PQL/BinaryPrinter.cpp	1970-01-01 00:00:00 +0000
+++ src/PetriEngine/PQL/BinaryPrinter.cpp	2021-10-18 11:40:53 +0000
@@ -0,0 +1,173 @@
+/* Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>,
+ *                     Rasmus Tollund <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHos ANY WARRANTY; withos even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#include "PetriEngine/PQL/BinaryPrinter.h"
+
+namespace PetriEngine::PQL {
+    void BinaryPrinter::_accept(const LiteralExpr *element){
+        os.write("l", sizeof(char));
+        int temp = element->value();
+        os.write(reinterpret_cast<const char*>(&temp), sizeof(int));
+    }
+
+    void BinaryPrinter::_accept(const UnfoldedIdentifierExpr *element){
+        os.write("i", sizeof(char));
+        int temp = element->offset();
+        os.write(reinterpret_cast<const char*>(&temp), sizeof(int));
+    }
+
+    void BinaryPrinter::_accept(const MinusExpr *element){
+        auto e1 = std::make_shared<PQL::LiteralExpr>(0);
+        std::vector<Expr_ptr> exprs;
+        exprs.push_back(e1);
+        exprs.push_back((*element)[0]);
+        PQL::SubtractExpr(std::move(exprs)).visit(*this);
+    }
+
+    void BinaryPrinter::_accept(const SubtractExpr *element){
+        os.write("-", sizeof(char));
+        uint32_t size = element->expressions().size();
+        os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
+        for(auto& e : element->expressions())
+            e->visit(*this);
+    }
+
+    void BinaryPrinter::_accept(const CommutativeExpr *element){
+        auto sop = element->op();
+        os.write(&sop[0], sizeof(char));
+        int32_t temp_constant = element->constant();
+        os.write(reinterpret_cast<const char*>(&temp_constant), sizeof(int32_t));
+        uint32_t size = element->places().size();
+        os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
+        size = element->expressions().size();
+        os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
+        for(auto& id : element->places())
+            os.write(reinterpret_cast<const char*>(&id.first), sizeof(uint32_t));
+        for(auto& e : element->expressions())
+            e->visit(*this);
+    }
+
+    void BinaryPrinter::_accept(const SimpleQuantifierCondition *condition){
+        auto path = condition->getPath();
+        auto quant = condition->getQuantifier();
+        os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
+        os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
+        condition->getCond()->visit(*this);
+    }
+
+    void BinaryPrinter::_accept(const UntilCondition *condition){
+        auto path = condition->getPath();
+        auto quant = condition->getQuantifier();
+        os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
+        os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
+        (*condition)[0]->visit(*this);
+        (*condition)[1]->visit(*this);
+    }
+
+    void BinaryPrinter::_accept(const LogicalCondition *condition){
+        auto path = condition->getPath();
+        auto quant = condition->getQuantifier();
+        os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
+        os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
+        uint32_t size = condition->operands();
+        os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
+        for(auto& c : *condition)
+            c->visit(*this);
+    }
+
+    void BinaryPrinter::_accept(const CompareConjunction *element){
+        auto path = element->getPath();
+        auto quant = Quantifier::COMPCONJ;
+        os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
+        os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
+        bool temp = element->isNegated();
+        os.write(reinterpret_cast<const char*>(&temp), sizeof(bool));
+        uint32_t size = element->constraints().size();
+        os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
+        for(auto& c : element->constraints())
+        {
+            os.write(reinterpret_cast<const char*>(&c._place), sizeof(int32_t));
+            os.write(reinterpret_cast<const char*>(&c._lower), sizeof(uint32_t));
+            os.write(reinterpret_cast<const char*>(&c._upper), sizeof(uint32_t));
+        }
+    }
+
+    void BinaryPrinter::_accept(const CompareCondition *condition){
+        auto path = condition->getPath();
+        auto quant = condition->getQuantifier();
+        os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
+        os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
+        std::string sop = condition->op();
+        os.write(sop.data(), sop.size());
+        os.write("\0", sizeof(char));
+        (*condition)[0]->visit(*this);
+        (*condition)[1]->visit(*this);
+    }
+
+    void BinaryPrinter::_accept(const DeadlockCondition *condition){
+        auto path = condition->getPath();
+        auto quant = Quantifier::DEADLOCK;
+        os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
+        os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
+    }
+
+    void BinaryPrinter::_accept(const BooleanCondition *condition){
+        auto path = condition->getPath();
+        auto quant = Quantifier::PN_BOOLEAN;
+        os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
+        os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
+        os.write(reinterpret_cast<const char*>(&condition->value), sizeof(bool));
+    }
+
+    void BinaryPrinter::_accept(const UnfoldedUpperBoundsCondition *condition){
+        auto path = condition->getPath();
+        auto quant = Quantifier::UPPERBOUNDS;
+        os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
+        os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
+        uint32_t size = condition->places().size();
+        os.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
+        double temp_max = condition->getMax();
+        os.write(reinterpret_cast<const char*>(&temp_max), sizeof(double));
+        double temp_offset = condition->getOffset();
+        os.write(reinterpret_cast<const char*>(&temp_offset), sizeof(double));
+        for(auto& b : condition->places())
+        {
+            os.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t));
+            os.write(reinterpret_cast<const char*>(&b._max), sizeof(double));
+        }
+    }
+
+    void BinaryPrinter::_accept(const NotCondition *condition){
+        auto path = condition->getPath();
+        auto quant = condition->getQuantifier();
+        os.write(reinterpret_cast<const char*>(&path), sizeof(Path));
+        os.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
+        condition->getCond()->visit(*this);
+    }
+
+    void BinaryPrinter::_accept(const IdentifierExpr *condition) {
+        condition->compiled()->visit(*this);
+    }
+
+    void BinaryPrinter::_accept(const ShallowCondition *condition) {
+        condition->getCompiled()->visit(*this);
+    }
+
+
+}
 
=== modified file 'src/PetriEngine/PQL/CMakeLists.txt'
--- src/PetriEngine/PQL/CMakeLists.txt	2021-08-11 09:06:51 +0000
+++ src/PetriEngine/PQL/CMakeLists.txt	2021-10-18 11:40:53 +0000
@@ -8,7 +8,7 @@
 
 add_flex_bison_dependency(pql_lexer pql_parser)
 
-add_library(PQL ${BISON_pql_parser_OUTPUTS} ${FLEX_pql_lexer_OUTPUTS} Expressions.cpp PQL.cpp Contexts.cpp QueryPrinter.cpp CTLVisitor.cpp)
+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)
 add_dependencies(PQL glpk-ext)
 target_link_libraries(PQL Simplification Reachability glpk PetriEngine)
 
 
=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
--- src/PetriEngine/PQL/Expressions.cpp	2021-10-03 14:50:33 +0000
+++ src/PetriEngine/PQL/Expressions.cpp	2021-10-18 11:40:53 +0000
@@ -976,6 +976,10 @@
 
         /******************** Range Contexts ********************/
 
+        void SimpleQuantifierCondition::visit(Visitor& ctx) const {
+            ctx.accept<decltype(this)>(this);
+        }
+
         void UntilCondition::visit(Visitor &ctx) const
         {
             ctx.accept<decltype(this)>(this);
@@ -1046,6 +1050,10 @@
             ctx.accept<decltype(this)>(this);
         }
 
+        void LogicalCondition::visit(Visitor& ctx) const {
+            ctx.accept<decltype(this)>(this);
+        }
+
         void AndCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
@@ -1060,7 +1068,15 @@
         {
             ctx.accept<decltype(this)>(this);
         }
-
+<<<<<<< TREE
+
+=======
+
+        void CompareCondition::visit(Visitor& ctx) const {
+            ctx.accept<decltype(this)>(this);
+        }
+        
+>>>>>>> MERGE-SOURCE
         void EqualCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
@@ -1176,6 +1192,10 @@
             ctx.accept<decltype(this)>(this);
         }
 
+        void CommutativeExpr::visit(Visitor& ctx) const {
+            ctx.accept<decltype(this)>(this);
+        }
+
         void MinusExpr::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
@@ -1757,6 +1777,7 @@
         }
 
         /******************** BIN output ********************/
+<<<<<<< TREE
 
         void LiteralExpr::toBinary(std::ostream& out) const {
             out.write("l", sizeof(char));
@@ -1908,15 +1929,16 @@
         void LiteralExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
             generateTabs(out,tabs) << "<integer-constant>" + std::to_string(_value) + "</integer-constant>\n";
         }
+=======
+        
+
+        /******************** CTL Output ********************/
+>>>>>>> MERGE-SOURCE
 
         void LiteralExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
             out << "<integer-constant>" + std::to_string(_value) + "</integer-constant>\n";
         }
 
-        void UnfoldedFireableCondition::toXML(std::ostream& out, uint32_t tabs) const{
-            generateTabs(out, tabs) << "<is-fireable><transition>" + _name << "</transition></is-fireable>\n";
-        }
-
         void UnfoldedFireableCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<is-fireable><transition>" + _name << "</transition></is-fireable>\n";
         }
@@ -1944,6 +1966,7 @@
                 out << "</is-fireable>";
             }
         }
+<<<<<<< TREE
 
         void UnfoldedIdentifierExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
             if (tokencount) {
@@ -1956,6 +1979,8 @@
                 generateTabs(out,tabs) << "</tokens-count>\n";
             }
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void UnfoldedIdentifierExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
             if (tokencount) {
@@ -1997,6 +2022,7 @@
                 }
             }
         }
+<<<<<<< TREE
 
         void PlusExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
             if (tokencount) {
@@ -2022,6 +2048,8 @@
             for(auto& e : _exprs) e->toXML(ss,tabs+1, tokencount);
             generateTabs(ss,tabs) << "</integer-sum>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void PlusExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
             if (tokencount) {
@@ -2047,30 +2075,37 @@
             for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);
             out << "</integer-sum>\n";
         }
+<<<<<<< TREE
 
         void SubtractExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
             generateTabs(ss,tabs) << "<integer-difference>\n";
             for(auto& e : _exprs) e->toXML(ss,tabs+1);
             generateTabs(ss,tabs) << "</integer-difference>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void SubtractExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
             out << "<integer-difference>\n";
             for(auto& e : _exprs) e->toCompactXML(out,tabs, context);
             out << "</integer-difference>\n";
         }
+<<<<<<< TREE
 
         void MultiplyExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
             generateTabs(ss,tabs) << "<integer-product>\n";
             for(auto& e : _exprs) e->toXML(ss,tabs+1);
             generateTabs(ss,tabs) << "</integer-product>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void MultiplyExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
             out << "<integer-product>\n";
             for(auto& e : _exprs) e->toCompactXML(out,tabs, context);
             out << "</integer-product>\n";
         }
+<<<<<<< TREE
 
         void MinusExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
 
@@ -2081,6 +2116,8 @@
                     "<integer-constant>1</integer-constant>\n" ; generateTabs(out,tabs+1) <<
                     "</integer-difference>\n" ; generateTabs(out,tabs) << "</integer-product>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void MinusExpr::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount) const{
             out << "<integer-product>\n";
@@ -2090,12 +2127,15 @@
                     "<integer-constant>1</integer-constant>\n" ; out <<
                     "</integer-difference>\n" ; out << "</integer-product>\n";
         }
+<<<<<<< TREE
 
         void EXCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<next>\n";
             _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) << "</next>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void EXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<exists-path>\n" ; out << "<next>\n";
@@ -2103,6 +2143,7 @@
             out << "</next>\n" ; out << "</exists-path>\n";
         }
 
+<<<<<<< TREE
         void AXCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<all-paths>\n"; generateTabs(out,tabs+1) << "<next>\n";
             _cond->toXML(out,tabs+2);
@@ -2110,58 +2151,74 @@
         }
 
         void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             out << "<all-paths>\n" ;out << "<next>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</next>\n" ; out << "</all-paths>\n";
         }
+<<<<<<< TREE
 
         void EFCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
             _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void EFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<exists-path>\n" ;out << "<finally>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</finally>\n" ; out << "</exists-path>\n";
         }
+<<<<<<< TREE
 
         void AFCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
             _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void AFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<all-paths>\n" ;out << "<finally>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</finally>\n" ; out << "</all-paths>\n";
         }
+<<<<<<< TREE
 
         void EGCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
             _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) <<  "</globally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void EGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<exists-path>\n" ;out << "<globally>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</globally>\n" ; out << "</exists-path>\n";
         }
+<<<<<<< TREE
 
         void AGCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
             _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void AGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<all-paths>\n" ;out << "<globally>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</globally>\n" ; out << "</all-paths>\n";
         }
+<<<<<<< TREE
 
         void EUCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
@@ -2170,6 +2227,8 @@
             _cond2->toXML(out,tabs+3);
             generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void EUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<exists-path>\n" ; out << "<until>\n" ; out << "<before>\n";
@@ -2178,6 +2237,7 @@
             _cond2->toCompactXML(out,tabs+2, context);
             out << "</reach>\n" ; out << "</until>\n" ; out << "</exists-path>\n";
         }
+<<<<<<< TREE
 
         void AUCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
@@ -2186,6 +2246,8 @@
             _cond2->toXML(out,tabs+3);
             generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void AUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<all-paths>\n" ; out << "<until>\n" ; out << "<before>\n";
@@ -2195,6 +2257,7 @@
             out << "</reach>\n" ; out << "</until>\n" ; out << "</all-paths>\n";
         }
 
+<<<<<<< TREE
         void ACondition::toXML(std::ostream& out, uint32_t tabs) const {
             generateTabs(out, tabs) << "<all-paths>\n";
             _cond->toXML(out, tabs+1);
@@ -2202,11 +2265,15 @@
         }
 
         void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             out << "<all-paths>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</all-paths>\n";
         }
 
+<<<<<<< TREE
         void ECondition::toXML(std::ostream& out, uint32_t tabs) const {
             generateTabs(out, tabs) << "<exists-path>\n";
             _cond->toXML(out, tabs+1);
@@ -2214,11 +2281,15 @@
         }
 
         void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             out << "<exists-path>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</exists-path>\n";
         }
 
+<<<<<<< TREE
         void FCondition::toXML(std::ostream& out, uint32_t tabs) const {
             generateTabs(out, tabs) << "<finally>\n";
             _cond->toXML(out, tabs+1);
@@ -2226,11 +2297,15 @@
         }
 
         void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             out << "<finally>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</finally>\n";
         }
 
+<<<<<<< TREE
         void GCondition::toXML(std::ostream& out, uint32_t tabs) const {
             generateTabs(out, tabs) << "<globally>\n";
             _cond->toXML(out, tabs+1);
@@ -2238,11 +2313,15 @@
         }
 
         void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             out << "<globally>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</globally>\n";
         }
 
+<<<<<<< TREE
         void XCondition::toXML(std::ostream& out, uint32_t tabs) const {
             generateTabs(out, tabs) << "<next>\n";
             _cond->toXML(out, tabs+1);
@@ -2250,11 +2329,15 @@
         }
 
         void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             out << "<next>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</next>\n";
         }
 
+<<<<<<< TREE
         void UntilCondition::toXML(std::ostream& out, uint32_t tabs) const {
             generateTabs(out,tabs) << "<until>\n" ; generateTabs(out,tabs+1) << "<before>\n";
             _cond1->toXML(out,tabs+2);
@@ -2264,6 +2347,9 @@
         }
 
         void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             out << "<until>\n" ; out << "<before>\n";
             _cond1->toCompactXML(out,tabs+2, context);
             out << "</before>\n" ; out << "<reach>\n";
@@ -2271,6 +2357,7 @@
             out << "</reach>\n"; out << "</until>\n" ;
         }
 
+<<<<<<< TREE
         void AndCondition::toXML(std::ostream& out,uint32_t tabs) const {
             if(_conds.size() == 0)
             {
@@ -2304,6 +2391,9 @@
         }
 
         void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             if(_conds.size() == 0)
             {
                 BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);
@@ -2334,6 +2424,7 @@
             }
             out << "</conjunction>\n";
         }
+<<<<<<< TREE
 
         void OrCondition::toXML(std::ostream& out,uint32_t tabs) const {
             if(_conds.size() == 0)
@@ -2366,6 +2457,8 @@
             }
             generateTabs(out,tabs) << "</disjunction>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void OrCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             if(_conds.size() == 0)
@@ -2399,6 +2492,7 @@
             out << "</disjunction>\n";
         }
 
+<<<<<<< TREE
         void CompareConjunction::toXML(std::ostream& out, uint32_t tabs) const
         {
             if(_negated) generateTabs(out,tabs++) << "<negation>";
@@ -2438,6 +2532,9 @@
         }
 
         void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             if(_negated) out << "<negation>";
             if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);
             else
@@ -2474,6 +2571,7 @@
             if(_negated) out << "</negation>";
         }
 
+<<<<<<< TREE
         void EqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<integer-eq>\n";
             _expr1->toXML(out,tabs+1);
@@ -2482,11 +2580,15 @@
         }
 
         void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+=======
+        void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+>>>>>>> MERGE-SOURCE
             out << "<integer-eq>\n";
             _expr1->toCompactXML(out,tabs, context);
             _expr2->toCompactXML(out,tabs, context);
             out << "</integer-eq>\n";
         }
+<<<<<<< TREE
 
         void NotEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<integer-ne>\n";
@@ -2494,6 +2596,8 @@
             _expr2->toXML(out,tabs+1);
             generateTabs(out,tabs) << "</integer-ne>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void NotEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<integer-ne>\n";
@@ -2501,6 +2605,7 @@
             _expr2->toCompactXML(out,tabs, context);
             out << "</integer-ne>\n";
         }
+<<<<<<< TREE
 
         void LessThanCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<integer-lt>\n";
@@ -2508,6 +2613,8 @@
             _expr2->toXML(out,tabs+1);
             generateTabs(out,tabs) << "</integer-lt>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void LessThanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<integer-lt>\n";
@@ -2515,6 +2622,7 @@
             _expr2->toCompactXML(out,tabs, context);
             out << "</integer-lt>\n";
         }
+<<<<<<< TREE
 
         void LessThanOrEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<integer-le>\n";
@@ -2522,6 +2630,8 @@
             _expr2->toXML(out,tabs+1);
             generateTabs(out,tabs) << "</integer-le>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void LessThanOrEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<integer-le>\n";
@@ -2529,6 +2639,7 @@
             _expr2->toCompactXML(out,tabs, context);
             out << "</integer-le>\n";
         }
+<<<<<<< TREE
 
         void NotCondition::toXML(std::ostream& out,uint32_t tabs) const {
 
@@ -2536,12 +2647,15 @@
             _cond->toXML(out,tabs+1);
             generateTabs(out,tabs) << "</negation>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void NotCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<negation>\n";
             _cond->toCompactXML(out,tabs, context);
             out << "</negation>\n";
         }
+<<<<<<< TREE
 
         void BooleanCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<" <<
@@ -2558,10 +2672,19 @@
         void DeadlockCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<deadlock/>\n";
         }
+=======
+
+        void BooleanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+            out << "<" << 
+                    (value ? "true" : "false")
+                    << "/>\n"; 
+        }
+>>>>>>> MERGE-SOURCE
 
         void DeadlockCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<deadlock/>\n";
         }
+<<<<<<< TREE
 
         void UnfoldedUpperBoundsCondition::toXML(std::ostream& out, uint32_t tabs) const {
             generateTabs(out, tabs) << "<place-bound>\n";
@@ -2569,6 +2692,8 @@
                 generateTabs(out, tabs + 1) << "<place>" << p._name << "</place>\n";
             generateTabs(out, tabs) << "</place-bound>\n";
         }
+=======
+>>>>>>> MERGE-SOURCE
 
         void UnfoldedUpperBoundsCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<place-bound>\n";
@@ -4462,6 +4587,8 @@
             return false;
         }
 
+
+
     } // PQL
 } // PetriEngine
 
 
=== added file 'src/PetriEngine/PQL/XMLPrinter.cpp'
--- src/PetriEngine/PQL/XMLPrinter.cpp	1970-01-01 00:00:00 +0000
+++ src/PetriEngine/PQL/XMLPrinter.cpp	2021-10-18 11:40:53 +0000
@@ -0,0 +1,399 @@
+/* Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>,
+ *                     Rasmus Tollund <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#include "PetriEngine/PQL/XMLPrinter.h"
+namespace PetriEngine {
+    namespace PQL {
+        std::ostream& XMLPrinter::generateTabs() {
+            for(uint32_t i = 0; i < tabs; i++) {
+                os << single_tab;
+            }
+            return os;
+        }
+
+        void XMLPrinter::openXmlTag(const std::string &tag) {
+            generateTabs() << "<" << tag << (print_newlines? ">\n": ">");
+            tabs++;
+        }
+
+        void XMLPrinter::closeXmlTag(const std::string &tag) {
+            tabs--;
+            generateTabs() << "</" << tag << (print_newlines? ">\n": ">");
+        }
+
+        void XMLPrinter::outputLine(const std::string &line) {
+            generateTabs() << line << (print_newlines? "\n": "");
+
+        }
+
+        void XMLPrinter::_accept(const NotCondition *element) {
+            openXmlTag("negation");
+            element->getCond()->visit(*this);
+            closeXmlTag("negation");
+        }
+
+        void XMLPrinter::_accept(const AndCondition *element) {
+            if(element->empty())
+            {
+                BooleanCondition::TRUE_CONSTANT->visit(*this);
+                return;
+            }
+            if(element->size() == 1)
+            {
+                (*element)[0]->visit(*this);
+                return;
+            }
+            openXmlTag("conjunction");
+            (*element)[0]->visit(*this);
+            for(size_t i = 1; i < element->size(); ++i)
+            {
+                if(i + 1 == element->size())
+                {
+                    (*element)[i]->visit(*this);
+                }
+                else
+                {
+                    openXmlTag("conjunction");
+                    (*element)[i]->visit(*this);
+                }
+            }
+            for(size_t i = element->size() - 1; i > 1; --i)
+            {
+                closeXmlTag("conjunction");
+            }
+            closeXmlTag("conjunction");
+        }
+
+        void XMLPrinter::_accept(const OrCondition *element) {
+            if(element->empty())
+            {
+                BooleanCondition::FALSE_CONSTANT->visit(*this);
+                return;
+            }
+            if(element->size() == 1)
+            {
+                (*element)[0]->visit(*this);
+                return;
+            }
+            openXmlTag("disjunction");
+            (*element)[0]->visit(*this);
+            for(size_t i = 1; i < element->size(); ++i)
+            {
+                if(i + 1 == element->size())
+                {
+                    (*element)[i]->visit(*this);
+                }
+                else
+                {
+                    openXmlTag("disjunction");
+                    (*element)[i]->visit(*this);
+                }
+            }
+            for(size_t i = element->size() - 1; i > 1; --i)
+            {
+                closeXmlTag("disjunction");
+            }
+            closeXmlTag("disjunction");
+        }
+
+        void XMLPrinter::_accept(const LessThanCondition *element) {
+            openXmlTag("integer-lt");
+            (*element)[0]->visit(*this);
+            (*element)[1]->visit(*this);
+            closeXmlTag("integer-lt");
+        }
+
+        void XMLPrinter::_accept(const LessThanOrEqualCondition *element) {
+            openXmlTag("integer-le");
+            (*element)[0]->visit(*this);
+            (*element)[1]->visit(*this);
+            closeXmlTag("integer-le");
+        }
+
+        void XMLPrinter::_accept(const EqualCondition *element) {
+            openXmlTag("integer-eq");
+            (*element)[0]->visit(*this);
+            (*element)[1]->visit(*this);
+            closeXmlTag("integer-eq");
+        }
+
+        void XMLPrinter::_accept(const NotEqualCondition *element) {
+            openXmlTag("integer-ne");
+            (*element)[0]->visit(*this);
+            (*element)[1]->visit(*this);
+            closeXmlTag("integer-ne");
+        }
+
+        void XMLPrinter::_accept(const DeadlockCondition *element) {
+            outputLine("<deadlock/>");
+        }
+
+        void XMLPrinter::_accept(const CompareConjunction *element) {
+            if(element->isNegated()) {
+                generateTabs() << "<negation>";
+            }
+
+            if(element->constraints().empty()) BooleanCondition::TRUE_CONSTANT->visit(*this);
+            else
+            {
+                bool single = element->constraints().size() == 1 &&
+                              (element->constraints()[0]._lower == 0 ||
+                               element->constraints()[0]._upper == std::numeric_limits<uint32_t>::max());
+                if(!single)
+                    openXmlTag("conjunction");
+                for(auto& c : element->constraints())
+                {
+                    if(c._lower != 0)
+                    {
+                        openXmlTag("integer-ge");
+                        openXmlTag("tokens-count");
+                        outputLine("<place>" + c._name + "</place>");
+                        closeXmlTag("tokens-count");
+                        outputLine("<integer-constant>" + std::to_string(c._lower) + "</integer-constant>");
+                        closeXmlTag("integer-ge");
+                    }
+                    if(c._upper != std::numeric_limits<uint32_t>::max())
+                    {
+                        openXmlTag("integer-le");
+                        openXmlTag("tokens-count");
+                        outputLine("<place>" + c._name + "</place>");
+                        closeXmlTag("tokens-count");
+                        outputLine("<integer-constant>" + std::to_string(c._upper) + "</integer-constant>");
+                        closeXmlTag("integer-le");
+                    }
+                }
+                if(!single)
+                    closeXmlTag("conjunction");
+            }
+            if(element->isNegated()) {
+                generateTabs() << "</negation>";
+            }
+        }
+
+        void XMLPrinter::_accept(const UnfoldedUpperBoundsCondition *element) {
+            openXmlTag("place-bound");
+            for(auto& p : element->places()) {
+                outputLine("<place>" + p._name + "</place>");
+            }
+            closeXmlTag("place-bound");
+        }
+
+        void XMLPrinter::_accept(const EFCondition *condition) {
+            openXmlTag("exists-path");
+            openXmlTag("finally");
+            condition->getCond()->visit(*this);
+            closeXmlTag("finally");
+            closeXmlTag("exists-path");
+        }
+
+        void XMLPrinter::_accept(const EGCondition *condition) {
+            openXmlTag("exists-path");
+            openXmlTag("globally");
+            condition->getCond()->visit(*this);
+            closeXmlTag("globally");
+            closeXmlTag("exists-path");
+        }
+
+        void XMLPrinter::_accept(const AGCondition *condition) {
+            openXmlTag("all-paths");
+            openXmlTag("globally");
+            condition->getCond()->visit(*this);
+            closeXmlTag("globally");
+            closeXmlTag("all-paths");
+        }
+
+        void XMLPrinter::_accept(const AFCondition *condition) {
+            openXmlTag("all-paths");
+            openXmlTag("finally");
+            condition->getCond()->visit(*this);
+            closeXmlTag("finally");
+            closeXmlTag("all-paths");
+        }
+
+        void XMLPrinter::_accept(const EXCondition *condition) {
+            openXmlTag("exists-path");
+            openXmlTag("next");
+            condition->getCond()->visit(*this);
+            closeXmlTag("next");
+            closeXmlTag("exists-path");
+        }
+
+        void XMLPrinter::_accept(const AXCondition *condition) {
+            openXmlTag("all-paths");
+            openXmlTag("next");
+            condition->getCond()->visit(*this);
+            closeXmlTag("next");
+            closeXmlTag("all-paths");
+        }
+
+        void XMLPrinter::_accept(const EUCondition *condition) {
+            openXmlTag("exists-path");
+            openXmlTag("until");
+            openXmlTag("before");
+            (*condition)[0]->visit(*this);
+            closeXmlTag("before");
+            openXmlTag("reach");
+            (*condition)[1]->visit(*this);
+            closeXmlTag("reach");
+            closeXmlTag("until");
+            closeXmlTag("exists-path");
+        }
+
+        void XMLPrinter::_accept(const AUCondition *condition) {
+            openXmlTag("all-paths");
+            openXmlTag("until");
+            openXmlTag("before");
+            (*condition)[0]->visit(*this);
+            closeXmlTag("before");
+            openXmlTag("reach");
+            (*condition)[1]->visit(*this);
+            closeXmlTag("reach");
+            closeXmlTag("until");
+            closeXmlTag("all-paths");
+
+        }
+
+        void XMLPrinter::_accept(const ACondition *condition) {
+            openXmlTag("all-paths");
+            condition->getCond()->visit(*this);
+            closeXmlTag("all-paths");
+        }
+
+        void XMLPrinter::_accept(const ECondition *condition) {
+            openXmlTag("exists-path");
+            condition->getCond()->visit(*this);
+            closeXmlTag("exists-path");
+        }
+
+        void XMLPrinter::_accept(const GCondition *condition) {
+            openXmlTag("globally");
+            condition->getCond()->visit(*this);
+            closeXmlTag("globally");
+        }
+
+        void XMLPrinter::_accept(const FCondition *condition) {
+            openXmlTag("finally");
+            condition->getCond()->visit(*this);
+            closeXmlTag("finally");
+        }
+
+        void XMLPrinter::_accept(const XCondition *condition) {
+            openXmlTag("next");
+            condition->getCond()->visit(*this);
+            closeXmlTag("next");
+        }
+
+        void XMLPrinter::_accept(const UntilCondition *condition) {
+            openXmlTag("until") ;
+            openXmlTag("before");
+            (*condition)[0]->visit(*this);
+            closeXmlTag("before") ;
+            openXmlTag("reach");
+            (*condition)[1]->visit(*this);
+            closeXmlTag("reach") ;
+            closeXmlTag("until") ;
+        }
+
+        void XMLPrinter::_accept(const UnfoldedFireableCondition *element) {
+            outputLine("<is-fireable><transition>" + element->getName() + "</transition></is-fireable>");
+        }
+
+        void XMLPrinter::_accept(const BooleanCondition *element) {
+            outputLine(element->value? "<true/>": "<false/>");
+        }
+
+        void XMLPrinter::_accept(const UnfoldedIdentifierExpr *element) {
+            if (token_count) {
+                outputLine("<place>" + element->name() + "</place>");
+            }
+            else
+            {
+                openXmlTag("tokens-count");
+                outputLine("<place>" + element->name() + "</place>");
+                closeXmlTag("tokens-count");
+            }
+        }
+
+        void XMLPrinter::_accept(const LiteralExpr *element) {
+            outputLine("<integer-constant>" + std::to_string(element->value()) + "</integer-constant>");
+        }
+
+        void XMLPrinter::_accept(const PlusExpr *element) {
+            if (token_count) {
+                for(auto& e : element->expressions())
+                    e->visit(*this);
+                return;
+            }
+
+            if(element->tk) {
+                openXmlTag("tokens-count");
+                for(auto& e : element->places())
+                    outputLine("<place>" + e.second + "</place>");
+                for(auto& e : element->expressions())
+                    e->visit(*this);
+                closeXmlTag("tokens-count");
+                return;
+            }
+            openXmlTag("integer-sum");
+            outputLine("<integer-constant>" + std::to_string(element->constant()) + "</integer-constant>");
+            for(auto& i : element->places())
+            {
+                openXmlTag("tokens-count");
+                outputLine("<place>" + i.second + "</place>");
+                closeXmlTag("tokens-count");
+            }
+            for(auto& e : element->expressions())
+                e->visit(*this);
+            closeXmlTag("integer-sum");
+        }
+
+        void XMLPrinter::_accept(const MultiplyExpr *element) {
+            openXmlTag("integer-product");
+            for(auto& e : element->expressions())
+                e->visit(*this);
+            closeXmlTag("integer-product");
+        }
+
+        void XMLPrinter::_accept(const MinusExpr *element) {
+            openXmlTag("integer-product");
+            (*element)[0]->visit(*this);
+            openXmlTag("integer-difference");
+            outputLine("<integer-constant>0</integer-constant>");
+            outputLine("<integer-constant>1</integer-constant>");
+            closeXmlTag("integer-difference");
+            closeXmlTag("integer-product");
+        }
+
+        void XMLPrinter::_accept(const SubtractExpr *element) {
+            openXmlTag("integer-difference");
+            for(auto& e : element->expressions())
+                e->visit(*this);
+            closeXmlTag("integer-difference");
+        }
+
+        void XMLPrinter::_accept(const IdentifierExpr *element) {
+            element->compiled()->visit(*this);
+        }
+
+        void XMLPrinter::_accept(const ShallowCondition *element) {
+            element->getCompiled()->visit(*this);
+        }
+    }
+}
+
 
=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp	2021-10-14 11:37:21 +0000
+++ src/VerifyPN.cpp	2021-10-18 11:40:53 +0000
@@ -75,6 +75,7 @@
 #include "PetriEngine/PetriNetBuilder.h"
 #include "PetriEngine/PQL/PQL.h"
 #include "PetriEngine/PQL/CTLVisitor.h"
+#include <PetriEngine/PQL/XMLPrinter.h>
 #include "PetriEngine/options.h"
 #include "PetriEngine/errorcodes.h"
 #include "PetriEngine/STSolver.h"
@@ -90,6 +91,7 @@
 #include "LTL/LTLMain.h"
 
 #include <atomic>
+#include <PetriEngine/PQL/BinaryPrinter.h>
 
 using namespace PetriEngine;
 using namespace PetriEngine::PQL;
@@ -940,7 +942,8 @@
             continue;
         }
         ss << "  <property>\n    <id>" << querynames[i] << "</id>\n    <description>Simplified</description>\n    <formula>\n";
-        queries[i]->toXML(ss, 3);
+        XMLPrinter xml_printer(ss, 3);
+        queries[i]->visit(xml_printer);
         ss << "    </formula>\n  </property>\n";
     }
 
@@ -985,12 +988,14 @@
         {
             out.write(querynames[i].data(), querynames[i].size());
             out.write("\0", sizeof(char));
-            queries[i]->toBinary(out);
+            BinaryPrinter binary_printer(out);
+            queries[i]->visit(binary_printer);
         }
         else
         {
             out << "  <property>\n    <id>" << querynames[i] << "</id>\n    <description>Simplified</description>\n    <formula>\n";
-            queries[i]->toXML(out, 3);
+            XMLPrinter xml_printer(out, 3);
+            queries[i]->visit(xml_printer);
             out << "    </formula>\n  </property>\n";
         }
     }