Merge lp:~verifydtapn-contributers/verifydtapn/ArithmeticQueries into lp:verifydtapn

[Peter Gjøl Jensen]

Branch contains changes implementing arithmetic operations in verifydtapn.
A lot of the changes are generated code and the remaining should be fairly straightforward.

[Jiri Srba (srba)]

Tested and it works.

review: Approve

[Jakob Taankvist (jakob-taankvist)]

I looked over the code, and I think it looks as expected.

review: Approve

[Mathias Grund Sørensen (mathias.grund)]

Looks as expected

review: Approve (code)

=== modified file 'src/Core/QueryParser/AST.cpp'
--- src/Core/QueryParser/AST.cpp	2013-08-09 21:47:22 +0000
+++ src/Core/QueryParser/AST.cpp	2014-03-20 14:00:01 +0000
@@ -47,7 +47,7 @@
 		{
 			return new AndExpression(*this);
 		}
-
+                
 		void AndExpression::accept(Visitor& visitor, Result& context) const
 		{
 			visitor.visit(*this, context);
@@ -58,21 +58,71 @@
 			return new OrExpression(*this);
 		}
 
-		void OrExpression::accept(Visitor& visitor, Result& context) const
-		{
-			visitor.visit(*this, context);
-		}
-
-		ParExpression* ParExpression::clone() const
-		{
-			return new ParExpression(*this);
-		}
-
-		void ParExpression::accept(Visitor& visitor, Result& context) const
-		{
-			visitor.visit(*this, context);
-		}
-
+                void OrExpression::accept(Visitor& visitor, Result& context) const
+		{
+			visitor.visit(*this, context);
+		}
+                
+		void PlusExpression::accept(Visitor& visitor, Result& context) const
+		{
+			visitor.visit(*this, context);
+		}
+
+                PlusExpression* PlusExpression::clone() const
+		{
+			return new PlusExpression(*this);
+		}
+                
+                void SubtractExpression::accept(Visitor& visitor, Result& context) const
+		{
+			visitor.visit(*this, context);
+		}
+
+                SubtractExpression* SubtractExpression::clone() const
+		{
+			return new SubtractExpression(*this);
+		}
+                
+                void MinusExpression::accept(Visitor& visitor, Result& context) const
+		{
+			visitor.visit(*this, context);
+		}
+
+                MinusExpression* MinusExpression::clone() const
+		{
+			return new MinusExpression(*this);
+		}
+
+                void MultiplyExpression::accept(Visitor& visitor, Result& context) const
+		{
+			visitor.visit(*this, context);
+		}
+
+                MultiplyExpression* MultiplyExpression::clone() const
+		{
+			return new MultiplyExpression(*this);
+		}
+                
+                void NumberExpression::accept(Visitor& visitor, Result& context) const
+		{
+			visitor.visit(*this, context);
+		}
+
+                NumberExpression* NumberExpression::clone() const
+		{
+			return new NumberExpression(*this);
+		} 
+                
+                void IdentifierExpression::accept(Visitor& visitor, Result& context) const
+		{
+			visitor.visit(*this, context);
+		}
+
+                IdentifierExpression* IdentifierExpression::clone() const
+		{
+			return new IdentifierExpression(*this);
+		} 
+                
 		Query* Query::clone() const
 		{
 			return new Query(*this);

=== modified file 'src/Core/QueryParser/AST.hpp'
--- src/Core/QueryParser/AST.hpp	2013-10-19 19:33:33 +0000
+++ src/Core/QueryParser/AST.hpp	2014-03-20 14:00:01 +0000
@@ -75,30 +75,31 @@
 		class AtomicProposition : public Expression
 		{
 		public:
-			AtomicProposition(int placeIndex, std::string* op, int n) : place(placeIndex), op(op->begin(), op->end()), n(n){};
-			AtomicProposition(const AtomicProposition& other) : place(other.place), op(other.op), n(other.n) { };
+			AtomicProposition(ArithmeticExpression* left, std::string* op,ArithmeticExpression* right) : left(left), op(op->begin(), op->end()), right(right){};
+			AtomicProposition(const AtomicProposition& other) : left(other.left), op(other.op), right(other.right) { };
 			AtomicProposition& operator=(const AtomicProposition& other)
 			{
 				if(&other != this){
-					place = other.place;
+					left = other.left;
 					op = other.op;
-					n = other.n;
+					right = other.right;
 				}
 				return *this;
 			}
 
 			virtual ~AtomicProposition() { };
 
+                        ArithmeticExpression& getLeft() const {return *left;};
+                        ArithmeticExpression& getRight() const {return *right;};
+                        std::string getOperator() const {return op;};
+                         
 			virtual AtomicProposition* clone() const;
 			virtual void accept(Visitor& visitor, Result& context) const;
 
-			const int getPlace() const { return place; }
-			const std::string& getOperator() const { return op; }
-			int getNumberOfTokens() const { return n; }
 		private:
-			int place;
+			ArithmeticExpression* left;
 			std::string op;
-			int n;
+			ArithmeticExpression* right;
 		};
 
 		class AndExpression : public Expression
@@ -167,34 +168,198 @@
 			Expression* left;
 			Expression* right;
 		};
-
-		class ParExpression : public Expression
-		{
-		public:
-			explicit ParExpression(Expression* expr) : expr(expr) { };
-			ParExpression(const ParExpression& other) : expr(other.expr->clone()) { };
-			ParExpression& operator=(const ParExpression& other)
-			{
-				if(&other != this){
-					delete expr;
-					expr = other.expr->clone();
-				}
-
-				return *this;
-			}
-
-			virtual ~ParExpression(){
-				if( expr ) delete expr;
-			};
-
-			virtual ParExpression* clone() const;
-			virtual void accept(Visitor& visitor, Result& context) const;
-
-			const Expression& getChild() const { return *expr; }
-		private:
-			Expression* expr;
-		};
-
+                
+                class ArithmeticExpression : public Visitable
+                {
+                    public:
+			virtual ~ArithmeticExpression() { };
+			virtual ArithmeticExpression* clone() const = 0;
+                };
+
+                class OperationExpression : public ArithmeticExpression {
+                protected:
+
+                    OperationExpression(ArithmeticExpression* left, ArithmeticExpression* right) : left(left), right(right) {
+                    };
+
+                    OperationExpression(const OperationExpression& other) : left(other.left), right(other.right) {
+                    };
+
+                    OperationExpression& operator=(const OperationExpression& other) {
+                        if (&other != this) {
+                            delete left;
+                            left = other.left;
+                            delete right;
+                            right = other.right;
+                        }
+                        return *this;
+                    }
+                    
+                    virtual ~OperationExpression() {
+                    };
+                    
+                public:
+                    ArithmeticExpression& getLeft() const {return *left;};
+                    ArithmeticExpression& getRight() const {return *right;};
+                    
+                protected:
+                    ArithmeticExpression* left;
+                    ArithmeticExpression* right;
+                };
+
+                class PlusExpression : public OperationExpression {
+                public:
+
+                    PlusExpression(ArithmeticExpression* left, ArithmeticExpression* right)
+                    : OperationExpression(left, right) {
+                    };
+
+                    PlusExpression(const PlusExpression& other)
+                    : OperationExpression(other) {
+                    };
+
+                    PlusExpression& operator=(const PlusExpression& other) {
+                        if (&other != this) {
+                            left = other.left;
+                            right = other.right;
+                        }
+                        return *this;
+                    }
+
+                    virtual ~PlusExpression() {
+                    };
+
+                    virtual PlusExpression* clone() const;
+                    virtual void accept(Visitor& visitor, Result& context) const;
+
+                };
+
+                class SubtractExpression : public OperationExpression {
+                public:
+
+                    SubtractExpression(ArithmeticExpression* left, ArithmeticExpression* right)
+                    : OperationExpression(left, right) {
+                    };
+
+                    SubtractExpression(const SubtractExpression& other)
+                    : OperationExpression(other) {
+                    };
+
+                    SubtractExpression& operator=(const SubtractExpression& other) {
+                        if (&other != this) {
+                            left = other.left;
+                            right = other.right;
+                        }
+                        return *this;
+                    }
+
+                    virtual ~SubtractExpression() {
+                    };
+
+                    virtual SubtractExpression* clone() const;
+                    virtual void accept(Visitor& visitor, Result& context) const;
+                };
+
+                class MinusExpression : public ArithmeticExpression {
+                public:
+                    MinusExpression(ArithmeticExpression* value) : value(value) {
+                    };
+
+                    MinusExpression(const MinusExpression& other)
+                    : value(other.value) {
+                    };
+
+                    MinusExpression& operator=(const MinusExpression& other) {
+                        if (&other != this) {
+                            value = other.value;
+                        }
+                        return *this;
+                    }
+
+                    ArithmeticExpression& getValue() const { return *value;};
+                    
+                    virtual ~MinusExpression() {
+                    };
+                    virtual MinusExpression* clone() const;
+                    virtual void accept(Visitor& visitor, Result& context) const;
+                private:
+                    ArithmeticExpression* value;
+                };
+
+                class MultiplyExpression : public OperationExpression {
+                public:
+
+                    MultiplyExpression(ArithmeticExpression* left, ArithmeticExpression* right)
+                    : OperationExpression(left, right) {
+                    };
+
+                    MultiplyExpression(const MultiplyExpression& other)
+                    : OperationExpression(other) {
+                    };
+
+                    MultiplyExpression& operator=(const MultiplyExpression& other) {
+                        if (&other != this) {
+                            left = other.left;
+                            right = other.right;
+                        }
+                        return *this;
+                    }
+
+                    virtual ~MultiplyExpression() {
+                    };
+                    virtual MultiplyExpression* clone() const;
+                    virtual void accept(Visitor& visitor, Result& context) const;
+                };
+
+                class NumberExpression : public ArithmeticExpression {
+                public:
+
+                    NumberExpression(int i) : value(i) {
+                    }
+
+                    NumberExpression(const NumberExpression& other) : value(other.value) {
+                    };
+
+                    NumberExpression& operator=(const NumberExpression& other) {
+                        value = other.value;
+                        return *this;
+                    };
+
+                    int getValue() const {return value;};
+                    
+                    virtual ~NumberExpression() {
+                    };
+                    virtual NumberExpression* clone() const;
+                    virtual void accept(Visitor& visitor, Result& context) const;
+                private:
+                    int value;
+                };
+
+                class IdentifierExpression : public ArithmeticExpression {
+                public:
+
+                    IdentifierExpression(int placeIndex) : place(placeIndex) {
+                    }
+
+                    IdentifierExpression(const IdentifierExpression& other) : place(other.place) {
+                    };
+
+                    IdentifierExpression& operator=(const IdentifierExpression& other) {
+                        place = other.place;
+                        return *this;
+                    };
+
+                    int getPlace() const { return place;};
+                    
+                    virtual ~IdentifierExpression() {
+                    };
+                    virtual IdentifierExpression* clone() const;
+                    virtual void accept(Visitor& visitor, Result& context) const;
+                private:
+                    int place;
+                };
+        
+                
 		enum Quantifier { EF, AG, EG, AF};
 
 		class Query : public Visitable

=== modified file 'src/Core/QueryParser/Generated/lexer.cpp'
--- src/Core/QueryParser/Generated/lexer.cpp	2013-08-28 19:51:15 +0000
+++ src/Core/QueryParser/Generated/lexer.cpp	2014-03-20 14:00:01 +0000
@@ -9,7 +9,7 @@
 #define FLEX_SCANNER
 #define YY_FLEX_MAJOR_VERSION 2
 #define YY_FLEX_MINOR_VERSION 5
-#define YY_FLEX_SUBMINOR_VERSION 35
+#define YY_FLEX_SUBMINOR_VERSION 37
 #if YY_FLEX_SUBMINOR_VERSION > 0
 #define FLEX_BETA
 #endif
@@ -47,7 +47,6 @@
 typedef uint16_t flex_uint16_t;
 typedef int32_t flex_int32_t;
 typedef uint32_t flex_uint32_t;
-typedef uint64_t flex_uint64_t;
 #else
 typedef signed char flex_int8_t;
 typedef short int flex_int16_t;
@@ -55,7 +54,6 @@
 typedef unsigned char flex_uint8_t; 
 typedef unsigned short int flex_uint16_t;
 typedef unsigned int flex_uint32_t;
-#endif /* ! C99 */
 
 /* Limits of integral types. */
 #ifndef INT8_MIN
@@ -86,6 +84,8 @@
 #define UINT32_MAX             (4294967295U)
 #endif
 
+#endif /* ! C99 */
+
 #endif /* ! FLEXINT_H */
 
 #ifdef __cplusplus
@@ -333,7 +333,7 @@
 
 /* Begin user sect3 */
 
-#define yywrap(n) 1
+#define yywrap() 1
 #define YY_SKIP_YYWRAP
 
 typedef unsigned char YY_CHAR;
@@ -359,13 +359,13 @@
  */
 #define YY_DO_BEFORE_ACTION \
 	(yytext_ptr) = yy_bp; \
-	yyleng = (yy_size_t) (yy_cp - yy_bp); \
+	yyleng = (size_t) (yy_cp - yy_bp); \
 	(yy_hold_char) = *yy_cp; \
 	*yy_cp = '\0'; \
 	(yy_c_buf_p) = yy_cp;
 
-#define YY_NUM_RULES 23
-#define YY_END_OF_BUFFER 24
+#define YY_NUM_RULES 26
+#define YY_END_OF_BUFFER 27
 /* This struct is not used in this scanner,
    but its presence is necessary. */
 struct yy_trans_info
@@ -373,14 +373,14 @@
 	flex_int32_t yy_verify;
 	flex_int32_t yy_nxt;
 	};
-static yyconst flex_int16_t yy_accept[58] =
+static yyconst flex_int16_t yy_accept[61] =
     {   0,
-        0,    0,   24,   23,    1,    2,   13,   23,   14,   15,
-        3,   16,   18,   21,   22,   22,   22,   22,   22,   22,
-       22,   23,   22,   22,    1,    2,    9,    3,   17,   19,
-       20,   22,   22,   22,   22,   22,    8,   22,    8,    6,
-        5,    4,    7,    9,   22,   22,   13,   22,   22,   22,
-       10,   22,   11,   22,   22,   12,    0
+        0,    0,   27,   26,    1,    2,   13,   26,   20,   21,
+       24,   22,   23,    3,   14,   16,   19,   25,   25,   25,
+       25,   25,   25,   25,   26,   25,   25,    1,    2,    9,
+        3,   15,   17,   18,   25,   25,   25,   25,   25,    8,
+       25,    8,    6,    5,    4,    7,    9,   25,   25,   13,
+       25,   25,   25,   10,   25,   11,   25,   25,   12,    0
     } ;
 
 static yyconst flex_int32_t yy_ec[256] =
@@ -389,16 +389,16 @@
         1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
         1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
         1,    2,    4,    1,    1,    1,    1,    5,    1,    6,
-        7,    1,    1,    1,    1,    1,    1,    8,    8,    8,
-        8,    8,    8,    8,    8,    8,    8,    1,    1,    9,
-       10,   11,    1,    1,   12,   13,   13,   13,   14,   15,
-       16,   13,   13,   13,   13,   13,   13,   13,   13,   13,
-       13,   13,   13,   13,   13,   13,   13,   13,   13,   13,
-        1,    1,    1,    1,   13,    1,   17,   13,   18,   19,
+        7,    8,    9,    1,   10,    1,    1,   11,   11,   11,
+       11,   11,   11,   11,   11,   11,   11,    1,    1,   12,
+       13,   14,    1,    1,   15,   16,   16,   16,   17,   18,
+       19,   16,   16,   16,   16,   16,   16,   16,   16,   16,
+       16,   16,   16,   16,   16,   16,   16,   16,   16,   16,
+        1,    1,    1,    1,   16,    1,   20,   16,   21,   22,
 
-       20,   21,   13,   13,   13,   13,   22,   23,   13,   24,
-       25,   13,   13,   26,   27,   28,   29,   13,   13,   13,
-       13,   13,    1,   30,    1,    1,    1,    1,    1,    1,
+       23,   24,   16,   16,   16,   16,   25,   26,   16,   27,
+       28,   16,   16,   29,   30,   31,   32,   16,   16,   16,
+       16,   16,    1,   33,    1,    1,    1,    1,    1,    1,
         1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
         1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
         1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
@@ -415,61 +415,66 @@
         1,    1,    1,    1,    1
     } ;
 
-static yyconst flex_int32_t yy_meta[31] =
-    {   0,
-        1,    1,    1,    1,    1,    1,    1,    2,    1,    1,
-        1,    2,    2,    2,    2,    2,    2,    2,    2,    2,
-        2,    2,    2,    2,    2,    2,    2,    2,    2,    1
-    } ;
-
-static yyconst flex_int16_t yy_base[59] =
-    {   0,
-        0,   19,   68,   69,   65,   63,   69,   60,   69,   69,
-       56,   53,   52,   51,    0,   36,   39,   41,   32,   30,
-       29,   24,   19,   21,   51,   49,   69,   43,   69,   69,
-       69,    0,   31,   32,   25,   19,    0,   17,   69,    0,
-        0,    0,    0,    0,   26,   17,    0,   23,   19,   21,
-        0,   15,    0,   21,   16,    0,   69,   30
-    } ;
-
-static yyconst flex_int16_t yy_def[59] =
-    {   0,
-       57,    1,   57,   57,   57,   57,   57,   57,   57,   57,
-       57,   57,   57,   57,   58,   58,   58,   58,   58,   58,
-       58,   57,   58,   58,   57,   57,   57,   57,   57,   57,
-       57,   58,   58,   58,   58,   58,   58,   58,   57,   58,
-       58,   58,   58,   58,   58,   58,   58,   58,   58,   58,
-       58,   58,   58,   58,   58,   58,    0,   57
-    } ;
-
-static yyconst flex_int16_t yy_nxt[100] =
+static yyconst flex_int32_t yy_meta[34] =
+    {   0,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        2,    1,    1,    1,    2,    2,    2,    2,    2,    2,
+        2,    2,    2,    2,    2,    2,    2,    2,    2,    2,
+        2,    2,    1
+    } ;
+
+static yyconst flex_int16_t yy_base[62] =
+    {   0,
+        0,   19,   71,   72,   68,   66,   72,   63,   72,   72,
+       72,   72,   72,   56,   53,   52,   51,    0,   36,   39,
+       41,   32,   30,   29,   24,   19,   21,   54,   52,   72,
+       43,   72,   72,   72,    0,   31,   32,   25,   19,    0,
+       17,   72,    0,    0,    0,    0,    0,   26,   17,    0,
+       23,   19,   21,    0,   15,    0,   21,   16,    0,   72,
+       33
+    } ;
+
+static yyconst flex_int16_t yy_def[62] =
+    {   0,
+       60,    1,   60,   60,   60,   60,   60,   60,   60,   60,
+       60,   60,   60,   60,   60,   60,   60,   61,   61,   61,
+       61,   61,   61,   61,   60,   61,   61,   60,   60,   60,
+       60,   60,   60,   60,   61,   61,   61,   61,   61,   61,
+       61,   60,   61,   61,   61,   61,   61,   61,   61,   61,
+       61,   61,   61,   61,   61,   61,   61,   61,   61,    0,
+       60
+    } ;
+
+static yyconst flex_int16_t yy_nxt[106] =
     {   0,
         4,    5,    6,    7,    8,    9,   10,   11,   12,   13,
-       14,   15,   15,   15,   15,   15,   16,   15,   17,   15,
-       18,   15,   15,   19,   20,   15,   15,   21,   15,   22,
-       23,   32,   24,   40,   41,   42,   43,   56,   55,   54,
-       53,   52,   51,   50,   49,   48,   47,   46,   45,   44,
-       28,   26,   25,   39,   38,   37,   36,   35,   34,   33,
-       31,   30,   29,   28,   27,   26,   25,   57,    3,   57,
-       57,   57,   57,   57,   57,   57,   57,   57,   57,   57,
-       57,   57,   57,   57,   57,   57,   57,   57,   57,   57,
-       57,   57,   57,   57,   57,   57,   57,   57,   57
+       14,   15,   16,   17,   18,   18,   18,   18,   18,   19,
+       18,   20,   18,   21,   18,   18,   22,   23,   18,   18,
+       24,   18,   25,   26,   35,   27,   43,   44,   45,   46,
+       59,   58,   57,   56,   55,   54,   53,   52,   51,   50,
+       49,   48,   47,   31,   29,   28,   42,   41,   40,   39,
+       38,   37,   36,   34,   33,   32,   31,   30,   29,   28,
+       60,    3,   60,   60,   60,   60,   60,   60,   60,   60,
+       60,   60,   60,   60,   60,   60,   60,   60,   60,   60,
+       60,   60,   60,   60,   60,   60,   60,   60,   60,   60,
 
+       60,   60,   60,   60,   60
     } ;
 
-static yyconst flex_int16_t yy_chk[100] =
+static yyconst flex_int16_t yy_chk[106] =
     {   0,
         1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
         1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
         1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        2,   58,    2,   23,   23,   24,   24,   55,   54,   52,
-       50,   49,   48,   46,   45,   38,   36,   35,   34,   33,
-       28,   26,   25,   22,   21,   20,   19,   18,   17,   16,
-       14,   13,   12,   11,    8,    6,    5,    3,   57,   57,
-       57,   57,   57,   57,   57,   57,   57,   57,   57,   57,
-       57,   57,   57,   57,   57,   57,   57,   57,   57,   57,
-       57,   57,   57,   57,   57,   57,   57,   57,   57
+        1,    1,    1,    2,   61,    2,   26,   26,   27,   27,
+       58,   57,   55,   53,   52,   51,   49,   48,   41,   39,
+       38,   37,   36,   31,   29,   28,   25,   24,   23,   22,
+       21,   20,   19,   17,   16,   15,   14,    8,    6,    5,
+        3,   60,   60,   60,   60,   60,   60,   60,   60,   60,
+       60,   60,   60,   60,   60,   60,   60,   60,   60,   60,
+       60,   60,   60,   60,   60,   60,   60,   60,   60,   60,
 
+       60,   60,   60,   60,   60
     } ;
 
 static yy_state_type yy_last_accepting_state;
@@ -505,7 +510,7 @@
 #define yyterminate() return token::END
 #line 26 "Core/QueryParser/flex.ll"
 # define YY_USER_ACTION  yylloc->columns (yyleng);
-#line 509 "Core/QueryParser/Generated/lexer.cpp"
+#line 514 "Core/QueryParser/Generated/lexer.cpp"
 
 #define INITIAL 0
 
@@ -592,7 +597,7 @@
 /* This used to be an fputs(), but since the string might contain NUL's,
  * we now use fwrite().
  */
-#define ECHO fwrite( yytext, yyleng, 1, yyout )
+#define ECHO do { if (fwrite( yytext, yyleng, 1, yyout )) {} } while (0)
 #endif
 
 /* Gets input and stuffs it into "buf".  number of characters read, or YY_NULL,
@@ -603,7 +608,7 @@
 	if ( YY_CURRENT_BUFFER_LVALUE->yy_is_interactive ) \
 		{ \
 		int c = '*'; \
-		yy_size_t n; \
+		size_t n; \
 		for ( n = 0; n < max_size && \
 			     (c = getc( yyin )) != EOF && c != '\n'; ++n ) \
 			buf[n] = (char) c; \
@@ -693,7 +698,7 @@
 
   yylloc->step ();
 
-#line 697 "Core/QueryParser/Generated/lexer.cpp"
+#line 702 "Core/QueryParser/Generated/lexer.cpp"
 
 	if ( !(yy_init) )
 		{
@@ -747,13 +752,13 @@
 			while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
 				{
 				yy_current_state = (int) yy_def[yy_current_state];
-				if ( yy_current_state >= 58 )
+				if ( yy_current_state >= 61 )
 					yy_c = yy_meta[(unsigned int) yy_c];
 				}
 			yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
 			++yy_cp;
 			}
-		while ( yy_current_state != 57 );
+		while ( yy_current_state != 60 );
 		yy_cp = (yy_last_accepting_cpos);
 		yy_current_state = (yy_last_accepting_state);
 
@@ -845,54 +850,69 @@
 case 14:
 YY_RULE_SETUP
 #line 50 "Core/QueryParser/flex.ll"
-{ return token::LPARAN; }
+{ yylval->string = new std::string(yytext); return token::LESS; }
 	YY_BREAK
 case 15:
 YY_RULE_SETUP
 #line 51 "Core/QueryParser/flex.ll"
-{ return token::RPARAN; }
+{ yylval->string = new std::string(yytext); return token::LESSEQUAL; }
 	YY_BREAK
 case 16:
 YY_RULE_SETUP
 #line 52 "Core/QueryParser/flex.ll"
-{ yylval->string = new std::string(yytext); return token::LESS; }
+{ yylval->string = new std::string(yytext); return token::EQUAL; }
 	YY_BREAK
 case 17:
 YY_RULE_SETUP
 #line 53 "Core/QueryParser/flex.ll"
-{ yylval->string = new std::string(yytext); return token::LESSEQUAL; }
+{ yylval->string = new std::string(yytext); return token::EQUAL; }
 	YY_BREAK
 case 18:
 YY_RULE_SETUP
 #line 54 "Core/QueryParser/flex.ll"
-{ yylval->string = new std::string(yytext); return token::EQUAL; }
+{ yylval->string = new std::string(yytext); return token::GREATEREQUAL; }
 	YY_BREAK
 case 19:
 YY_RULE_SETUP
 #line 55 "Core/QueryParser/flex.ll"
-{ yylval->string = new std::string(yytext); return token::EQUAL; }
+{ yylval->string = new std::string(yytext); return token::GREATER; }
 	YY_BREAK
 case 20:
 YY_RULE_SETUP
 #line 56 "Core/QueryParser/flex.ll"
-{ yylval->string = new std::string(yytext); return token::GREATEREQUAL; }
+{return token::LPARAN;}
 	YY_BREAK
 case 21:
 YY_RULE_SETUP
 #line 57 "Core/QueryParser/flex.ll"
-{ yylval->string = new std::string(yytext); return token::GREATER; }
+{return token::RPARAN;}
 	YY_BREAK
 case 22:
 YY_RULE_SETUP
 #line 58 "Core/QueryParser/flex.ll"
+{return token::PLUS;}
+	YY_BREAK
+case 23:
+YY_RULE_SETUP
+#line 59 "Core/QueryParser/flex.ll"
+{return token::MINUS;}
+	YY_BREAK
+case 24:
+YY_RULE_SETUP
+#line 60 "Core/QueryParser/flex.ll"
+{return token::MULTIPLY;}
+	YY_BREAK
+case 25:
+YY_RULE_SETUP
+#line 62 "Core/QueryParser/flex.ll"
 { yylval->string = new std::string(yytext); return token::IDENTIFIER; }
 	YY_BREAK
-case 23:
+case 26:
 YY_RULE_SETUP
-#line 60 "Core/QueryParser/flex.ll"
+#line 64 "Core/QueryParser/flex.ll"
 ECHO;
 	YY_BREAK
-#line 896 "Core/QueryParser/Generated/lexer.cpp"
+#line 916 "Core/QueryParser/Generated/lexer.cpp"
 case YY_STATE_EOF(INITIAL):
 	yyterminate();
 
@@ -1086,7 +1106,7 @@
 			{ /* Not enough room in the buffer - grow it. */
 
 			/* just a shorter name for the current buffer */
-			YY_BUFFER_STATE b = YY_CURRENT_BUFFER;
+			YY_BUFFER_STATE b = YY_CURRENT_BUFFER_LVALUE;
 
 			int yy_c_buf_p_offset =
 				(int) ((yy_c_buf_p) - b->yy_ch_buf);
@@ -1186,7 +1206,7 @@
 		while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
 			{
 			yy_current_state = (int) yy_def[yy_current_state];
-			if ( yy_current_state >= 58 )
+			if ( yy_current_state >= 61 )
 				yy_c = yy_meta[(unsigned int) yy_c];
 			}
 		yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
@@ -1214,13 +1234,13 @@
 	while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
 		{
 		yy_current_state = (int) yy_def[yy_current_state];
-		if ( yy_current_state >= 58 )
+		if ( yy_current_state >= 61 )
 			yy_c = yy_meta[(unsigned int) yy_c];
 		}
 	yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
-	yy_is_jam = (yy_current_state == 57);
+	yy_is_jam = (yy_current_state == 60);
 
-	return yy_is_jam ? 0 : yy_current_state;
+		return yy_is_jam ? 0 : yy_current_state;
 }
 
 #ifndef YY_NO_INPUT
@@ -1271,7 +1291,7 @@
 				case EOB_ACT_END_OF_FILE:
 					{
 					if ( yywrap( ) )
-						return 0;
+						return EOF;
 
 					if ( ! (yy_did_buffer_switch_on_eof) )
 						YY_NEW_FILE;
@@ -1409,10 +1429,6 @@
 	yyfree((void *) b  );
 }
 
-#ifndef __cplusplus
-extern int isatty (int );
-#endif /* __cplusplus */
-    
 /* Initializes or reinitializes a buffer.
  * This function is sometimes called more than once on the same buffer,
  * such as during a yyrestart() or at EOF.
@@ -1617,8 +1633,8 @@
 
 /** Setup the input buffer state to scan the given bytes. The next call to yylex() will
  * scan from a @e copy of @a bytes.
- * @param bytes the byte buffer to scan
- * @param len the number of bytes in the buffer pointed to by @a bytes.
+ * @param yybytes the byte buffer to scan
+ * @param _yybytes_len the number of bytes in the buffer pointed to by @a bytes.
  * 
  * @return the newly allocated buffer state object.
  */
@@ -1626,7 +1642,8 @@
 {
 	YY_BUFFER_STATE b;
 	char *buf;
-	yy_size_t n, i;
+	yy_size_t n;
+	int i;
     
 	/* Get memory for full buffer, including space for trailing EOB's. */
 	n = _yybytes_len + 2;
@@ -1856,7 +1873,7 @@
 
 #define YYTABLES_NAME "yytables"
 
-#line 60 "Core/QueryParser/flex.ll"
+#line 64 "Core/QueryParser/flex.ll"
 
 
 namespace VerifyTAPN

=== modified file 'src/Core/QueryParser/Generated/parser.cpp'
--- src/Core/QueryParser/Generated/parser.cpp	2013-08-28 19:51:15 +0000
+++ src/Core/QueryParser/Generated/parser.cpp	2014-03-20 14:00:01 +0000
@@ -45,7 +45,7 @@
 #line 46 "Core/QueryParser/Generated/parser.cpp"
 /* Unqualified %code blocks.  */
 /* Line 290 of lalr1.cc  */
-#line 37 "Core/QueryParser/grammar.yy"
+#line 38 "Core/QueryParser/grammar.yy"
 
 	#include "../TAPNQueryParser.hpp"
 
@@ -247,109 +247,130 @@
     {
       case 3: /* IDENTIFIER */
 /* Line 452 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
+#line 56 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).string); };
 /* Line 452 of lalr1.cc  */
 #line 254 "Core/QueryParser/Generated/parser.cpp"
         break;
       case 4: /* LESS */
 /* Line 452 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
+#line 56 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).string); };
 /* Line 452 of lalr1.cc  */
 #line 261 "Core/QueryParser/Generated/parser.cpp"
         break;
       case 5: /* LESSEQUAL */
 /* Line 452 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
+#line 56 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).string); };
 /* Line 452 of lalr1.cc  */
 #line 268 "Core/QueryParser/Generated/parser.cpp"
         break;
       case 6: /* EQUAL */
 /* Line 452 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
+#line 56 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).string); };
 /* Line 452 of lalr1.cc  */
 #line 275 "Core/QueryParser/Generated/parser.cpp"
         break;
       case 7: /* GREATEREQUAL */
 /* Line 452 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
+#line 56 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).string); };
 /* Line 452 of lalr1.cc  */
 #line 282 "Core/QueryParser/Generated/parser.cpp"
         break;
       case 8: /* GREATER */
 /* Line 452 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
+#line 56 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).string); };
 /* Line 452 of lalr1.cc  */
 #line 289 "Core/QueryParser/Generated/parser.cpp"
         break;
-      case 23: /* query */
+      case 26: /* query */
 /* Line 452 of lalr1.cc  */
-#line 55 "Core/QueryParser/grammar.yy"
+#line 58 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).query); };
 /* Line 452 of lalr1.cc  */
 #line 296 "Core/QueryParser/Generated/parser.cpp"
         break;
-      case 24: /* expression */
+      case 27: /* expression */
 /* Line 452 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
+#line 57 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).expr); };
 /* Line 452 of lalr1.cc  */
 #line 303 "Core/QueryParser/Generated/parser.cpp"
         break;
-      case 25: /* parExpression */
+      case 28: /* arithmeticExpression */
 /* Line 452 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-        { delete ((*yyvaluep).expr); };
+#line 57 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).arexpr); };
 /* Line 452 of lalr1.cc  */
 #line 310 "Core/QueryParser/Generated/parser.cpp"
         break;
-      case 26: /* notExpression */
+      case 29: /* multiplyExpression */
 /* Line 452 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-        { delete ((*yyvaluep).expr); };
+#line 57 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).arexpr); };
 /* Line 452 of lalr1.cc  */
 #line 317 "Core/QueryParser/Generated/parser.cpp"
         break;
-      case 27: /* orExpression */
+      case 30: /* arithmeticParantheses */
 /* Line 452 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-        { delete ((*yyvaluep).expr); };
+#line 57 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).arexpr); };
 /* Line 452 of lalr1.cc  */
 #line 324 "Core/QueryParser/Generated/parser.cpp"
         break;
-      case 28: /* andExpression */
+      case 31: /* parExpression */
 /* Line 452 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
+#line 57 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).expr); };
 /* Line 452 of lalr1.cc  */
 #line 331 "Core/QueryParser/Generated/parser.cpp"
         break;
-      case 29: /* boolExpression */
+      case 32: /* notExpression */
 /* Line 452 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
+#line 57 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).expr); };
 /* Line 452 of lalr1.cc  */
 #line 338 "Core/QueryParser/Generated/parser.cpp"
         break;
-      case 30: /* atomicProposition */
+      case 33: /* orExpression */
 /* Line 452 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
+#line 57 "Core/QueryParser/grammar.yy"
         { delete ((*yyvaluep).expr); };
 /* Line 452 of lalr1.cc  */
 #line 345 "Core/QueryParser/Generated/parser.cpp"
         break;
-      case 31: /* compareOp */
+      case 34: /* andExpression */
 /* Line 452 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
-        { delete ((*yyvaluep).string); };
+#line 57 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
 /* Line 452 of lalr1.cc  */
 #line 352 "Core/QueryParser/Generated/parser.cpp"
         break;
+      case 35: /* boolExpression */
+/* Line 452 of lalr1.cc  */
+#line 57 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 359 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 36: /* atomicProposition */
+/* Line 452 of lalr1.cc  */
+#line 57 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 366 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 37: /* compareOp */
+/* Line 452 of lalr1.cc  */
+#line 56 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 373 "Core/QueryParser/Generated/parser.cpp"
+        break;
 
       default:
         break;
@@ -449,7 +470,7 @@
   yylloc.begin.filename = yylloc.end.filename = &driver.file;
 }
 /* Line 539 of lalr1.cc  */
-#line 453 "Core/QueryParser/Generated/parser.cpp"
+#line 474 "Core/QueryParser/Generated/parser.cpp"
 
     /* Initialize the stacks.  The initial state will be pushed in
        yynewstate, since the latter expects the semantical and the
@@ -569,121 +590,174 @@
       {
           case 2:
 /* Line 664 of lalr1.cc  */
-#line 59 "Core/QueryParser/grammar.yy"
+#line 62 "Core/QueryParser/grammar.yy"
     { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EF, (yysemantic_stack_[(2) - (2)].expr)); driver.setAST((yyval.query)); }
     break;
 
   case 3:
 /* Line 664 of lalr1.cc  */
-#line 60 "Core/QueryParser/grammar.yy"
+#line 63 "Core/QueryParser/grammar.yy"
     { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AG, (yysemantic_stack_[(2) - (2)].expr)); driver.setAST((yyval.query)); }
     break;
 
   case 4:
 /* Line 664 of lalr1.cc  */
-#line 61 "Core/QueryParser/grammar.yy"
+#line 64 "Core/QueryParser/grammar.yy"
     { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EG, (yysemantic_stack_[(2) - (2)].expr)); driver.setAST((yyval.query)); }
     break;
 
   case 5:
 /* Line 664 of lalr1.cc  */
-#line 62 "Core/QueryParser/grammar.yy"
+#line 65 "Core/QueryParser/grammar.yy"
     { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AF, (yysemantic_stack_[(2) - (2)].expr)); driver.setAST((yyval.query)); }
     break;
 
   case 6:
 /* Line 664 of lalr1.cc  */
-#line 65 "Core/QueryParser/grammar.yy"
+#line 68 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 7:
 /* Line 664 of lalr1.cc  */
-#line 66 "Core/QueryParser/grammar.yy"
+#line 69 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 8:
 /* Line 664 of lalr1.cc  */
-#line 67 "Core/QueryParser/grammar.yy"
+#line 70 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 9:
 /* Line 664 of lalr1.cc  */
-#line 68 "Core/QueryParser/grammar.yy"
+#line 71 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 10:
 /* Line 664 of lalr1.cc  */
-#line 69 "Core/QueryParser/grammar.yy"
+#line 72 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 11:
 /* Line 664 of lalr1.cc  */
-#line 70 "Core/QueryParser/grammar.yy"
+#line 73 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 12:
 /* Line 664 of lalr1.cc  */
-#line 76 "Core/QueryParser/grammar.yy"
-    { (yyval.expr) = new VerifyTAPN::AST::ParExpression((yysemantic_stack_[(3) - (2)].expr)); }
+#line 79 "Core/QueryParser/grammar.yy"
+    { (yyval.arexpr) = new VerifyTAPN::AST::PlusExpression((yysemantic_stack_[(3) - (1)].arexpr), (yysemantic_stack_[(3) - (3)].arexpr)); }
     break;
 
   case 13:
 /* Line 664 of lalr1.cc  */
-#line 77 "Core/QueryParser/grammar.yy"
-    { (yyval.expr) = new VerifyTAPN::AST::NotExpression((yysemantic_stack_[(2) - (2)].expr)); }
+#line 80 "Core/QueryParser/grammar.yy"
+    { (yyval.arexpr) = new VerifyTAPN::AST::SubtractExpression((yysemantic_stack_[(3) - (1)].arexpr), (yysemantic_stack_[(3) - (3)].arexpr)); }
     break;
 
   case 14:
 /* Line 664 of lalr1.cc  */
-#line 78 "Core/QueryParser/grammar.yy"
-    { (yyval.expr) = new VerifyTAPN::AST::OrExpression((yysemantic_stack_[(3) - (1)].expr), (yysemantic_stack_[(3) - (3)].expr)); }
+#line 81 "Core/QueryParser/grammar.yy"
+    { (yyval.arexpr) = new VerifyTAPN::AST::MinusExpression((yysemantic_stack_[(2) - (2)].arexpr)); }
     break;
 
   case 15:
 /* Line 664 of lalr1.cc  */
-#line 79 "Core/QueryParser/grammar.yy"
-    { (yyval.expr) = new VerifyTAPN::AST::AndExpression((yysemantic_stack_[(3) - (1)].expr), (yysemantic_stack_[(3) - (3)].expr)); }
+#line 82 "Core/QueryParser/grammar.yy"
+    { (yyval.arexpr) = (yysemantic_stack_[(1) - (1)].arexpr); }
     break;
 
   case 16:
 /* Line 664 of lalr1.cc  */
-#line 80 "Core/QueryParser/grammar.yy"
-    { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(true); }
+#line 85 "Core/QueryParser/grammar.yy"
+    { (yyval.arexpr) = new VerifyTAPN::AST::MultiplyExpression((yysemantic_stack_[(3) - (1)].arexpr), (yysemantic_stack_[(3) - (3)].arexpr)); }
     break;
 
   case 17:
 /* Line 664 of lalr1.cc  */
-#line 81 "Core/QueryParser/grammar.yy"
-    { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(false); }
+#line 86 "Core/QueryParser/grammar.yy"
+    { (yyval.arexpr) = (yysemantic_stack_[(1) - (1)].arexpr); }
     break;
 
   case 18:
 /* Line 664 of lalr1.cc  */
-#line 83 "Core/QueryParser/grammar.yy"
+#line 89 "Core/QueryParser/grammar.yy"
+    { (yyval.arexpr) = (yysemantic_stack_[(3) - (2)].arexpr); }
+    break;
+
+  case 19:
+/* Line 664 of lalr1.cc  */
+#line 90 "Core/QueryParser/grammar.yy"
+    { (yyval.arexpr) = new VerifyTAPN::AST::NumberExpression((yysemantic_stack_[(1) - (1)].number));}
+    break;
+
+  case 20:
+/* Line 664 of lalr1.cc  */
+#line 91 "Core/QueryParser/grammar.yy"
     { 
-		int placeIndex = driver.getTAPN().getPlaceIndex(*(yysemantic_stack_[(3) - (1)].string));
-                delete (yysemantic_stack_[(3) - (1)].string);
-		if(placeIndex == -1) error((yylocation_stack_[(3) - (1)]), "unknown place"); 
-		(yyval.expr) = new VerifyTAPN::AST::AtomicProposition(placeIndex, (yysemantic_stack_[(3) - (2)].string), (yysemantic_stack_[(3) - (3)].number)); 
-                delete (yysemantic_stack_[(3) - (2)].string);
-	}
-    break;
-
-  case 19:
-/* Line 664 of lalr1.cc  */
-#line 89 "Core/QueryParser/grammar.yy"
+                                                                    int placeIndex = driver.getTAPN().getPlaceIndex(*(yysemantic_stack_[(1) - (1)].string));
+                                                                    delete (yysemantic_stack_[(1) - (1)].string);
+                                                                    if(placeIndex == -1) error((yylocation_stack_[(1) - (1)]), "unknown place"); 
+                                                                    (yyval.arexpr) = new VerifyTAPN::AST::IdentifierExpression(placeIndex); 
+                                                                 }
+    break;
+
+  case 21:
+/* Line 664 of lalr1.cc  */
+#line 99 "Core/QueryParser/grammar.yy"
+    { (yyval.expr) = (yysemantic_stack_[(3) - (2)].expr); }
+    break;
+
+  case 22:
+/* Line 664 of lalr1.cc  */
+#line 100 "Core/QueryParser/grammar.yy"
+    { (yyval.expr) = new VerifyTAPN::AST::NotExpression((yysemantic_stack_[(2) - (2)].expr)); }
+    break;
+
+  case 23:
+/* Line 664 of lalr1.cc  */
+#line 101 "Core/QueryParser/grammar.yy"
+    { (yyval.expr) = new VerifyTAPN::AST::OrExpression((yysemantic_stack_[(3) - (1)].expr), (yysemantic_stack_[(3) - (3)].expr)); }
+    break;
+
+  case 24:
+/* Line 664 of lalr1.cc  */
+#line 102 "Core/QueryParser/grammar.yy"
+    { (yyval.expr) = new VerifyTAPN::AST::AndExpression((yysemantic_stack_[(3) - (1)].expr), (yysemantic_stack_[(3) - (3)].expr)); }
+    break;
+
+  case 25:
+/* Line 664 of lalr1.cc  */
+#line 103 "Core/QueryParser/grammar.yy"
+    { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(true); }
+    break;
+
+  case 26:
+/* Line 664 of lalr1.cc  */
+#line 104 "Core/QueryParser/grammar.yy"
+    { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(false); }
+    break;
+
+  case 27:
+/* Line 664 of lalr1.cc  */
+#line 106 "Core/QueryParser/grammar.yy"
+    { (yyval.expr) = new VerifyTAPN::AST::AtomicProposition((yysemantic_stack_[(3) - (1)].arexpr), (yysemantic_stack_[(3) - (2)].string), (yysemantic_stack_[(3) - (3)].arexpr)); }
+    break;
+
+  case 28:
+/* Line 664 of lalr1.cc  */
+#line 107 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::DeadlockExpression(); }
     break;
 
 
 /* Line 664 of lalr1.cc  */
-#line 687 "Core/QueryParser/Generated/parser.cpp"
+#line 761 "Core/QueryParser/Generated/parser.cpp"
       default:
         break;
       }
@@ -983,14 +1057,16 @@
 
   /* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
      STATE-NUM.  */
-  const signed char Parser::yypact_ninf_ = -5;
+  const signed char Parser::yypact_ninf_ = -29;
   const signed char
   Parser::yypact_[] =
   {
-        12,     0,     0,     0,     0,     4,     2,     0,     3,    -5,
-      -5,    -5,    -1,    -5,    -5,    -5,    -5,    -5,    -5,    -1,
-      -1,    -1,    -5,    -5,    -5,    -5,    -5,    -5,    17,    -4,
-      -5,     0,     0,    -5,    -5,    10,    -5
+        46,    -1,    -1,    -1,    -1,     7,   -29,   -29,    -1,     9,
+     -29,   -29,   -29,    25,    -2,    43,    14,   -29,   -29,   -29,
+     -29,   -29,   -29,   -29,    -2,    -2,    -2,   -29,    -6,    38,
+      -1,   -29,    18,    14,    -1,    -1,   -29,   -29,   -29,   -29,
+     -29,    25,    25,    18,    25,   -29,   -29,    40,    -5,   -29,
+      14,    14,     3,   -29
   };
 
   /* YYDEFACT[S] -- default reduction number in state S.  Performed when
@@ -999,24 +1075,28 @@
   const unsigned char
   Parser::yydefact_[] =
   {
-         0,     0,     0,     0,     0,     0,     0,     0,     0,    16,
-      17,    19,     2,     6,     7,     8,     9,    11,    10,     3,
-       5,     4,     1,    20,    21,    22,    23,    24,     0,     0,
-      13,     0,     0,    18,    12,    14,    15
+         0,     0,     0,     0,     0,     0,    20,    19,     0,     0,
+      25,    26,    28,     0,     2,     0,    15,    17,     6,     7,
+       8,     9,    11,    10,     3,     5,     4,     1,     0,     0,
+       0,    22,     0,    14,     0,     0,    29,    30,    31,    32,
+      33,     0,     0,     0,     0,    21,    18,     0,    23,    24,
+      12,    13,    27,    16
   };
 
   /* YYPGOTO[NTERM-NUM].  */
   const signed char
   Parser::yypgoto_[] =
   {
-        -5,    -5,    -2,    20,    -5,    -5,    -5,    -5,    -5,    -5
+       -29,   -29,     2,    -8,   -12,   -28,    22,   -29,   -29,   -29,
+     -29,   -29,   -29
   };
 
   /* YYDEFGOTO[NTERM-NUM].  */
   const signed char
   Parser::yydefgoto_[] =
   {
-        -1,     5,    12,    13,    14,    15,    16,    17,    18,    28
+        -1,     5,    28,    15,    16,    17,    18,    19,    20,    21,
+      22,    23,    43
   };
 
   /* YYTABLE[YYPACT[STATE-NUM]].  What to do in state STATE-NUM.  If
@@ -1026,20 +1106,26 @@
   const unsigned char
   Parser::yytable_[] =
   {
-        19,    20,    21,     6,    22,    29,    23,    24,    25,    26,
-      27,    34,    31,    32,     7,    31,    32,     7,     8,     9,
-      10,    11,     1,     2,     3,     4,    33,    32,    30,    35,
-      36
+        29,    33,     6,    14,    24,    25,    26,    27,     7,    45,
+      34,    35,    35,     8,    34,    35,    53,     9,    10,    11,
+      12,     6,    13,    30,    47,    41,    42,     7,     6,    50,
+      51,    31,    32,     0,     7,    52,    48,    49,    44,    32,
+       0,    13,    36,    37,    38,    39,    40,    36,    37,    38,
+      39,    40,     0,    46,     0,    46,     1,     2,     3,     4,
+      41,    42,    41,    42,     0,    41,    42
   };
 
   /* YYCHECK.  */
-  const unsigned char
+  const signed char
   Parser::yycheck_[] =
   {
-         2,     3,     4,     3,     0,     7,     4,     5,     6,     7,
-       8,    15,    16,    17,    14,    16,    17,    14,    18,    19,
-      20,    21,    10,    11,    12,    13,     9,    17,     8,    31,
-      32
+         8,    13,     3,     1,     2,     3,     4,     0,     9,    15,
+      16,    17,    17,    14,    16,    17,    44,    18,    19,    20,
+      21,     3,    23,    14,    32,    22,    23,     9,     3,    41,
+      42,     9,    14,    -1,     9,    43,    34,    35,    24,    14,
+      -1,    23,     4,     5,     6,     7,     8,     4,     5,     6,
+       7,     8,    -1,    15,    -1,    15,    10,    11,    12,    13,
+      22,    23,    22,    23,    -1,    22,    23
   };
 
   /* STOS_[STATE-NUM] -- The (internal number of the) accessing
@@ -1047,10 +1133,12 @@
   const unsigned char
   Parser::yystos_[] =
   {
-         0,    10,    11,    12,    13,    23,     3,    14,    18,    19,
-      20,    21,    24,    25,    26,    27,    28,    29,    30,    24,
-      24,    24,     0,     4,     5,     6,     7,     8,    31,    24,
-      25,    16,    17,     9,    15,    24,    24
+         0,    10,    11,    12,    13,    26,     3,     9,    14,    18,
+      19,    20,    21,    23,    27,    28,    29,    30,    31,    32,
+      33,    34,    35,    36,    27,    27,    27,     0,    27,    28,
+      14,    31,    14,    29,    16,    17,     4,     5,     6,     7,
+       8,    22,    23,    37,    24,    15,    15,    28,    27,    27,
+      29,    29,    28,    30
   };
 
 #if YYDEBUG
@@ -1061,7 +1149,7 @@
   {
          0,   256,   257,   258,   259,   260,   261,   262,   263,   264,
      265,   266,   267,   268,   269,   270,   271,   272,   273,   274,
-     275,   276
+     275,   276,   277,   278,   279
   };
 #endif
 
@@ -1069,9 +1157,10 @@
   const unsigned char
   Parser::yyr1_[] =
   {
-         0,    22,    23,    23,    23,    23,    24,    24,    24,    24,
-      24,    24,    25,    26,    27,    28,    29,    29,    30,    30,
-      31,    31,    31,    31,    31
+         0,    25,    26,    26,    26,    26,    27,    27,    27,    27,
+      27,    27,    28,    28,    28,    28,    29,    29,    30,    30,
+      30,    31,    32,    33,    34,    35,    35,    36,    36,    37,
+      37,    37,    37,    37
   };
 
   /* YYR2[YYN] -- Number of symbols composing right hand side of rule YYN.  */
@@ -1079,8 +1168,9 @@
   Parser::yyr2_[] =
   {
          0,     2,     2,     2,     2,     2,     1,     1,     1,     1,
-       1,     1,     3,     2,     3,     3,     1,     1,     3,     1,
-       1,     1,     1,     1,     1
+       1,     1,     3,     3,     2,     1,     3,     1,     3,     1,
+       1,     3,     2,     3,     3,     1,     1,     3,     1,     1,
+       1,     1,     1,     1
   };
 
 
@@ -1092,9 +1182,11 @@
     "END", "error", "$undefined", "IDENTIFIER", "LESS", "LESSEQUAL",
   "EQUAL", "GREATEREQUAL", "GREATER", "NUMBER", "EF", "AG", "AF", "EG",
   "LPARAN", "RPARAN", "OR", "AND", "NOT", "BOOL_TRUE", "BOOL_FALSE",
-  "DEADLOCK", "$accept", "query", "expression", "parExpression",
-  "notExpression", "orExpression", "andExpression", "boolExpression",
-  "atomicProposition", "compareOp", YY_NULL
+  "DEADLOCK", "PLUS", "MINUS", "MULTIPLY", "$accept", "query",
+  "expression", "arithmeticExpression", "multiplyExpression",
+  "arithmeticParantheses", "parExpression", "notExpression",
+  "orExpression", "andExpression", "boolExpression", "atomicProposition",
+  "compareOp", YY_NULL
   };
 
 #if YYDEBUG
@@ -1102,13 +1194,15 @@
   const Parser::rhs_number_type
   Parser::yyrhs_[] =
   {
-        23,     0,    -1,    10,    24,    -1,    11,    24,    -1,    13,
-      24,    -1,    12,    24,    -1,    25,    -1,    26,    -1,    27,
-      -1,    28,    -1,    30,    -1,    29,    -1,    14,    24,    15,
-      -1,    18,    25,    -1,    24,    16,    24,    -1,    24,    17,
-      24,    -1,    19,    -1,    20,    -1,     3,    31,     9,    -1,
-      21,    -1,     4,    -1,     5,    -1,     6,    -1,     7,    -1,
-       8,    -1
+        26,     0,    -1,    10,    27,    -1,    11,    27,    -1,    13,
+      27,    -1,    12,    27,    -1,    31,    -1,    32,    -1,    33,
+      -1,    34,    -1,    36,    -1,    35,    -1,    28,    22,    29,
+      -1,    28,    23,    29,    -1,    23,    29,    -1,    29,    -1,
+      29,    24,    30,    -1,    30,    -1,    14,    28,    15,    -1,
+       9,    -1,     3,    -1,    14,    27,    15,    -1,    18,    31,
+      -1,    27,    16,    27,    -1,    27,    17,    27,    -1,    19,
+      -1,    20,    -1,    28,    37,    28,    -1,    21,    -1,     4,
+      -1,     5,    -1,     6,    -1,     7,    -1,     8,    -1
   };
 
   /* YYPRHS[YYN] -- Index of the first RHS symbol of rule number YYN in
@@ -1117,17 +1211,19 @@
   Parser::yyprhs_[] =
   {
          0,     0,     3,     6,     9,    12,    15,    17,    19,    21,
-      23,    25,    27,    31,    34,    38,    42,    44,    46,    50,
-      52,    54,    56,    58,    60
+      23,    25,    27,    31,    35,    38,    40,    44,    46,    50,
+      52,    54,    58,    61,    65,    69,    71,    73,    77,    79,
+      81,    83,    85,    87
   };
 
   /* YYRLINE[YYN] -- Source line where rule number YYN was defined.  */
   const unsigned char
   Parser::yyrline_[] =
   {
-         0,    59,    59,    60,    61,    62,    65,    66,    67,    68,
-      69,    70,    76,    77,    78,    79,    80,    81,    82,    89,
-      90,    90,    90,    90,    90
+         0,    62,    62,    63,    64,    65,    68,    69,    70,    71,
+      72,    73,    79,    80,    81,    82,    85,    86,    89,    90,
+      91,    99,   100,   101,   102,   103,   104,   106,   107,   109,
+     109,   109,   109,   109
   };
 
   // Print the state stack on the debug stream.
@@ -1194,7 +1290,7 @@
        2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
        2,     2,     2,     2,     2,     2,     1,     2,     3,     4,
        5,     6,     7,     8,     9,    10,    11,    12,    13,    14,
-      15,    16,    17,    18,    19,    20,    21
+      15,    16,    17,    18,    19,    20,    21,    22,    23,    24
     };
     if ((unsigned int) t <= yyuser_token_number_max_)
       return translate_table[t];
@@ -1203,24 +1299,24 @@
   }
 
   const int Parser::yyeof_ = 0;
-  const int Parser::yylast_ = 30;
-  const int Parser::yynnts_ = 10;
+  const int Parser::yylast_ = 66;
+  const int Parser::yynnts_ = 13;
   const int Parser::yyempty_ = -2;
-  const int Parser::yyfinal_ = 22;
+  const int Parser::yyfinal_ = 27;
   const int Parser::yyterror_ = 1;
   const int Parser::yyerrcode_ = 256;
-  const int Parser::yyntokens_ = 22;
+  const int Parser::yyntokens_ = 25;
 
-  const unsigned int Parser::yyuser_token_number_max_ = 276;
+  const unsigned int Parser::yyuser_token_number_max_ = 279;
   const Parser::token_number_type Parser::yyundef_token_ = 2;
 
 /* Line 1135 of lalr1.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
 /* Line 1135 of lalr1.cc  */
-#line 1222 "Core/QueryParser/Generated/parser.cpp"
+#line 1318 "Core/QueryParser/Generated/parser.cpp"
 /* Line 1136 of lalr1.cc  */
-#line 92 "Core/QueryParser/grammar.yy"
+#line 111 "Core/QueryParser/grammar.yy"
 
 
 void 

=== modified file 'src/Core/QueryParser/Generated/parser.hpp'
--- src/Core/QueryParser/Generated/parser.hpp	2013-08-28 19:51:15 +0000
+++ src/Core/QueryParser/Generated/parser.hpp	2014-03-20 14:00:01 +0000
@@ -84,12 +84,13 @@
 
 	int          					number;
 	std::string* 					string;
-	VerifyTAPN::AST::Expression*	expr;
-	VerifyTAPN::AST::Query*		 	query;
+	VerifyTAPN::AST::Expression*                    expr;
+        VerifyTAPN::AST::ArithmeticExpression*           arexpr;
+	VerifyTAPN::AST::Query*                         query;
 
 
 /* Line 33 of lalr1.cc  */
-#line 93 "Core/QueryParser/Generated/parser.hpp"
+#line 94 "Core/QueryParser/Generated/parser.hpp"
     };
 #else
     typedef YYSTYPE semantic_type;
@@ -120,7 +121,10 @@
      NOT = 273,
      BOOL_TRUE = 274,
      BOOL_FALSE = 275,
-     DEADLOCK = 276
+     DEADLOCK = 276,
+     PLUS = 277,
+     MINUS = 278,
+     MULTIPLY = 279
    };
 
     };
@@ -229,7 +233,7 @@
     static const unsigned char yytable_[];
     static const signed char yytable_ninf_;
 
-    static const unsigned char yycheck_[];
+    static const signed char yycheck_[];
 
     /// For a state, its accessing symbol.
     static const unsigned char yystos_[];
@@ -303,7 +307,7 @@
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
 /* Line 33 of lalr1.cc  */
-#line 307 "Core/QueryParser/Generated/parser.hpp"
+#line 311 "Core/QueryParser/Generated/parser.hpp"
 
 
 

=== modified file 'src/Core/QueryParser/NormalizationVisitor.cpp'
--- src/Core/QueryParser/NormalizationVisitor.cpp	2013-08-13 20:59:28 +0000
+++ src/Core/QueryParser/NormalizationVisitor.cpp	2014-03-20 14:00:01 +0000
@@ -14,14 +14,6 @@
 			tuple.returnExpr = static_cast<Tuple&>(any).returnExpr;
 		}
 
-		void NormalizationVisitor::visit(const ParExpression& expr, Result& context)
-		{
-			Tuple& tuple = static_cast<Tuple&>(context);
-			Tuple any = Tuple(tuple.negate, NULL);
-			expr.getChild().accept(*this, any);
-			tuple.returnExpr = new ParExpression(static_cast<Tuple&>(any).returnExpr);
-		}
-
 		void NormalizationVisitor::visit(const OrExpression& expr, Result& context)
 		{
 			Tuple& tuple = static_cast<Tuple&>(context);
@@ -61,10 +53,28 @@
 			}else{
 				op = expr.getOperator();
 			}
-			tuple.returnExpr = new AtomicProposition(expr.getPlace(), &op, expr.getNumberOfTokens());
+			tuple.returnExpr = new AtomicProposition(&expr.getLeft(), &op, &expr.getRight());// dont visit arithmetics for now
 		}
-
-               void NormalizationVisitor::visit(const DeadlockExpression& expr, Result& context) {
+                
+                void NormalizationVisitor::visit(const NumberExpression& expr, Result& context){
+                }
+                
+                void NormalizationVisitor::visit(const IdentifierExpression& expr, Result& context){
+                }
+                
+                void NormalizationVisitor::visit(const MultiplyExpression& expr, Result& context){
+                }
+                
+                void NormalizationVisitor::visit(const MinusExpression& expr, Result& context){
+                }
+                
+                void NormalizationVisitor::visit(const SubtractExpression& expr, Result& context){
+                }
+                
+                void NormalizationVisitor::visit(const PlusExpression& expr, Result& context){
+                }
+                
+                void NormalizationVisitor::visit(const DeadlockExpression& expr, Result& context) {
 			Tuple& tuple = static_cast<Tuple&>(context);
 			tuple.returnExpr = new DeadlockExpression();                  
                 }

=== modified file 'src/Core/QueryParser/NormalizationVisitor.hpp'
--- src/Core/QueryParser/NormalizationVisitor.hpp	2013-08-09 21:47:22 +0000
+++ src/Core/QueryParser/NormalizationVisitor.hpp	2014-03-20 14:00:01 +0000
@@ -28,13 +28,18 @@
 			virtual ~NormalizationVisitor() {};
 
 			virtual void visit(const NotExpression& expr, Result& context);
-			virtual void visit(const ParExpression& expr, Result& context);
 			virtual void visit(const OrExpression& expr, Result& context);
 			virtual void visit(const AndExpression& expr, Result& context);
 			virtual void visit(const AtomicProposition& expr, Result& context);
 			virtual void visit(const BoolExpression& expr, Result& context);
 			virtual void visit(const Query& query, Result& context);
 			virtual void visit(const DeadlockExpression& expr, Result& context);
+                        virtual void visit(const NumberExpression& expr, Result& context);
+                        virtual void visit(const IdentifierExpression& expr, Result& context);
+                        virtual void visit(const MultiplyExpression& expr, Result& context);
+                        virtual void visit(const MinusExpression& expr, Result& context);
+                        virtual void visit(const SubtractExpression& expr, Result& context);
+                        virtual void visit(const PlusExpression& expr, Result& context);
 
 			AST::Query* normalize(const AST::Query& query) { Tuple any(false, NULL); query.accept(*this, any); 
                         return normalizedQuery; };

=== modified file 'src/Core/QueryParser/Visitor.hpp'
--- src/Core/QueryParser/Visitor.hpp	2013-08-09 21:47:22 +0000
+++ src/Core/QueryParser/Visitor.hpp	2014-03-20 14:00:01 +0000
@@ -8,12 +8,20 @@
 	namespace AST
 	{
 		class NotExpression;
-		class ParExpression;
 		class OrExpression;
 		class AndExpression;
 		class AtomicProposition;
                 class DeadlockExpression;
 		class BoolExpression;
+                class NumberExpression;
+                class IdentifierExpression;
+                class MultiplyExpression;
+                class MinusExpression;
+                class SubtractExpression;
+                class PlusExpression;
+                class ArithmeticExpression;
+                
+                
 		class Query;
                 
                 class Result {};
@@ -28,13 +36,18 @@
 		public:
 			virtual ~Visitor() { };
 			virtual void visit(const NotExpression& expr, Result& context) = 0;
-			virtual void visit(const ParExpression& expr, Result& context) = 0;
 			virtual void visit(const OrExpression& expr, Result& context) = 0;
 			virtual void visit(const AndExpression& expr, Result& context) = 0;
 			virtual void visit(const AtomicProposition& expr, Result& context) = 0;
 			virtual void visit(const BoolExpression& expr, Result& context) = 0;
 			virtual void visit(const Query& query, Result& context) = 0;
                         virtual void visit(const DeadlockExpression& expr, Result& context) = 0;
+                        virtual void visit(const NumberExpression& expr, Result& context) = 0;
+                        virtual void visit(const IdentifierExpression& expr, Result& context) = 0;
+                        virtual void visit(const MultiplyExpression& expr, Result& context) = 0;
+                        virtual void visit(const MinusExpression& expr, Result& context) = 0;
+                        virtual void visit(const SubtractExpression& expr, Result& context) = 0;
+                        virtual void visit(const PlusExpression& expr, Result& context) = 0;
 		};
 	}
 }

=== modified file 'src/Core/QueryParser/flex.ll'
--- src/Core/QueryParser/flex.ll	2013-04-08 19:04:49 +0000
+++ src/Core/QueryParser/flex.ll	2014-03-20 14:00:01 +0000
@@ -47,14 +47,18 @@
 false						{ return token::BOOL_FALSE; }
 deadlock                                        { return token::DEADLOCK; }
 "!"|not						{ return token::NOT; }
-"("							{ return token::LPARAN; }
-")"							{ return token::RPARAN; }
 "<"							{ yylval->string = new std::string(yytext); return token::LESS; }
 "<="						{ yylval->string = new std::string(yytext); return token::LESSEQUAL; }
 "="							{ yylval->string = new std::string(yytext); return token::EQUAL; }
 "=="						{ yylval->string = new std::string(yytext); return token::EQUAL; }
 ">="						{ yylval->string = new std::string(yytext); return token::GREATEREQUAL; }
 ">"							{ yylval->string = new std::string(yytext); return token::GREATER; }
+"("							{return token::LPARAN;}
+")"							{return token::RPARAN;}
+"+"							{return token::PLUS;}
+"-"							{return token::MINUS;}
+"*"							{return token::MULTIPLY;}
+
 [a-zA-Z_][a-zA-Z_0-9]*      { yylval->string = new std::string(yytext); return token::IDENTIFIER; }
 
 %%

=== modified file 'src/Core/QueryParser/grammar.yy'
--- src/Core/QueryParser/grammar.yy	2013-08-10 15:15:43 +0000
+++ src/Core/QueryParser/grammar.yy	2014-03-20 14:00:01 +0000
@@ -30,8 +30,9 @@
 {
 	int          					number;
 	std::string* 					string;
-	VerifyTAPN::AST::Expression*	expr;
-	VerifyTAPN::AST::Query*		 	query;
+	VerifyTAPN::AST::Expression*                    expr;
+        VerifyTAPN::AST::ArithmeticExpression*           arexpr;
+	VerifyTAPN::AST::Query*                         query;
 };
 
 %code{
@@ -46,48 +47,66 @@
 %token OR AND NOT
 %token BOOL_TRUE BOOL_FALSE
 %token DEADLOCK
-%type  <expr> expression notExpression parExpression orExpression andExpression boolExpression atomicProposition
+%token PLUS MINUS MULTIPLY
+%type <expr> expression notExpression parExpression orExpression andExpression boolExpression atomicProposition
+%type <arexpr> arithmeticExpression multiplyExpression arithmeticParantheses
 %type <query> query
 %type <string> compareOp
 
 %destructor { delete $$; } IDENTIFIER LESS LESSEQUAL EQUAL GREATEREQUAL GREATER compareOp
-%destructor { delete $$; } expression notExpression parExpression orExpression andExpression boolExpression atomicProposition
+%destructor { delete $$; } expression notExpression parExpression orExpression andExpression boolExpression atomicProposition arithmeticExpression multiplyExpression arithmeticParantheses
 %destructor { delete $$; } query
 
 %%
 %start query;
-query				: EF expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EF, $2); driver.setAST($$); }
-					| AG expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AG, $2); driver.setAST($$); }
-					| EG expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EG, $2); driver.setAST($$); }
-					| AF expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AF, $2); driver.setAST($$); }
-;
+query			: EF expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EF, $2); driver.setAST($$); }
+                        | AG expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AG, $2); driver.setAST($$); }
+                        | EG expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EG, $2); driver.setAST($$); }
+                        | AF expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AF, $2); driver.setAST($$); }
+                        ;
 
-expression			: parExpression { $$ = $1; }
-					| notExpression { $$ = $1; }
-					| orExpression { $$ = $1; }
-					| andExpression { $$ = $1; }
-					| atomicProposition { $$ = $1; }
-					| boolExpression { $$ = $1; }
-;
+expression              : parExpression             { $$ = $1; }
+                        | notExpression     { $$ = $1; }
+                        | orExpression      { $$ = $1; }
+                        | andExpression     { $$ = $1; }
+                        | atomicProposition { $$ = $1; }
+                        | boolExpression    { $$ = $1; }
+                        ;
 
 %left OR;
 %left AND;
 
-parExpression		: LPARAN expression RPARAN { $$ = new VerifyTAPN::AST::ParExpression($2); };
-notExpression		: NOT parExpression { $$ = new VerifyTAPN::AST::NotExpression($2); };
-orExpression		: expression OR expression { $$ = new VerifyTAPN::AST::OrExpression($1, $3); };
+arithmeticExpression	: arithmeticExpression PLUS multiplyExpression	{ $$ = new VerifyTAPN::AST::PlusExpression($1, $3); }
+                        | arithmeticExpression MINUS multiplyExpression	{ $$ = new VerifyTAPN::AST::SubtractExpression($1, $3); }
+                        | MINUS multiplyExpression                    { $$ = new VerifyTAPN::AST::MinusExpression($2); }
+                        | multiplyExpression                            { $$ = $1; }
+                        ;
+
+multiplyExpression	: multiplyExpression MULTIPLY arithmeticParantheses	{ $$ = new VerifyTAPN::AST::MultiplyExpression($1, $3); }
+                        | arithmeticParantheses                                 { $$ = $1; }
+                        ;
+
+arithmeticParantheses	: LPARAN arithmeticExpression RPARAN	{ $$ = $2; }
+                        | NUMBER                        	{ $$ = new VerifyTAPN::AST::NumberExpression($1);}
+                        | IDENTIFIER                            { 
+                                                                    int placeIndex = driver.getTAPN().getPlaceIndex(*$1);
+                                                                    delete $1;
+                                                                    if(placeIndex == -1) error(@1, "unknown place"); 
+                                                                    $$ = new VerifyTAPN::AST::IdentifierExpression(placeIndex); 
+                                                                 }
+                        ;
+
+parExpression		: LPARAN expression RPARAN  { $$ = $2; };
+notExpression		: NOT parExpression         { $$ = new VerifyTAPN::AST::NotExpression($2); };
+orExpression		: expression OR expression  { $$ = new VerifyTAPN::AST::OrExpression($1, $3); };
 andExpression		: expression AND expression { $$ = new VerifyTAPN::AST::AndExpression($1, $3); };
-boolExpression		: BOOL_TRUE { $$ = new VerifyTAPN::AST::BoolExpression(true); } 
-					| BOOL_FALSE { $$ = new VerifyTAPN::AST::BoolExpression(false); };
-atomicProposition	: IDENTIFIER compareOp NUMBER 
-	{ 
-		int placeIndex = driver.getTAPN().getPlaceIndex(*$1);
-                delete $1;
-		if(placeIndex == -1) error(@1, "unknown place"); 
-		$$ = new VerifyTAPN::AST::AtomicProposition(placeIndex, $2, $3); 
-                delete $2;
-	} | DEADLOCK { $$ = new VerifyTAPN::AST::DeadlockExpression(); } ;
-compareOp			: LESS | LESSEQUAL | EQUAL | GREATEREQUAL | GREATER; 
+boolExpression		: BOOL_TRUE                 { $$ = new VerifyTAPN::AST::BoolExpression(true); } 
+			| BOOL_FALSE                { $$ = new VerifyTAPN::AST::BoolExpression(false); };
+
+atomicProposition	: arithmeticExpression compareOp arithmeticExpression { $$ = new VerifyTAPN::AST::AtomicProposition($1, $2, $3); } 
+                        | DEADLOCK { $$ = new VerifyTAPN::AST::DeadlockExpression(); } ;
+
+compareOp		: LESS | LESSEQUAL | EQUAL | GREATEREQUAL | GREATER; 
      
 %%
 

=== modified file 'src/DiscreteVerification/DeadlockVisitor.cpp'
--- src/DiscreteVerification/DeadlockVisitor.cpp	2013-08-09 21:47:22 +0000
+++ src/DiscreteVerification/DeadlockVisitor.cpp	2014-03-20 14:00:01 +0000
@@ -16,10 +16,6 @@
             expr.getChild().accept(*this, context);
         }
 
-        void DeadlockVisitor::visit(const ParExpression& expr, Result& context) {
-            expr.getChild().accept(*this, context);
-        }
-
         void DeadlockVisitor::visit(const OrExpression& expr, Result& context) {
             BoolResult left, right;
             expr.getLeft().accept(*this, left);
@@ -53,5 +49,29 @@
         void DeadlockVisitor::visit(const DeadlockExpression& expr, Result& context) {
             static_cast<BoolResult&>(context).value = true;
         }
+        
+        void DeadlockVisitor::visit(const NumberExpression& expr, Result& context){
+            static_cast<BoolResult&>(context).value = false;
+        }
+        
+        void DeadlockVisitor::visit(const IdentifierExpression& expr, Result& context){
+            static_cast<BoolResult&>(context).value = false;
+        }
+        
+        void DeadlockVisitor::visit(const MultiplyExpression& expr, Result& context){
+            static_cast<BoolResult&>(context).value = false;
+        }
+        
+        void DeadlockVisitor::visit(const MinusExpression& expr, Result& context){
+            static_cast<BoolResult&>(context).value = false;
+        }
+        
+        void DeadlockVisitor::visit(const SubtractExpression& expr, Result& context){
+            static_cast<BoolResult&>(context).value = false;
+        }
+        
+        void DeadlockVisitor::visit(const PlusExpression& expr, Result& context){
+            static_cast<BoolResult&>(context).value = false;
+        }
     }
 }

=== modified file 'src/DiscreteVerification/DeadlockVisitor.hpp'
--- src/DiscreteVerification/DeadlockVisitor.hpp	2013-08-13 20:59:28 +0000
+++ src/DiscreteVerification/DeadlockVisitor.hpp	2014-03-20 14:00:01 +0000
@@ -28,13 +28,18 @@
 
         public: // visitor methods
             virtual void visit(const NotExpression& expr, Result& context);
-            virtual void visit(const ParExpression& expr, Result& context);
             virtual void visit(const OrExpression& expr, Result& context);
             virtual void visit(const AndExpression& expr, Result& context);
             virtual void visit(const AtomicProposition& expr, Result& context);
             virtual void visit(const BoolExpression& expr, Result& context);
             virtual void visit(const Query& query, Result& context);
             virtual void visit(const DeadlockExpression& expr, Result& context);
+            virtual void visit(const NumberExpression& expr, Result& context);
+            virtual void visit(const IdentifierExpression& expr, Result& context);
+            virtual void visit(const MultiplyExpression& expr, Result& context);
+            virtual void visit(const MinusExpression& expr, Result& context);
+            virtual void visit(const SubtractExpression& expr, Result& context);
+            virtual void visit(const PlusExpression& expr, Result& context);
 
         };
     } /* namespace DiscreteVerification */

=== modified file 'src/DiscreteVerification/PlaceVisitor.cpp'
--- src/DiscreteVerification/PlaceVisitor.cpp	2013-08-09 21:47:22 +0000
+++ src/DiscreteVerification/PlaceVisitor.cpp	2014-03-20 14:00:01 +0000
@@ -15,11 +15,6 @@
 			expr.getChild().accept(*this, context);
 		}
 
-		void PlaceVisitor::visit(const ParExpression& expr, Result& context)
-		{
-			expr.getChild().accept(*this, context);
-		}
-
 		void PlaceVisitor::visit(const OrExpression& expr, Result& context)
 		{
 			expr.getLeft().accept(*this, context);
@@ -34,8 +29,8 @@
 
 		void PlaceVisitor::visit(const AtomicProposition& expr, Result& context)
 		{
-			AST::IntVectorResult& v = static_cast< AST::IntVectorResult & >(context);
-			v.value.push_back(expr.getPlace());
+                    expr.getLeft().accept(*this,context);
+                    expr.getRight().accept(*this,context);
 		}
 
                 void PlaceVisitor::visit(const DeadlockExpression& expr, Result& context)
@@ -50,5 +45,21 @@
 		{
 			query.getChild().accept(*this, context);
 		}
+                
+                void PlaceVisitor::visit(const NumberExpression& expr, Result& context){};
+                
+                void PlaceVisitor::visit(const IdentifierExpression& expr, Result& context){
+                    AST::IntVectorResult& v = static_cast< AST::IntVectorResult & >(context);
+		    v.value.push_back(expr.getPlace());
+                };
+                
+                void PlaceVisitor::visit(const MinusExpression& expr, Result& context){
+                    expr.getValue().accept(*this,context);
+                };
+                
+                void PlaceVisitor::visit(const OperationExpression& expr, Result& context){
+                    expr.getLeft().accept(*this,context);
+                    expr.getRight().accept(*this,context);
+                };
 } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */

=== modified file 'src/DiscreteVerification/PlaceVisitor.hpp'
--- src/DiscreteVerification/PlaceVisitor.hpp	2013-08-09 21:47:22 +0000
+++ src/DiscreteVerification/PlaceVisitor.hpp	2014-03-20 14:00:01 +0000
@@ -25,13 +25,19 @@
 
 	public: // visitor methods
 		virtual void visit(const NotExpression& expr, Result& context);
-		virtual void visit(const ParExpression& expr, Result& context);
 		virtual void visit(const OrExpression& expr, Result& context);
 		virtual void visit(const AndExpression& expr, Result& context);
 		virtual void visit(const AtomicProposition& expr, Result& context);
 		virtual void visit(const BoolExpression& expr, Result& context);
 		virtual void visit(const Query& query, Result& context);
 		virtual void visit(const DeadlockExpression& expr, Result& context);
+                virtual void visit(const NumberExpression& expr, Result& context);
+                virtual void visit(const IdentifierExpression& expr, Result& context);
+                virtual void visit(const MinusExpression& expr, Result& context);
+                virtual void visit(const OperationExpression& expr, Result& context);
+                virtual void visit(const MultiplyExpression& expr, Result& context){visit((OperationExpression&)expr, context);};
+                virtual void visit(const SubtractExpression& expr, Result& context){visit((OperationExpression&)expr, context);};;
+                virtual void visit(const PlusExpression& expr, Result& context){visit((OperationExpression&)expr, context);};;
 };
 
 } /* namespace DiscreteVerification */

=== modified file 'src/DiscreteVerification/QueryVisitor.hpp'
--- src/DiscreteVerification/QueryVisitor.hpp	2013-08-19 09:20:39 +0000
+++ src/DiscreteVerification/QueryVisitor.hpp	2014-03-20 14:00:01 +0000
@@ -34,17 +34,22 @@
             
             virtual ~QueryVisitor() {
             };
-
+ 
         public: // visitor methods
 
             virtual void visit(const NotExpression& expr, AST::Result& context);
-            virtual void visit(const ParExpression& expr, AST::Result& context);
             virtual void visit(const OrExpression& expr, AST::Result& context);
             virtual void visit(const AndExpression& expr, AST::Result& context);
             virtual void visit(const AtomicProposition& expr, AST::Result& context);
             virtual void visit(const BoolExpression& expr, AST::Result& context);
             virtual void visit(const Query& query, AST::Result& context);
             virtual void visit(const DeadlockExpression& expr, AST::Result& context);
+            virtual void visit(const NumberExpression& expr,  AST::Result& context);
+            virtual void visit(const IdentifierExpression& expr,  AST::Result& context);
+            virtual void visit(const MultiplyExpression& expr,  AST::Result& context);
+            virtual void visit(const MinusExpression& expr,  AST::Result& context);
+            virtual void visit(const SubtractExpression& expr,  AST::Result& context);
+            virtual void visit(const PlusExpression& expr,  AST::Result& context);
         private:
             bool compare(int numberOfTokensInPlace, const std::string& op, int n) const;
 
@@ -64,11 +69,6 @@
         }
 
         template<typename T>
-        void QueryVisitor<T>::visit(const ParExpression& expr, AST::Result& context) {
-            expr.getChild().accept(*this, context);
-        }
-
-        template<typename T>
         void QueryVisitor<T>::visit(const OrExpression& expr, AST::Result& context) {
             BoolResult left, right;
             expr.getLeft().accept(*this, left);
@@ -98,9 +98,13 @@
         template<typename T>
 
         void QueryVisitor<T>::visit(const AtomicProposition& expr, AST::Result& context) {
-            int numberOfTokens = marking.numberOfTokensInPlace(expr.getPlace());
+            IntResult left;
+            expr.getLeft().accept(*this, left);
+            IntResult right;
+            expr.getRight().accept(*this, right);
+
             static_cast<BoolResult&>(context).value 
-                    = compare(numberOfTokens, expr.getOperator(), expr.getNumberOfTokens());
+                    = compare(left.value, expr.getOperator(), right.value);
         }
 
         template<typename T>
@@ -110,7 +114,50 @@
         }
 
         template<typename T>
-        void QueryVisitor<T>::visit(const Query& query, AST::Result& context) {
+        void QueryVisitor<T>::visit(const NumberExpression& expr,  AST::Result& context){
+            ((IntResult&)context).value = expr.getValue();
+        }
+        
+        template<typename T>
+        void QueryVisitor<T>::visit(const IdentifierExpression& expr, AST::Result& context){
+            ((IntResult&)context).value = marking.numberOfTokensInPlace(expr.getPlace());
+        }
+        template<typename T>
+        void QueryVisitor<T>::visit(const MultiplyExpression& expr,  AST::Result& context){
+            IntResult left;
+            expr.getLeft().accept(*this, left);
+            IntResult right;
+            expr.getRight().accept(*this, right);
+            ((IntResult&)context).value = left.value * right.value;
+        }
+        template<typename T>
+        void QueryVisitor<T>::visit(const MinusExpression& expr,  AST::Result& context){
+            IntResult value;
+            expr.getValue().accept(*this, value);
+            ((IntResult&)context).value = -value.value;
+        }
+        
+        template<typename T>
+        void QueryVisitor<T>::visit(const SubtractExpression& expr,  AST::Result& context){
+            IntResult left;
+            expr.getLeft().accept(*this, left);
+            IntResult right;
+            expr.getRight().accept(*this, right);
+            ((IntResult&)context).value = left.value - right.value;
+        }
+        
+        template<typename T>
+        void QueryVisitor<T>::visit(const PlusExpression& expr,  AST::Result& context){
+            IntResult left;
+            expr.getLeft().accept(*this, left);
+            IntResult right;
+            expr.getRight().accept(*this, right);
+            ((IntResult&)context).value = left.value + right.value;
+        }
+        
+        
+        template<typename T>
+        void QueryVisitor<T>::visit(const Query& query,  AST::Result& context) {
             query.getChild().accept(*this, context);
             if (query.getQuantifier() == AG || query.getQuantifier() == AF) {
                 static_cast<BoolResult&>(context).value

=== modified file 'src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.cpp'
--- src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.cpp	2013-08-09 22:46:32 +0000
+++ src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.cpp	2014-03-20 14:00:01 +0000
@@ -15,11 +15,6 @@
 			assert(false);
 		}
 
-		void LivenessWeightQueryVisitor::visit(const ParExpression& expr, Result& context)
-		{
-			expr.getChild().accept(*this, context);
-		}
-
 		void LivenessWeightQueryVisitor::visit(const OrExpression& expr, Result& context)
 		{
 			IntResult left, right;
@@ -52,11 +47,52 @@
 
 		void LivenessWeightQueryVisitor::visit(const AtomicProposition& expr, Result& context)
 		{
-			int numberOfTokens = marking.numberOfTokensInPlace(expr.getPlace());
+                    IntResult left;
+                    expr.getLeft().accept(*this, left);
+                    IntResult right;
+                    expr.getLeft().accept(*this, right);
 			static_cast<IntResult&>(context).value
-                                = compare(numberOfTokens, expr.getOperator(), expr.getNumberOfTokens());
+                                = compare(left.value, expr.getOperator(), right.value);
 		}
 
+                void LivenessWeightQueryVisitor::visit(const NumberExpression& expr, Result& context){
+                    ((IntResult&)context).value = expr.getValue();
+                }
+
+                void LivenessWeightQueryVisitor::visit(const IdentifierExpression& expr, Result& context){
+                    ((IntResult&)context).value = marking.numberOfTokensInPlace(expr.getPlace());
+                }
+                
+                void LivenessWeightQueryVisitor::visit(const MultiplyExpression& expr, Result& context){
+                    IntResult left;
+                    expr.getLeft().accept(*this, left);
+                    IntResult right;
+                    expr.getLeft().accept(*this, right);
+                    ((IntResult&)context).value = left.value * right.value;
+                }
+                
+                void LivenessWeightQueryVisitor::visit(const MinusExpression& expr, Result& context){
+                    IntResult value;
+                    expr.getValue().accept(*this, value);
+                    ((IntResult&)context).value = -value.value;
+                }
+
+                void LivenessWeightQueryVisitor::visit(const SubtractExpression& expr, Result& context){
+                    IntResult left;
+                    expr.getLeft().accept(*this, left);
+                    IntResult right;
+                    expr.getLeft().accept(*this, right);
+                    ((IntResult&)context).value = left.value - right.value;
+                }
+
+                void LivenessWeightQueryVisitor::visit(const PlusExpression& expr, Result& context){
+                    IntResult left;
+                    expr.getLeft().accept(*this, left);
+                    IntResult right;
+                    expr.getLeft().accept(*this, right);
+                    ((IntResult&)context).value = left.value + right.value;
+                }
+
 		void LivenessWeightQueryVisitor::visit(const BoolExpression& expr, Result& context)
 		{
 			static_cast<IntResult&>(context).value 

=== modified file 'src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.hpp'
--- src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.hpp	2013-08-09 21:47:22 +0000
+++ src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.hpp	2014-03-20 14:00:01 +0000
@@ -26,13 +26,18 @@
 
 	public: // visitor methods
 		virtual void visit(const NotExpression& expr, Result& context);
-		virtual void visit(const ParExpression& expr, Result& context);
 		virtual void visit(const OrExpression& expr, Result& context);
 		virtual void visit(const AndExpression& expr, Result& context);
 		virtual void visit(const AtomicProposition& expr, Result& context);
 		virtual void visit(const BoolExpression& expr, Result& context);
 		virtual void visit(const Query& query, Result& context);
                 virtual void visit(const DeadlockExpression& expr, Result& context);
+                virtual void visit(const NumberExpression& expr, Result& context);
+                virtual void visit(const IdentifierExpression& expr, Result& context);
+                virtual void visit(const MultiplyExpression& expr, Result& context);
+                virtual void visit(const MinusExpression& expr, Result& context);
+                virtual void visit(const SubtractExpression& expr, Result& context);
+                virtual void visit(const PlusExpression& expr, Result& context);
 	private:
 		int compare(int numberOfTokensInPlace, const std::string& op, int n) const;
 

=== modified file 'src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.cpp'
--- src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.cpp	2013-08-09 22:46:32 +0000
+++ src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.cpp	2014-03-20 14:00:01 +0000
@@ -15,11 +15,6 @@
 			assert(false);
 		}
 
-		void WeightQueryVisitor::visit(const ParExpression& expr, Result& context)
-		{
-			expr.getChild().accept(*this, context);
-		}
-
 		void WeightQueryVisitor::visit(const OrExpression& expr, Result& context)
 		{
 			IntResult left, right;
@@ -57,11 +52,52 @@
 
 		void WeightQueryVisitor::visit(const AtomicProposition& expr, Result& context)
 		{
-			int numberOfTokens = marking.numberOfTokensInPlace(expr.getPlace());
+                    IntResult left;
+                    expr.getLeft().accept(*this, left);
+                    IntResult right;
+                    expr.getLeft().accept(*this, right);
 			static_cast<IntResult&>(context).value
-                                = compare(numberOfTokens, expr.getOperator(), expr.getNumberOfTokens());
+                                = compare(left.value, expr.getOperator(), right.value);
 		}
 
+                void WeightQueryVisitor::visit(const NumberExpression& expr, Result& context){
+                    ((IntResult&)context).value = expr.getValue();
+                }
+
+                void WeightQueryVisitor::visit(const IdentifierExpression& expr, Result& context){
+                    ((IntResult&)context).value = marking.numberOfTokensInPlace(expr.getPlace());
+                }
+                
+                void WeightQueryVisitor::visit(const MultiplyExpression& expr, Result& context){
+                    IntResult left;
+                    expr.getLeft().accept(*this, left);
+                    IntResult right;
+                    expr.getLeft().accept(*this, right);
+                    ((IntResult&)context).value = left.value * right.value;
+                }
+                
+                void WeightQueryVisitor::visit(const MinusExpression& expr, Result& context){
+                    IntResult value;
+                    expr.getValue().accept(*this, value);
+                    ((IntResult&)context).value = -value.value;
+                }
+
+                void WeightQueryVisitor::visit(const SubtractExpression& expr, Result& context){
+                    IntResult left;
+                    expr.getLeft().accept(*this, left);
+                    IntResult right;
+                    expr.getLeft().accept(*this, right);
+                    ((IntResult&)context).value = left.value - right.value;
+                }
+
+                void WeightQueryVisitor::visit(const PlusExpression& expr, Result& context){
+                    IntResult left;
+                    expr.getLeft().accept(*this, left);
+                    IntResult right;
+                    expr.getLeft().accept(*this, right);
+                    ((IntResult&)context).value = left.value + right.value;
+                }
+                
 		void WeightQueryVisitor::visit(const BoolExpression& expr, Result& context)
 		{
 			static_cast<IntResult&>(context).value

=== modified file 'src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.hpp'
--- src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.hpp	2013-08-09 21:47:22 +0000
+++ src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.hpp	2014-03-20 14:00:01 +0000
@@ -26,13 +26,18 @@
 
 	public: // visitor methods
 		virtual void visit(const NotExpression& expr, Result& context);
-		virtual void visit(const ParExpression& expr, Result& context);
 		virtual void visit(const OrExpression& expr, Result& context);
 		virtual void visit(const AndExpression& expr, Result& context);
 		virtual void visit(const AtomicProposition& expr, Result& context);
 		virtual void visit(const BoolExpression& expr, Result& context);
 		virtual void visit(const Query& query, Result& context);
                 virtual void visit(const DeadlockExpression& expr, Result& context);
+                virtual void visit(const NumberExpression& expr, Result& context);
+                virtual void visit(const IdentifierExpression& expr, Result& context);
+                virtual void visit(const MultiplyExpression& expr, Result& context);
+                virtual void visit(const MinusExpression& expr, Result& context);
+                virtual void visit(const SubtractExpression& expr, Result& context);
+                virtual void visit(const PlusExpression& expr, Result& context);
 	private:
 		int compare(int numberOfTokensInPlace, const std::string& op, int n) const;