Merge lp:~tapaal-contributor/verifypn/unfoldTACPN into lp:verifypn

[Thomas Pedersen]

Merge in unfolding of TACPNs and adjust output of unfolded model and queries to fit with GUI

[lp:~tapaal-contributor/verifypn/unfoldTACPN]

235. By Thomas Pedersen <email address hidden> on 2021-02-25

Add colortype to dot colors and fix writing of arc weights

236. By Thomas Pedersen <email address hidden> on 2021-03-11

Expand timed net detection and handle missing invariants

237. By Thomas Pedersen <email address hidden> on 2021-04-08

Use same query writing method

238. By Thomas Pedersen <email address hidden> on 2021-04-12

Handle inhibitor arcs in CPNs

239. By Thomas Pedersen <email address hidden> on 2021-04-12

Remove expressions from inhibitor arcs and handle .all in tuples

240. By Thomas Pedersen <email address hidden> on 2021-04-19

Fix parsing of useroperators

Unmerged revisions

240. By Thomas Pedersen <email address hidden> on 2021-04-19

Fix parsing of useroperators

239. By Thomas Pedersen <email address hidden> on 2021-04-12

Remove expressions from inhibitor arcs and handle .all in tuples

238. By Thomas Pedersen <email address hidden> on 2021-04-12

Handle inhibitor arcs in CPNs

237. By Thomas Pedersen <email address hidden> on 2021-04-08

Use same query writing method

236. By Thomas Pedersen <email address hidden> on 2021-03-11

Expand timed net detection and handle missing invariants

235. By Thomas Pedersen <email address hidden> on 2021-02-25

Add colortype to dot colors and fix writing of arc weights

234. By Thomas Pedersen <email address hidden> on 2020-12-18

Merge with trunk

233. By Thomas Pedersen <email address hidden> on 2020-12-18

Adjust model and query output to work with gui

232. By Thomas Pedersen <email address hidden> on 2020-12-11

Fix some errors when passing colored net from GUI and creating reduced query

231. By Thomas Pedersen <email address hidden> on 2020-11-20

Fix parser check for time

=== modified file 'CMakeLists.txt'
--- CMakeLists.txt	2021-04-16 19:23:03 +0000
+++ CMakeLists.txt	2021-04-19 13:50:22 +0000
@@ -15,7 +15,11 @@
 set(CMAKE_POSITION_INDEPENDENT_CODE ON)
 
 
+<<<<<<< TREE
 set(VERIFYPN_VERSION 4.1.0)
+=======
+set(VERIFYPN_VERSION 4.0.0)
+>>>>>>> MERGE-SOURCE
 add_compile_definitions(VERIFYPN_VERSION=\"${VERIFYPN_VERSION}\")
 
 project(verifypn VERSION ${VERIFYPN_VERSION} LANGUAGES CXX C)

=== modified file 'include/PetriEngine/AbstractPetriNetBuilder.h'
--- include/PetriEngine/AbstractPetriNetBuilder.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/AbstractPetriNetBuilder.h	2021-04-19 13:50:22 +0000
@@ -25,6 +25,8 @@
 #include "PQL/PQL.h"
 #include "Colored/Multiset.h"
 #include "Colored/Expressions.h"
+#include "Colored/TimeInvariant.h"
+#include "Colored/TimeInterval.h"
 
 namespace PetriEngine {
 
@@ -32,6 +34,7 @@
     class AbstractPetriNetBuilder {
     protected:
         bool _isColored = false;
+        bool _isTimed = false;
         
     public:
         /** Add a new place with a unique name */
@@ -49,6 +52,35 @@
             std::cerr << "Colored places are not supported in standard P/T nets" << std::endl;
             exit(ErrorCode);
         }
+
+        virtual void addPlace(const std::string& name,
+                              Colored::Multiset&& tokens,
+                              Colored::ColorType* type,
+                              std::vector<Colored::TimeInvariant>& invariant,
+                              double x = 0,
+                              double y = 0)
+        {
+            std::cerr << "Colored timed places are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+        /** Adds a new colored and timed place with a unique name */
+        virtual void addPlace(const std::string& name,
+                int tokens,
+                Colored::TimeInvariant invariant,
+                double x = 0,
+                double y = 0)
+        {
+            std::cerr << "Colored timed places are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+
+        // add a time transition with a unique name
+        virtual void addTransition(const std::string &name, bool urgent,
+                                            double, double)
+        {
+            std::cerr << "Timed transitions are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
         /** Add a new transition with a unique name */
         virtual void addTransition(const std::string& name,
                 double x = 0,
@@ -62,6 +94,15 @@
             std::cerr << "Colored transitions are not supported in standard P/T nets" << std::endl;
             exit(ErrorCode);
         }
+        virtual void addTransition(const std::string& name,
+                                   const Colored::GuardExpression_ptr& guard,
+                                   bool urgent,
+                                   double x,
+                                   double y)
+        {
+            std::cerr << "Colored timed transitions are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
         /** Add input arc with given weight */
         virtual void addInputArc(const std::string& place,
                 const std::string& transition,
@@ -70,15 +111,36 @@
         /** Add colored input arc with given arc expression */
         virtual void addInputArc(const std::string& place,
                 const std::string& transition,
-                const Colored::ArcExpression_ptr& expr)
+                const Colored::ArcExpression_ptr& expr,
+                bool inhibitor,
+                int weight)
         {
             std::cerr << "Colored input arcs are not supported in standard P/T nets" << std::endl;
             exit(ErrorCode);
         }
+        /* Add timed colored input arc with given arc expression*/
+        virtual void addInputArc(const std::string &place,
+                const std::string &transition,
+                bool inhibitor, bool transport,
+                int weight,
+                PetriEngine::Colored::TimeInterval &interval, std::string transportID)
+        {
+            std::cerr << "Timed colored input arc are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+        virtual void addInputArc(const std::string &place,
+                                 const std::string &transition,
+                                 bool inhibitor, bool transport,
+                                 const Colored::ArcExpression_ptr& expr,
+                                 std::vector<PetriEngine::Colored::TimeInterval> &interval, int weight, std::string transportID)
+        {
+            std::cerr << "Timed colored input arc are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
         /** Add output arc with given weight */
         virtual void addOutputArc(const std::string& transition,
                 const std::string& place,
-                int weight = 1) = 0;
+                int weight = 1, bool transport = false, std::string transportID = "") = 0;
         /** Add output arc with given arc expression */
         virtual void addOutputArc(const std::string& transition,
                 const std::string& place,
@@ -87,6 +149,25 @@
             std::cerr << "Colored output arcs are not supported in standard P/T nets" << std::endl;
             exit(ErrorCode);
         }
+        virtual void addOutputArc(const std::string& transition,
+                                  const std::string& place,
+                                  const Colored::ArcExpression_ptr& expr, bool transport, std::string transportID)
+        {
+            std::cerr << "Colored output arcs are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+
+        /* Add transport arc with given arc expression */
+        virtual void addTransportArc(const std::string& source,
+                const std::string& transition,
+                const std::string& destination,
+                const Colored::ArcExpression_ptr& expr,
+                std::vector<Colored::TimeInterval>& interval)
+        {
+            std::cerr << "Transport arcs are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+
         /** Add color types with id */
         virtual void addColorType(const std::string& id,
                 Colored::ColorType* type)
@@ -103,6 +184,14 @@
             return _isColored;
         }
 
+        virtual void enableTimed() {
+            _isTimed = true;
+        }
+
+        virtual bool isTimed() const {
+            return _isTimed;
+        }
+
         virtual void sort() = 0;
         
         virtual ~AbstractPetriNetBuilder() {
@@ -112,3 +201,4 @@
 }
 
 #endif // ABSTRACTPETRINETBUILDER_H
+

=== modified file 'include/PetriEngine/Colored/ColoredNetStructures.h'
--- include/PetriEngine/Colored/ColoredNetStructures.h	2021-03-15 10:04:47 +0000
+++ include/PetriEngine/Colored/ColoredNetStructures.h	2021-04-19 13:50:22 +0000
@@ -26,6 +26,8 @@
 #include "Colors.h"
 #include "Expressions.h"
 #include "Multiset.h"
+#include "TimeInterval.h"
+#include "TimeInvariant.h"
 
 namespace PetriEngine {
     namespace Colored {
@@ -35,21 +37,42 @@
             uint32_t transition;
             ArcExpression_ptr expr;
             bool input;
+            bool inhibitor = false;
+            bool transport;
+            int weight;
+            std::vector<Colored::TimeInterval> interval;
+            std::string transportID;
+        };
+
+        struct TransportArc {
+            uint32_t source;
+            uint32_t transition;
+            uint32_t destination;
+            ArcExpression_ptr expr;
+            std::vector<Colored::TimeInterval> interval;
         };
         
         struct Transition {
             std::string name;
             GuardExpression_ptr guard;
+<<<<<<< TREE
             std::vector<Arc> input_arcs;
             std::vector<Arc> output_arcs;
             std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>> variableMaps;
             bool considered;
+=======
+            bool urgent;
+            std::vector<Arc> arcs;
+            //bool inhibitor = false;
+>>>>>>> MERGE-SOURCE
         };
         
         struct Place {
             std::string name;
             ColorType* type;
             Multiset marking;
+            std::vector<Colored::TimeInvariant> invariants;
+            //bool inhibitor = false;
         };
     }
 }

=== modified file 'include/PetriEngine/Colored/ColoredPetriNetBuilder.h'
--- include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2021-04-14 10:41:18 +0000
+++ include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2021-04-19 13:50:22 +0000
@@ -51,6 +51,12 @@
                 Colored::Multiset&& tokens,
                 double x = 0,
                 double y = 0) override;
+        void addPlace(const std::string& name,
+                      Colored::Multiset&& tokens,
+                      Colored::ColorType* type,
+                      std::vector<Colored::TimeInvariant>& invariant,
+                      double x = 0,
+                      double y = 0) override;
         void addTransition(const std::string& name,
                 double x = 0,
                 double y = 0) override;
@@ -58,22 +64,49 @@
                 const Colored::GuardExpression_ptr& guard,
                 double x = 0,
                 double y = 0) override;
+        void addTransition(const std::string& name,
+                           const Colored::GuardExpression_ptr& guard,
+                           bool urgent,
+                           double x,
+                           double y) override;
         void addInputArc(const std::string& place,
                 const std::string& transition,
                 bool inhibitor,
                 int) override;
+         void addInputArc(const std::string &place,
+                const std::string &transition,
+                bool inhibitor, bool transport,
+                const Colored::ArcExpression_ptr& expr,
+                std::vector<PetriEngine::Colored::TimeInterval> &interval, 
+                int weight, 
+                std::string transportID) override;
         void addInputArc(const std::string& place,
                 const std::string& transition,
-                const Colored::ArcExpression_ptr& expr) override;
-        void addOutputArc(const std::string& transition,
-                const std::string& place,
-                int weight = 1) override;
-        void addOutputArc(const std::string& transition,
-                const std::string& place,
-                const Colored::ArcExpression_ptr& expr) override;
+                const Colored::ArcExpression_ptr& expr,
+                bool inhibitor,
+                int weight) override;
+
+        void addOutputArc(const std::string& transition, 
+                          const std::string& place, 
+                          const Colored::ArcExpression_ptr& expr, 
+                          bool transport, 
+                          std::string transportID) override;
+        void addOutputArc(const std::string& transition,
+                const std::string& place,
+                const Colored::ArcExpression_ptr& expr) override;
+        void addOutputArc(const std::string& transition,
+                          const std::string& place,
+                          int weight = 1, bool transport = false, std::string transportID  = "") override;
         void addColorType(const std::string& id,
                 Colored::ColorType* type) override;
 
+        void addTransportArc(const std::string& source,
+                const std::string& transition,
+                const std::string& destination,
+                const Colored::ArcExpression_ptr& expr,
+                std::vector<Colored::TimeInterval>& interval) override;
+
+
 
         void sort() override;
 
@@ -139,12 +172,15 @@
             return _pttransitionnames;
         }
         
+        std::map<std::string, std::string> getInvariants() {return _invariantStrings;}
+
         PetriNetBuilder& unfold();
         PetriNetBuilder& stripColors();
         void computePlaceColorFixpoint(uint32_t max_intervals, uint32_t max_intervals_reduced, int32_t timeout);
         void computePartition();
         
     private:
+        std::map<std::string, std::string> _invariantStrings;
         std::unordered_map<std::string,uint32_t> _placenames;
         std::unordered_map<std::string,uint32_t> _transitionnames;
         std::unordered_map<uint32_t, std::unordered_map<uint32_t, Colored::ArcIntervals>> _arcIntervals;
@@ -152,17 +188,24 @@
         std::unordered_map<uint32_t,std::vector<uint32_t>> _placePreTransitionMap;
         std::unordered_map<uint32_t,FixpointBindingGenerator> _bindings;
         PTPlaceMap _ptplacenames;
+        std::unordered_map<std::string, std::string> _shadowPlacesNames;
         PTTransitionMap _pttransitionnames;
+        std::vector< std::tuple<double, double> > _placelocations;
+        std::vector< std::tuple<double, double> > _transitionlocations;
         uint32_t _nptplaces = 0;
         uint32_t _npttransitions = 0;
         uint32_t _nptarcs = 0;
         uint32_t _maxIntervals = 0;
         PetriEngine::IntervalGenerator intervalGenerator;
         
+        std::vector<Colored::Transition> _transitions;
         std::vector<Colored::Place> _places;
-        std::vector<Colored::Transition> _transitions;
         std::vector<Colored::Arc> _arcs;
+<<<<<<< TREE
         std::vector<Colored::ColorFixpoint> _placeColorFixpoints;
+=======
+        std::vector<Colored::Arc> inhibitorArcs;
+>>>>>>> MERGE-SOURCE
         ColorTypeMap _colors;
         PetriNetBuilder _ptBuilder;
         bool _unfolded = false;
@@ -191,21 +234,40 @@
         void addArc(const std::string& place,
                 const std::string& transition,
                 const Colored::ArcExpression_ptr& expr,
+<<<<<<< TREE
                 bool input);
 
 
         void getArcIntervals(Colored::Transition& transition, bool &transitionActivated, uint32_t max_intervals, uint32_t transitionId);      
         void processInputArcs(Colored::Transition& transition, uint32_t currentPlaceId, uint32_t transitionId, bool &transitionActivated, uint32_t max_intervals);
         void processOutputArcs(Colored::Transition& transition);
+=======
+                bool input, bool inhibitor, int weight);
+
+        void addTimedArc(const std::string& place,
+                         const std::string& transition,
+                         const Colored::ArcExpression_ptr& expr,
+                         std::vector<Colored::TimeInterval>& interval,
+                         bool inhibitor, bool transport,
+                         bool input, int weight, std::string transportID);
+>>>>>>> MERGE-SOURCE
         
+<<<<<<< TREE
         void unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color, uint32_t unfoldPlace, uint32_t id);
+=======
+        Colored::TimeInterval getTimeIntervalForArc(std::vector< Colored::TimeInterval> timeIntervals,const Colored::Color* color);
+        void unfoldPlace(Colored::Place& place);
+        Colored::TimeInvariant getTimeInvariantForPlace(std::vector< Colored::TimeInvariant> TimeInvariants, const Colored::Color* color);
+>>>>>>> MERGE-SOURCE
         void unfoldTransition(Colored::Transition& transition);
         void handleOrphanPlace(Colored::Place& place, std::unordered_map<std::string, uint32_t> unfoldedPlaceMap);
         void createPartionVarmaps();
 
         void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name);
+        void unfoldInhibitorArc(std::string &oldname, std::string &newname);
     };
     
+<<<<<<< TREE
     //Used for checking if a variable is inside either a succ or pred expression
     enum ExpressionType {
         None,
@@ -213,6 +275,33 @@
         Succ
     };
  
+=======
+    class BindingGenerator {
+    public:
+        class Iterator {
+        private:
+            BindingGenerator* _generator;
+            
+        public:
+            Iterator(BindingGenerator* generator);
+            
+            bool operator==(Iterator& other);
+            bool operator!=(Iterator& other);
+            Iterator& operator++();
+            const Colored::ExpressionContext::BindingMap operator++(int);
+            Colored::ExpressionContext::BindingMap& operator*();
+        };
+    private:
+        Colored::GuardExpression_ptr _expr;
+        Colored::ExpressionContext::BindingMap _bindings;
+        ColoredPetriNetBuilder::ColorTypeMap& _colorTypes;
+        
+        bool eval();
+        
+    public:
+        BindingGenerator(Colored::Transition& transition,
+                ColoredPetriNetBuilder::ColorTypeMap& colorTypes);
+>>>>>>> MERGE-SOURCE
 
 }
 

=== modified file 'include/PetriEngine/Colored/Colors.h'
--- include/PetriEngine/Colored/Colors.h	2021-04-14 10:41:18 +0000
+++ include/PetriEngine/Colored/Colors.h	2021-04-19 13:50:22 +0000
@@ -35,6 +35,7 @@
 namespace PetriEngine {
     namespace Colored {
         class ColorType;
+        class TimeInvariant;
 
         class Color {
         public:
@@ -47,6 +48,7 @@
             uint32_t _id;
             
         public:
+            Color();
             Color(ColorType* colorType, uint32_t id, std::vector<const Color*>& colors);
             Color(ColorType* colorType, uint32_t id, const char* color);
             ~Color() {}
@@ -54,8 +56,15 @@
             bool isTuple() const {
                 return _tuple.size() > 1;
             }
+<<<<<<< TREE
 
             void getColorConstraints(Colored::interval_t *constraintsVector, uint32_t *index) const;
+=======
+
+            const std::vector<const Color*> getTuple() const {
+                return _tuple;
+            }
+>>>>>>> MERGE-SOURCE
             
             std::vector<const Color*> getTupleColors() const {
                 return _tuple;
@@ -110,9 +119,15 @@
         public:
             static const Color* dotConstant(ColorType *ct) {
                 static DotConstant _instance;
+<<<<<<< TREE
                 if(ct != nullptr){
                     _instance._colorType = ct;
                 }
+=======
+                if(ct != nullptr){
+                    _instance._colorType = ct;
+                }                
+>>>>>>> MERGE-SOURCE
                 return &_instance;
             }
             
@@ -253,6 +268,25 @@
             }
         };
 
+        class StarColorType : public ColorType {
+        private:
+            StarColorType();
+
+        public:
+            static const ColorType* starColorType() {
+                static StarColorType _instance;
+
+                return &_instance;
+            }
+
+            StarColorType(StarColorType const&) = delete;
+            void operator=(StarColorType const&) = delete;
+
+            bool operator== (const StarColorType& other) {
+                return true;
+            }
+        };
+
         class ProductType : public ColorType {
         private:
             std::vector<ColorType*> constituents;

=== modified file 'include/PetriEngine/Colored/Expressions.h'
--- include/PetriEngine/Colored/Expressions.h	2021-04-14 11:51:52 +0000
+++ include/PetriEngine/Colored/Expressions.h	2021-04-19 13:50:22 +0000
@@ -124,6 +124,7 @@
             virtual ~ColorExpression() {}
             
             virtual const Color* eval(ExpressionContext& context) const = 0;
+<<<<<<< TREE
 
             virtual void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const = 0;
 
@@ -135,11 +136,18 @@
                 return Colored::intervalTuple_t();
             }
 
+=======
+
+            virtual ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const = 0;
+
+            virtual void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const = 0;
+>>>>>>> MERGE-SOURCE
         };
         
         class DotConstantExpression : public ColorExpression {
         public:
             const Color* eval(ExpressionContext& context) const override {
+<<<<<<< TREE
                 return DotConstant::dotConstant(nullptr);
             }
 
@@ -173,6 +181,18 @@
 
             std::string toString() const override {
                 return "dot";
+=======
+                return DotConstant::dotConstant(nullptr);
+            }
+
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return DotConstant::dotConstant(nullptr)->getColorType();
+            }
+
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                const Color *dotColor = DotConstant::dotConstant(nullptr);
+                constantMap[index] = dotColor;
+>>>>>>> MERGE-SOURCE
             }
         };
 
@@ -244,14 +264,24 @@
             void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
             }
 
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _variable->colorType;
+            }
+
             std::string toString() const override {
                 return _variable->name;
             }
 
+<<<<<<< TREE
             ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
                 return _variable->colorType;
             }
 
+=======
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+            }
+
+>>>>>>> MERGE-SOURCE
             VariableExpression(Variable* variable)
                     : _variable(variable) {}
         };
@@ -304,6 +334,7 @@
                 return _userOperator->toString();
             }
 
+<<<<<<< TREE
             void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
                 constantMap[index] = _userOperator;
             }
@@ -322,6 +353,16 @@
                 return tupleInterval;
             }
 
+=======
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                constantMap[index] = _userOperator;
+            }
+
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _userOperator->getColorType();
+            }
+
+>>>>>>> MERGE-SOURCE
             UserOperatorExpression(const Color* userOperator)
                     : _userOperator(userOperator) {}
         };
@@ -410,10 +451,24 @@
                 return _color->toString() + "++";
             }
 
-            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
-                return _color->getColorType(colorTypes);
-            }
-
+<<<<<<< TREE
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _color->getColorType(colorTypes);
+            }
+
+=======
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _color->getColorType(colorTypes);
+            }
+
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                _color->getConstants(constantMap, index);
+                for(auto& constIndexPair : constantMap){
+                    constIndexPair.second = &constIndexPair.second->operator++();
+                }
+            }
+
+>>>>>>> MERGE-SOURCE
             SuccessorExpression(ColorExpression_ptr&& color)
                     : _color(std::move(color)) {}
         };
@@ -468,10 +523,24 @@
                 return _color->toString() + "--";
             }
 
-            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
-                return _color->getColorType(colorTypes);
-            }
-
+<<<<<<< TREE
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _color->getColorType(colorTypes);
+            }
+
+=======
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _color->getColorType(colorTypes);
+            }
+
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                _color->getConstants(constantMap, index);
+                for(auto& constIndexPair : constantMap){
+                    constIndexPair.second = &constIndexPair.second->operator--();
+                }
+            }
+
+>>>>>>> MERGE-SOURCE
             PredecessorExpression(ColorExpression_ptr&& color)
                     : _color(std::move(color)) {}
         };
@@ -489,12 +558,14 @@
                     colors.push_back(color->eval(context));
                     types.push_back(colors.back()->getColorType());
                 }
+
                 ProductType* pt = context.findProductColorType(types);
 
                 const Color* col = pt->getColor(colors);
                 assert(col != nullptr);
                 return col;
             }
+<<<<<<< TREE
 
             bool isTuple() const override {
                 return true;
@@ -539,6 +610,34 @@
                 }
                 return true;
             }
+=======
+
+            void setColorType(ColorType* ct){
+                _colorType = ct;
+            }
+
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                std::vector<const ColorType*> types;
+                for (auto color : _colors) {
+                    types.push_back(color->getColorType(colorTypes));
+                }
+                for (auto& elem : colorTypes) {
+                    auto* pt = dynamic_cast<ProductType*>(elem.second);
+                    if (pt && pt->containsTypes(types)) {
+                        return pt;
+                    }
+                }
+                std::cout << "COULD NOT FIND PRODUCT TYPE" << std::endl;
+                return nullptr;
+            }
+
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                for (auto elem : _colors) {
+                    elem->getConstants(constantMap, index);
+                    index++;
+                }
+            }
+>>>>>>> MERGE-SOURCE
             
             void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
                 for (auto elem : _colors) {
@@ -1016,6 +1115,8 @@
         public:
             ArcExpression() {}
             virtual ~ArcExpression() {}
+
+            virtual void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const = 0;
             
             virtual Multiset eval(ExpressionContext& context) const = 0;
 
@@ -1110,6 +1211,12 @@
                 return  _sort->size();
             }
 
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const {
+                for (size_t i = 0; i < _sort->size(); i++) {
+                    constantMap[index].push_back(&(*_sort)[i]);
+                }
+            }
+
             std::string toString() const override {
                 return _sort->getName() + ".all";
             }
@@ -1144,6 +1251,7 @@
                 
                 return Multiset(col);
             }
+<<<<<<< TREE
 
             bool isTuple() const override {
                 for(auto colorExpr : _color){
@@ -1155,6 +1263,23 @@
             }
 
             void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+=======
+
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+                if (_all != nullptr)
+                    _all->getConstants(constantMap, index);
+                else for (auto elem : _color) {
+                    std::unordered_map<uint32_t, const Color*> elemMap;
+                    elem->getConstants(elemMap, index);
+                    for(auto pair : elemMap){
+                        constantMap[pair.first].push_back(pair.second);
+                    }
+                    index++;//not sure if index should be increased here, but no number expression have multiple elements
+                }
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+>>>>>>> MERGE-SOURCE
                 if (_all != nullptr)
                     return;
                 for (auto elem : _color) {
@@ -1264,6 +1389,14 @@
                 }
                 return ms;
             }
+
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+                uint32_t indexCopy = index;
+                for (auto elem : _constituents) {
+                    uint32_t localIndex = indexCopy;
+                    elem->getConstants(constantMap, localIndex);
+                }
+            }
             
             void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
                 for (auto elem : _constituents) {
@@ -1357,6 +1490,12 @@
             Multiset eval(ExpressionContext& context) const override {
                 return _left->eval(context) - _right->eval(context);
             }
+
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+                uint32_t rIndex = index;
+                _left->getConstants(constantMap, index);
+                _right->getConstants(constantMap, rIndex);
+            }
             
             void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
                 _left->getVariables(variables, varPositions, varModifierMap);
@@ -1418,6 +1557,10 @@
             Multiset eval(ExpressionContext& context) const override {
                 return _expr->eval(context) * _scalar;
             }
+
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+                _expr->getConstants(constantMap, index);
+            }
             
             void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
                 _expr->getVariables(variables, varPositions,varModifierMap);

=== added file 'include/PetriEngine/Colored/TimeInterval.h'
--- include/PetriEngine/Colored/TimeInterval.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/TimeInterval.h	2021-04-19 13:50:22 +0000
@@ -0,0 +1,118 @@
+//
+// Created by niels on 3/20/19.
+//
+
+#ifndef VERIFYPN_TIMEINTERVAL_H
+#define VERIFYPN_TIMEINTERVAL_H
+
+#include <limits>
+#include <iostream>
+#include <algorithm>
+#include <map>
+#include <cassert>
+#include <string>
+#include <cctype>
+#include <vector>
+#include "Colors.h"
+
+namespace PetriEngine {
+    namespace Colored{
+        class TimeInterval
+        {
+        public: //Construter
+            TimeInterval(Colored::Color color) : leftStrict(false), lowerBound(0), upperBound(std::numeric_limits<int>::max()), rightStrict(true), color(color){ };
+            TimeInterval(bool leftStrict, uint32_t lowerBound, uint32_t upperBound, bool rightStrict, Colored::Color color) : leftStrict(leftStrict), lowerBound(lowerBound), upperBound(upperBound), rightStrict(rightStrict), color(color) { };
+            TimeInterval(const TimeInterval& ti) : leftStrict(ti.leftStrict), lowerBound(ti.lowerBound), upperBound(ti.upperBound), rightStrict(ti.rightStrict), color(ti.color) {};
+            TimeInterval& operator=(const TimeInterval& ti)
+            {
+                leftStrict = ti.leftStrict;
+                lowerBound = ti.lowerBound;
+                upperBound = ti.upperBound;
+                rightStrict = ti.rightStrict;
+                return *this;
+            }
+
+            virtual ~TimeInterval() { /* empty */ }
+            void divideBoundsBy(int divider);
+            const Colored::Color& getColor()  const{
+                return color;
+            }
+
+
+        public: // inspectors
+            void print(std::ostream& out) const;
+            std::string toString();
+
+            inline const uint32_t getLowerBound() const { return lowerBound; }
+            inline const uint32_t getUpperBound() const { return upperBound; }
+            inline const bool isLowerBoundStrict() const { return leftStrict; }
+            inline const bool isUpperBoundStrict() const { return rightStrict; }
+            inline bool setUpperBound(uint32_t bound, bool isStrict)
+            {
+                if(upperBound == bound) rightStrict |= isStrict;
+                else if(upperBound > bound){
+                    rightStrict = isStrict;
+                    upperBound = bound;
+                }
+                if(upperBound < lowerBound) return false;
+                else return true;
+            }
+
+            inline const bool isZeroInfinity() const { return !leftStrict && lowerBound == 0 && upperBound == std::numeric_limits<int>::max() && rightStrict; }
+            inline const bool contains(uint32_t number) const
+            {
+                return number >= lowerBound && number <= upperBound;
+            }
+            inline bool intersects(const TimeInterval& other) const
+            {
+                assert(!leftStrict);
+                assert(!other.leftStrict);
+                assert(!rightStrict || upperBound == std::numeric_limits<int>().max());
+                assert(!other.rightStrict || other.upperBound == std::numeric_limits<int>().max());
+                if(other.lowerBound >= lowerBound &&
+                   other.lowerBound <= upperBound) return true;
+                return false;
+            }
+
+        public: // statics
+
+            static TimeInterval createFor(const std::string& interval,
+                                          std::vector<const Colored::Color*> colors, std::unordered_map<std::string, uint32_t> constantValues);
+            static inline void ltrim(std::string &s) {
+                s.erase(s.begin(), std::find_if(s.begin(), s.end(), [](int ch) {
+                    return !std::isspace(ch);
+                }));
+            }
+            static Colored::Color createColor(std::vector<const Colored::Color*> colors);
+
+            // trim from end
+            static inline void rtrim(std::string &s) {
+                s.erase(std::find_if(s.rbegin(), s.rend(), [](int ch) {
+                    return !std::isspace(ch);
+                }).base(), s.end());
+            }
+
+            // trim from both ends
+            static inline void trim(std::string &s) {
+                ltrim(s);
+                rtrim(s);
+            }
+
+        private: // data
+            bool leftStrict;
+            uint32_t lowerBound;
+            uint32_t upperBound;
+            bool rightStrict;
+            Colored::Color color;
+        };
+
+        inline std::ostream& operator<<(std::ostream& out, const TimeInterval& interval)
+        {
+            interval.print(out);
+            return out;
+        }
+        // trim from start
+    }
+}
+
+#endif //VERIFYPN_TIMEINTERVAL_H

=== added file 'include/PetriEngine/Colored/TimeInvariant.h'
--- include/PetriEngine/Colored/TimeInvariant.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/TimeInvariant.h	2021-04-19 13:50:22 +0000
@@ -0,0 +1,87 @@
+//
+// Created by niels on 3/20/19.
+//
+
+#ifndef VERIFYPN_TIMEINVARIANT_H
+#define VERIFYPN_TIMEINVARIANT_H
+
+#include <string>
+#include <map>
+#include <limits>
+#include <algorithm>
+#include <cctype>
+#include <locale>
+#include "Colors.h"
+
+namespace PetriEngine {
+    namespace Colored{
+        class TimeInvariant{
+
+        public:
+            TimeInvariant(Colored::Color color) : strictComparison(true), bound(std::numeric_limits<int>::max()), color(color) {};
+            TimeInvariant(bool strictComparison, int bound, PetriEngine::Colored::Color color) : strictComparison(strictComparison), bound(bound), color(color) { };
+            TimeInvariant(const TimeInvariant& ti) : strictComparison(ti.strictComparison), bound(ti.bound), color(ti.color) { };
+            TimeInvariant& operator=(const TimeInvariant& ti)
+            {
+                strictComparison = ti.strictComparison;
+                bound = ti.bound;
+                return *this;
+            }
+
+            virtual ~TimeInvariant(){ /*Left empty*/  };
+
+        public: // inspectors
+            void print(std::ostream& out) const;
+            std::string toString();
+            inline const int getBound() const { return bound; }
+            inline const bool isBoundStrict() const { return strictComparison; }
+            inline const Colored::Color getColor() {return color;}
+
+        public: // statics
+            static TimeInvariant createFor(const std::string& invariant, std::vector<const Colored::Color*> colors, std::unordered_map<std::string, uint32_t> constants);
+            static Colored::Color createColor(std::vector<const Colored::Color*> colors);
+
+        private: // data
+            bool strictComparison;
+            int bound;
+            Colored::Color color;
+        };
+
+        inline bool operator==(const TimeInvariant& a, const TimeInvariant& b)
+        {
+            return a.getBound() == b.getBound() && a.isBoundStrict() == b.isBoundStrict();
+        }
+
+        inline bool operator!=(const TimeInvariant& a, const TimeInvariant& b)
+        {
+            return !(a == b);
+        }
+
+        inline std::ostream& operator<<(std::ostream& out, const TimeInvariant& invariant)
+        {
+            invariant.print(out);
+            return out;
+        }
+        /*
+        *  Singleton pattern from:
+        * https://stackoverflow.com/questions/1008019/c-singleton-design-pattern
+        */
+        class TimeInvariantConstant : public TimeInvariant {
+        private:
+            TimeInvariantConstant();
+
+        public:
+            static const TimeInvariant* starColorDotConstant() {
+                static TimeInvariantConstant _instance;
+                return &_instance;
+            }
+            TimeInvariantConstant(TimeInvariant const&) = delete;
+            void operator=(TimeInvariant const&) = delete;
+            bool operator==(const TimeInvariant other) {
+                return true;
+            }
+        };
+    }
+}
+
+#endif //VERIFYPN_TIMEINVARIANT_H

=== modified file 'include/PetriEngine/NetStructures.h'
--- include/PetriEngine/NetStructures.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/NetStructures.h	2021-04-19 13:50:22 +0000
@@ -10,6 +10,7 @@
 
 #include <limits>
 #include <vector>
+#include <iostream>
 
 namespace PetriEngine {
 
@@ -18,12 +19,23 @@
         uint32_t weight;
         bool skip = false;
         bool inhib = false;
+        bool transport = false;
+        uint32_t lowerBound;
+        uint32_t upperBound;
+        bool lowerStrict;
+        bool upperStrict;
+        std::string interval;
+        std::string transportID;
 
         Arc() :
         place(std::numeric_limits<uint32_t>::max()),
         weight(std::numeric_limits<uint32_t>::max()),
         skip(false),
-        inhib(false) {
+        inhib(false),
+        lowerBound(std::numeric_limits<uint32_t>::max()),
+        upperBound(std::numeric_limits<uint32_t> ::max()),
+        lowerStrict(false),
+        upperStrict(false) {
         };
         
         bool operator < (const Arc& other) const
@@ -42,6 +54,7 @@
         std::vector<Arc> post;
         bool skip = false;
         bool inhib = false;
+        bool urgent = false;
         
         void addPreArc(const Arc& arc)
         {
@@ -89,3 +102,4 @@
 }
 #endif /* NETSTRUCTURES_H */
 
+

=== modified file 'include/PetriEngine/PetriNet.h'
--- include/PetriEngine/PetriNet.h	2021-03-23 14:10:04 +0000
+++ include/PetriEngine/PetriNet.h	2021-04-19 13:50:22 +0000
@@ -25,6 +25,8 @@
 #include <climits>
 #include <limits>
 #include <iostream>
+#include <map>
+#include <unordered_map>
 
 namespace PetriEngine {
 
@@ -42,6 +44,7 @@
     struct TransPtr {
         uint32_t inputs;
         uint32_t outputs;
+        bool urgent;
     };
     
     struct Invariant {
@@ -49,6 +52,9 @@
         uint32_t tokens;
         bool inhibitor;
         int8_t direction;
+        bool transport;
+        std::string interval;
+        std::string transportID;
         // we can pack things here, but might give slowdown
     } /*__attribute__((packed))*/; 
     
@@ -102,7 +108,13 @@
         
         void sort();
         
-        void toXML(std::ostream& out);
+        void toXML(std::ostream& out, bool timed, std::map<std::string, std::string> _invariantStrings, bool verifydtapn);
+
+        bool isTimed() {return timed;}
+        void setTimed(bool timed) {this->timed = timed;}
+        void setInvariants(std::map<std::string, std::string> invariants) {
+            invariantStrings = invariants;
+        }
         
         const MarkVal* initial() const {
             return _initialMarking;
@@ -122,12 +134,21 @@
          * @remarks We could also get this from the _places vector, but I don't see any
          * any complexity garentees for this type.
          */
+        std::string getType(std::pair<const Invariant*, const Invariant*> pair, bool pre);
+        std::string getArcIdentifier(std::string arcType);
+        inline const char * const BoolToString(bool b)
+        {
+            return b ? "true" : "false";
+        }
         uint32_t _ninvariants, _ntransitions, _nplaces;
 
         std::vector<TransPtr> _transitions;
         std::vector<Invariant> _invariants;
+        std::map<std::string, std::string> invariantStrings;
         std::vector<uint32_t> _placeToPtrs;
+        std::vector<std::string> usedTransportIDs;
         MarkVal* _initialMarking;
+        bool timed = false;
 
         std::vector<std::string> _transitionnames;
         std::vector<std::string> _placenames;
@@ -140,9 +161,14 @@
         friend class SuccessorGenerator;
         friend class ReducingSuccessorGenerator;
         friend class STSolver;
+<<<<<<< TREE
         friend class StubbornSet;
+=======
+        friend class Filter;
+>>>>>>> MERGE-SOURCE
     };
 
 } // PetriEngine
 
 #endif // PETRINET_H
+

=== modified file 'include/PetriEngine/PetriNetBuilder.h'
--- include/PetriEngine/PetriNetBuilder.h	2021-03-05 16:43:31 +0000
+++ include/PetriEngine/PetriNetBuilder.h	2021-04-19 13:50:22 +0000
@@ -29,6 +29,7 @@
 #include "Reducer.h"
 #include "NetStructures.h"
 #include "Reachability/ReachabilityResult.h"
+#include "Colored/TimeInvariant.h"
 namespace PetriEngine {
     /** Builder for building engine representations of PetriNets */
     class PetriNetBuilder : public AbstractPetriNetBuilder {
@@ -39,14 +40,27 @@
         PetriNetBuilder();
         PetriNetBuilder(const PetriNetBuilder& other);
         void addPlace(const std::string& name, int tokens, double x, double y) override;
+        void addPlace(const std::string& name,
+                int tokens,
+                Colored::TimeInvariant invariant,
+                double x = 0,
+                double y = 0) override;
         void addTransition(const std::string& name,
                 double x,
                 double y) override;
+        void addTransition(const std::string &name, bool urgent,
+                                           double, double) override;
         void addInputArc(const std::string& place,
                 const std::string& transition,
                 bool inhibitor,
                 int weight) override;
-        void addOutputArc(const std::string& transition, const std::string& place, int weight) override;
+        void addInputArc(const std::string &place,
+                         const std::string &transition,
+                         bool inhibitor, bool transport,
+                         int weight,
+                         Colored::TimeInterval &interval, std::string transportID) override;
+        
+        void addOutputArc(const std::string& transition, const std::string& place, int weight = 1, bool transport = false, std::string transportID = "") override;
 
         virtual void sort() override;
         /** Make the resulting petri net, you take ownership */
@@ -123,15 +137,24 @@
         void startTimer() {
             _start = std::chrono::high_resolution_clock::now();
         }
+
+        bool isTimed() {return timed;}
+
+        void setTimed(bool timed) { this->timed = timed;}
+
+        std::map<std::string, std::string> getInvariants() {return _invariantStrings;}
         
     private:
         uint32_t nextPlaceId(std::vector<uint32_t>& counts,  std::vector<uint32_t>& pcounts, std::vector<uint32_t>& ids, bool reorder);
         std::chrono::high_resolution_clock::time_point _start;
+        bool timed = false;
 
     protected:
         std::unordered_map<std::string, uint32_t> _placenames;
         std::unordered_map<std::string, uint32_t> _transitionnames;
 
+        std::map<std::string, std::string> _invariantStrings;
+
         std::vector< std::tuple<double, double> > _placelocations;
         std::vector< std::tuple<double, double> > _transitionlocations;
         
@@ -146,3 +169,4 @@
 
 #endif // PETRINETBUILDER_H
 
+

=== modified file 'include/PetriEngine/options.h'
--- include/PetriEngine/options.h	2021-04-14 11:51:52 +0000
+++ include/PetriEngine/options.h	2021-04-19 13:50:22 +0000
@@ -5,7 +5,13 @@
 #include <stddef.h>
 #include <limits>
 #include <set>
+<<<<<<< TREE
 #include <sstream>
+=======
+#include <string.h>
+#include <cctype>
+#include <iostream>
+>>>>>>> MERGE-SOURCE
 
 #include "Reachability/ReachabilitySearch.h"
 #include "../CTL/Algorithm/AlgorithmTypes.h"
@@ -81,6 +87,9 @@
     
     size_t seed() { return ++seed_offset; }
 
+    //TACPN options
+    bool outputVerifydtapnFormat = false;
+
     void print() {
         if (!printstatistics) {
             return;
@@ -175,3 +184,4 @@
 };
 
 #endif
+

=== modified file 'include/PetriParse/PNMLParser.h'
--- include/PetriParse/PNMLParser.h	2021-04-14 10:41:18 +0000
+++ include/PetriParse/PNMLParser.h	2021-04-19 13:50:22 +0000
@@ -39,7 +39,12 @@
         std::string source,
         target;
         int weight;
+        bool transport;
+        bool normal;
+        bool inhib;
         PetriEngine::Colored::ArcExpression_ptr expr;
+        std::vector<PetriEngine::Colored::TimeInterval> interval;
+        std::string transportID;
     };
     typedef std::vector<Arc> ArcList;
     typedef ArcList::iterator ArcIter;
@@ -48,6 +53,7 @@
         std::string id;
         double x, y;
         PetriEngine::Colored::GuardExpression_ptr expr;
+        bool urgent;
     };
     typedef std::vector<Transition> TransitionList;
     typedef TransitionList::iterator TransitionIter;
@@ -78,9 +84,15 @@
     }
 
 private:
+    inline bool stringToBool(std::string b)
+    {
+        return b == "true" ? 1 : 0;
+    }
     void parseElement(rapidxml::xml_node<>* element);
     void parsePlace(rapidxml::xml_node<>* element);
+    std::pair<std::string, std::vector<const PetriEngine::Colored::Color*>> parseTimeConstraint(rapidxml::xml_node<> *element);
     void parseArc(rapidxml::xml_node<>* element, bool inhibitor = false);
+    void parseInterval(rapidxml::xml_node<>* element);
     void parseTransition(rapidxml::xml_node<>* element);
     void parseDeclarations(rapidxml::xml_node<>* element);
     void parseNamedSort(rapidxml::xml_node<>* element);
@@ -89,27 +101,44 @@
     PetriEngine::Colored::ColorExpression_ptr parseColorExpression(rapidxml::xml_node<>* element);
     PetriEngine::Colored::AllExpression_ptr parseAllExpression(rapidxml::xml_node<>* element);
     PetriEngine::Colored::ColorType* parseUserSort(rapidxml::xml_node<>* element);
+<<<<<<< TREE
     PetriEngine::Colored::ArcExpression_ptr parseNumberOfExpression(rapidxml::xml_node<>* element);
     void collectColorsInTuple(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>>& collectedColors);
     PetriEngine::Colored::ArcExpression_ptr constructAddExpressionFromTupleExpression(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors, uint32_t numberof);
+=======
+    PetriEngine::Colored::ArcExpression_ptr parseNumberOfExpression(rapidxml::xml_node<>* element);
+    void collectColorsInTuple(rapidxml::xml_node<>* element, std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>>& collectedColors);
+    PetriEngine::Colored::ArcExpression_ptr constructAddExpressionFromTupleExpression(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors, uint32_t numberof);
+    std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> cartesianProduct(std::vector<PetriEngine::Colored::ColorExpression_ptr> rightSet, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftSet);
+    std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> cartesianProduct(std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> rightSet, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftSet);
+>>>>>>> MERGE-SOURCE
     void parseTransportArc(rapidxml::xml_node<>* element);
     void parseValue(rapidxml::xml_node<>* element, std::string& text);
     uint32_t parseNumberConstant(rapidxml::xml_node<>* element);
     void parsePosition(rapidxml::xml_node<>* element, double& x, double& y);
     void parseQueries(rapidxml::xml_node<>* element);
     const PetriEngine::Colored::Color* findColor(const char* name) const;
+<<<<<<< TREE
     const PetriEngine::Colored::Color* findColorForIntRange(const char* value, uint32_t start, uint32_t end) const;
     std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> cartesianProduct(std::vector<PetriEngine::Colored::ColorExpression_ptr> rightVector, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftVector);
     std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> cartesianProduct(std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> rightVector, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftVector);
+=======
+    bool checkIsTimed(rapidxml::xml_node<> *netType);
+>>>>>>> MERGE-SOURCE
     PetriEngine::AbstractPetriNetBuilder* builder;
     NodeNameMap id2name;
     ArcList arcs;
-    ArcList inhibarcs;
     TransitionList transitions;
     ColorTypeMap colorTypes;
     VariableMap variables;
     bool isColored;
+    bool isTimed;
     std::vector<Query> queries;
+    std::unordered_map<std::string, uint32_t> constantValues;
 };
 
-#endif // PNMLPARSER_H
\ No newline at end of file
+<<<<<<< TREE
+#endif // PNMLPARSER_H=======
+#endif // PNMLPARSER_H
+
+>>>>>>> MERGE-SOURCE

=== modified file 'src/PetriEngine/Colored/CMakeLists.txt'
--- src/PetriEngine/Colored/CMakeLists.txt	2021-04-14 10:41:18 +0000
+++ src/PetriEngine/Colored/CMakeLists.txt	2021-04-19 13:50:22 +0000
@@ -2,9 +2,15 @@
 
 add_library(Colored ColoredPetriNetBuilder.cpp
 Colors.cpp
+<<<<<<< TREE
 Multiset.cpp
 BindingGenerator.cpp
 PartitionBuilder.cpp
 EquivalenceClass.cpp
 GuardRestrictor.cpp)
+=======
+Multiset.cpp
+TimeInterval.cpp
+TimeInvariant.cpp)
+>>>>>>> MERGE-SOURCE
 add_dependencies(Colored rapidxml-ext ptrie-ext glpk-ext)

=== modified file 'src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp'
--- src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-04-14 11:51:52 +0000
+++ src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-04-19 13:50:22 +0000
@@ -24,13 +24,19 @@
     ColoredPetriNetBuilder::ColoredPetriNetBuilder() {
     }
 
-    ColoredPetriNetBuilder::ColoredPetriNetBuilder(const ColoredPetriNetBuilder& orig) {
+    ColoredPetriNetBuilder::ColoredPetriNetBuilder(const ColoredPetriNetBuilder& orig) 
+    : _placenames(orig._placenames), _transitionnames(orig._transitionnames),
+       _placelocations(orig._placelocations), _transitionlocations(orig._transitionlocations),
+       _transitions(orig._transitions), _places(orig._places)
+    {
+        
     }
 
     ColoredPetriNetBuilder::~ColoredPetriNetBuilder() {
     }
 
     void ColoredPetriNetBuilder::addPlace(const std::string& name, int tokens, double x, double y) {
+        
         if (!_isColored) {
             _ptBuilder.addPlace(name, tokens, x, y);
         }
@@ -42,6 +48,7 @@
             uint32_t next = _placenames.size();
             _places.emplace_back(Colored::Place {name, type, tokens});
             _placenames[name] = next;
+<<<<<<< TREE
 
             //set up place color fix points and initialize queue
             if (!tokens.empty()) {
@@ -65,6 +72,26 @@
             }
          
             _placeColorFixpoints.push_back(colorFixpoint);            
+=======
+            
+            _invariantStrings[name] = "< inf";
+            _placelocations.push_back(std::tuple<double, double>(x,y));
+        }
+    }
+
+    void ColoredPetriNetBuilder::addPlace(const std::string &name,
+                                          PetriEngine::Colored::Multiset &&tokens,
+                                          Colored::ColorType* type,
+                                          std::vector<PetriEngine::Colored::TimeInvariant> &invariant, double x,
+                                          double y) {
+        if(_placenames.count(name) == 0){
+            uint32_t next = _placenames.size();
+            _places.emplace_back(Colored::Place{name, type, tokens, invariant});
+            _placenames[name] = next;
+            
+            _invariantStrings[name] = invariant.size() ? invariant[0].toString(): "< inf";
+            _placelocations.push_back(std::tuple<double, double>(x,y));
+>>>>>>> MERGE-SOURCE
         }
     }
 
@@ -80,6 +107,20 @@
             uint32_t next = _transitionnames.size();
             _transitions.emplace_back(Colored::Transition {name, guard});
             _transitionnames[name] = next;
+            _transitionlocations.push_back(std::tuple<double, double>(x,y));
+        }
+    }
+
+    void ColoredPetriNetBuilder::addTransition(const std::string& name,
+            const Colored::GuardExpression_ptr& guard,
+            bool urgent,
+            double x,
+            double y) {
+        if (_transitionnames.count(name) == 0) {
+            uint32_t next = _transitionnames.size();
+            _transitions.emplace_back(Colored::Transition {name, guard, urgent});
+            _transitionnames[name] = next;
+            _transitionlocations.push_back(std::tuple<double, double>(x,y));
         }
     }
 
@@ -89,17 +130,27 @@
         }
     }
 
-    void ColoredPetriNetBuilder::addInputArc(const std::string& place, const std::string& transition, const Colored::ArcExpression_ptr& expr) {
-        addArc(place, transition, expr, true);
-    }
-
-    void ColoredPetriNetBuilder::addOutputArc(const std::string& transition, const std::string& place, int weight) {
+    void ColoredPetriNetBuilder::addInputArc(const std::string& place, const std::string& transition, const Colored::ArcExpression_ptr& expr, bool inhibitor, int weight) {
+        addArc(place, transition, expr, true, inhibitor, weight);
+    }
+
+    void ColoredPetriNetBuilder::addInputArc(const std::string &place,
+                                             const std::string &transition,
+                                             bool inhibitor, bool transport,
+                                             const Colored::ArcExpression_ptr& expr,
+                                             std::vector<PetriEngine::Colored::TimeInterval> &interval, int weight, std::string transportID) {
+        addTimedArc(place,transition,expr,interval,inhibitor, transport, true, weight, transportID);
+
+    }
+
+    void ColoredPetriNetBuilder::addOutputArc(const std::string& transition, const std::string& place, int weight, bool transport, std::string transportID) {
         if (!_isColored) {
-            _ptBuilder.addOutputArc(transition, place, weight);
+            _ptBuilder.addOutputArc(transition, place, weight, transport, transportID);
         }
     }
 
     void ColoredPetriNetBuilder::addOutputArc(const std::string& transition, const std::string& place, const Colored::ArcExpression_ptr& expr) {
+<<<<<<< TREE
         addArc(place, transition, expr, false);
     }
 
@@ -125,10 +176,130 @@
         Colored::Arc arc;
         arc.place = p;
         arc.transition = t;
+=======
+        addArc(place, transition, expr, false, false, 1);
+    }
+
+    void ColoredPetriNetBuilder::addOutputArc(const std::string& transition, const std::string& place, const Colored::ArcExpression_ptr& expr, bool transport, std::string transportID) {
+        std::vector<PetriEngine::Colored::TimeInterval> intervals;
+        addTimedArc(place, transition, expr, intervals, false, transport, false, 0, transportID);
+    }
+
+    void ColoredPetriNetBuilder::addArc(const std::string& place, const std::string& transition, const Colored::ArcExpression_ptr& expr, bool input, bool inhibitor, int weight) {
+        if(_transitionnames.count(transition) == 0)
+        {
+            std::cout << "Transition '" << transition << "' not found. Adding it." << std::endl;
+            addTransition(transition,0.0,0.0);
+        }
+        if(_placenames.count(place) == 0)
+        {
+            std::cout << "Place '" << place << "' not found. Adding it." << std::endl;
+            addPlace(place,0,0,0);
+        }
+        uint32_t p = _placenames[place];
+        uint32_t t = _transitionnames[transition];
+
+        assert(t < _transitions.size());
+        assert(p < _places.size());
+
+        Colored::Arc arc;
+        arc.place = p;
+        arc.transition = t;
+        if(!inhibitor)
+            assert(expr != nullptr);
+        arc.expr = std::move(expr);
+        arc.input = input;
+        if(inhibitor){
+            std::cout << "Adding inhib arc " << std::endl;
+            inhibitorArcs.push_back(std::move(arc));
+        } else {
+            _transitions[t].arcs.push_back(std::move(arc));
+        }
+        
+        
+    }
+
+    void ColoredPetriNetBuilder::addTimedArc(const std::string &place, const std::string &transition,
+                                             const PetriEngine::Colored::ArcExpression_ptr &expr,
+                                             std::vector<PetriEngine::Colored::TimeInterval> &interval, bool inhibitor, bool transport,
+                                             bool input, int weight, std::string transportID) {
+        if(_transitionnames.count(transition) == 0)
+        {
+            std::cout << "Transition '" << transition << "' not found. Adding it." << std::endl;
+            addTransition(transition,0.0,0.0);
+        }
+        if(_placenames.count(place) == 0)
+        {
+            std::cout << "Place '" << place << "' not found. Adding it." << std::endl;
+            addPlace(place,0,0,0);
+        }
+        uint32_t p = _placenames[place];
+        uint32_t t = _transitionnames[transition];
+
+        assert(t < _transitions.size());
+        assert(p < _places.size());
+
+        Colored::Arc arc;
+        arc.place = p;
+        arc.transition = t;
+        if(!inhibitor)
+            assert(expr != nullptr);
+        arc.expr = expr;
+        arc.input = input;
+        arc.weight = weight;
+        arc.interval = interval;
+        arc.inhibitor = inhibitor;
+        arc.transport = transport;
+        arc.transportID = transportID;
+        // _transitions[t].inhibitor |= inhibitor;
+        // _places[p].inhibitor |= inhibitor;
+        if(inhibitor){
+            std::cout << "Adding inhib arc " << std::endl;
+            inhibitorArcs.push_back(std::move(arc));
+        } else {
+            _transitions[t].arcs.push_back(std::move(arc));
+        }
+        
+    }
+
+    void ColoredPetriNetBuilder::addTransportArc(const std::string &source, const std::string &transition,
+                                                 const std::string &destination,
+                                                 const PetriEngine::Colored::ArcExpression_ptr &expr,
+                                                 std::vector<PetriEngine::Colored::TimeInterval> &interval) {
+        if(_transitionnames.count(transition) == 0)
+        {
+            std::cout << "Transition '" << transition << "' not found. Adding it." << std::endl;
+            addTransition(transition,0.0,0.0);
+        }
+        if(_placenames.count(source) == 0)
+        {
+            std::cout << "Place '" << source << "' not found. Adding it." << std::endl;
+            addPlace(source,0,0,0);
+        }
+        if(_placenames.count(destination) == 0)
+        {
+            std::cout << "Place '" << destination << "' not found. Adding it." << std::endl;
+            addPlace(destination,0,0,0);
+        }
+        uint32_t s = _placenames[source];
+        uint32_t t = _transitionnames[transition];
+
+        assert(t < _transitions.size());
+        assert(s < _places.size());
+
+        Colored::TransportArc transportArc;
+        transportArc.source = s;
+        transportArc.transition = t;
+>>>>>>> MERGE-SOURCE
         assert(expr != nullptr);
+<<<<<<< TREE
         arc.expr = std::move(expr);
         arc.input = input;
         input? _transitions[t].input_arcs.push_back(std::move(arc)): _transitions[t].output_arcs.push_back(std::move(arc));
+=======
+        transportArc.expr = expr;
+        transportArc.interval = interval;
+>>>>>>> MERGE-SOURCE
     }
 
     void ColoredPetriNetBuilder::addColorType(const std::string& id, Colored::ColorType* type) {
@@ -413,9 +584,17 @@
             auto end = std::chrono::high_resolution_clock::now();
             _time = (std::chrono::duration_cast<std::chrono::microseconds>(end - start).count())*0.000001;
         }
+<<<<<<< TREE
+=======
+        if (isTimed()) {
+            _ptBuilder.setTimed(true);
+        }
+
+>>>>>>> MERGE-SOURCE
         return _ptBuilder;
     }
 
+<<<<<<< TREE
     //Due to the way we unfold places, we only unfold palces connected to an arc (which makes sense)
     //However, in queries asking about orphan places it cannot find these, as they have not been unfolded
     //so we make a placeholder place which just has tokens equal to the number of colored tokens
@@ -460,9 +639,75 @@
         _ptBuilder.addPlace(name, tokenSize, 0.0, 0.0);
         _ptplacenames[place->name][id] = std::move(name);
         ++_nptplaces;
+=======
+    void ColoredPetriNetBuilder::unfoldPlace(Colored::Place& place) {
+        double xBuffer = 0;
+        double yBuffer = 0;
+        uint32_t index = _placenames[place.name];
+        auto placePos = _placelocations[index];
+        for (size_t i = 0; i < place.type->size(); ++i) {
+            double x = xBuffer + get<0>(placePos);
+            double y = yBuffer + get<1>(placePos);
+            std::string name = place.name + "Sub" + std::to_string(i);
+            const Colored::Color* color = &place.type->operator[](i);
+            if (isTimed()) {
+                Colored::TimeInvariant invariant = getTimeInvariantForPlace(place.invariants, color); //TODO:: this does not take the correct time invariant
+                _ptBuilder.addPlace(name, place.marking[color], invariant, x, y);
+                _invariantStrings[name] = invariant.toString();
+            } else {
+                _ptBuilder.addPlace(name, place.marking[color], x, y);
+            }
+
+            _ptplacenames[place.name][color->getId()] = std::move(name);
+            ++_nptplaces;
+            xBuffer += 50;
+            yBuffer += 0;
+            
+        }
+        if (isTimed()) { // we add the shadow place p.sum
+            double x = xBuffer + get<0>(placePos);
+            double y = yBuffer + get<1>(placePos);
+            Colored::Color color;
+            std::string placeName = place.name + "Sum";
+            _ptBuilder.addPlace(placeName, place.marking.size(), Colored::TimeInvariant(color), x, y);
+            _invariantStrings[placeName] = Colored::TimeInvariant(color).toString();
+            //_ptplacenames[place.name][color.getId()] = std::move(placeName);
+            _shadowPlacesNames[place.name] = std::move(placeName);
+            ++_nptplaces;
+        }
+    }
+
+    Colored::TimeInvariant ColoredPetriNetBuilder::getTimeInvariantForPlace(std::vector< Colored::TimeInvariant> TimeInvariants, const Colored::Color* color) {
+        for (Colored::TimeInvariant element : TimeInvariants) {
+            if (!element.getColor().isTuple()) {
+                if (element.getColor().getId() == color->getId()) {
+                    return element;
+                }
+            } else {
+                bool matches = true;
+                Colored::Color color = element.getColor();
+                std::vector<const Colored::Color*> colors = color.getTuple();
+                if (colors.size() == color.getTuple().size()) {
+                    for(uint32_t i = 0;i < colors.size(); i++) {
+                        if (colors[i]->getId() != color.getTuple()[i]->getId())
+                            matches = false;
+                    }
+                    if (matches)
+                        return element;
+                }
+            }
+        }
+        for (uint32_t j = 0; j < TimeInvariants.size(); ++j) {
+            if (TimeInvariants[j].getColor().getColorName() == "*") {
+                return TimeInvariants[j];
+            }
+        }
+        exit(ErrorCode);
+>>>>>>> MERGE-SOURCE
     }
 
     void ColoredPetriNetBuilder::unfoldTransition(Colored::Transition& transition) {
+<<<<<<< TREE
         if(_fixpointDone || _partitionComputed){            
             FixpointBindingGenerator gen(transition, _colors);
             size_t i = 0;
@@ -495,18 +740,60 @@
                 for (auto& arc : transition.output_arcs) {
                     unfoldArc(arc, b, name);
                 }
-            }
+=======
+        BindingGenerator gen(transition, _colors);
+        double buffer = 0;
+        uint32_t transitionId = _transitionnames[transition.name];
+        auto transitionPos = _transitionlocations[transitionId];
+        size_t i = 0;
+        for (auto& b : gen) {
+            std::string name = transition.name + "Sub" + std::to_string(i++);
+            if (isTimed()) {
+                _ptBuilder.addTransition(name, transition.urgent, get<0>(transitionPos) + buffer, get<1>(transitionPos));
+            } else {
+                _ptBuilder.addTransition(name, get<0>(transitionPos) + buffer, get<1>(transitionPos));
+            }
+            _pttransitionnames[transition.name].push_back(name);
+            ++_npttransitions;
+            for (auto& arc : transition.arcs) {
+                unfoldArc(arc, b, name);
+>>>>>>> MERGE-SOURCE
+            }
+<<<<<<< TREE
         }        
+=======
+            unfoldInhibitorArc(transition.name, name);
+            buffer += 250;
+        }
+    }
+
+    void ColoredPetriNetBuilder::unfoldInhibitorArc(std::string &oldname, std::string &newname) {
+        for (uint32_t i = 0; i < inhibitorArcs.size(); ++i) {
+            if (_transitions[inhibitorArcs[i].transition].name.compare(oldname) == 0) {
+                Colored::Arc inhibArc = inhibitorArcs[i];
+                std::string place = _shadowPlacesNames[_places[inhibArc.place].name];
+                _ptBuilder.addInputArc(place, newname, inhibArc.inhibitor, inhibArc.weight);
+            }
+        }
+>>>>>>> MERGE-SOURCE
     }
 
     void ColoredPetriNetBuilder::unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& tName) {
+<<<<<<< TREE
         Colored::ExpressionContext context {binding, _colors, _partition[arc.place]};
         auto ms = arc.expr->eval(context);       
         
+=======
+        Colored::ExpressionContext context {binding, _colors};
+        auto ms = arc.expr->eval(context);
+        int shadowWeight = 0;
+        std::vector<Colored::TimeInterval>& timeIntervals = arc.interval;
+>>>>>>> MERGE-SOURCE
         for (const auto& color : ms) {
             if (color.second == 0) {
                 continue;
             }
+<<<<<<< TREE
             
             const PetriEngine::Colored::Place& place = _places[arc.place];
             uint32_t id;
@@ -527,6 +814,74 @@
             }
             ++_nptarcs;
         }        
+=======
+            shadowWeight += color.second;
+            const std::string& pName = _ptplacenames[_places[arc.place].name][color.first->getId()];
+            if(isTimed()){
+                if (!arc.input) {
+                    _ptBuilder.addOutputArc(tName, pName, color.second, arc.transport, arc.transportID);
+                } else {
+                    Colored::TimeInterval timeInterval = getTimeIntervalForArc(timeIntervals, color.first);
+                    _ptBuilder.addInputArc(pName, tName, arc.inhibitor, arc.transport, color.second, timeInterval, arc.transportID);
+                }
+            } else {
+                if (!arc.input) {
+                    _ptBuilder.addOutputArc(tName, pName, color.second);
+                } else {
+                    _ptBuilder.addInputArc(pName, tName, arc.inhibitor, color.second);
+                }
+            }
+             
+            ++_nptarcs;
+        }
+        if(isTimed() && shadowWeight > 0) {
+            std::string pName = _shadowPlacesNames[_places[arc.place].name];
+            if (!arc.input) {
+                _ptBuilder.addOutputArc(tName, pName, shadowWeight, false, arc.transportID);
+            } else {
+                Colored::Color color;
+                Colored::TimeInterval timeInterval(color);
+                _ptBuilder.addInputArc(pName, tName, arc.inhibitor, false, shadowWeight, timeInterval, arc.transportID);
+            }
+            ++_nptarcs;
+            /*
+            if(inhibitorArcs.find(_places[arc.place].name) != inhibitorArcs.end()) {
+                Colored::Arc inhibArc = inhibitorArcs[_places[arc.place].name];
+                _ptBuilder.addInputArc(pName, tName, inhibArc.inhibitor, inhibArc.weight);
+                ++_nptarcs;
+            }
+             */
+        }
+    }
+
+    Colored::TimeInterval ColoredPetriNetBuilder::getTimeIntervalForArc(std::vector< Colored::TimeInterval> timeIntervals,const Colored::Color* color) {
+        for (Colored::TimeInterval element : timeIntervals) {
+            if (!element.getColor().isTuple()) {
+                if (element.getColor().getId() == color->getId()) {
+                    return element;
+                }
+            } else {
+                bool matches = true;
+                std::vector<const Colored::Color*> colors = element.getColor().getTuple();
+                
+                if (colors.size() == color->getTuple().size()) {
+                    for(uint32_t i = 0; i < colors.size(); i++) {
+                        if (colors[i]->getId() != color->getTuple()[i]->getId())
+                            matches = false;
+                    }
+                    if (matches)
+                        return element;
+                }
+            }
+        }
+        for (uint32_t j = 0; j < timeIntervals.size(); ++j) { // If there is no timeinterval for the specific color, we use the default * interval
+            if (timeIntervals[j].getColor().getColorName() == "*") {
+                return timeIntervals[j];
+            }
+        }
+        std::cerr << "There is no matching time interval to an arc" << std::endl;;
+        exit(ErrorCode);
+>>>>>>> MERGE-SOURCE
     }
 
     //----------------------- Strip Colors -----------------------//
@@ -535,11 +890,13 @@
         if (_unfolded) assert(false);
         if (_isColored && !_stripped) {
             for (auto& place : _places) {
-                _ptBuilder.addPlace(place.name, place.marking.size(), 0.0, 0.0);
+                if (!isTimed())
+                    _ptBuilder.addPlace(place.name, place.marking.size(), 0.0, 0.0);
             }
 
             for (auto& transition : _transitions) {
                 _ptBuilder.addTransition(transition.name, 0.0, 0.0);
+<<<<<<< TREE
                 for (auto& arc : transition.input_arcs) {
                     try {
                         _ptBuilder.addInputArc(_places[arc.place].name, _transitions[arc.transition].name, false,
@@ -557,6 +914,19 @@
                                                 arc.expr->weight());
                     } catch (Colored::WeightException& e) {
                         std::cerr << "Exception on output arc: " << arcToString(arc) << std::endl;
+=======
+                for (auto& arc : transition.arcs) {
+                    try {
+                        if (arc.input) {
+                            _ptBuilder.addInputArc(_places[arc.place].name, _transitions[arc.transition].name, false,
+                                                   arc.expr->weight());
+                        } else {
+                            _ptBuilder.addOutputArc(_transitions[arc.transition].name, _places[arc.place].name,
+                                                    arc.expr->weight(), arc.transport, arc.transportID);
+                        }
+                    } catch (Colored::WeightException& e) {
+                        std::cerr << "Exception on arc: " << arcToString(arc) << std::endl;
+>>>>>>> MERGE-SOURCE
                         std::cerr << "In expression: " << arc.expr->toString() << std::endl;
                         std::cerr << e.what() << std::endl;
                         exit(ErrorCode);
@@ -575,6 +945,104 @@
         return !arc.input ? "(" + _transitions[arc.transition].name + ", " + _places[arc.place].name + ")" :
                "(" + _places[arc.place].name + ", " + _transitions[arc.transition].name + ")";
     }
+<<<<<<< TREE
+=======
+
+    BindingGenerator::Iterator::Iterator(BindingGenerator* generator)
+            : _generator(generator)
+    {
+    }
+
+    bool BindingGenerator::Iterator::operator==(Iterator& other) {
+        return _generator == other._generator;
+    }
+
+    bool BindingGenerator::Iterator::operator!=(Iterator& other) {
+        return _generator != other._generator;
+    }
+
+    BindingGenerator::Iterator& BindingGenerator::Iterator::operator++() {
+        _generator->nextBinding();
+        if (_generator->isInitial()) _generator = nullptr;
+        return *this;
+    }
+
+    const Colored::ExpressionContext::BindingMap BindingGenerator::Iterator::operator++(int) {
+        auto prev = _generator->currentBinding();
+        ++*this;
+        return prev;
+    }
+
+    Colored::ExpressionContext::BindingMap& BindingGenerator::Iterator::operator*() {
+        return _generator->currentBinding();
+    }
+
+    BindingGenerator::BindingGenerator(Colored::Transition& transition,
+            ColoredPetriNetBuilder::ColorTypeMap& colorTypes)
+        : _colorTypes(colorTypes)
+    {
+        _expr = transition.guard;
+        std::set<Colored::Variable*> variables;
+        if (_expr != nullptr) {
+            _expr->getVariables(variables);
+        }
+        for (auto arc : transition.arcs) {
+            assert(arc.expr != nullptr);
+            arc.expr->getVariables(variables);
+        }
+        for (auto var : variables) {
+            _bindings[var->name] = &var->colorType->operator[](0);
+        }
+        
+        if (!eval())
+            nextBinding();
+    }
+
+    bool BindingGenerator::eval() {
+        if (_expr == nullptr)
+            return true;
+
+        Colored::ExpressionContext context {_bindings, _colorTypes};
+        return _expr->eval(context);
+    }
+
+    Colored::ExpressionContext::BindingMap& BindingGenerator::nextBinding() {
+        bool test = false;
+        while (!test) {
+            for (auto& _binding : _bindings) {
+                _binding.second = &_binding.second->operator++();
+                if (_binding.second->getId() != 0) {
+                    break;
+                }
+            }
+
+            if (isInitial())
+                break;
+
+            test = eval();
+        }
+        return _bindings;
+    }
+
+    Colored::ExpressionContext::BindingMap& BindingGenerator::currentBinding() {
+        return _bindings;
+    }
+
+    bool BindingGenerator::isInitial() const {
+        for (auto& b : _bindings) {
+            if (b.second->getId() != 0) return false;
+        }
+        return true;
+    }
+
+    BindingGenerator::Iterator BindingGenerator::begin() {
+        return {this};
+    }
+
+    BindingGenerator::Iterator BindingGenerator::end() {
+        return {nullptr};
+    }
+>>>>>>> MERGE-SOURCE
 }
     
  
\ No newline at end of file

=== modified file 'src/PetriEngine/Colored/Colors.cpp'
--- src/PetriEngine/Colored/Colors.cpp	2021-03-15 10:04:47 +0000
+++ src/PetriEngine/Colored/Colors.cpp	2021-04-19 13:50:22 +0000
@@ -49,6 +49,12 @@
             stream << color.toString();
             return stream;
         }
+
+        Color::Color() {
+            _id = 0;
+            _colorName = "*";
+            _colorType = new ColorType("*");
+        }
         
         Color::Color(ColorType* colorType, uint32_t id, std::vector<const Color*>& colors)
                 : _tuple(colors), _colorType(colorType), _colorName(""), _id(id)
@@ -191,6 +197,9 @@
         {
         }
         
+        StarColorType::StarColorType() : ColorType("*") {
+
+        }
         
         void ColorType::addColor(const char* colorName) {
             _colors.emplace_back(this, _colors.size(), colorName);

=== modified file 'src/PetriEngine/Colored/Multiset.cpp'
=== added file 'src/PetriEngine/Colored/TimeInterval.cpp'
--- src/PetriEngine/Colored/TimeInterval.cpp	1970-01-01 00:00:00 +0000
+++ src/PetriEngine/Colored/TimeInterval.cpp	2021-04-19 13:50:22 +0000
@@ -0,0 +1,91 @@
+//
+// Created by niels on 3/20/19.
+//
+#include "PetriEngine/Colored/TimeInterval.h"
+#include "PetriEngine/Colored/Colors.h"
+#include "PetriEngine/Colored/TimeInvariant.h"
+#include <vector>
+
+namespace PetriEngine {
+    namespace Colored {
+        TimeInterval TimeInterval::createFor(const std::string &interval, std::vector<const Colored::Color*> colors, std::unordered_map<std::string, uint32_t> constantValues) {
+            Colored::Color color = Colored::TimeInvariant::createColor(colors);
+            bool leftStrict = false;
+            std::string leftParentheses = "(";
+            std::size_t foundLeft = interval.find(leftParentheses);
+            if(foundLeft != std::string::npos){
+                leftStrict = true;
+            }
+
+            bool rightStrict = false;
+            std::string rightParentheses = ")";
+            std::size_t foundRight = interval.find(rightParentheses);
+            if(foundRight != std::string::npos) {
+                rightStrict = true;
+            }
+
+            std::string strLoverBound = interval.substr(0, interval.find(","));
+            trim(strLoverBound);
+            strLoverBound = strLoverBound.substr(1, strLoverBound.size());
+            std::string strUpperBound = interval.substr(interval.find(","), interval.size()-1);
+            trim(strUpperBound);
+            if(rightStrict == true){
+                strUpperBound = strUpperBound.substr(1, strUpperBound.find(")")-1);
+            } else{
+                strUpperBound = strUpperBound.substr(1, strUpperBound.find("]")-1);
+            }
+
+            int lowerBound;
+            int upperBound;
+            if (constantValues.find(strLoverBound) == constantValues.end())
+                lowerBound = std::stoi(strLoverBound);
+            else
+                lowerBound = constantValues[strLoverBound];
+
+            if(strUpperBound.compare("inf") == 0 )
+                upperBound = std::numeric_limits<int>().max();
+            else {
+                if (constantValues.find(strUpperBound) == constantValues.end())
+                    upperBound = std::stoi(strUpperBound);
+                else
+                    upperBound = constantValues[strUpperBound];
+            }
+
+            return TimeInterval(leftStrict, lowerBound, upperBound, rightStrict, color);
+        }
+
+        void TimeInterval::print(std::ostream &out) const
+        {
+            std::string leftParenthesis = leftStrict ? "(" : "[";
+            std::string rightParenthesis = rightStrict ? ")" : "]";
+            std::string strLowerBound = std::to_string(lowerBound);
+            std::string strUpperBound = upperBound == std::numeric_limits<int>().max() ? "inf" : std::to_string(upperBound);
+
+            out << leftParenthesis << strLowerBound << "," << strUpperBound << rightParenthesis;
+        }
+
+        std::string TimeInterval::toString() {
+            std::string leftParenthesis = leftStrict ? "(" : "[";
+            std::string rightParenthesis = rightStrict ? ")" : "]";
+            std::string strLowerBound = std::to_string(lowerBound);
+            std::string strUpperBound = upperBound == std::numeric_limits<int>().max() ? "inf" : std::to_string(upperBound);
+
+            return leftParenthesis + strLowerBound + "," + strUpperBound + rightParenthesis;
+        }
+        void TimeInterval::divideBoundsBy(int divider) {
+            if(lowerBound != 0 )
+                lowerBound = lowerBound / divider;
+            if(upperBound != std::numeric_limits<int>().max() ) {
+                upperBound = upperBound / divider;
+            }
+        }
+        Colored::Color TimeInterval::createColor(std::vector<const Colored::Color*> colors) {
+            if (colors.size() == 1 ) {
+                return Color(colors.front()->getColorType(), colors.front()->getId(), colors.front()->getColorName().c_str());
+            } else {
+                return Color(colors.front()->getColorType(), colors.front()->getId(), colors);
+            }
+        }
+    }
+}
+

=== added file 'src/PetriEngine/Colored/TimeInvariant.cpp'
--- src/PetriEngine/Colored/TimeInvariant.cpp	1970-01-01 00:00:00 +0000
+++ src/PetriEngine/Colored/TimeInvariant.cpp	2021-04-19 13:50:22 +0000
@@ -0,0 +1,71 @@
+//
+// Created by niels on 3/20/19.
+//
+
+#include "PetriEngine/Colored/TimeInvariant.h"
+#include "PetriEngine/Colored/TimeInterval.h"
+
+namespace PetriEngine {
+    namespace Colored {
+
+        TimeInvariant TimeInvariant::createFor(const std::string& invariant, std::vector<const Colored::Color*> colors, std::unordered_map<std::string, uint32_t> constants){
+            Colored::Color color = createColor(colors);
+            bool strict = false;
+
+            std::string leq = "<=";
+            bool found = invariant.find(leq) != std::string::npos;
+            if(!found) {
+                strict = true;
+            }
+            int bound = std::numeric_limits<int>().max();
+
+            int pos = strict ? 1 : 2;
+            std::string number = invariant.substr(pos);
+            TimeInterval::trim(number);
+
+            bool foundInf = false;
+            std::string inf = "inf";
+            std::size_t findInf = invariant.find(inf);
+            if(findInf != std::string::npos) {
+                foundInf = true;
+            }
+
+            if(foundInf == false) {
+                if (constants.find(number) == constants.end())
+                    bound = std::stoi(number);
+                else
+                    bound = constants[number];
+            }
+
+
+            if (bound == std::numeric_limits<int>().max())
+                return TimeInvariant(color);
+            else
+                return TimeInvariant(strict, bound, color);
+        }
+
+        Colored::Color TimeInvariant::createColor(std::vector<const Colored::Color*> colors) {
+            if (colors.size() == 1 ) {
+                return Color(colors.front()->getColorType(), colors.front()->getId(), colors.front()->getColorName().c_str());
+            } else {
+                std::cerr << colors.size()  << " colors size";
+                return Color(colors.front()->getColorType(), colors.front()->getId(), colors);
+            }
+        }
+
+        void TimeInvariant::print(std::ostream& out) const
+        {
+            std::string comparison = strictComparison ? "<" : "<=";
+            std::string strBound = bound == std::numeric_limits<int>().max() ? "inf" : std::to_string(bound);
+            strBound = " " + strBound;
+            out << comparison << strBound;
+        }
+        std::string TimeInvariant::toString() {
+            std::string comparison = strictComparison ? "<" : "<=";
+            std::string strBound = bound == std::numeric_limits<int>().max() ? "inf" : std::to_string(bound);
+            strBound = " " + strBound;
+            comparison = comparison + strBound;
+            return comparison;
+        }
+    }
+}
\ No newline at end of file

=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
--- src/PetriEngine/PQL/Expressions.cpp	2021-04-14 11:51:52 +0000
+++ src/PetriEngine/PQL/Expressions.cpp	2021-04-19 13:50:22 +0000
@@ -171,6 +171,172 @@
                 return FALSE_CONSTANT;
             }
         }
+<<<<<<< TREE
+=======
+        
+        /******************** To String ********************/
+
+        void LiteralExpr::toString(std::ostream& out) const {
+            out << _value;
+        }
+
+        void UnfoldedIdentifierExpr::toString(std::ostream& out) const {
+            out << _name;
+        }
+
+        void NaryExpr::toString(std::ostream& ss) const {
+            ss << "(";
+            _exprs[0]->toString(ss);
+            for(size_t i = 1; i < _exprs.size(); ++i)
+            {
+                ss << " " << op() << " ";
+                _exprs[i]->toString(ss);
+            }
+            ss << ")";
+        }
+
+        void CommutativeExpr::toString(std::ostream& ss) const {
+            ss << "( " << _constant;
+            for(auto& i : _ids)
+                ss << " " << op() << " " << i.second;
+            for(auto& e : _exprs)
+            {
+                ss << " " << op() << " ";
+                e->toString(ss);
+            }
+            ss << ")";
+        }
+
+
+        void MinusExpr::toString(std::ostream& out) const {
+            out << "-";
+            _expr->toString(out);
+        }
+
+        void SimpleQuantifierCondition::toString(std::ostream& out) const {
+            out << op() << " ";
+            _cond->toString(out);
+        }
+        
+        void UntilCondition::toString(std::ostream& out) const {
+            out << op() << " (";
+            _cond1->toString(out);
+            out << " U ";
+            _cond2->toString(out);
+            out << ")";
+        }
+        
+        void LogicalCondition::toString(std::ostream& out) const {
+            out << "(";
+            _conds[0]->toString(out);
+            for(size_t i = 1; i < _conds.size(); ++i)
+            {
+                out << " " << op() << " ";
+                _conds[i]->toString(out);
+            }
+            out << ")";
+        }
+        
+        void CompareConjunction::toString(std::ostream& out) const {
+            out << "(";
+            if(_negated) out << "not";
+            bool first = true;
+            for(auto& c : _constraints)
+            {
+                if(!first) out << " and ";
+                if(c._lower != 0) 
+                    out << "(" << c._lower << " <= " << c._name << ")";
+                if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max()) 
+                    out << " and ";
+                if(c._upper != std::numeric_limits<uint32_t>::max()) 
+                    out << "(" << c._upper << " >= " << c._name << ")";
+                first = false;
+            }
+            out << ")";
+        }
+
+        void CompareCondition::toString(std::ostream& out) const {
+            out << "(";
+            _expr1->toString(out);
+            out << " " << op() << " ";
+            _expr2->toString(out);
+            out <<")";
+        }
+
+        void NotCondition::toString(std::ostream& out) const {
+            out << "(not ";
+            _cond->toString(out);
+            out << ")";
+        }
+
+        void BooleanCondition::toString(std::ostream& out) const {
+            if (_value)
+                out << "true";
+            else
+                out << "false";
+        }
+
+        void DeadlockCondition::toString(std::ostream& out) const {
+            out << "deadlock";
+        }
+
+        void StableMarkingCondition::_toString(std::ostream &out) const {
+            if(_compiled) _compiled->toString(out);
+            else out << "stable-marking";
+        }
+
+        void LivenessCondition::_toString(std::ostream &out) const {
+            if(_compiled) _compiled->toString(out);
+            else out << "liveness";
+        }
+
+        void QuasiLivenessCondition::_toString(std::ostream &out) const {
+            if(_compiled) _compiled->toString(out);
+            else out << "liveness";
+        }
+
+        void KSafeCondition::_toString(std::ostream &out) const {
+            if(_compiled) _compiled->toString(out);
+            else
+            {
+                out << "k-safe(";
+                _bound->toString(out);
+                out << ")";
+            }
+        }
+
+        void UpperBoundsCondition::_toString(std::ostream& out) const {
+            if(_compiled) _compiled->toString(out);
+            else
+            {
+                out << "bounds (";
+                for(size_t i = 0; i < _places.size(); ++i)
+                {
+                    if(i != 0) out << ", ";
+                    out << _places[i];
+                }
+                out << ")";            
+            }
+        }
+        
+        void UnfoldedUpperBoundsCondition::toString(std::ostream& out) const {
+            out << "bounds (";
+            for(size_t i = 0; i < _places.size(); ++i)
+            {
+                if(i != 0) out << ", ";
+                out << _places[i]._name;
+            }
+            out << ")";
+        }
+
+        void FireableCondition::_toString(std::ostream &out) const {
+            out << "is-fireable(" << _name << ")";
+        }
+
+        void UnfoldedFireableCondition::_toString(std::ostream &out) const {
+            out << "is-fireable(" << _name << ")";
+        }
+>>>>>>> MERGE-SOURCE
 
         /******************** To TAPAAL Query ********************/
 
@@ -4090,3 +4256,4 @@
     } // PQL
 } // PetriEngine
 
+

=== modified file 'src/PetriEngine/PetriNet.cpp'
--- src/PetriEngine/PetriNet.cpp	2021-03-15 10:04:47 +0000
+++ src/PetriEngine/PetriNet.cpp	2021-04-19 13:50:22 +0000
@@ -26,6 +26,9 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
+#include <algorithm>
+#include <iostream>
+#include <string>
 
 namespace PetriEngine {
 
@@ -176,20 +179,32 @@
         }
     }
     
-    void PetriNet::toXML(std::ostream& out)
+    void PetriNet::toXML(std::ostream& out, bool timed, std::map<std::string, std::string> _invariantStrings, bool verifydtapn)
     {
-        out << "<?xml version=\"1.0\"?>\n"
-            << "<pnml xmlns=\"http://www.pnml.org/version-2009/grammar/pnml\">\n" 
-            << "<net id=\"ClientsAndServers-PT-N0500P0\" type=\"http://www.pnml.org/version-2009/grammar/ptnet\">\n";
-        out << "<page id=\"page0\">\n" 
-            << "<name>\n" 
-            << "<text>DefaultPage</text>" 
-            << "</name>";
+        if(!timed) {
+            out << "<?xml version=\"1.0\"?>\n"
+                << "<pnml xmlns=\"http://www.pnml.org/version-2009/grammar/pnml\">\n" 
+                << "<net id=\"ClientsAndServers-PT-N0500P0\" type=\"http://www.pnml.org/version-2009/grammar/ptnet\">\n";
+            out << "<page id=\"page0\">\n" 
+                << "<name>\n" 
+                << "<text>DefaultPage</text>" 
+                << "</name>";
+        } else {
+            if (!verifydtapn) {
+                out << "<?xml version=\"1.0\"?>\n";
+            }
+
+            out << "<pnml xmlns=\"http://www.pnml.org/version-2009/grammar/pnml\">\n"
+                << "<net id=\"ClientsAndServers-PT-N0500P0\" active=\"true\" type=\"P/T net\">\n";
+
+
+        }
 
         for(size_t i = 0; i < _nplaces; ++i)
         {
             auto& p = _placenames[i];
             auto& placelocation = _placelocations[i];
+<<<<<<< TREE
             out << "<place id=\"" << p << "\">\n"
                 << "<graphics><position x=\"" << std::get<0>(placelocation)
                 << "\" y=\"" << std::get<1>(placelocation) << "\"/></graphics>\n"
@@ -197,17 +212,62 @@
             if(_initialMarking[i] > 0)
             {
                 out << "<initialMarking><text>" << _initialMarking[i] << "</text></initialMarking>\n";
+=======
+            if(!timed) {
+                out << "<place id=\"" << p << "\">\n"
+                    << "<graphics><position x=\"" << get<0>(placelocation) 
+                    << "\" y=\"" << get<1>(placelocation) << "\"/></graphics>\n"
+                    << "<name><text>" << p << "</text></name>\n";
+                if(_initialMarking[i] > 0)
+                {
+                    out << "<initialMarking><text>" << _initialMarking[i] << "</text></initialMarking>\n";
+                }
+                out << "</place>\n";
+            } else {
+                std::string invariant = _invariantStrings.at(p);
+                std::string toReplace("<");
+                size_t pos = invariant.find(toReplace);
+                invariant.replace(pos, toReplace.length(), "&lt;");
+
+                if (verifydtapn) {
+                    out << R"(<place id=")" << p << "\"" << R"( initialMarking=")" << _initialMarking[i] << R"(" invariant=")" << invariant <<
+                        R"(" name=")" << p << "\"/>\n";
+                }
+                else {
+                    out << R"(<place displayName="true" id=")" << p << "\"" << R"( initialMarking=")" << _initialMarking[i] << R"(" invariant=")" << invariant <<
+                        R"(" markingOffsetX="0.0" markingOffsetY="0.0" name=")" << p << R"(" nameOffsetX="-5.0" nameOffsetY="35.0" positionX=")" << get<0>(placelocation) <<  R"(" positionY=")" << get<1>(placelocation) << "\" />\n";
+                }
+>>>>>>> MERGE-SOURCE
             }
-            out << "</place>\n";
         }
         for(size_t i = 0; i < _ntransitions; ++i)
         {
             auto& transitionlocation = _transitionlocations[i];
+<<<<<<< TREE
             out << "<transition id=\"" << _transitionnames[i] << "\">\n"
                 << "<name><text>" << _transitionnames[i] << "</text></name>\n";
             out << "<graphics><position x=\"" << std::get<0>(transitionlocation)
                 << "\" y=\"" << std::get<1>(transitionlocation) << "\"/></graphics>\n";
             out << "</transition>\n";
+=======
+            if (!timed) {
+                out << "<transition id=\"" << _transitionnames[i] << "\">\n"
+                    << "<name><text>" << _transitionnames[i] << "</text></name>\n";
+                out << "<graphics><position x=\"" << get<0>(transitionlocation) 
+                    << "\" y=\"" << get<1>(transitionlocation) << "\"/></graphics>\n";
+                out << "</transition>\n";
+            } else {
+                if (verifydtapn) {
+                    out << R"(<transition id=")" << _transitionnames[i] << "\" name=\"" << _transitionnames[i]  << R"(" urgent=")" << BoolToString(_transitions[i].urgent) << "\"";
+                    out << "/>\n";
+                }
+                else {
+                    out << R"(<transition angle="0" displayName="true" id=")" << _transitionnames[i] << "\" name=\"" << _transitionnames[i]  << R"(" infiniteServer="false" nameOffsetX="-5.0" nameOffsetY="35.0" positionX=")" << get<0>(transitionlocation) << R"(" positionY=")" << get<1>(transitionlocation) << R"(" priority="0"
+                urgent=")" << BoolToString(_transitions[i].urgent) << " \"";
+                    out << "/>\n";
+                }
+            }
+>>>>>>> MERGE-SOURCE
         }
         size_t id = 0;
         for(size_t t = 0; t < _ntransitions; ++t)
@@ -216,37 +276,123 @@
 
             for(; pre.first != pre.second; ++pre.first)
             {
-                out << "<arc id=\"" << (id++) << "\" source=\""
-                    << _placenames[pre.first->place] << "\" target=\""
-                    << _transitionnames[t]
-                    << "\" type=\""
-                    << (pre.first->inhibitor ? "inhibitor" : "normal")
-                    << "\">\n";
-                
-                if(pre.first->tokens > 1)
-                {
-                    out << "<inscription><text>" << pre.first->tokens << "</text></inscription>\n";                    
+                if(!timed) {
+                    out << "<arc id=\"" << (id++) << "\" source=\""
+                        << _placenames[pre.first->place] << "\" target=\""
+                        << _transitionnames[t]
+                        << "\" type=\""
+                        << (pre.first->inhibitor ? "inhibitor" : "normal")
+                        << "\">\n";
+                    
+                    if(pre.first->tokens > 1)
+                    {
+                        out << "<inscription><text>" << pre.first->tokens << "</text></inscription>\n";                    
+                    }
+                    
+                    out << "</arc>\n";
+                } else {
+                    std::string type = getType(pre, true);
+                    std::string arcName = getArcIdentifier(type);
+                    if (verifydtapn) {
+                        if (arcName.compare("transportArc") == 0) {
+                            auto post = postset(t);
+                            for (; post.first != post.second; ++post.first) {
+                                if (post.first->transportID.compare(pre.first->transportID) == 0 && (getType(post, false).compare("transport")) == 0) {
+                                    out << "<" << arcName << R"( id=")" << (id++) << R"(" inscription=")" << pre.first->interval << R"(" source=")" <<   _placenames[pre.first->place] << R"(" transition=")" << _transitionnames[t] <<  "\" weight=\"" << pre.first->tokens << "\" target=\"" << _placenames[post.first->place] << "\" />\n";
+                                    continue;
+                                }
+                            }
+                        } else {
+                            out << "<" << arcName << R"( id=")" << (id++) << R"(" inscription=")" << pre.first->interval << R"(" source=")" <<   _placenames[pre.first->place] << "\" weight=\"" << pre.first->tokens << "\" target=\"" << _transitionnames[t] << "\" />\n";
+                        }
+                    }
+                    else {
+                        if (arcName.compare("transportArc") == 0) {
+                            auto post = postset(t);
+                            for (; post.first != post.second; ++post.first) {
+                                if (post.first->transportID.compare(pre.first->transportID) == 0 && (getType(post, false).compare("transport")) == 0) {
+                                    out << R"(<arc id=")" << (id++) << R"(" inscription=")" << pre.first->interval << R"(" nameOffsetX="0.0" source=")" <<   _placenames[pre.first->place] << "\" weight=\"" << pre.first->tokens << "\" target=\"" << _transitionnames[t] << "\" type=\"" << type << "\" />\n";
+                                    out << R"(<arc id=")" << (id++) << R"(" inscription=")" << pre.first->interval
+                                    << R"(" nameOffsetX="0.0" source=")" << _transitionnames[t] << "\" weight=\"" << post.first->tokens << "\" target=\"" <<  _placenames[post.first->place] << "\" type=\"" << type << "\" />\n";
+                                    continue;
+                                }
+                            }
+                        }
+                        else {
+                            out << R"(<arc id=")" << (id++) << R"(" inscription=")" << pre.first->interval << R"(" nameOffsetX="0.0" source=")" <<   _placenames[pre.first->place] << "\" weight=\"" << pre.first->tokens << "\" target=\"" << _transitionnames[t] << "\" type=\"" << type << "\" />\n";
+                        }
+
+                    }
                 }
-                
-                out << "</arc>\n";
             }
 
             auto post = postset(t);
             for(; post.first != post.second; ++post.first)
             {
-                out << "<arc id=\"" << (id++) << "\" source=\""
-                    << _transitionnames[t] << "\" target=\""
-                    << _placenames[post.first->place] << "\">\n";
-                
-                if(post.first->tokens > 1)
-                {
-                    out << "<inscription><text>" << post.first->tokens << "</text></inscription>\n";                    
-                }
-                
-                out << "</arc>\n";
+                if (!timed) {
+                    out << "<arc id=\"" << (id++) << "\" source=\""
+                        << _transitionnames[t] << "\" target=\""
+                        << _placenames[post.first->place] << "\">\n";
+                    
+                    if(post.first->tokens > 1)
+                    {
+                        out << "<inscription><text>" << post.first->tokens << "</text></inscription>\n";                    
+                    }
+                    
+                    out << "</arc>\n";
+                }
+                else {
+                    std::string type = getType(post, false);
+                    if(type.compare("transport") == 0)
+                        continue;
+                    if (verifydtapn) {
+                        std::string arcName = getArcIdentifier(type);
+                        out << "<" << arcName <<  " id=\"" << (id++) << "\" source=\""
+                            << _transitionnames[t] << "\" target=\""
+                            << _placenames[post.first->place] << "\" weight=\"" << post.first->tokens << "\"/>\n";
+                    } else {
+                        out << "<arc id=\"" << (id++) << "\" source=\""
+                            << _transitionnames[t] << "\" target=\""
+                            << _placenames[post.first->place] << R"(" type=")" << type << "\" weight=\"" << post.first->tokens << "\"/>\n";
+                    }
+                }
             }
         }
-        out << "</page></net>\n</pnml>";
+        if (!timed)
+            out << "</page></net>\n</pnml>";
+        else
+            out << "</net>\n</pnml>";
+    }
+
+    std::string PetriNet::getType(std::pair<const Invariant*, const Invariant*> pair, bool pre) {
+        if(pre) {
+            if (pair.first->transport)
+                return "transport";
+            else if (pair.first->inhibitor)
+                return "inhibitor";
+            else
+                return "timed";
+        } else {
+            if (pair.first->transport)
+                return "transport";
+            else
+                return "normal";
+        }
+    }
+
+    std::string PetriNet::getArcIdentifier(std::string arcType) {
+        std::string arcIdentifier;
+        if (arcType.compare("normal") == 0) {
+            arcIdentifier = "outputArc";
+        } else if (arcType.compare("timed") == 0 ) {
+            arcIdentifier = "inputArc";
+        } else if (arcType.compare("transport") == 0) {
+            arcIdentifier = "transportArc";
+        } else {
+            arcIdentifier = "inhibitorArc";
+        }
+        return arcIdentifier;
     }
     
 } // PetriEngine
+

=== modified file 'src/PetriEngine/PetriNetBuilder.cpp'
--- src/PetriEngine/PetriNetBuilder.cpp	2021-03-15 10:04:47 +0000
+++ src/PetriEngine/PetriNetBuilder.cpp	2021-04-19 13:50:22 +0000
@@ -60,7 +60,27 @@
         
     }
 
+<<<<<<< TREE
     void PetriNetBuilder::addTransition(const std::string &name,
+=======
+    void PetriNetBuilder::addPlace(const string &name, int tokens, Colored::TimeInvariant invariant,
+                                   double x, double y) {
+        if(_placenames.count(name) == 0){
+            uint32_t next = _placenames.size();
+            _places.emplace_back();
+            _placenames[name] = next;
+            _invariantStrings[name] = invariant.toString();
+            _placelocations.push_back(std::tuple<double, double>(x,y));
+
+        }
+        uint32_t id = _placenames[name];
+        while(initialMarking.size() <= id) initialMarking.emplace_back();
+            initialMarking[id] = tokens;
+
+    }
+
+    void PetriNetBuilder::addTransition(const string &name,
+>>>>>>> MERGE-SOURCE
             double x, double y) {
         if(_transitionnames.count(name) == 0)
         {
@@ -71,7 +91,23 @@
         }
     }
 
+<<<<<<< TREE
     void PetriNetBuilder::addInputArc(const std::string &place, const std::string &transition, bool inhibitor, int weight) {
+=======
+    void PetriNetBuilder::addTransition(const string &name, bool urgent,
+                                        double x, double y) {
+        if(_transitionnames.count(name) == 0)
+        {
+            uint32_t next = _transitionnames.size();
+            _transitions.emplace_back();
+            _transitionnames[name] = next;
+            _transitions[next].urgent = urgent;
+            _transitionlocations.push_back(std::tuple<double, double>(x,y));
+        }
+    }
+
+    void PetriNetBuilder::addInputArc(const string &place, const string &transition, bool inhibitor, int weight) {
+>>>>>>> MERGE-SOURCE
         if(_transitionnames.count(transition) == 0)
         {
             addTransition(transition,0.0,0.0);
@@ -96,7 +132,54 @@
         _places[p].inhib |= inhibitor;
     }
 
+<<<<<<< TREE
     void PetriNetBuilder::addOutputArc(const std::string &transition, const std::string &place, int weight) {
+=======
+    void PetriNetBuilder::addInputArc(const std::string &place,
+                                      const std::string &transition,
+                                      bool inhibitor, bool transport,
+                                      int weight,
+                                      PetriEngine::Colored::TimeInterval &interval, std::string transportID) {
+        if(_transitionnames.count(transition) == 0)
+        {
+            addTransition(transition,0.0,0.0);
+        }
+        if(_placenames.count(place) == 0)
+        {
+            //addPlace(place,0,0,0);
+        }
+        uint32_t p = _placenames[place];
+        uint32_t t = _transitionnames[transition];
+            
+
+        uint32_t lowerBound = interval.getLowerBound();
+        uint32_t upperBound = interval.getUpperBound();
+        bool lowerStrict = interval.isLowerBoundStrict();
+        bool upperStrict = interval.isUpperBoundStrict();
+
+        Arc arc;
+        arc.place = p;
+        arc.weight = weight;
+        arc.skip = false;
+        arc.inhib = inhibitor;
+        arc.transport = transport;
+        arc.lowerBound = lowerBound;
+        arc.upperBound = upperBound;
+        arc.lowerStrict = lowerStrict;
+        arc.upperStrict = upperStrict;
+        arc.interval = interval.toString();
+        arc.transportID = transportID;
+        assert(t < _transitions.size());
+        assert(p < _places.size());
+        _transitions[t].pre.push_back(arc);
+        _transitions[t].inhib |= inhibitor;
+        _places[p].consumers.push_back(t);
+        _places[p].inhib |= inhibitor;
+
+    }
+
+    void PetriNetBuilder::addOutputArc(const string &transition, const string &place, int weight, bool transport, std::string transportID) {
+>>>>>>> MERGE-SOURCE
         if(_transitionnames.count(transition) == 0)
         {
             addTransition(transition,0,0);
@@ -110,11 +193,12 @@
 
         assert(t < _transitions.size());
         assert(p < _places.size());
-        
         Arc arc;
         arc.place = p;
         arc.weight = weight;
         arc.skip = false;
+        arc.transport = transport;
+        arc.transportID = transportID;
         _transitions[t].post.push_back(arc);
         _places[p].producers.push_back(t);
     }
@@ -159,7 +243,7 @@
          * If anybody wants to spend time on it, this is the first step towards
          * a decision-tree like construction, possibly improving successor generation. 
          */
-        
+
         uint32_t nplaces = _places.size() - reducer.RemovedPlaces();
         uint32_t ntrans = _transitions.size() - reducer.RemovedTransitions();
         
@@ -167,9 +251,13 @@
         std::vector<uint32_t> place_prod_count = std::vector<uint32_t>(_places.size());
         std::vector<uint32_t> place_idmap = std::vector<uint32_t>(_places.size());
         std::vector<uint32_t> trans_idmap = std::vector<uint32_t>(_transitions.size());
+<<<<<<< TREE
 
 
         
+=======
+
+>>>>>>> MERGE-SOURCE
         uint32_t invariants = 0;
         
         for(uint32_t i = 0; i < _places.size(); ++i)
@@ -190,7 +278,11 @@
 
         
         PetriNet* net = new PetriNet(ntrans, invariants, nplaces);
-        
+        if (isTimed()) {
+            net->setTimed(true);
+            net->setInvariants(_invariantStrings);
+        }
+
         uint32_t next = nextPlaceId(place_cons_count, place_prod_count, place_idmap, reorder);
         uint32_t free = 0;
         uint32_t freeinv = 0;
@@ -208,6 +300,7 @@
                 
                 if(trans.skip) continue;
                 net->_transitions[freetrans].inputs = freeinv;
+                net->_transitions[freetrans].urgent = trans.urgent;
                 
                 // add inhibitors
                 for(auto pre : trans.pre)
@@ -216,6 +309,9 @@
                     iv.place = pre.place;
                     iv.tokens = pre.weight;
                     iv.inhibitor = pre.inhib;
+                    iv.transport = pre.transport;
+                    iv.interval = pre.interval;
+                    iv.transportID = pre.transportID;
                     assert(pre.inhib);
                     assert(place_cons_count[pre.place] > 0);
                     --place_cons_count[pre.place];
@@ -228,7 +324,9 @@
                 {
                     assert(freeinv < net->_ninvariants);
                     net->_invariants[freeinv].place = post.place;
-                    net->_invariants[freeinv].tokens = post.weight;                    
+                    net->_invariants[freeinv].tokens = post.weight;
+                    net->_invariants[freeinv].transport = post.transport;
+                    net->_invariants[freeinv].transportID = post.transportID;                    
                     ++freeinv;
                 }
                 
@@ -297,6 +395,9 @@
                     iv.place = pre.place;
                     iv.tokens = pre.weight;
                     iv.inhibitor = pre.inhib;
+                    iv.transport = pre.transport;
+                    iv.interval = pre.interval;
+                    iv.transportID = pre.transportID;
                     ++freeinv;
                     assert(place_cons_count[pre.place] > 0);
                     --place_cons_count[pre.place];
@@ -306,9 +407,11 @@
                 for(auto post : trans.post)
                 {
                     assert(freeinv < net->_ninvariants);
-                    auto& post_inv = net->_invariants[freeinv];
+                    Invariant& post_inv = net->_invariants[freeinv];
                     post_inv.place = post.place;
-                    post_inv.tokens = post.weight;    
+                    post_inv.tokens = post.weight;
+                    post_inv.transport = post.transport;
+                    post_inv.transportID = post.transportID;    
                     --place_prod_count[post.place];
                     ++freeinv;
                 }
@@ -476,3 +579,4 @@
 
 
 } // PetriEngine
+

=== modified file 'src/PetriParse/PNMLParser.cpp'
--- src/PetriParse/PNMLParser.cpp	2021-04-14 10:41:18 +0000
+++ src/PetriParse/PNMLParser.cpp	2021-04-19 13:50:22 +0000
@@ -23,6 +23,7 @@
 #include <cstdlib>
 #include <iostream>
 #include <limits>
+#include <fstream>
 #include <cstring>
 
 
@@ -38,7 +39,6 @@
     id2name.clear();
     arcs.clear();
     transitions.clear();
-    inhibarcs.clear();
     colorTypes.clear();
 
     //Set the builder
@@ -57,12 +57,38 @@
         exit(ErrorCode);
     }
     
-    auto declarations = root->first_node("net")->first_node("declaration");
+    auto declarations = root->first_node("declaration");
+    if(declarations == nullptr){
+        declarations = root->first_node("net")->first_node("declaration");
+    }
+    
     isColored = declarations != nullptr;
     if (isColored) {
         builder->enableColors();
         parseDeclarations(declarations);
     }
+
+    auto netType = root->first_node("net");
+    rapidxml::xml_node<> *placeElement = netType->first_node("place");
+    while(placeElement == nullptr && netType != nullptr){
+        netType = netType->first_node();
+        placeElement = netType->first_node("place");
+    }
+    
+    if (isColored && checkIsTimed(netType)){
+        builder->enableTimed();
+        isTimed = true;
+    } else {
+        isTimed = false;
+    }
+        
+    //xml_node<> *child = node->first_node(); child; child = child->next_sibling()
+    for (auto it = root->first_node(); it; it = it->next_sibling()) {
+        if (strcmp(it->name(), "constant") == 0)
+            constantValues[it->first_attribute("name")->value()] = atoi(it->first_attribute("value")->value());
+         else
+            break;
+    }
     parseElement(root);
 
     //Add all the transition
@@ -70,7 +96,10 @@
         if (!isColored) {
             builder->addTransition(transition.id, transition.x, transition.y);
         } else {
-            builder->addTransition(transition.id, transition.expr, transition.x, transition.y);
+            if (isTimed)
+                builder->addTransition(transition.id, transition.expr, transition.urgent, transition.x, transition.y);
+            else
+                builder->addTransition(transition.id, transition.expr, transition.x, transition.y);
         }
 
     //Add all the arcs
@@ -97,14 +126,18 @@
 
         if (source.isPlace && !target.isPlace) {
             if (!isColored) {
-                builder->addInputArc(source.id, target.id, false, arc.weight);
+                builder->addInputArc(source.id, target.id, arc.inhib, arc.weight);
+            } else if(isTimed) {
+                builder->addInputArc(source.id, target.id, arc.inhib, arc.transport, arc.expr, arc.interval, arc.weight, arc.transportID);
             } else {
-                builder->addInputArc(source.id, target.id, arc.expr);
+                builder->addInputArc(source.id, target.id, arc.expr, arc.inhib, arc.weight);
             }
 
         } else if (!source.isPlace && target.isPlace) {
             if (!isColored) {
                 builder->addOutputArc(source.id, target.id, arc.weight);
+            } else if (isTimed) {
+                builder->addOutputArc(source.id, target.id, arc.expr, arc.transport, arc.transportID);
             } else {
                 builder->addOutputArc(source.id, target.id, arc.expr);
             }
@@ -116,21 +149,28 @@
         }
     }
 
-    for(Arc& inhibitor : inhibarcs)
-    {
-        NodeName source = id2name[inhibitor.source];
-        NodeName target = id2name[inhibitor.target];
-        if (source.isPlace && !target.isPlace) {
-            builder->addInputArc(source.id, target.id, true, inhibitor.weight);
-        }
-        else
-        {
-            fprintf(stderr,
-                    "XML Parsing error: Inhibitor from \"%s\" to \"%s\" is not valid!\n",
-                    source.id.c_str(),
-                    target.id.c_str());
-        }
-    }
+    // std::cout << "Found " << inhibarcs.size() << " inhibitor arcs " << std::endl;
+    // for(Arc& inhibitor : inhibarcs)
+    // {
+    //     NodeName source = id2name[inhibitor.source];
+    //     NodeName target = id2name[inhibitor.target];
+    //     if (source.isPlace && !target.isPlace) {
+    //         if(!isColored){
+    //             builder->addInputArc(source.id, target.id, inhibitor.inhib, inhibitor.weight);
+    //         } else if (isTimed){
+    //             builder->addInputArc(source.id, target.id, inhibitor.inhib, inhibitor.transport, inhibitor.expr, inhibitor.interval, inhibitor.weight, inhibitor.transportID);
+    //         } else {
+    //             builder->addInputArc(source.id, target.id, inhibitor.expr, inhibitor.inhib);
+    //         }            
+    //     }
+    //     else
+    //     {
+    //         fprintf(stderr,
+    //                 "XML Parsing error: Inhibitor from \"%s\" to \"%s\" is not valid!\n",
+    //                 source.id.c_str(),
+    //                 target.id.c_str());
+    //     }
+    // }
     
     //Unset the builder
     this->builder = nullptr;
@@ -139,11 +179,39 @@
     id2name.clear();
     arcs.clear();
     transitions.clear();
-    inhibarcs.clear();
     colorTypes.clear();
     builder->sort();
 }
 
+bool PNMLParser::checkIsTimed(rapidxml::xml_node<> *netType){
+    rapidxml::xml_node<char> * placeElement = netType->first_node("place");
+    rapidxml::xml_node<char> * arcElement = netType->first_node("inputArc");
+    while(placeElement == nullptr && netType != nullptr){
+        netType = netType->first_node();
+        if(netType != nullptr){
+            placeElement = netType->first_node("place");
+        }        
+    }
+    while(arcElement == nullptr && netType != nullptr){
+        netType = netType->first_node();
+        if(netType != nullptr){
+            arcElement = netType->first_node("inputArc");
+        }        
+    }
+    if(placeElement != nullptr){
+        if(placeElement->first_attribute("invariant") == nullptr){
+            return false;
+        }
+    }
+    if(arcElement != nullptr){
+        if(arcElement->first_attribute("inscription") == nullptr){
+            return false;
+        }
+    }
+
+    return true;
+}
+
 void PNMLParser::parseDeclarations(rapidxml::xml_node<>* element) {
     for (auto it = element->first_node(); it; it = it->next_sibling()) {
         if (strcmp(it->name(), "namedsort") == 0) {
@@ -481,6 +549,13 @@
         number = 1;
         first = num;
     }
+
+    if(strcmp(first->first_node()->name(), "tuple") == 0){
+        std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors;	
+        collectColorsInTuple(first->first_node(), collectedColors);	
+        return constructAddExpressionFromTupleExpression(first->first_node(), collectedColors, number);	
+    }
+
     auto allExpr = parseAllExpression(first);
     if (allExpr) {
         return std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(allExpr), number);
@@ -493,6 +568,86 @@
     }
 }
 
+void PNMLParser::collectColorsInTuple(rapidxml::xml_node<>* element, std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>>& collectedColors){	
+    if (strcmp(element->name(), "tuple") == 0) {	
+        for (auto it = element->first_node(); it; it = it->next_sibling()) {	
+            collectColorsInTuple(it->first_node(), collectedColors);	
+        }	
+    } else if (strcmp(element->name(), "all") == 0) {	
+        std::vector<PetriEngine::Colored::ColorExpression_ptr> expressionsToAdd;	
+        auto expr = parseAllExpression(element);	
+        std::unordered_map<uint32_t, std::vector<const PetriEngine::Colored::Color *>> constantMap;	
+        uint32_t index = 0;	
+        expr->getConstants(constantMap, index);	
+        for(auto positionColors : constantMap){	
+            for(auto color : positionColors.second){	
+                expressionsToAdd.push_back(std::make_shared<PetriEngine::Colored::UserOperatorExpression>(color));	
+            }            	
+        }	
+        collectedColors.push_back(expressionsToAdd);	
+        return;	
+    } else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {	
+        collectColorsInTuple(element->first_node(), collectedColors);	
+    } else if (strcmp(element->name(), "useroperator") == 0 || strcmp(element->name(), "dotconstant") == 0 || strcmp(element->name(), "variable") == 0 	
+                    || strcmp(element->name(), "successor") == 0 || strcmp(element->name(), "predecessor") == 0) {	
+        std::vector<PetriEngine::Colored::ColorExpression_ptr> expressionsToAdd;	
+        auto color = parseColorExpression(element);	
+        expressionsToAdd.push_back(color);	
+        collectedColors.push_back(expressionsToAdd);	
+        return;	
+    } else{	
+        printf("Could not collect tuple colors from arc expression '%s'\n", element->name());	
+        return;	
+    }	
+}
+
+PetriEngine::Colored::ArcExpression_ptr PNMLParser::constructAddExpressionFromTupleExpression(rapidxml::xml_node<>* element,std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors, uint32_t numberof){	
+    auto initCartesianSet = cartesianProduct(collectedColors[0], collectedColors[1]);	
+    for(uint32_t i = 2; i < collectedColors.size(); i++){	
+        initCartesianSet = cartesianProduct(initCartesianSet, collectedColors[i]);	
+    }	
+    std::vector<PetriEngine::Colored::NumberOfExpression_ptr> numberOfExpressions;	
+    for(auto set : initCartesianSet){	
+        std::vector<PetriEngine::Colored::ColorExpression_ptr> colors;	
+        for (auto color : set) {	
+            colors.push_back(color);	
+        }	
+        std::shared_ptr<PetriEngine::Colored::TupleExpression> tupleExpr = std::make_shared<PetriEngine::Colored::TupleExpression>(std::move(colors));	
+        tupleExpr->setColorType(tupleExpr->getColorType(colorTypes));	
+        std::vector<PetriEngine::Colored::ColorExpression_ptr> placeholderVector;	
+        placeholderVector.push_back(tupleExpr);	
+        numberOfExpressions.push_back(std::make_shared<PetriEngine::Colored::NumberOfExpression>(std::move(placeholderVector),numberof));	
+    }	
+    std::vector<PetriEngine::Colored::ArcExpression_ptr> constituents;	
+    for (auto expr : numberOfExpressions) {	
+        constituents.push_back(expr);	
+    }	
+    return std::make_shared<PetriEngine::Colored::AddExpression>(std::move(constituents));	
+}
+    
+std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> PNMLParser::cartesianProduct(std::vector<PetriEngine::Colored::ColorExpression_ptr> rightSet, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftSet){	
+    std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> returnSet;	
+    for(auto expr : rightSet){	
+        for(auto expr2 : leftSet){	
+            std::vector<PetriEngine::Colored::ColorExpression_ptr> toAdd;	
+            toAdd.push_back(expr);	
+            toAdd.push_back(expr2);	
+            returnSet.push_back(toAdd);	
+        }	
+    }	
+    return returnSet;	
+}	
+std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> PNMLParser::cartesianProduct(std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> rightSet, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftSet){	
+    std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> returnSet;	
+    for(auto set : rightSet){	
+        for(auto expr2 : leftSet){	
+            set.push_back(expr2);	
+            returnSet.push_back(set);	
+        }	
+    }	
+    return returnSet;	
+}
+
 void PNMLParser::parseElement(rapidxml::xml_node<>* element) {
     
     for (auto it = element->first_node(); it; it = it->next_sibling()) {
@@ -514,11 +669,11 @@
         } else if (strcmp(it->name(),"queries") == 0) {
             parseQueries(it);
         } else if (strcmp(it->name(), "k-bound") == 0) {
-            std::cerr << "k-bound should be given as command line option -k" << std::endl;
-            exit(ErrorCode);
+            //std::cerr << "k-bound should be given as command line option -k" << std::endl;
+            //exit(ErrorCode);
         } else if (strcmp(it->name(),"query") == 0) {
-            std::cerr << "query tag not supported, please use PQL or XML-style queries instead" << std::endl;
-            exit(ErrorCode);            
+            //std::cerr << "query tag not supported, please use PQL or XML-style queries instead" << std::endl;
+            //exit(ErrorCode);            
         }
         else
         {
@@ -527,6 +682,41 @@
     }
 }
 
+std::pair<string, std::vector<const Colored::Color*>> PNMLParser::parseTimeConstraint(rapidxml::xml_node<> *element) { // parses the inscription and colors belonging to either an interval or invariant and returns it.
+    string colorTypeName;
+    string inscription;
+    std::vector<const Colored::Color*> colors;
+    for (auto i = element->first_node(); i; i = i->next_sibling()) {
+        if (strcmp(i->name(), "colortype") == 0) {
+            colorTypeName = i->first_attribute("name")->value();
+
+            if (colorTypes.find(colorTypeName) == colorTypes.end()) {
+                cerr << "The color type " << colorTypeName << " does not exist" << std::endl;
+                exit(ErrorCode);
+            }
+            else {
+                for (auto it = i->first_node(); it; it = it->next_sibling()) {
+                    if (strcmp(it->name(), "color") == 0) {
+                        Colored::Color* test = new Colored::Color(colorTypes[colorTypeName], 0, it->first_attribute("value")->value());
+                        colors.push_back(test);
+
+                    }
+                    else {
+                        std::cerr << "the colortype to the place element " << element->first_attribute("id")->value() << " does not have or should only have colors" << std::endl;
+                        exit(ErrorCode);
+                    }
+                }
+            }
+
+
+        } else if (strcmp(i->name(), "inscription") == 0) {
+            inscription = i->first_attribute("inscription")->value();
+
+        }
+    }
+    return std::make_pair(inscription, colors);
+}
+
 void PNMLParser::parseQueries(rapidxml::xml_node<>* element) {
     std::string query;
 
@@ -542,17 +732,44 @@
 
 void PNMLParser::parsePlace(rapidxml::xml_node<>* element) {
     double x = 0, y = 0;
+<<<<<<< TREE
     std::string id(element->first_attribute("id")->value());
+=======
+    string starInvariant;
+    string id(element->first_attribute("id")->value());
+>>>>>>> MERGE-SOURCE
     
     auto initial = element->first_attribute("initialMarking");
     long long initialMarking = 0;
     PetriEngine::Colored::Multiset hlinitialMarking;
     PetriEngine::Colored::ColorType* type = nullptr;
+    std::vector<PetriEngine::Colored::TimeInvariant> timeInvariants;
     if(initial)
          initialMarking = atoll(initial->value());
 
+    if (isTimed) {
+        auto posX = element->first_attribute("positionX");
+        if (posX != nullptr){
+             x = atoll(posX->value());
+        }
+        auto posY = element->first_attribute("positionY");
+        if ( posY != nullptr){
+            y = atoll(posY->value());
+        }
+        auto invariant = element->first_attribute("invariant");
+        if(invariant != nullptr){
+            starInvariant = invariant->value();
+        }
+        
+
+        std::vector<const Colored::Color*> colors;
+        colors.push_back(new Colored::Color());
+        timeInvariants.push_back(Colored::TimeInvariant::createFor(starInvariant, colors, constantValues));
+    } 
+
     for (auto it = element->first_node(); it; it = it->next_sibling()) {
         // name element is ignored
+<<<<<<< TREE
         if (strcmp(it->name(), "graphics") == 0) {
             parsePosition(it, x, y);
         } else if (strcmp(it->name(),"initialMarking") == 0) {
@@ -566,6 +783,33 @@
             hlinitialMarking = parseArcExpression(it->first_node("structure"))->eval(context);
         } else if (strcmp(it->name(), "type") == 0) {
             type = parseUserSort(it);
+=======
+        if (isTimed) {
+            if (strcmp(it->name(), "colorinvariant") == 0) {
+                std::pair<string, std::vector<const Colored::Color*>> pair = parseTimeConstraint(it);
+                timeInvariants.push_back(Colored::TimeInvariant::createFor(pair.first, pair.second, constantValues));
+            } else if (strcmp(it->name(),"hlinitialMarking") == 0) {
+                std::unordered_map<std::string, const PetriEngine::Colored::Color*> binding;
+                PetriEngine::Colored::ExpressionContext context {binding, colorTypes};
+                hlinitialMarking = parseArcExpression(it->first_node("structure"))->eval(context);
+            } else if (strcmp(it->name(), "type") == 0) {
+                type = parseUserSort(it);
+            }
+        } else {
+            if (strcmp(it->name(), "graphics") == 0) {
+                parsePosition(it, x, y);
+            } else if (strcmp(it->name(),"initialMarking") == 0) {
+                string text;
+                parseValue(it, text);
+                initialMarking = atoll(text.c_str());
+            } else if (strcmp(it->name(),"hlinitialMarking") == 0) {
+                std::unordered_map<std::string, const PetriEngine::Colored::Color*> binding;
+                PetriEngine::Colored::ExpressionContext context {binding, colorTypes};
+                hlinitialMarking = parseArcExpression(it->first_node("structure"))->eval(context);
+            } else if (strcmp(it->name(), "type") == 0) {
+                type = parseUserSort(it);
+            }
+>>>>>>> MERGE-SOURCE
         }
     }
     
@@ -584,7 +828,10 @@
         }
         else
         {
-            builder->addPlace(id, type, std::move(hlinitialMarking), x, y);
+            if (isTimed)
+                builder->addPlace(id, std::move(hlinitialMarking), type, timeInvariants, x, y);
+            else
+                builder->addPlace(id, type, std::move(hlinitialMarking), x, y);
         }
     }
     //Map id to name
@@ -599,17 +846,31 @@
             target = element->first_attribute("target")->value();
     int weight = 1;
     auto type = element->first_attribute("type");
-    if(type && strcmp(type->value(), "timed") == 0)
+    bool transport = false;
+    string starInterval;
+    bool normal = false;
+    std::string transportID = "0";
+    std::vector<Colored::TimeInterval> timeIntervals;
+    if((type && strcmp(type->value(), "timed") == 0) || (element && strcmp(element->name(), "timedArc") == 0))
     {
-        std::cerr << "timed arcs are not supported" << std::endl;
-        exit(ErrorCode);
+        //TODO:: parse standard interval
     }
-    else if(type && strcmp(type->value(), "inhibitor") == 0)
+    else if((type && strcmp(type->value(), "inhibitor") == 0) || (element && strcmp(element->name(), "inhibitorArc") == 0) || (type && strcmp(type->value(), "tapnInhibitor") == 0))
     {
+        std::cout << "Found inhib arc" << std::endl;
         inhibitor = true;
     }
+    else if((type && strcmp(type->value(), "transport") == 0) || (element && strcmp(element->name(), "transportArc") == 0))
+    {
+        transportID = element->first_attribute("transportID")->value();
+        transport = true;
+    }
+    else if ((type && strcmp(type->value(), "normal") == 0) || (element && (strcmp(element->name(), "inputArc") == 0 || strcmp(element->name(), "outputArc") == 0))) {
+        normal = true;
+    }
 
     bool first = true;
+<<<<<<< TREE
     for (auto it = element->first_node("inscription"); it; it = it->next_sibling("inscription")) {
         std::string text;
         parseValue(it, text);
@@ -619,13 +880,32 @@
             std::cerr << "ERROR: Found non-integer-text in inscription-tag (weight) on arc from " << source << " to " << target << " with value \"" << text << "\". An integer was expected." << std::endl;
             exit(ErrorCode);
         }
+=======
+    auto weightTag = element->first_attribute("weight");
+    if(weightTag != nullptr){
+        string text;
+        weight = atoi(weightTag->value());
+>>>>>>> MERGE-SOURCE
         assert(weight > 0);
-        if(!first)
-        {
-            std::cerr << "ERROR: Multiple inscription tags in xml of a arc from " << source << " to " << target << "." << std::endl;
-            exit(ErrorCode);
+    } else {
+        for (auto it = element->first_node("inscription"); it; it = it->next_sibling("inscription")) {
+            string text;
+            parseValue(it, text);
+            weight = atoi(text.c_str());
+            /*
+            if(std::find_if(text.begin(), text.end(), [](char c) { return !std::isdigit(c) && !std::isblank(c); }) != text.end())
+            {
+                std::cerr << "ERROR: Found non-integer-text in inscription-tag (weight) on arc from " << source << " to " << target << " with value \"" << text << "\". An integer was expected." << std::endl;
+                exit(ErrorCode);
+            }*/
+            assert(weight > 0);
+            if(!first)
+            {
+                std::cerr << "ERROR: Multiple inscription tags in xml of a arc from " << source << " to " << target << "." << std::endl;
+                exit(ErrorCode);
+            }
+            first = false;
         }
-        first = false;
     }
     
     PetriEngine::Colored::ArcExpression_ptr expr;
@@ -639,31 +919,36 @@
         }
         first = false;
     }
+    if(isTimed && !normal && !inhibitor) {
+        starInterval = element->first_attribute("inscription")->value();
+        std::vector<const Colored::Color*> colors;
+        colors.push_back(new Colored::Color());
+        timeIntervals.push_back(Colored::TimeInterval::createFor(starInterval, colors, constantValues));
+        for (auto it = element->first_node("colorinterval"); it; it = it->next_sibling("colorinterval")) {
+            std::pair<string, std::vector<const Colored::Color*>> pair = parseTimeConstraint(it);
+            timeIntervals.push_back(Colored::TimeInterval::createFor(pair.first, pair.second, constantValues));
+        }
+    }
     
-    if (isColored)
+    if (isColored && !normal && !inhibitor)
         assert(expr != nullptr);
     Arc arc;
     arc.source = source;
     arc.target = target;
     arc.weight = weight;
-    arc.expr = expr;
+    arc.inhib = inhibitor;
+    arc.transport = transport;
+    arc.normal = normal;
+    arc.transportID = transportID;
+    if(!inhibitor)
+        arc.expr = expr;
+    if(!normal && !inhibitor)
+        arc.interval = timeIntervals;
     assert(weight > 0);
     
-    if (inhibitor && isColored) {
-        std::cerr << "inhibitor arcs are not supported in colored Petri nets" << std::endl;
-        exit(ErrorCode);
-    }
-    
     if(weight != 0)
-    {
-        if(inhibitor)
-        {
-            inhibarcs.push_back(arc);   
-        }
-        else
-        {
-            arcs.push_back(arc);
-        }
+    { 
+        arcs.push_back(arc);
     }
     else
     {
@@ -703,6 +988,23 @@
     t.y = 0;
     t.id = element->first_attribute("id")->value();
     t.expr = nullptr;
+    t.urgent = false;
+
+
+    if(isTimed) {
+        auto posX = element->first_attribute("positionX");
+        if (posX != nullptr){
+             t.x = atoll(posX->value());
+        }
+        auto posY = element->first_attribute("positionY");
+        if ( posY != nullptr){
+            t.y = atoll(posY->value());
+        }
+        auto urgent = element->first_attribute("urgent");
+        if (urgent != nullptr) {
+            t.urgent = stringToBool(urgent->value());
+        }        
+    }
 
 
     for (auto it = element->first_node(); it; it = it->next_sibling()) {
@@ -768,6 +1070,7 @@
     printf("Could not find color: %s\nCANNOT_COMPUTE\n", name);
     exit(ErrorCode);
 }
+<<<<<<< TREE
 
 const PetriEngine::Colored::Color* PNMLParser::findColorForIntRange(const char* value, uint32_t start, uint32_t end) const{	
 	for (const auto& elem : colorTypes) {	
@@ -780,3 +1083,6 @@
 	printf("Could not find color: %s\nCANNOT_COMPUTE\n", value);	
 	exit(ErrorCode);	
 }
+=======
+
+>>>>>>> MERGE-SOURCE

=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp	2021-04-16 18:53:36 +0000
+++ src/VerifyPN.cpp	2021-04-19 13:50:22 +0000
@@ -330,6 +330,7 @@
         {
             options.model_out_file = std::string(argv[++i]);
         }
+<<<<<<< TREE
         else if (strcmp(argv[i], "--write-buchi") == 0)
         {
             options.buchi_out_file = std::string(argv[++i]);
@@ -354,6 +355,14 @@
                 ++i;
             }
         }
+=======
+        else if (strcmp(argv[i], "-verifydtapn") == 0 ) {
+            std::string outputOption = argv[++i];
+            if (outputOption.compare("tt") == 0 ) {
+                options.outputVerifydtapnFormat = true;
+            }
+        }
+>>>>>>> MERGE-SOURCE
 #ifdef VERIFYPN_MC_Simplification
         else if (strcmp(argv[i], "-z") == 0)
         {
@@ -464,6 +473,7 @@
 #ifdef VERIFYPN_MC_Simplification
                     "  -z <number of cores>                 Number of cores to use (currently only query simplification)\n"
 #endif
+<<<<<<< TREE
                     "  -tar                                 Enables Trace Abstraction Refinement for reachability properties\n"
                     "  --max-intervals <interval count>     The max amount of intervals kept when computing the color fixpoint\n"
                     "                  <interval count>     Default is 255 and then after <interval-timeout> second(s) to 5\n"
@@ -482,6 +492,18 @@
                     "                                       For some queries this helps reduce the overhead of query\n"
                     "                                       simplification and Büchi construction, but gives worse\n"
                     "                                       results since there is less opportunity for optimizations.\n"
+=======
+                    "  -tar                               Enables Trace Abstraction Refinement for reachability properties\n"
+                    "  -verifydtapn <tt>                  Specifies the format of the output model (tt is currently the only valid value)\n"
+                    "                                     - tt output as dtapn format\n"
+                    "  --write-simplified <filename>      Outputs the queries to the given file after simplification\n"
+                    "  --write-reduced <filename>         Outputs the model to the given file after structural reduction\n"
+                    "  --binary-query-io <0,1,2,3>        Determines the input/output format of the query-file\n"
+                    "                                     - 0 MCC XML format for Input and Output\n"
+                    "                                     - 1 Input is binary, output is XML\n"
+                    "                                     - 2 Output is binary, input is XML\n"
+                    "                                     - 3 Input and Output is binary\n"
+>>>>>>> MERGE-SOURCE
                     "\n"
                     "Return Values:\n"
                     "  0   Successful, query satisfiable\n"
@@ -833,7 +855,11 @@
         out.open(filename, std::ios::binary | std::ios::out);
         uint32_t cnt = 0;
         for(uint32_t j = 0; j < queries.size(); j++) {
-            if(queries[j]->isTriviallyTrue() || queries[j]->isTriviallyFalse()) continue;
+            if(queries[j]->isTriviallyTrue())
+                queries[j] = std::make_shared<EFCondition>(std::make_shared<BooleanCondition>(true));
+            else if(queries[j]->isTriviallyFalse())
+                queries[j] = std::make_shared<EFCondition>(std::make_shared<BooleanCondition>(false));
+            
             ++cnt;
         }
         out.write(reinterpret_cast<const char *>(&cnt), sizeof(uint32_t));
@@ -854,7 +880,10 @@
 
     for(uint32_t j = 0; j < queries.size(); j++) {
         auto i = order[j];
-        if(queries[i]->isTriviallyTrue() || queries[i]->isTriviallyFalse()) continue;
+        if(queries[i]->isTriviallyTrue())
+            queries[i] = std::make_shared<EFCondition>(std::make_shared<BooleanCondition>(true));
+        else if(queries[i]->isTriviallyFalse())
+            queries[i] = std::make_shared<EFCondition>(std::make_shared<BooleanCondition>(false));
         if(binary)
         {
             out.write(querynames[i].data(), querynames[i].size());
@@ -998,6 +1027,7 @@
     if (options.printstatistics) {
         std::cout << "Finished parsing model" << std::endl;
     }
+    
 
     //----------------------- Parse Query -----------------------//
     std::vector<std::string> querynames;
@@ -1095,6 +1125,7 @@
 #endif
             std::vector<std::stringstream> tstream(queries.size());
             uint32_t old = to_handle;
+
             for(size_t c = 0; c < std::min<uint32_t>(options.cores, old); ++c)
             {
 #ifdef VERIFYPN_MC_Simplification
@@ -1126,6 +1157,7 @@
 #endif
                     // this is used later, we already know that this is a plain reachability (or AG)
                     bool wasAGCPNApprox = dynamic_cast<NotCondition*>(queries[i].get()) != nullptr;
+<<<<<<< TREE
                     int preSize=queries[i]->formulaSize();
 
                     if (options.logic == TemporalLogic::LTL) {
@@ -1138,9 +1170,24 @@
                     }
                     queries[i] = Condition::initialMarkingRW([&](){ return queries[i]; }, stats,  context, false, false, true)
                                             ->pushNegation(stats, context, false, false, true);
+=======
+                    int preSize=queries[i]->formulaSize();
+                    //If the reduction time is set to 0 then the queries should not be reduced
+                    if(options.queryReductionTimeout != 0){
+                        queries[i] = Condition::initialMarkingRW([&](){ return queries[i]; }, stats,  context, false, false, true)
+                                        ->pushNegation(stats, context, false, false, true);
+                    } 
+                    
+>>>>>>> MERGE-SOURCE
                     wasAGCPNApprox |= dynamic_cast<NotCondition*>(queries[i].get()) != nullptr;
+<<<<<<< TREE
 
                     if(options.queryReductionTimeout > 0 && options.printstatistics) {
+=======
+                    
+                    if(options.queryReductionTimeout > 0 && options.printstatistics)
+                    {
+>>>>>>> MERGE-SOURCE
                         out << "RWSTATS PRE:";
                         stats.print(out);
                         out << std::endl;
@@ -1191,9 +1238,9 @@
                     if(options.cpnOverApprox && wasAGCPNApprox)
                     {
                         if(queries[i]->isTriviallyTrue())
-                            queries[i] = std::make_shared<BooleanCondition>(false);
+                            queries[i] = std::make_shared<EFCondition>(std::make_shared<BooleanCondition>(true));
                         else if(queries[i]->isTriviallyFalse())
-                            queries[i] = std::make_shared<BooleanCondition>(true);
+                            queries[i] = std::make_shared<EFCondition>(std::make_shared<BooleanCondition>(false));
                         queries[i]->setInvariant(wasAGCPNApprox);
                     }
 
@@ -1243,7 +1290,26 @@
                 return queries[a]->containsNext() < queries[b]->containsNext();
             return queries[a]->formulaSize() < queries[b]->formulaSize();
         });
-        writeQueries(queries, querynames, reorder, options.query_out_file, options.binary_query_io & 2, builder.getPlaceNames());
+        // if (options.outputVerifydtapnFormat) {
+        //     std::ofstream queryFile(options.query_out_file);
+        //     for (uint32_t i = 0; i < queries.size(); ++i) {
+        //         std::cout << "Writing query ";
+        //         queries[i].get()->toString(std::cout);
+        //         std::cout << std::endl;
+
+        //         if(queries[i]->isTriviallyTrue()){
+        //             std::cout << "trivially true" << std::endl;
+        //             queries[i] = std::make_shared<EFCondition>(std::make_shared<BooleanCondition>(true));
+        //         } else if(queries[i]->isTriviallyFalse()){
+        //             queries[i] = std::make_shared<EFCondition>(std::make_shared<BooleanCondition>(false));
+        //             std::cout << "trivially false" << std::endl;
+        //         }
+        //         queries[i].get()->toString(queryFile);
+        //     }
+
+        // } else {
+            writeQueries(queries, querynames, reorder, options.query_out_file, options.binary_query_io & 2, builder.getPlaceNames());
+        // }
     }
 
     qnet = nullptr;
@@ -1306,7 +1372,7 @@
     {
         std::fstream file;
         file.open(options.model_out_file, std::ios::out);
-        net->toXML(file);
+        net->toXML(file, cpnBuilder.isTimed(), cpnBuilder.getInvariants(), options.outputVerifydtapnFormat);
     }
 
     if(alldone) return SuccessCode;