Merge lp:~tapaal-contributor/verifypn/update-parser into lp:verifypn

[Thomas Pedersen]

Small changes made for the interaction with the colored GUI:

Handle passing and unfolding of inhibitor arcs.
Add options for retrieving the unfolded net and queries before reductions.
Fix scalar products, such that the scalar is applied.

This branch also contains the latest version of the unfolding techniques.

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

Generally, check if you can use const-ref, use typedefs, and try to chop your methods/functions into smaller pieces.

Also remove dead/commented out elements where it is no longer needed - and validate that the "fail on error"-pieces you removed should really be removed (i.e. the calls to std::exit).

review: Needs Fixing

[lp:~tapaal-contributor/verifypn/update-parser]

245. By Peter Haahr Taankvist on 2021-06-10

Merge in parser fix from optimize unfolding

246. By Peter Haahr Taankvist on 2021-06-10

Delete commented out code

247. By Thomas Pedersen <email address hidden> on 2021-06-10

Fix comments, split up functions and add typedefs

[Thomas Pedersen (tpede16)]

We have tried to fix the comments and we left a few of our own where we could not fix it.

[lp:~tapaal-contributor/verifypn/update-parser]

248. By Peter G. Jensen <email address hidden> on 2021-06-10

less moving, more const

249. By Peter G. Jensen <email address hidden> on 2021-06-10

finishing comment

250. By Thomas Pedersen <email address hidden> on 2021-06-11

Improve arguments in color.h

251. By Thomas Pedersen <email address hidden> on 2021-06-11

Handle inhibitor arcs in color stripping

252. By Thomas Pedersen <email address hidden> on 2021-06-11

Fix color stripping query marking

253. By Peter Haahr Taankvist on 2021-06-11

Remove unused functions

254. By Thomas Pedersen <email address hidden> on 2021-06-11

Update arguments in guardRestrictor

255. By Thomas Pedersen <email address hidden> on 2021-06-11

Refactor IntervalGenerator

256. By Thomas Pedersen <email address hidden> on 2021-06-14

Fix some return types

257. By Thomas Pedersen <email address hidden> on 2021-06-14

Finish fixing return types

258. By Thomas Pedersen <email address hidden> on 2021-06-14

Handle guard vars not on in arcs

259. By Thomas Pedersen <email address hidden> on 2021-06-14

Fix creation of equivalence classes

260. By Peter G. Jensen <email address hidden> on 2021-06-14

fixing use of dealloc

261. By Thomas Pedersen <email address hidden> on 2021-06-14

Refactor arguments in colored expressions

262. By Thomas Pedersen <email address hidden> on 2021-06-15

Fix adding tokens to color fixpoint

263. By Thomas Pedersen <email address hidden> on 2021-06-15

Move EquivalenceVec to class

264. By Thomas Pedersen <email address hidden> on 2021-06-17

Fix partitionbuilder constructor and errors added in refactoring

265. By Thomas Pedersen <email address hidden> on 2021-06-21

Update partitionBuilder arguments and equivalenceVec functions

266. By Thomas Pedersen <email address hidden> on 2021-06-21

Update arguments in ColoredPetriNetBuilder

267. By Thomas Pedersen <email address hidden> on 2021-06-21

Make multiset iterator const

268. By Thomas Pedersen <email address hidden> on 2021-06-21

Add some more const references

269. By Thomas Pedersen <email address hidden> on 2021-06-21

Include erase operation in simplify loop

270. By Peter G. Jensen <email address hidden> on 2021-06-22

more const-ref, in particular in loops. Removed some pointers also

271. By Peter G. Jensen <email address hidden> on 2021-06-22

cleaning up types & refactoring

272. By Peter G. Jensen <email address hidden> on 2021-06-22

Merged removal of debug output

273. By Peter G. Jensen <email address hidden> on 2021-06-22

cleanup

274. By Thomas Pedersen <email address hidden> on 2021-06-23

Remove side effect of static function

275. By Thomas Pedersen <email address hidden> on 2021-06-24

Implement var resrictions for inequality

276. By Thomas Pedersen <email address hidden> on 2021-06-24

Remove unused notExpression

277. By Thomas Pedersen <email address hidden> on 2021-06-24

Disable stable places check when fixpoint has not been computed

278. By Thomas Pedersen <email address hidden> on 2021-07-05

Attempt to fix dot constant colortype assignment

279. By Peter G. Jensen <email address hidden> on 2021-07-05

removing funky static, fixing types, more const

280. By Peter G. Jensen <email address hidden> on 2021-07-05

removing unused method

281. By Peter G. Jensen <email address hidden> on 2021-07-05

no need for casting

282. By Peter G. Jensen <email address hidden> on 2021-07-05

remember to deallocate

283. By Peter G. Jensen <email address hidden> on 2021-07-05

unused field removed

284. By Peter G. Jensen <email address hidden> on 2021-07-05

fixed deallocation

285. By Thomas Pedersen <email address hidden> on 2021-07-05

Remove unused loop and old comment

286. By Thomas Pedersen <email address hidden> on 2021-07-05

Re-add relevant comment

287. By Thomas Pedersen <email address hidden> on 2021-07-06

Fix inequality implementation to not just invert the varmap

288. By Peter G. Jensen <email address hidden> on 2021-07-06

making destructor virtual

289. By Peter G. Jensen <email address hidden> on 2021-07-06

fixing off-by-one when reducing, leading to segfault

290. By Peter G. Jensen <email address hidden> on 2021-07-06

removing unused code, initializing variable

291. By Peter G. Jensen <email address hidden> on 2021-07-06

fixing simplify again

292. By Peter G. Jensen <email address hidden> on 2021-07-06

remove unused variable

293. By Peter G. Jensen <email address hidden> on 2021-07-06

fixing type

294. By Peter G. Jensen <email address hidden> on 2021-07-06

fixing loop guard

295. By Thomas Pedersen <email address hidden> on 2021-07-06

Reset both sides in inequality after equality fails

296. By Peter G. Jensen <email address hidden> on 2021-07-07

updated text in help

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

review: Approve

[Jiri Srba (srba)]

Compiles on mac.

review: Approve

=== modified file 'include/PetriEngine/AbstractPetriNetBuilder.h'
--- include/PetriEngine/AbstractPetriNetBuilder.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/AbstractPetriNetBuilder.h	2021-07-07 08:15:00 +0000
@@ -27,7 +27,6 @@
 #include "Colored/Expressions.h"
 
 namespace PetriEngine {
-
     /** Abstract builder for petri nets */
     class AbstractPetriNetBuilder {
     protected:
@@ -41,7 +40,7 @@
                 double y = 0) = 0;
         /** Add a new colored place with a unique name */
         virtual void addPlace(const std::string& name,
-                Colored::ColorType* type,
+                const Colored::ColorType* type,
                 Colored::Multiset&& tokens,
                 double x = 0,
                 double y = 0)
@@ -70,7 +69,8 @@
         /** 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);
@@ -89,7 +89,7 @@
         }
         /** Add color types with id */
         virtual void addColorType(const std::string& id,
-                Colored::ColorType* type)
+                const Colored::ColorType* type)
         {
             std::cerr << "Color types are not supported in standard P/T nets" << std::endl;
             exit(ErrorCode);

=== modified file 'include/PetriEngine/Colored/ArcIntervals.h'
--- include/PetriEngine/Colored/ArcIntervals.h	2021-03-15 10:04:47 +0000
+++ include/PetriEngine/Colored/ArcIntervals.h	2021-07-07 08:15:00 +0000
@@ -25,69 +25,22 @@
     namespace Colored {
 
         struct ArcIntervals {
-            std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> _varIndexModMap;
-            std::vector<Colored::intervalTuple_t> _intervalTupleVec;
-            Colored::ColorFixpoint * _source;
+            VariableModifierMap _varIndexModMap;
+            std::vector<Colored::interval_vector_t> _intervalTupleVec;
+            const Colored::ColorFixpoint * _source;
             
             ~ArcIntervals() {_varIndexModMap.clear();}
             ArcIntervals() {
             }
 
-            ArcIntervals(Colored::ColorFixpoint * source) : _source(source){
-            }
-
-            ArcIntervals(Colored::ColorFixpoint * source, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varIndexModMap) : _varIndexModMap(varIndexModMap), _source(source) {
-            };
-
-            ArcIntervals(Colored::ColorFixpoint * source, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varIndexModMap,  std::vector<Colored::intervalTuple_t> ranges) : _varIndexModMap(varIndexModMap), _intervalTupleVec(ranges), _source(source) {
-            };
-
-            size_t size() {
-                return _intervalTupleVec.size();
-            }
-
-            Colored::intervalTuple_t& operator[] (size_t index) {
-                return _intervalTupleVec[index];
-            }
-            
-            Colored::intervalTuple_t& operator[] (int index) {
-                return _intervalTupleVec[index];
-            }
-            
-            Colored::intervalTuple_t& operator[] (uint32_t index) {
-                assert(index < _intervalTupleVec.size());
-                return _intervalTupleVec[index];
-            }
-
-            Colored::intervalTuple_t& back(){
-                return _intervalTupleVec.back();
-            }
-
-            bool hasValidIntervals(){
-                for(auto intervalTuple : _intervalTupleVec){
-                    if (intervalTuple.hasValidIntervals()){
-                        return true;
-                    }
-                }
-                return false;
-            }
-
-            bool containsVariable(Colored::Variable * var){
-                for (auto varModPair : _varIndexModMap){
-                    if(varModPair.first == var){
-                        return true;
-                    }
-                }
-                return false;
-            }
-
-            std::set<const Colored::Variable *> getVariables(){
-                std::set<const Colored::Variable *> res;
-                for (auto varModPair : _varIndexModMap){
-                    res.insert(varModPair.first);
-                }
-                return res;
-            }
+            ArcIntervals(const Colored::ColorFixpoint * source) : _source(source){
+            }
+
+            ArcIntervals(const Colored::ColorFixpoint * source, VariableModifierMap varIndexModMap) : _varIndexModMap(varIndexModMap), _source(source) {
+            };
+
+            ArcIntervals(const Colored::ColorFixpoint * source, VariableModifierMap varIndexModMap,  std::vector<Colored::interval_vector_t> ranges) : _varIndexModMap(varIndexModMap), _intervalTupleVec(ranges), _source(source) {
+            };
 
             void print() {
                 std::cout << "[ ";

=== modified file 'include/PetriEngine/Colored/BindingGenerator.h'
--- include/PetriEngine/Colored/BindingGenerator.h	2021-04-14 10:41:18 +0000
+++ include/PetriEngine/Colored/BindingGenerator.h	2021-07-07 08:15:00 +0000
@@ -25,8 +25,6 @@
 
 namespace PetriEngine {
 
-    typedef std::unordered_map<std::string, Colored::ColorType*> ColorTypeMap;
-
     class NaiveBindingGenerator {
     public:
         class Iterator {
@@ -39,22 +37,21 @@
             bool operator==(Iterator& other);
             bool operator!=(Iterator& other);
             Iterator& operator++();
-            const Colored::ExpressionContext::BindingMap operator++(int);
-            Colored::ExpressionContext::BindingMap& operator*();
+            const Colored::BindingMap& operator*() const;
         };
     private:
         Colored::GuardExpression_ptr _expr;
-        Colored::ExpressionContext::BindingMap _bindings;
-        ColorTypeMap& _colorTypes;
+        Colored::BindingMap _bindings;
+        Colored::ColorTypeMap& _colorTypes;
         
-        bool eval();
+        bool eval() const;
         
     public:
-        NaiveBindingGenerator(Colored::Transition& transition,
-                ColorTypeMap& colorTypes);
+        NaiveBindingGenerator(const Colored::Transition& transition,
+                Colored::ColorTypeMap& colorTypes);
 
-        Colored::ExpressionContext::BindingMap& nextBinding();
-        Colored::ExpressionContext::BindingMap& currentBinding();
+        const Colored::BindingMap& nextBinding();
+        const Colored::BindingMap& currentBinding() const;
         bool isInitial() const;
         Iterator begin();
         Iterator end();
@@ -73,32 +70,42 @@
             bool operator==(Iterator& other);
             bool operator!=(Iterator& other);
             Iterator& operator++();
-            const Colored::ExpressionContext::BindingMap operator++(int);
-            Colored::ExpressionContext::BindingMap& operator*();
+            const Colored::BindingMap operator++(int);
+            const Colored::BindingMap& operator*() const;
         };
     private:
-        Colored::GuardExpression_ptr _expr;
-        Colored::ExpressionContext::BindingMap _bindings;
-        ColorTypeMap& _colorTypes;
-        Colored::Transition &_transition;
+        const Colored::GuardExpression_ptr &_expr;
+        Colored::BindingMap _bindings;
+        std::vector<std::vector<std::vector<uint32_t>>> _symmetric_var_combinations;
+        const Colored::ColorTypeMap& _colorTypes;
+        const Colored::Transition &_transition;
+        const std::vector<std::set<const Colored::Variable *>>& _symmetric_vars;
+        Colored::BindingMap::iterator _bindingIterator;
         bool _isDone;
         bool _noValidBindings;
         uint32_t _nextIndex = 0;
+        uint32_t _currentOuterId = 0;
+        uint32_t _currentInnerId = 0;
+        uint32_t _symmetric_vars_set = 0;
         
-        bool eval();
+        bool eval() const;
+        bool assignSymmetricVars();
+        void generateCombinations(
+            uint32_t options,
+            uint32_t samples,
+            std::vector<std::vector<uint32_t>> &result,
+            std::vector<uint32_t> &current) const;
         
     public:
-        FixpointBindingGenerator(Colored::Transition& transition,
-                ColorTypeMap& colorTypes);
+        FixpointBindingGenerator(const Colored::Transition &transition,
+                const Colored::ColorTypeMap& colorTypes,  const std::vector<std::set<const Colored::Variable *>>& symmetric_vars);
 
         FixpointBindingGenerator(const FixpointBindingGenerator& ) = default;
         
-        FixpointBindingGenerator operator= (const FixpointBindingGenerator& b) {
-            return FixpointBindingGenerator(b);
-        }
+        FixpointBindingGenerator& operator= (const FixpointBindingGenerator& b) = default;
 
-        Colored::ExpressionContext::BindingMap& nextBinding();
-        Colored::ExpressionContext::BindingMap& currentBinding();
+        const Colored::BindingMap& nextBinding();
+        const Colored::BindingMap& currentBinding() const;
         bool isInitial() const;
         Iterator begin();
         Iterator end();

=== modified file 'include/PetriEngine/Colored/ColoredNetStructures.h'
--- include/PetriEngine/Colored/ColoredNetStructures.h	2021-04-29 09:42:52 +0000
+++ include/PetriEngine/Colored/ColoredNetStructures.h	2021-07-07 08:15:00 +0000
@@ -35,6 +35,7 @@
             uint32_t transition;
             ArcExpression_ptr expr;
             bool input;
+            uint32_t weight;
         };
         
         struct Transition {
@@ -42,14 +43,15 @@
             GuardExpression_ptr guard;
             std::vector<Arc> input_arcs;
             std::vector<Arc> output_arcs;
-            std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>> variableMaps;
+            std::vector<std::unordered_map<const Variable *, interval_vector_t>> variableMaps;
             bool considered;
         };
         
         struct Place {
             std::string name;
-            ColorType* type;
+            const ColorType* type;
             Multiset marking;
+            bool inhibitor;
             bool stable = true;
         };
     }

=== modified file 'include/PetriEngine/Colored/ColoredPetriNetBuilder.h'
--- include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2021-04-29 09:42:52 +0000
+++ include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2021-07-07 08:15:00 +0000
@@ -47,7 +47,7 @@
                 double x = 0,
                 double y = 0) override ;
         void addPlace(const std::string& name,
-                Colored::ColorType* type,
+                const Colored::ColorType* type,
                 Colored::Multiset&& tokens,
                 double x = 0,
                 double y = 0) override;
@@ -64,7 +64,8 @@
                 int) override;
         void addInputArc(const std::string& place,
                 const std::string& transition,
-                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,
                 int weight = 1) override;
@@ -72,7 +73,7 @@
                 const std::string& place,
                 const Colored::ArcExpression_ptr& expr) override;
         void addColorType(const std::string& id,
-                Colored::ColorType* type) override;
+                const Colored::ColorType* type) override;
 
 
         void sort() override;
@@ -85,10 +86,6 @@
             return _partitionTimer;
         }
 
-        double getPartitionVarMapTime() const {
-            return _partitionVarMapTimer;
-        }
-
         double getFixpointTime() const {
             return _fixPointCreationTime;
         }
@@ -115,7 +112,6 @@
         }
 
         uint32_t getUnfoldedPlaceCount() const {
-            //return _nptplaces;
             return _ptBuilder.numberOfPlaces();
         }
 
@@ -142,7 +138,9 @@
         PetriNetBuilder& unfold();
         PetriNetBuilder& stripColors();
         void computePlaceColorFixpoint(uint32_t max_intervals, uint32_t max_intervals_reduced, int32_t timeout);
-        void computePartition();
+        void computePartition(int32_t timeout);
+        void computeSymmetricVariables();
+        void printSymmetricVariables() const;
         
     private:
         std::unordered_map<std::string,uint32_t> _placenames;
@@ -153,16 +151,19 @@
         std::unordered_map<uint32_t,FixpointBindingGenerator> _bindings;
         PTPlaceMap _ptplacenames;
         PTTransitionMap _pttransitionnames;
-        uint32_t _nptplaces = 0;
-        uint32_t _npttransitions = 0;
         uint32_t _nptarcs = 0;
         uint32_t _maxIntervals = 0;
-        PetriEngine::IntervalGenerator intervalGenerator;
+        const Colored::IntervalGenerator intervalGenerator = Colored::IntervalGenerator();
         
         std::vector<Colored::Place> _places;
         std::vector<Colored::Transition> _transitions;
+        std::vector<Colored::Arc> _inhibitorArcs;
         std::vector<Colored::ColorFixpoint> _placeColorFixpoints;
-        ColorTypeMap _colors;
+        //transition id to vector of vectors of variables, where variable in vector are symmetric
+        std::unordered_map<uint32_t, std::vector<std::set<const Colored::Variable *>>> symmetric_var_map;
+
+        std::unordered_map<uint32_t, std::string> _sumPlacesNames;
+        Colored::ColorTypeMap _colors;
         PetriNetBuilder _ptBuilder;
         bool _unfolded = false;
         bool _stripped = false;
@@ -177,33 +178,35 @@
 
         double _partitionTimer = 0;
 
-        double _partitionVarMapTimer = 0;
-
-        std::string arcToString(Colored::Arc& arc) const ;
-
-        void printPlaceTable();
-
-        
-
-        std::unordered_map<uint32_t, Colored::ArcIntervals> setupTransitionVars(Colored::Transition transition);
+        std::string arcToString(const Colored::Arc& arc) const ;
+
+        void printPlaceTable() const;
+
+        void checkSymmetricVarsInArcs(const Colored::Transition &transition, const Colored::Arc &inArc, const std::set<const Colored::Variable*> &inArcVars, bool &isEligible ) const;
+        void checkSymmetricVarsOutArcs(const Colored::Transition &transition, const std::set<const Colored::Variable*> &inArcVars, bool &isEligible) const;
+        void removeInvalidVarmaps(Colored::Transition& transition) const;
+        void addTransitionVars(Colored::Transition& transition) const;
+
+        std::unordered_map<uint32_t, Colored::ArcIntervals> setupTransitionVars(const Colored::Transition &transition) const;
         
         void addArc(const std::string& place,
                 const std::string& transition,
                 const Colored::ArcExpression_ptr& expr,
-                bool input);
+                bool input, bool inhibitor, int weight);
 
         void findStablePlaces();
 
-        void getArcIntervals(Colored::Transition& transition, bool &transitionActivated, uint32_t max_intervals, uint32_t transitionId);      
+        void getArcIntervals(const 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);
         
         void unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color, uint32_t unfoldPlace, uint32_t id);
-        void unfoldTransition(Colored::Transition& transition);
-        void handleOrphanPlace(Colored::Place& place, std::unordered_map<std::string, uint32_t> unfoldedPlaceMap);
+        void unfoldTransition(uint32_t transitionId);
+        void handleOrphanPlace(const Colored::Place& place, const std::unordered_map<std::string, uint32_t> &unfoldedPlaceMap);
         void createPartionVarmaps();
+        void unfoldInhibitorArc(const std::string &oldname, const std::string &newname);
 
-        void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name);
+        void unfoldArc(const Colored::Arc& arc, const Colored::BindingMap& binding, const std::string& name);
     };
     
     //Used for checking if a variable is inside either a succ or pred expression

=== modified file 'include/PetriEngine/Colored/Colors.h'
--- include/PetriEngine/Colored/Colors.h	2021-04-22 12:43:03 +0000
+++ include/PetriEngine/Colored/Colors.h	2021-07-07 08:15:00 +0000
@@ -35,33 +35,38 @@
 namespace PetriEngine {
     namespace Colored {
         class ColorType;
+        class Variable;
+        class Color;
+        
+        typedef std::unordered_map<std::string, const ColorType*> ColorTypeMap;
+        typedef std::unordered_map<const Variable *, const Color *> BindingMap;
 
-        class Color {
+        class Color final {
         public:
             friend std::ostream& operator<< (std::ostream& stream, const Color& color);
             
         protected:
             const std::vector<const Color*> _tuple;
-            ColorType* _colorType;
+            const ColorType * const _colorType;
             std::string _colorName;
             uint32_t _id;
             
         public:
-            Color(ColorType* colorType, uint32_t id, std::vector<const Color*>& colors);
-            Color(ColorType* colorType, uint32_t id, const char* color);
+            Color(const ColorType* colorType, uint32_t id, std::vector<const Color*>& colors);
+            Color(const ColorType* colorType, uint32_t id, const char* color);
             ~Color() {}
             
             bool isTuple() const {
                 return _tuple.size() > 1;
             }
 
-            void getColorConstraints(Colored::interval_t *constraintsVector, uint32_t *index) const;
+            void getColorConstraints(Colored::interval_t& constraintsVector, uint32_t& index) const;
             
-            std::vector<const Color*> getTupleColors() const {
+            const std::vector<const Color*>& getTupleColors() const {
                 return _tuple;
             }
 
-            void getTupleId(std::vector<uint32_t> *idVector) const;
+            void getTupleId(std::vector<uint32_t>& idVector) const;
 
             const std::string& getColorName() const {
                 if (this->isTuple()) {
@@ -70,7 +75,7 @@
                 return _colorName;
             }
             
-            ColorType* getColorType() const {
+            const ColorType* getColorType() const {
                 return _colorType;
             }
             
@@ -99,226 +104,156 @@
             static std::string toString(const std::vector<const Color*>& colors);
         };
         
-        /*
-         *  Singleton pattern from: 
-         * https://stackoverflow.com/questions/1008019/c-singleton-design-pattern
-         */
-        class DotConstant : public Color {
-        private:
-            DotConstant();
-            
-        public:
-            static const Color* dotConstant(ColorType *ct) {
-                static DotConstant _instance;
-                if(ct != nullptr){
-                    _instance._colorType = ct;
-                }
-                return &_instance;
-            }
-            
-            DotConstant(DotConstant const&) = delete;
-            void operator=(DotConstant const&) = delete;
-
-            bool operator== (const DotConstant& other) {
-                return true;
-            }
-        };
-        
         class ColorType {
-        public:
-            class iterator {
-            private:
-                ColorType& type;
-                size_t index;
-
-            public:
-                iterator(ColorType& type, size_t index) : type(type), index(index) {}
-
-                const Color& operator++() {
-                    return type[++index];
-                }
-
-                const Color& operator++(int) {
-                    return type[index++];
-                }
-
-                const Color& operator--() {
-                    return type[--index];
-                }
-                const Color& operator--(int) {
-                    return type[index--];
-                }
-
-                const Color& operator*() {
-                    return type[index];
-                }
-
-                const Color* operator->() {
-                    return &type[index];
-                }
-
-                bool operator==(iterator& other) {
-                    return type == other.type && index == other.index;
-                }
-
-                bool operator!=(iterator& other) {
-                    return !(type == other.type) || index != other.index;
-                }
-            };
-            
         private:
             std::vector<Color> _colors;
-            uintptr_t _id;
-            std::string _name;
+            std::string _name;            
+        public:
             
-        public:
-            ColorType(std::vector<ColorType*> elements);
             ColorType(std::string name = "Undefined") : _colors(), _name(std::move(name)) {
-                _id = (uintptr_t)this;
             }
+
+            virtual ~ColorType() = default;
             
+            static const ColorType* dotInstance();
             virtual void addColor(const char* colorName);
-            virtual void addColor(std::vector<const Color*>& colors);
-            virtual void addDot() {
-                _colors.push_back(*DotConstant::dotConstant(this));
-            }
-            
+
             virtual size_t size() const {
                 return _colors.size();
             }
 
-            virtual size_t productSize() {
+            virtual size_t size(const std::vector<bool> &excludedFields) const {
+                return _colors.size();
+            }
+
+            virtual size_t productSize() const {
                 return 1;
             }
 
-            virtual std::vector<size_t> getConstituentsSizes(){
+            virtual std::vector<size_t> getConstituentsSizes() const{
                 std::vector<size_t> result;                
                 result.push_back(_colors.size());
                 
                 return result;
             }
 
-            virtual Colored::interval_t getFullInterval(){
+            virtual Colored::interval_t getFullInterval() const{
                 Colored::interval_t interval;
-                interval.addRange(Reachability::range_t(0, size()-1));
+                interval.addRange(0, size()-1);
                 return interval;
             }
 
-            virtual void getColortypes(std::vector<ColorType *> &colorTypes){
-                colorTypes.push_back(this);
-            }
-
-            virtual void printConstituents(){
-                std::cout << _name << std::endl;
-            }
-            
-            virtual const Color& operator[] (size_t index) {
-                return _colors[index];
-            }
-            
-            virtual const Color& operator[] (int index) {
-                return _colors[index];
-            }
-            
-            virtual const Color& operator[] (uint32_t index) {
+            virtual void getColortypes(std::vector<const ColorType *> &colorTypes) const{
+                colorTypes.emplace_back(this);
+            }
+            
+            virtual const Color& operator[] (size_t index) const {
+                return _colors[index];
+            }
+            
+            virtual const Color& operator[] (int index) const {
+                return _colors[index];
+            }
+            
+            virtual const Color& operator[] (uint32_t index) const {
                 assert(index < _colors.size());
                 return _colors[index];
             }
             
-            virtual const Color* operator[] (const char* index);
+            virtual const Color* operator[] (const char* index) const;
             
-            virtual const Color* operator[] (const std::string& index) {
+            virtual const Color* operator[] (const std::string& index) const {
                 return (*this)[index.c_str()];
             }
 
-            virtual const Color* getColor(std::vector<uint32_t> ids){
+            virtual const Color* getColor(const std::vector<uint32_t> &ids) const {
                 assert(ids.size() == 1);
                 return &_colors[ids[0]];
             }
             
-            bool operator== (const ColorType& other) const {
-                return _id == other._id;
-            }
-
-            uintptr_t getId() {
-                return _id;
-            }
-
             const std::string& getName() const {
                 return _name;
             }
             
-            iterator begin() {
-                return {*this, 0};
+            std::vector<Color>::const_iterator begin() const {
+                return _colors.begin();
             }
 
-            iterator end() {
-                return {*this, size()};
+            std::vector<Color>::const_iterator end() const {
+                return _colors.end();
             }
         };
-
+        
         class ProductType : public ColorType {
         private:
-            std::vector<ColorType*> constituents;
-            std::unordered_map<size_t,Color> cache;
+            std::vector<const ColorType*> _constituents;
+            mutable std::unordered_map<size_t,Color> _cache;
 
         public:
             ProductType(const std::string& name = "Undefined") : ColorType(name) {}
             ~ProductType() {
-                cache.clear();
+                _cache.clear();
             }
 
-            void addType(ColorType* type) {
-                constituents.push_back(type);
+            void addType(const ColorType* type) {
+                _constituents.push_back(type);
             }
 
             void addColor(const char* colorName) override {}
-            void addColor(std::vector<const Color*>& colors) override {}
-            void addDot() override {}
 
             size_t size() const override {
                 size_t product = 1;
-                for (auto ct : constituents) {
+                for (auto* ct : _constituents) {
                     product *= ct->size();
                 }
                 return product;
             }
 
-            virtual size_t productSize() {
+            size_t size(const std::vector<bool> &excludedFields) const override {
+                size_t product = 1;
+                for (uint32_t i = 0; i < _constituents.size(); i++) {
+                    if(!excludedFields[i]){
+                        product *= _constituents[i]->size();
+                    }                    
+                }
+                return product;
+            }
+
+            virtual size_t productSize() const{
                 size_t size = 0;
-                for (auto ct : constituents){
+                for (auto* ct : _constituents){
                     size += ct->productSize();
                 }
                 return size;
             }
 
-            std::vector<size_t> getConstituentsSizes() override{
+            std::vector<size_t> getConstituentsSizes() const override{
                 std::vector<size_t> result;
-                for (auto ct : constituents) {
+                for (auto* ct : _constituents) {
                     result.push_back(ct->size());
                 }
                 return result;
             }
 
-            Colored::interval_t getFullInterval() override{
+            Colored::interval_t getFullInterval() const override{
                 Colored::interval_t interval;
-                for(auto ct : constituents) {
+                for(auto ct : _constituents) {
                     interval.addRange(Reachability::range_t(0, ct->size()-1));
                 }                
                 return interval;
             }
 
-            void getColortypes(std::vector<ColorType *> &colorTypes) override{
-                for(auto ct : constituents){
+            void getColortypes(std::vector<const ColorType *> &colorTypes) const override{
+                for(auto ct : _constituents){
                     ct->getColortypes(colorTypes);
                 }
             }
 
             bool containsTypes(const std::vector<const ColorType*>& types) const {
-                if (constituents.size() != types.size()) return false;
+                if (_constituents.size() != types.size()) return false;
 
-                for (size_t i = 0; i < constituents.size(); ++i) {
-                    if (!(*constituents[i] == *types[i])) {
+                for (size_t i = 0; i < _constituents.size(); ++i) {
+                    if (!(_constituents[i] == types[i])) {
                         return false;
                     }
                 }
@@ -326,72 +261,46 @@
                 return true;
             }
 
-            void printConstituents() override{
-                for(auto ct : constituents){
-                   ct->printConstituents();
-                }
-            }
-
-            const ColorType* getNestedColorType(size_t index) {
-                return constituents[index];
-            }
-
-            const Color* getColor(std::vector<uint32_t> ids){
-                assert(ids.size() == constituents.size());
-                std::vector<const Color *> colors;
-                for(uint32_t i = 0; i < ids.size(); i++){
-                    colors.push_back(&constituents[i]->operator[](i));
-                }
-                return getColor(colors);
-            }
-
-            const Color* getColor(const std::vector<const Color*>& colors);
-
-            const Color& operator[](size_t index) override;
-            const Color& operator[](int index) override {
-                return operator[]((size_t)index);
-            }
-            const Color& operator[](uint32_t index) override {
-                return operator[]((size_t)index);
-            }
-
-            const Color* operator[](const char* index) override;
-            const Color* operator[](const std::string& index) override;
+            const ColorType* getNestedColorType(size_t index) const {
+                return _constituents[index];
+            }
+
+            const Color* getColor(const std::vector<uint32_t> &ids) const override;
+
+            const Color* getColor(const std::vector<const Color*>& colors) const;
+
+            const Color& operator[](size_t index) const override;
+            const Color& operator[](int index) const override {
+                return operator[]((size_t)index);
+            }
+            const Color& operator[](uint32_t index) const override {
+                return operator[]((size_t)index);
+            }
+
+            const Color* operator[](const char* index) const override;
+            const Color* operator[](const std::string& index) const override;
         };
         
         struct Variable {
             std::string name;
-            ColorType* colorType;
+            const ColorType* colorType;
         };
 
         struct ColorFixpoint {
-            Colored::intervalTuple_t constraints;
+            Colored::interval_vector_t constraints;
             bool inQueue;
-
-            bool constainsColor(std::pair<const PetriEngine::Colored::Color *const, std::vector<uint32_t>> constPair) {
-                std::unordered_map<uint32_t, bool> contained;
-                for(auto interval : constraints._intervals) {
-                    for(uint32_t id : constPair.second){
-                        
-                        if(contained[id] != true){
-                            contained[id] = interval[id].contains(constPair.first->getId());
-                        }                        
-                    }
-                }
-
-                for(auto pair : contained){
-                    if (!pair.second){
-                        return false;
-                    }
-                }
-                return true;
-            }
         };
 
         struct ColorTypePartition {
             std::vector<const Color *> colors;
             std::string name;
         };
+
+        typedef std::unordered_map<uint32_t, const Colored::Variable *> PositionVariableMap;
+        //Map from variables to a vector of maps from variable positions to the modifiers applied to the variable in that position
+        typedef std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> VariableModifierMap;
+        typedef std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::interval_vector_t> VariableIntervalMap;
+        typedef std::unordered_map<uint32_t, std::vector<const Color*>> PositionColorsMap;
     }
 }
 

=== modified file 'include/PetriEngine/Colored/EquivalenceClass.h'
--- include/PetriEngine/Colored/EquivalenceClass.h	2021-04-14 10:41:18 +0000
+++ include/PetriEngine/Colored/EquivalenceClass.h	2021-07-07 08:15:00 +0000
@@ -1,5 +1,5 @@
-#ifndef PARTITION_H
-#define PARTITION_H
+#ifndef EQUIVALENCECLASS_H
+#define EQUIVALENCECLASS_H
 
 #include "Intervals.h"
 #include "Colors.h"
@@ -9,71 +9,43 @@
     namespace Colored {
         class EquivalenceClass {
             public:
-                EquivalenceClass();
-                EquivalenceClass(ColorType *colorType);
-                EquivalenceClass(ColorType *colorType, intervalTuple_t colorIntervals);
+                EquivalenceClass(uint32_t id);
+                EquivalenceClass(uint32_t id, const ColorType *colorType);
+                EquivalenceClass(uint32_t id, const ColorType *colorType, interval_vector_t&& colorIntervals);
                 ~EquivalenceClass() {}
-                std::string toString(){
-                    std::cout << "Id: " << _id << std::endl;
+                std::string toString() const{
                     return _colorIntervals.toString();
                 }
 
-                bool isEmpty(){
-                    if(_colorIntervals.size() < 1 || _colorIntervals.getFirst().size() < 1){
+                bool isEmpty() const{
+                    if(_colorIntervals.size() < 1 || _colorIntervals.front().size() < 1){
                         return true;
                     } 
                     return false;
                 }
 
-                bool containsColor(std::vector<uint32_t> ids);
-
-                size_t size();
-
-                EquivalenceClass intersect(EquivalenceClass other);
-
-                EquivalenceClass subtract(EquivalenceClass other, bool print);
-
-                static uint32_t idCounter;
+                bool containsColor(const std::vector<uint32_t> &ids, const std::vector<bool> &diagonalPositions) const;
+
+                size_t size() const;
+
+                EquivalenceClass intersect(uint32_t id, const EquivalenceClass &other) const;
+
+                EquivalenceClass subtract(uint32_t id, const EquivalenceClass &other, const std::vector<bool> &diagonalPositions) const;
+                
+                uint32_t id() const { return _id; }
+                const ColorType* type() const { return _colorType; }
+                const interval_vector_t& intervals() const { return _colorIntervals; }
+                void clear() { _colorIntervals.clear(); }
+                void setIntervalVector(const interval_vector_t& interval) { _colorIntervals = interval; }
+                void addInterval(interval_t&& interval) { _colorIntervals.addInterval(interval); }
+            private:
                 uint32_t _id;
-                ColorType *_colorType;
-                intervalTuple_t _colorIntervals;
-
-            private:
+                const ColorType *_colorType;
+                interval_vector_t _colorIntervals;
 
             
         };
-
-        struct EquivalenceVec{
-            std::vector<EquivalenceClass> _equivalenceClasses;
-            std::unordered_map<const Colored::Color *, EquivalenceClass *> colorEQClassMap;
-            bool diagonal = false;
-
-            void applyPartition(Colored::ArcIntervals& arcInterval){
-                if(diagonal){
-                    return;
-                }
-                std::vector<Colored::intervalTuple_t> newTupleVec;
-                for(auto intervalTuple : arcInterval._intervalTupleVec){
-                    intervalTuple.combineNeighbours();
-                    intervalTuple_t newIntervalTuple;
-                    for(auto interval : intervalTuple._intervals){
-                        for(auto EQClass : _equivalenceClasses){
-                            for(auto EQinterval : EQClass._colorIntervals._intervals){
-                                auto overlap = interval.getOverlap(EQinterval);
-                                if(overlap.isSound()){
-                                    newIntervalTuple.addInterval(EQinterval.getSingleColorInterval());
-                                    continue;
-                                }
-                            }
-                        }
-                    }
-                   newTupleVec.push_back(std::move(newIntervalTuple));
-                }
-                arcInterval._intervalTupleVec = std::move(newTupleVec);               
-            }
-        };
-
     }
 }
 
-#endif /* PARTITION_H */
\ No newline at end of file
+#endif /* EQUIVALENCECLASS_H */
\ No newline at end of file

=== added file 'include/PetriEngine/Colored/EquivalenceVec.h'
--- include/PetriEngine/Colored/EquivalenceVec.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/EquivalenceVec.h	2021-07-07 08:15:00 +0000
@@ -0,0 +1,69 @@
+#ifndef EQUIVALENCEVEC_H
+#define EQUIVALENCEVEC_H
+
+#include "Intervals.h"
+#include "Colors.h"
+#include "ArcIntervals.h"
+#include "EquivalenceClass.h"
+
+namespace PetriEngine {
+    namespace Colored {
+        class EquivalenceVec{
+            public:
+                void applyPartition(Colored::ArcIntervals& arcInterval) const;
+                void mergeEqClasses();
+                void applyPartition(std::vector<uint32_t> &colorIds) const;
+
+                bool isDiagonal() const{
+                    return _diagonal;
+                }
+
+                void setDiagonal(bool diagonal) {
+                    _diagonal = diagonal;
+                }
+
+                const std::vector<EquivalenceClass> & getEquivalenceClasses() const{
+                    return _equivalenceClasses;
+                }
+
+
+                const std::vector<bool> & getDiagonalTuplePositions() const{
+                    return _diagonalTuplePositions;
+                }
+
+                void push_back_Eqclass(const EquivalenceClass &Eqclass){
+                    _equivalenceClasses.push_back(Eqclass);
+                }
+
+                void erase_Eqclass(uint32_t position){
+                    _equivalenceClasses.erase(_equivalenceClasses.begin() + position);
+                }
+
+                void push_back_diagonalTuplePos(bool val){
+                    _diagonalTuplePositions.push_back(val);
+                }
+
+                void addColorToEqClassMap(const Color *color);
+
+                void setDiagonalTuplePosition(uint32_t position, bool value){
+                    _diagonalTuplePositions[position] = value;
+                }
+
+                void setDiagonalTuplePositions(const std::vector<bool> &diagonalPositions){
+                    _diagonalTuplePositions = diagonalPositions;
+                }
+
+                const std::unordered_map<const Colored::Color *, EquivalenceClass *> &getColorEqClassMap() const{
+                    return _colorEQClassMap;
+                }
+
+            private:
+                std::vector<EquivalenceClass> _equivalenceClasses;
+                std::unordered_map<const Colored::Color *, EquivalenceClass *> _colorEQClassMap;
+                std::vector<bool> _diagonalTuplePositions;
+                bool _diagonal = false;
+        };
+    }
+}
+
+#endif /* EQUIVALENCEVEC_H */
\ No newline at end of file

=== modified file 'include/PetriEngine/Colored/Expressions.h'
--- include/PetriEngine/Colored/Expressions.h	2021-04-22 12:43:03 +0000
+++ include/PetriEngine/Colored/Expressions.h	2021-07-07 08:15:00 +0000
@@ -27,11 +27,12 @@
 #include <iostream>
 #include <cassert>
 #include <memory>
+#include <typeinfo>
 
 
 #include "Colors.h"
 #include "Multiset.h"
-#include "EquivalenceClass.h"
+#include "EquivalenceVec.h"
 #include "ArcIntervals.h"
 #include "GuardRestrictor.h"
 #include "../errorcodes.h"
@@ -41,15 +42,13 @@
     
     namespace Colored {
         struct ExpressionContext {
-            typedef std::unordered_map<const Colored::Variable *, const PetriEngine::Colored::Color *> BindingMap;
+            
 
-            BindingMap& binding;
-            std::unordered_map<std::string, ColorType*>& colorTypes;
-            Colored::EquivalenceVec& placePartition;
+            const BindingMap& binding;
+            const ColorTypeMap& colorTypes;
+            const Colored::EquivalenceVec& placePartition;
             
             const Color* findColor(const std::string& color) const {
-                if (color.compare("dot") == 0)
-                    return DotConstant::dotConstant(nullptr);
                 for (auto& elem : colorTypes) {
                     auto col = (*elem.second)[color];
                     if (col)
@@ -59,9 +58,9 @@
                 exit(ErrorCode);
             }
 
-            ProductType* findProductColorType(const std::vector<const ColorType*>& types) const {
+            const ProductType* findProductColorType(const std::vector<const ColorType*>& types) const {
                 for (auto& elem : colorTypes) {
-                    auto* pt = dynamic_cast<ProductType*>(elem.second);
+                    auto* pt = dynamic_cast<const ProductType*>(elem.second);
 
                     if (pt && pt->containsTypes(types)) {
                         return pt;
@@ -70,6 +69,8 @@
                 return nullptr;
             }
         };
+        
+        
 
         class WeightException : public std::exception {
         private:
@@ -81,38 +82,46 @@
                 return ("Undefined weight: " + _message).c_str();
             }
         };
+
+        template<typename Base, typename T>
+        inline bool instanceof(const T*) {
+            return std::is_base_of<Base, T>::value;
+        }
         
         class Expression {
         public:
             Expression() {}
         
-            virtual void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const {}
-
-            virtual void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap) const {
-                uint32_t index = 0;
-                getVariables(variables, varPositions, varModifierMap, &index);
-            }
-
-            virtual void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions) const {
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap;
-                uint32_t index = 0;
-                getVariables(variables, varPositions, varModifierMap, &index);
+            virtual void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const {}
+
+            virtual void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts) const {
+                uint32_t index = 0;
+                getVariables(variables, varPositions, varModifierMap, includeSubtracts, index);
+            }
+
+            virtual void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions) const {
+                VariableModifierMap varModifierMap;
+                uint32_t index = 0;
+                getVariables(variables, varPositions, varModifierMap, false, index);
+            }
+
+            virtual void getVariables(std::set<const Colored::Variable*>& variables) const {
+                PositionVariableMap varPositions;
+                VariableModifierMap varModifierMap;
+                uint32_t index = 0;
+
+                getVariables(variables, varPositions, varModifierMap, false, index);
             }
 
             virtual bool isTuple() const {
                 return false;
             }
 
-            virtual void getVariables(std::set<const Colored::Variable*>& variables) const {
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositions;
-                std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap;
+            virtual bool isEligibleForSymmetry(std::vector<uint32_t>& numbers) const{
+                return false;
+            }
 
-                getVariables(variables, varPositions, varModifierMap);
-            }
             
-            virtual void expressionType() {
-                std::cout << "Expression" << std::endl;
-            }
 
             virtual std::string toString() const {
                 return "Unsupported";
@@ -124,40 +133,40 @@
             ColorExpression() {}
             virtual ~ColorExpression() {}
             
-            virtual const Color* eval(ExpressionContext& context) const = 0;
+            virtual const Color* eval(const ExpressionContext& context) const = 0;
 
             virtual void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const = 0;
 
-            virtual bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const = 0;
-
-            virtual ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const = 0;
-
-            virtual Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const {
-                return Colored::intervalTuple_t();
+            virtual bool getArcIntervals(Colored::ArcIntervals& arcIntervals, const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const = 0;
+
+            virtual const ColorType* getColorType(const ColorTypeMap& colorTypes) const = 0;
+
+            virtual Colored::interval_vector_t getOutputIntervals(const VariableIntervalMap& varMap, std::vector<const Colored::ColorType *> &colortypes) const {
+                return Colored::interval_vector_t();
             }
 
         };
         
         class DotConstantExpression : public ColorExpression {
         public:
-            const Color* eval(ExpressionContext& context) const override {
-                return DotConstant::dotConstant(nullptr);
+            const Color* eval(const ExpressionContext& context) const override {
+                return &(*ColorType::dotInstance()->begin());
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
                 if (arcIntervals._intervalTupleVec.empty()) {
                     //We can add all place tokens when considering the dot constant as, that must be present
                     arcIntervals._intervalTupleVec.push_back(cfp.constraints);
                 }
-                return !cfp.constraints._intervals.empty();
+                return !cfp.constraints.empty();
             }
 
-            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+            Colored::interval_vector_t getOutputIntervals(const VariableIntervalMap& varMap, std::vector<const Colored::ColorType *> &colortypes) const override {
                 Colored::interval_t interval;
-                Colored::intervalTuple_t tupleInterval;
-                const Color *dotColor = DotConstant::dotConstant(nullptr);
+                Colored::interval_vector_t tupleInterval;
+                const Color *dotColor = &(*ColorType::dotInstance()->begin());
                  
-                colortypes->push_back(dotColor->getColorType());
+                colortypes.emplace_back(dotColor->getColorType());
                 
                 interval.addRange(dotColor->getId(), dotColor->getId());
                 tupleInterval.addInterval(interval);
@@ -165,11 +174,12 @@
             }
 
             void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
-                const Color *dotColor = DotConstant::dotConstant(nullptr);
+                const Color *dotColor = &(*ColorType::dotInstance()->begin());
                 constantMap[index] = dotColor;
             }
-            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
-                return DotConstant::dotConstant(nullptr)->getColorType();
+            
+            const ColorType* getColorType(const ColorTypeMap& colorTypes) const override{
+                return ColorType::dotInstance();
             }
 
             std::string toString() const override {
@@ -181,16 +191,16 @@
         
         class VariableExpression : public ColorExpression {
         private:
-            Variable* _variable;
+            const Variable* _variable;
             
         public:
-            const Color* eval(ExpressionContext& context) const override {
-                return context.binding[_variable];
+            const Color* eval(const ExpressionContext& context) const override {
+                return context.binding.find(_variable)->second;
             }
             
-            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 getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
                 variables.insert(_variable);
-                varPositions[*index] = _variable;
+                varPositions[index] = _variable;
                 if(varModifierMap.count(_variable) == 0){
                     std::vector<std::unordered_map<uint32_t, int32_t>> newVec;
                     
@@ -202,44 +212,42 @@
                         break;
                     }
                     std::unordered_map<uint32_t, int32_t> newMap;
-                    newMap[*index] = 0;
+                    newMap[index] = 0;
                     newVec.push_back(newMap);
                     varModifierMap[_variable] = newVec;
                 } else {
-                    varModifierMap[_variable].back()[*index] = 0;
+                    varModifierMap[_variable].back()[index] = 0;
                 }                
             }
 
-            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
-                Colored::intervalTuple_t varInterval;
+            Colored::interval_vector_t getOutputIntervals(const VariableIntervalMap& varMap, std::vector<const Colored::ColorType *> &colortypes) const override {
+                Colored::interval_vector_t varInterval;
                 
                 // If we see a new variable on an out arc, it gets its full interval
                 if (varMap.count(_variable) == 0){
-                    Colored::intervalTuple_t intervalTuple;
-                    intervalTuple.addInterval(_variable->colorType->getFullInterval());
-                    varMap[_variable] = intervalTuple;
-                }
-
-                for(auto interval : varMap[_variable]._intervals){
-                    varInterval.addInterval(interval);
-                }
+                    varInterval.addInterval(_variable->colorType->getFullInterval());
+                } else {
+                    for(const auto& interval : varMap.find(_variable)->second){
+                        varInterval.addInterval(interval);
+                    }
+                }               
                                            
-                std::vector<ColorType*> varColorTypes;
+                std::vector<const ColorType*> varColorTypes;
                 _variable->colorType->getColortypes(varColorTypes);
 
-                for(auto ct : varColorTypes){
-                    colortypes->push_back(ct);
+                for(auto &ct : varColorTypes){
+                    colortypes.push_back(std::move(ct));
                 }
 
                 return varInterval;
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
                 if (arcIntervals._intervalTupleVec.empty()){
                     //As variables does not restrict the values before the guard we include all tokens
                     arcIntervals._intervalTupleVec.push_back(cfp.constraints);
                 }
-                return !cfp.constraints._intervals.empty();
+                return !cfp.constraints.empty();
             }
 
             void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
@@ -249,11 +257,11 @@
                 return _variable->name;
             }
 
-            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+            const ColorType* getColorType(const ColorTypeMap& colorTypes) const override{
                 return _variable->colorType;
             }
 
-            VariableExpression(Variable* variable)
+            VariableExpression(const Variable* variable)
                     : _variable(variable) {}
         };
         
@@ -262,11 +270,11 @@
             const Color* _userOperator;
             
         public:
-            const Color* eval(ExpressionContext& context) const override {
+            const Color* eval(const ExpressionContext& context) const override {
                 return _userOperator;
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
                 uint32_t colorId = _userOperator->getId() + modifier;
                 while(colorId < 0){
                     colorId += _userOperator->getColorType()->size();
@@ -274,10 +282,10 @@
                 colorId = colorId % _userOperator->getColorType()->size();
                 
                 if(arcIntervals._intervalTupleVec.empty()){
-                    Colored::intervalTuple_t newIntervalTuple;
+                    Colored::interval_vector_t newIntervalTuple;
                     bool colorInFixpoint = false;
-                    for (auto interval : cfp.constraints._intervals){
-                        if(interval[*index].contains(colorId)){
+                    for (const auto& interval : cfp.constraints){
+                        if(interval[index].contains(colorId)){
                             newIntervalTuple.addInterval(interval);
                             colorInFixpoint = true;
                         }
@@ -287,8 +295,8 @@
                 } else {
                     std::vector<uint32_t> intervalsToRemove;
                     for(auto& intervalTuple : arcIntervals._intervalTupleVec){
-                        for (uint32_t i = 0; i < intervalTuple._intervals.size(); i++){
-                            if(!intervalTuple[i][*index].contains(colorId)){
+                        for (uint32_t i = 0; i < intervalTuple.size(); i++){
+                            if(!intervalTuple[i][index].contains(colorId)){
                                 intervalsToRemove.push_back(i);
                             }
                         }
@@ -297,7 +305,7 @@
                             intervalTuple.removeInterval(*i);
                         }
                     }              
-                    return !arcIntervals._intervalTupleVec[0]._intervals.empty();
+                    return !arcIntervals._intervalTupleVec[0].empty();
                 }
             }
 
@@ -308,15 +316,16 @@
             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{
+            
+            const ColorType* getColorType(const ColorTypeMap& colorTypes) const override {
                 return _userOperator->getColorType();
             }
 
-            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+            Colored::interval_vector_t getOutputIntervals(const VariableIntervalMap& varMap, std::vector<const Colored::ColorType *> &colortypes) const override {
                 Colored::interval_t interval;
-                Colored::intervalTuple_t tupleInterval;
+                Colored::interval_vector_t tupleInterval;
                  
-                colortypes->push_back(_userOperator->getColorType());
+                colortypes.emplace_back(_userOperator->getColorType());
                 
                 interval.addRange(_userOperator->getId(), _userOperator->getId());
                 tupleInterval.addInterval(interval);
@@ -327,46 +336,12 @@
                     : _userOperator(userOperator) {}
         };
         
-        class UserSortExpression : public Expression {
-        private:
-            ColorType* _userSort;
-            
-        public:
-            ColorType* eval(ExpressionContext& context) const {
-                return _userSort;
-            }
-
-            std::string toString() const override {
-                return _userSort->getName();
-            }
-
-            UserSortExpression(ColorType* userSort)
-                    : _userSort(userSort) {}
-        };
-
-        typedef std::shared_ptr<UserSortExpression> UserSortExpression_ptr;
-        
-        class NumberConstantExpression : public Expression {
-        private:
-            uint32_t _number;
-            
-        public:
-            uint32_t eval(ExpressionContext& context) const {
-                return _number;
-            }
-            
-            NumberConstantExpression(uint32_t number)
-                    : _number(number) {}
-        };
-
-        typedef std::shared_ptr<NumberConstantExpression> NumberConstantExpression_ptr;
-        
         class SuccessorExpression : public ColorExpression {
         private:
             ColorExpression_ptr _color;
             
         public:
-            const Color* eval(ExpressionContext& context) const override {
+            const Color* eval(const ExpressionContext& context) const override {
                 return &++(*_color->eval(context));
             }
 
@@ -374,30 +349,30 @@
                 return _color->isTuple();
             }
             
-            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 getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
                 //save index before evaluating nested expression to decrease all the correct modifiers
-                uint32_t indexBefore = *index;
-                _color->getVariables(variables, varPositions, varModifierMap, index);
+                uint32_t indexBefore = index;
+                _color->getVariables(variables, varPositions, varModifierMap, includeSubtracts, index);
                 for(auto& varModifierPair : varModifierMap){
                     for(auto& idModPair : varModifierPair.second.back()){
-                        if(idModPair.first <= *index && idModPair.first >= indexBefore){
+                        if(idModPair.first <= index && idModPair.first >= indexBefore){
                             idModPair.second--;
                         } 
                     }                   
                 }                
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
                return _color->getArcIntervals(arcIntervals, cfp, index, modifier+1);
             }
 
-            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+            Colored::interval_vector_t getOutputIntervals(const VariableIntervalMap& varMap, std::vector<const Colored::ColorType *> &colortypes) const override {
                 //store the number of colortyps already in colortypes vector and use that as offset when indexing it
-                auto colortypesBefore = colortypes->size();
+                auto colortypesBefore = colortypes.size();
 
                 auto nestedInterval = _color->getOutputIntervals(varMap, colortypes);
                 Colored::GuardRestrictor guardRestrictor = Colored::GuardRestrictor();
-                return guardRestrictor.shiftIntervals(varMap, colortypes, &nestedInterval, 1, colortypesBefore);
+                return guardRestrictor.shiftIntervals(varMap, colortypes, nestedInterval, 1, colortypesBefore);
             }
 
             void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
@@ -411,7 +386,7 @@
                 return _color->toString() + "++";
             }
 
-            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+            const ColorType* getColorType(const ColorTypeMap& colorTypes) const override{
                 return _color->getColorType(colorTypes);
             }
 
@@ -424,7 +399,7 @@
             ColorExpression_ptr _color;
             
         public:
-            const Color* eval(ExpressionContext& context) const override {
+            const Color* eval(const ExpressionContext& context) const override {
                 return &--(*_color->eval(context));
             }
 
@@ -432,30 +407,30 @@
                 return _color->isTuple();
             }
             
-            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 getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
                 //save index before evaluating nested expression to decrease all the correct modifiers
-                uint32_t indexBefore = *index;
-                _color->getVariables(variables, varPositions, varModifierMap, index);
+                uint32_t indexBefore = index;
+                _color->getVariables(variables, varPositions, varModifierMap, includeSubtracts, index);
                 for(auto& varModifierPair : varModifierMap){
                     for(auto& idModPair : varModifierPair.second.back()){
-                        if(idModPair.first <= *index && idModPair.first >= indexBefore){
+                        if(idModPair.first <= index && idModPair.first >= indexBefore){
                             idModPair.second++;
                         } 
                     }                   
                 } 
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
                 return _color->getArcIntervals(arcIntervals, cfp, index, modifier-1);
             }
             
-            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+            Colored::interval_vector_t getOutputIntervals(const VariableIntervalMap& varMap, std::vector<const Colored::ColorType *> &colortypes) const override {
                 //store the number of colortyps already in colortypes vector and use that as offset when indexing it
-                auto colortypesBefore = colortypes->size();
+                auto colortypesBefore = colortypes.size();
 
                 auto nestedInterval = _color->getOutputIntervals(varMap, colortypes);
                 Colored::GuardRestrictor guardRestrictor;
-                return guardRestrictor.shiftIntervals(varMap, colortypes, &nestedInterval, -1, colortypesBefore);
+                return guardRestrictor.shiftIntervals(varMap, colortypes, nestedInterval, -1, colortypesBefore);
             }
 
             void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
@@ -469,7 +444,7 @@
                 return _color->toString() + "--";
             }
 
-            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+            const ColorType* getColorType(const ColorTypeMap& colorTypes) const override{
                 return _color->getColorType(colorTypes);
             }
 
@@ -480,17 +455,17 @@
         class TupleExpression : public ColorExpression {
         private:
             std::vector<ColorExpression_ptr> _colors;
-            ColorType* _colorType;
+            const ColorType* _colorType = nullptr;
             
         public:
-            const Color* eval(ExpressionContext& context) const override {
+            const Color* eval(const ExpressionContext& context) const override {
                 std::vector<const Color*> colors;
                 std::vector<const ColorType*> types;
-                for (auto color : _colors) {
+                for (const auto& color : _colors) {
                     colors.push_back(color->eval(context));
                     types.push_back(colors.back()->getColorType());
                 }
-                ProductType* pt = context.findProductColorType(types);
+                const ProductType* pt = context.findProductColorType(types);
                 assert(pt != nullptr);
                 const Color* col = pt->getColor(colors);
                 assert(col != nullptr);
@@ -501,26 +476,25 @@
                 return true;
             }
 
-            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
-                Colored::intervalTuple_t intervals;
-                Colored::intervalTuple_t intervalHolder;                
+            Colored::interval_vector_t getOutputIntervals(const VariableIntervalMap& varMap, std::vector<const Colored::ColorType *> &colortypes) const override {
+                Colored::interval_vector_t intervals;
 
-                for(auto colorExp : _colors) {
-                    Colored::intervalTuple_t intervalHolder;
+                for(const auto& colorExp : _colors) {
+                    Colored::interval_vector_t intervalHolder;
                     auto nested_intervals = colorExp->getOutputIntervals(varMap, colortypes);
 
-                    if(intervals._intervals.empty()){
+                    if(intervals.empty()){
                         intervals = nested_intervals;
                     } else {                        
-                        for(auto nested_interval : nested_intervals._intervals){
-                            Colored::intervalTuple_t newIntervals;
-                            for(auto interval : intervals._intervals){
-                                for(auto nestedRange : nested_interval._ranges) {
+                        for(const auto& nested_interval : nested_intervals){
+                            Colored::interval_vector_t newIntervals;
+                            for(auto interval : intervals){
+                                for(const auto& nestedRange : nested_interval._ranges) {
                                     interval.addRange(nestedRange);    
                                 }
                                 newIntervals.addInterval(interval);
                             }
-                            for(auto newInterval : newIntervals._intervals){
+                            for(const auto& newInterval : newIntervals){
                                 intervalHolder.addInterval(newInterval);
                             }
                         }
@@ -530,37 +504,37 @@
                 return intervals;
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
-                for (auto expr : _colors) {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
+                for (const auto& expr : _colors) {
                     bool res = expr->getArcIntervals(arcIntervals, cfp, index, modifier);
                     if(!res){
                         return false;
                     }
-                    (*index)++;
+                    ++index;
                 }
                 return true;
             }
             
-            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) {
-                    elem->getVariables(variables, varPositions, varModifierMap, index);
-                    (*index)++;
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                for (const auto& elem : _colors) {
+                    elem->getVariables(variables, varPositions, varModifierMap, includeSubtracts, index);
+                    ++index;
                 }
             }
 
-            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+            const ColorType* getColorType(const ColorTypeMap& colorTypes) const override{
                 
                 std::vector<const ColorType*> types;
                 if(_colorType != nullptr){
                     return _colorType;
                 }
 
-                for (auto color : _colors) {
+                for (const auto& color : _colors) {
                     types.push_back(color->getColorType(colorTypes));
                 }
                 
                 for (auto elem : colorTypes) {
-                    auto* pt = dynamic_cast<ProductType*>(elem.second);
+                    auto* pt = dynamic_cast<const ProductType*>(elem.second);
                     if (pt && pt->containsTypes(types)) {
                         return pt;
                     }
@@ -571,7 +545,7 @@
             }
 
             void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
-                for (auto elem : _colors) {
+                for (const auto& elem : _colors) {
                     elem->getConstants(constantMap, index);
                     index++;
                 }
@@ -586,7 +560,7 @@
                 return res;
             }
 
-            void setColorType(ColorType* ct){
+            void setColorType(const ColorType* ct){
                 _colorType = ct;
             }
 
@@ -599,11 +573,11 @@
             GuardExpression() {}
             virtual ~GuardExpression() {}
             
-            virtual bool eval(ExpressionContext& context) const = 0;
-
-            virtual void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const = 0;
-
-            virtual void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const {
+            virtual bool eval(const ExpressionContext& context) const = 0;
+
+            virtual void restrictVars(std::vector<VariableIntervalMap>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const = 0;
+
+            virtual void restrictVars(std::vector<VariableIntervalMap>& variableMap) const {
                 std::set<const Colored::Variable*> diagonalVars;
                 restrictVars(variableMap, diagonalVars);
             }
@@ -617,31 +591,31 @@
             ColorExpression_ptr _right;
             
         public:
-            bool eval(ExpressionContext& context) const override {
+            bool eval(const ExpressionContext& context) const override {
                 return _left->eval(context) < _right->eval(context);
             }
 
-            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);
-                _right->getVariables(variables, varPositions, varModifierMap);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
+                _right->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
             }
 
             bool isTuple() const override {
                 return _left->isTuple() || _right->isTuple();
             }
 
-            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+            void restrictVars(std::vector<VariableIntervalMap>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
+                VariableModifierMap varModifierMapL;
+                VariableModifierMap varModifierMapR;
+                PositionVariableMap varPositionsL;
+                PositionVariableMap varPositionsR;
                 std::unordered_map<uint32_t, const Color*> constantMapL;
                 std::unordered_map<uint32_t, const Color*> constantMapR;
                 std::set<const Variable *> leftVars;
                 std::set<const Variable *> rightVars;
                 uint32_t index = 0;
-                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
-                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL, false);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR, false);
                 _left->getConstants(constantMapL, index);
                 index = 0;
                 _right->getConstants(constantMapR, index);
@@ -650,7 +624,7 @@
                     return;
                 }
                 Colored::GuardRestrictor guardRestrictor;
-                guardRestrictor.restrictVars(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars, true, true);
+                guardRestrictor.restrictVars(variableMap, varModifierMapL, varModifierMapR, varPositionsL, varPositionsR, constantMapL, constantMapR, diagonalVars, true, true);
             }
             
             std::string toString() const override {
@@ -669,7 +643,7 @@
             ColorExpression_ptr _right;
             
         public:
-            bool eval(ExpressionContext& context) const override {
+            bool eval(const ExpressionContext& context) const override {
                 return _left->eval(context) > _right->eval(context);
             }
 
@@ -677,23 +651,23 @@
                 return _left->isTuple() || _right->isTuple();
             }
             
-            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);
-                _right->getVariables(variables, varPositions, varModifierMap);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
+                _right->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
             }
 
-            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+            void restrictVars(std::vector<VariableIntervalMap>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
+                VariableModifierMap varModifierMapL;
+                VariableModifierMap varModifierMapR;
+                PositionVariableMap varPositionsL;
+                PositionVariableMap varPositionsR;
                 std::unordered_map<uint32_t, const Color*> constantMapL;
                 std::unordered_map<uint32_t, const Color*> constantMapR;
                 std::set<const Colored::Variable *> leftVars;
                 std::set<const Colored::Variable *> rightVars;
                 uint32_t index = 0;
-                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
-                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL, false);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR, false);
                 _left->getConstants(constantMapL, index);
                 index = 0;
                 _right->getConstants(constantMapR, index);
@@ -703,7 +677,7 @@
                 }
 
                 Colored::GuardRestrictor guardRestrictor;
-                guardRestrictor.restrictVars(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars, false, true);
+                guardRestrictor.restrictVars(variableMap, varModifierMapL, varModifierMapR, varPositionsL, varPositionsR, constantMapL, constantMapR, diagonalVars, false, true);
             }
 
             std::string toString() const override {
@@ -721,7 +695,7 @@
             ColorExpression_ptr _right;
             
         public:
-            bool eval(ExpressionContext& context) const override {
+            bool eval(const ExpressionContext& context) const override {
                 return _left->eval(context) <= _right->eval(context);
             }
 
@@ -729,23 +703,23 @@
                 return _left->isTuple() || _right->isTuple();
             }
             
-            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);
-                _right->getVariables(variables, varPositions, varModifierMap);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
+                _right->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
             }
 
-            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+            void restrictVars(std::vector<VariableIntervalMap>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
+                VariableModifierMap varModifierMapL;
+                VariableModifierMap varModifierMapR;
+                PositionVariableMap varPositionsL;
+                PositionVariableMap varPositionsR;
                 std::unordered_map<uint32_t, const Color*> constantMapL;
                 std::unordered_map<uint32_t, const Color*> constantMapR;
                 std::set<const Colored::Variable *> leftVars;
                 std::set<const Colored::Variable *> rightVars;
                 uint32_t index = 0;
-                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
-                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL, false);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR, false);
                 _left->getConstants(constantMapL, index);
                 index = 0;
                 _right->getConstants(constantMapR, index);
@@ -755,7 +729,7 @@
                 }
 
                 Colored::GuardRestrictor guardRestrictor;
-                guardRestrictor.restrictVars(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars, true, false); 
+                guardRestrictor.restrictVars(variableMap, varModifierMapL, varModifierMapR, varPositionsL, varPositionsR, constantMapL, constantMapR, diagonalVars, true, false); 
             }
 
             std::string toString() const override {
@@ -774,7 +748,7 @@
             ColorExpression_ptr _right;
             
         public:
-            bool eval(ExpressionContext& context) const override {
+            bool eval(const ExpressionContext& context) const override {
                 return _left->eval(context) >= _right->eval(context);
             }
 
@@ -782,23 +756,23 @@
                 return _left->isTuple() || _right->isTuple();
             }
             
-            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);
-                _right->getVariables(variables, varPositions, varModifierMap);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
+                _right->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
             }
 
-            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+            void restrictVars(std::vector<VariableIntervalMap>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
+                VariableModifierMap varModifierMapL;
+                VariableModifierMap varModifierMapR;
+                PositionVariableMap varPositionsL;
+                PositionVariableMap varPositionsR;
                 std::unordered_map<uint32_t, const Color*> constantMapL;
                 std::unordered_map<uint32_t, const Color*> constantMapR;
                 std::set<const Colored::Variable *> leftVars;
                 std::set<const Colored::Variable *> rightVars;
                 uint32_t index = 0;
-                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
-                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL, false);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR, false);
                 _left->getConstants(constantMapL, index);
                 index = 0;
                 _right->getConstants(constantMapR, index);
@@ -808,7 +782,7 @@
                 }
 
                 Colored::GuardRestrictor guardRestrictor;
-                guardRestrictor.restrictVars(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars, false, false);                
+                guardRestrictor.restrictVars(variableMap, varModifierMapL, varModifierMapR, varPositionsL, varPositionsR, constantMapL, constantMapR, diagonalVars, false, false);                
             }
             
             std::string toString() const override {
@@ -826,7 +800,7 @@
             ColorExpression_ptr _right;
             
         public:
-            bool eval(ExpressionContext& context) const override {
+            bool eval(const ExpressionContext& context) const override {
                 return _left->eval(context) == _right->eval(context);
             }
             
@@ -834,24 +808,24 @@
                 return _left->isTuple() || _right->isTuple();
             }
 
-            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);
-                _right->getVariables(variables, varPositions, varModifierMap);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
+                _right->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
             }
             
 
-            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
-                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
-                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+            void restrictVars(std::vector<VariableIntervalMap>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
+                VariableModifierMap varModifierMapL;
+                VariableModifierMap varModifierMapR;
+                PositionVariableMap varPositionsL;
+                PositionVariableMap varPositionsR;
                 std::unordered_map<uint32_t, const Color*> constantMapL;
                 std::unordered_map<uint32_t, const Color*> constantMapR;
                 std::set<const Colored::Variable *> leftVars;
                 std::set<const Colored::Variable *> rightVars;
                 uint32_t index = 0;
-                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
-                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL, false);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR, false);
                 _left->getConstants(constantMapL, index);
                 index = 0;
                 _right->getConstants(constantMapR, index);
@@ -861,7 +835,7 @@
                 }
                 
                 Colored::GuardRestrictor guardRestrictor;
-                guardRestrictor.restrictEquality(variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, diagonalVars);
+                guardRestrictor.restrictEquality(variableMap, varModifierMapL, varModifierMapR, varPositionsL, varPositionsR, constantMapL, constantMapR, diagonalVars);
             }
 
             std::string toString() const override {
@@ -879,7 +853,7 @@
             ColorExpression_ptr _right;
             
         public:
-            bool eval(ExpressionContext& context) const override {
+            bool eval(const ExpressionContext& context) const override {
                 return _left->eval(context) != _right->eval(context);
             }
 
@@ -887,13 +861,32 @@
                 return _left->isTuple() || _right->isTuple();
             }
             
-            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);
-                _right->getVariables(variables, varPositions, varModifierMap);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
+                _right->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
             }
 
-            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
-                
+            void restrictVars(std::vector<VariableIntervalMap>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
+                VariableModifierMap varModifierMapL;
+                VariableModifierMap varModifierMapR;
+                PositionVariableMap varPositionsL;
+                PositionVariableMap varPositionsR;
+                std::unordered_map<uint32_t, const Color*> constantMapL;
+                std::unordered_map<uint32_t, const Color*> constantMapR;
+                std::set<const Colored::Variable *> leftVars;
+                std::set<const Colored::Variable *> rightVars;
+                uint32_t index = 0;
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL, false);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR, false);
+                _left->getConstants(constantMapL, index);
+                index = 0;
+                _right->getConstants(constantMapR, index);
+
+                if(leftVars.empty() && rightVars.empty()){
+                    return;
+                }
+                Colored::GuardRestrictor guardRestrictor;
+                guardRestrictor.restrictInEquality(variableMap, varModifierMapL, varModifierMapR, varPositionsL, varPositionsR, constantMapL, constantMapR, diagonalVars);
             }
 
             std::string toString() const override {
@@ -905,53 +898,13 @@
                     : _left(std::move(left)), _right(std::move(right)) {}
         };
         
-        class NotExpression : public GuardExpression {
-        private:
-            GuardExpression_ptr _expr;
-            
-        public:
-            bool eval(ExpressionContext& context) const override {
-                return !_expr->eval(context);
-            }
-
-            bool isTuple() const override {
-                return _expr->isTuple();
-            }
-            
-            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, index);
-            }
-
-            std::string toString() const override {
-                std::string res = "!" + _expr->toString();
-                return res;
-            }
-
-            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
-                std::set<const Colored::Variable *> variables;
-                _expr->getVariables(variables);
-                //TODO: invert the var intervals here instead of using the full intervals
-
-                for(auto var : variables){
-                    auto fullInterval = var->colorType->getFullInterval();
-                    Colored::intervalTuple_t fullTuple;
-                    fullTuple.addInterval(fullInterval);
-                    for(auto& varMap : variableMap){
-                        varMap[var] = fullTuple;
-                    }                    
-                }
-            }
-            
-            NotExpression(GuardExpression_ptr&& expr) : _expr(std::move(expr)) {}
-        };
-        
         class AndExpression : public GuardExpression {
         private:
             GuardExpression_ptr _left;
             GuardExpression_ptr _right;
             
         public:
-            bool eval(ExpressionContext& context) const override {
+            bool eval(const ExpressionContext& context) const override {
                 return _left->eval(context) && _right->eval(context);
             }
 
@@ -959,12 +912,12 @@
                 return _left->isTuple() || _right->isTuple();
             }
             
-            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);
-                _right->getVariables(variables, varPositions, varModifierMap);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
+                _right->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
             }
 
-            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
+            void restrictVars(std::vector<VariableIntervalMap>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override {
                 _left->restrictVars(variableMap, diagonalVars);
                 _right->restrictVars(variableMap, diagonalVars);
             }
@@ -984,7 +937,7 @@
             GuardExpression_ptr _right;
             
         public:
-            bool eval(ExpressionContext& context) const override {
+            bool eval(const ExpressionContext& context) const override {
                 return _left->eval(context) || _right->eval(context);
             }
 
@@ -992,23 +945,17 @@
                 return _left->isTuple() || _right->isTuple();
             }
             
-            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);
-                _right->getVariables(variables, varPositions, varModifierMap);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
+                _right->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
             }
 
-            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override{
+            void restrictVars(std::vector<VariableIntervalMap>& variableMap, std::set<const Colored::Variable*> &diagonalVars) const override{
                 auto varMapCopy = variableMap;
                 _left->restrictVars(variableMap, diagonalVars);
                 _right->restrictVars(varMapCopy, diagonalVars);
 
-                for(size_t i = 0; i < variableMap.size(); i++){
-                    for(auto& varPair : varMapCopy[i]){
-                        for(auto& interval : varPair.second._intervals){
-                            variableMap[i][varPair.first].addInterval(std::move(interval));
-                        }
-                    }
-                }
+                variableMap.insert(variableMap.end(), varMapCopy.begin(), varMapCopy.end());
             }
 
             std::string toString() const override {
@@ -1025,25 +972,22 @@
             ArcExpression() {}
             virtual ~ArcExpression() {}
             
-            virtual Multiset eval(ExpressionContext& context) const = 0;
-
-            virtual void expressionType() override {
-                std::cout << "ArcExpression" << std::endl;
-            }
-            virtual void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const = 0;
-
-            virtual bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const = 0;
+            virtual Multiset eval(const ExpressionContext& context) const = 0;
+
+            virtual void getConstants(PositionColorsMap &constantMap, uint32_t &index) const = 0;
+
+            virtual bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const = 0;
 
             virtual uint32_t weight() const = 0;
 
-            virtual Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec) const {
+            virtual std::vector<Colored::interval_vector_t> getOutputIntervals(const std::vector<VariableIntervalMap>& varMapVec) const {
                 std::vector<const Colored::ColorType *> colortypes;
                 
-                return getOutputIntervals(varMapVec, &colortypes);
+                return getOutputIntervals(varMapVec, colortypes);
             }
 
-            virtual Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const {
-                return Colored::intervalTuple_t();
+            virtual std::vector<Colored::interval_vector_t> getOutputIntervals(const std::vector<VariableIntervalMap>& varMapVec, std::vector<const Colored::ColorType *> &colortypes) const{
+                return std::vector<Colored::interval_vector_t>(0);
             }
         };
 
@@ -1051,20 +995,20 @@
         
         class AllExpression : public Expression {
         private:
-            ColorType* _sort;
+            const ColorType* _sort;
             
         public:
             virtual ~AllExpression() {};
-            std::vector<std::pair<const Color*,uint32_t>> eval(ExpressionContext& context) const {
+            std::vector<std::pair<const Color*,uint32_t>> eval(const ExpressionContext& context) const {
                 std::vector<std::pair<const Color*,uint32_t>> colors;
                 assert(_sort != nullptr);
-                if(context.placePartition.diagonal || context.placePartition._equivalenceClasses.empty()){
+                if(context.placePartition.isDiagonal() || context.placePartition.getEquivalenceClasses().empty()){
                     for (size_t i = 0; i < _sort->size(); i++) {
                         colors.push_back(std::make_pair(&(*_sort)[i], 1));
                     }
                 } else {
-                    for (auto EqClass : context.placePartition._equivalenceClasses){
-                        colors.push_back(std::make_pair(_sort->getColor(EqClass._colorIntervals.getLowerIds()),EqClass.size()));
+                    for (const auto& eq_class : context.placePartition.getEquivalenceClasses()){
+                        colors.push_back(std::make_pair(_sort->getColor(eq_class.intervals().getLowerIds()),eq_class.size()));
                     }
                 }
                 
@@ -1075,34 +1019,33 @@
                 return _sort->productSize() > 1;
             }
 
-            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const {
+            void getConstants(PositionColorsMap &constantMap, uint32_t &index) const {
                 for (size_t i = 0; i < _sort->size(); i++) {
                     constantMap[index].push_back(&(*_sort)[i]);
                 }
             }
 
-            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const {
-                Colored::intervalTuple_t newIntervalTuple;
+            Colored::interval_vector_t getOutputIntervals(const std::vector<VariableIntervalMap>& varMapVec, std::vector<const Colored::ColorType *> &colortypes) const {
+                Colored::interval_vector_t newIntervalTuple;
                 newIntervalTuple.addInterval(_sort->getFullInterval());
                 return newIntervalTuple;
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const {
                 
                 if(arcIntervals._intervalTupleVec.empty()){
                     bool colorsInFixpoint = false;
-                    Colored::intervalTuple_t newIntervalTuple;
-                    cfp.constraints.simplify();
+                    Colored::interval_vector_t newIntervalTuple;
                     if(cfp.constraints.getContainedColors() == _sort->size()){
                         colorsInFixpoint = true;
-                        for(auto interval : cfp.constraints._intervals){                            
+                        for(const auto& interval : cfp.constraints){                            
                             newIntervalTuple.addInterval(interval);
                         }
                     }                    
                     arcIntervals._intervalTupleVec.push_back(newIntervalTuple);
                     return colorsInFixpoint;
                 } else {
-                    std::vector<Colored::intervalTuple_t> newIntervalTupleVec;
+                    std::vector<Colored::interval_vector_t> newIntervalTupleVec;
                     for(uint32_t i = 0; i < arcIntervals._intervalTupleVec.size(); i++){
                         auto& intervalTuple = arcIntervals._intervalTupleVec[i];
                         if(intervalTuple.getContainedColors() == _sort->size()){
@@ -1122,7 +1065,7 @@
                 return _sort->getName() + ".all";
             }
 
-            AllExpression(ColorType* sort) : _sort(sort) 
+            AllExpression(const ColorType* sort) : _sort(sort) 
             {
                 assert(sort != nullptr);
             }
@@ -1137,10 +1080,10 @@
             AllExpression_ptr _all;
             
         public:
-            Multiset eval(ExpressionContext& context) const override {
+            Multiset eval(const ExpressionContext& context) const override {
                 std::vector<std::pair<const Color*,uint32_t>> col;
                 if (!_color.empty()) {
-                    for (auto elem : _color) {
+                    for (const auto& elem : _color) {
                         col.push_back(std::make_pair(elem->eval(context), _number));
                     }
                 } else if (_all != nullptr) {
@@ -1152,9 +1095,18 @@
                 
                 return Multiset(col);
             }
+            bool isEligibleForSymmetry(std::vector<uint32_t>& numbers) const override{
+                //Not entirely sure what to do if there is more than one colorExpression, but should probably return false
+                if(_color.size() > 1){
+                    return false;
+                }
+                numbers.emplace_back(_number);
+                //Maybe we need to check color expression also
+                return true;
+            }
 
             bool isTuple() const override {
-                for(auto colorExpr : _color){
+                for(const auto& colorExpr : _color){
                     if(colorExpr->isTuple()){
                         return true;
                     }
@@ -1162,59 +1114,48 @@
                 return false;
             }
 
-            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 getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
                 if (_all != nullptr)
                     return;
-                for (auto elem : _color) {
+                for (const auto& elem : _color) {
                     //TODO: can there be more than one element in a number of expression?
-                    elem->getVariables(variables, varPositions, varModifierMap, index);
+                    elem->getVariables(variables, varPositions, varModifierMap, includeSubtracts, index);
                 }
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
                 if (_all != nullptr) {
                     return _all->getArcIntervals(arcIntervals, cfp, index, modifier);
                 }
-                //uint32_t i = 0;
-                for (auto elem : _color) {
-                    //(*index) += i;
+                for (const auto& elem : _color) {
                     if(!elem->getArcIntervals(arcIntervals, cfp, index, modifier)){
                         return false;
                     }
-                    //i++;
                 }
                 return true;
             }
 
-            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override {
-                Colored::intervalTuple_t intervals;
+            std::vector<Colored::interval_vector_t> getOutputIntervals(const std::vector<VariableIntervalMap>& varMapVec, std::vector<const Colored::ColorType *> &colortypes) const override {
+                std::vector<Colored::interval_vector_t> intervalsVec;
                 if (_all == nullptr) {
-                    for (auto elem : _color) {
-                        for(auto& varMap : varMapVec){
-                            auto nestedIntervals = elem->getOutputIntervals(varMap, colortypes);
-
-                            if (intervals._intervals.empty()) {
-                                intervals = nestedIntervals;
-                            } else {
-                                for(auto interval : nestedIntervals._intervals) {
-                                    intervals.addInterval(interval);
-                                }
-                            }
+                    for (const auto& elem : _color) {
+                        for(const auto& varMap : varMapVec){
+                            intervalsVec.push_back(elem->getOutputIntervals(varMap, colortypes));
                         }                        
                     }
                 } else {
-                    return _all->getOutputIntervals(varMapVec, colortypes);
+                    intervalsVec.push_back(_all->getOutputIntervals(varMapVec, colortypes));
                 }
-                return intervals;
+                return intervalsVec;
             }
 
-            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+            void getConstants(PositionColorsMap &constantMap, uint32_t &index) const override {
                 if (_all != nullptr)
                     _all->getConstants(constantMap, index);
-                else for (auto elem : _color) {
+                else for (const auto& elem : _color) {
                     std::unordered_map<uint32_t, const Color*> elemMap;
                     elem->getConstants(elemMap, index);
-                    for(auto pair : elemMap){
+                    for(const auto& pair : elemMap){
                         constantMap[pair.first].push_back(pair.second);
                     }
                 }
@@ -1263,26 +1204,47 @@
             std::vector<ArcExpression_ptr> _constituents;
             
         public:
-            Multiset eval(ExpressionContext& context) const override {
+            Multiset eval(const ExpressionContext& context) const override {
                 Multiset ms;
-                for (auto expr : _constituents) {
+                for (const auto& expr : _constituents) {
                     ms += expr->eval(context);
                 }
                 return ms;
             }
+
+            bool isEligibleForSymmetry(std::vector<uint32_t>& numbers) const override{
+                for(const auto& elem : _constituents){
+                    if(!elem->isEligibleForSymmetry(numbers)){
+                        return false;
+                    }
+                }
+                
+                if(numbers.size() < 2){
+                    return false;
+                }
+                //pick a number
+                //every number has to be equal
+                uint32_t firstNumber = numbers[0];
+                for(uint32_t number : numbers){
+                    if(firstNumber != number){
+                        return false;
+                    }
+                }
+                return true;
+            }
             
-            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) {
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                for (const auto& elem : _constituents) {
                     for(auto& pair : varModifierMap){
                         std::unordered_map<uint32_t, int32_t> newMap;
                         pair.second.push_back(newMap);
                     }
-                    elem->getVariables(variables, varPositions, varModifierMap);
+                    elem->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
                 }
             }
 
             bool isTuple() const override {
-                for(auto arcExpr : _constituents){
+                for(const auto& arcExpr : _constituents){
                     if(arcExpr->isTuple()){
                         return true;
                     }
@@ -1290,13 +1252,13 @@
                 return false;
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
-                for (auto elem : _constituents) {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
+                for (const auto& elem : _constituents) {
                     uint32_t newIndex = 0;
                     Colored::ArcIntervals newArcIntervals;
                     std::vector<uint32_t> intervalsForRemoval;
                     std::vector<Colored::interval_t> newIntervals;
-                    if(!elem->getArcIntervals(newArcIntervals, cfp, &newIndex, modifier)){
+                    if(!elem->getArcIntervals(newArcIntervals, cfp, newIndex, modifier)){
                         return false;
                     }
 
@@ -1309,26 +1271,20 @@
                 return true;
             }            
 
-            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override {
-                Colored::intervalTuple_t intervals;
+            std::vector<Colored::interval_vector_t> getOutputIntervals(const std::vector<VariableIntervalMap>& varMapVec, std::vector<const Colored::ColorType *> &colortypes) const override {
+                std::vector<Colored::interval_vector_t> intervalsVec;
                 
-                for (auto elem : _constituents) {
+                for (const auto& elem : _constituents) {
                     auto nestedIntervals = elem->getOutputIntervals(varMapVec, colortypes);
 
-                    if (intervals._intervals.empty()) {
-                        intervals = nestedIntervals;
-                    } else {
-                        for(auto interval : nestedIntervals._intervals) {
-                            intervals.addInterval(interval);
-                        }
-                    }
+                    intervalsVec.insert(intervalsVec.end(), nestedIntervals.begin(), nestedIntervals.end());
                 }
-                return intervals;
+                return intervalsVec;
             }
 
-            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+            void getConstants(PositionColorsMap &constantMap, uint32_t &index) const override {
                 uint32_t indexCopy = index;
-                for (auto elem : _constituents) {
+                for (const auto& elem : _constituents) {
                     uint32_t localIndex = indexCopy;
                     elem->getConstants(constantMap, localIndex);
                 }
@@ -1336,7 +1292,7 @@
 
             uint32_t weight() const override {
                 uint32_t res = 0;
-                for (auto expr : _constituents) {
+                for (const auto& expr : _constituents) {
                     res += expr->weight();
                 }
                 return res;
@@ -1360,34 +1316,34 @@
             ArcExpression_ptr _right;
             
         public:
-            Multiset eval(ExpressionContext& context) const override {
+            Multiset eval(const ExpressionContext& context) const override {
                 return _left->eval(context) - _right->eval(context);
             }
             
-            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);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
                 //We ignore the restrictions imposed by the subtraction for now
-                //_right->getVariables(variables, varPositions, varModifierMap);
+                if(includeSubtracts){
+                    _right->getVariables(variables, varPositions, varModifierMap, includeSubtracts);
+                }
             }
 
             bool isTuple() const override {
                 return _left->isTuple() || _right->isTuple();
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
                 return _left->getArcIntervals(arcIntervals, cfp, index, modifier);
                 //We ignore the restrictions imposed by the subtraction for now
                 //_right->getArcIntervals(arcIntervals, cfp, &rightIndex);
             }
 
-            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override {
+            std::vector<Colored::interval_vector_t> getOutputIntervals(const std::vector<VariableIntervalMap>& varMapVec, std::vector<const Colored::ColorType *> &colortypes) const override {
                 //We could maybe reduce the intervals slightly by checking if the upper or lower bound is being subtracted
-                auto leftIntervals = _left->getOutputIntervals(varMapVec, colortypes);
-
-                return leftIntervals;
+                return _left->getOutputIntervals(varMapVec, colortypes);
             }   
 
-            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+            void getConstants(PositionColorsMap &constantMap, uint32_t &index) const override {
                 uint32_t rIndex = index;
                 _left->getConstants(constantMap, index);
                 _right->getConstants(constantMap, rIndex);
@@ -1421,27 +1377,27 @@
             ArcExpression_ptr _expr;
             
         public:
-            Multiset eval(ExpressionContext& context) const override {
+            Multiset eval(const ExpressionContext& context) const override {
                 return _expr->eval(context) * _scalar;
             }
             
-            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);
+            void getVariables(std::set<const Colored::Variable*>& variables, PositionVariableMap& varPositions, VariableModifierMap& varModifierMap, bool includeSubtracts, uint32_t& index) const override {
+                _expr->getVariables(variables, varPositions,varModifierMap, includeSubtracts);
             }
 
             bool isTuple() const override {
                 return _expr->isTuple();
             }
 
-            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals,const PetriEngine::Colored::ColorFixpoint& cfp, uint32_t& index, int32_t modifier) const override {
                return _expr ->getArcIntervals(arcIntervals, cfp, index, modifier);
             }
 
-            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override {
+            std::vector<Colored::interval_vector_t> getOutputIntervals(const std::vector<VariableIntervalMap>& varMapVec, std::vector<const Colored::ColorType *> &colortypes) const override {
                 return _expr->getOutputIntervals(varMapVec, colortypes);
             }
 
-            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+            void getConstants(PositionColorsMap &constantMap, uint32_t &index) const override {
                 _expr->getConstants(constantMap, index);
             }
 

=== modified file 'include/PetriEngine/Colored/GuardRestrictor.h'
--- include/PetriEngine/Colored/GuardRestrictor.h	2021-04-14 10:41:18 +0000
+++ include/PetriEngine/Colored/GuardRestrictor.h	2021-07-07 08:15:00 +0000
@@ -33,90 +33,109 @@
 
                 GuardRestrictor();
 
-                void restrictDiagonal(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
-                            std::unordered_map<uint32_t, const Color*> *constantMapL,
-                            std::unordered_map<uint32_t, const Color*> *constantMapR,
+                void restrictDiagonal(std::vector<VariableIntervalMap>& variableMap,
+                            const VariableModifierMap &varModifierMapL,
+                            const VariableModifierMap &varModifierMapR,
+                            const PositionVariableMap &varPositionsL,
+                            const PositionVariableMap &varPositionsR,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
                             std::set<const Colored::Variable*> &diagonalVars,
                             const Colored::Variable *var, 
-                            uint32_t index, bool lessthan, bool strict);
+                            uint32_t index, bool lessthan, bool strict) const;
 
                 
 
-                void restrictEquality(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
-                            std::unordered_map<uint32_t, const Color*> *constantMapL,
-                            std::unordered_map<uint32_t, const Color*> *constantMapR,
-                            std::set<const Colored::Variable*> &diagonalVars);
-
-                void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
-                            std::unordered_map<uint32_t, const Color*> *constantMapL,
-                            std::unordered_map<uint32_t, const Color*> *constantMapR,
+                void restrictEquality(std::vector<VariableIntervalMap>& variableMap,
+                            const VariableModifierMap &varModifierMapL,
+                            const VariableModifierMap &varModifierMapR,
+                            const PositionVariableMap &varPositionsL,
+                            const PositionVariableMap &varPositionsR,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
+                            std::set<const Colored::Variable*> &diagonalVars) const;
+
+                void restrictInEquality(std::vector<VariableIntervalMap>& variableMap,
+                            const VariableModifierMap &varModifierMapL,
+                            const VariableModifierMap &varModifierMapR,
+                            const PositionVariableMap &varPositionsL,
+                            const PositionVariableMap &varPositionsR,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
+                            std::set<const Colored::Variable*> &diagonalVars) const;
+
+                void restrictVars(std::vector<VariableIntervalMap>& variableMap,
+                            const VariableModifierMap &varModifierMapL,
+                            const VariableModifierMap &varModifierMapR,
+                            const PositionVariableMap &varPositionsL,
+                            const PositionVariableMap &varPositionsR,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
                             std::set<const Colored::Variable*> &diagonalVars, 
-                            bool lessthan, bool strict);
+                            bool lessthan, bool strict) const;
 
-                intervalTuple_t shiftIntervals(std::unordered_map<const Variable *, intervalTuple_t>& varMap, 
-                            std::vector<const ColorType *> *colortypes, intervalTuple_t *intervals, 
+                interval_vector_t shiftIntervals(const VariableIntervalMap& varMap, 
+                            const std::vector<const ColorType *> &colortypes, interval_vector_t &intervals, 
                             int32_t modifier, uint32_t ctSizeBefore) const; 
 
             private:
-                int32_t getVarModifier(std::unordered_map<uint32_t, int32_t> *modPairMap, uint32_t index);
-                interval_t getIntervalFromIds(std::vector<uint32_t> *idVec, uint32_t ctSize, int32_t modifier);
-                intervalTuple_t getIntervalOverlap(std::vector<Colored::interval_t> *intervals1, std::vector<Colored::interval_t> *intervals2);
-
-                void expandIdVec(std::unordered_map<const Variable *, intervalTuple_t> *varMap,
-                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
-                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
-                            std::unordered_map<uint32_t, const Variable *> *varPositions,
-                            std::unordered_map<uint32_t, const Color*> *constantMap,
-                            const Variable *otherVar, 
-                            std::vector<uint32_t> &idVec, size_t targetSize, uint32_t index);
-
-                void expandIntervalVec(std::unordered_map<const Variable *, intervalTuple_t> varMap,
-                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
-                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
-                            std::unordered_map<uint32_t, const Variable *> *varPositions,
-                            std::unordered_map<uint32_t, const Color*> *constantMap,
-                            const Variable *otherVar, 
-                            std::vector<interval_t> &intervalVec, size_t targetSize, uint32_t index);
-
-                void restrictByConstant(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositions,
-                            std::unordered_map<uint32_t, const Color*> *constantMap,
+                int32_t getVarModifier(const std::unordered_map<uint32_t, int32_t> &modPairMap, uint32_t index) const;
+                interval_t getIntervalFromIds(const std::vector<uint32_t> &idVec, uint32_t ctSize, int32_t modifier) const;
+                interval_vector_t getIntervalOverlap(const Colored::interval_vector_t &intervals1, const Colored::interval_vector_t &intervals2) const;
+                void invertIntervals(interval_vector_t &intervals, const interval_vector_t &oldIntervals, const ColorType *colorType) const;
+
+
+                void handleInequalityConstants(const std::vector<VariableIntervalMap> &variableMapCopy, 
+                                        std::vector<VariableIntervalMap> &variableMap, 
+                                        const Variable *var, uint32_t varMapIndex) const;
+
+                void handleInequalityVars(const std::vector<VariableIntervalMap> &variableMapCopy, 
+                                        std::vector<VariableIntervalMap> &variableMap, 
+                                        const Variable *var1, const Variable *var2, uint32_t varMapIndex) const;
+
+                void expandIdVec(const VariableIntervalMap &varMap,
+                            const VariableModifierMap &mainVarModifierMap,
+                            const VariableModifierMap &otherVarModifierMap,
+                            const std::unordered_map<uint32_t, const Variable *> &varPositions,
+                            const std::unordered_map<uint32_t, const Color*> &constantMap,
+                            const Variable *otherVar, 
+                            std::vector<uint32_t> &idVec, size_t targetSize, uint32_t index) const;
+
+                void expandIntervalVec(const VariableIntervalMap &varMap,
+                            const VariableModifierMap &mainVarModifierMap,
+                            const VariableModifierMap &otherVarModifierMap,
+                            const std::unordered_map<uint32_t, const Variable *> &varPositions,
+                            const std::unordered_map<uint32_t, const Color*> &constantMap,
+                            const Variable *otherVar, 
+                            interval_vector_t &intervalVec, size_t targetSize, uint32_t index) const;
+
+                void restrictByConstant(std::vector<VariableIntervalMap>& variableMap,
+                            const VariableModifierMap &mainVarModifierMap,
+                            const VariableModifierMap &otherVarModifierMap,
+                            const PositionVariableMap &varPositions,
+                            const std::unordered_map<uint32_t, const Color*> &constantMap,
                             const Colored::Variable *var,
                             const Colored::Variable *otherVar, 
-                            uint32_t index, bool lessthan, bool strict);
+                            uint32_t index, bool lessthan, bool strict) const;
 
-                void restrictEqByConstant(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositions,
-                            std::unordered_map<uint32_t, const Color*> *constantMap,
+                void restrictEqByConstant(std::vector<VariableIntervalMap>& variableMap,
+                            const VariableModifierMap &mainVarModifierMap,
+                            const VariableModifierMap &otherVarModifierMap,
+                            const PositionVariableMap &varPositions,
+                            const std::unordered_map<uint32_t, const Color*> &constantMap,
                             const Colored::Variable *var,
-                            uint32_t index);
+                            uint32_t index) const;
 
-                void restrictEqDiagonal(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
-                            std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsL,
-                            std::unordered_map<uint32_t, const Colored::Variable *> *varPositionsR,
-                            std::unordered_map<uint32_t, const Color*> *constantMapL,
-                            std::unordered_map<uint32_t, const Color*> *constantMapR,
+                void restrictEqDiagonal(std::vector<VariableIntervalMap>& variableMap,
+                            const VariableModifierMap &varModifierMapL,
+                            const VariableModifierMap &varModifierMapR,
+                            const PositionVariableMap &varPositionsL,
+                            const PositionVariableMap &varPositionsR,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapL,
+                            const std::unordered_map<uint32_t, const Color*> &constantMapR,
                             std::set<const Colored::Variable*> &diagonalVars,
                             const Colored::Variable *var, 
-                            uint32_t index);    
+                            uint32_t index) const;    
         };
     }
 }

=== modified file 'include/PetriEngine/Colored/IntervalGenerator.h'
--- include/PetriEngine/Colored/IntervalGenerator.h	2021-04-14 10:41:18 +0000
+++ include/PetriEngine/Colored/IntervalGenerator.h	2021-07-07 08:15:00 +0000
@@ -21,178 +21,28 @@
 #include "ColoredNetStructures.h"
 
 namespace PetriEngine {
-    struct IntervalGenerator {
-        std::vector<Colored::interval_t> getIntervalsFromInterval(Colored::interval_t *interval, uint32_t varPosition, int32_t varModifier, std::vector<Colored::ColorType*> *varColorTypes){
-            std::vector<Colored::interval_t> varIntervals;
-            Colored::interval_t firstVarInterval;
-            varIntervals.push_back(firstVarInterval);
-            for(uint32_t i = varPosition; i < varPosition + varColorTypes->size(); i++){
-                auto ctSize = varColorTypes->operator[](i - varPosition)->size();
-                int32_t lower_val = ctSize + (interval->operator[](i)._lower + varModifier);
-                int32_t upper_val = ctSize + (interval->operator[](i)._upper + varModifier);
-                uint32_t lower = lower_val % ctSize;
-                uint32_t upper = upper_val % ctSize;
-
-                if(lower > upper ){
-                    if(lower == upper+1){
-                        for (auto& varInterval : varIntervals){
-                            varInterval.addRange(0, ctSize -1);
-                        }
-                    } else {
-                        std::vector<Colored::interval_t> newIntervals;
-                        for (auto& varInterval : varIntervals){
-                            Colored::interval_t newVarInterval = varInterval;                                  
-                            varInterval.addRange(0, upper);
-                            newVarInterval.addRange(lower, ctSize -1);
-                            newIntervals.push_back(newVarInterval);
-                        }
-                        varIntervals.insert(varIntervals.end(), newIntervals.begin(), newIntervals.end());
-                    }                
-                } else {
-                    for (auto& varInterval : varIntervals){
-                        varInterval.addRange(lower, upper);
-                    }
-                }            
-            }
-            return varIntervals;
-        }
-
-        void getArcVarIntervals(Colored::intervalTuple_t& varIntervals, std::unordered_map<uint32_t, int32_t> *modIndexMap, Colored::interval_t *interval, std::vector<Colored::ColorType*> *varColorTypes){
-            for(auto& posModPair : *modIndexMap){
-                auto intervals = getIntervalsFromInterval(interval, posModPair.first, posModPair.second, varColorTypes);
-
-                if(varIntervals._intervals.empty()){
-                    for(auto& interval : intervals){
-                        varIntervals.addInterval(std::move(interval));
-                    }
-                } else {
-                    Colored::intervalTuple_t newVarIntervals; 
-                    for(uint32_t i = 0; i < varIntervals.size(); i++){
-                        auto varInterval = &varIntervals[i];
-                        for(auto& interval : intervals){
-                            auto overlap = varInterval->getOverlap(std::move(interval));
-                            if(overlap.isSound()){ 
-                                newVarIntervals.addInterval(std::move(overlap));
-                                //break;
-                            }                                                
-                        }                                   
-                    }                                                                                       
-                    varIntervals = std::move(newVarIntervals);                                          
-                }     
-            } 
-        }
-
-        void populateLocalMap(Colored::ArcIntervals *arcIntervals, 
-                            std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t> &varMap,
-                            std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> &localVarMap,
-                            Colored::interval_t* interval, bool& allVarsAssigned,  uint32_t tuplePos){
-            for(auto& pair : arcIntervals->_varIndexModMap){                     
-                Colored::intervalTuple_t varIntervals; 
-                std::vector<Colored::ColorType*> varColorTypes;
-                pair.first->colorType->getColortypes(varColorTypes);
-                
-                getArcVarIntervals(varIntervals, &pair.second[tuplePos], interval, &varColorTypes);                          
-                
-                if (arcIntervals->_intervalTupleVec.size() > 1 && pair.second[tuplePos].empty()) {
-                    //The variable is not on this side of the add expression, so we add a full interval to compare against for the other side
-                    varIntervals.addInterval(pair.first->colorType->getFullInterval());
-                }
-
-                if(varMap.count(pair.first) == 0){
-                    localVarMap[pair.first] = std::move(varIntervals);                                  
-                } else {                                    
-                    for(auto& varInterval : varIntervals._intervals){
-                        for(auto& interval : varMap[pair.first]._intervals){
-                            auto overlapInterval = varInterval.getOverlap(interval);
-
-                            if(overlapInterval.isSound()){
-                                localVarMap[pair.first].addInterval(overlapInterval);
-                            }
-                        }
-                    }                                    
-                }
-
-                if(localVarMap[pair.first]._intervals.empty()){
-                    allVarsAssigned = false;
-                }                                
-            }         
-        }
-
-        void fillVarMaps(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>> &variableMaps,
-                                            Colored::ArcIntervals *arcIntervals,
-                                            uint32_t *intervalTupleSize,
-                                            uint32_t *tuplePos)
-        {
-            for(uint32_t i = 0; i < *intervalTupleSize; i++){
-                std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> localVarMap;
-                bool validInterval = true;
-                auto interval = &arcIntervals->_intervalTupleVec[*tuplePos]._intervals[i];
-            
-                for(auto pair : arcIntervals->_varIndexModMap){
-                    Colored::intervalTuple_t varIntervals;
-                    std::vector<Colored::ColorType*> varColorTypes;
-                    pair.first->colorType->getColortypes(varColorTypes);
-                    getArcVarIntervals(varIntervals, &pair.second[*tuplePos], interval, &varColorTypes); 
-
-                    if(arcIntervals->_intervalTupleVec.size() > 1 && pair.second[*tuplePos].empty()){
-                        //The variable is not on this side of the add expression, so we add a full interval to compare against for the other side
-                        varIntervals.addInterval(pair.first->colorType->getFullInterval());
-                    } else if(varIntervals.size() < 1){
-                        //If any varinterval ends up empty then we were unable to use this arc interval
-                        validInterval = false;
-                        break;
-                    }
-                    localVarMap[pair.first] = varIntervals;
-                }
-
-                if(validInterval){
-                    variableMaps.push_back(localVarMap);
-                }                          
-            }  
-        }
-
-        bool getVarIntervals(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMaps, std::unordered_map<uint32_t, Colored::ArcIntervals> placeArcIntervals){
-            for(auto& placeArcInterval : placeArcIntervals){            
-                for(uint32_t j = 0; j < placeArcInterval.second._intervalTupleVec.size(); j++){
-                    uint32_t intervalTupleSize = placeArcInterval.second._intervalTupleVec[j].size();
-                    //If we have not found intervals for any place yet, we fill the intervals from this place
-                    //Else we restrict the intervals we already found to only keep those that can also be matched in this place
-                    if(variableMaps.empty()){                    
-                        fillVarMaps(variableMaps, &placeArcInterval.second, &intervalTupleSize, &j);                                            
-                    } else {
-                        std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>> newVarMapVec;
-                        
-                        for(auto& varMap : variableMaps){          
-                            for(uint32_t i = 0; i < intervalTupleSize; i++){
-                                std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> localVarMap;
-                                bool allVarsAssigned = true;
-                                auto interval = &placeArcInterval.second._intervalTupleVec[j]._intervals[i];
-                                
-                                populateLocalMap(&placeArcInterval.second, varMap, localVarMap, interval, allVarsAssigned, j);                       
-                                
-                                for(auto& varTuplePair : varMap){
-                                    if(localVarMap.count(varTuplePair.first) == 0){
-                                        localVarMap[varTuplePair.first] = std::move(varTuplePair.second);
-                                    }
-                                }
-
-                                if(allVarsAssigned){
-                                    newVarMapVec.push_back(std::move(localVarMap));
-                                }
-                                                               
-                            }                                                                                    
-                        }               
-                        variableMaps = std::move(newVarMapVec);                    
-                    }
-                    //If we did not find any intervals for an arc, then the transition cannot be activated
-                    if(variableMaps.empty()){
-                        return false;
-                    }                          
-                }
-            }
-            return true;
-        }
-    };    
+    namespace Colored {
+        class IntervalGenerator {
+            public:
+                IntervalGenerator();
+                bool getVarIntervals(std::vector<VariableIntervalMap>& variableMaps, const std::unordered_map<uint32_t, ArcIntervals> &placeArcIntervals) const;
+            private:
+
+                std::vector<interval_t> getIntervalsFromInterval(const interval_t &interval, uint32_t varPosition, int32_t varModifier, const std::vector<const ColorType*> &varColorTypes) const;
+
+                void getArcVarIntervals(interval_vector_t& varIntervals, const std::unordered_map<uint32_t, int32_t> &modIndexMap, const interval_t &interval, const std::vector<const ColorType*> &varColorTypes) const;
+
+                void populateLocalMap(const ArcIntervals &arcIntervals, 
+                                    const VariableIntervalMap &varMap,
+                                    VariableIntervalMap &localVarMap,
+                                    const interval_t &interval, bool& allVarsAssigned,  uint32_t tuplePos) const;
+
+                void fillVarMaps(std::vector<VariableIntervalMap> &variableMaps,
+                                                    const ArcIntervals &arcIntervals,
+                                                    const uint32_t &intervalTupleSize,
+                                                    const uint32_t &tuplePos) const;               
+        }; 
+    }       
 }
 
 #endif /* INTERVALGENERATOR_H */
\ No newline at end of file

=== modified file 'include/PetriEngine/Colored/Intervals.h'
--- include/PetriEngine/Colored/Intervals.h	2021-04-22 12:43:03 +0000
+++ include/PetriEngine/Colored/Intervals.h	2021-07-07 08:15:00 +0000
@@ -41,26 +41,15 @@
 
             ~interval_t(){}
 
-            interval_t(std::vector<Reachability::range_t> ranges) : _ranges(ranges) {
+            interval_t(const std::vector<Reachability::range_t>& ranges) : _ranges(ranges) {
             }
 
-            size_t size(){
+            size_t size() const {
                 return _ranges.size();
             }
 
-            uint32_t intervalCombinations(){
-                uint32_t product = 1;
-                for(auto range : _ranges){
-                    product *= range.size();
-                }
-                if(_ranges.empty()){
-                    return 0;
-                }
-                return product;
-            }
-
-            bool isSound(){
-                for(auto range: _ranges) {
+            bool isSound() const {
+                for(const auto& range: _ranges) {
                     if(!range.isSound()){
                         return false;
                     }
@@ -68,8 +57,12 @@
                 return true;
             }
 
-            void addRange(Reachability::range_t newRange) {
-                _ranges.push_back(newRange);
+            void addRange(Reachability::range_t&& newRange) {
+                _ranges.emplace_back(newRange);
+            }
+            
+            void addRange(const Reachability::range_t& newRange) {
+                _ranges.emplace_back(newRange);
             }
 
             void addRange(Reachability::range_t newRange, uint32_t index){
@@ -77,59 +70,37 @@
             }
 
             void addRange(uint32_t l, uint32_t u) {
-                _ranges.push_back(Reachability::range_t(l, u));
-            }
-
-            void addRange(uint32_t lower, uint32_t upper, uint32_t index){
-                _ranges.insert(_ranges.begin() + index, Reachability::range_t(lower, upper));
+                _ranges.emplace_back(l, u);
             }
 
             Reachability::range_t& operator[] (size_t index) {
-                return _ranges[index];
-            }
-            
-            Reachability::range_t& operator[] (int index) {
-                return _ranges[index];
-            }
-            
-            Reachability::range_t& operator[] (uint32_t index) {
                 assert(index < _ranges.size());
                 return _ranges[index];
             }
-
-            Reachability::range_t& getFirst() {
-                return _ranges[0];
-            }
-
-            Reachability::range_t& getLast() {
-                return _ranges.back();
-            }
-
-            std::vector<uint32_t> getLowerIds(){
+            
+            const Reachability::range_t& operator[] (size_t index) const {
+
+                return _ranges[index];
+            }
+
+
+            std::vector<uint32_t> getLowerIds() const {
                 std::vector<uint32_t> ids;
-                for(auto range : _ranges){
+                for(auto& range : _ranges){
                     ids.push_back(range._lower);
                 }
                 return ids;
             }
 
-            std::vector<uint32_t> getUpperIds(){
-                std::vector<uint32_t> ids;
-                for(auto range : _ranges){
-                    ids.push_back(range._upper);
-                }
-                return ids;
-            }
-
-            interval_t getSingleColorInterval(){
+            interval_t getSingleColorInterval() const {
                 interval_t newInterval;
-                for(auto id : getLowerIds()){
-                    newInterval.addRange(id,id);
+                for(auto& range : _ranges){
+                    newInterval.addRange(range._lower, range._lower);
                 }
                 return newInterval;
             }
 
-            bool equals(interval_t other){
+            bool equals(const interval_t& other) const {
                 if(other.size() != size()){
                     return false;
                 }
@@ -142,33 +113,27 @@
                 return true;
             }
 
-            uint32_t getContainedColors(){
+            uint32_t getContainedColors() const {
                 uint32_t colors = 1;
-                for(auto range: _ranges) {
+                for(const auto& range : _ranges) {
                     colors *= 1+  range._upper - range._lower;
                 }          
                 return colors;
             }
 
-            bool contains(interval_t other){
+            bool contains(const interval_t &other, const std::vector<bool> &diagonalPositions) const {
                 if(other.size() != size()){
                     return false;
                 }
                 for(uint32_t i = 0; i < size(); i++){
-                    if(!_ranges[i].compare(other[i]).first){
+                    if(!diagonalPositions[i] && !_ranges[i].compare(other[i]).first){
                         return false;
                     }
                 }
                 return true;
             }
 
-            void constrain(interval_t other){
-                for(uint32_t i = 0; i < _ranges.size(); i++){
-                    _ranges[i] &= other._ranges[i];
-                }
-            }
-
-            interval_t getOverlap(interval_t other){
+            interval_t getOverlap(const interval_t &other) const {
                 interval_t overlapInterval;
                 if(size() != other.size()){
                     return overlapInterval;
@@ -182,7 +147,43 @@
                 return overlapInterval;
             }
 
-            std::vector<interval_t> getSubtracted(interval_t other, uint32_t ctSize){
+            interval_t getOverlap(const interval_t& other, const std::vector<bool> &diagonalPositions) const {
+                interval_t overlapInterval;
+                if(size() != other.size()){
+                    return overlapInterval;
+                }
+
+                for(uint32_t i = 0; i < size(); i++){
+                    if(diagonalPositions[i]){
+                        overlapInterval.addRange(_ranges[i]);
+                    } else {
+                        auto rangeCopy = _ranges[i];
+                        overlapInterval.addRange(rangeCopy &= other[i]);
+                    }                    
+                }
+
+                return overlapInterval;
+            }
+
+            interval_t& operator|=(const interval_t& other) {
+                assert(size() == other.size());
+                for(uint32_t l = 0; l < size(); ++l) {
+                    _ranges[l] |= other[l];
+                }
+                return *this;
+            }
+            
+            bool intersects(const interval_t& otherInterval) const {
+                assert(size() == otherInterval.size());
+                for(uint32_t k = 0; k < size(); k++) {     
+                    if(!_ranges[k].intersects(otherInterval[k])) {
+                        return false;
+                    }
+                }
+                return true;
+            }
+            
+            std::vector<interval_t> getSubtracted(const interval_t& other, const std::vector<bool> &diagonalPositions) const {
                 std::vector<interval_t> result;
                 
                 if(size() != other.size()){
@@ -191,9 +192,11 @@
                 
                 for(uint32_t i = 0; i < size(); i++){
                     interval_t newInterval = *this;
+                    if(diagonalPositions[i]){
+                        continue;
+                    }
                     
                     int32_t newMinUpper = std::min(((int) other[i]._lower) -1, (int)_ranges[i]._upper);
-                    //uint32_t otherUpper = (other[i]._upper +1) >= ctSize? ctSize-1: other[i]._upper +1;
                     uint32_t newMaxLower = std::max(other[i]._upper +1, _ranges[i]._lower);
 
                     if(((int32_t) _ranges[i]._lower) <= newMinUpper && newMaxLower <= _ranges[i]._upper){
@@ -218,80 +221,87 @@
                 return result;
             }
 
-            void print() {
-                for(auto range : _ranges){
+            void print() const {
+                for(const auto& range : _ranges){
                     std::cout << " " << range._lower << "-" << range._upper << " ";
                 }
             }
 
-            std::string toString() {
+            std::string toString() const {
                 std::ostringstream strs;
-                for(auto range : _ranges){
+                for(const auto& range : _ranges){
                     strs << " " << range._lower << "-" << range._upper << " ";
                 }
                 return strs.str();
             }
         };
 
-        struct closestIntervals {
+        struct interval_dist_t {
             uint32_t intervalId1;
             uint32_t intervalId2;
             uint32_t distance;
         };
 
-        struct intervalTuple_t {
+        class interval_vector_t {
+        private:
             std::vector<interval_t> _intervals;
-            double totalinputtime = 0;
-
-            ~intervalTuple_t() {
-            }
-
-            intervalTuple_t() {
-            }
-
-            intervalTuple_t(std::vector<interval_t> ranges) :  _intervals(ranges) {
+        public:            
+
+            ~interval_vector_t() {
+            }
+
+            interval_vector_t() {
+            }
+
+            interval_vector_t(const std::vector<interval_t>& ranges) :  _intervals(ranges) {
             };
 
-            interval_t& getFirst(){
+            std::vector<interval_t>::iterator begin() { return _intervals.begin(); }
+            std::vector<interval_t>::iterator end() { return _intervals.end(); }
+            std::vector<interval_t>::const_iterator begin() const { return _intervals.begin(); }
+            std::vector<interval_t>::const_iterator end() const { return _intervals.end(); }
+
+            
+            bool empty() const {
+                return _intervals.empty();
+            }
+
+            void clear() {
+                _intervals.clear();
+            }
+            
+            const interval_t& front() const{
                 return _intervals[0];
             }
 
-            interval_t& back() {
+            const interval_t& back() const {
                 return _intervals.back();
             }
 
-            size_t size() {
+            size_t size() const {
                 return _intervals.size();
             }
 
-            size_t tupleSize() {
+            size_t tupleSize() const {
                 return _intervals[0].size();
             }
 
-            uint32_t getContainedColors(){
+            uint32_t getContainedColors() const {
                 uint32_t colors = 0;
-                for (auto interval : _intervals) {
+                for (const auto& interval : _intervals) {
                     colors += interval.getContainedColors();              
                 }
                 return colors;
             }
 
-            std::pair<uint32_t,uint32_t> shiftInterval(uint32_t lower, uint32_t upper, uint32_t ctSize, int32_t modifier){
+            static std::pair<uint32_t,uint32_t> shiftInterval(uint32_t lower, uint32_t upper, uint32_t ctSize, int32_t modifier) {
                 int32_t lower_val = ctSize + (lower + modifier);
                 int32_t upper_val = ctSize + (upper + modifier);
                 return std::make_pair(lower_val % ctSize, upper_val % ctSize);
             }
 
-            uint32_t intervalCombinations(){
-                uint32_t res = 0;
-                for(auto interval : _intervals){
-                    res += interval.intervalCombinations();
-                }
-                return res;
-            }
-
-            bool hasValidIntervals(){
-                for(auto interval : _intervals) {
+            bool hasValidIntervals() const {
+                for(const auto& interval : _intervals) {
                     if(interval.isSound()){
                         return true;
                     }
@@ -299,20 +309,21 @@
                 return false;
             }
 
+            const interval_t& operator[] (size_t index) const {
+                assert(index < _intervals.size());
+                return _intervals[index];
+            }
+
             interval_t& operator[] (size_t index) {
-                return _intervals[index];
-            }
-            
-            interval_t& operator[] (int index) {
-                return _intervals[index];
-            }
-            
-            interval_t& operator[] (uint32_t index) {
                 assert(index < _intervals.size());
                 return _intervals[index];
             }
-
-            interval_t isRangeEnd(std::vector<uint32_t> ids) {
+            
+            void append(const interval_vector_t& other) {
+                _intervals.insert(_intervals.end(), other._intervals.begin(), other._intervals.end());
+            }
+            
+            interval_t isRangeEnd(const std::vector<uint32_t>& ids) const {
                 for (uint32_t j = 0; j < _intervals.size(); j++) {
                     bool rangeEnd = true;
                     for (uint32_t i = 0; i < _intervals[j].size(); i++) {
@@ -326,16 +337,16 @@
                         if(j+1 != _intervals.size()) {
                             return _intervals[j+1];
                         } else {
-                            return getFirst();
+                            return front();
                         }
                     }
                 }
                 return interval_t();
             }
 
-            std::vector<Colored::interval_t> shrinkIntervals(uint32_t newSize){
+            std::vector<Colored::interval_t> shrinkIntervals(uint32_t newSize) const {
                 std::vector<Colored::interval_t> resizedIntervals;
-                for(auto interval : _intervals){
+                for(auto& interval : _intervals){
                     Colored::interval_t resizedInterval;
                     for(uint32_t i = 0; i < newSize; i++){
                         resizedInterval.addRange(interval[i]);
@@ -345,7 +356,7 @@
                 return resizedIntervals;
             }
 
-            void addInterval(interval_t interval) {
+            void addInterval(const interval_t& interval) {
                 uint32_t vecIndex = 0;
 
                 if(!_intervals.empty()) {
@@ -392,9 +403,9 @@
                 _intervals.insert(_intervals.begin() + vecIndex, interval);
             }
 
-            void constrainLower(std::vector<uint32_t> values, bool strict) {
-                for(uint32_t i = 0; i < _intervals.size(); i++) {
-                    for(uint32_t j = 0; j < values.size(); j++){
+            void constrainLower(const std::vector<uint32_t>& values, bool strict) {
+                for(uint32_t i = 0; i < _intervals.size(); ++i) {
+                    for(uint32_t j = 0; j < values.size(); ++j){
                         if(strict && _intervals[i][j]._lower <= values[j]){
                             _intervals[i][j]._lower = values[j]+1;
                         } 
@@ -406,9 +417,9 @@
                 simplify();
             }
 
-            void constrainUpper(std::vector<uint32_t> values, bool strict) {
-                for(uint32_t i = 0; i < _intervals.size(); i++) {
-                    for(uint32_t j = 0; j < values.size(); j++){
+            void constrainUpper(const std::vector<uint32_t>& values, bool strict) {
+                for(uint32_t i = 0; i < _intervals.size(); ++i) {
+                    for(uint32_t j = 0; j < values.size(); ++j){
                         if(strict && _intervals[i][j]._upper >= values[j]){
                             _intervals[i][j]._upper = values[j]-1;
                         } 
@@ -420,29 +431,17 @@
                 simplify();
             }
 
-            void expandLower(std::vector<uint32_t> values) {
-                for(uint32_t i = 0; i < values.size(); i++) {
-                    _intervals[0][i]._lower = std::min(values[i],_intervals[0][i]._lower);
-                }
-            }
-
-            void expandUpper(std::vector<uint32_t> values) {
-                for(uint32_t i = 0; i < values.size(); i++) {
-                    _intervals[0][i]._upper = std::max(values[i],_intervals[0][i]._upper);
-                }
-            }
-
-            void print() {
-                for (auto interval : _intervals){
+            void print() const {
+                for (const auto& interval : _intervals){
                     std::cout << "[";
                     interval.print();
                     std::cout << "]" << std::endl;
                 }
             }
 
-            std::string toString() {
+            std::string toString() const {
                 std::string out;
-                for (auto interval : _intervals){
+                for (const auto &interval : _intervals){
                     out += "[";
                     out += interval.toString();
                     out += "]\n";
@@ -450,9 +449,9 @@
                 return out;
             }
 
-            std::vector<uint32_t> getLowerIds(){
+            std::vector<uint32_t> getLowerIds() const {
                 std::vector<uint32_t> ids;
-                for(auto interval : _intervals){
+                for(const auto& interval : _intervals){
                     if(ids.empty()){
                         ids = interval.getLowerIds();
                     } else {
@@ -464,13 +463,13 @@
                 return ids;
             }
 
-            std::vector<uint32_t> getLowerIds(int32_t modifier, std::vector<size_t> sizes){
+            std::vector<uint32_t> getLowerIds(int32_t modifier, const std::vector<size_t>& sizes) const {
                 std::vector<uint32_t> ids;
                 for(uint32_t j = 0; j < size(); j++){
-                    auto interval = &_intervals[j];
+                    auto& interval = _intervals[j];
                     if(ids.empty()){
                         for(uint32_t i = 0; i < ids.size(); i++){
-                            auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier);
+                            auto shiftedInterval = shiftInterval(interval[i]._lower, interval[i]._upper, sizes[i], modifier);
                             if(shiftedInterval.first > shiftedInterval.second){
                                 ids.push_back(0);
                             } else {
@@ -482,7 +481,7 @@
                             if(ids[i] == 0){
                                 continue;
                             }
-                            auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier);
+                            auto shiftedInterval = shiftInterval(interval[i]._lower, interval[i]._upper, sizes[i], modifier);
                             if(shiftedInterval.first > shiftedInterval.second){
                                 ids[i] = 0;
                             } else {
@@ -494,27 +493,13 @@
                 return ids;
             }
 
-            std::vector<uint32_t> getUpperIds(){
-                std::vector<uint32_t> ids;
-                for(auto interval : _intervals){
-                    if(ids.empty()){
-                        ids = interval.getUpperIds();
-                    } else {
-                        for(uint32_t i = 0; i < ids.size(); i++){
-                            ids[i] = std::max(ids[i], interval[i]._upper);
-                        }
-                    }
-                }
-                return ids;
-            }
-
-            std::vector<uint32_t> getUpperIds(int32_t modifier, std::vector<size_t> sizes){
+            std::vector<uint32_t> getUpperIds(int32_t modifier, const std::vector<size_t>& sizes) const {
                 std::vector<uint32_t> ids;
                 for(uint32_t j = 0; j < size(); j++){
-                    auto interval = &_intervals[j];
+                    const auto& interval = _intervals[j];
                     if(ids.empty()){
                         for(uint32_t i = 0; i < ids.size(); i++){
-                            auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier);
+                            auto shiftedInterval = shiftInterval(interval[i]._lower, interval[i]._upper, sizes[i], modifier);
 
                             if(shiftedInterval.first > shiftedInterval.second){
                                 ids.push_back(sizes[i]-1);
@@ -527,7 +512,7 @@
                             if(ids[i] == sizes[i]-1){
                                 continue;
                             }
-                            auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier);
+                            auto shiftedInterval = shiftInterval(interval[i]._lower, interval[i]._upper, sizes[i], modifier);
 
                             if(shiftedInterval.first > shiftedInterval.second){
                                 ids[i] = sizes[i]-1;
@@ -540,7 +525,7 @@
                 return ids;
             }
 
-            void applyModifier(int32_t modifier, std::vector<size_t> sizes){
+            void applyModifier(int32_t modifier, const std::vector<size_t>& sizes) {
                 std::vector<interval_t> collectedIntervals;
                 for(auto& interval : _intervals){
                     std::vector<interval_t> newIntervals;
@@ -550,7 +535,7 @@
                         for(auto& interval1 : newIntervals){
                             auto shiftedInterval = shiftInterval(interval1[i]._lower, interval1[i]._upper, sizes[i], modifier);
 
-                            if(shiftedInterval.first > shiftedInterval.second){
+                            if(shiftedInterval.first > shiftedInterval.second) {
                                 auto newInterval = interval1;
 
                                 interval1[i]._lower = 0;
@@ -559,7 +544,7 @@
                                 newInterval[i]._lower = shiftedInterval.first;
                                 newInterval[i]._upper = sizes[i]-1;
                                 tempIntervals.push_back(std::move(newInterval));
-                            }else {
+                            } else {
                                 interval1[i]._lower = shiftedInterval.first;
                                 interval1[i]._upper = shiftedInterval.second;
                             }
@@ -572,43 +557,34 @@
                 _intervals = std::move(collectedIntervals);
             }
 
-            bool contains(interval_t interval){
-                for(auto localInterval : _intervals){
-                    if(localInterval.contains(interval)){
+            bool contains(const interval_t &interval, const std::vector<bool> &diagonalPositions) const {
+                for(const auto &localInterval : _intervals){
+                    if(localInterval.contains(interval, diagonalPositions)){
                         return true;
                     }
                 }
                 return false;
             }
 
-            void removeInterval(interval_t interval) {
-                for (uint32_t i = 0; i < _intervals.size(); i++) {
-                    if(interval.equals(_intervals[i])){
-                        removeInterval(i);
-                        return;
-                    }
-                }
-            }
-
             void removeInterval(uint32_t index) {               
                 _intervals.erase(_intervals.begin() + index); 
             }
 
             
 
-            void restrict(uint32_t k){              
+            void restrict(uint32_t k) {              
                 simplify();
                 if(k == 0){
                     return;
                 }
                 
                 while (size() > k){ 
-                    closestIntervals closestInterval = getClosestIntervals();
-                    auto interval = &_intervals[closestInterval.intervalId1]; 
-                    auto otherInterval = &_intervals[closestInterval.intervalId2]; 
+                    interval_dist_t closestInterval = getClosestIntervals();
+                    auto& interval = _intervals[closestInterval.intervalId1]; 
+                    const auto& otherInterval = _intervals[closestInterval.intervalId2]; 
 
-                    for(uint32_t l = 0; l < interval->size(); l++) {
-                        interval->operator[](l) |= otherInterval->operator[](l);
+                    for(uint32_t l = 0; l < interval.size(); l++) {
+                        interval[l] |= otherInterval[l];
                     }
                     
                     _intervals.erase(_intervals.begin() + closestInterval.intervalId2);
@@ -616,85 +592,55 @@
                 simplify();
             }
 
-            closestIntervals getClosestIntervals(){
-                closestIntervals currentBest = {0,0, UINT32_MAX};
-                    for (uint32_t i = 0; i < size()-1; i++) {
-                        auto interval = &_intervals[i];
-                        for(uint32_t j = i+1; j < size(); j++){
-                            auto otherInterval = &_intervals[j];
-                            uint32_t dist = 0;
-                            
-                            for(uint32_t k = 0; k < interval->size(); k++) {
-                                int32_t val1 = otherInterval->operator[](k)._lower - interval->operator[](k)._upper;
-                                int32_t val2 = interval->operator[](k)._lower - otherInterval->operator[](k)._upper;
-                                // int32_t lowerDist = interval->operator[](k)._lower > otherInterval->operator[](k)._lower? 
-                                //     interval->operator[](k)._lower - otherInterval->operator[](k)._lower : 
-                                //     otherInterval->operator[](k)._lower - interval->operator[](k)._lower;
-                                // int32_t upperDist = interval->operator[](k)._upper > otherInterval->operator[](k)._upper? 
-                                //     interval->operator[](k)._upper - otherInterval->operator[](k)._upper : 
-                                //     otherInterval->operator[](k)._upper - interval->operator[](k)._upper;
-                                dist += std::max(0, std::max(val1, val2));
-                                //dist += std::max(upperDist + lowerDist, upperDist + lowerDist + std::max(val1, val2));
-                                if(dist >= currentBest.distance){
-                                    break;
-                                }
+            interval_dist_t getClosestIntervals() const {
+                interval_dist_t currentBest = {0,0, std::numeric_limits<uint32_t>::max()};
+                for (uint32_t i = 0; i < size()-1; i++) {
+                    const auto& interval = _intervals[i];
+                    for(uint32_t j = i+1; j < size(); j++){
+                        const auto& otherInterval = _intervals[j];
+                        uint32_t dist = 0;
+
+                        for(uint32_t k = 0; k < interval.size(); k++) {
+                            int32_t val1 = otherInterval[k]._lower - interval[k]._upper;
+                            int32_t val2 = interval[k]._lower - otherInterval[k]._upper;
+                            dist += std::max(0, std::max(val1, val2));
+                            if(dist >= currentBest.distance){
+                                break;
                             }
-                            
-                            if(dist < currentBest.distance){
-                                currentBest.distance = dist;
-                                currentBest.intervalId1 = i;
-                                currentBest.intervalId2 = j;
-
-                                //if the distance is 1 we cannot find any intervals that are closer so we stop searching
-                                if(currentBest.distance == 1){
-                                    return currentBest;
-                                }
-                            }                           
                         }
+
+                        if(dist < currentBest.distance){
+                            currentBest.distance = dist;
+                            currentBest.intervalId1 = i;
+                            currentBest.intervalId2 = j;
+
+                            //if the distance is 1 we cannot find any intervals that are closer so we stop searching
+                            if(currentBest.distance == 1){
+                                return currentBest;
+                            }
+                        }                           
                     }
+                }
                 return currentBest;
             }
 
             void simplify() {
-                std::set<uint32_t> rangesToRemove;
-                if(_intervals.empty()){
-                    return;
+                while(!_intervals.empty() && !_intervals[0].isSound()){
+                    _intervals.erase(_intervals.begin());
                 }
-
-                for (uint32_t i = 0; i < _intervals.size(); i++) {
-                    auto interval = &_intervals[i];
-                    if(!interval->isSound()){
-                        rangesToRemove.insert(i);
-                        continue;
-                    }   
-                    for(uint32_t j = i+1; j < _intervals.size(); j++){
-                        auto otherInterval = &_intervals[j];
-
-                        if(!otherInterval->isSound()){
-                            continue;
-                        }   
-                        bool overlap = true;
-
-                        if(overlap){
-                            for(uint32_t k = 0; k < interval->size(); k++) {                            
-                                if(interval->operator[](k)._lower > otherInterval->operator[](k)._upper  || otherInterval->operator[](k)._lower > interval->operator[](k)._upper) {
-                                    overlap = false;
-                                    break;
-                                }
-                            }
-                        }
-                        
-                        if(overlap) {
-                            for(uint32_t l = 0; l < interval->size(); l++) {
-                                interval->operator[](l) |= otherInterval->operator[](l);
-                            }
-                            rangesToRemove.insert(j);
-                        }  
+                for (size_t i = 0; i < _intervals.size(); ++i) {                    
+                    for(size_t j = _intervals.size()-1; j > i; --j){
+                        const auto& otherInterval = _intervals[j];
+                        auto& interval = _intervals[i];
+                        if(!otherInterval.isSound()){
+                            _intervals.erase(_intervals.begin() + j);
+                        }
+                        else if(interval.intersects(otherInterval)) {
+                            interval |= otherInterval;
+                            _intervals.erase(_intervals.begin() + j);
+                        }
                     }
                 }
-                for (auto i = rangesToRemove.rbegin(); i != rangesToRemove.rend(); ++i) {
-                    _intervals.erase(_intervals.begin() + *i);
-                }
             }
 
             void combineNeighbours() {
@@ -704,15 +650,15 @@
                 }
 
                 for (uint32_t i = 0; i < _intervals.size(); i++) {
-                    auto interval = &_intervals[i];
-                    if(!interval->isSound()){
+                    auto& interval = _intervals[i];
+                    if(!interval.isSound()){
                         rangesToRemove.insert(i);
                         continue;
                     }   
                     for(uint32_t j = i+1; j < _intervals.size(); j++){
-                        auto otherInterval = &_intervals[j];
+                        const auto& otherInterval = _intervals[j];
 
-                        if(!otherInterval->isSound()){
+                        if(!otherInterval.isSound()){
                             continue;
                         }   
                         bool overlap = true;
@@ -720,9 +666,10 @@
                         uint32_t dist = 1;
 
                         if(overlap){
-                            for(uint32_t k = 0; k < interval->size(); k++) {                            
-                                if(interval->operator[](k)._lower > otherInterval->operator[](k)._upper  || otherInterval->operator[](k)._lower > interval->operator[](k)._upper) {
-                                    if(interval->operator[](k)._lower > otherInterval->operator[](k)._upper + dist  || otherInterval->operator[](k)._lower > interval->operator[](k)._upper + dist) {
+                            for(uint32_t k = 0; k < interval.size(); k++) {                            
+                                if(interval[k]._lower > otherInterval[k]._upper  || otherInterval[k]._lower > interval[k]._upper) {
+                                    if(interval[k]._lower > otherInterval[k]._upper + dist  || 
+                                        otherInterval[k]._lower > interval[k]._upper + dist) {
                                         overlap = false;
                                         break;
                                     } else {
@@ -733,8 +680,8 @@
                         }
                         
                         if(overlap) {
-                            for(uint32_t l = 0; l < interval->size(); l++) {
-                                interval->operator[](l) |= otherInterval->operator[](l);
+                            for(uint32_t l = 0; l < interval.size(); l++) {
+                                interval[l] |= otherInterval[l];
                             }
                             rangesToRemove.insert(j);
                         }  

=== modified file 'include/PetriEngine/Colored/Multiset.h'
--- include/PetriEngine/Colored/Multiset.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/Colored/Multiset.h	2021-07-07 08:15:00 +0000
@@ -26,18 +26,18 @@
         private:
             class Iterator {
             private:
-                Multiset* ms;
-                size_t index;
+                const Multiset* _ms;
+                size_t _index;
 
             public:
-                Iterator(Multiset* ms, size_t index)
-                        : ms(ms), index(index) {}
+                Iterator(const Multiset* ms, size_t index)
+                        : _ms(ms), _index(index) {}
 
                 bool operator==(Iterator& other);
                 bool operator!=(Iterator& other);
                 Iterator& operator++();
-                std::pair<const Color*,uint32_t&> operator++(int);
-                std::pair<const Color*,uint32_t&> operator*();
+                std::pair<const Color*,const uint32_t&> operator++(int);
+                std::pair<const Color*, const uint32_t&> operator*();
             };
 
             typedef std::vector<std::pair<uint32_t,uint32_t>> Internal;
@@ -67,14 +67,14 @@
 
             size_t size() const;
             
-            Iterator begin();
-            Iterator end();
+            const Iterator begin() const;
+            const Iterator end() const;
 
             std::string toString() const;
             
         private:
             Internal _set;
-            ColorType* type;
+            const ColorType* _type;
         };
     }
 }

=== modified file 'include/PetriEngine/Colored/PartitionBuilder.h'
--- include/PetriEngine/Colored/PartitionBuilder.h	2021-04-22 12:43:03 +0000
+++ include/PetriEngine/Colored/PartitionBuilder.h	2021-07-07 08:15:00 +0000
@@ -1,59 +1,76 @@
 #include "ColoredNetStructures.h"
-#include "EquivalenceClass.h"
+#include "EquivalenceVec.h"
 #include "IntervalGenerator.h"
  
 namespace PetriEngine {
     namespace Colored {
         class PartitionBuilder {
+
+            
             public:
-                PartitionBuilder(std::vector<Transition> *transitions, 
-                                std::vector<Place> *places, 
-                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, 
-                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap);
+                PartitionBuilder(const std::vector<Transition> &transitions, 
+                                const std::vector<Place> &places, 
+                                const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePostTransitionMap, 
+                                const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePreTransitionMap);
 
-                PartitionBuilder(std::vector<Transition> *transitions, 
-                                std::vector<Place> *places, 
-                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, 
-                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap,
-                                std::vector<Colored::ColorFixpoint> *placeColorFixpoints);
+                PartitionBuilder(const std::vector<Transition> &transitions, 
+                                const std::vector<Place> &places, 
+                                const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePostTransitionMap, 
+                                const std::unordered_map<uint32_t,std::vector<uint32_t>> &placePreTransitionMap,
+                                const std::vector<Colored::ColorFixpoint> *placeColorFixpoints);
                 
                 ~PartitionBuilder() {}
 
                 //void initPartition();
-                void partitionNet();
-                void refinePartition();
-                void printPartion();
-                void assignColorMap(std::unordered_map<uint32_t, EquivalenceVec> &partition);
+                bool partitionNet(int32_t timeout);
+                void printPartion() const;
+                void assignColorMap(std::unordered_map<uint32_t, EquivalenceVec> &partition) const;
 
-                std::unordered_map<uint32_t, EquivalenceVec> getPartition(){
+                std::unordered_map<uint32_t, EquivalenceVec> getPartition() const{
                     return _partition;
                 }
+
             private:
-                std::vector<Transition> *_transitions;
-                std::unordered_map<uint32_t,std::vector<uint32_t>> *_placePostTransitionMap;
-                std::unordered_map<uint32_t,std::vector<uint32_t>> *_placePreTransitionMap;
+                const std::vector<Transition> &_transitions;
+                const std::vector<Place> &_places;
+                const std::unordered_map<uint32_t,std::vector<uint32_t>> &_placePostTransitionMap;
+                const std::unordered_map<uint32_t,std::vector<uint32_t>> &_placePreTransitionMap;
                 std::unordered_map<uint32_t,bool> _inQueue;
-                std::vector<Place> *_places;
                 std::unordered_map<uint32_t, EquivalenceVec> _partition;
-                PetriEngine::IntervalGenerator intervalGenerator;
+                const PetriEngine::Colored::IntervalGenerator _interval_generator = IntervalGenerator();
                 std::vector<uint32_t> _placeQueue;
 
                 bool splitPartition(EquivalenceVec equivalenceVec, uint32_t placeId);
 
                 void handleTransition(uint32_t transitionId, uint32_t postPlaceId);
-                void handleTransition(Transition *transitionId, uint32_t postPlaceId, Arc *postArc);
+                void handleTransition(const Transition &transitionId, const uint32_t postPlaceId, const Arc *postArc);
 
                 void handleLeafTransitions();
                 
                 void addToQueue(uint32_t placeId);
 
-                std::vector<std::unordered_map<const Variable *, intervalTuple_t>> prepareVariables(
-                            std::unordered_map<const Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap, 
-                            EquivalenceClass *eqClass , Arc *postArc, uint32_t placeId);
-
-                bool findOverlap(EquivalenceVec equivalenceVec1, EquivalenceVec equivalenceVec2, uint32_t &overlap1, uint32_t &overlap2, EquivalenceClass &intersection);
-
-                uint32_t eqClassIdCounter = 0;
+                bool checkTupleDiagonal(uint32_t placeId);
+                bool checkDiagonal(uint32_t placeId);
+
+                void handleInArcs(const Transition &transition, std::set<const Colored::Variable*> &diagonalVars, const PositionVariableMap &varPositionMap, const std::vector<PetriEngine::Colored::VariableIntervalMap> &varMaps, uint32_t postPlaceId);
+
+                void applyNewIntervals(const Arc &inArc, const std::vector<PetriEngine::Colored::VariableIntervalMap> &varMaps);
+
+                void checkVarOnArc(const VariableModifierMap &varModifierMap, std::set<const Colored::Variable*> &diagonalVars, uint32_t placeId, bool inputArc);
+
+                void checkVarOnInputArcs(const std::unordered_map<uint32_t,PositionVariableMap> &placeVariableMap, const PositionVariableMap &preVarPositionMap, std::set<const Colored::Variable*> &diagonalVars, uint32_t placeId);
+
+                void markSharedVars(const PositionVariableMap &preVarPositionMap, const PositionVariableMap &varPositionMap, uint32_t postPlaceId, uint32_t prePlaceId);
+                void checkVarInGuard(const PositionVariableMap &preVarPositionMap, const std::set<const Colored::Variable*> &diagonalVars, uint32_t placeId);
+
+                std::vector<VariableIntervalMap> prepareVariables(
+                            const VariableModifierMap &varModifierMap, 
+                            const EquivalenceClass& eqClass , const Arc *postArc, uint32_t placeId);
+
+                bool findOverlap(const EquivalenceVec &equivalenceVec1,const EquivalenceVec &equivalenceVec2, uint32_t &overlap1, uint32_t &overlap2, EquivalenceClass &intersection);
+
+                uint32_t _eq_id_counter = 0;
+
         };
     }
-}
\ No newline at end of file
+}

=== modified file 'include/PetriEngine/PQL/Expressions.h'
--- include/PetriEngine/PQL/Expressions.h	2021-04-06 13:10:00 +0000
+++ include/PetriEngine/PQL/Expressions.h	2021-07-07 08:15:00 +0000
@@ -105,6 +105,7 @@
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
             bool tk = false;
 
             void visit(Visitor& visitor) const override;
@@ -125,6 +126,7 @@
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
 
 
             void toBinary(std::ostream&) const override;
@@ -143,6 +145,7 @@
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
 
 
             void visit(Visitor& visitor) const override;
@@ -164,6 +167,7 @@
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
             void toBinary(std::ostream&) const override;
 
             void visit(Visitor& visitor) const override;
@@ -187,6 +191,7 @@
             int evaluate(const EvaluationContext& context) override;
             Expr::Types type() const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
             void toBinary(std::ostream&) const override;
 
             void visit(Visitor& visitor) const override;
@@ -218,6 +223,7 @@
             void toXML(std::ostream& os, uint32_t tabs, bool tokencount = false) const override {
                 _compiled->toXML(os, tabs, tokencount);
             }
+            void toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
 
             int formulaSize() const override {
                 if(_compiled) return _compiled->formulaSize();
@@ -266,6 +272,7 @@
             int evaluate(const EvaluationContext& context) override;
             Expr::Types type() const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const override;
             void toBinary(std::ostream&) const override;
             int formulaSize() const override{
                 return 1;
@@ -309,6 +316,8 @@
 
             void toXML(std::ostream& out, uint32_t tabs) const override
             { _compiled->toXML(out, tabs); }
+            void toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const override{
+            }
 
 
             Quantifier getQuantifier() const override
@@ -376,6 +385,7 @@
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
             void toBinary(std::ostream&) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
 
             Quantifier getQuantifier() const override { return Quantifier::NEG; }
@@ -443,6 +453,7 @@
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::pError; }
             uint32_t distance(DistanceContext& context) const override {
@@ -471,6 +482,7 @@
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
             Path getPath() const override             { return Path::pError; }
             uint32_t distance(DistanceContext& context) const override {
@@ -509,6 +521,7 @@
           Retval simplify(SimplificationContext &context) const override;
 
           void toXML(std::ostream &, uint32_t tabs) const override;
+          void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
           Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
 
@@ -550,6 +563,7 @@
             }
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
             Path getPath() const override             { return Path::F; }
             uint32_t distance(DistanceContext& context) const override {
@@ -577,6 +591,7 @@
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             Retval simplify(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
             Path getPath() const override             { return Path::X; }
             uint32_t distance(DistanceContext& context) const override {
@@ -598,6 +613,7 @@
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::X; }
             uint32_t distance(DistanceContext& context) const override;
@@ -618,6 +634,7 @@
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::G; }
             uint32_t distance(DistanceContext& context) const override;
@@ -639,6 +656,7 @@
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::F; }
             uint32_t distance(DistanceContext& context) const override;
@@ -658,6 +676,7 @@
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
             Path getPath() const override             { return Path::X; }
             uint32_t distance(DistanceContext& context) const override;
@@ -677,6 +696,7 @@
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
             Path getPath() const override             { return Path::G; }
             uint32_t distance(DistanceContext& context) const override;
@@ -696,6 +716,7 @@
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
             Path getPath() const override             { return Path::F; }
             uint32_t distance(DistanceContext& context) const override;
@@ -742,6 +763,7 @@
             void visit(Visitor&) const override;
             void visit(MutatingVisitor&) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             uint32_t distance(DistanceContext& context) const override { return (*this)[1]->distance(context); }
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
         private:
@@ -763,6 +785,7 @@
             uint32_t distance(DistanceContext& context) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
         private:
             std::string op() const override;
@@ -777,6 +800,7 @@
             void visit(MutatingVisitor&) override;
             uint32_t distance(DistanceContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             virtual bool isLoopSensitive() const override { return true; }
         private:
@@ -794,6 +818,8 @@
             std::string getName() const {
                 return _name;
             }
+            void toXML(std::ostream& out, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
         protected:
             void _analyze(AnalysisContext& context) override;
 
@@ -810,7 +836,7 @@
             Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void visit(Visitor&) const override;
             void visit(MutatingVisitor&) override;
-
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             std::string getName() const {
                 return _name;
             }
@@ -890,6 +916,7 @@
             void visit(Visitor&) const override;
             void visit(MutatingVisitor&) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Quantifier getQuantifier() const override { return Quantifier::AND; }
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             uint32_t distance(DistanceContext& context) const override;
@@ -914,6 +941,7 @@
             void visit(Visitor&) const override;
             void visit(MutatingVisitor&) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             Quantifier getQuantifier() const override { return Quantifier::OR; }
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
@@ -1001,6 +1029,7 @@
             CTLType getQueryType() const override { return CTLType::LOPERATOR; }
             Path getPath() const override         { return Path::pError; }
             virtual void toXML(std::ostream& stream, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
             Retval simplify(SimplificationContext& context) const override;
             Result evaluate(const EvaluationContext& context) override;
             Result evalAndSet(const EvaluationContext& context) override;
@@ -1090,6 +1119,7 @@
             using CompareCondition::CompareCondition;
             Retval simplify(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             uint32_t distance(DistanceContext& context) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
@@ -1110,6 +1140,7 @@
             void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
             Retval simplify(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
 
             uint32_t distance(DistanceContext& context) const override;
@@ -1130,6 +1161,7 @@
             using CompareCondition::CompareCondition;
             Retval simplify(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             uint32_t distance(DistanceContext& context) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
@@ -1149,6 +1181,7 @@
             using CompareCondition::CompareCondition;
             Retval simplify(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             uint32_t distance(DistanceContext& context) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
@@ -1191,6 +1224,7 @@
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
             void toBinary(std::ostream&) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
             Path getPath() const override { return Path::pError; }
@@ -1223,6 +1257,7 @@
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
             void toBinary(std::ostream&) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             static Condition_ptr DEADLOCK;
             Quantifier getQuantifier() const override { return Quantifier::DEADLOCK; }
@@ -1355,6 +1390,7 @@
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
+            void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const override;
 
             Quantifier getQuantifier() const override { return Quantifier::UPPERBOUNDS; }
             Path getPath() const override { return Path::pError; }

=== modified file 'include/PetriEngine/PQL/PQL.h'
--- include/PetriEngine/PQL/PQL.h	2021-03-23 14:10:04 +0000
+++ include/PetriEngine/PQL/PQL.h	2021-07-07 08:15:00 +0000
@@ -120,6 +120,7 @@
             /** Output the expression as it currently is to a file in XML */
             virtual void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const = 0;
             virtual void toBinary(std::ostream&) const = 0;
+            virtual void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context, bool tokencount = false) const = 0;
 
             /** Count size of the entire formula in number of nodes */
             [[nodiscard]] virtual int formulaSize() const = 0;
@@ -231,6 +232,7 @@
             
             /** Output the condition as it currently is to a file in XML */
             virtual void toXML(std::ostream&, uint32_t tabs) const = 0;
+            virtual void toCompactXML(std::ostream&, uint32_t tabs, AnalysisContext& context) const = 0;
             virtual void toBinary(std::ostream& out) const = 0;
 
             /** Checks if the condition is trivially true */

=== modified file 'include/PetriEngine/PetriNetBuilder.h'
--- include/PetriEngine/PetriNetBuilder.h	2021-03-05 16:43:31 +0000
+++ include/PetriEngine/PetriNetBuilder.h	2021-07-07 08:15:00 +0000
@@ -135,8 +135,8 @@
         std::vector< std::tuple<double, double> > _placelocations;
         std::vector< std::tuple<double, double> > _transitionlocations;
         
-        std::vector<Transition> _transitions;
-        std::vector<Place> _places;
+        std::vector<PetriEngine::Transition> _transitions;
+        std::vector<PetriEngine::Place> _places;
         
         std::vector<MarkVal> initialMarking;
         Reducer reducer;

=== modified file 'include/PetriEngine/Reducer.h'
--- include/PetriEngine/Reducer.h	2021-06-22 09:25:10 +0000
+++ include/PetriEngine/Reducer.h	2021-07-07 08:15:00 +0000
@@ -14,7 +14,6 @@
 #include "NetStructures.h"
 
 #include <vector>
-#include <optional>
 
 namespace PetriEngine {
 
@@ -132,7 +131,7 @@
         bool ReducebyRuleA(uint32_t* placeInQuery);
         bool ReducebyRuleB(uint32_t* placeInQuery, bool remove_deadlocks, bool remove_consumers);
         bool ReducebyRuleC(uint32_t* placeInQuery);
-        bool ReducebyRuleD(uint32_t *placeInQuery, bool remove_consumers);
+        bool ReducebyRuleD(uint32_t* placeInQuery);
         bool ReducebyRuleE(uint32_t* placeInQuery);
         bool ReducebyRuleI(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers);
         bool ReducebyRuleF(uint32_t* placeInQuery);
@@ -147,9 +146,9 @@
         std::string getTransitionName(uint32_t transition);
         std::string getPlaceName(uint32_t place);
         
-        Transition& getTransition(uint32_t transition);
-        ArcIter getOutArc(Transition&, uint32_t place);
-        ArcIter getInArc(uint32_t place, Transition&);
+        PetriEngine::Transition& getTransition(uint32_t transition);
+        ArcIter getOutArc(PetriEngine::Transition&, uint32_t place);
+        ArcIter getInArc(uint32_t place, PetriEngine::Transition&);
         void eraseTransition(std::vector<uint32_t>&, uint32_t);
         void skipTransition(uint32_t);
         void skipPlace(uint32_t);

=== modified file 'include/PetriEngine/TAR/range.h'
--- include/PetriEngine/TAR/range.h	2021-02-18 12:01:45 +0000
+++ include/PetriEngine/TAR/range.h	2021-07-07 08:15:00 +0000
@@ -56,11 +56,11 @@
                 return no_lower() && no_upper();
             }
 
-            bool isSound() {
+            bool isSound() const {
                 return _lower <= _upper;
             }
 
-            bool contains(uint32_t id){
+            bool contains(uint32_t id) const {
                 return _lower <= id && id <= _upper;
             }
 
@@ -69,7 +69,7 @@
                 _lower = min();
             }
 
-            uint32_t size(){
+            uint32_t size() const {
                 return 1 + _upper - _lower;
             }
 
@@ -99,6 +99,10 @@
                         );
             }
 
+            bool intersects(const range_t& other) const {
+                return _lower <= other._upper  && other._lower <= _upper;
+            }
+            
             range_t& operator&=(const range_t& other) {
                 _lower = std::max(_lower, other._lower);
                 _upper = std::min(_upper, other._upper);

=== modified file 'include/PetriEngine/options.h'
--- include/PetriEngine/options.h	2021-04-14 11:51:52 +0000
+++ include/PetriEngine/options.h	2021-07-07 08:15:00 +0000
@@ -41,13 +41,14 @@
     bool printstatistics = true;
     std::set<size_t> querynumbers;
     PetriEngine::Reachability::Strategy strategy = PetriEngine::Reachability::DEFAULT;
-    int queryReductionTimeout = 30, intervalTimeout = 10, lpsolveTimeout = 10;
+    int queryReductionTimeout = 30, intervalTimeout = 10, partitionTimeout = 5, lpsolveTimeout = 10;
     TraceLevel trace = TraceLevel::None;
     bool use_query_reductions = true;
     uint32_t siphontrapTimeout = 0;
     uint32_t siphonDepth = 0;
     uint32_t cores = 1;
     std::string output_stats;
+    bool doVerification = true;
 
     TemporalLogic logic = TemporalLogic::CTL;
     bool noreach = false;
@@ -68,12 +69,15 @@
 
     std::string query_out_file;
     std::string model_out_file;
+    std::string unfolded_out_file;
+    std::string unfold_query_out_file;
 
     
     //CPN Specific options
     bool cpnOverApprox = false;
     bool computeCFP = true;
     bool computePartition = true;
+    bool symmetricVariables = true;
     bool isCPN = false;
     uint32_t seed_offset = 0;
     int max_intervals = 250; //0 disabled

=== modified file 'include/PetriParse/PNMLParser.h'
--- include/PetriParse/PNMLParser.h	2021-04-22 12:43:03 +0000
+++ include/PetriParse/PNMLParser.h	2021-07-07 08:15:00 +0000
@@ -39,6 +39,7 @@
         std::string source,
         target;
         int weight;
+        bool inhib;
         PetriEngine::Colored::ArcExpression_ptr expr;
     };
     typedef std::vector<Arc> ArcList;
@@ -58,8 +59,8 @@
     };
     typedef std::unordered_map<std::string, NodeName> NodeNameMap;
     
-    typedef std::unordered_map<std::string, PetriEngine::Colored::ColorType*> ColorTypeMap;
-    typedef std::unordered_map<std::string, PetriEngine::Colored::Variable*> VariableMap;
+    typedef std::unordered_map<std::string, const PetriEngine::Colored::ColorType*> ColorTypeMap;
+    typedef std::unordered_map<std::string, const PetriEngine::Colored::Variable*> VariableMap;
 
 public:
 
@@ -89,7 +90,7 @@
     PetriEngine::Colored::GuardExpression_ptr parseGuardExpression(rapidxml::xml_node<>* element, bool notFlag);
     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);
+    const PetriEngine::Colored::ColorType* parseUserSort(rapidxml::xml_node<>* element);
     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);
@@ -106,7 +107,6 @@
     PetriEngine::AbstractPetriNetBuilder* builder;
     NodeNameMap id2name;
     ArcList arcs;
-    ArcList inhibarcs;
     TransitionList transitions;
     ColorTypeMap colorTypes;
     VariableMap variables;

=== modified file 'src/LTL/LTLMain.cpp'
--- src/LTL/LTLMain.cpp	2021-06-06 19:08:53 +0000
+++ src/LTL/LTLMain.cpp	2021-07-07 08:15:00 +0000
@@ -190,13 +190,11 @@
                 assert(false);
                 std::cerr << "Error: cannot LTL verify with algorithm None";
         }
-        bool answer = result.satisfied ^ negate_answer;
         std::cout << "FORMULA " << queryName
-                  << (answer ? " TRUE" : " FALSE") << " TECHNIQUES EXPLICIT "
+                  << (result.satisfied ^ negate_answer ? " TRUE" : " FALSE") << " TECHNIQUES EXPLICIT "
                   << LTL::to_string(options.ltlalgorithm)
                   << (result.is_weak ? " WEAK_SKIP" : "")
                   << std::endl;
-        std::cout << "Query is" << (answer ? "" : " NOT") << " satisfied." << std::endl;
 #ifdef DEBUG_EXPLORED_STATES
         std::cout << "FORMULA " << queryName << " STATS EXPLORED " << result.explored_states << std::endl;
 #endif

=== modified file 'src/PetriEngine/Colored/BindingGenerator.cpp'
--- src/PetriEngine/Colored/BindingGenerator.cpp	2021-04-14 10:41:18 +0000
+++ src/PetriEngine/Colored/BindingGenerator.cpp	2021-07-07 08:15:00 +0000
@@ -38,20 +38,14 @@
         _generator->nextBinding();
         if (_generator->isInitial()) _generator = nullptr;
         return *this;
-    }
-
-    const Colored::ExpressionContext::BindingMap NaiveBindingGenerator::Iterator::operator++(int) {
-        auto prev = _generator->currentBinding();
-        ++*this;
-        return prev;
-    }
-
-    Colored::ExpressionContext::BindingMap& NaiveBindingGenerator::Iterator::operator*() {
+    }   
+
+    const Colored::BindingMap& NaiveBindingGenerator::Iterator::operator*() const {
         return _generator->currentBinding();
     }
 
-    NaiveBindingGenerator::NaiveBindingGenerator(Colored::Transition& transition,
-            ColorTypeMap& colorTypes)
+    NaiveBindingGenerator::NaiveBindingGenerator(const Colored::Transition& transition,
+            Colored::ColorTypeMap& colorTypes)
         : _colorTypes(colorTypes)
     {
         _expr = transition.guard;
@@ -59,15 +53,15 @@
         if (_expr != nullptr) {
             _expr->getVariables(variables);
         }
-        for (auto arc : transition.input_arcs) {
-            assert(arc.expr != nullptr);
-            arc.expr->getVariables(variables);
-        }
-        for (auto arc : transition.output_arcs) {
-            assert(arc.expr != nullptr);
-            arc.expr->getVariables(variables);
-        }
-        for (auto var : variables) {
+        for (const auto& arc : transition.input_arcs) {
+            assert(arc.expr != nullptr);
+            arc.expr->getVariables(variables);
+        }
+        for (const auto& arc : transition.output_arcs) {
+            assert(arc.expr != nullptr);
+            arc.expr->getVariables(variables);
+        }
+        for (const auto& var : variables) {
             _bindings[var] = &var->colorType->operator[](0);
         }
         
@@ -75,21 +69,21 @@
             nextBinding();
     }
 
-    bool NaiveBindingGenerator::eval() {
+    bool NaiveBindingGenerator::eval() const {
         if (_expr == nullptr)
             return true;
         Colored::EquivalenceVec placePartition;
 
-        Colored::ExpressionContext context {_bindings, _colorTypes, placePartition};
+        const Colored::ExpressionContext &context {_bindings, _colorTypes, placePartition};
         return _expr->eval(context);
     }
 
-    Colored::ExpressionContext::BindingMap& NaiveBindingGenerator::nextBinding() {
+    const Colored::BindingMap& NaiveBindingGenerator::nextBinding() {
         bool test = false;
         while (!test) {
-            for (auto& _binding : _bindings) {
-                _binding.second = &_binding.second->operator++();
-                if (_binding.second->getId() != 0) {
+            for (auto& binding : _bindings) {
+                binding.second = &binding.second->operator++();
+                if (binding.second->getId() != 0) {
                     break;
                 }
             }
@@ -102,7 +96,7 @@
         return _bindings;
     }
 
-    Colored::ExpressionContext::BindingMap& NaiveBindingGenerator::currentBinding() {
+    const Colored::BindingMap& NaiveBindingGenerator::currentBinding() const {
         return _bindings;
     }
 
@@ -122,9 +116,8 @@
     }
 
 
-
-        FixpointBindingGenerator::Iterator::Iterator(FixpointBindingGenerator* generator)
-            : _generator(generator)
+    FixpointBindingGenerator::Iterator::Iterator(FixpointBindingGenerator* generator)
+        : _generator(generator)
     {
     }
 
@@ -148,94 +141,143 @@
         return *this;
     }
 
-    const Colored::ExpressionContext::BindingMap FixpointBindingGenerator::Iterator::operator++(int) {
-        auto prev = _generator->currentBinding();
-        ++*this;
-        return prev;
-    }
-
-    Colored::ExpressionContext::BindingMap& FixpointBindingGenerator::Iterator::operator*() {
+    const Colored::BindingMap& FixpointBindingGenerator::Iterator::operator*() const {
         return _generator->currentBinding();
     }
 
-    FixpointBindingGenerator::FixpointBindingGenerator(Colored::Transition& transition,
-        ColorTypeMap& colorTypes)
-    : _colorTypes(colorTypes), _transition(transition)
+    FixpointBindingGenerator::FixpointBindingGenerator(const Colored::Transition& transition,
+        const Colored::ColorTypeMap& colorTypes,  const std::vector<std::set<const Colored::Variable *>>& symmetric_vars)
+    : _expr(transition.guard), _colorTypes(colorTypes), _transition(transition), _symmetric_vars(symmetric_vars)
     {
         _isDone = false;
         _noValidBindings = false;
         _nextIndex = 0;
-        _expr = _transition.guard;
 
         std::set<const Colored::Variable*> variables;
         if (_expr != nullptr) {
             _expr->getVariables(variables);
         }
-        for (auto arc : _transition.input_arcs) {
-            assert(arc.expr != nullptr);
-            arc.expr->getVariables(variables);
-        }
-        for (auto arc : _transition.output_arcs) {
-            assert(arc.expr != nullptr);
-            arc.expr->getVariables(variables);
+        for (const auto &arc : _transition.input_arcs) {
+            assert(arc.expr != nullptr);
+            arc.expr->getVariables(variables);
+        }
+        for (const auto &arc : _transition.output_arcs) {
+            assert(arc.expr != nullptr);
+            arc.expr->getVariables(variables);
+        }
+
+        for(const auto &varSet : symmetric_vars){
+            std::vector<std::vector<uint32_t>> combinations;
+            std::vector<uint32_t> temp;
+            generateCombinations(varSet.begin().operator*()->colorType->size()-1, varSet.size(), combinations, temp);
+            _symmetric_var_combinations.push_back(combinations);
         }       
         
         
-        for (auto var : variables) {
-            if(_transition.variableMaps.empty() || _transition.variableMaps[_nextIndex][var]._intervals.empty()){
+        for (auto* var : variables) {
+            if(_transition.variableMaps.empty() || _transition.variableMaps[_nextIndex].find(var)->second.empty()){
                 _noValidBindings = true;
                 break;
             }
-            auto color = var->colorType->getColor(_transition.variableMaps[_nextIndex][var].getFirst().getLowerIds());
+            auto color = var->colorType->getColor(_transition.variableMaps[_nextIndex].find(var)->second.front().getLowerIds());
             _bindings[var] = color;
         }
+        assignSymmetricVars();
         
         if (!_noValidBindings && !eval())
             nextBinding();
     }
 
-
-    bool FixpointBindingGenerator::eval() {
+    bool FixpointBindingGenerator::assignSymmetricVars(){
+        if(_currentOuterId < _symmetric_vars.size()){
+            if(_currentInnerId >= _symmetric_var_combinations[_currentOuterId].size()){
+                _currentOuterId++;
+                _currentInnerId = 0;
+            }
+        } else {
+            return false;
+        }
+        uint32_t j = 0;
+        for(auto var : _symmetric_vars[_currentOuterId]){
+            _bindings[var] = &var->colorType->operator[](_symmetric_var_combinations[_currentOuterId][_currentInnerId][j]);
+            j++;
+        }
+        _currentInnerId++;
+        if(_currentInnerId >= _symmetric_var_combinations[_currentOuterId].size()){
+            if(_currentOuterId < _symmetric_vars.size()){
+                _currentOuterId++;
+                _currentInnerId = 0;
+            } else {
+                return false;
+            }
+        }
+        return true;        
+    }
+
+
+    bool FixpointBindingGenerator::eval() const{
         if (_expr == nullptr)
             return true;
 
         Colored::EquivalenceVec placePartition;
-        Colored::ExpressionContext context {_bindings, _colorTypes, placePartition};
+        const Colored::ExpressionContext &context {_bindings, _colorTypes, placePartition};
         return _expr->eval(context);
     }
 
-    Colored::ExpressionContext::BindingMap& FixpointBindingGenerator::nextBinding() {
+    const Colored::BindingMap& FixpointBindingGenerator::nextBinding() {
         bool test = false;
         while (!test) {
             bool next = true;
 
-            for (auto& _binding : _bindings) {               
-                auto varInterval = _transition.variableMaps[_nextIndex][_binding.first];                
-                std::vector<uint32_t> colorIds;
-                _binding.second->getTupleId(&colorIds);
-                auto nextIntervalBinding = varInterval.isRangeEnd(colorIds);
-
-                if (nextIntervalBinding.size() == 0){                    
-                    _binding.second = &_binding.second->operator++();
-                    next = false;
-                    break;                    
-                } else {
-                    _binding.second = _binding.second->getColorType()->getColor(nextIntervalBinding.getLowerIds());
-                    
-                    if(!nextIntervalBinding.equals(varInterval.getFirst())){
+            if(assignSymmetricVars()){
+                next = false;
+            } else {
+                for (auto& binding : _bindings) {
+                    bool varSymmetric = false;
+                    for(auto& set : _symmetric_vars){
+                        if(set.find(binding.first) != set.end()){
+                            varSymmetric = true;
+                            break;
+                        }
+                    }
+                    if(varSymmetric){
+                        continue;
+                    }
+
+                    const auto &varInterval = _transition.variableMaps[_nextIndex].find(binding.first)->second;                
+                    std::vector<uint32_t> colorIds;
+                    binding.second->getTupleId(colorIds);
+                    const auto &nextIntervalBinding = varInterval.isRangeEnd(colorIds);
+
+                    if (nextIntervalBinding.size() == 0){                    
+                        binding.second = &binding.second->operator++();
+                        _currentInnerId = 0;
+                        _currentOuterId = 0;
+                        assignSymmetricVars();
                         next = false;
-                        break;
-                    }              
+                        break;                    
+                    } else {
+                        binding.second = binding.second->getColorType()->getColor(nextIntervalBinding.getLowerIds());
+                        _currentInnerId = 0;
+                        _currentOuterId = 0;
+                        assignSymmetricVars();
+                        if(!nextIntervalBinding.equals(varInterval.front())){
+                            next = false;
+                            
+                            break;
+                        }              
+                    }
                 }
-            }
+            }            
+
             if(next){
                 _nextIndex++;
                 if(isInitial()){
                     _isDone = true;
                     break;
                 }
-                for(auto& _binding : _bindings){
-                    _binding.second =  _binding.second->getColorType()->getColor(_transition.variableMaps[_nextIndex][_binding.first].getFirst().getLowerIds());
+                for(auto& binding : _bindings){
+                    binding.second =  binding.second->getColorType()->getColor(_transition.variableMaps[_nextIndex].find(binding.first)->second.front().getLowerIds());
                 }
             }                 
             test = eval();
@@ -244,11 +286,27 @@
         return _bindings;
     }
 
-    Colored::ExpressionContext::BindingMap& FixpointBindingGenerator::currentBinding() {
+    void FixpointBindingGenerator::generateCombinations(
+            uint32_t options,
+            uint32_t samples,
+            std::vector<std::vector<uint32_t>> &result,
+            std::vector<uint32_t> &current) const {
+        if (samples == 0) {
+            result.push_back(current);
+            return;
+        }
+        for (uint32_t i = 0; i <= options; i++) {
+            current.push_back(i);
+            generateCombinations(i, samples - 1, result, current);
+            current.pop_back();
+        }
+    }
+
+    const Colored::BindingMap& FixpointBindingGenerator::currentBinding() const {
         return _bindings;
     }
 
-    bool FixpointBindingGenerator::isInitial() const{        
+    bool FixpointBindingGenerator::isInitial() const {
         return _nextIndex >= _transition.variableMaps.size();
     }
 

=== 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-07-07 08:15:00 +0000
@@ -6,5 +6,7 @@
 BindingGenerator.cpp
 PartitionBuilder.cpp
 EquivalenceClass.cpp
-GuardRestrictor.cpp)
+GuardRestrictor.cpp
+IntervalGenerator.cpp
+EquivalenceVec.cpp)
 add_dependencies(Colored rapidxml-ext ptrie-ext glpk-ext)

=== modified file 'src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp'
--- src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-04-30 17:01:57 +0000
+++ src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-07-07 08:15:00 +0000
@@ -19,15 +19,26 @@
 
 #include "PetriEngine/Colored/ColoredPetriNetBuilder.h"
 #include <chrono>
-
+#include <tuple>
+using std::get;
 namespace PetriEngine {
     ColoredPetriNetBuilder::ColoredPetriNetBuilder() {
     }
 
-    ColoredPetriNetBuilder::ColoredPetriNetBuilder(const ColoredPetriNetBuilder& orig) {
+    ColoredPetriNetBuilder::ColoredPetriNetBuilder(const ColoredPetriNetBuilder& orig) 
+    : _placenames(orig._placenames), _transitionnames(orig._transitionnames),
+       _places(orig._places), _transitions(orig._transitions)
+    {
     }
 
     ColoredPetriNetBuilder::~ColoredPetriNetBuilder() {
+        // cleaning up colors
+        for(auto& e : _colors)
+        {
+            if(e.second != Colored::ColorType::dotInstance())
+                delete e.second;
+        }
+        _colors.clear();
     }
 
     void ColoredPetriNetBuilder::addPlace(const std::string& name, int tokens, double x, double y) {
@@ -36,7 +47,7 @@
         }
     }
 
-    void ColoredPetriNetBuilder::addPlace(const std::string& name, Colored::ColorType* type, Colored::Multiset&& tokens, double x, double y) {
+    void ColoredPetriNetBuilder::addPlace(const std::string& name, const Colored::ColorType* type, Colored::Multiset&& tokens, double x, double y) {
         if(_placenames.count(name) == 0)
         {
             uint32_t next = _placenames.size();
@@ -48,23 +59,33 @@
                 _placeFixpointQueue.emplace_back(next);
             }
 
-            Colored::intervalTuple_t placeConstraints;
+            Colored::interval_vector_t placeConstraints;
             Colored::ColorFixpoint colorFixpoint = {placeConstraints, !tokens.empty()};
+            uint32_t colorCounter = 0;
+            
+            if(tokens.size() == type->size()) {
+                for(const auto& colorPair : tokens){
+                    if(colorPair.second > 0){
+                        colorCounter++;
+                    } else {
+                        break;
+                    }
+                }
+            }            
 
-            if(tokens.size() == type->size()){
+            if(colorCounter == type->size()){
                 colorFixpoint.constraints.addInterval(type->getFullInterval());
             } else {
-                uint32_t index = 0;
-                for (auto colorPair : tokens) {
+                for (const auto& colorPair : tokens) {
                     Colored::interval_t tokenConstraints;
-                    colorPair.first->getColorConstraints(&tokenConstraints, &index);
+                    uint32_t index = 0;
+                    colorPair.first->getColorConstraints(tokenConstraints, index);
 
                     colorFixpoint.constraints.addInterval(tokenConstraints);
-                    index = 0;
                 }
             }
          
-            _placeColorFixpoints.push_back(colorFixpoint);            
+            _placeColorFixpoints.push_back(colorFixpoint);    
         }
     }
 
@@ -89,8 +110,8 @@
         }
     }
 
-    void ColoredPetriNetBuilder::addInputArc(const std::string& place, const std::string& transition, const Colored::ArcExpression_ptr& expr) {
-        addArc(place, transition, expr, true);
+    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::addOutputArc(const std::string& transition, const std::string& place, int weight) {
@@ -100,10 +121,10 @@
     }
 
     void ColoredPetriNetBuilder::addOutputArc(const std::string& transition, const std::string& place, const Colored::ArcExpression_ptr& expr) {
-        addArc(place, transition, expr, false);
+        addArc(place, transition, expr, false, false, 1);
     }
 
-    void ColoredPetriNetBuilder::addArc(const std::string& place, const std::string& transition, const Colored::ArcExpression_ptr& expr, bool input) {
+    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;
@@ -125,46 +146,173 @@
         Colored::Arc arc;
         arc.place = p;
         arc.transition = t;
-        assert(expr != nullptr);
+        _places[p].inhibitor |= inhibitor;
+        if(!inhibitor)
+            assert(expr != nullptr);
         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));
+        arc.weight = weight;
+        if(inhibitor){
+            _inhibitorArcs.push_back(std::move(arc));
+        } else {
+            input? _transitions[t].input_arcs.push_back(std::move(arc)): _transitions[t].output_arcs.push_back(std::move(arc));
+        }
         
     }
 
-    void ColoredPetriNetBuilder::addColorType(const std::string& id, Colored::ColorType* type) {
+    void ColoredPetriNetBuilder::addColorType(const std::string& id, const Colored::ColorType* type) {
         _colors[id] = type;
     }
 
     void ColoredPetriNetBuilder::sort() {
     }
 
+    //------------------- Symmetric Variables --------------------//
+    void ColoredPetriNetBuilder::computeSymmetricVariables(){
+        if(_isColored){
+            for(uint32_t transitionId = 0; transitionId < _transitions.size(); transitionId++){
+                const Colored::Transition &transition = _transitions[transitionId];
+                if(transition.guard){
+                    continue;
+                    //the variables cannot appear on the guard
+                }
+                
+                for(const auto &inArc : transition.input_arcs){
+                    std::set<const Colored::Variable*> inArcVars;
+                    std::vector<uint32_t> numbers;
+
+                    //Application of symmetric variables for partitioned places is currently unhandled
+                    if(_partitionComputed && !_partition[inArc.place].isDiagonal()){
+                        continue;
+                    }
+                    
+                    //the expressions is eligible if it is an addexpression that contains only 
+                    //numberOfExpressions with the same number
+                    bool isEligible = inArc.expr->isEligibleForSymmetry(numbers);
+
+                    if(isEligible && numbers.size() > 1){
+                        inArc.expr->getVariables(inArcVars);
+                        //It cannot be symmetric with anything if there is only one variable
+                        if(inArcVars.size() < 2){
+                            continue;
+                        }
+                        //The variables may appear only on one input arc and one output arc
+                        checkSymmetricVarsInArcs(transition, inArc, inArcVars, isEligible);
+                        
+                        
+                        //All the variables have to appear on exactly one output arc and nowhere else
+                        checkSymmetricVarsOutArcs(transition, inArcVars, isEligible);                    
+                    }else{
+                        isEligible = false;
+                    }
+                    if(isEligible){
+                        symmetric_var_map[transitionId].emplace_back(inArcVars);
+                    }
+                }
+            }
+        }
+    }
+
+    void ColoredPetriNetBuilder::checkSymmetricVarsInArcs(const Colored::Transition &transition, const Colored::Arc &inArc, const std::set<const Colored::Variable*> &inArcVars, bool &isEligible ) const{
+        for(auto& otherInArc : transition.input_arcs){
+            if(inArc.place == otherInArc.place){
+                continue;
+            }
+            std::set<const Colored::Variable*> otherArcVars;
+            otherInArc.expr->getVariables(otherArcVars);
+            for(auto* var : inArcVars){
+                if(otherArcVars.find(var) != otherArcVars.end()){
+                    isEligible = false;
+                    break;
+                }
+            }
+        }
+    }
+
+    void ColoredPetriNetBuilder::checkSymmetricVarsOutArcs(const Colored::Transition &transition, const std::set<const Colored::Variable*> &inArcVars, bool &isEligible) const{
+        uint32_t numArcs = 0;
+        bool foundSomeVars = false;
+        for(auto& outputArc : transition.output_arcs){
+            bool foundArc = true;
+            std::set<const Colored::Variable*> otherArcVars;
+            outputArc.expr->getVariables(otherArcVars);
+            for(auto* var : inArcVars){
+                if(otherArcVars.find(var) == otherArcVars.end()){
+                    foundArc = false;
+                } else{
+                    foundSomeVars = true;
+                } 
+            }
+            if(foundArc){
+                //Application of symmetric variables for partitioned places is currently unhandled
+                if(_partitionComputed && !_partition.find(outputArc.place)->second.isDiagonal()){
+                    isEligible = false;
+                    break;
+                }
+                numArcs++;
+                //All vars were present
+                foundSomeVars = false;
+            }
+            //If some vars are present the vars are not eligible
+            if(foundSomeVars){
+                isEligible = false;
+                break;
+            }  
+        }
+
+        if(numArcs != 1){
+            isEligible = false;
+        }
+    }
+
+    void ColoredPetriNetBuilder::printSymmetricVariables() const {
+        for(uint32_t transitionId = 0; transitionId < _transitions.size(); transitionId++){
+            const auto &transition = _transitions[transitionId];
+            if ( symmetric_var_map.find(transitionId) == symmetric_var_map.end() ) {
+                std::cout << "Transition " << transition.name << " has no symmetric variables" << std::endl;
+            }else{
+                std::cout << "Transition " << transition.name << " has symmetric variables: " << std::endl;
+                for(const auto &set : symmetric_var_map.find(transitionId)->second){
+                    std::string toPrint = "SET: ";
+                    for(auto* variable : set){
+                        toPrint += variable->name + ", ";
+                    }
+                    std::cout << toPrint << std::endl;
+                }
+            }
+        }
+    }
+
+
     //----------------------- Partitioning -----------------------//
 
-    void ColoredPetriNetBuilder::computePartition(){
-        auto partitionStart = std::chrono::high_resolution_clock::now();
-        Colored::PartitionBuilder pBuilder = _fixpointDone? Colored::PartitionBuilder(&_transitions, &_places, &_placePostTransitionMap, &_placePreTransitionMap, &_placeColorFixpoints) : Colored::PartitionBuilder(&_transitions, &_places, &_placePostTransitionMap, &_placePreTransitionMap);
-        
-        pBuilder.partitionNet();
-        //pBuilder.printPartion();
-        _partition = pBuilder.getPartition();
-        pBuilder.assignColorMap(_partition);
-        _partitionComputed = true;
-        auto partitionEnd = std::chrono::high_resolution_clock::now();
-        _partitionTimer = (std::chrono::duration_cast<std::chrono::microseconds>(partitionEnd - partitionStart).count())*0.000001;
+    void ColoredPetriNetBuilder::computePartition(int32_t timeout){
+        if(_isColored){
+            auto partitionStart = std::chrono::high_resolution_clock::now();
+            Colored::PartitionBuilder pBuilder = _fixpointDone? Colored::PartitionBuilder(_transitions, _places, _placePostTransitionMap, _placePreTransitionMap, &_placeColorFixpoints) : Colored::PartitionBuilder(_transitions, _places, _placePostTransitionMap, _placePreTransitionMap);
+            
+            if(pBuilder.partitionNet(timeout)){
+                //pBuilder.printPartion();
+                _partition = pBuilder.getPartition();
+                pBuilder.assignColorMap(_partition);
+                _partitionComputed = true;
+            }         
+            auto partitionEnd = std::chrono::high_resolution_clock::now();
+            _partitionTimer = (std::chrono::duration_cast<std::chrono::microseconds>(partitionEnd - partitionStart).count())*0.000001;
+        }        
     }
 
     //----------------------- Color fixpoint -----------------------//
 
-    void ColoredPetriNetBuilder::printPlaceTable() {
-        for (auto place: _places) {
-            auto placeID = _placenames[place.name];
-            auto placeColorFixpoint = _placeColorFixpoints[placeID];
+    void ColoredPetriNetBuilder::printPlaceTable() const{
+        for (const auto &place: _places) {
+            const auto &placeID = _placenames.find(place.name)->second;
+            const auto &placeColorFixpoint = _placeColorFixpoints[placeID];
             std::cout << "Place: " << place.name << " in queue: " << placeColorFixpoint.inQueue  << " with colortype " << place.type->getName() << std::endl;
 
-            for(auto fixpointPair : placeColorFixpoint.constraints._intervals) {
+            for(const auto &fixpointPair : placeColorFixpoint.constraints) {
                 std::cout << "[";
-                for(auto range : fixpointPair._ranges) {
+                for(const auto &range : fixpointPair._ranges) {
                     std::cout << range._lower << "-" << range._upper << ", ";
                 }
                 std::cout << "]"<< std::endl;                    
@@ -172,61 +320,62 @@
             std::cout << std::endl;
         }
     }
-
-
-      
+ 
     void ColoredPetriNetBuilder::computePlaceColorFixpoint(uint32_t maxIntervals, uint32_t maxIntervalsReduced, int32_t timeout) {
-        //Start timers for timing color fixpoint creation and max interval reduction steps
-        auto start = std::chrono::high_resolution_clock::now();
-        std::chrono::_V2::system_clock::time_point end = std::chrono::high_resolution_clock::now();
-        auto reduceTimer = std::chrono::high_resolution_clock::now();        
-        while(!_placeFixpointQueue.empty()){
-            //Reduce max interval once timeout passes
-            if(maxIntervals > maxIntervalsReduced && timeout > 0 && std::chrono::duration_cast<std::chrono::seconds>(end - reduceTimer).count() >= timeout){
-                maxIntervals = maxIntervalsReduced; 
-            }
+        if(_isColored){
+            //Start timers for timing color fixpoint creation and max interval reduction steps
+            auto start = std::chrono::high_resolution_clock::now();
+            auto end = std::chrono::high_resolution_clock::now();
+            auto reduceTimer = std::chrono::high_resolution_clock::now();        
+            while(!_placeFixpointQueue.empty()){
+                //Reduce max interval once timeout passes
+                if(maxIntervals > maxIntervalsReduced && timeout > 0 && std::chrono::duration_cast<std::chrono::seconds>(end - reduceTimer).count() >= timeout){
+                    maxIntervals = maxIntervalsReduced; 
+                }
+