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

[Peter Gjøl Jensen]

This branch removes boost from the core engine.
I did not remove boost from the entire code-base, as rewriting it would either take a long time and/or have little to no positive influence on the running-time.

The boost library is therefore still used for:
Parsing of model
Parsing of commandline input
Interval operations
hashing markings

I don't think we can do any of the above better/easier than by using boost.

I also did a minor change in the query-visitor, such that AND and OR operations have a "lazy" evaluation, such that the right-hand-side is only evaluated IF the left part has the right value.
This could potentially give some major speedups in long queries - with the database it does not seem to impact the result in any significant way, but might do so (positively) on complex queries on larger nets.

Overall the results from running the database are all in favor of the "nonBoost" version - but the engine is to fast to say anything about the speedup. On larger examples there exists a speedup, but it seems to be only a few percentage.

Changes overview:

Lines 0-173, 1785-2028, 3325-3436, 3608-3710, 3609-3998, 4124-4257, is removal of boost::any from the visitors
Lines 174-1782 is autogenerated files, just discard those.
Lines 2044-2736 is removal of boost in general from the TAPN model.
Lines 2740-3014 is propagation of changes in the model to the parser
Lines 3014-3322, 3440-3606 is propagation of changes in model to the verification-part
Lines 4002-4119 is removal of unused libraries
Lines 4259-4704 is propagation of changes to the successor generators
Lines 4707-5272 is propagation of changes to the verification-types
Lines 5274-5315 is propagation of changes to main and some deletions of objects to ease the use of valgrind when searching for memory-leaks.

Pay special attention to:
Lines 3715 - 3859 where the query parser has a "lazy" evaluation of OR and AND.
indicesOfCurrentPermutation which should be deleted properly to avoid memory-leaks in lines 4259-4704 (The successor generators)

[Jakob Taankvist (jakob-taankvist)]

I have run this version of the engine on a few examples - and it looks like it works

I've also looked through the diff. It's so nice to see the removal of all the smartpointers from the model!

I don't know how big the speed penalty there is by doing the visitor context using inheritance? I think this could be done more efficiently using type arguments/templates, I also think this would make the code look nicer.

In lines 2167 - 2206, is there a reason we don't use const iterators anymore? Are we transitioning to C++11? In that case we could use a C++11 foreach loop?

Delete these lines? :
3792 +// static_cast<BoolResult&>(context).value
3793 +// = left.value || right.value;

and

3809 +// static_cast<BoolResult&>(context).value
3810 +// = left.value && right.value;

review: Needs Information

[lp:~verifydtapn-contributers/verifydtapn/nonBoost]

329. By Peter Gjøl Jensen on 2013-08-19

removed outcommented code

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

With regards to using template parameters instead of template parameters, there seems to be some performance to gain (see http://www.cs.ucsb.edu/~urs/oocsb/papers/oopsla96.pdf) - but this would be mostly from removing the inheritance on the visitor and the nodes.

I tried it, though, and there are some issues.
The Visitor-pattern is implemented such that the visitor visits a node and the node then applies the visitors to itself (if any)(the accept method of the model). This will make the visitor call accept through the vtabel, and thus "dynamically cast" the node to the correct type. The node then applies the correct visitor.visit method to itself where the type is known at compile-time.

This means that we have to parse the "context" around while doing this, and as bool, int are base-types and vector<int> is neither, having a generic "context" is impossible without inheritance.

Making the visitor use template parameters will thus force the expressions to use template parameters, again forcing us to (in the code) create a query for each type of template parameter that we have.

I also tried using enums to mark the type of the nodes explicitly and do static-casts in the visitor - but this gives some other problems with partial defined classes.

This is where I stopped trying. If you have any ideas on how to solve this without the inheritance, I would appreciate it.

With regards to c++11, I don't think we are switching just yet.

We do not use const-iterator in the specific case, as we want to add to the preset of the arc.
So if we made it const,
arc->getOutputTransition() will give a const output transition (because the output transition is not wrapped in a pointer now) to which we want to add the arc, which now is const.
This will require the "Vector" you have defined to be of the type std::vector<const TimedTransition*>, which again would give issues on line 2164 (or rather, the initialize method of the TimedArcPetriNet.cpp file). Therefore the use of const is contradicting itself.

I have removed the four lines of outcommented code.

[Jakob Taankvist (jakob-taankvist)]

I just quickly looked into doing the visitor using genetics instead of inheritance, and it seams like it's rather complicated, so I think we should merge this branch as it works, and it's faster than before.

review: Approve

[Jiri Srba (srba)]

I get some compile warnings, can they be fixed please?

Core/QueryParser/Generated/lexer.cpp: In function ‘yy_buffer_state* yy_scan_bytes(const char*, yy_size_t)’:
Core/QueryParser/Generated/lexer.cpp:1634: warning: comparison between signed and unsigned integer expressions
Core/QueryParser/Generated/lexer.cpp: In function ‘yy_buffer_state* yy_scan_bytes(const char*, yy_size_t)’:
Core/QueryParser/Generated/lexer.cpp:1634: warning: comparison between signed and unsigned integer expressions

review: Needs Fixing

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

I have looked through the code and it looks good.

Please remove commented code on lines: 4452 4455 4578 4582 and remove the else clauses which only contain the commented code.

I have not tried running it, as it sounds like you have already tested this.

review: Approve

[lp:~verifydtapn-contributers/verifydtapn/nonBoost]

330. By Peter Gjøl Jensen on 2013-08-26

removed outcommented code

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

> I get some compile warnings, can they be fixed please?
>
> Core/QueryParser/Generated/lexer.cpp: In function ‘yy_buffer_state*
> yy_scan_bytes(const char*, yy_size_t)’:
> Core/QueryParser/Generated/lexer.cpp:1634: warning: comparison between signed
> and unsigned integer expressions
> Core/QueryParser/Generated/lexer.cpp: In function ‘yy_buffer_state*
> yy_scan_bytes(const char*, yy_size_t)’:
> Core/QueryParser/Generated/lexer.cpp:1634: warning: comparison between signed
> and unsigned integer expressions

The warnings seem to stem from autogenerated code. It seems to be an issue with newer versions of flex:
http://sourceforge.net/p/flex/bugs/140/

[Jiri Srba (srba)]

I can see, a patch should be included in the next release.
What do we do inbetween? Can you not used the older version of flex?

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

It seems to be an issue in the newest versions 2.5.36 and 2.5.37 (installed on your mac, not bundled with the engine), so there really is little to do other than simply ignoring this type of errors (-Wno-sign-compare).

[Jiri Srba (srba)]

Ok, I see. So it will be merged to trunk now.

review: Approve

=== modified file 'src/Core/QueryParser/AST.cpp'
--- src/Core/QueryParser/AST.cpp	2013-06-04 11:39:54 +0000
+++ src/Core/QueryParser/AST.cpp	2013-08-26 13:51:29 +0000
@@ -8,12 +8,12 @@
 			return new NotExpression(*this);
 		}
 
-		void NotExpression::accept(Visitor& visitor, boost::any& context) const
+		void NotExpression::accept(Visitor& visitor, Result& context) const
 		{
 			visitor.visit(*this, context);
 		}
 
-		void BoolExpression::accept(Visitor& visitor, boost::any& context) const
+		void BoolExpression::accept(Visitor& visitor, Result& context) const
 		{
 			visitor.visit(*this, context);
 		}
@@ -23,7 +23,7 @@
 			return new BoolExpression(*this);
 		}
 
-                void DeadlockExpression::accept(Visitor& visitor, boost::any& context) const
+                void DeadlockExpression::accept(Visitor& visitor, Result& context) const
 		{      
 			visitor.visit(*this, context);
 		}
@@ -33,7 +33,7 @@
 			return new DeadlockExpression(*this);
 		}
         
-		void AtomicProposition::accept(Visitor& visitor, boost::any& context) const
+		void AtomicProposition::accept(Visitor& visitor, Result& context) const
 		{
 			visitor.visit(*this, context);
 		}
@@ -48,7 +48,7 @@
 			return new AndExpression(*this);
 		}
 
-		void AndExpression::accept(Visitor& visitor, boost::any& context) const
+		void AndExpression::accept(Visitor& visitor, Result& context) const
 		{
 			visitor.visit(*this, context);
 		}
@@ -58,7 +58,7 @@
 			return new OrExpression(*this);
 		}
 
-		void OrExpression::accept(Visitor& visitor, boost::any& context) const
+		void OrExpression::accept(Visitor& visitor, Result& context) const
 		{
 			visitor.visit(*this, context);
 		}
@@ -68,7 +68,7 @@
 			return new ParExpression(*this);
 		}
 
-		void ParExpression::accept(Visitor& visitor, boost::any& context) const
+		void ParExpression::accept(Visitor& visitor, Result& context) const
 		{
 			visitor.visit(*this, context);
 		}
@@ -78,7 +78,7 @@
 			return new Query(*this);
 		}
 
-		void Query::accept(Visitor& visitor, boost::any& context) const
+		void Query::accept(Visitor& visitor, Result& context) const
 		{
 			visitor.visit(*this, context);
 		}

=== modified file 'src/Core/QueryParser/AST.hpp'
--- src/Core/QueryParser/AST.hpp	2013-06-04 11:39:54 +0000
+++ src/Core/QueryParser/AST.hpp	2013-08-26 13:51:29 +0000
@@ -4,7 +4,6 @@
 #include <string>
 #include <iostream>
 #include "Visitor.hpp"
-#include "boost/any.hpp"
 
 namespace VerifyTAPN{
 	namespace AST {
@@ -12,14 +11,13 @@
 		class Visitable
 		{
 		public:
-			virtual void accept(Visitor& visitor, boost::any& context) const = 0;
+			virtual void accept(Visitor& visitor, Result& context) const = 0;
 		};
 
 		class Expression : public Visitable
 		{
 		public:
 			virtual ~Expression() { };
-			//virtual void Accept(Visitor& visitor, boost::any& context) const = 0;
 			virtual Expression* clone() const = 0;
 		};
 
@@ -43,7 +41,7 @@
 			};
 
 			virtual NotExpression* clone() const;
-			virtual void accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, Result& context) const;
 
 			const Expression& getChild() const { return *expr; }
 		private:
@@ -57,7 +55,7 @@
 			virtual ~DeadlockExpression() { };
 
 			virtual DeadlockExpression* clone() const;
-			virtual void accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, Result& context) const;
                 };
 
 		class BoolExpression : public Expression
@@ -67,7 +65,7 @@
 			virtual ~BoolExpression() { };
 
 			virtual BoolExpression* clone() const;
-			virtual void accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, Result& context) const;
 
 			bool getValue() const { return value; };
 		private:
@@ -92,7 +90,7 @@
 			virtual ~AtomicProposition() { };
 
 			virtual AtomicProposition* clone() const;
-			virtual void accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, Result& context) const;
 
 			const int getPlace() const { return place; }
 			const std::string& getOperator() const { return op; }
@@ -126,7 +124,7 @@
 			}
 
 			virtual AndExpression* clone() const;
-			void accept(Visitor& visitor, boost::any& context) const;
+			void accept(Visitor& visitor, Result& context) const;
 
 			const Expression& getLeft() const { return *left; }
 			const Expression& getRight() const { return *right; }
@@ -161,7 +159,7 @@
 
 
 			virtual OrExpression* clone() const;
-			virtual void accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, Result& context) const;
 
 			const Expression& getLeft() const { return *left; }
 			const Expression& getRight() const { return *right; }
@@ -190,7 +188,7 @@
 			};
 
 			virtual ParExpression* clone() const;
-			virtual void accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, Result& context) const;
 
 			const Expression& getChild() const { return *expr; }
 		private:
@@ -216,7 +214,7 @@
 			virtual ~Query() { if( expr ) delete expr; }
 
 			virtual Query* clone() const;
-			virtual void accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, Result& context) const;
 
 			Quantifier getQuantifier() const { return quantifier; }
 			const Expression& getChild() const { return *expr; }

=== modified file 'src/Core/QueryParser/Generated/lexer.cpp'
--- src/Core/QueryParser/Generated/lexer.cpp	2013-06-04 11:39:54 +0000
+++ src/Core/QueryParser/Generated/lexer.cpp	2013-08-26 13:51:29 +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
@@ -142,15 +142,7 @@
 
 /* Size of default input buffer. */
 #ifndef YY_BUF_SIZE
-#ifdef __ia64__
-/* On IA-64, the buffer size is 16k, not 8k.
- * Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case.
- * Ditto for the __ia64__ case accordingly.
- */
-#define YY_BUF_SIZE 32768
-#else
 #define YY_BUF_SIZE 16384
-#endif /* __ia64__ */
 #endif
 
 /* The state buf must be large enough to hold one state per character in the main buffer.
@@ -162,7 +154,12 @@
 typedef struct yy_buffer_state *YY_BUFFER_STATE;
 #endif
 
-extern int yyleng;
+#ifndef YY_TYPEDEF_YY_SIZE_T
+#define YY_TYPEDEF_YY_SIZE_T
+typedef size_t yy_size_t;
+#endif
+
+extern yy_size_t yyleng;
 
 extern FILE *yyin, *yyout;
 
@@ -188,11 +185,6 @@
 
 #define unput(c) yyunput( c, (yytext_ptr)  )
 
-#ifndef YY_TYPEDEF_YY_SIZE_T
-#define YY_TYPEDEF_YY_SIZE_T
-typedef size_t yy_size_t;
-#endif
-
 #ifndef YY_STRUCT_YY_BUFFER_STATE
 #define YY_STRUCT_YY_BUFFER_STATE
 struct yy_buffer_state
@@ -210,7 +202,7 @@
 	/* Number of characters read into yy_ch_buf, not including EOB
 	 * characters.
 	 */
-	int yy_n_chars;
+	yy_size_t yy_n_chars;
 
 	/* Whether we "own" the buffer - i.e., we know we created it,
 	 * and can realloc() it to grow it, and should free() it to
@@ -280,8 +272,8 @@
 
 /* yy_hold_char holds the character lost when yytext is formed. */
 static char yy_hold_char;
-static int yy_n_chars;		/* number of characters read into yy_ch_buf */
-int yyleng;
+static yy_size_t yy_n_chars;		/* number of characters read into yy_ch_buf */
+yy_size_t yyleng;
 
 /* Points to current character in buffer. */
 static char *yy_c_buf_p = (char *) 0;
@@ -309,7 +301,7 @@
 
 YY_BUFFER_STATE yy_scan_buffer (char *base,yy_size_t size  );
 YY_BUFFER_STATE yy_scan_string (yyconst char *yy_str  );
-YY_BUFFER_STATE yy_scan_bytes (yyconst char *bytes,int len  );
+YY_BUFFER_STATE yy_scan_bytes (yyconst char *bytes,yy_size_t len  );
 
 void *yyalloc (yy_size_t  );
 void *yyrealloc (void *,yy_size_t  );
@@ -341,7 +333,7 @@
 
 /* Begin user sect3 */
 
-#define yywrap(n) 1
+#define yywrap() 1
 #define YY_SKIP_YYWRAP
 
 typedef unsigned char YY_CHAR;
@@ -513,7 +505,7 @@
 #define yyterminate() return token::END
 #line 26 "Core/QueryParser/flex.ll"
 # define YY_USER_ACTION  yylloc->columns (yyleng);
-#line 517 "Core/QueryParser/Generated/lexer.cpp"
+#line 509 "Core/QueryParser/Generated/lexer.cpp"
 
 #define INITIAL 0
 
@@ -552,7 +544,7 @@
 
 void yyset_out  (FILE * out_str  );
 
-int yyget_leng (void );
+yy_size_t yyget_leng (void );
 
 char *yyget_text (void );
 
@@ -592,12 +584,7 @@
 
 /* Amount of stuff to slurp up with each read. */
 #ifndef YY_READ_BUF_SIZE
-#ifdef __ia64__
-/* On IA-64, the buffer size is 16k, not 8k */
-#define YY_READ_BUF_SIZE 16384
-#else
 #define YY_READ_BUF_SIZE 8192
-#endif /* __ia64__ */
 #endif
 
 /* Copy whatever the last rule matched to the standard output. */
@@ -706,7 +693,7 @@
 
   yylloc->step ();
 
-#line 710 "Core/QueryParser/Generated/lexer.cpp"
+#line 697 "Core/QueryParser/Generated/lexer.cpp"
 
 	if ( !(yy_init) )
 		{
@@ -905,7 +892,7 @@
 #line 60 "Core/QueryParser/flex.ll"
 ECHO;
 	YY_BREAK
-#line 909 "Core/QueryParser/Generated/lexer.cpp"
+#line 896 "Core/QueryParser/Generated/lexer.cpp"
 case YY_STATE_EOF(INITIAL):
 	yyterminate();
 
@@ -1092,21 +1079,21 @@
 
 	else
 		{
-			int num_to_read =
+			yy_size_t num_to_read =
 			YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1;
 
 		while ( num_to_read <= 0 )
 			{ /* 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);
 
 			if ( b->yy_is_our_buffer )
 				{
-				int new_size = b->yy_buf_size * 2;
+				yy_size_t new_size = b->yy_buf_size * 2;
 
 				if ( new_size <= 0 )
 					b->yy_buf_size += b->yy_buf_size / 8;
@@ -1137,7 +1124,7 @@
 
 		/* Read in more data. */
 		YY_INPUT( (&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]),
-			(yy_n_chars), (size_t) num_to_read );
+			(yy_n_chars), num_to_read );
 
 		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
 		}
@@ -1233,7 +1220,7 @@
 	yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
 	yy_is_jam = (yy_current_state == 57);
 
-	return yy_is_jam ? 0 : yy_current_state;
+		return yy_is_jam ? 0 : yy_current_state;
 }
 
 #ifndef YY_NO_INPUT
@@ -1260,7 +1247,7 @@
 
 		else
 			{ /* need more input */
-			int offset = (yy_c_buf_p) - (yytext_ptr);
+			yy_size_t offset = (yy_c_buf_p) - (yytext_ptr);
 			++(yy_c_buf_p);
 
 			switch ( yy_get_next_buffer(  ) )
@@ -1422,10 +1409,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.
@@ -1538,7 +1521,7 @@
  */
 static void yyensure_buffer_stack (void)
 {
-	int num_to_alloc;
+	yy_size_t num_to_alloc;
     
 	if (!(yy_buffer_stack)) {
 
@@ -1635,7 +1618,7 @@
  * 
  * @return the newly allocated buffer state object.
  */
-YY_BUFFER_STATE yy_scan_bytes  (yyconst char * yybytes, int  _yybytes_len )
+YY_BUFFER_STATE yy_scan_bytes  (yyconst char * yybytes, yy_size_t  _yybytes_len )
 {
 	YY_BUFFER_STATE b;
 	char *buf;
@@ -1722,7 +1705,7 @@
 /** Get the length of the current token.
  * 
  */
-int yyget_leng  (void)
+yy_size_t yyget_leng  (void)
 {
         return yyleng;
 }

=== modified file 'src/Core/QueryParser/Generated/location.hh'
--- src/Core/QueryParser/Generated/location.hh	2013-06-04 11:39:54 +0000
+++ src/Core/QueryParser/Generated/location.hh	2013-08-26 13:51:29 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Locations for Bison parsers in C++
    
-      Copyright (C) 2002-2007, 2009-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2007, 2009-2013 Free Software Foundation, Inc.
    
    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
@@ -31,41 +31,56 @@
    version 2.2 of Bison.  */
 
 /**
- ** \file location.hh
+ ** \file Core/QueryParser/Generated/location.hh
  ** Define the VerifyTAPN::location class.
  */
 
-#ifndef BISON_LOCATION_HH
-# define BISON_LOCATION_HH
+#ifndef YY_YY_CORE_QUERYPARSER_GENERATED_LOCATION_HH_INCLUDED
+# define YY_YY_CORE_QUERYPARSER_GENERATED_LOCATION_HH_INCLUDED
 
-# include <iostream>
-# include <string>
 # include "position.hh"
 
-
-/* Line 162 of location.cc  */
+/* Line 166 of location.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 162 of location.cc  */
-#line 52 "Core/QueryParser/Generated/location.hh"
+/* Line 166 of location.cc  */
+#line 48 "Core/QueryParser/Generated/location.hh"
 
   /// Abstract a location.
   class location
   {
   public:
 
-    /// Construct a location.
-    location ()
-      : begin (), end ()
+    /// Construct a location from \a b to \a e.
+    location (const position& b, const position& e)
+      : begin (b)
+      , end (e)
+    {
+    }
+
+    /// Construct a 0-width location in \a p.
+    explicit location (const position& p = position ())
+      : begin (p)
+      , end (p)
+    {
+    }
+
+    /// Construct a 0-width location in \a f, \a l, \a c.
+    explicit location (std::string* f,
+                       unsigned int l = 1u,
+                       unsigned int c = 1u)
+      : begin (f, l, c)
+      , end (f, l, c)
     {
     }
 
 
     /// Initialization.
-    inline void initialize (std::string* fn)
+    void initialize (std::string* f = YY_NULL,
+                     unsigned int l = 1u,
+                     unsigned int c = 1u)
     {
-      begin.initialize (fn);
+      begin.initialize (f, l, c);
       end = begin;
     }
 
@@ -73,19 +88,19 @@
      ** \{ */
   public:
     /// Reset initial location to final location.
-    inline void step ()
+    void step ()
     {
       begin = end;
     }
 
     /// Extend the current location to the COUNT next columns.
-    inline void columns (unsigned int count = 1)
+    void columns (unsigned int count = 1)
     {
       end += count;
     }
 
     /// Extend the current location to the COUNT next lines.
-    inline void lines (unsigned int count = 1)
+    void lines (unsigned int count = 1)
     {
       end.lines (count);
     }
@@ -142,7 +157,9 @@
    **
    ** Avoid duplicate information.
    */
-  inline std::ostream& operator<< (std::ostream& ostr, const location& loc)
+  template <typename YYChar>
+  inline std::basic_ostream<YYChar>&
+  operator<< (std::basic_ostream<YYChar>& ostr, const location& loc)
   {
     position last = loc.end - 1;
     ostr << loc.begin;
@@ -157,12 +174,10 @@
     return ostr;
   }
 
-
-/* Line 271 of location.cc  */
+/* Line 296 of location.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
-/* Line 271 of location.cc  */
-#line 167 "Core/QueryParser/Generated/location.hh"
-
-#endif // not BISON_LOCATION_HH
+/* Line 296 of location.cc  */
+#line 182 "Core/QueryParser/Generated/location.hh"
+
+#endif /* !YY_YY_CORE_QUERYPARSER_GENERATED_LOCATION_HH_INCLUDED  */

=== modified file 'src/Core/QueryParser/Generated/parser.cpp'
--- src/Core/QueryParser/Generated/parser.cpp	2013-06-04 11:39:54 +0000
+++ src/Core/QueryParser/Generated/parser.cpp	2013-08-26 13:51:29 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Skeleton implementation for Bison LALR(1) parsers in C++
    
-      Copyright (C) 2002-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2013 Free Software Foundation, Inc.
    
    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
@@ -33,29 +33,34 @@
 
 /* First part of user declarations.  */
 
-
-/* Line 293 of lalr1.cc  */
-#line 39 "Core/QueryParser/Generated/parser.cpp"
+/* Line 283 of lalr1.cc  */
+#line 38 "Core/QueryParser/Generated/parser.cpp"
 
 
 #include "parser.hpp"
 
 /* User implementation prologue.  */
 
-
-/* Line 299 of lalr1.cc  */
-#line 48 "Core/QueryParser/Generated/parser.cpp"
+/* Line 289 of lalr1.cc  */
+#line 46 "Core/QueryParser/Generated/parser.cpp"
 /* Unqualified %code blocks.  */
-
-/* Line 300 of lalr1.cc  */
+/* Line 290 of lalr1.cc  */
 #line 37 "Core/QueryParser/grammar.yy"
 
 	#include "../TAPNQueryParser.hpp"
 
 
-
-/* Line 300 of lalr1.cc  */
-#line 59 "Core/QueryParser/Generated/parser.cpp"
+/* Line 290 of lalr1.cc  */
+#line 55 "Core/QueryParser/Generated/parser.cpp"
+
+
+# ifndef YY_NULL
+#  if defined __cplusplus && 201103L <= __cplusplus
+#   define YY_NULL nullptr
+#  else
+#   define YY_NULL 0
+#  endif
+# endif
 
 #ifndef YY_
 # if defined YYENABLE_NLS && YYENABLE_NLS
@@ -69,25 +74,26 @@
 # endif
 #endif
 
+#define YYRHSLOC(Rhs, K) ((Rhs)[K])
 /* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N].
    If N is 0, then set CURRENT to the empty location which ends
    the previous symbol: RHS[0] (always defined).  */
 
-#define YYRHSLOC(Rhs, K) ((Rhs)[K])
-#ifndef YYLLOC_DEFAULT
-# define YYLLOC_DEFAULT(Current, Rhs, N)                               \
- do                                                                    \
-   if (N)                                                              \
-     {                                                                 \
-       (Current).begin = YYRHSLOC (Rhs, 1).begin;                      \
-       (Current).end   = YYRHSLOC (Rhs, N).end;                        \
-     }                                                                 \
-   else                                                                \
-     {                                                                 \
-       (Current).begin = (Current).end = YYRHSLOC (Rhs, 0).end;        \
-     }                                                                 \
- while (false)
-#endif
+# ifndef YYLLOC_DEFAULT
+#  define YYLLOC_DEFAULT(Current, Rhs, N)                               \
+    do                                                                  \
+      if (N)                                                            \
+        {                                                               \
+          (Current).begin  = YYRHSLOC (Rhs, 1).begin;                   \
+          (Current).end    = YYRHSLOC (Rhs, N).end;                     \
+        }                                                               \
+      else                                                              \
+        {                                                               \
+          (Current).begin = (Current).end = YYRHSLOC (Rhs, 0).end;      \
+        }                                                               \
+    while (/*CONSTCOND*/ false)
+# endif
+
 
 /* Suppress unused-variable warnings by "using" E.  */
 #define YYUSE(e) ((void) (e))
@@ -123,9 +129,9 @@
 #else /* !YYDEBUG */
 
 # define YYCDEBUG if (false) std::cerr
-# define YY_SYMBOL_PRINT(Title, Type, Value, Location)
-# define YY_REDUCE_PRINT(Rule)
-# define YY_STACK_PRINT()
+# define YY_SYMBOL_PRINT(Title, Type, Value, Location) YYUSE(Type)
+# define YY_REDUCE_PRINT(Rule)        static_cast<void>(0)
+# define YY_STACK_PRINT()             static_cast<void>(0)
 
 #endif /* !YYDEBUG */
 
@@ -137,13 +143,11 @@
 #define YYERROR		goto yyerrorlab
 #define YYRECOVERING()  (!!yyerrstatus_)
 
-
-/* Line 382 of lalr1.cc  */
+/* Line 357 of lalr1.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 382 of lalr1.cc  */
-#line 147 "Core/QueryParser/Generated/parser.cpp"
+/* Line 357 of lalr1.cc  */
+#line 151 "Core/QueryParser/Generated/parser.cpp"
 
   /* Return YYSTR after stripping away unnecessary quotes and
      backslashes, so that it's suitable for yyerror.  The heuristic is
@@ -209,11 +213,10 @@
   {
     YYUSE (yylocationp);
     YYUSE (yyvaluep);
-    switch (yytype)
-      {
-         default:
-	  break;
-      }
+    std::ostream& yyo = debug_stream ();
+    std::ostream& yyoutput = yyo;
+    YYUSE (yyoutput);
+    YYUSE (yytype);
   }
 
 
@@ -237,149 +240,120 @@
     YYUSE (yymsg);
     YYUSE (yyvaluep);
 
-    YY_SYMBOL_PRINT (yymsg, yytype, yyvaluep, yylocationp);
+    if (yymsg)
+      YY_SYMBOL_PRINT (yymsg, yytype, yyvaluep, yylocationp);
 
     switch (yytype)
-      {
-        case 3: /* "IDENTIFIER" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 252 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 4: /* "LESS" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
+    {
+      case 3: /* IDENTIFIER */
+/* Line 452 of lalr1.cc  */
+#line 53 "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"
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
 #line 261 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 5: /* "LESSEQUAL" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 270 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 6: /* "EQUAL" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 279 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 7: /* "GREATEREQUAL" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 288 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 8: /* "GREATER" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 297 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 23: /* "query" */
-
-/* Line 480 of lalr1.cc  */
+        break;
+      case 5: /* LESSEQUAL */
+/* Line 452 of lalr1.cc  */
+#line 53 "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"
+        { 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"
+        { 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"
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 289 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 23: /* query */
+/* Line 452 of lalr1.cc  */
 #line 55 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->query); };
-
-/* Line 480 of lalr1.cc  */
-#line 306 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 24: /* "expression" */
-
-/* Line 480 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 315 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 25: /* "parExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
+        { delete ((*yyvaluep).query); };
+/* Line 452 of lalr1.cc  */
+#line 296 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 24: /* expression */
+/* Line 452 of lalr1.cc  */
+#line 54 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 303 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 25: /* parExpression */
+/* Line 452 of lalr1.cc  */
+#line 54 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 310 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 26: /* notExpression */
+/* Line 452 of lalr1.cc  */
+#line 54 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 317 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 27: /* orExpression */
+/* Line 452 of lalr1.cc  */
+#line 54 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
 #line 324 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 26: /* "notExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 333 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 27: /* "orExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 342 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 28: /* "andExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 351 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 29: /* "boolExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 360 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 30: /* "atomicProposition" */
-
-/* Line 480 of lalr1.cc  */
-#line 54 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 369 "Core/QueryParser/Generated/parser.cpp"
-	break;
-      case 31: /* "compareOp" */
-
-/* Line 480 of lalr1.cc  */
+        break;
+      case 28: /* andExpression */
+/* Line 452 of lalr1.cc  */
+#line 54 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 331 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 29: /* boolExpression */
+/* Line 452 of lalr1.cc  */
+#line 54 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 338 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 30: /* atomicProposition */
+/* Line 452 of lalr1.cc  */
+#line 54 "Core/QueryParser/grammar.yy"
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 345 "Core/QueryParser/Generated/parser.cpp"
+        break;
+      case 31: /* compareOp */
+/* Line 452 of lalr1.cc  */
 #line 53 "Core/QueryParser/grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 378 "Core/QueryParser/Generated/parser.cpp"
-	break;
-
-	default:
-	  break;
-      }
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 352 "Core/QueryParser/Generated/parser.cpp"
+        break;
+
+      default:
+        break;
+    }
   }
 
   void
@@ -436,17 +410,18 @@
     int yychar = yyempty_;
     int yytoken = 0;
 
-    /* State.  */
+    // State.
     int yyn;
     int yylen = 0;
     int yystate = 0;
 
-    /* Error handling.  */
+    // Error handling.
     int yynerrs_ = 0;
     int yyerrstatus_ = 0;
 
     /// Semantic value of the lookahead.
-    semantic_type yylval;
+    static semantic_type yyval_default;
+    semantic_type yylval = yyval_default;
     /// Location of the lookahead.
     location_type yylloc;
     /// The locations where the error started and ended.
@@ -459,28 +434,30 @@
 
     int yyresult;
 
+    // FIXME: This shoud be completely indented.  It is not yet to
+    // avoid gratuitous conflicts when merging into the master branch.
+    try
+      {
     YYCDEBUG << "Starting parse" << std::endl;
 
 
-    /* User initialization code.  */
-    
-/* Line 565 of lalr1.cc  */
+/* User initialization code.  */
+/* Line 539 of lalr1.cc  */
 #line 21 "Core/QueryParser/grammar.yy"
 {
   // Initialize the initial location.
   yylloc.begin.filename = yylloc.end.filename = &driver.file;
 }
-
-/* Line 565 of lalr1.cc  */
-#line 476 "Core/QueryParser/Generated/parser.cpp"
+/* Line 539 of lalr1.cc  */
+#line 453 "Core/QueryParser/Generated/parser.cpp"
 
     /* Initialize the stacks.  The initial state will be pushed in
        yynewstate, since the latter expects the semantical and the
        location values to have been already stored, initialize these
        stacks with a primary value.  */
-    yystate_stack_ = state_stack_type (0);
-    yysemantic_stack_ = semantic_stack_type (0);
-    yylocation_stack_ = location_stack_type (0);
+    yystate_stack_.clear ();
+    yysemantic_stack_.clear ();
+    yylocation_stack_.clear ();
     yysemantic_stack_.push (yylval);
     yylocation_stack_.push (yylloc);
 
@@ -506,11 +483,10 @@
     /* Read a lookahead token.  */
     if (yychar == yyempty_)
       {
-	YYCDEBUG << "Reading a token: ";
-	yychar = yylex (&yylval, &yylloc, driver);
+        YYCDEBUG << "Reading a token: ";
+        yychar = yylex (&yylval, &yylloc, driver);
       }
 
-
     /* Convert token to internal form.  */
     if (yychar <= yyeof_)
       {
@@ -581,128 +557,114 @@
     else
       yyval = yysemantic_stack_[0];
 
+    // Compute the default @$.
     {
       slice<location_type, location_stack_type> slice (yylocation_stack_, yylen);
       YYLLOC_DEFAULT (yyloc, slice, yylen);
     }
+
+    // Perform the reduction.
     YY_REDUCE_PRINT (yyn);
     switch (yyn)
       {
-	  case 2:
-
-/* Line 690 of lalr1.cc  */
+          case 2:
+/* Line 664 of lalr1.cc  */
 #line 59 "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 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 60 "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 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 61 "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 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 62 "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 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 65 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 7:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 66 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 8:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 67 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 9:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 68 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 10:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 69 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 11:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 70 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 12:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 76 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::ParExpression((yysemantic_stack_[(3) - (2)].expr)); }
     break;
 
   case 13:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 77 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::NotExpression((yysemantic_stack_[(2) - (2)].expr)); }
     break;
 
   case 14:
-
-/* Line 690 of lalr1.cc  */
+/* 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)); }
     break;
 
   case 15:
-
-/* Line 690 of lalr1.cc  */
+/* 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)); }
     break;
 
   case 16:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 80 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(true); }
     break;
 
   case 17:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 81 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(false); }
     break;
 
   case 18:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 83 "Core/QueryParser/grammar.yy"
     { 
 		int placeIndex = driver.getTAPN().getPlaceIndex(*(yysemantic_stack_[(3) - (1)].string));
@@ -712,19 +674,18 @@
     break;
 
   case 19:
-
-/* Line 690 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 87 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::DeadlockExpression(); }
     break;
 
 
-
-/* Line 690 of lalr1.cc  */
-#line 725 "Core/QueryParser/Generated/parser.cpp"
-	default:
-          break;
+/* Line 664 of lalr1.cc  */
+#line 685 "Core/QueryParser/Generated/parser.cpp"
+      default:
+        break;
       }
+
     /* User semantic actions sometimes alter yychar, and that requires
        that yytoken be updated with the new translation.  We take the
        approach of translating immediately before every use of yytoken.
@@ -775,20 +736,19 @@
     yyerror_range[1] = yylloc;
     if (yyerrstatus_ == 3)
       {
-	/* If just tried and failed to reuse lookahead token after an
-	 error, discard it.  */
-
-	if (yychar <= yyeof_)
-	  {
-	  /* Return failure if at end of input.  */
-	  if (yychar == yyeof_)
-	    YYABORT;
-	  }
-	else
-	  {
-	    yydestruct_ ("Error: discarding", yytoken, &yylval, &yylloc);
-	    yychar = yyempty_;
-	  }
+        /* If just tried and failed to reuse lookahead token after an
+           error, discard it.  */
+        if (yychar <= yyeof_)
+          {
+            /* Return failure if at end of input.  */
+            if (yychar == yyeof_)
+              YYABORT;
+          }
+        else
+          {
+            yydestruct_ ("Error: discarding", yytoken, &yylval, &yylloc);
+            yychar = yyempty_;
+          }
       }
 
     /* Else will try to reuse lookahead token after shifting the error
@@ -837,7 +797,7 @@
 
 	/* Pop the current state because it cannot handle the error token.  */
 	if (yystate_stack_.height () == 1)
-	YYABORT;
+	  YYABORT;
 
 	yyerror_range[1] = yylocation_stack_[0];
 	yydestruct_ ("Error: popping",
@@ -885,16 +845,42 @@
     /* Do not reclaim the symbols of the rule which action triggered
        this YYABORT or YYACCEPT.  */
     yypop_ (yylen);
-    while (yystate_stack_.height () != 1)
+    while (1 < yystate_stack_.height ())
       {
-	yydestruct_ ("Cleanup: popping",
-		   yystos_[yystate_stack_[0]],
-		   &yysemantic_stack_[0],
-		   &yylocation_stack_[0]);
-	yypop_ ();
+        yydestruct_ ("Cleanup: popping",
+                     yystos_[yystate_stack_[0]],
+                     &yysemantic_stack_[0],
+                     &yylocation_stack_[0]);
+        yypop_ ();
       }
 
     return yyresult;
+    }
+    catch (...)
+      {
+        YYCDEBUG << "Exception caught: cleaning lookahead and stack"
+                 << std::endl;
+        // Do not try to display the values of the reclaimed symbols,
+        // as their printer might throw an exception.
+        if (yychar != yyempty_)
+          {
+            /* Make sure we have latest lookahead translation.  See
+               comments at user semantic actions for why this is
+               necessary.  */
+            yytoken = yytranslate_ (yychar);
+            yydestruct_ (YY_NULL, yytoken, &yylval, &yylloc);
+          }
+
+        while (1 < yystate_stack_.height ())
+          {
+            yydestruct_ (YY_NULL,
+                         yystos_[yystate_stack_[0]],
+                         &yysemantic_stack_[0],
+                         &yylocation_stack_[0]);
+            yypop_ ();
+          }
+        throw;
+      }
   }
 
   // Generate an error message.
@@ -963,7 +949,7 @@
           }
       }
 
-    char const* yyformat = 0;
+    char const* yyformat = YY_NULL;
     switch (yycount)
       {
 #define YYCASE_(N, S)                         \
@@ -1095,7 +1081,7 @@
        1,     1,     1,     1,     1
   };
 
-#if YYDEBUG || YYERROR_VERBOSE || YYTOKEN_TABLE
+
   /* YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM.
      First, the terminals, then, starting at \a yyntokens_, nonterminals.  */
   const char*
@@ -1106,9 +1092,8 @@
   "LPARAN", "RPARAN", "OR", "AND", "NOT", "BOOL_TRUE", "BOOL_FALSE",
   "DEADLOCK", "$accept", "query", "expression", "parExpression",
   "notExpression", "orExpression", "andExpression", "boolExpression",
-  "atomicProposition", "compareOp", 0
+  "atomicProposition", "compareOp", YY_NULL
   };
-#endif
 
 #if YYDEBUG
   /* YYRHS -- A `-1'-separated list of the rules' RHS.  */
@@ -1227,16 +1212,12 @@
   const unsigned int Parser::yyuser_token_number_max_ = 276;
   const Parser::token_number_type Parser::yyundef_token_ = 2;
 
-
-/* Line 1136 of lalr1.cc  */
+/* Line 1135 of lalr1.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
+/* Line 1135 of lalr1.cc  */
+#line 1220 "Core/QueryParser/Generated/parser.cpp"
 /* Line 1136 of lalr1.cc  */
-#line 1237 "Core/QueryParser/Generated/parser.cpp"
-
-
-/* Line 1138 of lalr1.cc  */
 #line 90 "Core/QueryParser/grammar.yy"
 
 
@@ -1247,4 +1228,3 @@
 	driver.error (l, m);
 	exit(1);
 }
-

=== modified file 'src/Core/QueryParser/Generated/parser.hpp'
--- src/Core/QueryParser/Generated/parser.hpp	2013-06-04 11:39:54 +0000
+++ src/Core/QueryParser/Generated/parser.hpp	2013-08-26 13:51:29 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Skeleton interface for Bison LALR(1) parsers in C++
    
-      Copyright (C) 2002-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2013 Free Software Foundation, Inc.
    
    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
@@ -30,14 +30,18 @@
    This special exception was added by the Free Software Foundation in
    version 2.2 of Bison.  */
 
+/**
+ ** \file Core/QueryParser/Generated/parser.hpp
+ ** Define the VerifyTAPN::parser class.
+ */
+
 /* C++ LALR(1) parser skeleton written by Akim Demaille.  */
 
-#ifndef PARSER_HEADER_H
-# define PARSER_HEADER_H
+#ifndef YY_YY_CORE_QUERYPARSER_GENERATED_PARSER_HPP_INCLUDED
+# define YY_YY_CORE_QUERYPARSER_GENERATED_PARSER_HPP_INCLUDED
 
 /* "%code requires" blocks.  */
-
-/* Line 35 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 7 "Core/QueryParser/grammar.yy"
 
 # include <string>
@@ -47,9 +51,8 @@
 }
 
 
-
-/* Line 35 of lalr1.cc  */
-#line 53 "Core/QueryParser/Generated/parser.hpp"
+/* Line 33 of lalr1.cc  */
+#line 56 "Core/QueryParser/Generated/parser.hpp"
 
 
 #include <string>
@@ -62,26 +65,11 @@
 # define YYDEBUG 0
 #endif
 
-/* Enabling verbose error messages.  */
-#ifdef YYERROR_VERBOSE
-# undef YYERROR_VERBOSE
-# define YYERROR_VERBOSE 1
-#else
-# define YYERROR_VERBOSE 1
-#endif
-
-/* Enabling the token table.  */
-#ifndef YYTOKEN_TABLE
-# define YYTOKEN_TABLE 0
-#endif
-
-
-/* Line 35 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 35 of lalr1.cc  */
-#line 85 "Core/QueryParser/Generated/parser.hpp"
+/* Line 33 of lalr1.cc  */
+#line 73 "Core/QueryParser/Generated/parser.hpp"
 
   /// A Bison parser.
   class Parser
@@ -91,8 +79,7 @@
 #ifndef YYSTYPE
     union semantic_type
     {
-
-/* Line 35 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 30 "Core/QueryParser/grammar.yy"
 
 	int          					number;
@@ -101,9 +88,8 @@
 	VerifyTAPN::AST::Query*		 	query;
 
 
-
-/* Line 35 of lalr1.cc  */
-#line 107 "Core/QueryParser/Generated/parser.hpp"
+/* Line 33 of lalr1.cc  */
+#line 93 "Core/QueryParser/Generated/parser.hpp"
     };
 #else
     typedef YYSTYPE semantic_type;
@@ -164,6 +150,10 @@
 #endif
 
   private:
+    /// This class is not copyable.
+    Parser (const Parser&);
+    Parser& operator= (const Parser&);
+
     /// Report a syntax error.
     /// \param loc    where the syntax error is found.
     /// \param msg    a description of the syntax error.
@@ -247,16 +237,14 @@
     /// For a rule, its LHS.
     static const unsigned char yyr1_[];
     /// For a rule, its RHS length.
-    static const unsigned char yyr2_[];
-
-#if YYDEBUG || YYERROR_VERBOSE || YYTOKEN_TABLE
+    static const unsigned char yyr2_[]; 
+
+    /// Convert the symbol name \a n to a form suitable for a diagnostic.
+    static std::string yytnamerr_ (const char *n);
+
+
     /// For a symbol, its name in clear.
     static const char* const yytname_[];
-#endif
-
-    /// Convert the symbol name \a n to a form suitable for a diagnostic.
-    static std::string yytnamerr_ (const char *n);
-
 #if YYDEBUG
     /// A type to store symbol numbers and -1.
     typedef signed char rhs_number_type;
@@ -283,6 +271,7 @@
 
     /// \brief Reclaim the memory associated to a symbol.
     /// \param yymsg        Why this token is reclaimed.
+    ///                     If null, do not display the symbol, just free it.
     /// \param yytype       The symbol type.
     /// \param yyvaluep     Its semantic value.
     /// \param yylocationp  Its location.
@@ -310,14 +299,12 @@
     /* User arguments.  */
     VerifyTAPN::TAPNQueryParser& driver;
   };
-
-/* Line 35 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
-/* Line 35 of lalr1.cc  */
-#line 320 "Core/QueryParser/Generated/parser.hpp"
-
-
-
-#endif /* ! defined PARSER_HEADER_H */
+/* Line 33 of lalr1.cc  */
+#line 307 "Core/QueryParser/Generated/parser.hpp"
+
+
+
+#endif /* !YY_YY_CORE_QUERYPARSER_GENERATED_PARSER_HPP_INCLUDED  */

=== modified file 'src/Core/QueryParser/Generated/position.hh'
--- src/Core/QueryParser/Generated/position.hh	2013-06-04 11:39:54 +0000
+++ src/Core/QueryParser/Generated/position.hh	2013-08-26 13:51:29 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Positions for Bison parsers in C++
    
-      Copyright (C) 2002-2007, 2009-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2007, 2009-2013 Free Software Foundation, Inc.
    
    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
@@ -31,62 +31,72 @@
    version 2.2 of Bison.  */
 
 /**
- ** \file position.hh
+ ** \file Core/QueryParser/Generated/position.hh
  ** Define the VerifyTAPN::position class.
  */
 
-#ifndef BISON_POSITION_HH
-# define BISON_POSITION_HH
+#ifndef YY_YY_CORE_QUERYPARSER_GENERATED_POSITION_HH_INCLUDED
+# define YY_YY_CORE_QUERYPARSER_GENERATED_POSITION_HH_INCLUDED
 
+# include <algorithm> // std::max
 # include <iostream>
 # include <string>
-# include <algorithm>
-
-
-/* Line 37 of location.cc  */
+
+# ifndef YY_NULL
+#  if defined __cplusplus && 201103L <= __cplusplus
+#   define YY_NULL nullptr
+#  else
+#   define YY_NULL 0
+#  endif
+# endif
+
+/* Line 36 of location.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 37 of location.cc  */
-#line 52 "Core/QueryParser/Generated/position.hh"
+/* Line 36 of location.cc  */
+#line 58 "Core/QueryParser/Generated/position.hh"
   /// Abstract a position.
   class position
   {
   public:
 
     /// Construct a position.
-    position ()
-      : filename (0), line (1), column (1)
+    explicit position (std::string* f = YY_NULL,
+                       unsigned int l = 1u,
+                       unsigned int c = 1u)
+      : filename (f)
+      , line (l)
+      , column (c)
     {
     }
 
 
     /// Initialization.
-    inline void initialize (std::string* fn)
+    void initialize (std::string* fn = YY_NULL,
+                     unsigned int l = 1u,
+                     unsigned int c = 1u)
     {
       filename = fn;
-      line = 1;
-      column = 1;
+      line = l;
+      column = c;
     }
 
     /** \name Line and Column related manipulators
      ** \{ */
-  public:
     /// (line related) Advance to the COUNT next lines.
-    inline void lines (int count = 1)
+    void lines (int count = 1)
     {
-      column = 1;
+      column = 1u;
       line += count;
     }
 
     /// (column related) Advance to the COUNT next columns.
-    inline void columns (int count = 1)
+    void columns (int count = 1)
     {
       column = std::max (1u, column + count);
     }
     /** \} */
 
-  public:
     /// File name to which this position refers.
     std::string* filename;
     /// Current line number.
@@ -96,7 +106,7 @@
   };
 
   /// Add and assign a position.
-  inline const position&
+  inline position&
   operator+= (position& res, const int width)
   {
     res.columns (width);
@@ -112,7 +122,7 @@
   }
 
   /// Add and assign a position.
-  inline const position&
+  inline position&
   operator-= (position& res, const int width)
   {
     return res += -width;
@@ -147,19 +157,18 @@
    ** \param ostr the destination output stream
    ** \param pos a reference to the position to redirect
    */
-  inline std::ostream&
-  operator<< (std::ostream& ostr, const position& pos)
+  template <typename YYChar>
+  inline std::basic_ostream<YYChar>&
+  operator<< (std::basic_ostream<YYChar>& ostr, const position& pos)
   {
     if (pos.filename)
       ostr << *pos.filename << ':';
     return ostr << pos.line << '.' << pos.column;
   }
 
-
-/* Line 144 of location.cc  */
+/* Line 148 of location.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
-/* Line 144 of location.cc  */
-#line 165 "Core/QueryParser/Generated/position.hh"
-#endif // not BISON_POSITION_HH
+/* Line 148 of location.cc  */
+#line 174 "Core/QueryParser/Generated/position.hh"
+#endif /* !YY_YY_CORE_QUERYPARSER_GENERATED_POSITION_HH_INCLUDED  */

=== modified file 'src/Core/QueryParser/Generated/stack.hh'
--- src/Core/QueryParser/Generated/stack.hh	2013-06-04 11:39:54 +0000
+++ src/Core/QueryParser/Generated/stack.hh	2013-08-26 13:51:29 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Stack handling for Bison parsers in C++
    
-      Copyright (C) 2002-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2013 Free Software Foundation, Inc.
    
    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
@@ -30,23 +30,25 @@
    This special exception was added by the Free Software Foundation in
    version 2.2 of Bison.  */
 
-#ifndef BISON_STACK_HH
-# define BISON_STACK_HH
-
-#include <deque>
-
-
-/* Line 1149 of lalr1.cc  */
+/**
+ ** \file Core/QueryParser/Generated/stack.hh
+ ** Define the VerifyTAPN::stack class.
+ */
+
+#ifndef YY_YY_CORE_QUERYPARSER_GENERATED_STACK_HH_INCLUDED
+# define YY_YY_CORE_QUERYPARSER_GENERATED_STACK_HH_INCLUDED
+
+# include <deque>
+
+/* Line 34 of stack.hh  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 1149 of lalr1.cc  */
-#line 45 "Core/QueryParser/Generated/stack.hh"
+/* Line 34 of stack.hh  */
+#line 48 "Core/QueryParser/Generated/stack.hh"
   template <class T, class S = std::deque<T> >
   class stack
   {
   public:
-
     // Hide our reversed order.
     typedef typename S::reverse_iterator iterator;
     typedef typename S::const_reverse_iterator const_iterator;
@@ -85,7 +87,13 @@
     pop (unsigned int n = 1)
     {
       for (; n; --n)
-	seq_.pop_front ();
+        seq_.pop_front ();
+    }
+
+    void
+    clear ()
+    {
+      seq_.clear ();
     }
 
     inline
@@ -99,7 +107,8 @@
     inline const_iterator end () const { return seq_.rend (); }
 
   private:
-
+    stack (const stack&);
+    stack& operator= (const stack&);
     S seq_;
   };
 
@@ -108,10 +117,9 @@
   class slice
   {
   public:
-
-    slice (const S& stack,
-	   unsigned int range) : stack_ (stack),
-				 range_ (range)
+    slice (const S& stack, unsigned int range)
+      : stack_ (stack)
+      , range_ (range)
     {
     }
 
@@ -123,17 +131,13 @@
     }
 
   private:
-
     const S& stack_;
     unsigned int range_;
   };
-
-/* Line 1235 of lalr1.cc  */
+/* Line 124 of stack.hh  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
-/* Line 1235 of lalr1.cc  */
-#line 137 "Core/QueryParser/Generated/stack.hh"
-
-#endif // not BISON_STACK_HH[]dnl
-
+/* Line 124 of stack.hh  */
+#line 142 "Core/QueryParser/Generated/stack.hh"
+
+#endif /* !YY_YY_CORE_QUERYPARSER_GENERATED_STACK_HH_INCLUDED  */

=== modified file 'src/Core/QueryParser/NormalizationVisitor.cpp'
--- src/Core/QueryParser/NormalizationVisitor.cpp	2013-08-12 15:06:44 +0000
+++ src/Core/QueryParser/NormalizationVisitor.cpp	2013-08-26 13:51:29 +0000
@@ -5,63 +5,56 @@
 {
 	namespace AST
 	{
-		struct Tuple{
-			bool negate;
-			Expression* returnExpr;
-
-		public:
-			Tuple(bool negate, Expression* expr) : negate(negate), returnExpr(expr) {};
-		};
-
-		void NormalizationVisitor::visit(const NotExpression& expr, boost::any& context)
-		{
-			Tuple& tuple = boost::any_cast<Tuple&>(context);
-			boost::any any = Tuple(!tuple.negate, NULL);
-			expr.getChild().accept(*this, any);
-			tuple.returnExpr = boost::any_cast<Tuple&>(any).returnExpr;
-		}
-
-		void NormalizationVisitor::visit(const ParExpression& expr, boost::any& context)
-		{
-			Tuple& tuple = boost::any_cast<Tuple&>(context);
-			boost::any any = Tuple(tuple.negate, NULL);
-			expr.getChild().accept(*this, any);
-			tuple.returnExpr = new ParExpression(boost::any_cast<Tuple&>(any).returnExpr);
-		}
-
-		void NormalizationVisitor::visit(const OrExpression& expr, boost::any& context)
-		{
-			Tuple& tuple = boost::any_cast<Tuple&>(context);
-			boost::any left = Tuple(tuple.negate, NULL), right = Tuple(tuple.negate, NULL);
-			if(tuple.negate){
-				expr.getLeft().accept(*this, left);
-				expr.getRight().accept(*this, right);
-				tuple.returnExpr = new AndExpression(boost::any_cast<Tuple&>(left).returnExpr, boost::any_cast<Tuple&>(right).returnExpr);
-			}else{
-				expr.getLeft().accept(*this, left);
-				expr.getRight().accept(*this, right);
-				tuple.returnExpr = new OrExpression(boost::any_cast<Tuple&>(left).returnExpr, boost::any_cast<Tuple&>(right).returnExpr);
-			}
-		}
-
-		void NormalizationVisitor::visit(const AndExpression& expr, boost::any& context)
-		{
-			Tuple& tuple = boost::any_cast<Tuple&>(context);
-			boost::any left = Tuple(tuple.negate, NULL), right = Tuple(tuple.negate, NULL);
-			if(tuple.negate){
-				expr.getLeft().accept(*this, left);
-				expr.getRight().accept(*this, right);
-				tuple.returnExpr = new OrExpression(boost::any_cast<Tuple&>(left).returnExpr, boost::any_cast<Tuple&>(right).returnExpr);
-			}else{
-				expr.getLeft().accept(*this, left);
-				expr.getRight().accept(*this, right);
-				tuple.returnExpr = new AndExpression(boost::any_cast<Tuple&>(left).returnExpr, boost::any_cast<Tuple&>(right).returnExpr);
-			}
-		}
-
-		void NormalizationVisitor::visit(const AtomicProposition& expr, boost::any& context)
-		{
-			Tuple& tuple = boost::any_cast<Tuple&>(context);
+
+		void NormalizationVisitor::visit(const NotExpression& expr, Result& context)
+		{
+			Tuple& tuple = static_cast<Tuple&>(context);
+			Tuple any = Tuple(!tuple.negate, NULL);
+			expr.getChild().accept(*this, any);
+			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);
+			Tuple left = Tuple(tuple.negate, NULL), right = Tuple(tuple.negate, NULL);
+			if(tuple.negate){
+				expr.getLeft().accept(*this, left);
+				expr.getRight().accept(*this, right);
+				tuple.returnExpr = new AndExpression(static_cast<Tuple&>(left).returnExpr, static_cast<Tuple&>(right).returnExpr);
+			}else{
+				expr.getLeft().accept(*this, left);
+				expr.getRight().accept(*this, right);
+				tuple.returnExpr = new OrExpression(static_cast<Tuple&>(left).returnExpr, static_cast<Tuple&>(right).returnExpr);
+			}
+		}
+
+		void NormalizationVisitor::visit(const AndExpression& expr, Result& context)
+		{
+			Tuple& tuple = static_cast<Tuple&>(context);
+			Tuple left = Tuple(tuple.negate, NULL), right = Tuple(tuple.negate, NULL);
+			if(tuple.negate){
+				expr.getLeft().accept(*this, left);
+				expr.getRight().accept(*this, right);
+				tuple.returnExpr = new OrExpression(static_cast<Tuple&>(left).returnExpr, static_cast<Tuple&>(right).returnExpr);
+			}else{
+				expr.getLeft().accept(*this, left);
+				expr.getRight().accept(*this, right);
+				tuple.returnExpr = new AndExpression(static_cast<Tuple&>(left).returnExpr, static_cast<Tuple&>(right).returnExpr);
+			}
+		}
+
+		void NormalizationVisitor::visit(const AtomicProposition& expr, Result& context)
+		{
+			Tuple& tuple = static_cast<Tuple&>(context);
 			std::string op;
 			if(tuple.negate){
 				op = negateOperator(expr.getOperator());
@@ -71,15 +64,14 @@
 			tuple.returnExpr = new AtomicProposition(expr.getPlace(), &op, expr.getNumberOfTokens());
 		}
 
-               void NormalizationVisitor::visit(const DeadlockExpression& expr, boost::any& context) {
-			Tuple& tuple = boost::any_cast<Tuple&>(context);
+               void NormalizationVisitor::visit(const DeadlockExpression& expr, Result& context) {
+			Tuple& tuple = static_cast<Tuple&>(context);
 			tuple.returnExpr = new DeadlockExpression();                  
                 }
                 
-
-		void NormalizationVisitor::visit(const BoolExpression& expr, boost::any& context)
+		void NormalizationVisitor::visit(const BoolExpression& expr, Result& context)
 		{
-			Tuple& tuple = boost::any_cast<Tuple&>(context);
+			Tuple& tuple = static_cast<Tuple&>(context);
 			if(tuple.negate){
 				tuple.returnExpr = new BoolExpression(!expr.getValue());
 			}else{
@@ -87,12 +79,12 @@
 			}
 		}
 
-		void NormalizationVisitor::visit(const Query& query, boost::any& context)
+		void NormalizationVisitor::visit(const Query& query, Result& context)
 		{
-			boost::any any = Tuple(false, NULL);
+			Tuple any = Tuple(false, NULL);
 			query.getChild().accept(*this, any);
 
-			normalizedQuery = new AST::Query(query.getQuantifier(), boost::any_cast<Tuple&>(any).returnExpr);
+			normalizedQuery = new AST::Query(query.getQuantifier(), static_cast<Tuple&>(any).returnExpr);
 		}
 
 		std::string NormalizationVisitor::negateOperator(const std::string& op) const{

=== modified file 'src/Core/QueryParser/NormalizationVisitor.hpp'
--- src/Core/QueryParser/NormalizationVisitor.hpp	2013-06-30 14:56:38 +0000
+++ src/Core/QueryParser/NormalizationVisitor.hpp	2013-08-26 13:51:29 +0000
@@ -14,23 +14,29 @@
 
 namespace VerifyTAPN {
 	namespace AST {
-
+                class  Tuple : public Result {
+                    public:
+			bool negate;
+			Expression* returnExpr;
+			Tuple(bool negate, Expression* expr) : negate(negate), returnExpr(expr) {};
+		};
+                
 		class NormalizationVisitor : public Visitor
 		{
 		public:
 			NormalizationVisitor() : normalizedQuery() { };
 			virtual ~NormalizationVisitor() {};
 
-			virtual void visit(const NotExpression& expr, boost::any& context);
-			virtual void visit(const ParExpression& expr, boost::any& context);
-			virtual void visit(const OrExpression& expr, boost::any& context);
-			virtual void visit(const AndExpression& expr, boost::any& context);
-			virtual void visit(const AtomicProposition& expr, boost::any& context);
-			virtual void visit(const BoolExpression& expr, boost::any& context);
-			virtual void visit(const Query& query, boost::any& context);
-			virtual void visit(const DeadlockExpression& expr, boost::any& context);
+			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);
 
-			AST::Query* normalize(const AST::Query& query) { boost::any any; query.accept(*this, any); 
+			AST::Query* normalize(const AST::Query& query) { Tuple any(false, NULL); query.accept(*this, any); 
                         return normalizedQuery; };
 		private:
 			std::string negateOperator(const std::string& op) const;

=== modified file 'src/Core/QueryParser/Visitor.hpp'
--- src/Core/QueryParser/Visitor.hpp	2013-06-04 11:39:54 +0000
+++ src/Core/QueryParser/Visitor.hpp	2013-08-26 13:51:29 +0000
@@ -1,7 +1,7 @@
 #ifndef VISITOR_HPP_
 #define VISITOR_HPP_
 
-#include "boost/any.hpp"
+#include <vector>
 
 namespace VerifyTAPN
 {
@@ -15,19 +15,26 @@
                 class DeadlockExpression;
 		class BoolExpression;
 		class Query;
-
+                
+                class Result {};
+                template<typename T>
+                class SpecificResult : public Result { public: T value; };
+                typedef SpecificResult<int> IntResult;
+                typedef SpecificResult<bool> BoolResult;
+                typedef SpecificResult<std::vector<int> > IntVectorResult;
+                
 		class Visitor
 		{
 		public:
 			virtual ~Visitor() { };
-			virtual void visit(const NotExpression& expr, boost::any& context) = 0;
-			virtual void visit(const ParExpression& expr, boost::any& context) = 0;
-			virtual void visit(const OrExpression& expr, boost::any& context) = 0;
-			virtual void visit(const AndExpression& expr, boost::any& context) = 0;
-			virtual void visit(const AtomicProposition& expr, boost::any& context) = 0;
-			virtual void visit(const BoolExpression& expr, boost::any& context) = 0;
-			virtual void visit(const Query& query, boost::any& context) = 0;
-                        virtual void visit(const DeadlockExpression& expr, boost::any& context) = 0;
+			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;
 		};
 	}
 }

=== modified file 'src/Core/TAPN/InhibitorArc.cpp'
--- src/Core/TAPN/InhibitorArc.cpp	2013-05-08 15:10:14 +0000
+++ src/Core/TAPN/InhibitorArc.cpp	2013-08-26 13:51:29 +0000
@@ -6,7 +6,7 @@
 	namespace TAPN {
 		void InhibitorArc::print(std::ostream& out) const
 		{
-			out << "From " << place->getName() << " to " << transition->getName() << " weight: " << weight;
+			out << "From " << place.getName() << " to " << transition.getName() << " weight: " << weight;
 		}
 	}
 }

=== modified file 'src/Core/TAPN/InhibitorArc.hpp'
--- src/Core/TAPN/InhibitorArc.hpp	2013-05-08 11:57:14 +0000
+++ src/Core/TAPN/InhibitorArc.hpp	2013-08-26 13:51:29 +0000
@@ -3,7 +3,6 @@
 
 #include <vector>
 #include "TimeInterval.hpp"
-#include "boost/smart_ptr.hpp"
 
 namespace VerifyTAPN {
 	namespace TAPN {
@@ -12,22 +11,21 @@
 
 		class InhibitorArc {
 			public: // typedefs
-				typedef std::vector< boost::shared_ptr<InhibitorArc> > Vector;
-				typedef std::vector< boost::weak_ptr<InhibitorArc> > WeakPtrVector;
+				typedef std::vector<InhibitorArc*> Vector;
 			public:
-				InhibitorArc(const boost::shared_ptr<TimedPlace>& place, const boost::shared_ptr<TimedTransition>& transition, const int weight) : place(place), transition(transition), weight(weight) { };
+				InhibitorArc(TimedPlace& place, TimedTransition& transition, const int weight) : place(place), transition(transition), weight(weight) { };
 				virtual ~InhibitorArc() { /* empty */ }
 
 			public: // modifiers
-				inline TimedPlace& getInputPlace() { return *place; }
-				inline TimedTransition& getOutputTransition() { return *transition; }
+				inline TimedPlace& getInputPlace() const { return place; }
+				inline TimedTransition& getOutputTransition() const { return transition; }
 
 			public: // Inspectors
 				void print(std::ostream& out) const;
 				inline const int getWeight() const { return weight; }
 			private:
-				const boost::shared_ptr<TimedPlace> place;
-				const boost::shared_ptr<TimedTransition> transition;
+				TimedPlace& place;
+				TimedTransition& transition;
 				const int weight;
 		};
 

=== modified file 'src/Core/TAPN/OutputArc.cpp'
--- src/Core/TAPN/OutputArc.cpp	2013-05-08 15:10:14 +0000
+++ src/Core/TAPN/OutputArc.cpp	2013-08-26 13:51:29 +0000
@@ -6,17 +6,17 @@
 	namespace TAPN {
 		void OutputArc::print(std::ostream& out) const
 		{
-			out << "From " << transition->getName() << " to " << place->getName() << " weight: " << weight;
-		}
-
-		TimedPlace& OutputArc::getOutputPlace()
-		{
-			return *place;
-		}
-
-		TimedTransition& OutputArc::getInputTransition()
-		{
-			return *transition;
+			out << "From " << transition.getName() << " to " << place.getName() << " weight: " << weight;
+		}
+
+		TimedPlace& OutputArc::getOutputPlace() const
+		{
+			return place;
+		}
+
+		TimedTransition& OutputArc::getInputTransition() const
+		{
+			return transition;
 		}
 	}
 }

=== modified file 'src/Core/TAPN/OutputArc.hpp'
--- src/Core/TAPN/OutputArc.hpp	2013-05-08 12:01:52 +0000
+++ src/Core/TAPN/OutputArc.hpp	2013-08-26 13:51:29 +0000
@@ -2,7 +2,7 @@
 #define VERIFYTAPN_TAPN_OUTPUTARC_HPP_
 
 #include <vector>
-#include "boost/smart_ptr.hpp"
+#include <iostream>
 
 namespace VerifyTAPN {
 	namespace TAPN {
@@ -12,23 +12,22 @@
 		class OutputArc
 		{
 		public: // typedefs
-			typedef std::vector< boost::shared_ptr<OutputArc> > Vector;
-			typedef std::vector< boost::weak_ptr<OutputArc> > WeakPtrVector;
+			typedef std::vector< OutputArc* > Vector;
 		public:
-			OutputArc(const boost::shared_ptr<TimedTransition>& transition, const boost::shared_ptr<TimedPlace>& place, const int weight)
+			OutputArc(TimedTransition& transition, TimedPlace& place, const int weight)
 				: transition(transition), place(place), weight(weight) { };
 			virtual ~OutputArc() { /* empty */ }
 
 		public: // modifiers
-			TimedPlace& getOutputPlace();
-			TimedTransition& getInputTransition();
+			TimedPlace& getOutputPlace() const;
+			TimedTransition& getInputTransition() const;
 
 		public: // inspectors
 			void print(std::ostream& out) const;
 			inline const int getWeight() const { return weight; }
 		private:
-			const boost::shared_ptr<TimedTransition> transition;
-			const boost::shared_ptr<TimedPlace> place;
+			TimedTransition& transition;
+			TimedPlace& place;
 			const int weight;
 		};
 

=== modified file 'src/Core/TAPN/TimedArcPetriNet.cpp'
--- src/Core/TAPN/TimedArcPetriNet.cpp	2013-08-13 18:19:17 +0000
+++ src/Core/TAPN/TimedArcPetriNet.cpp	2013-08-26 13:51:29 +0000
@@ -16,34 +16,34 @@
 				transitions[i]->setIndex(i);
 			}
 
-			for(TimedInputArc::Vector::const_iterator iter = inputArcs.begin(); iter != inputArcs.end(); ++iter)
-			{
-				const boost::shared_ptr<TimedInputArc>& arc = *iter;
-				arc->getOutputTransition().addToPreset(arc);
-				arc->getInputPlace().addInputArc(arc);
-				updateMaxConstant(arc->getInterval());
-			}
-
-			for(TransportArc::Vector::const_iterator iter = transportArcs.begin(); iter != transportArcs.end(); ++iter)
-			{
-				const boost::shared_ptr<TransportArc>& arc = *iter;
-				arc->getTransition().addTransportArcGoingThrough(arc);
-				arc->getSource().addTransportArc(arc);
-				updateMaxConstant(arc->getInterval());
-			}
-
-			for(InhibitorArc::Vector::const_iterator iter = inhibitorArcs.begin(); iter != inhibitorArcs.end(); ++iter) {
-				const boost::shared_ptr<InhibitorArc>& arc = *iter;
-				arc->getOutputTransition().addIncomingInhibitorArc(arc);
-				arc->getInputPlace().addInhibitorArc(arc);
+			for(TimedInputArc::Vector::iterator iter = inputArcs.begin(); iter != inputArcs.end(); ++iter)
+			{
+                                TimedInputArc* arc = *iter;
+				arc->getOutputTransition().addToPreset(*arc);
+				arc->getInputPlace().addInputArc(*arc);
+				updateMaxConstant(arc->getInterval());
+			}
+
+			for(TransportArc::Vector::iterator iter = transportArcs.begin(); iter != transportArcs.end(); ++iter)
+			{
+				TransportArc* arc = *iter;
+				arc->getTransition().addTransportArcGoingThrough(*arc);
+				arc->getSource().addTransportArc(*arc);
+				updateMaxConstant(arc->getInterval());
+			}
+
+			for(InhibitorArc::Vector::iterator iter = inhibitorArcs.begin(); iter != inhibitorArcs.end(); ++iter) {
+				InhibitorArc* arc = *iter;
+				arc->getOutputTransition().addIncomingInhibitorArc(*arc);
+				arc->getInputPlace().addInhibitorArc(*arc);
 				arc->getInputPlace().setHasInhibitorArcs(true);
 			}
 
-			for(OutputArc::Vector::const_iterator iter = outputArcs.begin(); iter != outputArcs.end(); ++iter)
+			for(OutputArc::Vector::iterator iter = outputArcs.begin(); iter != outputArcs.end(); ++iter)
 			{
-				const boost::shared_ptr<OutputArc>& arc = *iter;
-				arc->getInputTransition().addToPostset(arc);
-				arc->getOutputPlace().addOutputArc(arc);
+				OutputArc* arc = *iter;
+				arc->getInputTransition().addToPostset(*arc);
+				arc->getOutputPlace().addOutputArc(*arc);
 			}
 
 
@@ -117,7 +117,7 @@
 					{
 						if((*arcIter)->getInputPlace() == **iter)
 						{
-							boost::shared_ptr<TimedInputArc> ia = *arcIter;
+							TimedInputArc* ia = *arcIter;
 							const TAPN::TimeInterval& interval = ia->getInterval();
 
 							const int lowerBound = interval.getLowerBound();
@@ -140,7 +140,7 @@
 						if((*transport_iter)->getSource() == **iter)
 						{
 							int maxArc = -1;
-							boost::shared_ptr<TransportArc> ta = *transport_iter;
+							TransportArc* ta = *transport_iter;
 							const TAPN::TimeInterval& interval = ta->getInterval();
 							const int lowerBound = interval.getLowerBound();
 							const int upperBound = interval.getUpperBound();
@@ -184,9 +184,9 @@
 			}
 
 			for(TimedTransition::Vector::iterator iter = transitions.begin(); iter != transitions.end(); iter++){
-				for(OutputArc::WeakPtrVector::const_iterator place_iter = iter->get()->getPostset().begin(); place_iter != iter->get()->getPostset().end(); place_iter++){
-					if(place_iter->lock()->getOutputPlace().getMaxConstant() > -1){
-						iter->get()->setUntimedPostset(false);
+				for(OutputArc::Vector::iterator place_iter = (*iter)->getPostset().begin(); place_iter != (*iter)->getPostset().end(); place_iter++){
+					if((*place_iter)->getOutputPlace().getMaxConstant() > -1){
+						(*iter)->setUntimedPostset(false);
 						break;
 					}
 				}
@@ -195,7 +195,7 @@
 
 		void TimedArcPetriNet::calculateCausality(TimedPlace& p, std::vector< TimedPlace* >* result) const
 		{
-			for(std::vector< TimedPlace* >::const_iterator iter = result->begin(); iter != result->end(); iter++){
+			for(TimedPlace::Vector::const_iterator iter = result->begin(); iter != result->end(); iter++){
 				if(**iter == p) return;
 			}
 			result->push_back(&p);
@@ -209,18 +209,17 @@
 		}
 
 		void TimedArcPetriNet::updatePlaceTypes(const AST::Query* query, VerificationOptions options){
-			std::vector< int > placeNumbers;
-			boost::any context = placeNumbers;
+
+                        AST::IntVectorResult placeNumbers;
 			DiscreteVerification::PlaceVisitor visitor;
-			query->accept(visitor, context);
-			placeNumbers = boost::any_cast< std::vector< int > >(context);
+			query->accept(visitor, placeNumbers);
 
 			for(TimedPlace::Vector::const_iterator iter = places.begin(); iter != places.end(); ++iter){
 				if(options.getKeepDeadTokens() && (*iter)->getType() == Dead){
 					(*iter)->setType(Std);
 					continue;
 				}
-				for(std::vector<int>::const_iterator id_iter = placeNumbers.begin(); id_iter != placeNumbers.end(); id_iter++){
+				for(std::vector<int>::const_iterator id_iter = placeNumbers.value.begin(); id_iter != placeNumbers.value.end(); id_iter++){
 					if((*id_iter) == (*iter)->getIndex() && (*iter)->getType() == Dead){
 						(*iter)->setType(Std);
 						break;

=== modified file 'src/Core/TAPN/TimedArcPetriNet.hpp'
--- src/Core/TAPN/TimedArcPetriNet.hpp	2013-08-13 18:19:17 +0000
+++ src/Core/TAPN/TimedArcPetriNet.hpp	2013-08-26 13:51:29 +0000
@@ -8,7 +8,6 @@
 #include "TransportArc.hpp"
 #include "InhibitorArc.hpp"
 #include "OutputArc.hpp"
-#include "boost/make_shared.hpp"
 #include "google/sparse_hash_map"
 #include "boost/functional/hash.hpp"
 #include "../QueryParser/AST.hpp"
@@ -23,14 +22,22 @@
 		{
 
 		public:// construction
-			TimedArcPetriNet(const TimedPlace::Vector& places,
-				const TimedTransition::Vector& transitions,
-				const TimedInputArc::Vector& inputArcs,
-				const OutputArc::Vector& outputArcs,
-				const TransportArc::Vector& transportArcs,
-				const InhibitorArc::Vector& inhibitorArcs)
+			TimedArcPetriNet(TimedPlace::Vector& places,
+				TimedTransition::Vector& transitions,
+				TimedInputArc::Vector& inputArcs,
+				OutputArc::Vector& outputArcs,
+				TransportArc::Vector& transportArcs,
+				InhibitorArc::Vector& inhibitorArcs)
 				: places(places), transitions(transitions), inputArcs(inputArcs), outputArcs(outputArcs), transportArcs(transportArcs), inhibitorArcs(inhibitorArcs), maxConstant(0) { };
-			virtual ~TimedArcPetriNet() { /* empty */ }
+			~TimedArcPetriNet() { 
+                            // call delete on all data
+                            for(unsigned int i = 0; i < places.size();++i) delete places[i];
+                            for(unsigned int i = 0; i < transitions.size();++i) delete transitions[i];
+                            for(unsigned int i = 0; i < inputArcs.size();++i) delete inputArcs[i];
+                            for(unsigned int i = 0; i < outputArcs.size();++i) delete outputArcs[i];
+                            for(unsigned int i = 0; i < transportArcs.size();++i) delete transportArcs[i];
+                            for(unsigned int i = 0; i < inhibitorArcs.size();++i) delete inhibitorArcs[i];
+                        }
 
 		public: // inspectors
 			void print(std::ostream& out) const;
@@ -64,12 +71,12 @@
 			void findMaxConstants();
 
 		private: // data
-			const TimedPlace::Vector places;
+			TimedPlace::Vector places;
 			TimedTransition::Vector transitions;
-			const TimedInputArc::Vector inputArcs;
-			const OutputArc::Vector outputArcs;
-			const TransportArc::Vector transportArcs;
-			const InhibitorArc::Vector inhibitorArcs;
+			TimedInputArc::Vector inputArcs;
+			OutputArc::Vector outputArcs;
+			TransportArc::Vector transportArcs;
+			InhibitorArc::Vector inhibitorArcs;
 			int maxConstant;
 		};
 

=== modified file 'src/Core/TAPN/TimedInputArc.cpp'
--- src/Core/TAPN/TimedInputArc.cpp	2013-05-08 15:10:14 +0000
+++ src/Core/TAPN/TimedInputArc.cpp	2013-08-26 13:51:29 +0000
@@ -6,7 +6,7 @@
 	namespace TAPN {
 		void TimedInputArc::print(std::ostream& out) const
 		{
-			out << "From " << place->getName() << " to " << transition->getName() << " weight: " << weight;
+			out << "From " << place.getName() << " to " << transition.getName() << " weight: " << weight;
 			out << " with interval " << interval;
 		}
 	}

=== modified file 'src/Core/TAPN/TimedInputArc.hpp'
--- src/Core/TAPN/TimedInputArc.hpp	2013-05-08 13:30:33 +0000
+++ src/Core/TAPN/TimedInputArc.hpp	2013-08-26 13:51:29 +0000
@@ -3,7 +3,6 @@
 
 #include <vector>
 #include "TimeInterval.hpp"
-#include "boost/smart_ptr.hpp"
 
 namespace VerifyTAPN {
 	namespace TAPN {
@@ -13,25 +12,24 @@
 		class TimedInputArc
 		{
 		public: // typedefs
-			typedef std::vector< boost::shared_ptr<TimedInputArc> > Vector;
-			typedef std::vector< boost::weak_ptr<TimedInputArc> > WeakPtrVector;
+			typedef std::vector< TimedInputArc* > Vector;
 		public:
-			TimedInputArc(const boost::shared_ptr<TimedPlace>& place, const boost::shared_ptr<TimedTransition>& transition, const int weight) : interval(), place(place), transition(transition), weight(weight) { };
-			TimedInputArc(const boost::shared_ptr<TimedPlace>& place, const boost::shared_ptr<TimedTransition>& transition, const int weight, const TimeInterval& interval) : interval(interval), place(place), transition(transition), weight(weight) { };
+			TimedInputArc(TimedPlace& place, TimedTransition& transition, const int weight) : interval(), place(place), transition(transition), weight(weight) { };
+			TimedInputArc(TimedPlace& place, TimedTransition& transition, const int weight, TimeInterval interval) : interval(interval), place(place), transition(transition), weight(weight) { };
 			virtual ~TimedInputArc() { /* empty */}
 
 		public: // modifiers
-			inline TimedPlace& getInputPlace() { return *place; }
-			inline TimedTransition& getOutputTransition() { return *transition; }
-			inline const TimeInterval& getInterval() { return interval; }
+			inline TimedPlace& getInputPlace() const { return place; }
+			inline TimedTransition& getOutputTransition() const { return transition; }
+			const inline TimeInterval& getInterval() const { return interval; }
 
 		public: // Inspectors
 			void print(std::ostream& out) const;
 			inline const int getWeight() const { return weight; }
 		private:
-			const TimeInterval interval;
-			const boost::shared_ptr<TimedPlace> place;
-			const boost::shared_ptr<TimedTransition> transition;
+			TimeInterval interval;
+			TimedPlace& place;
+			TimedTransition& transition;
 			const int weight;
 		};
 

=== modified file 'src/Core/TAPN/TimedPlace.hpp'
--- src/Core/TAPN/TimedPlace.hpp	2013-05-08 13:49:42 +0000
+++ src/Core/TAPN/TimedPlace.hpp	2013-08-26 13:51:29 +0000
@@ -10,7 +10,6 @@
 #include "OutputArc.hpp"
 #include "TransportArc.hpp"
 #include "InhibitorArc.hpp"
-#include "boost/shared_ptr.hpp"
 
 namespace VerifyTAPN{
 	namespace TAPN{
@@ -32,7 +31,7 @@
 			static const std::string BOTTOM_NAME;
 
 		public: // typedefs
-			typedef std::vector< boost::shared_ptr<TimedPlace> > Vector;
+			typedef std::vector<TimedPlace*> Vector;
 
 		public: // construction / destruction
 			TimedPlace(const std::string& name, const std::string& id, const TimeInvariant timeInvariant)
@@ -45,10 +44,10 @@
 			inline void setIndex(int i) { index = i; };
 			inline void setMaxConstant(int max) { maxConstant = max; }
 			inline void setHasInhibitorArcs(bool inhibitorArcs) { containsInhibitorArcs = inhibitorArcs; }
-			inline void addInputArc(boost::shared_ptr<TimedInputArc> inputArc) { inputArcs.push_back(inputArc); }
-			inline void addTransportArc(boost::shared_ptr<TransportArc> transportArc) { transportArcs.push_back(transportArc); }
-			inline void addInhibitorArc(boost::shared_ptr<InhibitorArc> inhibitorArc) { inhibitorArcs.push_back(inhibitorArc); }
-			inline void addOutputArc(boost::shared_ptr<OutputArc> outputArc) { outputArcs.push_back(outputArc); }
+			inline void addInputArc(TimedInputArc& inputArc) { inputArcs.push_back(&inputArc); }
+			inline void addTransportArc(TransportArc& transportArc) { transportArcs.push_back(&transportArc); }
+			inline void addInhibitorArc(InhibitorArc& inhibitorArc) { inhibitorArcs.push_back(&inhibitorArc); }
+			inline void addOutputArc(OutputArc& outputArc) { outputArcs.push_back(&outputArc); }
 			inline void setType(PlaceType type){ this->type = type; }
 		public: // inspection
 			inline const PlaceType getType() const { return type; }
@@ -60,9 +59,9 @@
 			inline const int getMaxConstant() const { return maxConstant; }
 			inline const TAPN::TimeInvariant& getInvariant() const { return timeInvariant; };
 			inline bool hasInhibitorArcs() const { return containsInhibitorArcs; };
-			inline const TransportArc::WeakPtrVector& getTransportArcs() const { return transportArcs; }
-			inline const InhibitorArc::WeakPtrVector& getInhibitorArcs() const { return inhibitorArcs; }
-			inline const TimedInputArc::WeakPtrVector& getInputArcs() const { return inputArcs; }
+			inline const TransportArc::Vector& getTransportArcs() const { return transportArcs; }
+			inline const InhibitorArc::Vector& getInhibitorArcs() const { return inhibitorArcs; }
+			inline const TimedInputArc::Vector& getInputArcs() const { return inputArcs; }
 
 		private: // data
 			PlaceType type;
@@ -73,10 +72,10 @@
 			bool untimed;
 			int maxConstant;
 			bool containsInhibitorArcs;
-			TimedInputArc::WeakPtrVector inputArcs;
-			TransportArc::WeakPtrVector transportArcs;
-			InhibitorArc::WeakPtrVector inhibitorArcs;
-			OutputArc::WeakPtrVector outputArcs;
+			TimedInputArc::Vector inputArcs;
+			TransportArc::Vector transportArcs;
+			InhibitorArc::Vector inhibitorArcs;
+			OutputArc::Vector outputArcs;
 		};
 
 		inline std::ostream& operator<<(std::ostream& out, const TimedPlace& place)

=== modified file 'src/Core/TAPN/TimedTransition.cpp'
--- src/Core/TAPN/TimedTransition.cpp	2013-07-20 12:05:45 +0000
+++ src/Core/TAPN/TimedTransition.cpp	2013-08-26 13:51:29 +0000
@@ -1,66 +1,52 @@
+#include <cstdlib>
 #include "TimedTransition.hpp"
 #include "TimedPlace.hpp"
 
 namespace VerifyTAPN {
-	namespace TAPN {
-		void TimedTransition::print(std::ostream& out) const
-		{
-			out << getName();
-                        if(this->urgent)
-                            out << " urgent ";
-                        out << "(" << index << ")";
-		}
-
-		void TimedTransition::addToPreset(const boost::shared_ptr<TimedInputArc>& arc)
-		{
-			if(arc)
-			{
-                                if(this->urgent){   // all urgency in discrete time must have untimed 
-                                                    //inputarcs to not break semantics
-                                    if(!arc.get()->getInterval().isZeroInfinity()){
-                                        std::cout << "Urgent transitions must have untimed input arcs" << std::endl;
-                                        exit(1);
-                                    }
-                                }
-                                preset.push_back(arc);
-			}
-		}
-
-		void TimedTransition::addTransportArcGoingThrough(const boost::shared_ptr<TransportArc>& arc)
-		{
-			if(arc)
-			{
-                            if(this->urgent){   // all urgency in discrete time must have untimed 
-                                                //inputarcs to not break semantics
-                                if(!arc.get()->getInterval().isZeroInfinity()){
-                                    std::cout << "Urgent transitions must have untimed transportarcs" << std::endl;
-                                    exit(1);
-                                } else if(arc.get()->getDestination().getInvariant() != TimeInvariant::LS_INF){
-                                    // urgency breaks if we have invariant at destination
-                                    std::cout << "Transportarcs going through an urgent transition cannot have invariants at destination-places." << std::endl;
-                                    exit(1);                                    
-                                }
-                            }
-				transportArcs.push_back(arc);
-			}
-		}
-
-		void TimedTransition::addIncomingInhibitorArc(const boost::shared_ptr<InhibitorArc>& arc)
-		{
-			if(arc)
-			{
-				inhibitorArcs.push_back(arc);
-			}
-		}
-
-		void TimedTransition::addToPostset(const boost::shared_ptr<OutputArc>& arc)
-		{
-			if(arc)
-			{
-				postset.push_back(arc);
-			}
-		}
-	}
+    namespace TAPN {
+
+        void TimedTransition::print(std::ostream& out) const {
+            out << getName();
+            if (this->urgent)
+                out << " urgent ";
+            out << "(" << index << ")";
+        }
+
+        void TimedTransition::addToPreset(TimedInputArc& arc) {
+
+            if (this->urgent) { // all urgency in discrete time must have untimed 
+                //inputarcs to not break semantics
+                if (!arc.getInterval().isZeroInfinity()) {
+                    std::cout << "Urgent transitions must have untimed input arcs" << std::endl;
+                    exit(1);
+                }
+            }
+            preset.push_back(&arc);
+        }
+
+        void TimedTransition::addTransportArcGoingThrough(TransportArc& arc) {
+            if (this->urgent) { // all urgency in discrete time must have untimed 
+                //inputarcs to not break semantics
+                if (!arc.getInterval().isZeroInfinity()) {
+                    std::cout << "Urgent transitions must have untimed transportarcs" << std::endl;
+                    exit(1);
+                } else if (arc.getDestination().getInvariant() != TimeInvariant::LS_INF) {
+                    // urgency breaks if we have invariant at destination
+                    std::cout << "Transportarcs going through an urgent transition cannot have invariants at destination-places." << std::endl;
+                    exit(1);
+                }
+            }
+            transportArcs.push_back(&arc);
+        }
+
+        void TimedTransition::addIncomingInhibitorArc(InhibitorArc& arc) {
+            inhibitorArcs.push_back(&arc);
+        }
+
+        void TimedTransition::addToPostset(OutputArc& arc) {
+            postset.push_back(&arc);
+        }
+    }
 }
 
 

=== modified file 'src/Core/TAPN/TimedTransition.hpp'
--- src/Core/TAPN/TimedTransition.hpp	2013-06-28 12:53:59 +0000
+++ src/Core/TAPN/TimedTransition.hpp	2013-08-26 13:51:29 +0000
@@ -7,7 +7,6 @@
 #include "TransportArc.hpp"
 #include "InhibitorArc.hpp"
 #include "OutputArc.hpp"
-#include "boost/shared_ptr.hpp"
 
 namespace VerifyTAPN {
 
@@ -19,34 +18,38 @@
 		class TimedTransition
 		{
 		public: // typedefs
-			typedef std::vector< boost::shared_ptr<TimedTransition> > Vector;
+			typedef std::vector<TimedTransition*> Vector;
 		public:
 			TimedTransition(const std::string& name, const std::string& id, bool urgent) : name(name), id(id), preset(), postset(), transportArcs(), index(-1), untimedPostset(true), urgent(urgent) { };
 			TimedTransition() : name("*EMPTY*"), id("-1"), preset(), postset(), transportArcs(), index(-1), untimedPostset(true),urgent(false) { };
 			virtual ~TimedTransition() { /* empty */ }
 
 		public: // modifiers
-			void addToPreset(const boost::shared_ptr<TimedInputArc>& arc);
-			void addToPostset(const boost::shared_ptr<OutputArc>& arc);
-			void addTransportArcGoingThrough(const boost::shared_ptr<TransportArc>& arc);
-			void addIncomingInhibitorArc(const boost::shared_ptr<InhibitorArc>& arc);
+			void addToPreset(TimedInputArc& arc);
+			void addToPostset(OutputArc& arc);
+			void addTransportArcGoingThrough(TransportArc& arc);
+			void addIncomingInhibitorArc(InhibitorArc& arc);
 
 			inline void setIndex(int i) { index = i; };
 		public: // inspectors
 			inline const std::string& getName() const { return name; };
 			inline const std::string& getId() const { return id; };
 			void print(std::ostream&) const;
-			inline const TimedInputArc::WeakPtrVector& getPreset() const { return preset; }
-			inline const TransportArc::WeakPtrVector& getTransportArcs() const { return transportArcs; }
-			inline const InhibitorArc::WeakPtrVector& getInhibitorArcs() const { return inhibitorArcs; }
+			inline TimedInputArc::Vector& getPreset() { return preset; }
+			const inline TimedInputArc::Vector& getPreset() const { return preset; }
+			inline TransportArc::Vector& getTransportArcs() { return transportArcs; }
+			const inline TransportArc::Vector& getTransportArcs() const { return transportArcs; }
+			inline InhibitorArc::Vector& getInhibitorArcs() { return inhibitorArcs; }
+			const inline InhibitorArc::Vector& getInhibitorArcs() const { return inhibitorArcs; }
 			inline const unsigned int getPresetSize() const { return getNumberOfInputArcs() + getNumberOfTransportArcs(); }
-			inline const OutputArc::WeakPtrVector& getPostset() const { return postset; }
+			inline OutputArc::Vector& getPostset() { return postset; }
+			const inline OutputArc::Vector& getPostset() const { return postset; }
 			inline const unsigned int getPostsetSize() const { return postset.size() + transportArcs.size(); }
-			inline unsigned int getNumberOfInputArcs() const { return preset.size(); };
-			inline unsigned int getNumberOfTransportArcs() const { return transportArcs.size(); };
+			inline const unsigned int getNumberOfInputArcs() const { return preset.size(); };
+			inline const unsigned int getNumberOfTransportArcs() const { return transportArcs.size(); };
 
 			inline const bool isConservative() const { return preset.size() == postset.size(); }
-			inline unsigned int getIndex() const { return index; }
+			inline const unsigned int getIndex() const { return index; }
 			inline const bool hasUntimedPostset() const { return untimedPostset; }
 			inline void setUntimedPostset(bool untimed){ untimedPostset = untimed; }
                         inline const bool isUrgent() const {
@@ -56,10 +59,10 @@
 		private: // data
 			std::string name;
 			std::string id;
-			TimedInputArc::WeakPtrVector preset;
-			OutputArc::WeakPtrVector postset;
-			TransportArc::WeakPtrVector transportArcs;
-			InhibitorArc::WeakPtrVector inhibitorArcs;
+			TimedInputArc::Vector preset;
+			OutputArc::Vector postset;
+			TransportArc::Vector transportArcs;
+			InhibitorArc::Vector inhibitorArcs;
 			unsigned int index;
 			bool untimedPostset;
                         bool urgent;

=== modified file 'src/Core/TAPN/TransportArc.cpp'
--- src/Core/TAPN/TransportArc.cpp	2013-05-08 15:10:14 +0000
+++ src/Core/TAPN/TransportArc.cpp	2013-08-26 13:51:29 +0000
@@ -8,7 +8,7 @@
 	{
 		void TransportArc::print(std::ostream& out) const
 		{
-			out << "From " << source->getName() << " to " << transition->getName() << " to " << destination->getName() << " weight: " << weight;
+			out << "From " << source.getName() << " to " << transition.getName() << " to " << destination.getName() << " weight: " << weight;
 			out << " with interval " << interval;
 		}
 	}

=== modified file 'src/Core/TAPN/TransportArc.hpp'
--- src/Core/TAPN/TransportArc.hpp	2013-05-08 15:10:14 +0000
+++ src/Core/TAPN/TransportArc.hpp	2013-08-26 13:51:29 +0000
@@ -1,9 +1,8 @@
 #ifndef TRANSPORTARC_HPP_
 #define TRANSPORTARC_HPP_
 
+#include "TimeInterval.hpp"
 #include <vector>
-#include "TimeInterval.hpp"
-#include "boost/smart_ptr.hpp"
 
 namespace VerifyTAPN
 {
@@ -15,32 +14,31 @@
 		class TransportArc
 		{
 		public:
-			typedef std::vector< boost::shared_ptr<TransportArc> > Vector;
-			typedef std::vector< boost::weak_ptr<TransportArc> > WeakPtrVector;
+                    	typedef std::vector< TransportArc* > Vector;
 		public:
 			TransportArc(
-					const boost::shared_ptr<TimedPlace>& source,
-					const boost::shared_ptr<TimedTransition>& transition,
-					const boost::shared_ptr<TimedPlace>& destination,
-					const TAPN::TimeInterval& interval,
+					TimedPlace& source,
+					TimedTransition& transition,
+					TimedPlace& destination,
+					TAPN::TimeInterval interval,
 					const int weight
 			) : interval(interval), source(source), transition(transition), destination(destination), weight(weight) {};
 
 			virtual ~TransportArc() {};
 		public:
-			inline TimedPlace& getSource() { return *source; }
-			inline TimedTransition& getTransition() { return *transition; }
-			inline TimedPlace& getDestination() { return *destination; }
-			inline const TimeInterval& getInterval() { return interval; }
+			inline TimedPlace& getSource() const { return source; }
+			inline TimedTransition& getTransition() const { return transition; }
+			inline TimedPlace& getDestination() const { return destination; }
+			inline const TimeInterval& getInterval() const { return interval; }
 
 		public: // Inspectors
 				void print(std::ostream& out) const;
 				inline const int getWeight() const { return weight; }
 		private:
-			const TAPN::TimeInterval interval;
-			const boost::shared_ptr<TimedPlace> source;
-			const boost::shared_ptr<TimedTransition> transition;
-			const boost::shared_ptr<TimedPlace> destination;
+			TAPN::TimeInterval interval;
+			TimedPlace& source;
+			TimedTransition& transition;
+			TimedPlace& destination;
 			const int weight;
 		};
 

=== modified file 'src/Core/TAPNParser/TAPNXmlParser.cpp'
--- src/Core/TAPNParser/TAPNXmlParser.cpp	2013-05-29 18:02:37 +0000
+++ src/Core/TAPNParser/TAPNXmlParser.cpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,7 @@
 namespace VerifyTAPN {
 using namespace rapidxml;
 
-boost::shared_ptr<TimedArcPetriNet> TAPNXmlParser::parse(const std::string & filename) const
+TimedArcPetriNet* TAPNXmlParser::parse(const std::string & filename) const
 {
 	const std::string contents = VerifyTAPN::readFile(filename);
 	std::vector<char> charArray(contents.begin(), contents.end());
@@ -41,14 +41,14 @@
 	return parseInitialMarking(*root, tapn);
 }
 
-boost::shared_ptr<TimedArcPetriNet> TAPNXmlParser::parseTAPN(const xml_node<>& root) const
+TimedArcPetriNet* TAPNXmlParser::parseTAPN(const xml_node<>& root) const
 {
 	TimedPlace::Vector places = parsePlaces(root);
 	TimedTransition::Vector transitions = parseTransitions(root);
 
 	TAPNXmlParser::ArcCollections arcs = parseArcs(root, places, transitions);
 
-	boost::shared_ptr<TimedArcPetriNet> tapn = boost::make_shared<TimedArcPetriNet>(places, transitions, arcs.inputArcs, arcs.outputArcs, arcs.transportArcs, arcs.inhibitorArcs);
+	TimedArcPetriNet* tapn = new TimedArcPetriNet(places, transitions, arcs.inputArcs, arcs.outputArcs, arcs.transportArcs, arcs.inhibitorArcs);
 
 	return tapn;
 }
@@ -59,7 +59,7 @@
 
 	xml_node<>* placeNode = root.first_node("place");
 	while(placeNode != NULL){
-		boost::shared_ptr<TimedPlace> place = parsePlace(*placeNode);
+		TimedPlace* place = parsePlace(*placeNode);
 		places.push_back(place);
 		placeNode = placeNode->next_sibling("place");
 	}
@@ -67,14 +67,14 @@
 	return places;
 }
 
-boost::shared_ptr<TimedPlace> TAPNXmlParser::parsePlace(const xml_node<>& placeNode) const
+TimedPlace* TAPNXmlParser::parsePlace(const xml_node<>& placeNode) const
 {
 	std::string id(placeNode.first_attribute("id")->value());
 	std::string name(placeNode.first_attribute("name")->value());
 
 	std::string invariantNode = placeNode.first_attribute("invariant")->value();
 	TimeInvariant timeInvariant = TimeInvariant::createFor(invariantNode);
-	return boost::make_shared<TimedPlace>(name, id, timeInvariant);
+	return new TimedPlace(name, id, timeInvariant);
 }
 
 TimedTransition::Vector TAPNXmlParser::parseTransitions(const xml_node<>& root) const
@@ -83,7 +83,7 @@
 
 	xml_node<>* transitionNode = root.first_node("transition");
 	while(transitionNode != NULL){
-		boost::shared_ptr<TimedTransition> transition = parseTransition(*transitionNode);
+		TimedTransition* transition = parseTransition(*transitionNode);
 		transitions.push_back(transition);
 		transitionNode = transitionNode->next_sibling("transition");
 	}
@@ -91,7 +91,7 @@
 	return transitions;
 }
 
-boost::shared_ptr<TimedTransition> TAPNXmlParser::parseTransition(const xml_node<>& transitionNode) const
+TimedTransition* TAPNXmlParser::parseTransition(const xml_node<>& transitionNode) const
 {
 	std::string id(transitionNode.first_attribute("id")->value());
 	std::string name(transitionNode.first_attribute("name")->value());
@@ -103,7 +103,7 @@
                 urgent = true;
             }
         }
-	return boost::make_shared<TimedTransition>(name, id,urgent );
+	return new TimedTransition(name, id,urgent );
 }
 
 TAPNXmlParser::ArcCollections TAPNXmlParser::parseArcs(const xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
@@ -163,7 +163,7 @@
 	return outputArcs;
 }
 
-boost::shared_ptr<TimedInputArc> TAPNXmlParser::parseInputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+TimedInputArc* TAPNXmlParser::parseInputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
 {
 	std::string source = arcNode.first_attribute("source")->value();
 	std::string target = arcNode.first_attribute("target")->value();
@@ -174,13 +174,22 @@
 		weight = atoi(attribute->value());
 	}
 
-	TimedPlace::Vector::const_iterator place = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::getId), _1) == source);
-	TimedTransition::Vector::const_iterator transition = find_if(transitions.begin(), transitions.end(), boost::bind(boost::mem_fn(&TimedTransition::getId), _1) == target);
+        TimedPlace::Vector::const_iterator place = places.begin();
+        while(place != places.end()){
+            if((*place)->getId() == source) break;
+            ++place;
+        }
+        
+        TimedTransition::Vector::const_iterator transition = transitions.begin();
+        while(transition != transitions.end()){
+            if((*transition)->getId() == target) break;
+            ++transition;
+        }     
 
-	return boost::make_shared<TimedInputArc>(*place, *transition, weight, TimeInterval::createFor(interval));
+	return new TimedInputArc(**place, **transition, weight, TimeInterval::createFor(interval));
 }
 
-boost::shared_ptr<TransportArc> TAPNXmlParser::parseTransportArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+TransportArc* TAPNXmlParser::parseTransportArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
 {
 	std::string sourceName = arcNode.first_attribute("source")->value();
 	std::string transitionName = arcNode.first_attribute("transition")->value();
@@ -192,42 +201,75 @@
 		weight = atoi(attribute->value());
 	}
 
-	TimedPlace::Vector::const_iterator source = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::getId), _1) == sourceName);
-	TimedTransition::Vector::const_iterator transition = find_if(transitions.begin(), transitions.end(), boost::bind(boost::mem_fn(&TimedTransition::getId), _1) == transitionName);
-	TimedPlace::Vector::const_iterator target = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::getId), _1) == targetName);
-	return boost::make_shared<TransportArc>(*source, *transition, *target, TimeInterval::createFor(interval), weight);
-}
-
-boost::shared_ptr<InhibitorArc> TAPNXmlParser::parseInhibitorArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
-{
-	std::string source = arcNode.first_attribute("source")->value();
-	std::string target = arcNode.first_attribute("target")->value();
-	int weight = 1;
-	xml_attribute<char>* attribute = arcNode.first_attribute("weight");
-	if(attribute != NULL){
-		weight = atoi(attribute->value());
-	}
-
-	TimedPlace::Vector::const_iterator place = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::getId), _1) == source);
-	TimedTransition::Vector::const_iterator transition = find_if(transitions.begin(), transitions.end(), boost::bind(boost::mem_fn(&TimedTransition::getId), _1) == target);
-
-	return boost::make_shared<InhibitorArc>(*place, *transition, weight);
-}
-
-boost::shared_ptr<OutputArc> TAPNXmlParser::parseOutputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
-{
-	std::string source = arcNode.first_attribute("source")->value();
-	std::string target = arcNode.first_attribute("target")->value();
-	int weight = 1;
-	xml_attribute<char>* attribute = arcNode.first_attribute("weight");
-	if(attribute != NULL){
-		weight = atoi(attribute->value());
-	}
-
-	TimedTransition::Vector::const_iterator transition = find_if(transitions.begin(), transitions.end(), boost::bind(boost::mem_fn(&TimedTransition::getId), _1) == source);
-	TimedPlace::Vector::const_iterator place = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::getId), _1) == target);
-
-	return boost::make_shared<OutputArc>(*transition, *place, weight);
+        TimedPlace::Vector::const_iterator source = places.begin();
+        while(source != places.end()){
+            if((*source)->getId() == sourceName) break;
+            ++source;
+        }
+        
+        TimedTransition::Vector::const_iterator transition = transitions.begin();
+        while(transition != transitions.end()){
+            if((*transition)->getId() == transitionName) break;
+            ++transition;
+        }
+        
+        TimedPlace::Vector::const_iterator target = places.begin();
+        while(target != places.end()){
+            if((*target)->getId() == targetName) break;
+            ++target;
+        }
+
+	return new TransportArc(**source, **transition, **target, TimeInterval::createFor(interval), weight);
+}
+
+InhibitorArc* TAPNXmlParser::parseInhibitorArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+{
+	std::string source = arcNode.first_attribute("source")->value();
+	std::string target = arcNode.first_attribute("target")->value();
+	int weight = 1;
+	xml_attribute<char>* attribute = arcNode.first_attribute("weight");
+	if(attribute != NULL){
+		weight = atoi(attribute->value());
+	}
+
+        TimedPlace::Vector::const_iterator place = places.begin();
+        while(place != places.end()){
+            if((*place)->getId() == source) break;
+            ++place;
+        }
+
+        TimedTransition::Vector::const_iterator transition = transitions.begin();
+        while(transition != transitions.end()){
+            if((*transition)->getId() == target) break;
+            ++transition;
+        }
+
+	return new InhibitorArc(**place, **transition, weight);
+}
+
+OutputArc* TAPNXmlParser::parseOutputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+{
+	std::string source = arcNode.first_attribute("source")->value();
+	std::string target = arcNode.first_attribute("target")->value();
+	int weight = 1;
+	xml_attribute<char>* attribute = arcNode.first_attribute("weight");
+	if(attribute != NULL){
+		weight = atoi(attribute->value());
+	}
+
+        TimedTransition::Vector::const_iterator transition = transitions.begin();
+        while(transition != transitions.end()){
+            if((*transition)->getId() == source) break;
+            ++transition;
+        }
+
+        TimedPlace::Vector::const_iterator place = places.begin();
+        while(place != places.end()){
+            if((*place)->getId() == target) break;
+            ++place;
+        }
+
+	return new OutputArc(**transition, **place, weight);
 
 }
 

=== modified file 'src/Core/TAPNParser/TAPNXmlParser.hpp'
--- src/Core/TAPNParser/TAPNXmlParser.hpp	2013-05-08 15:19:35 +0000
+++ src/Core/TAPNParser/TAPNXmlParser.hpp	2013-08-26 13:51:29 +0000
@@ -2,7 +2,6 @@
 #define VERIFYTAPN_TAPNXMLPARSER_HPP_
 
 #include "../TAPN/TAPN.hpp"
-#include "boost/smart_ptr.hpp"
 #include "../../../lib/rapidxml-1.13/rapidxml.hpp"
 
 namespace VerifyTAPN {
@@ -27,26 +26,26 @@
 		virtual ~TAPNXmlParser() { /* empty */ };
 
 	public:
-		boost::shared_ptr<TimedArcPetriNet> parse(const std::string & filename) const;
+		TimedArcPetriNet* parse(const std::string & filename) const;
 		std::vector<int> parseMarking(const std::string & filename, const TimedArcPetriNet& tapn) const;
 	private:
-		boost::shared_ptr<TimedArcPetriNet> parseTAPN(const rapidxml::xml_node<> & root) const;
+		TimedArcPetriNet* parseTAPN(const rapidxml::xml_node<> & root) const;
 
 		TimedPlace::Vector parsePlaces(const rapidxml::xml_node<>& root) const;
-		boost::shared_ptr<TimedPlace> parsePlace(const rapidxml::xml_node<>& placeNode) const;
+		TimedPlace* parsePlace(const rapidxml::xml_node<>& placeNode) const;
 
 		TimedTransition::Vector parseTransitions(const rapidxml::xml_node<>& root) const;
-		boost::shared_ptr<TimedTransition> parseTransition(const rapidxml::xml_node<>& transitionNode) const;
+		TimedTransition* parseTransition(const rapidxml::xml_node<>& transitionNode) const;
 
 		ArcCollections parseArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
 		TransportArc::Vector parseTransportArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
 		InhibitorArc::Vector parseInhibitorArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
 		TimedInputArc::Vector parseInputArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
 		OutputArc::Vector parseOutputArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
-		boost::shared_ptr<TimedInputArc> parseInputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
-		boost::shared_ptr<InhibitorArc> parseInhibitorArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
-		boost::shared_ptr<TransportArc> parseTransportArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
-		boost::shared_ptr<OutputArc> parseOutputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
+		TimedInputArc* parseInputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
+		InhibitorArc* parseInhibitorArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
+		TransportArc* parseTransportArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
+		OutputArc* parseOutputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const;
 		std::vector<int> parseInitialMarking(const rapidxml::xml_node<>& root, const TimedArcPetriNet& tapn) const;
 	};
 }

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarking.hpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2013-05-10 15:48:15 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2013-08-26 13:51:29 +0000
@@ -10,7 +10,6 @@
 
 #include <assert.h>
 #include <vector>
-#include "boost/functional/hash.hpp"
 #include "NonStrictMarkingBase.hpp"
 #include <iostream>
 #include "../../Core/TAPN/TAPN.hpp"

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2013-07-21 17:57:29 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2013-08-26 13:51:29 +0000
@@ -238,7 +238,7 @@
             int count = tapn.getTransitions().size();
             int* status = new int[count];
 
-            for (vector<boost::shared_ptr<TAPN::TimedTransition> >::const_iterator tit = tapn.getTransitions().begin();
+            for (TAPN::TimedTransition::Vector::const_iterator tit = tapn.getTransitions().begin();
                     tit != tapn.getTransitions().end(); ++tit) {
                 int presetSize = (*tit)->getPresetSize();
                 int index = (*tit)->getIndex();
@@ -255,15 +255,15 @@
                 int numtokens = place_iter->numberOfTokens();
 
                 // for regular input arcs
-                for (TAPN::TimedInputArc::WeakPtrVector::const_iterator arc_iter = place_iter->place->getInputArcs().begin();
+                for (TAPN::TimedInputArc::Vector::const_iterator arc_iter = place_iter->place->getInputArcs().begin();
                         arc_iter != place_iter->place->getInputArcs().end(); ++arc_iter) {
-                    int id = arc_iter->lock().get()->getOutputTransition().getIndex();
-                    int weight = arc_iter->lock().get()->getWeight();
+                    int id = (*arc_iter)->getOutputTransition().getIndex();
+                    int weight = (*arc_iter)->getWeight();
                     if(numtokens < weight) {
                         status[id] = -1;        // -1 for impossible to enable
                     } else if(status[id] != -1) {
-                        int lb = arc_iter->lock().get()->getInterval().getLowerBound();
-                        int ub = arc_iter->lock().get()->getInterval().getUpperBound();
+                        int lb = (*arc_iter)->getInterval().getLowerBound();
+                        int ub = (*arc_iter)->getInterval().getUpperBound();
                         // decrement if token can satisfy the bounds
                         for (TokenList::const_iterator tokenit = place_iter->tokens.begin();
                                 tokenit != place_iter->tokens.end(); ++tokenit){
@@ -285,15 +285,15 @@
                 }
 
                 // for transport arcs
-                for (TAPN::TransportArc::WeakPtrVector::const_iterator arc_iter = place_iter->place->getTransportArcs().begin();
+                for (TAPN::TransportArc::Vector::const_iterator arc_iter = place_iter->place->getTransportArcs().begin();
                         arc_iter != place_iter->place->getTransportArcs().end(); ++arc_iter) {
-                    int id = arc_iter->lock().get()->getTransition().getIndex();
-                    int weight = arc_iter->lock().get()->getWeight();
-                    if(numtokens < arc_iter->lock().get()->getWeight())
+                    int id = (*arc_iter)->getTransition().getIndex();
+                    int weight = (*arc_iter)->getWeight();
+                    if(numtokens < (*arc_iter)->getWeight())
                         status[id] = -1; // impossible to enable
                     else if(status[id] != -1) { // if enable able so far
-                        int lb = arc_iter->lock().get()->getInterval().getLowerBound();
-                        int ub = arc_iter->lock().get()->getInterval().getUpperBound();
+                        int lb = (*arc_iter)->getInterval().getLowerBound();
+                        int ub = (*arc_iter)->getInterval().getUpperBound();
                         // decrement if token can satisfy the bounds
                         for (TokenList::const_iterator tokenit = place_iter->tokens.begin();
                                 tokenit != place_iter->tokens.end(); ++tokenit){
@@ -315,11 +315,11 @@
                 }
 
                 // for inhibitor arcs
-                for (TAPN::InhibitorArc::WeakPtrVector::const_iterator arc_iter = place_iter->place->getInhibitorArcs().begin();
+                for (TAPN::InhibitorArc::Vector::const_iterator arc_iter = place_iter->place->getInhibitorArcs().begin();
                         arc_iter != place_iter->place->getInhibitorArcs().end(); ++arc_iter) {
-                    int id = arc_iter->lock().get()->getOutputTransition().getIndex();
+                    int id = (*arc_iter)->getOutputTransition().getIndex();
                     // no precheck if it was disabled, actual calculation is just as fast
-                    if(numtokens >= arc_iter->lock().get()->getWeight())        // we satisfy the inhibitor
+                    if(numtokens >= (*arc_iter)->getWeight())        // we satisfy the inhibitor
                         status[id] = -1;                                        // transition cannot fire
                 }
                 
@@ -408,7 +408,7 @@
             return youngest;
         }
 
-        int NonStrictMarkingBase::makeBase(TAPN::TimedArcPetriNet* tapn) {
+        int NonStrictMarkingBase::makeBase() {
 #ifdef DEBUG
             std::cout << "Before makeBase: " << *this << std::endl;
 #endif

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp	2013-07-21 11:18:50 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp	2013-08-26 13:51:29 +0000
@@ -203,7 +203,7 @@
 			}
 		}
                 int getYoungest();
-		int makeBase(TAPN::TimedArcPetriNet* tapn);
+		int makeBase();
                 virtual NonStrictMarkingBase& Clone()
                 {
                         NonStrictMarkingBase* clone = new NonStrictMarkingBase(*this);

=== modified file 'src/DiscreteVerification/DataStructures/PTrie.h'
--- src/DiscreteVerification/DataStructures/PTrie.h	2013-05-14 19:21:29 +0000
+++ src/DiscreteVerification/DataStructures/PTrie.h	2013-08-26 13:51:29 +0000
@@ -58,7 +58,7 @@
             };
 
 
-            PTrie(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, int knumber, int nplaces, int mage) :
+            PTrie(TAPN::TimedArcPetriNet& tapn, int knumber, int nplaces, int mage) :
             maxNumberOfTokens(knumber),
             maxAge(mage + 1),
             numberOfPlaces(nplaces),
@@ -118,7 +118,7 @@
             uint markingBitSize;
             const uint blockSize;
 
-            boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn;
+            TAPN::TimedArcPetriNet& tapn;
 
             MarkingEncoding encoding;
             vector<PNode*> pnodeArray;
@@ -241,7 +241,7 @@
                     int age = floor(data / this->numberOfPlaces);
                     uint place = (data % this->numberOfPlaces);
                     Token t = Token(age, count);
-                    m->addTokenInPlace(tapn->getPlace(place), t);
+                    m->addTokenInPlace(tapn.getPlace(place), t);
                     data = 0;
                     count = 0;
                 }

=== modified file 'src/DiscreteVerification/DataStructures/PWList.hpp'
--- src/DiscreteVerification/DataStructures/PWList.hpp	2013-05-08 16:29:47 +0000
+++ src/DiscreteVerification/DataStructures/PWList.hpp	2013-08-26 13:51:29 +0000
@@ -72,7 +72,7 @@
 
         public:
 
-            PWListHybrid(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, WaitingList<EncodingPointer<MetaData> >* w_l, int knumber, int nplaces, int mage, bool isLiveness, bool makeTrace) :
+            PWListHybrid(TAPN::TimedArcPetriNet& tapn, WaitingList<EncodingPointer<MetaData> >* w_l, int knumber, int nplaces, int mage, bool isLiveness, bool makeTrace) :
             PWListBase(isLiveness),
             waiting_list(w_l),
             makeTrace(makeTrace) {

=== modified file 'src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.cpp'
--- src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.cpp	2013-05-08 16:29:47 +0000
+++ src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.cpp	2013-08-26 13:51:29 +0000
@@ -10,7 +10,7 @@
 namespace VerifyTAPN {
     namespace DiscreteVerification {
 
-        std::pair<LivenessDart*, bool> TimeDartLivenessPWHashMap::add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start) {
+        std::pair<LivenessDart*, bool> TimeDartLivenessPWHashMap::add(NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start) {
             discoveredMarkings++;
             TimeDartList& m = markings_storage[marking->getHashKey()];
             for (TimeDartList::const_iterator iter = m.begin();
@@ -61,7 +61,7 @@
             waiting_list->flushBuffer();
         }
 
-        std::pair<LivenessDart*, bool> TimeDartLivenessPWPData::add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start) {
+        std::pair<LivenessDart*, bool> TimeDartLivenessPWPData::add(NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start) {
 
             
             discoveredMarkings++;

=== modified file 'src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp'
--- src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp	2013-05-08 16:29:47 +0000
+++ src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp	2013-08-26 13:51:29 +0000
@@ -43,7 +43,7 @@
             };
 
         public: // modifiers
-            virtual std::pair<LivenessDart*, bool> add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* base, int youngest, WaitingDart* parent, int upper, int start) = 0;
+            virtual std::pair<LivenessDart*, bool> add( NonStrictMarkingBase* base, int youngest, WaitingDart* parent, int upper, int start) = 0;
             virtual WaitingDart* getNextUnexplored() = 0;
             virtual void popWaiting() = 0;
             virtual void flushBuffer() = 0;
@@ -69,7 +69,7 @@
             ~TimeDartLivenessPWHashMap() {
             };
             friend std::ostream& operator<<(std::ostream& out, TimeDartLivenessPWHashMap& x);
-            virtual std::pair<LivenessDart*, bool> add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* base, int youngest, WaitingDart* parent, int upper, int start);
+            virtual std::pair<LivenessDart*, bool> add(NonStrictMarkingBase* base, int youngest, WaitingDart* parent, int upper, int start);
             virtual WaitingDart* getNextUnexplored();
             virtual void popWaiting();
 
@@ -88,13 +88,13 @@
 
 
             
-            TimeDartLivenessPWPData(VerificationOptions options, WaitingList<EncodingPointer<WaitingDart> >* w_l, boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, int nplaces, int mage) : TimeDartLivenessPWBase(), options(options), waiting_list(w_l), passed(tapn,  options.getKBound(), nplaces, mage) {
+            TimeDartLivenessPWPData(VerificationOptions options, WaitingList<EncodingPointer<WaitingDart> >* w_l, TAPN::TimedArcPetriNet& tapn, int nplaces, int mage) : TimeDartLivenessPWBase(), options(options), waiting_list(w_l), passed(tapn,  options.getKBound(), nplaces, mage) {
             };
 
             ~TimeDartLivenessPWPData() {
             };
             friend std::ostream& operator<<(std::ostream& out, TimeDartLivenessPWHashMap& x);
-            virtual std::pair<LivenessDart*, bool> add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* base, int youngest, WaitingDart* parent, int upper, int start);
+            virtual std::pair<LivenessDart*, bool> add(NonStrictMarkingBase* base, int youngest, WaitingDart* parent, int upper, int start);
             virtual WaitingDart* getNextUnexplored();
             virtual void popWaiting();
 

=== modified file 'src/DiscreteVerification/DataStructures/TimeDartPWList.cpp'
--- src/DiscreteVerification/DataStructures/TimeDartPWList.cpp	2013-05-08 16:29:47 +0000
+++ src/DiscreteVerification/DataStructures/TimeDartPWList.cpp	2013-08-26 13:51:29 +0000
@@ -10,7 +10,7 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-bool TimeDartPWHashMap::add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start){
+bool TimeDartPWHashMap::add(NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start){
 	discoveredMarkings++;
 	TimeDartList& m = markings_storage[marking->getHashKey()];
 	for(TimeDartList::const_iterator iter = m.begin();
@@ -53,7 +53,7 @@
 	return waiting_list->pop();
 }
 
-bool TimeDartPWPData::add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start){
+bool TimeDartPWPData::add(NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start){
 	discoveredMarkings++;
         PTrie<TimeDartBase>::Result res = passed.add(marking);
 

=== modified file 'src/DiscreteVerification/DataStructures/TimeDartPWList.hpp'
--- src/DiscreteVerification/DataStructures/TimeDartPWList.hpp	2013-05-08 16:29:47 +0000
+++ src/DiscreteVerification/DataStructures/TimeDartPWList.hpp	2013-08-26 13:51:29 +0000
@@ -39,7 +39,7 @@
                 return stored;
             };
 
-            virtual bool add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start) = 0;
+            virtual bool add(NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start) = 0;
             virtual TimeDartBase* getNextUnexplored() = 0;
 
             inline void setMaxNumTokensIfGreater(int i) {
@@ -71,7 +71,7 @@
             };
             virtual ~TimeDartPWHashMap();
             friend std::ostream& operator<<(std::ostream& out, TimeDartPWHashMap& x);
-            virtual bool add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking,int youngest, WaitingDart* parent, int upper, int start);
+            virtual bool add(NonStrictMarkingBase* marking,int youngest, WaitingDart* parent, int upper, int start);
             virtual TimeDartBase* getNextUnexplored();
 
             virtual bool hasWaitingStates() {
@@ -88,7 +88,7 @@
         class TimeDartPWPData : public TimeDartPWBase {
         public:
 
-            TimeDartPWPData(WaitingList<EncodingPointer<TimeDartBase> >* w_l, boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, int knumber, int nplaces, int mage, bool trace) :
+            TimeDartPWPData(WaitingList<EncodingPointer<TimeDartBase> >* w_l, TAPN::TimedArcPetriNet& tapn, int knumber, int nplaces, int mage, bool trace) :
             TimeDartPWBase(trace), waiting_list(w_l), passed(tapn, knumber, nplaces, mage) {
             };
             
@@ -98,7 +98,7 @@
         private:
             WaitingList<EncodingPointer<TimeDartBase> >* waiting_list;
             PTrie<TimeDartBase> passed;
-            virtual bool add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start);
+            virtual bool add(NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start);
             virtual TimeDartBase* getNextUnexplored();
 
             virtual bool hasWaitingStates() {

=== modified file 'src/DiscreteVerification/DataStructures/WaitingList.hpp'
--- src/DiscreteVerification/DataStructures/WaitingList.hpp	2013-05-08 16:29:47 +0000
+++ src/DiscreteVerification/DataStructures/WaitingList.hpp	2013-08-26 13:51:29 +0000
@@ -13,8 +13,6 @@
 #include <queue>
 #include <stack>
 #include <vector>
-#include "boost/optional.hpp"
-#include "boost/shared_ptr.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../SearchStrategies/WeightQueryVisitor.hpp"
 #include "../SearchStrategies/LivenessWeightQueryVisitor.hpp"
@@ -237,9 +235,9 @@
 int HeuristicStackWaitingList<T>::calculateWeight(NonStrictMarkingBase* marking)
 {
 	LivenessWeightQueryVisitor weight(*marking);
-	boost::any weight_c;
+	IntResult weight_c;
 	query->accept(weight, weight_c);
-	return boost::any_cast<int>(weight_c);
+	return weight_c.value;
 }
 
 template <class T>
@@ -321,9 +319,9 @@
 int HeuristicWaitingList<T>::calculateWeight(NonStrictMarkingBase* marking)
 {
 	WeightQueryVisitor weight(*marking);
-	boost::any weight_c;
+	IntResult weight_c;
 	query->accept(weight, weight_c);
-	return boost::any_cast<int>(weight_c);
+	return weight_c.value;
 }
 
 template <class T>

=== modified file 'src/DiscreteVerification/DeadlockVisitor.cpp'
--- src/DiscreteVerification/DeadlockVisitor.cpp	2013-07-16 20:42:58 +0000
+++ src/DiscreteVerification/DeadlockVisitor.cpp	2013-08-26 13:51:29 +0000
@@ -12,44 +12,46 @@
 
         using namespace AST;
 
-        void DeadlockVisitor::visit(const NotExpression& expr, boost::any& context) {
-            expr.getChild().accept(*this, context);
-        }
-
-        void DeadlockVisitor::visit(const ParExpression& expr, boost::any& context) {
-            expr.getChild().accept(*this, context);
-        }
-
-        void DeadlockVisitor::visit(const OrExpression& expr, boost::any& context) {
-            boost::any left, right;
-            expr.getLeft().accept(*this, left);
-            expr.getRight().accept(*this, right);
-
-            context = boost::any_cast<bool>(left) || boost::any_cast<bool>(right);
-        }
-
-        void DeadlockVisitor::visit(const AndExpression& expr, boost::any& context) {
-            boost::any left, right;
-            expr.getLeft().accept(*this, left);
-            expr.getRight().accept(*this, right);
-
-            context = boost::any_cast<bool>(left) || boost::any_cast<bool>(right);
-        }
-
-        void DeadlockVisitor::visit(const AtomicProposition& expr, boost::any& context) {
-            context = false;
-        }
-
-        void DeadlockVisitor::visit(const BoolExpression& expr, boost::any& context) {
-            context = false;
-        }
-
-        void DeadlockVisitor::visit(const Query& query, boost::any& context) {
+        void DeadlockVisitor::visit(const NotExpression& expr, Result& context) {
+            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);
+            expr.getRight().accept(*this, right);
+
+            static_cast<BoolResult&>(context).value
+                    = left.value || right.value;
+        }
+
+        void DeadlockVisitor::visit(const AndExpression& expr, Result& context) {
+            BoolResult left, right;
+            expr.getLeft().accept(*this, left);
+            expr.getRight().accept(*this, right);
+
+            static_cast<BoolResult&>(context).value 
+                    = left.value || right.value;
+        }
+
+        void DeadlockVisitor::visit(const AtomicProposition& expr, Result& context) {
+            static_cast<BoolResult&>(context).value = false;
+        }
+
+        void DeadlockVisitor::visit(const BoolExpression& expr, Result& context) {
+            static_cast<BoolResult&>(context).value = false;
+        }
+
+        void DeadlockVisitor::visit(const Query& query, Result& context) {
             query.getChild().accept(*this, context);
         }
 
-        void DeadlockVisitor::visit(const DeadlockExpression& expr, boost::any& context) {
-            context = true;
+        void DeadlockVisitor::visit(const DeadlockExpression& expr, Result& context) {
+            static_cast<BoolResult&>(context).value = true;
         }
     }
 }

=== modified file 'src/DiscreteVerification/DeadlockVisitor.hpp'
--- src/DiscreteVerification/DeadlockVisitor.hpp	2013-08-12 15:39:11 +0000
+++ src/DiscreteVerification/DeadlockVisitor.hpp	2013-08-26 13:51:29 +0000
@@ -27,15 +27,14 @@
             };
 
         public: // visitor methods
-
-            virtual void visit(const NotExpression& expr, boost::any& context);
-            virtual void visit(const ParExpression& expr, boost::any& context);
-            virtual void visit(const OrExpression& expr, boost::any& context);
-            virtual void visit(const AndExpression& expr, boost::any& context);
-            virtual void visit(const AtomicProposition& expr, boost::any& context);
-            virtual void visit(const BoolExpression& expr, boost::any& context);
-            virtual void visit(const Query& query, boost::any& context);
-            virtual void visit(const DeadlockExpression& expr, boost::any& context);
+            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);
 
         };
     } /* namespace DiscreteVerification */

=== modified file 'src/DiscreteVerification/DiscreteVerification.cpp'
--- src/DiscreteVerification/DiscreteVerification.cpp	2013-07-05 13:16:38 +0000
+++ src/DiscreteVerification/DiscreteVerification.cpp	2013-08-26 13:51:29 +0000
@@ -12,7 +12,7 @@
 
     namespace DiscreteVerification {
 
-        template<typename T> void VerifyAndPrint(Verification<T>* verifier, VerificationOptions& options, AST::Query* query);
+        template<typename T> void VerifyAndPrint(Verification<T>& verifier, VerificationOptions& options, AST::Query* query);
 
         DiscreteVerification::DiscreteVerification() {
             // TODO Auto-generated constructor stub
@@ -23,15 +23,15 @@
             // TODO Auto-generated destructor stub
         }
 
-        int DiscreteVerification::run(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, std::vector<int> initialPlacement, AST::Query* query, VerificationOptions& options) {
-            if (!(*tapn).isNonStrict()) {
+        int DiscreteVerification::run(TAPN::TimedArcPetriNet& tapn, std::vector<int> initialPlacement, AST::Query* query, VerificationOptions& options) {
+            if (!tapn.isNonStrict()) {
                 std::cout << "The supplied net contains strict intervals." << std::endl;
                 return -1;
             }
 
-            NonStrictMarking* initialMarking = new NonStrictMarking(*tapn, initialPlacement);
+            NonStrictMarking* initialMarking = new NonStrictMarking(tapn, initialPlacement);
 
-            std::cout << "MC: " << tapn->getMaxConstant() << std::endl;
+            std::cout << "MC: " << tapn.getMaxConstant() << std::endl;
 #if DEBUG
             std::cout << "Places: " << std::endl;
             for (TAPN::TimedPlace::Vector::const_iterator iter = tapn.get()->getPlaces().begin(); iter != tapn.get()->getPlaces().end(); iter++) {
@@ -54,50 +54,56 @@
                     //TODO fix initialization
                     WaitingList<EncodingPointer<MetaData> >* strategy = getWaitingList<EncodingPointer<MetaData> > (query, options);
                     if (query->getQuantifier() == EG || query->getQuantifier() == AF) {
+                        LivenessSearchPTrie verifier = LivenessSearchPTrie(tapn, *initialMarking, query, options, strategy);
                         VerifyAndPrint(
-                                new LivenessSearchPTrie(tapn, *initialMarking, query, options, strategy),
+                                verifier,
                                 options,
                                 query);
                     } else if (query->getQuantifier() == EF || query->getQuantifier() == AG) {
+                        ReachabilitySearchPTrie verifier = ReachabilitySearchPTrie(tapn, *initialMarking, query, options, strategy);
                         VerifyAndPrint(
-                                new ReachabilitySearchPTrie(tapn, *initialMarking, query, options, strategy),
+                                verifier,
                                 options,
                                 query);
                     }
                 } else {
                     WaitingList<NonStrictMarking>* strategy = getWaitingList<NonStrictMarking > (query, options);
                     if (query->getQuantifier() == EG || query->getQuantifier() == AF) {
+                        LivenessSearch verifier = LivenessSearch(tapn, *initialMarking, query, options, strategy);
                         VerifyAndPrint(
-                                new LivenessSearch(tapn, *initialMarking, query, options, strategy),
+                                verifier,
                                 options,
                                 query);
                     } else if (query->getQuantifier() == EF || query->getQuantifier() == AG) {
+                        ReachabilitySearch verifier = ReachabilitySearch(tapn, *initialMarking, query, options, strategy);
                         VerifyAndPrint(
-                                new ReachabilitySearch(tapn, *initialMarking, query, options, strategy),
+                                verifier,
                                 options,
                                 query);
                     }
                 }
             } else if (options.getVerificationType() == VerificationOptions::TIMEDART) {
                 if (query->getQuantifier() == EG || query->getQuantifier() == AF) {
-                    boost::any c;
+                    AST::BoolResult containsDeadlock;
                     DeadlockVisitor deadlockVisitor = DeadlockVisitor();
-                    deadlockVisitor.visit(*query, c);
-                    bool containsDeadlock = boost::any_cast<bool>(c);
-                    if (containsDeadlock) {
+                    deadlockVisitor.visit(*query, containsDeadlock);
+
+                    if (containsDeadlock.value) {
                         cout << "The combination of TimeDarts, Deadlock proposition and EG or AF queries is currently not supported" << endl;
                         exit(1);
                     }                
                     if (options.getMemoryOptimization() == VerificationOptions::PTRIE) {
                         WaitingList<EncodingPointer<WaitingDart> >* strategy = getWaitingList<EncodingPointer<WaitingDart> > (query, options);
+                        TimeDartLivenessPData verifier = TimeDartLivenessPData(tapn, *initialMarking, query, options, strategy);
                         VerifyAndPrint(
-                                new TimeDartLivenessPData(tapn, *initialMarking, query, options, strategy),
+                                verifier,
                                 options,
                                 query);
                     } else {
                         WaitingList<WaitingDart>* strategy = getWaitingList<WaitingDart > (query, options);
+                        TimeDartLiveness verifier = TimeDartLiveness(tapn, *initialMarking, query, options, strategy);
                         VerifyAndPrint(
-                                new TimeDartLiveness(tapn, *initialMarking, query, options, strategy),
+                                verifier,
                                 options,
                                 query);
                     }
@@ -105,14 +111,16 @@
 
                     if (options.getMemoryOptimization() == VerificationOptions::PTRIE) {
                         WaitingList<TimeDartEncodingPointer>* strategy = getWaitingList<TimeDartEncodingPointer > (query, options);
+                        TimeDartReachabilitySearchPData verifier = TimeDartReachabilitySearchPData(tapn, *initialMarking, query, options, strategy);
                         VerifyAndPrint(
-                                new TimeDartReachabilitySearchPData(tapn, *initialMarking, query, options, strategy),
+                                verifier,
                                 options,
                                 query);
                     } else {
                         WaitingList<TimeDartBase>* strategy = getWaitingList<TimeDartBase > (query, options);
+                        TimeDartReachabilitySearch verifier = TimeDartReachabilitySearch(tapn, *initialMarking, query, options, strategy);
                         VerifyAndPrint(
-                                new TimeDartReachabilitySearch(tapn, *initialMarking, query, options, strategy),
+                                verifier,
                                 options,
                                 query);
                     }
@@ -125,22 +133,22 @@
             return 0;
         }
 
-        template<typename T> void VerifyAndPrint(Verification<T>* verifier, VerificationOptions& options, AST::Query* query) {
-            bool result = (query->getQuantifier() == AG || query->getQuantifier() == AF) ? !verifier->verify() : verifier->verify();
+        template<typename T> void VerifyAndPrint(Verification<T>& verifier, VerificationOptions& options, AST::Query* query) {
+            bool result = (query->getQuantifier() == AG || query->getQuantifier() == AF) ? !verifier.verify() : verifier.verify();
 
-            verifier->printStats();
-            verifier->printTransitionStatistics();
+            verifier.printStats();
+            verifier.printTransitionStatistics();
 
             std::cout << "Query is " << (result ? "satisfied" : "NOT satisfied") << "." << std::endl;
             std::cout << "Max number of tokens found in any reachable marking: ";
-            if (verifier->maxUsedTokens() > options.getKBound())
+            if (verifier.maxUsedTokens() > options.getKBound())
                 std::cout << ">" << options.getKBound() << std::endl;
             else
-                std::cout << verifier->maxUsedTokens() << std::endl;
+                std::cout << verifier.maxUsedTokens() << std::endl;
 
             if (options.getTrace() == VerificationOptions::SOME_TRACE) {
                 if ((query->getQuantifier() == EF && result) || (query->getQuantifier() == AG && !result) || (query->getQuantifier() == EG && result) || (query->getQuantifier() == AF && !result)) {
-                    verifier->getTrace();
+                    verifier.getTrace();
                 } else {
                     std::cout << "A trace could not be generated due to the query result" << std::endl;
                 }

=== modified file 'src/DiscreteVerification/DiscreteVerification.hpp'
--- src/DiscreteVerification/DiscreteVerification.hpp	2013-05-08 16:29:47 +0000
+++ src/DiscreteVerification/DiscreteVerification.hpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,6 @@
 #define DISCRETEVERIFICATION_HPP_
 
 #include <iostream>
-#include "boost/smart_ptr.hpp"
 #include "../Core/TAPN/TAPN.hpp"
 #include "../Core/QueryParser/AST.hpp"
 #include "../Core/VerificationOptions.hpp"
@@ -36,7 +35,7 @@
 public:
 	DiscreteVerification();
 	virtual ~DiscreteVerification();
-	static int run(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, std::vector<int> initialPlacement, AST::Query* query, VerificationOptions& options);
+	static int run(TAPN::TimedArcPetriNet& tapn, std::vector<int> initialPlacement, AST::Query* query, VerificationOptions& options);
 private:
 	static void printHumanTrace(bool result, NonStrictMarking* m, std::stack<NonStrictMarking*>& stack, AST::Quantifier query);
 	static void printXMLTrace(bool result, NonStrictMarking* m, std::stack<NonStrictMarking*>& stack, AST::Quantifier query);

=== modified file 'src/DiscreteVerification/PlaceVisitor.cpp'
--- src/DiscreteVerification/PlaceVisitor.cpp	2013-06-04 11:39:54 +0000
+++ src/DiscreteVerification/PlaceVisitor.cpp	2013-08-26 13:51:29 +0000
@@ -10,44 +10,43 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-		void PlaceVisitor::visit(const NotExpression& expr, boost::any& context)
-		{
-			expr.getChild().accept(*this, context);
-		}
-
-		void PlaceVisitor::visit(const ParExpression& expr, boost::any& context)
-		{
-			expr.getChild().accept(*this, context);
-		}
-
-		void PlaceVisitor::visit(const OrExpression& expr, boost::any& context)
-		{
-			expr.getLeft().accept(*this, context);
-			expr.getRight().accept(*this, context);
-		}
-
-		void PlaceVisitor::visit(const AndExpression& expr, boost::any& context)
-		{
-			expr.getLeft().accept(*this, context);
-			expr.getRight().accept(*this, context);
-		}
-
-		void PlaceVisitor::visit(const AtomicProposition& expr, boost::any& context)
-		{
-			std::vector<int> v = boost::any_cast< std::vector< int > >(context);
-			v.push_back(expr.getPlace());
-			context = v;
-		}
-
-                void PlaceVisitor::visit(const DeadlockExpression& expr, boost::any& context)
+		void PlaceVisitor::visit(const NotExpression& expr, Result& context)
+		{
+			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);
+			expr.getRight().accept(*this, context);
+		}
+
+		void PlaceVisitor::visit(const AndExpression& expr, Result& context)
+		{
+			expr.getLeft().accept(*this, context);
+			expr.getRight().accept(*this, context);
+		}
+
+		void PlaceVisitor::visit(const AtomicProposition& expr, Result& context)
+		{
+			AST::IntVectorResult& v = static_cast< AST::IntVectorResult & >(context);
+			v.value.push_back(expr.getPlace());
+		}
+
+                void PlaceVisitor::visit(const DeadlockExpression& expr, Result& context)
 		{
 		}
                 
-		void PlaceVisitor::visit(const BoolExpression& expr, boost::any& context)
+		void PlaceVisitor::visit(const BoolExpression& expr, Result& context)
 		{
 		}
 
-		void PlaceVisitor::visit(const Query& query, boost::any& context)
+		void PlaceVisitor::visit(const Query& query, Result& context)
 		{
 			query.getChild().accept(*this, context);
 		}

=== modified file 'src/DiscreteVerification/PlaceVisitor.hpp'
--- src/DiscreteVerification/PlaceVisitor.hpp	2013-06-04 11:39:54 +0000
+++ src/DiscreteVerification/PlaceVisitor.hpp	2013-08-26 13:51:29 +0000
@@ -24,14 +24,14 @@
 		virtual ~PlaceVisitor(){};
 
 	public: // visitor methods
-		virtual void visit(const NotExpression& expr, boost::any& context);
-		virtual void visit(const ParExpression& expr, boost::any& context);
-		virtual void visit(const OrExpression& expr, boost::any& context);
-		virtual void visit(const AndExpression& expr, boost::any& context);
-		virtual void visit(const AtomicProposition& expr, boost::any& context);
-		virtual void visit(const BoolExpression& expr, boost::any& context);
-		virtual void visit(const Query& query, boost::any& context);
-		virtual void visit(const DeadlockExpression& expr, boost::any& context);
+		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);
 };
 
 } /* namespace DiscreteVerification */

=== modified file 'src/DiscreteVerification/QueryVisitor.hpp'
--- src/DiscreteVerification/QueryVisitor.hpp	2013-07-05 14:00:53 +0000
+++ src/DiscreteVerification/QueryVisitor.hpp	2013-08-26 13:51:29 +0000
@@ -37,14 +37,14 @@
 
         public: // visitor methods
 
-            virtual void visit(const NotExpression& expr, boost::any& context);
-            virtual void visit(const ParExpression& expr, boost::any& context);
-            virtual void visit(const OrExpression& expr, boost::any& context);
-            virtual void visit(const AndExpression& expr, boost::any& context);
-            virtual void visit(const AtomicProposition& expr, boost::any& context);
-            virtual void visit(const BoolExpression& expr, boost::any& context);
-            virtual void visit(const Query& query, boost::any& context);
-            virtual void visit(const DeadlockExpression& expr, boost::any& context);
+            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);
         private:
             bool compare(int numberOfTokensInPlace, const std::string& op, int n) const;
 
@@ -57,62 +57,75 @@
         };
         
         template<typename T>
-        void QueryVisitor<T>::visit(const NotExpression& expr, boost::any& context) {
-            boost::any c;
+        void QueryVisitor<T>::visit(const NotExpression& expr, AST::Result& context) {
+            BoolResult c;
             expr.getChild().accept(*this, c);
-            context = !boost::any_cast<bool>(c);
+            static_cast<BoolResult&>(context).value = !c.value;
         }
 
         template<typename T>
-        void QueryVisitor<T>::visit(const ParExpression& expr, boost::any& context) {
+        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, boost::any& context) {
-            boost::any left, right;
-            expr.getLeft().accept(*this, left);
-            expr.getRight().accept(*this, right);
-
-            context = boost::any_cast<bool>(left) || boost::any_cast<bool>(right);
-        }
-
-        template<typename T>
-        void QueryVisitor<T>::visit(const AndExpression& expr, boost::any& context) {
-            boost::any left, right;
-            expr.getLeft().accept(*this, left);
-            expr.getRight().accept(*this, right);
-
-            context = boost::any_cast<bool>(left) && boost::any_cast<bool>(right);
-        }
-
-        template<typename T>
-
-        void QueryVisitor<T>::visit(const AtomicProposition& expr, boost::any& context) {
+        void QueryVisitor<T>::visit(const OrExpression& expr, AST::Result& context) {
+            BoolResult left, right;
+            expr.getLeft().accept(*this, left);
+            // use lazy evaluation
+            if(left.value){
+                static_cast<BoolResult&>(context).value = true;
+            } else {
+                expr.getRight().accept(*this, right);
+                static_cast<BoolResult&>(context).value = right.value;
+            }
+        }
+
+        template<typename T>
+        void QueryVisitor<T>::visit(const AndExpression& expr, AST::Result& context) {
+            BoolResult left, right;
+            expr.getLeft().accept(*this, left);
+            
+            // use lazy evaluation
+            if(!left.value){
+                static_cast<BoolResult&>(context).value = false;
+            } else {
+                expr.getRight().accept(*this, right);
+                static_cast<BoolResult&>(context).value = right.value;
+            }
+        }
+
+        template<typename T>
+
+        void QueryVisitor<T>::visit(const AtomicProposition& expr, AST::Result& context) {
             int numberOfTokens = marking.numberOfTokensInPlace(expr.getPlace());
-            context = compare(numberOfTokens, expr.getOperator(), expr.getNumberOfTokens());
-        }
-
-        template<typename T>
-        void QueryVisitor<T>::visit(const BoolExpression& expr, boost::any& context) {
-            context = expr.getValue();
-        }
-
-        template<typename T>
-        void QueryVisitor<T>::visit(const Query& query, boost::any& context) {
+            static_cast<BoolResult&>(context).value 
+                    = compare(numberOfTokens, expr.getOperator(), expr.getNumberOfTokens());
+        }
+
+        template<typename T>
+        void QueryVisitor<T>::visit(const BoolExpression& expr, AST::Result& context) {
+            static_cast<BoolResult&>(context).value 
+                    = expr.getValue();
+        }
+
+        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) {
-                context = !boost::any_cast<bool>(context);
+                static_cast<BoolResult&>(context).value
+                        = !static_cast<BoolResult&>(context).value;
             }
         }
         
         template<typename T>
-        void QueryVisitor<T>::visit(const DeadlockExpression& expr, boost::any& context) {
+        void QueryVisitor<T>::visit(const DeadlockExpression& expr, AST::Result& context) {
             if(!deadlockChecked){
                 deadlockChecked = true;
                 deadlocked = marking.canDeadlock(tapn, maxDelay);
             }
-            context = deadlocked;
+            static_cast<BoolResult&>(context).value 
+                    = deadlocked;
         }
 
         template<typename T>

=== modified file 'src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.cpp'
--- src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.cpp	2013-06-22 20:22:35 +0000
+++ src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.cpp	2013-08-26 13:51:29 +0000
@@ -10,66 +10,67 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-		void LivenessWeightQueryVisitor::visit(const NotExpression& expr, boost::any& context)
+		void LivenessWeightQueryVisitor::visit(const NotExpression& expr, Result& context)
 		{
 			assert(false);
 		}
 
-		void LivenessWeightQueryVisitor::visit(const ParExpression& expr, boost::any& context)
+		void LivenessWeightQueryVisitor::visit(const ParExpression& expr, Result& context)
 		{
 			expr.getChild().accept(*this, context);
 		}
 
-		void LivenessWeightQueryVisitor::visit(const OrExpression& expr, boost::any& context)
-		{
-			boost::any left, right;
-			expr.getLeft().accept(*this, left);
-			expr.getRight().accept(*this, right);
-
-			context = min(boost::any_cast<int>(left), boost::any_cast<int>(right));
-		}
-
-		void LivenessWeightQueryVisitor::visit(const AndExpression& expr, boost::any& context)
-		{
-			boost::any left, right;
-			expr.getLeft().accept(*this, left);
-			expr.getRight().accept(*this, right);
-
-			int l = boost::any_cast<int>(left);
-			if(l == std::numeric_limits<int>::max()){
-				context = l;
-				return;
-			}
-
-			int r = boost::any_cast<int>(right);
-			if(r == std::numeric_limits<int>::max()){
-				context = r;
-				return;
-			}
-
-			context = l+r;
-		}
-
-
-		void LivenessWeightQueryVisitor::visit(const AtomicProposition& expr, boost::any& context)
+		void LivenessWeightQueryVisitor::visit(const OrExpression& expr, Result& context)
+		{
+			IntResult left, right;
+			expr.getLeft().accept(*this, left);
+			expr.getRight().accept(*this, right);
+
+			static_cast<IntResult&>(context).value 
+                                = min(static_cast<IntResult>(left).value, static_cast<IntResult>(right).value);
+		}
+
+		void LivenessWeightQueryVisitor::visit(const AndExpression& expr, Result& context)
+		{
+			IntResult left, right;
+                        
+			expr.getLeft().accept(*this, left);
+			if(left.value == std::numeric_limits<int>::max()){
+				static_cast<IntResult&>(context).value = left.value;
+				return;
+			}
+                        
+			expr.getRight().accept(*this, right);
+			if(right.value == std::numeric_limits<int>::max()){
+				static_cast<IntResult&>(context).value = right.value;
+				return;
+			}
+
+			static_cast<IntResult&>(context).value = left.value+right.value;
+		}
+
+
+		void LivenessWeightQueryVisitor::visit(const AtomicProposition& expr, Result& context)
 		{
 			int numberOfTokens = marking.numberOfTokensInPlace(expr.getPlace());
-			context = compare(numberOfTokens, expr.getOperator(), expr.getNumberOfTokens());
+			static_cast<IntResult&>(context).value
+                                = compare(numberOfTokens, expr.getOperator(), expr.getNumberOfTokens());
 		}
 
-		void LivenessWeightQueryVisitor::visit(const BoolExpression& expr, boost::any& context)
+		void LivenessWeightQueryVisitor::visit(const BoolExpression& expr, Result& context)
 		{
-			context = expr.getValue()? 0 : std::numeric_limits<int>::max();
+			static_cast<IntResult&>(context).value 
+                                = expr.getValue()? 0 : std::numeric_limits<int>::max();
 		}
 
-		void LivenessWeightQueryVisitor::visit(const Query& query, boost::any& context)
+		void LivenessWeightQueryVisitor::visit(const Query& query, Result& context)
 		{
 			query.getChild().accept(*this, context);
 		}
 
-                void LivenessWeightQueryVisitor::visit(const DeadlockExpression& expr, boost::any& context)
+                void LivenessWeightQueryVisitor::visit(const DeadlockExpression& expr, Result& context)
 		{
-                        context = 0;
+                        static_cast<IntResult&>(context).value = 0;
 		}
                 
 		int LivenessWeightQueryVisitor::compare(int numberOfTokensInPlace, const std::string& op, int n) const

=== modified file 'src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.hpp'
--- src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.hpp	2013-06-04 11:39:54 +0000
+++ src/DiscreteVerification/SearchStrategies/LivenessWeightQueryVisitor.hpp	2013-08-26 13:51:29 +0000
@@ -25,14 +25,14 @@
 		virtual ~LivenessWeightQueryVisitor(){};
 
 	public: // visitor methods
-		virtual void visit(const NotExpression& expr, boost::any& context);
-		virtual void visit(const ParExpression& expr, boost::any& context);
-		virtual void visit(const OrExpression& expr, boost::any& context);
-		virtual void visit(const AndExpression& expr, boost::any& context);
-		virtual void visit(const AtomicProposition& expr, boost::any& context);
-		virtual void visit(const BoolExpression& expr, boost::any& context);
-		virtual void visit(const Query& query, boost::any& context);
-                virtual void visit(const DeadlockExpression& expr, boost::any& context);
+		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);
 	private:
 		int compare(int numberOfTokensInPlace, const std::string& op, int n) const;
 

=== modified file 'src/DiscreteVerification/SearchStrategies/NonStrictBFS.hpp'
--- src/DiscreteVerification/SearchStrategies/NonStrictBFS.hpp	2013-04-23 10:43:58 +0000
+++ src/DiscreteVerification/SearchStrategies/NonStrictBFS.hpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,6 @@
 #define NONSTRICTBFS_HPP_
 
 #include "../DataStructures/PWList.hpp"
-#include "boost/smart_ptr.hpp"
 #include "../../Core/TAPN/TAPN.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../../Core/VerificationOptions.hpp"
@@ -24,7 +23,6 @@
 #include "../SuccessorGenerator.hpp"
 
 #include "../QueryVisitor.hpp"
-#include "boost/any.hpp"
 #include "SearchStrategy.hpp"
 
 #include <stack>

=== modified file 'src/DiscreteVerification/SearchStrategies/NonStrictDFS.hpp'
--- src/DiscreteVerification/SearchStrategies/NonStrictDFS.hpp	2013-04-23 10:43:58 +0000
+++ src/DiscreteVerification/SearchStrategies/NonStrictDFS.hpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,6 @@
 #define NONSTRICTDFS_HPP_
 
 #include "../DataStructures/PWList.hpp"
-#include "boost/smart_ptr.hpp"
 #include "../../Core/TAPN/TAPN.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../../Core/VerificationOptions.hpp"
@@ -24,7 +23,6 @@
 #include "../SuccessorGenerator.hpp"
 
 #include "../QueryVisitor.hpp"
-#include "boost/any.hpp"
 #include "SearchStrategy.hpp"
 
 #include <stack>

=== modified file 'src/DiscreteVerification/SearchStrategies/NonStrictDFSHeuristic.hpp'
--- src/DiscreteVerification/SearchStrategies/NonStrictDFSHeuristic.hpp	2013-04-23 10:43:58 +0000
+++ src/DiscreteVerification/SearchStrategies/NonStrictDFSHeuristic.hpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,6 @@
 #define NONSTRICTDFSHEURISTIC_HPP_
 
 #include "../DataStructures/PWList.hpp"
-#include "boost/smart_ptr.hpp"
 #include "../../Core/TAPN/TAPN.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../../Core/VerificationOptions.hpp"
@@ -24,7 +23,6 @@
 #include "../SuccessorGenerator.hpp"
 
 #include "../QueryVisitor.hpp"
-#include "boost/any.hpp"
 
 #include <stack>
 #include "SearchStrategy.hpp"

=== modified file 'src/DiscreteVerification/SearchStrategies/NonStrictDFSRandom.hpp'
--- src/DiscreteVerification/SearchStrategies/NonStrictDFSRandom.hpp	2013-04-23 10:43:58 +0000
+++ src/DiscreteVerification/SearchStrategies/NonStrictDFSRandom.hpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,6 @@
 #define NONSTRICTDFSRANDOM_HPP_
 
 #include "../DataStructures/PWList.hpp"
-#include "boost/smart_ptr.hpp"
 #include "../../Core/TAPN/TAPN.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../../Core/VerificationOptions.hpp"
@@ -24,7 +23,6 @@
 #include "../SuccessorGenerator.hpp"
 
 #include "../QueryVisitor.hpp"
-#include "boost/any.hpp"
 #include "SearchStrategy.hpp"
 
 #include <stack>

=== modified file 'src/DiscreteVerification/SearchStrategies/NonStrictHeuristic.hpp'
--- src/DiscreteVerification/SearchStrategies/NonStrictHeuristic.hpp	2013-04-23 10:43:58 +0000
+++ src/DiscreteVerification/SearchStrategies/NonStrictHeuristic.hpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,6 @@
 #define NONSTRICTHEURISTIC_HPP_
 
 #include "../DataStructures/PWList.hpp"
-#include "boost/smart_ptr.hpp"
 #include "../../Core/TAPN/TAPN.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../../Core/VerificationOptions.hpp"
@@ -24,7 +23,6 @@
 #include "../SuccessorGenerator.hpp"
 
 #include "../QueryVisitor.hpp"
-#include "boost/any.hpp"
 
 #include <stack>
 #include "SearchStrategy.hpp"

=== modified file 'src/DiscreteVerification/SearchStrategies/NonStrictRandom.hpp'
--- src/DiscreteVerification/SearchStrategies/NonStrictRandom.hpp	2013-04-23 10:43:58 +0000
+++ src/DiscreteVerification/SearchStrategies/NonStrictRandom.hpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,6 @@
 #define NONSTRICTRANDOM_HPP_
 
 #include "../DataStructures/PWList.hpp"
-#include "boost/smart_ptr.hpp"
 #include "../../Core/TAPN/TAPN.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../../Core/VerificationOptions.hpp"
@@ -24,7 +23,6 @@
 #include "../SuccessorGenerator.hpp"
 
 #include "../QueryVisitor.hpp"
-#include "boost/any.hpp"
 #include "SearchStrategy.hpp"
 
 #include <stack>

=== modified file 'src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.cpp'
--- src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.cpp	2013-06-30 15:24:02 +0000
+++ src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.cpp	2013-08-26 13:51:29 +0000
@@ -10,63 +10,65 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-		void WeightQueryVisitor::visit(const NotExpression& expr, boost::any& context)
+		void WeightQueryVisitor::visit(const NotExpression& expr, Result& context)
 		{
 			assert(false);
 		}
 
-		void WeightQueryVisitor::visit(const ParExpression& expr, boost::any& context)
+		void WeightQueryVisitor::visit(const ParExpression& expr, Result& context)
 		{
 			expr.getChild().accept(*this, context);
 		}
 
-		void WeightQueryVisitor::visit(const OrExpression& expr, boost::any& context)
-		{
-			boost::any left, right;
-			expr.getLeft().accept(*this, left);
-			expr.getRight().accept(*this, right);
-
-			context = min(boost::any_cast<int>(left), boost::any_cast<int>(right));
-		}
-
-		void WeightQueryVisitor::visit(const AndExpression& expr, boost::any& context)
-		{
-			boost::any left, right;
-			expr.getLeft().accept(*this, left);
-			expr.getRight().accept(*this, right);
-
-			int l = boost::any_cast<int>(left);
-			if(l == std::numeric_limits<int>::max()){
-				context = l;
-				return;
-			}
-
-			int r = boost::any_cast<int>(right);
-			if(r == std::numeric_limits<int>::max()){
-				context = r;
-				return;
-			}
-
-			context = l+r;
-		}
-
-                void WeightQueryVisitor::visit(const DeadlockExpression& expr, boost::any& context)
-		{
-                    context = 0;
-		}
-
-		void WeightQueryVisitor::visit(const AtomicProposition& expr, boost::any& context)
+		void WeightQueryVisitor::visit(const OrExpression& expr, Result& context)
+		{
+			IntResult left, right;
+			expr.getLeft().accept(*this, left);
+			expr.getRight().accept(*this, right);
+
+			static_cast<IntResult&>(context).value
+                                = min(left.value, right.value);
+		}
+
+		void WeightQueryVisitor::visit(const AndExpression& expr, Result& context)
+		{
+			IntResult left, right;
+                        
+			expr.getLeft().accept(*this, left);
+			if(left.value == std::numeric_limits<int>::max()){
+				static_cast<IntResult&>(context).value = left.value;
+				return;
+			}
+
+                        expr.getRight().accept(*this, right);
+			if(right.value == std::numeric_limits<int>::max()){
+				static_cast<IntResult&>(context).value = right.value;
+				return;
+			}
+
+			static_cast<IntResult&>(context).value 
+                                = left.value+right.value;
+		}
+
+                void WeightQueryVisitor::visit(const DeadlockExpression& expr, Result& context)
+		{
+                    static_cast<IntResult&>(context).value = 0;
+		}
+
+		void WeightQueryVisitor::visit(const AtomicProposition& expr, Result& context)
 		{
 			int numberOfTokens = marking.numberOfTokensInPlace(expr.getPlace());
-			context = compare(numberOfTokens, expr.getOperator(), expr.getNumberOfTokens());
+			static_cast<IntResult&>(context).value
+                                = compare(numberOfTokens, expr.getOperator(), expr.getNumberOfTokens());
 		}
 
-		void WeightQueryVisitor::visit(const BoolExpression& expr, boost::any& context)
+		void WeightQueryVisitor::visit(const BoolExpression& expr, Result& context)
 		{
-			context = expr.getValue()? 0 : std::numeric_limits<int>::max();
+			static_cast<IntResult&>(context).value
+                                = expr.getValue()? 0 : std::numeric_limits<int>::max();
 		}
 
-		void WeightQueryVisitor::visit(const Query& query, boost::any& context)
+		void WeightQueryVisitor::visit(const Query& query, Result& context)
 		{
 			query.getChild().accept(*this, context);
 		}

=== modified file 'src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.hpp'
--- src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.hpp	2013-06-04 11:39:54 +0000
+++ src/DiscreteVerification/SearchStrategies/WeightQueryVisitor.hpp	2013-08-26 13:51:29 +0000
@@ -25,14 +25,14 @@
 		virtual ~WeightQueryVisitor(){};
 
 	public: // visitor methods
-		virtual void visit(const NotExpression& expr, boost::any& context);
-		virtual void visit(const ParExpression& expr, boost::any& context);
-		virtual void visit(const OrExpression& expr, boost::any& context);
-		virtual void visit(const AndExpression& expr, boost::any& context);
-		virtual void visit(const AtomicProposition& expr, boost::any& context);
-		virtual void visit(const BoolExpression& expr, boost::any& context);
-		virtual void visit(const Query& query, boost::any& context);
-                virtual void visit(const DeadlockExpression& expr, boost::any& context);
+		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);
 	private:
 		int compare(int numberOfTokensInPlace, const std::string& op, int n) const;
 

=== modified file 'src/DiscreteVerification/SuccessorGenerator.hpp'
--- src/DiscreteVerification/SuccessorGenerator.hpp	2013-07-20 10:03:22 +0000
+++ src/DiscreteVerification/SuccessorGenerator.hpp	2013-08-26 13:51:29 +0000
@@ -12,8 +12,7 @@
 #include "DataStructures/NonStrictMarking.hpp"
 #include "google/sparse_hash_map"
 #include <limits>
-#include "boost/tuple/tuple_io.hpp"
-#include "boost/ptr_container/ptr_vector.hpp"
+#include <vector>
 #include "VerificationTypes/Verification.hpp"
 
 namespace VerifyTAPN {
@@ -21,7 +20,6 @@
 
         using namespace std;
         using namespace TAPN;
-        using namespace boost;
 
         struct ArcRef {
             TokenList enabledBy;
@@ -32,23 +30,23 @@
 
         struct InputArcRef : ArcRef {
 
-            InputArcRef(boost::weak_ptr<TimedInputArc> arc) : arc(arc) {
+            InputArcRef(const TimedInputArc& arc) : arc(arc) {
             }
-            boost::weak_ptr<TimedInputArc> arc;
+            const TimedInputArc& arc;
         };
 
         struct InhibitorArcRef : ArcRef {
 
-            InhibitorArcRef(boost::weak_ptr<InhibitorArc> arc) : arc(arc) {
+            InhibitorArcRef(const InhibitorArc& arc) : arc(arc) {
             }
-            boost::weak_ptr<InhibitorArc> arc;
+            const InhibitorArc& arc;
         };
 
         struct TransportArcRef : ArcRef {
 
-            TransportArcRef(boost::weak_ptr<TransportArc> arc) : arc(arc) {
+            TransportArcRef(const TransportArc& arc) : arc(arc) {
             }
-            boost::weak_ptr<TransportArc> arc;
+            const TransportArc& arc;
         };
 
         template<typename T>
@@ -98,37 +96,37 @@
         template<typename T>
         class InputArcAndTokens : public ArcAndTokens<T> {
         public:
-            boost::weak_ptr<TimedInputArc> arc;
+            const TimedInputArc& arc;
 
-            InputArcAndTokens(boost::weak_ptr<TimedInputArc> arc, TokenList enabledBy, vector<unsigned int > modificationVector)
+            InputArcAndTokens(const TimedInputArc& arc, TokenList enabledBy, vector<unsigned int > modificationVector)
             : ArcAndTokens<T>(enabledBy, modificationVector), arc(arc) {
             }
 
-            InputArcAndTokens(boost::weak_ptr<TimedInputArc> arc, TokenList enabledBy)
-            : ArcAndTokens<T>(enabledBy, arc.lock()->getWeight()), arc(arc) {
+            InputArcAndTokens(const TimedInputArc& arc, TokenList enabledBy)
+            : ArcAndTokens<T>(enabledBy, arc.getWeight()), arc(arc) {
             }
 
             void moveToken(Token& token, T& m) {
-                m.removeToken(arc.lock()->getInputPlace().getIndex(), token.getAge());
+                m.removeToken(arc.getInputPlace().getIndex(), token.getAge());
             }
         };
 
         template<typename T>
         class TransportArcAndTokens : public ArcAndTokens<T> {
         public:
-            boost::weak_ptr<TransportArc> arc;
+            const TransportArc& arc;
 
-            TransportArcAndTokens(boost::weak_ptr<TransportArc> arc, TokenList enabledBy, vector<unsigned int > modificationVector)
+            TransportArcAndTokens(const TransportArc& arc, TokenList enabledBy, vector<unsigned int > modificationVector)
             : ArcAndTokens<T>(enabledBy, modificationVector), arc(arc) {
             }
 
-            TransportArcAndTokens(boost::weak_ptr<TransportArc> arc, TokenList enabledBy)
-            : ArcAndTokens<T>(enabledBy, arc.lock()->getWeight()), arc(arc) {
+            TransportArcAndTokens(const TransportArc& arc, TokenList enabledBy)
+            : ArcAndTokens<T>(enabledBy, arc.getWeight()), arc(arc) {
             }
 
             void moveToken(Token& token, T& m) {
-                m.removeToken(arc.lock()->getSource().getIndex(), token.getAge());
-                m.addTokenInPlace(arc.lock()->getDestination(), token);
+                m.removeToken(arc.getSource().getIndex(), token.getAge());
+                m.addTokenInPlace(arc.getDestination(), token);
             }
         };
 
@@ -138,7 +136,7 @@
         class SuccessorGenerator {
             typedef google::sparse_hash_map<const void*, TokenList> ArcHashMap;
             typedef ArcAndTokens<T> ArcAndTokenWithType;
-            typedef typename boost::ptr_vector< ArcAndTokenWithType > ArcAndTokensVector;
+            typedef typename std::vector<ArcAndTokenWithType*> ArcAndTokensVector;
 
         public:
             
@@ -195,7 +193,7 @@
             clearTransitionsArray();
             for (TimedTransition::Vector::const_iterator iter = tapn.getTransitions().begin(); iter != tapn.getTransitions().end(); iter++) {
                 if ((*iter)->getPreset().size() + (*iter)->getTransportArcs().size() == 0) {
-                    allwaysEnabled.push_back(iter->get());
+                    allwaysEnabled.push_back((*iter));
                 }
             }
         }
@@ -215,24 +213,24 @@
             std::vector<const TAPN::TimedTransition* > enabledTransitions;
 
             for (PlaceList::const_iterator iter = marking.getPlaceList().begin(); iter < marking.getPlaceList().end(); iter++) {
-                for (TAPN::TimedInputArc::WeakPtrVector::const_iterator arc_iter = iter->place->getInputArcs().begin();
+                for (TAPN::TimedInputArc::Vector::const_iterator arc_iter = iter->place->getInputArcs().begin();
                         arc_iter != iter->place->getInputArcs().end(); arc_iter++) {
                     processArc(enabledArcs, enabledTransitionArcs, enabledTransitions,
-                            *iter, arc_iter->lock()->getInterval(), arc_iter->lock().get(), arc_iter->lock()->getOutputTransition());
+                            *iter, (*arc_iter)->getInterval(), (*arc_iter), (*arc_iter)->getOutputTransition());
                 }
 
-                for (TAPN::TransportArc::WeakPtrVector::const_iterator arc_iter = iter->place->getTransportArcs().begin();
+                for (TAPN::TransportArc::Vector::const_iterator arc_iter = iter->place->getTransportArcs().begin();
                         arc_iter != iter->place->getTransportArcs().end(); arc_iter++) {
                     processArc(enabledArcs, enabledTransitionArcs, enabledTransitions,
-                            *iter, arc_iter->lock()->getInterval(), arc_iter->lock().get(),
-                            arc_iter->lock()->getTransition(), arc_iter->lock()->getDestination().getInvariant().getBound());
+                            *iter, (*arc_iter)->getInterval(), (*arc_iter),
+                            (*arc_iter)->getTransition(), (*arc_iter)->getDestination().getInvariant().getBound());
                 }
 
-                for (TAPN::InhibitorArc::WeakPtrVector::const_iterator arc_iter = iter->place->getInhibitorArcs().begin();
+                for (TAPN::InhibitorArc::Vector::const_iterator arc_iter = iter->place->getInhibitorArcs().begin();
                         arc_iter != iter->place->getInhibitorArcs().end(); arc_iter++) {
                     TimeInterval t(false, 0, std::numeric_limits<int>().max(), true);
                     processArc(enabledArcs, enabledTransitionArcs, enabledTransitions,
-                            *iter, t, arc_iter->lock().get(), arc_iter->lock()->getOutputTransition(), std::numeric_limits<int>().max(), true);
+                            *iter, t, (*arc_iter), (*arc_iter)->getOutputTransition(), std::numeric_limits<int>().max(), true);
                 }
             }
 
@@ -285,9 +283,9 @@
                 bool inhibited = false;
                 //Check that no inhibitors is enabled;
 
-                for (TAPN::InhibitorArc::WeakPtrVector::const_iterator inhib_iter = (*iter)->getInhibitorArcs().begin(); inhib_iter != (*iter)->getInhibitorArcs().end(); inhib_iter++) {
+                for (TAPN::InhibitorArc::Vector::const_iterator inhib_iter = (*iter)->getInhibitorArcs().begin(); inhib_iter != (*iter)->getInhibitorArcs().end(); inhib_iter++) {
                     // Maybe this could be done more efficiently using ArcHashMap? Dunno exactly how it works
-                    if (init_marking.numberOfTokensInPlace(inhib_iter->lock().get()->getInputPlace().getIndex()) >= inhib_iter->lock().get()->getWeight()) {
+                    if (init_marking.numberOfTokensInPlace((*inhib_iter)->getInputPlace().getIndex()) >= (*inhib_iter)->getWeight()) {
                         inhibited = true;
                         break;
                     }
@@ -308,20 +306,22 @@
 
             // Initialize vectors
             ArcAndTokensVector indicesOfCurrentPermutation;
-            for (TimedInputArc::WeakPtrVector::const_iterator iter = transition.getPreset().begin(); iter != transition.getPreset().end(); iter++) {
-                InputArcAndTokens<T>* arcAndTokens = new InputArcAndTokens<T > (*iter, enabledArcs[iter->lock().get()]);
+            for (TimedInputArc::Vector::const_iterator iter = transition.getPreset().begin(); iter != transition.getPreset().end(); iter++) {
+                InputArcAndTokens<T>* arcAndTokens = new InputArcAndTokens<T > (**iter, enabledArcs[(*iter)]);
                 if (arcAndTokens->isOK) {
                     indicesOfCurrentPermutation.push_back(arcAndTokens);
                 } else {
+                    for(unsigned int i = 0; i < indicesOfCurrentPermutation.size(); ++i) delete indicesOfCurrentPermutation[i];
                     return false;
                 }
             }
             // Transport arcs
-            for (TransportArc::WeakPtrVector::const_iterator iter = transition.getTransportArcs().begin(); iter != transition.getTransportArcs().end(); iter++) {
-                TransportArcAndTokens<T>* arcAndTokens = new TransportArcAndTokens<T > (*iter, enabledArcs[iter->lock().get()]);
+            for (TransportArc::Vector::const_iterator iter = transition.getTransportArcs().begin(); iter != transition.getTransportArcs().end(); iter++) {
+                TransportArcAndTokens<T>* arcAndTokens = new TransportArcAndTokens<T > (**iter, enabledArcs[(*iter)]);
                 if (arcAndTokens->isOK) {
                     indicesOfCurrentPermutation.push_back(arcAndTokens);
                 } else {
+                    for(unsigned int i = 0; i < indicesOfCurrentPermutation.size(); ++i) delete indicesOfCurrentPermutation[i];
                     return false;
                 }
             }
@@ -345,14 +345,15 @@
 
                 //Loop through arc indexes from the back
                 for (int arcAndTokenIndex = indicesOfCurrentPermutation.size() - 1; arcAndTokenIndex >= 0; arcAndTokenIndex--) {
-                    TokenList& enabledTokens = indicesOfCurrentPermutation.at(arcAndTokenIndex).enabledBy;
-                    vector<unsigned int >& modificationVector = indicesOfCurrentPermutation.at(arcAndTokenIndex).modificationVector;
+                    TokenList& enabledTokens = indicesOfCurrentPermutation.at(arcAndTokenIndex)->enabledBy;
+                    vector<unsigned int >& modificationVector = indicesOfCurrentPermutation[arcAndTokenIndex]->modificationVector;
                     if (incrementModificationVector(modificationVector, enabledTokens)) {
                         changedSomething = true;
                         break;
                     }
                 }
             }
+            for(unsigned int i = 0; i < indicesOfCurrentPermutation.size(); ++i) delete indicesOfCurrentPermutation[i];
             return false;
         }
 
@@ -425,17 +426,17 @@
         bool SuccessorGenerator<T>::insertMarking(T& init_marking, const TimedTransition& transition, ArcAndTokensVector& indicesOfCurrentPermutation) const {
             T* m = new T(init_marking);
             for (typename ArcAndTokensVector::iterator iter = indicesOfCurrentPermutation.begin(); iter != indicesOfCurrentPermutation.end(); iter++) {
-                vector<unsigned int>& tokens = iter->modificationVector;
+                vector<unsigned int>& tokens = (*iter)->modificationVector;
 
                 for (vector< unsigned int >::const_iterator tokenIter = tokens.begin(); tokenIter < tokens.end(); tokenIter++) {
-                    Token t((iter->enabledBy)[*tokenIter].getAge(), 1);
-                    iter->moveToken(t, *m);
+                    Token t(((*iter)->enabledBy)[*tokenIter].getAge(), 1);
+                    (*iter)->moveToken(t, *m);
                 }
             }
 
-            for (OutputArc::WeakPtrVector::const_iterator postsetIter = transition.getPostset().begin(); postsetIter != transition.getPostset().end(); postsetIter++) {
-                Token t(0, postsetIter->lock()->getWeight());
-                m->addTokenInPlace(postsetIter->lock()->getOutputPlace(), t);
+            for (OutputArc::Vector::const_iterator postsetIter = transition.getPostset().begin(); postsetIter != transition.getPostset().end(); postsetIter++) {
+                Token t(0, (*postsetIter)->getWeight());
+                m->addTokenInPlace((*postsetIter)->getOutputPlace(), t);
             }
             return verifier.addToPW(m);
         }

=== modified file 'src/DiscreteVerification/TimeDartSuccessorGenerator.cpp'
--- src/DiscreteVerification/TimeDartSuccessorGenerator.cpp	2013-05-08 15:10:14 +0000
+++ src/DiscreteVerification/TimeDartSuccessorGenerator.cpp	2013-08-26 13:51:29 +0000
@@ -11,7 +11,7 @@
 namespace DiscreteVerification {
 
 TimeDartSuccessorGenerator::~TimeDartSuccessorGenerator(){
-
+    delete[] transitionStatistics;
 }
 
 TimeDartSuccessorGenerator::TimeDartSuccessorGenerator(TAPN::TimedArcPetriNet& tapn, Verification<NonStrictMarkingBase>& verifier)  : tapn(tapn), allwaysEnabled(), numberoftransitions(tapn.getTransitions().size()), transitionStatistics(), verifier(verifier){
@@ -20,7 +20,7 @@
 	clearTransitionsArray();
 	for(TimedTransition::Vector::const_iterator iter = tapn.getTransitions().begin(); iter != tapn.getTransitions().end(); iter++){
 		if((*iter)->getPreset().size() + (*iter)->getTransportArcs().size() == 0){
-			allwaysEnabled.push_back(iter->get());
+			allwaysEnabled.push_back((*iter));
 		}
 	}
 }
@@ -30,14 +30,14 @@
 	ArcHashMap enabledArcs(transition.getPresetSize() + transition.getTransportArcs().size());
 
 	// Calculate enabling tokens
-	for(TAPN::TimedInputArc::WeakPtrVector::const_iterator arc_iter = transition.getPreset().begin();
+	for(TAPN::TimedInputArc::Vector::const_iterator arc_iter = transition.getPreset().begin();
 			arc_iter != transition.getPreset().end(); arc_iter++){
-			processArc(enabledArcs,	marking.getTokenList( arc_iter->lock()->getInputPlace().getIndex() ), arc_iter->lock()->getInterval(), arc_iter->lock().get(), transition);
+			processArc(enabledArcs,	marking.getTokenList( (*arc_iter)->getInputPlace().getIndex() ), (*arc_iter)->getInterval(), (*arc_iter), transition);
 	}
 
-	for(TAPN::TransportArc::WeakPtrVector::const_iterator arc_iter = transition.getTransportArcs().begin();
+	for(TAPN::TransportArc::Vector::const_iterator arc_iter = transition.getTransportArcs().begin();
 			arc_iter != transition.getTransportArcs().end(); arc_iter++){
-			processArc(enabledArcs,	marking.getTokenList( arc_iter->lock()->getSource().getIndex() ), arc_iter->lock()->getInterval(), arc_iter->lock().get(), transition, arc_iter->lock()->getDestination().getInvariant().getBound());
+			processArc(enabledArcs,	marking.getTokenList( (*arc_iter)->getSource().getIndex() ), (*arc_iter)->getInterval(), (*arc_iter), transition, (*arc_iter)->getDestination().getInvariant().getBound());
 	}
 
 	return generateMarkings(marking, transition, enabledArcs);
@@ -65,9 +65,9 @@
 		bool inhibited = false;
 		//Check that no inhibitors is enabled;
 
-		for(TAPN::InhibitorArc::WeakPtrVector::const_iterator inhib_iter = transition.getInhibitorArcs().begin(); inhib_iter != transition.getInhibitorArcs().end(); inhib_iter++){
+		for(TAPN::InhibitorArc::Vector::const_iterator inhib_iter = transition.getInhibitorArcs().begin(); inhib_iter != transition.getInhibitorArcs().end(); inhib_iter++){
 			// Maybe this could be done more efficiently using ArcHashMap? Dunno exactly how it works
-			if(init_marking.numberOfTokensInPlace(inhib_iter->lock().get()->getInputPlace().getIndex()) >= inhib_iter->lock().get()->getWeight()){
+			if(init_marking.numberOfTokensInPlace((*inhib_iter)->getInputPlace().getIndex()) >= (*inhib_iter)->getWeight()){
 				inhibited = true;
 				break;
 			}
@@ -85,20 +85,22 @@
 
 	// Initialize vectors
 	ArcAndTokensVector indicesOfCurrentPermutation;
-	for(TimedInputArc::WeakPtrVector::const_iterator iter = transition.getPreset().begin(); iter != transition.getPreset().end(); iter++){
-		InputArcAndTokens<NonStrictMarkingBase>* arcAndTokens = new InputArcAndTokens<NonStrictMarkingBase>(*iter, enabledArcs[iter->lock().get()]);
+	for(TimedInputArc::Vector::const_iterator iter = transition.getPreset().begin(); iter != transition.getPreset().end(); iter++){
+		InputArcAndTokens<NonStrictMarkingBase>* arcAndTokens = new InputArcAndTokens<NonStrictMarkingBase>(**iter, enabledArcs[(*iter)]);
 		if(arcAndTokens->isOK){
 			indicesOfCurrentPermutation.push_back(arcAndTokens);
 		}else{
-			return false;
+                    for(unsigned int i = 0; i < indicesOfCurrentPermutation.size(); ++i) delete indicesOfCurrentPermutation[i];
+                    return false;
 		}
 	}
 	// Transport arcs
-	for(TransportArc::WeakPtrVector::const_iterator iter = transition.getTransportArcs().begin(); iter != transition.getTransportArcs().end(); iter++){
-		TransportArcAndTokens<NonStrictMarkingBase>* arcAndTokens = new TransportArcAndTokens<NonStrictMarkingBase>(*iter, enabledArcs[iter->lock().get()]);
+	for(TransportArc::Vector::const_iterator iter = transition.getTransportArcs().begin(); iter != transition.getTransportArcs().end(); iter++){
+		TransportArcAndTokens<NonStrictMarkingBase>* arcAndTokens = new TransportArcAndTokens<NonStrictMarkingBase>(**iter, enabledArcs[(*iter)]);
 		if(arcAndTokens->isOK){
 			indicesOfCurrentPermutation.push_back(arcAndTokens);
 		}else{
+                    for(unsigned int i = 0; i < indicesOfCurrentPermutation.size(); ++i) delete indicesOfCurrentPermutation[i];
 			return false;
 		}
 	}
@@ -116,14 +118,15 @@
 
 		//Loop through arc indexes from the back
 		for(int arcAndTokenIndex = indicesOfCurrentPermutation.size()-1; arcAndTokenIndex >= 0; arcAndTokenIndex--){
-			TokenList& enabledTokens = indicesOfCurrentPermutation.at(arcAndTokenIndex).enabledBy;
-			vector<unsigned int >& modificationVector = indicesOfCurrentPermutation.at(arcAndTokenIndex).modificationVector;
+			TokenList& enabledTokens = indicesOfCurrentPermutation[arcAndTokenIndex]->enabledBy;
+			vector<unsigned int >& modificationVector = indicesOfCurrentPermutation[arcAndTokenIndex]->modificationVector;
 			if(incrementModificationVector(modificationVector, enabledTokens)){
 				changedSomething = true;
 				break;
 			}
 		}
 	}
+        for(unsigned int i = 0; i < indicesOfCurrentPermutation.size(); ++i) delete indicesOfCurrentPermutation[i];
         return false;
 }       
 
@@ -194,17 +197,17 @@
 bool TimeDartSuccessorGenerator::insertMarking(NonStrictMarkingBase& init_marking, const TimedTransition& transition, ArcAndTokensVector& indicesOfCurrentPermutation) const{
 	NonStrictMarkingBase* m = new NonStrictMarkingBase(init_marking);
 	for(ArcAndTokensVector::iterator iter = indicesOfCurrentPermutation.begin(); iter != indicesOfCurrentPermutation.end(); iter++){
-		vector<unsigned int>& tokens = iter->modificationVector;
+		vector<unsigned int>& tokens = (*iter)->modificationVector;
 
 		for(vector< unsigned int >::const_iterator tokenIter = tokens.begin(); tokenIter < tokens.end(); tokenIter++){
-			Token t((iter->enabledBy)[*tokenIter].getAge(), 1);
-			iter->moveToken(t, *m);
+			Token t(((*iter)->enabledBy)[*tokenIter].getAge(), 1);
+			(*iter)->moveToken(t, *m);
 		}
 	}
 
-	for(OutputArc::WeakPtrVector::const_iterator postsetIter = transition.getPostset().begin(); postsetIter != transition.getPostset().end(); postsetIter++){
-		Token t(0, postsetIter->lock()->getWeight());
-		m->addTokenInPlace(postsetIter->lock()->getOutputPlace(), t);
+	for(OutputArc::Vector::const_iterator postsetIter = transition.getPostset().begin(); postsetIter != transition.getPostset().end(); postsetIter++){
+		Token t(0, (*postsetIter)->getWeight());
+		m->addTokenInPlace((*postsetIter)->getOutputPlace(), t);
 	}
         return this->verifier.addToPW(m);
 	

=== modified file 'src/DiscreteVerification/TimeDartSuccessorGenerator.hpp'
--- src/DiscreteVerification/TimeDartSuccessorGenerator.hpp	2013-04-23 11:57:15 +0000
+++ src/DiscreteVerification/TimeDartSuccessorGenerator.hpp	2013-08-26 13:51:29 +0000
@@ -12,8 +12,6 @@
 #include "DataStructures/NonStrictMarkingBase.hpp"
 #include "google/sparse_hash_map"
 #include <limits>
-#include "boost/tuple/tuple_io.hpp"
-#include "boost/ptr_container/ptr_vector.hpp"
 #include "SuccessorGenerator.hpp"
 
 namespace VerifyTAPN {
@@ -21,11 +19,10 @@
 
 using namespace std;
 using namespace TAPN;
-using namespace boost;
 
 class TimeDartSuccessorGenerator {
 	typedef google::sparse_hash_map<const void*, TokenList> ArcHashMap;
-	typedef boost::ptr_vector< ArcAndTokens<NonStrictMarkingBase> > ArcAndTokensVector;
+	typedef std::vector< ArcAndTokens<NonStrictMarkingBase>*> ArcAndTokensVector;
 
 public:
 	TimeDartSuccessorGenerator(TAPN::TimedArcPetriNet& tapn, Verification<NonStrictMarkingBase>& verifier);

=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp'
--- src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2013-08-13 19:16:37 +0000
+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2013-08-26 13:51:29 +0000
@@ -10,13 +10,13 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-LivenessSearch::LivenessSearch(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
-	: tapn(tapn), initialMarking(initialMarking), query(query), options(options), successorGenerator( *tapn.get(), *this ){
+LivenessSearch::LivenessSearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
+	: tapn(tapn), initialMarking(initialMarking), query(query), options(options), successorGenerator( tapn, *this ){
 
 }
     
-LivenessSearch::LivenessSearch(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
-	: pwList(new PWList(waiting_list, true)), tapn(tapn), initialMarking(initialMarking), query(query), options(options), successorGenerator( *tapn.get(), *this ){
+LivenessSearch::LivenessSearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
+	: pwList(new PWList(waiting_list, true)), tapn(tapn), initialMarking(initialMarking), query(query), options(options), successorGenerator( tapn, *this ){
 
 }
 
@@ -92,9 +92,9 @@
 	if(places.size() == 0) return true;	//Delay always possible in empty markings
 
 	PlaceList::const_iterator markedPlace_iter = places.begin();
-	for(TAPN::TimedPlace::Vector::const_iterator place_iter = tapn->getPlaces().begin(); place_iter != tapn->getPlaces().end(); place_iter++){
-		int inv = place_iter->get()->getInvariant().getBound();
-		if(*(place_iter->get()) == *(markedPlace_iter->place)){
+	for(TAPN::TimedPlace::Vector::const_iterator place_iter = tapn.getPlaces().begin(); place_iter != tapn.getPlaces().end(); place_iter++){
+		int inv = (*place_iter)->getInvariant().getBound();
+		if(**place_iter == *(markedPlace_iter->place)){
 			if(markedPlace_iter->maxTokenAge() > inv-1){
 				return false;
 			}
@@ -120,10 +120,10 @@
 		return false;
 	}
 
-	QueryVisitor<NonStrictMarking> checker(*marking, *tapn.get());
-	boost::any context;
+	QueryVisitor<NonStrictMarking> checker(*marking, tapn);
+	AST::BoolResult context;
 	query->accept(checker, context);
-	if(!boost::any_cast<bool>(context))	return false;
+	if(!context.value)	return false;
 	if(!pwList->add(marking)){
 		//Test if collision is in trace
             if(marking->meta->inTrace){
@@ -153,7 +153,7 @@
 	NonStrictMarking* m = trace.top();
 	generateTraceStack(m, &printStack, &trace);
 	if(options.getXmlTrace()){
-		printXMLTrace(m, printStack, query, *this->tapn.get());
+		printXMLTrace(m, printStack, query, tapn);
 	} else {
 		printHumanTrace(m, printStack, query->getQuantifier());
 	}

=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp'
--- src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp	2013-05-08 13:25:46 +0000
+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,6 @@
 #define LIVENESSSEARCH_HPP_
 
 #include "../DataStructures/PWList.hpp"
-#include "boost/smart_ptr.hpp"
 #include "../../Core/TAPN/TAPN.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../../Core/VerificationOptions.hpp"
@@ -21,7 +20,6 @@
 #include "../../Core/TAPN/OutputArc.hpp"
 #include "../SuccessorGenerator.hpp"
 #include "../QueryVisitor.hpp"
-#include "boost/any.hpp"
 #include "../DataStructures/NonStrictMarking.hpp"
 #include <stack>
 #include "Verification.hpp"
@@ -32,8 +30,8 @@
 
 class LivenessSearch : public Verification<NonStrictMarking>{
 public:
-	LivenessSearch(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options);
-    LivenessSearch(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
+	LivenessSearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options);
+    LivenessSearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
 	virtual ~LivenessSearch();
 	bool verify();
 	NonStrictMarking* GetLastMarking() { return lastMarking; }
@@ -52,7 +50,7 @@
 protected:
 	int validChildren;
 	PWListBase* pwList;
-	boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn;
+	TAPN::TimedArcPetriNet& tapn;
 	NonStrictMarking& initialMarking;
 	AST::Query* query;
 	VerificationOptions options;
@@ -67,10 +65,10 @@
 };
 class LivenessSearchPTrie : public LivenessSearch{
 public:
-    LivenessSearchPTrie(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<EncodingPointer<MetaData> >* waiting_list) 
+    LivenessSearchPTrie(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<EncodingPointer<MetaData> >* waiting_list) 
     : LivenessSearch(tapn,initialMarking, query, options)
     {
-        pwList = new PWListHybrid(tapn, waiting_list, options.getKBound(), tapn->getNumberOfPlaces(), tapn->getMaxConstant(), true, options.getTrace() == VerificationOptions::SOME_TRACE);
+        pwList = new PWListHybrid(tapn, waiting_list, options.getKBound(), tapn.getNumberOfPlaces(), tapn.getMaxConstant(), true, options.getTrace() == VerificationOptions::SOME_TRACE);
     };
     virtual void deleteMarking(NonStrictMarking* m) {
         delete m;

=== modified file 'src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp'
--- src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2013-08-13 19:16:37 +0000
+++ src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2013-08-26 13:51:29 +0000
@@ -10,13 +10,13 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-ReachabilitySearch::ReachabilitySearch(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
-	: tapn(tapn), initialMarking(initialMarking), query(query), options(options), successorGenerator( *tapn.get(), *this ){
+ReachabilitySearch::ReachabilitySearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
+	: tapn(tapn), initialMarking(initialMarking), query(query), options(options), successorGenerator( tapn, *this ){
 
 }
     
-ReachabilitySearch::ReachabilitySearch(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
-	: pwList(new PWList(waiting_list, false)), tapn(tapn), initialMarking(initialMarking), query(query), options(options), successorGenerator( *tapn.get(), *this ){
+ReachabilitySearch::ReachabilitySearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
+	: pwList(new PWList(waiting_list, false)), tapn(tapn), initialMarking(initialMarking), query(query), options(options), successorGenerator( tapn, *this ){
 
 }
 
@@ -61,9 +61,9 @@
 	if(places.size() == 0) return true;	//Delay always possible in empty markings
 
 	PlaceList::const_iterator markedPlace_iter = places.begin();
-	for(TAPN::TimedPlace::Vector::const_iterator place_iter = tapn->getPlaces().begin(); place_iter != tapn->getPlaces().end(); place_iter++){
-		int inv = place_iter->get()->getInvariant().getBound();
-		if(*(place_iter->get()) == *(markedPlace_iter->place)){
+	for(TAPN::TimedPlace::Vector::const_iterator place_iter = tapn.getPlaces().begin(); place_iter != tapn.getPlaces().end(); place_iter++){
+		int inv = (*place_iter)->getInvariant().getBound();
+		if(**place_iter == *(markedPlace_iter->place)){
 			if(markedPlace_iter->maxTokenAge() > inv-1){
 				return false;
 			}
@@ -91,10 +91,11 @@
 	}
 
 	if(pwList->add(marking)){
-		QueryVisitor<NonStrictMarking> checker(*marking, *tapn.get());
-		boost::any context;
+		QueryVisitor<NonStrictMarking> checker(*marking, tapn);
+		BoolResult context;
+
 		query->accept(checker, context);
-		if(boost::any_cast<bool>(context)) {
+		if(context.value) {
 			lastMarking = marking;
 			return true;
 		} else {
@@ -118,7 +119,7 @@
 	stack < NonStrictMarking*> printStack;
 	generateTraceStack(lastMarking, &printStack);
 	if(options.getXmlTrace()){
-		printXMLTrace(lastMarking, printStack, query, *this->tapn.get());
+		printXMLTrace(lastMarking, printStack, query, tapn);
 	} else {
 		printHumanTrace(lastMarking, printStack, query->getQuantifier());
 	}
@@ -138,7 +139,7 @@
             printStack.push(m);
             next = next->parent;
         };
-        printXMLTrace(lastMarking, printStack, query, *this->tapn.get());
+        printXMLTrace(lastMarking, printStack, query, tapn);
 }
 
 ReachabilitySearch::~ReachabilitySearch() {

=== modified file 'src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp'
--- src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp	2013-05-08 13:25:46 +0000
+++ src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp	2013-08-26 13:51:29 +0000
@@ -9,7 +9,6 @@
 #define REACHABILITYSEARCH_HPP_
 
 #include "../DataStructures/PWList.hpp"
-#include "boost/smart_ptr.hpp"
 #include "../../Core/TAPN/TAPN.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../../Core/VerificationOptions.hpp"
@@ -21,7 +20,6 @@
 #include "../../Core/TAPN/OutputArc.hpp"
 #include "../SuccessorGenerator.hpp"
 #include "../QueryVisitor.hpp"
-#include "boost/any.hpp"
 #include "../DataStructures/NonStrictMarking.hpp"
 #include <stack>
 #include "Verification.hpp"
@@ -32,8 +30,8 @@
 
 class ReachabilitySearch : public Verification<NonStrictMarking>{
 public:
-        ReachabilitySearch(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options);
-	ReachabilitySearch(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
+        ReachabilitySearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options);
+	ReachabilitySearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
 	virtual ~ReachabilitySearch();
 	bool verify();
 	NonStrictMarking* getLastMarking() { return lastMarking; }
@@ -52,7 +50,7 @@
 protected:
 	int validChildren;
 	PWListBase* pwList;
-	boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn;
+	TAPN::TimedArcPetriNet& tapn;
 	NonStrictMarking& initialMarking;
 	AST::Query* query;
 	VerificationOptions options;
@@ -67,10 +65,10 @@
 
 class ReachabilitySearchPTrie : public ReachabilitySearch{
 public:
-    ReachabilitySearchPTrie(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<EncodingPointer<MetaData> >* waiting_list) 
+    ReachabilitySearchPTrie(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<EncodingPointer<MetaData> >* waiting_list) 
     : ReachabilitySearch(tapn,initialMarking, query, options)
     {
-        pwList = new PWListHybrid(tapn, waiting_list, options.getKBound(), tapn->getNumberOfPlaces(), tapn->getMaxConstant(), false, options.getTrace() == VerificationOptions::SOME_TRACE);
+        pwList = new PWListHybrid(tapn, waiting_list, options.getKBound(), tapn.getNumberOfPlaces(), tapn.getMaxConstant(), false, options.getTrace() == VerificationOptions::SOME_TRACE);
     };
     
     virtual void deleteMarking(NonStrictMarking* m) {

=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartLiveness.cpp'
--- src/DiscreteVerification/VerificationTypes/TimeDartLiveness.cpp	2013-08-12 15:06:44 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartLiveness.cpp	2013-08-26 13:51:29 +0000
@@ -56,8 +56,8 @@
                 waitingDart->dart->setPassed(waitingDart->w);
                 this->tmpdart = waitingDart;
                 // Iterate over transitions
-                for (TimedTransition::Vector::const_iterator transition_iter = tapn->getTransitions().begin();
-                        transition_iter != tapn->getTransitions().end(); transition_iter++) {
+                for (TimedTransition::Vector::const_iterator transition_iter = tapn.getTransitions().begin();
+                        transition_iter != tapn.getTransitions().end(); transition_iter++) {
                     TimedTransition& transition = **transition_iter;
 
                     // Calculate enabled set
@@ -135,14 +135,15 @@
                 delete marking;
                 return false;
             }
-            
-            int youngest = marking->makeBase(tapn.get());
-
-            QueryVisitor<NonStrictMarkingBase> checker(*marking, *tapn.get());
-            boost::any context;
+
+            int youngest = marking->makeBase();
+
+            QueryVisitor<NonStrictMarkingBase> checker(*marking, tapn);
+            AST::BoolResult context;
+
             query->accept(checker, context);
-            if (boost::any_cast<bool>(context)) {
-                std::pair < LivenessDart*, bool> result = pwList->add(tapn.get(), marking, youngest, parent, upper, start);
+            if (context.value) {
+                std::pair < LivenessDart*, bool> result = pwList->add(marking, youngest, parent, upper, start);
 
 
                 if (parent != NULL && parent->dart->getBase()->equals(*result.first->getBase()) && youngest <= upper) {
@@ -181,6 +182,8 @@
         }
 
         TimeDartLiveness::~TimeDartLiveness() {
+            delete tmpdart;
+            delete pwList;
         }
 
     } /* namespace DiscreteVerification */

=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartLiveness.hpp'
--- src/DiscreteVerification/VerificationTypes/TimeDartLiveness.hpp	2013-05-08 13:25:46 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartLiveness.hpp	2013-08-26 13:51:29 +0000
@@ -10,13 +10,10 @@
 
 #include "../DataStructures/TimeDart.hpp"
 #include "../DataStructures/TimeDartLivenessPWList.hpp"
-#include "boost/smart_ptr.hpp"
-#include "boost/numeric/interval.hpp"
 #include "../../Core/TAPN/TAPN.hpp"
 #include "../../Core/QueryParser/AST.hpp"
 #include "../../Core/VerificationOptions.hpp"
 #include "../QueryVisitor.hpp"
-#include "boost/any.hpp"
 #include "../DataStructures/NonStrictMarkingBase.hpp"
 #include <stack>
 #include "TimeDartVerification.hpp"
@@ -29,11 +26,11 @@
         class TimeDartLiveness : public TimeDartVerification {
         public:
 
-            TimeDartLiveness(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarkingBase& initialMarking, AST::Query* query, VerificationOptions options)
+            TimeDartLiveness(TAPN::TimedArcPetriNet& tapn, NonStrictMarkingBase& initialMarking, AST::Query* query, VerificationOptions options)
             : TimeDartVerification(tapn, options, query, initialMarking) {
             };
 
-            TimeDartLiveness(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarkingBase& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<WaitingDart>* waiting_list)
+            TimeDartLiveness(TAPN::TimedArcPetriNet& tapn, NonStrictMarkingBase& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<WaitingDart>* waiting_list)
             : TimeDartVerification(tapn, options, query, initialMarking) {
                 pwList = new TimeDartLivenessPWHashMap( options, waiting_list);
             };
@@ -68,9 +65,9 @@
         class TimeDartLivenessPData : public TimeDartLiveness {
         public:
 
-            TimeDartLivenessPData(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, NonStrictMarkingBase& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<EncodingPointer<WaitingDart> >* waiting_list)
+            TimeDartLivenessPData(TAPN::TimedArcPetriNet& tapn, NonStrictMarkingBase& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<EncodingPointer<WaitingDart> >* waiting_list)
             : TimeDartLiveness(tapn, initialMarking, query, options) {
-                pwList = new TimeDartLivenessPWPData(options, waiting_list, tapn, tapn->getNumberOfPlaces(), tapn->getMaxConstant());
+                pwList = new TimeDartLivenessPWPData(options, waiting_list, tapn, tapn.getNumberOfPlaces(), tapn.getMaxConstant());
             };
 
         protected:

=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.cpp'
--- src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.cpp	2013-07-15 19:04:34 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.cpp	2013-08-26 13:51:29 +0000
@@ -25,13 +25,13 @@
 
 		int passed = dart.getPassed();
 		dart.setPassed(dart.getWaiting());
-		tapn->getTransitions();
+		tapn.getTransitions();
                 this->tmpdart = NULL;
                 if(options.getTrace() == VerificationOptions::SOME_TRACE){
                     this->tmpdart = ((ReachabilityTraceableDart*)&dart)->trace;
                 }
-		for(TimedTransition::Vector::const_iterator transition_iter = tapn->getTransitions().begin();
-				transition_iter != tapn->getTransitions().end(); transition_iter++){
+		for(TimedTransition::Vector::const_iterator transition_iter = tapn.getTransitions().begin();
+				transition_iter != tapn.getTransitions().end(); transition_iter++){
 			TimedTransition& transition = **transition_iter;
 			pair<int,int> calculatedStart = calculateStart(transition, dart.getBase());
 			if(calculatedStart.first == -1){	// Transition cannot be enabled in marking
@@ -85,21 +85,21 @@
 		return false;
 	}
         
-        int youngest = marking->makeBase(tapn.get());
+        int youngest = marking->makeBase();
         
-	if(pwList->add(tapn.get(), marking, youngest, parent, upper, start)){
+	if(pwList->add( marking, youngest, parent, upper, start)){
 
 
                 if(maxDelay != std::numeric_limits<int>::max())
                     maxDelay += youngest;
-                if(maxDelay > tapn->getMaxConstant()){
-                    maxDelay = tapn->getMaxConstant() + 1;
+                if(maxDelay > tapn.getMaxConstant()){
+                    maxDelay = tapn.getMaxConstant() + 1;
                 }
                 
-		QueryVisitor<NonStrictMarkingBase> checker(*marking, *tapn.get(), maxDelay);
-		boost::any context;
+		QueryVisitor<NonStrictMarkingBase> checker(*marking, tapn, maxDelay);
+                AST::BoolResult context;
 		query->accept(checker, context);