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

[Peter Gjøl Jensen]

The changes are all renaming of methods, classes and variables, such that the code is consistent with respect to camelcase, getters and setters.

There are two other changes;
TokenList emptyTokenList;
in nonstrictmarking base has been made static.

Pairing has also been removed from the TAPN model as it was unused.

Furthermore, I propose that printHumanTrace is removed as it is unused and with high probability bugged.

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

Also, the following methods have been moved and made inline in NonStrictMarkingBase:

incrementAge()
incrementAge(int age)
decrementAge()

[Jiri Srba (srba)]

Does not compile any more. A prefix of the long error list:

In file included from ./DiscreteVerification/DataStructures/WaitingList.hpp:12,
                 from ./DiscreteVerification/DataStructures/PWList.hpp:11,
                 from ./DiscreteVerification/DataStructures/PWList.cpp:8:
./DiscreteVerification/DataStructures/TimeDart.hpp:12:19: error: PTrie.h: No such file or directory
In file included from ./DiscreteVerification/DataStructures/WaitingList.hpp:12,
                 from ./DiscreteVerification/DataStructures/PWList.hpp:11,
                 from ./DiscreteVerification/DataStructures/PWList.cpp:8:
./DiscreteVerification/DataStructures/TimeDart.hpp:12:19: error: PTrie.h: No such file or directory
In file included from ./DiscreteVerification/DataStructures/PWList.cpp:8:
./DiscreteVerification/DataStructures/PWList.hpp:71: error: ISO C++ forbids declaration of ‘PTrie’ with no type
./DiscreteVerification/DataStructures/PWList.hpp:71: error: expected ‘;’ before ‘<’ token
./DiscreteVerification/DataStructures/PWList.hpp: In constructor ‘VerifyTAPN::DiscreteVerification::PWListHybrid::PWListHybrid(boost::shared_ptr<VerifyTAPN::TAPN::TimedArcPetriNet>&, VerifyTAPN::DiscreteVerification::WaitingList<VerifyTAPN::DiscreteVerification::EncodingPointer<VerifyTAPN::DiscreteVerification::MetaData> >*, int, int, int, bool, bool)’:
./DiscreteVerification/DataStructures/PWList.hpp:80: error: ‘passed’ was not declared in this scope
./DiscreteVerification/DataStructures/PWList.hpp:80: error: expected type-specifier before ‘PTrie’
./DiscreteVerification/DataStructures/PWList.hpp:80: error: expected `;' before ‘PTrie’
./DiscreteVerification/DataStructures/PWList.hpp: In member function ‘VerifyTAPN::DiscreteVerification::NonStrictMarking* VerifyTAPN::DiscreteVerification::PWListHybrid::decode(VerifyTAPN::DiscreteVerification::EncodingPointer<VerifyTAPN::DiscreteVerification::MetaData>*)’:
./DiscreteVerification/DataStructures/PWList.hpp:88: error: ‘class VerifyTAPN::DiscreteVerification::PWListHybrid’ has no member named ‘passed’
./DiscreteVerification/DataStructures/PWList.hpp: In member function ‘virtual long long int VerifyTAPN::DiscreteVerification::PWListHybrid::size() const’:
./DiscreteVerification/DataStructures/PWList.hpp:98: error: ‘passed’ was not declared in this scope
./DiscreteVerification/DataStructures/PWList.hpp: In member function ‘void VerifyTAPN::DiscreteVerification::PWListHybrid::printMemStats()’:
./DiscreteVerification/DataStructures/PWList.hpp:102: error: ‘passed’ was
....
...
..

review: Needs Fixing

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

314. By Peter Gjøl Jensen on 2013-05-08

added missing file

315. By Peter Gjøl Jensen on 2013-05-08

corrected grammar

316. By Peter Gjøl Jensen on 2013-05-08

fixed errors in grammar

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

Sorry, A file was missing after I renamed it. It should compile now

[Jiri Srba (srba)]

Well, still more errors:

In file included from ./DiscreteVerification/DataStructures/TimeDart.hpp:12,
                 from ./DiscreteVerification/DataStructures/WaitingList.hpp:12,
                 from ./DiscreteVerification/DataStructures/PWList.hpp:11,
                 from ./DiscreteVerification/DataStructures/PWList.cpp:8:
./DiscreteVerification/DataStructures/PTrie.h: In constructor ‘VerifyTAPN::DiscreteVerification::PTrie<T>::PTrie(boost::shared_ptr<VerifyTAPN::TAPN::TimedArcPetriNet>&, int, int, int)’:
./DiscreteVerification/DataStructures/PTrie.h:74: error: wrong number of template arguments (1, should be 2)
/Users/srba/dev/boost_1_46_1/boost/detail/container_fwd.hpp:85: error: provided for ‘template<class T, class Allocator> struct std::list’
In file included from ./DiscreteVerification/DataStructures/TimeDart.hpp:12,
                 from ./DiscreteVerification/DataStructures/WaitingList.hpp:12,
                 from ./DiscreteVerification/DataStructures/PWList.hpp:11,
                 from ./DiscreteVerification/DataStructures/PWList.cpp:8:
./DiscreteVerification/DataStructures/PTrie.h: In constructor ‘VerifyTAPN::DiscreteVerification::PTrie<T>::PTrie(boost::shared_ptr<VerifyTAPN::TAPN::TimedArcPetriNet>&, int, int, int)’:
./DiscreteVerification/DataStructures/PTrie.h:74: error: wrong number of template arguments (1, should be 2)
/Users/srba/dev/boost_1_46_1/boost/detail/container_fwd.hpp:85: error: provided for ‘template<class T, class Allocator> struct std::list’
In file included from ./DiscreteVerification/DataStructures/TimeDart.hpp:12,
                 from ./DiscreteVerification/DataStructures/WaitingList.hpp:12,
                 from ./DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp:11,
                 from ./DiscreteVerification/DataStructures/TimeDartLivenessPWList.cpp:8:
./DiscreteVerification/DataStructures/PTrie.h: In constructor ‘VerifyTAPN::DiscreteVerification::PTrie<T>::PTrie(boost::shared_ptr<VerifyTAPN::TAPN::TimedArcPetriNet>&, int, int, int)’:
./DiscreteVerification/DataStructures/PTrie.h:74: error: wrong number of template arguments (1, should be 2)
/Users/srba/dev/boost_1_46_1/boost/detail/container_fwd.hpp:85: error: provided for ‘template<class T, class Allocator> struct std::list’
In file included from ./DiscreteVerification/DataStructures/TimeDart.hpp:12,
                 from ./DiscreteVerification/DataStructures/WaitingList.hpp:12,
                 from ./DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp:11,
                 from ./DiscreteVerification/DataStructures/TimeDartLivenessPWList.cpp:8:
./DiscreteVerification/DataStructures/PTrie.h: In constructor ‘VerifyTAPN::DiscreteVerification::PTrie<T>::PTrie(boost::shared_ptr<VerifyTAPN::TAPN::TimedArcPetriNet>&, int, int, int)’:
./DiscreteVerification/DataStructures/PTrie.h:74: error: wrong number of template arguments (1, should be 2)
/Users/srba/dev/boost_1_46_1/boost/detail/container_fwd.hpp:85: error: provided for ‘template<class T, class Allocator> struct std::list’
In file included from ./DiscreteVerification/DataStructures/TimeDart.hpp:12,
                 from ./DiscreteVerification/DataStructures/WaitingList.hpp:1...

review: Needs Fixing

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

317. By Peter Gjøl Jensen on 2013-05-10

fixed need for --fpermssive on linux

318. By Peter Gjøl Jensen on 2013-05-10

made allocator for PTrie explicit

319. By Peter Gjøl Jensen on 2013-05-13

fixed warnings for g++ 4.7

320. By Peter Gjøl Jensen on 2013-05-14

corrected calculation of splitsize

321. By Peter Gjøl Jensen on 2013-05-14

diverged merge

322. By Jiri Srba on 2013-05-14

change version number to 2.0.1

323. By Peter Gjøl Jensen on 2013-05-15

fixed warning

Unmerged revisions

=== modified file 'lib/rapidxml-1.13/rapidxml_print.hpp'
--- lib/rapidxml-1.13/rapidxml_print.hpp	2012-03-02 10:59:16 +0000
+++ lib/rapidxml-1.13/rapidxml_print.hpp	2013-05-15 15:27:27 +0000
@@ -10,89 +10,102 @@
 
 // Only include streams if not disabled
 #ifndef RAPIDXML_NO_STREAMS
-    #include <ostream>
-    #include <iterator>
+#include <ostream>
+#include <iterator>
 #endif
 
-namespace rapidxml
-{
+namespace rapidxml {
 
     ///////////////////////////////////////////////////////////////////////
     // Printing flags
 
-    const int print_no_indenting = 0x1;   //!< Printer flag instructing the printer to suppress indenting of XML. See print() function.
+    const int print_no_indenting = 0x1; //!< Printer flag instructing the printer to suppress indenting of XML. See print() function.
 
     ///////////////////////////////////////////////////////////////////////
     // Internal
 
     //! \cond internal
-    namespace internal
-    {
-        
+    namespace internal {
+
         ///////////////////////////////////////////////////////////////////////////
         // Internal character operations
-    
+
         // Copy characters from given range to given output iterator
+
         template<class OutIt, class Ch>
-        inline OutIt copy_chars(const Ch *begin, const Ch *end, OutIt out)
-        {
+        inline OutIt copy_chars(const Ch *begin, const Ch *end, OutIt out) {
             while (begin != end)
                 *out++ = *begin++;
             return out;
         }
-        
+
         // Copy characters from given range to given output iterator and expand
         // characters into references (&lt; &gt; &apos; &quot; &amp;)
+
         template<class OutIt, class Ch>
-        inline OutIt copy_and_expand_chars(const Ch *begin, const Ch *end, Ch noexpand, OutIt out)
-        {
-            while (begin != end)
-            {
-                if (*begin == noexpand)
-                {
-                    *out++ = *begin;    // No expansion, copy character
-                }
-                else
-                {
-                    switch (*begin)
-                    {
-                    case Ch('<'):
-                        *out++ = Ch('&'); *out++ = Ch('l'); *out++ = Ch('t'); *out++ = Ch(';');
-                        break;
-                    case Ch('>'): 
-                        *out++ = Ch('&'); *out++ = Ch('g'); *out++ = Ch('t'); *out++ = Ch(';');
-                        break;
-                    case Ch('\''): 
-                        *out++ = Ch('&'); *out++ = Ch('a'); *out++ = Ch('p'); *out++ = Ch('o'); *out++ = Ch('s'); *out++ = Ch(';');
-                        break;
-                    case Ch('"'): 
-                        *out++ = Ch('&'); *out++ = Ch('q'); *out++ = Ch('u'); *out++ = Ch('o'); *out++ = Ch('t'); *out++ = Ch(';');
-                        break;
-                    case Ch('&'): 
-                        *out++ = Ch('&'); *out++ = Ch('a'); *out++ = Ch('m'); *out++ = Ch('p'); *out++ = Ch(';'); 
-                        break;
-                    default:
-                        *out++ = *begin;    // No expansion, copy character
+        inline OutIt copy_and_expand_chars(const Ch *begin, const Ch *end, Ch noexpand, OutIt out) {
+            while (begin != end) {
+                if (*begin == noexpand) {
+                    *out++ = *begin; // No expansion, copy character
+                } else {
+                    switch (*begin) {
+                        case Ch('<'):
+                            *out++ = Ch('&');
+                            *out++ = Ch('l');
+                            *out++ = Ch('t');
+                            *out++ = Ch(';');
+                            break;
+                        case Ch('>'):
+                            *out++ = Ch('&');
+                            *out++ = Ch('g');
+                            *out++ = Ch('t');
+                            *out++ = Ch(';');
+                            break;
+                        case Ch('\''):
+                            *out++ = Ch('&');
+                            *out++ = Ch('a');
+                            *out++ = Ch('p');
+                            *out++ = Ch('o');
+                            *out++ = Ch('s');
+                            *out++ = Ch(';');
+                            break;
+                        case Ch('"'):
+                            *out++ = Ch('&');
+                            *out++ = Ch('q');
+                            *out++ = Ch('u');
+                            *out++ = Ch('o');
+                            *out++ = Ch('t');
+                            *out++ = Ch(';');
+                            break;
+                        case Ch('&'):
+                            *out++ = Ch('&');
+                            *out++ = Ch('a');
+                            *out++ = Ch('m');
+                            *out++ = Ch('p');
+                            *out++ = Ch(';');
+                            break;
+                        default:
+                            *out++ = *begin; // No expansion, copy character
                     }
                 }
-                ++begin;    // Step to next character
+                ++begin; // Step to next character
             }
             return out;
         }
 
         // Fill given output iterator with repetitions of the same character
+
         template<class OutIt, class Ch>
-        inline OutIt fill_chars(OutIt out, int n, Ch ch)
-        {
+        inline OutIt fill_chars(OutIt out, int n, Ch ch) {
             for (int i = 0; i < n; ++i)
                 *out++ = ch;
             return out;
         }
 
         // Find character
+
         template<class Ch, Ch ch>
-        inline bool find_char(const Ch *begin, const Ch *end)
-        {
+        inline bool find_char(const Ch *begin, const Ch *end) {
             while (begin != end)
                 if (*begin++ == ch)
                     return true;
@@ -101,99 +114,36 @@
 
         ///////////////////////////////////////////////////////////////////////////
         // Internal printing operations
-    
+
         // Print node
         template<class OutIt, class Ch>
-        inline OutIt print_node(OutIt out, const xml_node<Ch> *node, int flags, int indent)
-        {
-            // Print proper node type
-            switch (node->type())
-            {
-
-            // Document
-            case node_document:
-                out = print_children(out, node, flags, indent);
-                break;
-
-            // Element
-            case node_element:
-                out = print_element_node(out, node, flags, indent);
-                break;
-            
-            // Data
-            case node_data:
-                out = print_data_node(out, node, flags, indent);
-                break;
-            
-            // CDATA
-            case node_cdata:
-                out = print_cdata_node(out, node, flags, indent);
-                break;
-
-            // Declaration
-            case node_declaration:
-                out = print_declaration_node(out, node, flags, indent);
-                break;
-
-            // Comment
-            case node_comment:
-                out = print_comment_node(out, node, flags, indent);
-                break;
-            
-            // Doctype
-            case node_doctype:
-                out = print_doctype_node(out, node, flags, indent);
-                break;
-
-            // Pi
-            case node_pi:
-                out = print_pi_node(out, node, flags, indent);
-                break;
-
-                // Unknown
-            default:
-                assert(0);
-                break;
-            }
-            
-            // If indenting not disabled, add line break after node
-            if (!(flags & print_no_indenting))
-                *out = Ch('\n'), ++out;
-
-            // Return modified iterator
-            return out;
-        }
-        
+        inline OutIt print_node(OutIt out, const xml_node<Ch> *node, int flags, int indent);
+
         // Print children of the node                               
+
         template<class OutIt, class Ch>
-        inline OutIt print_children(OutIt out, const xml_node<Ch> *node, int flags, int indent)
-        {
+        inline OutIt print_children(OutIt out, const xml_node<Ch> *node, int flags, int indent) {
             for (xml_node<Ch> *child = node->first_node(); child; child = child->next_sibling())
                 out = print_node(out, child, flags, indent);
             return out;
         }
 
         // Print attributes of the node
+
         template<class OutIt, class Ch>
-        inline OutIt print_attributes(OutIt out, const xml_node<Ch> *node, int flags)
-        {
-            for (xml_attribute<Ch> *attribute = node->first_attribute(); attribute; attribute = attribute->next_attribute())
-            {
-                if (attribute->name() && attribute->value())
-                {
+        inline OutIt print_attributes(OutIt out, const xml_node<Ch> *node, int flags) {
+            for (xml_attribute<Ch> *attribute = node->first_attribute(); attribute; attribute = attribute->next_attribute()) {
+                if (attribute->name() && attribute->value()) {
                     // Print attribute name
                     *out = Ch(' '), ++out;
                     out = copy_chars(attribute->name(), attribute->name() + attribute->name_size(), out);
                     *out = Ch('='), ++out;
                     // Print attribute value using appropriate quote type
-                    if (find_char<Ch, Ch('"')>(attribute->value(), attribute->value() + attribute->value_size()))
-                    {
+                    if (find_char < Ch, Ch('"')>(attribute->value(), attribute->value() + attribute->value_size())) {
                         *out = Ch('\''), ++out;
                         out = copy_and_expand_chars(attribute->value(), attribute->value() + attribute->value_size(), Ch('"'), out);
                         *out = Ch('\''), ++out;
-                    }
-                    else
-                    {
+                    } else {
                         *out = Ch('"'), ++out;
                         out = copy_and_expand_chars(attribute->value(), attribute->value() + attribute->value_size(), Ch('\''), out);
                         *out = Ch('"'), ++out;
@@ -204,9 +154,9 @@
         }
 
         // Print data node
+
         template<class OutIt, class Ch>
-        inline OutIt print_data_node(OutIt out, const xml_node<Ch> *node, int flags, int indent)
-        {
+        inline OutIt print_data_node(OutIt out, const xml_node<Ch> *node, int flags, int indent) {
             assert(node->type() == node_data);
             if (!(flags & print_no_indenting))
                 out = fill_chars(out, indent, Ch('\t'));
@@ -215,32 +165,44 @@
         }
 
         // Print data node
+
         template<class OutIt, class Ch>
-        inline OutIt print_cdata_node(OutIt out, const xml_node<Ch> *node, int flags, int indent)
-        {
+        inline OutIt print_cdata_node(OutIt out, const xml_node<Ch> *node, int flags, int indent) {
             assert(node->type() == node_cdata);
             if (!(flags & print_no_indenting))
                 out = fill_chars(out, indent, Ch('\t'));
-            *out = Ch('<'); ++out;
-            *out = Ch('!'); ++out;
-            *out = Ch('['); ++out;
-            *out = Ch('C'); ++out;
-            *out = Ch('D'); ++out;
-            *out = Ch('A'); ++out;
-            *out = Ch('T'); ++out;
-            *out = Ch('A'); ++out;
-            *out = Ch('['); ++out;
+            *out = Ch('<');
+            ++out;
+            *out = Ch('!');
+            ++out;
+            *out = Ch('[');
+            ++out;
+            *out = Ch('C');
+            ++out;
+            *out = Ch('D');
+            ++out;
+            *out = Ch('A');
+            ++out;
+            *out = Ch('T');
+            ++out;
+            *out = Ch('A');
+            ++out;
+            *out = Ch('[');
+            ++out;
             out = copy_chars(node->value(), node->value() + node->value_size(), out);
-            *out = Ch(']'); ++out;
-            *out = Ch(']'); ++out;
-            *out = Ch('>'); ++out;
+            *out = Ch(']');
+            ++out;
+            *out = Ch(']');
+            ++out;
+            *out = Ch('>');
+            ++out;
             return out;
         }
 
         // Print element node
+
         template<class OutIt, class Ch>
-        inline OutIt print_element_node(OutIt out, const xml_node<Ch> *node, int flags, int indent)
-        {
+        inline OutIt print_element_node(OutIt out, const xml_node<Ch> *node, int flags, int indent) {
             assert(node->type() == node_element);
 
             // Print element name and attributes, if any
@@ -249,33 +211,25 @@
             *out = Ch('<'), ++out;
             out = copy_chars(node->name(), node->name() + node->name_size(), out);
             out = print_attributes(out, node, flags);
-            
+
             // If node is childless
-            if (node->value_size() == 0 && !node->first_node())
-            {
+            if (node->value_size() == 0 && !node->first_node()) {
                 // Print childless node tag ending
                 *out = Ch('/'), ++out;
                 *out = Ch('>'), ++out;
-            }
-            else
-            {
+            } else {
                 // Print normal node tag ending
                 *out = Ch('>'), ++out;
 
                 // Test if node contains a single data node only (and no other nodes)
                 xml_node<Ch> *child = node->first_node();
-                if (!child)
-                {
+                if (!child) {
                     // If node has no children, only print its value without indenting
                     out = copy_and_expand_chars(node->value(), node->value() + node->value_size(), Ch(0), out);
-                }
-                else if (child->next_sibling() == 0 && child->type() == node_data)
-                {
+                } else if (child->next_sibling() == 0 && child->type() == node_data) {
                     // If node has a sole data child, only print its value without indenting
                     out = copy_and_expand_chars(child->value(), child->value() + child->value_size(), Ch(0), out);
-                }
-                else
-                {
+                } else {
                     // Print all children with full indenting
                     if (!(flags & print_no_indenting))
                         *out = Ch('\n'), ++out;
@@ -294,9 +248,9 @@
         }
 
         // Print declaration node
+
         template<class OutIt, class Ch>
-        inline OutIt print_declaration_node(OutIt out, const xml_node<Ch> *node, int flags, int indent)
-        {
+        inline OutIt print_declaration_node(OutIt out, const xml_node<Ch> *node, int flags, int indent) {
             // Print declaration start
             if (!(flags & print_no_indenting))
                 out = fill_chars(out, indent, Ch('\t'));
@@ -308,18 +262,18 @@
 
             // Print attributes
             out = print_attributes(out, node, flags);
-            
+
             // Print declaration end
             *out = Ch('?'), ++out;
             *out = Ch('>'), ++out;
-            
+
             return out;
         }
 
         // Print comment node
+
         template<class OutIt, class Ch>
-        inline OutIt print_comment_node(OutIt out, const xml_node<Ch> *node, int flags, int indent)
-        {
+        inline OutIt print_comment_node(OutIt out, const xml_node<Ch> *node, int flags, int indent) {
             assert(node->type() == node_comment);
             if (!(flags & print_no_indenting))
                 out = fill_chars(out, indent, Ch('\t'));
@@ -335,9 +289,9 @@
         }
 
         // Print doctype node
+
         template<class OutIt, class Ch>
-        inline OutIt print_doctype_node(OutIt out, const xml_node<Ch> *node, int flags, int indent)
-        {
+        inline OutIt print_doctype_node(OutIt out, const xml_node<Ch> *node, int flags, int indent) {
             assert(node->type() == node_doctype);
             if (!(flags & print_no_indenting))
                 out = fill_chars(out, indent, Ch('\t'));
@@ -357,9 +311,9 @@
         }
 
         // Print pi node
+
         template<class OutIt, class Ch>
-        inline OutIt print_pi_node(OutIt out, const xml_node<Ch> *node, int flags, int indent)
-        {
+        inline OutIt print_pi_node(OutIt out, const xml_node<Ch> *node, int flags, int indent) {
             assert(node->type() == node_pi);
             if (!(flags & print_no_indenting))
                 out = fill_chars(out, indent, Ch('\t'));
@@ -373,6 +327,68 @@
             return out;
         }
 
+        // Print node
+
+        template<class OutIt, class Ch>
+        inline OutIt print_node(OutIt out, const xml_node<Ch> *node, int flags, int indent) {
+            // Print proper node type
+            switch (node->type()) {
+
+                    // Document
+                case node_document:
+                    out = print_children(out, node, flags, indent);
+                    break;
+
+                    // Element
+                case node_element:
+                    out = print_element_node(out, node, flags, indent);
+                    break;
+
+                    // Data
+                case node_data:
+                    out = print_data_node(out, node, flags, indent);
+                    break;
+
+                    // CDATA
+                case node_cdata:
+                    out = print_cdata_node(out, node, flags, indent);
+                    break;
+
+                    // Declaration
+                case node_declaration:
+                    out = print_declaration_node(out, node, flags, indent);
+                    break;
+
+                    // Comment
+                case node_comment:
+                    out = print_comment_node(out, node, flags, indent);
+                    break;
+
+                    // Doctype
+                case node_doctype:
+                    out = print_doctype_node(out, node, flags, indent);
+                    break;
+
+                    // Pi
+                case node_pi:
+                    out = print_pi_node(out, node, flags, indent);
+                    break;
+
+                    // Unknown
+                default:
+                    assert(0);
+                    break;
+            }
+
+            // If indenting not disabled, add line break after node
+            if (!(flags & print_no_indenting))
+                *out = Ch('\n'), ++out;
+
+            // Return modified iterator
+            return out;
+        }
+
+
     }
     //! \endcond
 
@@ -384,9 +400,9 @@
     //! \param node Node to be printed. Pass xml_document to print entire document.
     //! \param flags Flags controlling how XML is printed.
     //! \return Output iterator pointing to position immediately after last character of printed text.
-    template<class OutIt, class Ch> 
-    inline OutIt print(OutIt out, const xml_node<Ch> &node, int flags = 0)
-    {
+
+    template<class OutIt, class Ch>
+    inline OutIt print(OutIt out, const xml_node<Ch> &node, int flags = 0) {
         return internal::print_node(out, &node, flags, 0);
     }
 
@@ -397,9 +413,9 @@
     //! \param node Node to be printed. Pass xml_document to print entire document.
     //! \param flags Flags controlling how XML is printed.
     //! \return Output stream.
-    template<class Ch> 
-    inline std::basic_ostream<Ch> &print(std::basic_ostream<Ch> &out, const xml_node<Ch> &node, int flags = 0)
-    {
+
+    template<class Ch>
+    inline std::basic_ostream<Ch> &print(std::basic_ostream<Ch> &out, const xml_node<Ch> &node, int flags = 0) {
         print(std::ostream_iterator<Ch>(out), node, flags);
         return out;
     }
@@ -408,12 +424,14 @@
     //! \param out Output stream to print to.
     //! \param node Node to be printed.
     //! \return Output stream.
-    template<class Ch> 
-    inline std::basic_ostream<Ch> &operator <<(std::basic_ostream<Ch> &out, const xml_node<Ch> &node)
-    {
+
+    template<class Ch>
+    inline std::basic_ostream<Ch> &operator <<(std::basic_ostream<Ch> &out, const xml_node<Ch> &node) {
         return print(out, node);
     }
 
+
+
 #endif
 
 }

=== modified file 'src/Core/ArgsParser.cpp'
--- src/Core/ArgsParser.cpp	2013-02-24 22:48:05 +0000
+++ src/Core/ArgsParser.cpp	2013-05-15 15:27:27 +0000
@@ -19,7 +19,7 @@
 static const std::string KEEP_DEAD = "keep-dead-tokens";
 
 std::ostream& operator<<(std::ostream& out, const Switch& flag) {
-	flag.Print(out);
+	flag.print(out);
 	return out;
 }
 
@@ -43,36 +43,36 @@
 	}
 }
 
-void Switch::Print(std::ostream& out) const {
+void Switch::print(std::ostream& out) const {
 	std::stringstream s;
-	s << "-" << ShortName();
-	s << " [ --" << LongName() << " ]";
+	s << "-" << getShortName();
+	s << " [ --" << getLongName() << " ]";
 	out << std::setw(WIDTH) << std::left << s.str();
-	PrintIndentedDescription(out, Description());
+	PrintIndentedDescription(out, getDescription());
 }
 ;
 
-void SwitchWithArg::Print(std::ostream& out) const {
+void SwitchWithArg::print(std::ostream& out) const {
 	std::stringstream s;
-	s << "-" << ShortName();
-	s << " [ --" << LongName() << " ] ";
+	s << "-" << getShortName();
+	s << " [ --" << getLongName() << " ] ";
 	s << " arg (=" << default_value << ")";
 	out << std::setw(WIDTH) << std::left << s.str();
-	PrintIndentedDescription(out, Description());
+	PrintIndentedDescription(out, getDescription());
 }
 ;
 
-void SwitchWithStringArg::Print(std::ostream& out) const {
+void SwitchWithStringArg::print(std::ostream& out) const {
 	std::stringstream s;
-	s << "-" << ShortName();
-	s << " [ --" << LongName() << " ] ";
+	s << "-" << getShortName();
+	s << " [ --" << getLongName() << " ] ";
 	s << " a1,a2,.. (=" << default_value << ")";
 	out << std::setw(WIDTH) << std::left << s.str();
-	PrintIndentedDescription(out, Description());
+	PrintIndentedDescription(out, getDescription());
 }
 ;
 
-bool Switch::Handles(const std::string& flag) const {
+bool Switch::handles(const std::string& flag) const {
 	std::stringstream stream;
 	stream << "-" << name << " ";
 	if (flag.find(stream.str()) != std::string::npos)
@@ -83,50 +83,50 @@
 }
 ;
 
-option Switch::Parse(const std::string& flag) {
-	assert(Handles(flag));
-	handled_option = true;
-	return option(LongName(), "1");
-}
-;
-
-option SwitchWithArg::Parse(const std::string& flag) {
-	assert(Handles(flag));
-	handled_option = true;
-	std::string copy(flag);
-	std::stringstream stream;
-	stream << "-" << ShortName() << " ";
-	if (flag.find(stream.str()) != std::string::npos) {
-		boost::erase_all(copy, stream.str());
-	} else {
-		std::stringstream long_name_stream;
-		long_name_stream << "--" << LongName() << " ";
-		boost::erase_all(copy, long_name_stream.str());
-	}
-	boost::trim(copy);
-	return option(LongName(), copy);
-}
-;
-
-option SwitchWithStringArg::Parse(const std::string& flag) {
-	assert(Handles(flag));
-	handled_option = true;
-	std::string copy(flag);
-	std::stringstream stream;
-	stream << "-" << ShortName() << " ";
-	if (flag.find(stream.str()) != std::string::npos) {
-		boost::erase_all(copy, stream.str());
-	} else {
-		std::stringstream long_name_stream;
-		long_name_stream << "--" << LongName() << " ";
-		boost::erase_all(copy, long_name_stream.str());
-	}
-	boost::trim(copy);
-	return option(LongName(), copy);
-}
-;
-
-void ArgsParser::Initialize() {
+option Switch::parse(const std::string& flag) {
+	assert(handles(flag));
+	handled_option = true;
+	return option(getLongName(), "1");
+}
+;
+
+option SwitchWithArg::parse(const std::string& flag) {
+	assert(handles(flag));
+	handled_option = true;
+	std::string copy(flag);
+	std::stringstream stream;
+	stream << "-" << getShortName() << " ";
+	if (flag.find(stream.str()) != std::string::npos) {
+		boost::erase_all(copy, stream.str());
+	} else {
+		std::stringstream long_name_stream;
+		long_name_stream << "--" << getLongName() << " ";
+		boost::erase_all(copy, long_name_stream.str());
+	}
+	boost::trim(copy);
+	return option(getLongName(), copy);
+}
+;
+
+option SwitchWithStringArg::parse(const std::string& flag) {
+	assert(handles(flag));
+	handled_option = true;
+	std::string copy(flag);
+	std::stringstream stream;
+	stream << "-" << getShortName() << " ";
+	if (flag.find(stream.str()) != std::string::npos) {
+		boost::erase_all(copy, stream.str());
+	} else {
+		std::stringstream long_name_stream;
+		long_name_stream << "--" << getLongName() << " ";
+		boost::erase_all(copy, long_name_stream.str());
+	}
+	boost::trim(copy);
+	return option(getLongName(), copy);
+}
+;
+
+void ArgsParser::initialize() {
     // NOTE: The Help() function only splits and indents descriptions based on newlines.
     //       Each line in the description is assumed to fit within the remaining width
     //       of the console, so keep descriptions short, or implement manual word-wrapping :).
@@ -164,7 +164,7 @@
             "Output trace in xml format for TAPAAL."));
 };
 
-void ArgsParser::Help() const {
+void ArgsParser::printHelp() const {
 	std::cout
 			<< "Usage: verifydtapn -k <number> [optional arguments] model-file query-file"
 			<< std::endl;
@@ -180,20 +180,20 @@
 }
 ;
 
-void ArgsParser::Version() const {
+void ArgsParser::printVersion() const {
 	std::cout << "VerifyDTAPN " << version << std::endl;
 	std::cout << "Licensed under BSD." << std::endl;
 }
 
-VerificationOptions ArgsParser::Parse(int argc, char* argv[]) const {
+VerificationOptions ArgsParser::parse(int argc, char* argv[]) const {
 	if (argc == 1 || std::string(argv[1]) == "-h"
 			|| std::string(argv[1]) == "--help") {
-		Help();
+		printHelp();
 		exit(0);
 	}
 
 	if (std::string(argv[1]) == "-v" || std::string(argv[1]) == "--version") {
-		Version();
+		printVersion();
 		exit(0);
 	}
 
@@ -244,8 +244,8 @@
 		bool handled = false;
 		for (parser_vec::const_iterator it = parsers.begin();
 				it != parsers.end(); it++) {
-			if ((*it)->Handles(*flag)) {
-				options.insert((*it)->Parse(*flag));
+			if ((*it)->handles(*flag)) {
+				options.insert((*it)->parse(*flag));
 				handled = true;
 			}
 		}
@@ -260,48 +260,48 @@
 	// Put in default values for non-specified options
 	for (parser_vec::const_iterator it = parsers.begin(); it != parsers.end();
 			it++) {
-		if (!(*it)->HandledOption()) {
-			options.insert((*it)->DefaultOption());
+		if (!(*it)->handledOption()) {
+			options.insert((*it)->getDefaultOption());
 		}
 	}
 
-	return CreateVerificationOptions(options, model_file, query_file);
+	return createVerificationOptions(options, model_file, query_file);
 }
 
-SearchType intToSearchTypeEnum(int i) {
+VerificationOptions::SearchType intToSearchTypeEnum(int i) {
 	switch (i) {
 	case 0:
-		return BREADTHFIRST;
+		return VerificationOptions::BREADTHFIRST;
 	case 1:
-		return DEPTHFIRST;
+		return VerificationOptions::DEPTHFIRST;
 	case 2:
-		return RANDOM;
+		return VerificationOptions::RANDOM;
 	case 3:
-		return COVERMOST;
+		return VerificationOptions::COVERMOST;
 	default:
 		std::cout << "Unknown search strategy specified." << std::endl;
 		exit(1);
 	}
 }
 
-VerificationType intToVerificationTypeEnum(int i) {
+VerificationOptions::VerificationType intToVerificationTypeEnum(int i) {
 	switch (i) {
 	case 0:
-		return DISCRETE;
+		return VerificationOptions::DISCRETE;
 	case 1:
-		return TIMEDART;
+		return VerificationOptions::TIMEDART;
 	default:
 		std::cout << "Unknown verification method specified." << std::endl;
 		exit(1);
 	}
 }
 
-MemoryOptimization intToMemoryOptimizationEnum(int i) {
+VerificationOptions::MemoryOptimization intToMemoryOptimizationEnum(int i) {
 	switch (i) {
 	case 0:
-		return NO_MEMORY_OPTIMIZATION;
+		return VerificationOptions::NO_MEMORY_OPTIMIZATION;
 	case 1:
-		return PTRIE;
+		return VerificationOptions::PTRIE;
 	default:
 		std::cout << "Unknown memory optimization specified." << std::endl;
 		exit(1);
@@ -309,19 +309,19 @@
 }
 
 
-Trace intToEnum(int i) {
+VerificationOptions::Trace intToEnum(int i) {
 	switch (i) {
 	case 0:
-		return NONE;
+		return VerificationOptions::NO_TRACE;
 	case 1:
-		return SOME;
+		return VerificationOptions::SOME_TRACE;
 	default:
 		std::cout << "Unknown trace option specified." << std::endl;
 		exit(1);
 	}
 }
 
-unsigned int ArgsParser::TryParseInt(const option& option) const {
+unsigned int ArgsParser::tryParseInt(const option& option) const {
 	unsigned int result = 0;
 	try {
 		result = boost::lexical_cast<unsigned int>(option.second);
@@ -333,32 +333,32 @@
 	return result;
 }
 
-std::vector<std::string> ArgsParser::ParseIncPlaces(
+std::vector<std::string> ArgsParser::parseIncPlaces(
 		const std::string& string) const {
 	std::vector<std::string> vec;
 	boost::split(vec, string, boost::is_any_of(","));
 	return vec;
 }
 
-VerificationOptions ArgsParser::CreateVerificationOptions(const option_map& map,
+VerificationOptions ArgsParser::createVerificationOptions(const option_map& map,
 		const std::string& modelFile, const std::string& queryFile) const {
 	assert(map.find(KBOUND_OPTION) != map.end());
-	unsigned int kbound = TryParseInt(*map.find(KBOUND_OPTION));
+	unsigned int kbound = tryParseInt(*map.find(KBOUND_OPTION));
 
 	assert(map.find(SEARCH_OPTION) != map.end());
-	SearchType search = intToSearchTypeEnum(
-			TryParseInt(*map.find(SEARCH_OPTION)));
+	VerificationOptions::SearchType search = intToSearchTypeEnum(
+			tryParseInt(*map.find(SEARCH_OPTION)));
 
 	assert(map.find(VERIFICATION_OPTION) != map.end());
-	VerificationType verification = intToVerificationTypeEnum(
-			TryParseInt(*map.find(VERIFICATION_OPTION)));
+	VerificationOptions::VerificationType verification = intToVerificationTypeEnum(
+			tryParseInt(*map.find(VERIFICATION_OPTION)));
         
 	assert(map.find(MEMORY_OPTIMIZATION_OPTION) != map.end());
-	MemoryOptimization memoptimization = intToMemoryOptimizationEnum(
-			TryParseInt(*map.find(MEMORY_OPTIMIZATION_OPTION)));
+	VerificationOptions::MemoryOptimization memoptimization = intToMemoryOptimizationEnum(
+			tryParseInt(*map.find(MEMORY_OPTIMIZATION_OPTION)));
         
 	assert(map.find(TRACE_OPTION) != map.end());
-	Trace trace = intToEnum(TryParseInt(*map.find(TRACE_OPTION)));
+	VerificationOptions::Trace trace = intToEnum(tryParseInt(*map.find(TRACE_OPTION)));
 
 	assert(map.find(MAX_CONSTANT_OPTION) != map.end());
 	bool max_constant = boost::lexical_cast<bool>(

=== modified file 'src/Core/ArgsParser.hpp'
--- src/Core/ArgsParser.hpp	2013-03-25 14:03:05 +0000
+++ src/Core/ArgsParser.hpp	2013-05-15 15:27:27 +0000
@@ -35,14 +35,14 @@
 			Switch(const std::string& name, const std::string& long_name, const std::string& description) : name(name), long_name(long_name), description(description), handled_option(false) { };
 			virtual ~Switch() { };
 		public:
-			inline const std::string& ShortName() const { return name; };
-			inline const std::string& LongName() const { return long_name; };
-			inline const std::string& Description() const { return description; };
-			virtual bool Handles(const std::string& flag) const;
-			virtual option Parse(const std::string& flag);
-			virtual void Print(std::ostream& out) const;
-			inline bool HandledOption() const { return handled_option; };
-			virtual option DefaultOption() const { return option(long_name, "0"); };
+			inline const std::string& getShortName() const { return name; };
+			inline const std::string& getLongName() const { return long_name; };
+			inline const std::string& getDescription() const { return description; };
+			virtual bool handles(const std::string& flag) const;
+			virtual option parse(const std::string& flag);
+			virtual void print(std::ostream& out) const;
+			inline bool handledOption() const { return handled_option; };
+			virtual option getDefaultOption() const { return option(long_name, "0"); };
 		private:
 			std::string name;
 			std::string long_name;
@@ -58,9 +58,9 @@
 	public:
 		SwitchWithStringArg(const std::string& name, const std::string& long_name, const std::string& description, const std::string& default_value) : Switch(name, long_name, description), default_value(default_value) { };
 		virtual ~SwitchWithStringArg() { };
-		virtual option Parse(const std::string& flag);
-		virtual void Print(std::ostream& out) const;
-		virtual option DefaultOption() const { return option(LongName(), default_value); };
+		virtual option parse(const std::string& flag);
+		virtual void print(std::ostream& out) const;
+		virtual option getDefaultOption() const { return option(getLongName(), default_value); };
 	private:
 		std::string default_value;
 	};
@@ -70,9 +70,9 @@
 	public:
 		SwitchWithArg(const std::string& name, const std::string& long_name, const std::string& description, unsigned int default_value) : Switch(name, long_name, description), default_value(default_value) { };
 		virtual ~SwitchWithArg() { };
-		virtual option Parse(const std::string& flag);
-		virtual void Print(std::ostream& out) const;
-		virtual option DefaultOption() const { return option(LongName(), boost::lexical_cast<std::string>(default_value)); };
+		virtual option parse(const std::string& flag);
+		virtual void print(std::ostream& out) const;
+		virtual option getDefaultOption() const { return option(getLongName(), boost::lexical_cast<std::string>(default_value)); };
 	private:
 		unsigned int default_value;
 	};
@@ -80,17 +80,17 @@
 	class ArgsParser {
 		typedef std::vector< boost::shared_ptr<Switch> > parser_vec;
 	public:
-		ArgsParser() : parsers(), version(2,0,0) { Initialize(); };
+		ArgsParser() : parsers(), version(2,0,1) { initialize(); };
 		virtual ~ArgsParser() {};
 
-		VerificationOptions Parse(int argc, char* argv[]) const;
+		VerificationOptions parse(int argc, char* argv[]) const;
 	private:
-		VerificationOptions CreateVerificationOptions(const option_map& map,const std::string& modelFile, const std::string& queryFile) const;
-		unsigned int TryParseInt(const option& option) const;
-		std::vector<std::string> ParseIncPlaces(const std::string& string) const;
-		void Initialize();
-		void Help() const;
-		void Version() const;
+		VerificationOptions createVerificationOptions(const option_map& map,const std::string& modelFile, const std::string& queryFile) const;
+		unsigned int tryParseInt(const option& option) const;
+		std::vector<std::string> parseIncPlaces(const std::string& string) const;
+		void initialize();
+		void printHelp() const;
+		void printVersion() const;
 	private: // data
 		parser_vec parsers;
 		VerifyTAPN::Version version;

=== modified file 'src/Core/QueryParser/AST.cpp'
--- src/Core/QueryParser/AST.cpp	2012-03-02 10:59:16 +0000
+++ src/Core/QueryParser/AST.cpp	2013-05-15 15:27:27 +0000
@@ -8,14 +8,14 @@
 			return new NotExpression(*this);
 		}
 
-		void NotExpression::Accept(Visitor& visitor, boost::any& context) const
+		void NotExpression::accept(Visitor& visitor, boost::any& context) const
 		{
-			visitor.Visit(*this, context);
+			visitor.visit(*this, context);
 		}
 
-		void BoolExpression::Accept(Visitor& visitor, boost::any& context) const
+		void BoolExpression::accept(Visitor& visitor, boost::any& context) const
 		{
-			visitor.Visit(*this, context);
+			visitor.visit(*this, context);
 		}
 
 		BoolExpression* BoolExpression::clone() const
@@ -23,9 +23,9 @@
 			return new BoolExpression(*this);
 		}
 
-		void AtomicProposition::Accept(Visitor& visitor, boost::any& context) const
+		void AtomicProposition::accept(Visitor& visitor, boost::any& context) const
 		{
-			visitor.Visit(*this, context);
+			visitor.visit(*this, context);
 		}
 
 		AtomicProposition* AtomicProposition::clone() const
@@ -38,9 +38,9 @@
 			return new AndExpression(*this);
 		}
 
-		void AndExpression::Accept(Visitor& visitor, boost::any& context) const
+		void AndExpression::accept(Visitor& visitor, boost::any& context) const
 		{
-			visitor.Visit(*this, context);
+			visitor.visit(*this, context);
 		}
 
 		OrExpression* OrExpression::clone() const
@@ -48,9 +48,9 @@
 			return new OrExpression(*this);
 		}
 
-		void OrExpression::Accept(Visitor& visitor, boost::any& context) const
+		void OrExpression::accept(Visitor& visitor, boost::any& context) const
 		{
-			visitor.Visit(*this, context);
+			visitor.visit(*this, context);
 		}
 
 		ParExpression* ParExpression::clone() const
@@ -58,9 +58,9 @@
 			return new ParExpression(*this);
 		}
 
-		void ParExpression::Accept(Visitor& visitor, boost::any& context) const
+		void ParExpression::accept(Visitor& visitor, boost::any& context) const
 		{
-			visitor.Visit(*this, context);
+			visitor.visit(*this, context);
 		}
 
 		Query* Query::clone() const
@@ -68,9 +68,9 @@
 			return new Query(*this);
 		}
 
-		void Query::Accept(Visitor& visitor, boost::any& context) const
+		void Query::accept(Visitor& visitor, boost::any& context) const
 		{
-			visitor.Visit(*this, context);
+			visitor.visit(*this, context);
 		}
 	}
 }

=== modified file 'src/Core/QueryParser/AST.hpp'
--- src/Core/QueryParser/AST.hpp	2012-04-19 12:40:05 +0000
+++ src/Core/QueryParser/AST.hpp	2013-05-15 15:27:27 +0000
@@ -12,7 +12,7 @@
 		class Visitable
 		{
 		public:
-			virtual void Accept(Visitor& visitor, boost::any& context) const = 0;
+			virtual void accept(Visitor& visitor, boost::any& context) const = 0;
 		};
 
 		class Expression : public Visitable
@@ -43,9 +43,9 @@
 			};
 
 			virtual NotExpression* clone() const;
-			virtual void Accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, boost::any& context) const;
 
-			const Expression& Child() const { return *expr; }
+			const Expression& getChild() const { return *expr; }
 		private:
 			Expression* expr;
 		};
@@ -57,9 +57,9 @@
 			virtual ~BoolExpression() { };
 
 			virtual BoolExpression* clone() const;
-			virtual void Accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, boost::any& context) const;
 
-			bool GetValue() const { return value; };
+			bool getValue() const { return value; };
 		private:
 			bool value;
 		};
@@ -82,11 +82,11 @@
 			virtual ~AtomicProposition() { };
 
 			virtual AtomicProposition* clone() const;
-			virtual void Accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, boost::any& context) const;
 
-			const int Place() const { return place; }
-			const std::string& Operator() const { return op; }
-			int N() const { return n; }
+			const int getPlace() const { return place; }
+			const std::string& getOperator() const { return op; }
+			int getNumberOfTokens() const { return n; }
 		private:
 			int place;
 			std::string op;
@@ -116,10 +116,10 @@
 			}
 
 			virtual AndExpression* clone() const;
-			void Accept(Visitor& visitor, boost::any& context) const;
+			void accept(Visitor& visitor, boost::any& context) const;
 
-			const Expression& Left() const { return *left; }
-			const Expression& Right() const { return *right; }
+			const Expression& getLeft() const { return *left; }
+			const Expression& getRight() const { return *right; }
 		private:
 			Expression* left;
 			Expression* right;
@@ -151,10 +151,10 @@
 
 
 			virtual OrExpression* clone() const;
-			virtual void Accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, boost::any& context) const;
 
-			const Expression& Left() const { return *left; }
-			const Expression& Right() const { return *right; }
+			const Expression& getLeft() const { return *left; }
+			const Expression& getRight() const { return *right; }
 		private:
 			Expression* left;
 			Expression* right;
@@ -180,9 +180,9 @@
 			};
 
 			virtual ParExpression* clone() const;
-			virtual void Accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, boost::any& context) const;
 
-			const Expression& Child() const { return *expr; }
+			const Expression& getChild() const { return *expr; }
 		private:
 			Expression* expr;
 		};
@@ -206,10 +206,10 @@
 			virtual ~Query() { if( expr ) delete expr; }
 
 			virtual Query* clone() const;
-			virtual void Accept(Visitor& visitor, boost::any& context) const;
+			virtual void accept(Visitor& visitor, boost::any& context) const;
 
-			Quantifier GetQuantifier() const { return quantifier; }
-			const Expression& Child() const { return *expr; }
+			Quantifier getQuantifier() const { return quantifier; }
+			const Expression& getChild() const { return *expr; }
 		private:
 			Quantifier quantifier;
 			Expression* expr;

=== modified file 'src/Core/QueryParser/Generated/location.hh'
--- src/Core/QueryParser/Generated/location.hh	2013-04-14 11:02:23 +0000
+++ src/Core/QueryParser/Generated/location.hh	2013-05-15 15:27:27 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.6.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Locations for Bison parsers in C++
    
-      Copyright (C) 2002-2007, 2009-2012 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
@@ -40,10 +40,10 @@
 
 # include "position.hh"
 
-/* Line 164 of location.cc  */
+/* Line 166 of location.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-/* Line 164 of location.cc  */
+/* Line 166 of location.cc  */
 #line 48 "Core/QueryParser/Generated/location.hh"
 
   /// Abstract a location.
@@ -157,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;
@@ -172,10 +174,10 @@
     return ostr;
   }
 
-/* Line 292 of location.cc  */
+/* Line 296 of location.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-/* Line 292 of location.cc  */
-#line 180 "Core/QueryParser/Generated/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-04-14 11:02:23 +0000
+++ src/Core/QueryParser/Generated/parser.cpp	2013-05-15 15:27:27 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.6.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Skeleton implementation for Bison LALR(1) parsers in C++
    
-      Copyright (C) 2002-2012 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,7 +33,7 @@
 
 /* First part of user declarations.  */
 
-/* Line 278 of lalr1.cc  */
+/* Line 283 of lalr1.cc  */
 #line 38 "Core/QueryParser/Generated/parser.cpp"
 
 
@@ -41,16 +41,16 @@
 
 /* User implementation prologue.  */
 
-/* Line 284 of lalr1.cc  */
+/* Line 289 of lalr1.cc  */
 #line 46 "Core/QueryParser/Generated/parser.cpp"
 /* Unqualified %code blocks.  */
-/* Line 285 of lalr1.cc  */
+/* Line 290 of lalr1.cc  */
 #line 37 "Core/QueryParser/grammar.yy"
 
 	#include "../TAPNQueryParser.hpp"
 
 
-/* Line 285 of lalr1.cc  */
+/* Line 290 of lalr1.cc  */
 #line 55 "Core/QueryParser/Generated/parser.cpp"
 
 
@@ -129,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 */
 
@@ -143,10 +143,10 @@
 #define YYERROR		goto yyerrorlab
 #define YYRECOVERING()  (!!yyerrstatus_)
 
-/* Line 352 of lalr1.cc  */
+/* Line 357 of lalr1.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-/* Line 352 of lalr1.cc  */
+/* Line 357 of lalr1.cc  */
 #line 151 "Core/QueryParser/Generated/parser.cpp"
 
   /* Return YYSTR after stripping away unnecessary quotes and
@@ -216,11 +216,7 @@
     std::ostream& yyo = debug_stream ();
     std::ostream& yyoutput = yyo;
     YYUSE (yyoutput);
-    switch (yytype)
-      {
-         default:
-	  break;
-      }
+    YYUSE (yytype);
   }
 
 
@@ -244,119 +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 453 of lalr1.cc  */
+    {
+      case 3: /* IDENTIFIER */
+/* Line 452 of lalr1.cc  */
 #line 52 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).string); };
-/* Line 453 of lalr1.cc  */
-#line 257 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 254 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 4: /* LESS */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 52 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).string); };
-/* Line 453 of lalr1.cc  */
-#line 264 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 261 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 5: /* LESSEQUAL */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 52 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).string); };
-/* Line 453 of lalr1.cc  */
-#line 271 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 268 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 6: /* EQUAL */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 52 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).string); };
-/* Line 453 of lalr1.cc  */
-#line 278 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 275 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 7: /* GREATEREQUAL */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 52 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).string); };
-/* Line 453 of lalr1.cc  */
-#line 285 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 282 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 8: /* GREATER */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 52 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).string); };
-/* Line 453 of lalr1.cc  */
-#line 292 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 289 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 22: /* query */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 54 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).query); };
-/* Line 453 of lalr1.cc  */
-#line 299 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).query); };
+/* Line 452 of lalr1.cc  */
+#line 296 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 23: /* expression */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 53 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).expr); };
-/* Line 453 of lalr1.cc  */
-#line 306 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 303 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 24: /* parExpression */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 53 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).expr); };
-/* Line 453 of lalr1.cc  */
-#line 313 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 310 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 25: /* notExpression */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 53 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).expr); };
-/* Line 453 of lalr1.cc  */
-#line 320 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 317 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 26: /* orExpression */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 53 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).expr); };
-/* Line 453 of lalr1.cc  */
-#line 327 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 324 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 27: /* andExpression */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 53 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).expr); };
-/* Line 453 of lalr1.cc  */
-#line 334 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 331 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 28: /* boolExpression */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 53 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).expr); };
-/* Line 453 of lalr1.cc  */
-#line 341 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 338 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 29: /* atomicProposition */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 53 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).expr); };
-/* Line 453 of lalr1.cc  */
-#line 348 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).expr); };
+/* Line 452 of lalr1.cc  */
+#line 345 "Core/QueryParser/Generated/parser.cpp"
+        break;
       case 30: /* compareOp */
-/* Line 453 of lalr1.cc  */
+/* Line 452 of lalr1.cc  */
 #line 52 "Core/QueryParser/grammar.yy"
-	{ delete ((*yyvaluep).string); };
-/* Line 453 of lalr1.cc  */
-#line 355 "Core/QueryParser/Generated/parser.cpp"
-	break;
+        { delete ((*yyvaluep).string); };
+/* Line 452 of lalr1.cc  */
+#line 352 "Core/QueryParser/Generated/parser.cpp"
+        break;
 
-	default:
-	  break;
-      }
+      default:
+        break;
+    }
   }
 
   void
@@ -437,6 +434,10 @@
 
     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;
 
 
@@ -448,15 +449,15 @@
   yylloc.begin.filename = yylloc.end.filename = &driver.file;
 }
 /* Line 539 of lalr1.cc  */
-#line 452 "Core/QueryParser/Generated/parser.cpp"
+#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);
 
@@ -482,8 +483,8 @@
     /* 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.  */
@@ -556,125 +557,129 @@
     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 661 of lalr1.cc  */
+          case 2:
+/* Line 664 of lalr1.cc  */
 #line 58 "Core/QueryParser/grammar.yy"
-    { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EF, (yysemantic_stack_[(2) - (2)].expr)); driver.SetAST((yyval.query)); }
+    { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EF, (yysemantic_stack_[(2) - (2)].expr)); driver.setAST((yyval.query)); }
     break;
 
   case 3:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 59 "Core/QueryParser/grammar.yy"
-    { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AG, (yysemantic_stack_[(2) - (2)].expr)); driver.SetAST((yyval.query)); }
+    { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AG, (yysemantic_stack_[(2) - (2)].expr)); driver.setAST((yyval.query)); }
     break;
 
   case 4:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 60 "Core/QueryParser/grammar.yy"
-    { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EG, (yysemantic_stack_[(2) - (2)].expr)); driver.SetAST((yyval.query)); }
+    { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EG, (yysemantic_stack_[(2) - (2)].expr)); driver.setAST((yyval.query)); }
     break;
 
   case 5:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 61 "Core/QueryParser/grammar.yy"
-    { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AF, (yysemantic_stack_[(2) - (2)].expr)); driver.SetAST((yyval.query)); }
+    { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AF, (yysemantic_stack_[(2) - (2)].expr)); driver.setAST((yyval.query)); }
     break;
 
   case 6:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 64 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 7:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 65 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 8:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 66 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 9:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 67 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 10:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 68 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 11:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 69 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 12:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 75 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::ParExpression((yysemantic_stack_[(3) - (2)].expr)); }
     break;
 
   case 13:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 76 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::NotExpression((yysemantic_stack_[(2) - (2)].expr)); }
     break;
 
   case 14:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 77 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::OrExpression((yysemantic_stack_[(3) - (1)].expr), (yysemantic_stack_[(3) - (3)].expr)); }
     break;
 
   case 15:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 78 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::AndExpression((yysemantic_stack_[(3) - (1)].expr), (yysemantic_stack_[(3) - (3)].expr)); }
     break;
 
   case 16:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 79 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(true); }
     break;
 
   case 17:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 80 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(false); }
     break;
 
   case 18:
-/* Line 661 of lalr1.cc  */
+/* Line 664 of lalr1.cc  */
 #line 82 "Core/QueryParser/grammar.yy"
     { 
-		int placeIndex = driver.tapn().GetPlaceIndex(*(yysemantic_stack_[(3) - (1)].string));
+		int placeIndex = driver.getTAPN().getPlaceIndex(*(yysemantic_stack_[(3) - (1)].string));
 		if(placeIndex == -1) error((yylocation_stack_[(3) - (1)]), "unknown place"); 
 		(yyval.expr) = new VerifyTAPN::AST::AtomicProposition(placeIndex, (yysemantic_stack_[(3) - (2)].string), (yysemantic_stack_[(3) - (3)].number)); 
 	}
     break;
 
 
-/* Line 661 of lalr1.cc  */
-#line 675 "Core/QueryParser/Generated/parser.cpp"
-	default:
-          break;
+/* Line 664 of lalr1.cc  */
+#line 679 "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.
@@ -725,20 +730,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
@@ -787,7 +791,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",
@@ -835,16 +839,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.
@@ -1173,12 +1203,12 @@
   const unsigned int Parser::yyuser_token_number_max_ = 275;
   const Parser::token_number_type Parser::yyundef_token_ = 2;
 
-/* Line 1106 of lalr1.cc  */
+/* Line 1135 of lalr1.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-/* Line 1106 of lalr1.cc  */
-#line 1181 "Core/QueryParser/Generated/parser.cpp"
-/* Line 1107 of lalr1.cc  */
+/* Line 1135 of lalr1.cc  */
+#line 1211 "Core/QueryParser/Generated/parser.cpp"
+/* Line 1136 of lalr1.cc  */
 #line 89 "Core/QueryParser/grammar.yy"
 
 

=== modified file 'src/Core/QueryParser/Generated/parser.hpp'
--- src/Core/QueryParser/Generated/parser.hpp	2013-04-14 11:02:23 +0000
+++ src/Core/QueryParser/Generated/parser.hpp	2013-05-15 15:27:27 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.6.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Skeleton interface for Bison LALR(1) parsers in C++
    
-      Copyright (C) 2002-2012 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
@@ -41,7 +41,7 @@
 # define YY_YY_CORE_QUERYPARSER_GENERATED_PARSER_HPP_INCLUDED
 
 /* "%code requires" blocks.  */
-/* Line 36 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 7 "Core/QueryParser/grammar.yy"
 
 # include <string>
@@ -51,7 +51,7 @@
 }
 
 
-/* Line 36 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 56 "Core/QueryParser/Generated/parser.hpp"
 
 
@@ -65,10 +65,10 @@
 # define YYDEBUG 0
 #endif
 
-/* Line 36 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-/* Line 36 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 73 "Core/QueryParser/Generated/parser.hpp"
 
   /// A Bison parser.
@@ -79,7 +79,7 @@
 #ifndef YYSTYPE
     union semantic_type
     {
-/* Line 36 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 30 "Core/QueryParser/grammar.yy"
 
 	int          					number;
@@ -88,7 +88,7 @@
 	VerifyTAPN::AST::Query*		 	query;
 
 
-/* Line 36 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 93 "Core/QueryParser/Generated/parser.hpp"
     };
 #else
@@ -149,6 +149,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.
@@ -266,6 +270,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.
@@ -293,11 +298,11 @@
     /* User arguments.  */
     VerifyTAPN::TAPNQueryParser& driver;
   };
-/* Line 36 of lalr1.cc  */
+/* Line 33 of lalr1.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-/* Line 36 of lalr1.cc  */
-#line 301 "Core/QueryParser/Generated/parser.hpp"
+/* Line 33 of lalr1.cc  */
+#line 306 "Core/QueryParser/Generated/parser.hpp"
 
 
 

=== modified file 'src/Core/QueryParser/Generated/position.hh'
--- src/Core/QueryParser/Generated/position.hh	2013-04-14 11:02:23 +0000
+++ src/Core/QueryParser/Generated/position.hh	2013-05-15 15:27:27 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.6.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Positions for Bison parsers in C++
    
-      Copyright (C) 2002-2007, 2009-2012 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
@@ -50,10 +50,10 @@
 #  endif
 # endif
 
-/* Line 38 of location.cc  */
+/* Line 36 of location.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-/* Line 38 of location.cc  */
+/* Line 36 of location.cc  */
 #line 58 "Core/QueryParser/Generated/position.hh"
   /// Abstract a position.
   class position
@@ -157,17 +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 149 of location.cc  */
+/* Line 148 of location.cc  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-/* Line 149 of location.cc  */
-#line 173 "Core/QueryParser/Generated/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-04-14 11:02:23 +0000
+++ src/Core/QueryParser/Generated/stack.hh	2013-05-15 15:27:27 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.6.5.  */
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
 
 /* Stack handling for Bison parsers in C++
    
-      Copyright (C) 2002-2012 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
@@ -40,10 +40,10 @@
 
 # include <deque>
 
-/* Line 37 of stack.hh  */
+/* Line 34 of stack.hh  */
 #line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-/* Line 37 of stack.hh  */
+/* Line 34 of stack.hh  */
 #line 48 "Core/QueryParser/Generated/stack.hh"
   template <class T, class S = std::deque<T> >
   class stack
@@ -90,6 +90,12 @@
         seq_.pop_front ();
     }
 
+    void
+    clear ()
+    {
+      seq_.clear ();
+    }
+
     inline
     unsigned int
     height () const
@@ -101,6 +107,8 @@
     inline const_iterator end () const { return seq_.rend (); }
 
   private:
+    stack (const stack&);
+    stack& operator= (const stack&);
     S seq_;
   };
 
@@ -126,10 +134,10 @@
     const S& stack_;
     unsigned int range_;
   };
-/* Line 119 of stack.hh  */
+/* Line 124 of stack.hh  */
 #line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-/* Line 119 of stack.hh  */
-#line 134 "Core/QueryParser/Generated/stack.hh"
+/* 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	2012-03-02 10:59:16 +0000
+++ src/Core/QueryParser/NormalizationVisitor.cpp	2013-05-15 15:27:27 +0000
@@ -13,83 +13,83 @@
 			Tuple(bool negate, Expression* expr) : negate(negate), returnExpr(expr) {};
 		};
 
-		void NormalizationVisitor::Visit(const NotExpression& expr, boost::any& context)
+		void NormalizationVisitor::visit(const NotExpression& expr, boost::any& context)
 		{
 			Tuple& tuple = boost::any_cast<Tuple&>(context);
 			boost::any any = Tuple(!tuple.negate, NULL);
-			expr.Child().Accept(*this, any);
+			expr.getChild().accept(*this, any);
 			tuple.returnExpr = boost::any_cast<Tuple&>(any).returnExpr;
 		}
 
-		void NormalizationVisitor::Visit(const ParExpression& expr, boost::any& context)
+		void NormalizationVisitor::visit(const ParExpression& expr, boost::any& context)
 		{
 			Tuple& tuple = boost::any_cast<Tuple&>(context);
 			boost::any any = Tuple(tuple.negate, NULL);
-			expr.Child().Accept(*this, any);
+			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.Left().Accept(*this, left);
-				expr.Right().Accept(*this, right);
-				tuple.returnExpr = new AndExpression(boost::any_cast<Tuple&>(left).returnExpr, boost::any_cast<Tuple&>(right).returnExpr);
-			}else{
-				expr.Left().Accept(*this, left);
-				expr.Right().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.Left().Accept(*this, left);
-				expr.Right().Accept(*this, right);
-				tuple.returnExpr = new OrExpression(boost::any_cast<Tuple&>(left).returnExpr, boost::any_cast<Tuple&>(right).returnExpr);
-			}else{
-				expr.Left().Accept(*this, left);
-				expr.Right().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)
+		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);
 			std::string op;
 			if(tuple.negate){
-				op = NegateOperator(expr.Operator());
+				op = negateOperator(expr.getOperator());
 			}else{
-				op = expr.Operator();
+				op = expr.getOperator();
 			}
-			tuple.returnExpr = new AtomicProposition(expr.Place(), &op, expr.N());
+			tuple.returnExpr = new AtomicProposition(expr.getPlace(), &op, expr.getNumberOfTokens());
 		}
 
-		void NormalizationVisitor::Visit(const BoolExpression& expr, boost::any& context)
+		void NormalizationVisitor::visit(const BoolExpression& expr, boost::any& context)
 		{
 			Tuple& tuple = boost::any_cast<Tuple&>(context);
 			if(tuple.negate){
-				tuple.returnExpr = new BoolExpression(!expr.GetValue());
+				tuple.returnExpr = new BoolExpression(!expr.getValue());
 			}else{
-				tuple.returnExpr = new BoolExpression(expr.GetValue());
+				tuple.returnExpr = new BoolExpression(expr.getValue());
 			}
 		}
 
-		void NormalizationVisitor::Visit(const Query& query, boost::any& context)
+		void NormalizationVisitor::visit(const Query& query, boost::any& context)
 		{
 			boost::any any = Tuple(false, NULL);
-			query.Child().Accept(*this, any);
+			query.getChild().accept(*this, any);
 
-			normalizedQuery = new AST::Query(query.GetQuantifier(), boost::any_cast<Tuple&>(any).returnExpr);
+			normalizedQuery = new AST::Query(query.getQuantifier(), boost::any_cast<Tuple&>(any).returnExpr);
 		}
 
-		std::string NormalizationVisitor::NegateOperator(const std::string& op) const{
+		std::string NormalizationVisitor::negateOperator(const std::string& op) const{
 			if(op == "=" || op == "=="){
 				return "!=";
 			}else if(op == ">"){

=== modified file 'src/Core/QueryParser/NormalizationVisitor.hpp'
--- src/Core/QueryParser/NormalizationVisitor.hpp	2012-03-02 10:59:16 +0000
+++ src/Core/QueryParser/NormalizationVisitor.hpp	2013-05-15 15:27:27 +0000
@@ -20,17 +20,17 @@
 		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 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);
 
-			AST::Query* Normalize(const AST::Query& query) { boost::any any; query.Accept(*this, any); return normalizedQuery; };
+			AST::Query* normalize(const AST::Query& query) { boost::any any; query.accept(*this, any); return normalizedQuery; };
 		private:
-			std::string NegateOperator(const std::string& op) const;
+			std::string negateOperator(const std::string& op) const;
 		private:
 			AST::Query* normalizedQuery;
 		};

=== modified file 'src/Core/QueryParser/TAPNQueryParser.cpp'
--- src/Core/QueryParser/TAPNQueryParser.cpp	2012-03-02 10:59:16 +0000
+++ src/Core/QueryParser/TAPNQueryParser.cpp	2013-05-15 15:27:27 +0000
@@ -14,11 +14,11 @@
 		return result;
 	}
 
-	void TAPNQueryParser::SetAST(AST::Query* query){
+	void TAPNQueryParser::setAST(AST::Query* query){
 		ast = query->clone();
 	}
 
-	AST::Query* TAPNQueryParser::GetAST(){
+	AST::Query* TAPNQueryParser::getAST(){
 		return ast;
 	}
 

=== modified file 'src/Core/QueryParser/TAPNQueryParser.hpp'
--- src/Core/QueryParser/TAPNQueryParser.hpp	2012-03-02 10:59:16 +0000
+++ src/Core/QueryParser/TAPNQueryParser.hpp	2013-05-15 15:27:27 +0000
@@ -31,17 +31,18 @@
 
 	public:
 		int parse(const std::string& file);
-		void SetAST(VerifyTAPN::AST::Query* ast);
-		AST::Query* GetAST();
+		void setAST(VerifyTAPN::AST::Query* ast);
+		AST::Query* getAST();
 
-		const VerifyTAPN::TAPN::TimedArcPetriNet& tapn() { return net; };
+		const VerifyTAPN::TAPN::TimedArcPetriNet& getTAPN() { return net; };
 
 	public: // error handling
 		void error(const location& l, const std::string& m);
 		void error(const std::string& m);
 
-	public:
+                // must be public for the generated lexer and parser to work!
 		std::string file;
+        private:
 		VerifyTAPN::AST::Query* ast;
 		const VerifyTAPN::TAPN::TimedArcPetriNet& net;
 	};

=== modified file 'src/Core/QueryParser/Visitor.hpp'
--- src/Core/QueryParser/Visitor.hpp	2012-03-02 10:59:16 +0000
+++ src/Core/QueryParser/Visitor.hpp	2013-05-15 15:27:27 +0000
@@ -19,13 +19,13 @@
 		{
 		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 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;
 		};
 	}
 }

=== modified file 'src/Core/QueryParser/grammar.yy'
--- src/Core/QueryParser/grammar.yy	2012-04-19 12:40:05 +0000
+++ src/Core/QueryParser/grammar.yy	2013-05-15 15:27:27 +0000
@@ -55,10 +55,10 @@
 
 %%
 %start query;
-query				: EF expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EF, $2); driver.SetAST($$); }
-					| AG expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AG, $2); driver.SetAST($$); }
-					| EG expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EG, $2); driver.SetAST($$); }
-					| AF expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AF, $2); driver.SetAST($$); }
+query				: EF expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EF, $2); driver.setAST($$); }
+					| AG expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AG, $2); driver.setAST($$); }
+					| EG expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EG, $2); driver.setAST($$); }
+					| AF expression { $$ = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AF, $2); driver.setAST($$); }
 ;
 
 expression			: parExpression { $$ = $1; }
@@ -80,7 +80,7 @@
 					| BOOL_FALSE { $$ = new VerifyTAPN::AST::BoolExpression(false); };
 atomicProposition	: IDENTIFIER compareOp NUMBER 
 	{ 
-		int placeIndex = driver.tapn().GetPlaceIndex(*$1);
+		int placeIndex = driver.getTAPN().getPlaceIndex(*$1);
 		if(placeIndex == -1) error(@1, "unknown place"); 
 		$$ = new VerifyTAPN::AST::AtomicProposition(placeIndex, $2, $3); 
 	};

=== modified file 'src/Core/TAPN/InhibitorArc.cpp'
--- src/Core/TAPN/InhibitorArc.cpp	2012-04-16 10:37:52 +0000
+++ src/Core/TAPN/InhibitorArc.cpp	2013-05-15 15:27:27 +0000
@@ -4,9 +4,9 @@
 
 namespace VerifyTAPN {
 	namespace TAPN {
-		void InhibitorArc::Print(std::ostream& out) const
+		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	2012-04-16 10:22:56 +0000
+++ src/Core/TAPN/InhibitorArc.hpp	2013-05-15 15:27:27 +0000
@@ -19,12 +19,12 @@
 				virtual ~InhibitorArc() { /* empty */ }
 
 			public: // modifiers
-				inline TimedPlace& InputPlace() { return *place; }
-				inline TimedTransition& OutputTransition() { return *transition; }
+				inline TimedPlace& getInputPlace() { return *place; }
+				inline TimedTransition& getOutputTransition() { return *transition; }
 
 			public: // Inspectors
-				void Print(std::ostream& out) const;
-				inline const int GetWeight() const { return weight; }
+				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;
@@ -33,7 +33,7 @@
 
 		inline std::ostream& operator<<(std::ostream& out, const InhibitorArc& arc)
 		{
-			arc.Print(out);
+			arc.print(out);
 			return out;
 		}
 	}

=== modified file 'src/Core/TAPN/OutputArc.cpp'
--- src/Core/TAPN/OutputArc.cpp	2012-04-16 10:37:52 +0000
+++ src/Core/TAPN/OutputArc.cpp	2013-05-15 15:27:27 +0000
@@ -4,17 +4,17 @@
 
 namespace VerifyTAPN {
 	namespace TAPN {
-		void OutputArc::Print(std::ostream& out) const
+		void OutputArc::print(std::ostream& out) const
 		{
-			out << "From " << transition->GetName() << " to " << place->GetName() << " weight: " << weight;
+			out << "From " << transition->getName() << " to " << place->getName() << " weight: " << weight;
 		}
 
-		TimedPlace& OutputArc::OutputPlace()
+		TimedPlace& OutputArc::getOutputPlace()
 		{
 			return *place;
 		}
 
-		TimedTransition& OutputArc::InputTransition()
+		TimedTransition& OutputArc::getInputTransition()
 		{
 			return *transition;
 		}

=== modified file 'src/Core/TAPN/OutputArc.hpp'
--- src/Core/TAPN/OutputArc.hpp	2012-04-16 10:22:56 +0000
+++ src/Core/TAPN/OutputArc.hpp	2013-05-15 15:27:27 +0000
@@ -20,12 +20,12 @@
 			virtual ~OutputArc() { /* empty */ }
 
 		public: // modifiers
-			TimedPlace& OutputPlace();
-			TimedTransition& InputTransition();
+			TimedPlace& getOutputPlace();
+			TimedTransition& getInputTransition();
 
 		public: // inspectors
-			void Print(std::ostream& out) const;
-			inline const int GetWeight() const { return weight; }
+			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;
@@ -34,7 +34,7 @@
 
 		inline std::ostream& operator<<(std::ostream& out, const OutputArc& arc)
 		{
-			arc.Print(out);
+			arc.print(out);
 			return out;
 		}
 	}

=== removed file 'src/Core/TAPN/Pairing.cpp'
--- src/Core/TAPN/Pairing.cpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPN/Pairing.cpp	1970-01-01 00:00:00 +0000
@@ -1,74 +0,0 @@
-#include "Pairing.hpp"
-#include "../TAPN/TimedTransition.hpp"
-#include "../TAPN/TimedArcPetriNet.hpp"
-
-namespace VerifyTAPN {
-
-using namespace TAPN;
-
-	void Pairing::GeneratePairingFor(const TimedArcPetriNet& tapn, const TAPN::TimedTransition& t) {
-		TimedInputArc::WeakPtrVector preset = t.GetPreset();
-		OutputArc::WeakPtrVector postset = t.GetPostset();
-
-		unsigned int sizeOfPairing = preset.size() >= postset.size() ? preset.size() : postset.size();
-
-		int inputPlace;
-		int outputPlace;
-
-		for(unsigned int i = 0; i < sizeOfPairing; i++)
-		{
-			if(i < preset.size() && i < postset.size())
-			{
-				boost::shared_ptr<TimedInputArc> tiaPtr = preset[i].lock();
-				boost::shared_ptr<OutputArc> oaPtr = postset[i].lock();
-
-				inputPlace = tapn.GetPlaceIndex(tiaPtr->InputPlace());
-				outputPlace = tapn.GetPlaceIndex(oaPtr->OutputPlace());
-
-				Add(inputPlace, outputPlace);
-			}
-			else if(i < preset.size() && i >= postset.size()){
-				boost::shared_ptr<TimedInputArc> tiaPtr = preset[i].lock();
-
-				inputPlace = tapn.GetPlaceIndex(tiaPtr->InputPlace());
-				Add(inputPlace, TimedPlace::BottomIndex());
-			}
-			else if(i >= preset.size() && i < postset.size())
-			{
-				boost::shared_ptr<OutputArc> oaPtr = postset[i].lock();
-
-				outputPlace = tapn.GetPlaceIndex(oaPtr->OutputPlace());
-
-				Add(TimedPlace::BottomIndex(),outputPlace);
-			}
-		}
-	}
-
-	const std::list<int>& Pairing::GetOutputPlacesFor(int inputPlace) const
-	{
-		return pairing[inputPlace];
-	}
-
-	void Pairing::Add(int inputPlace, int outputPlace)
-	{
-		std::list<int>& outPlaces = pairing[inputPlace];
-
-		outPlaces.push_back(outputPlace);
-	}
-
-	void Pairing::Print(std::ostream& out) const
-	{
-		out << "( INPUT PLACE, OUTPUT PLACE )\n";
-		out << "-------------------------------\n";
-		for(HashMap::const_iterator iter = pairing.begin(); iter != pairing.end(); ++iter)
-		{
-			std::list<int> outPlaces = (*iter).second;
-			for(std::list<int>::const_iterator pIter = outPlaces.begin(); pIter != outPlaces.end(); ++pIter)
-			{
-				out << "(" << (*iter).first << ", " << (*pIter) << ")" << "\n";
-			}
-		}
-
-		out << "\n";
-	}
-}

=== removed file 'src/Core/TAPN/Pairing.hpp'
--- src/Core/TAPN/Pairing.hpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPN/Pairing.hpp	1970-01-01 00:00:00 +0000
@@ -1,44 +0,0 @@
-#ifndef PAIRING_HPP_
-#define PAIRING_HPP_
-#include "google/sparse_hash_map"
-#include "../TAPN/TimedPlace.hpp"
-#include "boost/functional/hash.hpp"
-#include <string>
-#include <list>
-
-namespace VerifyTAPN {
-	namespace TAPN {
-		class TimedTransition;
-		class TimedArcPetriNet;
-	}
-
-	class Pairing {
-		public:
-			typedef google::sparse_hash_map<int, std::list<int>, boost::hash<int> > HashMap;
-		public: // construction
-			Pairing(const TAPN::TimedArcPetriNet& tapn, const TAPN::TimedTransition& t) : pairing() { GeneratePairingFor(tapn, t); };
-			Pairing() : pairing() { };
-
-		public: // inspectors
-			const std::list<int>& GetOutputPlacesFor(int inputPlace) const;
-			inline bool IsPairingEmpty() const { return pairing.empty(); }
-			void Print(std::ostream& out) const;
-
-		private: // initializers
-			void GeneratePairingFor(const TAPN::TimedArcPetriNet& tapn, const TAPN::TimedTransition& t);
-			void Add(int inputPlace, int outputPlace);
-
-		private: // data
-			mutable HashMap pairing;
-
-	};
-
-	inline std::ostream& operator<<(std::ostream& out, const Pairing& pairing)
-	{
-		pairing.Print(out);
-		return out;
-	}
-
-}
-
-#endif /* PAIRING_HPP_ */

=== modified file 'src/Core/TAPN/TimeInterval.cpp'
--- src/Core/TAPN/TimeInterval.cpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPN/TimeInterval.cpp	2013-05-15 15:27:27 +0000
@@ -6,7 +6,7 @@
 namespace VerifyTAPN {
 	namespace TAPN {
 		using namespace boost::algorithm;
-		TimeInterval TimeInterval::CreateFor(const std::string& interval)
+		TimeInterval TimeInterval::createFor(const std::string& interval)
 		{
 			bool leftStrict = boost::algorithm::icontains(interval, "(");
 			bool rightStrict = boost::algorithm::icontains(interval,")");
@@ -30,7 +30,7 @@
 			return TimeInterval(leftStrict, lowerBound, upperBound, rightStrict);
 		}
 
-		void TimeInterval::Print(std::ostream& out) const
+		void TimeInterval::print(std::ostream& out) const
 		{
 			std::string leftParenthesis = leftStrict ? "(" : "[";
 			std::string rightParenthesis = rightStrict ? ")" : "]";

=== modified file 'src/Core/TAPN/TimeInterval.hpp'
--- src/Core/TAPN/TimeInterval.hpp	2012-06-19 09:03:00 +0000
+++ src/Core/TAPN/TimeInterval.hpp	2013-05-15 15:27:27 +0000
@@ -25,16 +25,16 @@
 			virtual ~TimeInterval() { /* empty */ }
 
 		public: // inspectors
-			void Print(std::ostream& out) const;
-			inline const int GetLowerBound() const { return lowerBound; }
-			inline const int GetUpperBound() const { return upperBound; }
-			inline const bool IsLowerBoundStrict() const { return leftStrict; }
-			inline const bool IsUpperBoundStrict() const { return rightStrict; }
+			void print(std::ostream& out) const;
+			inline const int getLowerBound() const { return lowerBound; }
+			inline const int getUpperBound() const { return upperBound; }
+			inline const bool isLowerBoundStrict() const { return leftStrict; }
+			inline const bool isUpperBoundStrict() const { return rightStrict; }
 
-			inline const bool IsZeroInfinity() const { return !leftStrict && lowerBound == 0 && upperBound == std::numeric_limits<int>().max() && rightStrict; }
+			inline const bool isZeroInfinity() const { return !leftStrict && lowerBound == 0 && upperBound == std::numeric_limits<int>().max() && rightStrict; }
 
 		public: // statics
-			static TimeInterval CreateFor(const std::string& interval);
+			static TimeInterval createFor(const std::string& interval);
 
 
 		private: // data
@@ -46,7 +46,7 @@
 
 		inline std::ostream& operator<<(std::ostream& out, const TimeInterval& interval)
 		{
-			interval.Print(out);
+			interval.print(out);
 			return out;
 		}
 	}

=== modified file 'src/Core/TAPN/TimeInvariant.cpp'
--- src/Core/TAPN/TimeInvariant.cpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPN/TimeInvariant.cpp	2013-05-15 15:27:27 +0000
@@ -6,7 +6,7 @@
 	namespace TAPN {
 		const TimeInvariant TimeInvariant::LS_INF;
 
-		TimeInvariant TimeInvariant::CreateFor(const std::string& invariant)
+		TimeInvariant TimeInvariant::createFor(const std::string& invariant)
 		{
 			bool strict = !boost::algorithm::icontains(invariant, "<=");
 			int bound = std::numeric_limits<int>().max();
@@ -23,7 +23,7 @@
 			return TimeInvariant(strict, bound);
 		}
 
-		void TimeInvariant::Print(std::ostream& out) const
+		void TimeInvariant::print(std::ostream& out) const
 		{
 			std::string comparison = strictComparison ? "<" : "<=";
 			std::string strBound = bound == std::numeric_limits<int>().max() ? "inf" : boost::lexical_cast<std::string>(bound);

=== modified file 'src/Core/TAPN/TimeInvariant.hpp'
--- src/Core/TAPN/TimeInvariant.hpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPN/TimeInvariant.hpp	2013-05-15 15:27:27 +0000
@@ -25,12 +25,12 @@
 
 			virtual ~TimeInvariant() { /* Empty */ };
 		public: // inspectors
-			void Print(std::ostream& out) const;
-			inline const int GetBound() const { return bound; }
-			inline const bool IsBoundStrict() const { return strictComparison; }
+			void print(std::ostream& out) const;
+			inline const int getBound() const { return bound; }
+			inline const bool isBoundStrict() const { return strictComparison; }
 
 		public: // statics
-			static TimeInvariant CreateFor(const std::string& invariant);
+			static TimeInvariant createFor(const std::string& invariant);
 
 		private: // data
 			bool strictComparison;
@@ -39,7 +39,7 @@
 
 		inline bool operator==(const TimeInvariant& a, const TimeInvariant& b)
 		{
-			return a.GetBound() == b.GetBound() && a.IsBoundStrict() == b.IsBoundStrict();
+			return a.getBound() == b.getBound() && a.isBoundStrict() == b.isBoundStrict();
 		}
 
 		inline bool operator!=(const TimeInvariant& a, const TimeInvariant& b)
@@ -49,7 +49,7 @@
 
 		inline std::ostream& operator<<(std::ostream& out, const TimeInvariant& invariant)
 		{
-			invariant.Print(out);
+			invariant.print(out);
 			return out;
 		}
 	}

=== modified file 'src/Core/TAPN/TimedArcPetriNet.cpp'
--- src/Core/TAPN/TimedArcPetriNet.cpp	2012-10-10 06:32:18 +0000
+++ src/Core/TAPN/TimedArcPetriNet.cpp	2013-05-15 15:27:27 +0000
@@ -5,58 +5,58 @@
 
 namespace VerifyTAPN {
 	namespace TAPN {
-		void TimedArcPetriNet::Initialize(bool useGlobalMaxConstant)
+		void TimedArcPetriNet::initialize(bool useGlobalMaxConstant)
 		{
 			for(unsigned int i = 0; i < places.size(); i++){
-				places[i]->SetIndex(i);
-				UpdateMaxConstant(places[i]->GetInvariant());
+				places[i]->setIndex(i);
+				updateMaxConstant(places[i]->getInvariant());
 			}
 
 			for(unsigned int i = 0; i < transitions.size(); i++){
-				transitions[i]->SetIndex(i);
+				transitions[i]->setIndex(i);
 			}
 
 			for(TimedInputArc::Vector::const_iterator iter = inputArcs.begin(); iter != inputArcs.end(); ++iter)
 			{
 				const boost::shared_ptr<TimedInputArc>& arc = *iter;
-				arc->OutputTransition().AddToPreset(arc);
-				arc->InputPlace().AddInputArc(arc);
-				UpdateMaxConstant(arc->Interval());
+				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->Transition().AddTransportArcGoingThrough(arc);
-				arc->Source().AddTransportArc(arc);
-				UpdateMaxConstant(arc->Interval());
+				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->OutputTransition().AddIncomingInhibitorArc(arc);
-				arc->InputPlace().AddInhibitorArc(arc);
-				arc->InputPlace().SetHasInhibitorArcs(true);
+				arc->getOutputTransition().addIncomingInhibitorArc(arc);
+				arc->getInputPlace().addInhibitorArc(arc);
+				arc->getInputPlace().setHasInhibitorArcs(true);
 			}
 
 			for(OutputArc::Vector::const_iterator iter = outputArcs.begin(); iter != outputArcs.end(); ++iter)
 			{
 				const boost::shared_ptr<OutputArc>& arc = *iter;
-				arc->InputTransition().AddToPostset(arc);
-				arc->OutputPlace().AddOutputArc(arc);
+				arc->getInputTransition().addToPostset(arc);
+				arc->getOutputPlace().addOutputArc(arc);
 			}
 
-			GeneratePairings();
-			FindMaxConstants();
+
+			findMaxConstants();
 
 			if(useGlobalMaxConstant){
 				for(TimedPlace::Vector::const_iterator place_iter = places.begin(); place_iter != places.end(); ++place_iter)
 				{
-					(*place_iter)->SetMaxConstant(MaxConstant()==0? -1:MaxConstant());
+					(*place_iter)->setMaxConstant(getMaxConstant()==0? -1:getMaxConstant());
 				}
 			}
 
-			MarkUntimedPlaces();
+			markUntimedPlaces();
 		}
 
 		void TimedArcPetriNet::removeOrphantedTransitions(){
@@ -69,7 +69,7 @@
 				TimedTransition::Vector::iterator iter = transitions.begin();
 				while(iter != transitions.end())
 				{
-					if((*iter)->GetPresetSize() == 0 && (*iter)->GetPostsetSize() == 0){
+					if((*iter)->getPresetSize() == 0 && (*iter)->getPostsetSize() == 0){
 						iter = transitions.erase(iter);
 						if(!hasShownMessage){
 							std::cout << "Orphaned transitions have been removed." << std::endl << std::endl;
@@ -82,98 +82,98 @@
 			}
 		}
 
-		void TimedArcPetriNet::MarkUntimedPlaces()
+		void TimedArcPetriNet::markUntimedPlaces()
 		{
 			for(TimedPlace::Vector::const_iterator iter = places.begin(); iter != places.end(); ++iter)
 			{
-				bool isUntimedPlace = (*iter)->GetInvariant() == TimeInvariant::LS_INF;
+				bool isUntimedPlace = (*iter)->getInvariant() == TimeInvariant::LS_INF;
 
 				for(TransportArc::Vector::const_iterator arcIter = transportArcs.begin(); arcIter != transportArcs.end(); ++arcIter)
 				{
-					isUntimedPlace = isUntimedPlace && (*arcIter)->Source() != **iter;
+					isUntimedPlace = isUntimedPlace && (*arcIter)->getSource() != **iter;
 				}
 
 				if(isUntimedPlace)
 				{
 					for(TimedInputArc::Vector::const_iterator arcIter = inputArcs.begin(); arcIter != inputArcs.end(); ++arcIter)
 					{
-						if((*arcIter)->InputPlace() == **iter)
+						if((*arcIter)->getInputPlace() == **iter)
 						{
-							isUntimedPlace = isUntimedPlace && (*arcIter)->Interval().IsZeroInfinity();
+							isUntimedPlace = isUntimedPlace && (*arcIter)->getInterval().isZeroInfinity();
 						}
 					}
 				}
 
-				if(isUntimedPlace) (*iter)->MarkPlaceAsUntimed();
+				if(isUntimedPlace) (*iter)->markPlaceAsUntimed();
 			}
 		}
 
-		void TimedArcPetriNet::FindMaxConstants()
+		void TimedArcPetriNet::findMaxConstants()
 		{
 			for(TimedPlace::Vector::const_iterator iter = places.begin(); iter != places.end(); ++iter)
 			{
 				int maxConstant = -1;
-				if((*iter)->GetInvariant() != TimeInvariant::LS_INF){
-					maxConstant = (*iter)->GetInvariant().GetBound();
-					(*iter)->SetMaxConstant(maxConstant);
-					(*iter)->SetType(Inv);
+				if((*iter)->getInvariant() != TimeInvariant::LS_INF){
+					maxConstant = (*iter)->getInvariant().getBound();
+					(*iter)->setMaxConstant(maxConstant);
+					(*iter)->setType(Inv);
 				}
 				else {
-					(*iter)->SetType(Dead);
+					(*iter)->setType(Dead);
 					for(TimedInputArc::Vector::const_iterator arcIter = inputArcs.begin(); arcIter != inputArcs.end(); ++arcIter)
 					{
-						if((*arcIter)->InputPlace() == **iter)
+						if((*arcIter)->getInputPlace() == **iter)
 						{
 							boost::shared_ptr<TimedInputArc> ia = *arcIter;
-							const TAPN::TimeInterval& interval = ia->Interval();
+							const TAPN::TimeInterval& interval = ia->getInterval();
 
-							const int lowerBound = interval.GetLowerBound();
-							const int upperBound = interval.GetUpperBound();
+							const int lowerBound = interval.getLowerBound();
+							const int upperBound = interval.getUpperBound();
 
 							if(upperBound != std::numeric_limits<int>().max() || lowerBound != 0){
 								if(upperBound == std::numeric_limits<int>().max()){
 									maxConstant = (maxConstant < lowerBound ? lowerBound : maxConstant);
-									(*iter)->SetType(Std);
+									(*iter)->setType(Std);
 								} else {
 									maxConstant = (maxConstant < upperBound ? upperBound : maxConstant);
 								}
 							} else {
-								(*iter)->SetType(Std);
+								(*iter)->setType(Std);
 							}
 						}
 					}
 					for(TransportArc::Vector::const_iterator transport_iter = transportArcs.begin(); transport_iter != transportArcs.end(); transport_iter++)
 					{
-						if((*transport_iter)->Source() == **iter)
+						if((*transport_iter)->getSource() == **iter)
 						{
 							int maxArc = -1;
 							boost::shared_ptr<TransportArc> ta = *transport_iter;
-							const TAPN::TimeInterval& interval = ta->Interval();
-							const int lowerBound = interval.GetLowerBound();
-							const int upperBound = interval.GetUpperBound();
+							const TAPN::TimeInterval& interval = ta->getInterval();
+							const int lowerBound = interval.getLowerBound();
+							const int upperBound = interval.getUpperBound();
 
 							if(upperBound != std::numeric_limits<int>().max() || lowerBound != 0){
 								if(upperBound == std::numeric_limits<int>().max()){
 									maxArc = lowerBound;
-									(*iter)->SetType(Std);
+									(*iter)->setType(Std);
 								} else {
 									maxArc = upperBound;
 								}
 							} else {
-								(*iter)->SetType(Std);
+								(*iter)->setType(Std);
 							}
-							int destinationInvariant = ta->Destination().GetInvariant().GetBound();
+							int destinationInvariant = ta->getDestination().getInvariant().getBound();
 							if(destinationInvariant != std::numeric_limits<int>().max()){
 								maxArc = maxArc < destinationInvariant ? maxArc : destinationInvariant;
 							}
 							maxConstant = maxConstant < maxArc ? maxArc : maxConstant;
 						}
 					}
-					(*iter)->SetMaxConstant(maxConstant);
+					(*iter)->setMaxConstant(maxConstant);
 
 					for(InhibitorArc::Vector::const_iterator inhib_iter = inhibitorArcs.begin(); inhib_iter != inhibitorArcs.end(); inhib_iter++){
-						if((*inhib_iter)->InputPlace().GetIndex() == (*iter)->GetIndex() && (*iter)->GetType() == Dead){
-							(*iter)->SetType(Std);
+						if((*inhib_iter)->getInputPlace().getIndex() == (*iter)->getIndex() && (*iter)->getType() == Dead){
+							(*iter)->setType(Std);
 						}
 					}
 				}
@@ -184,15 +184,15 @@
 				std::vector< TimedPlace* > causalitySet;
 				calculateCausality(**place_iter, &causalitySet);
 				for(std::vector< TimedPlace* >::const_iterator cau_iter = causalitySet.begin(); cau_iter != causalitySet.end(); cau_iter++){
-					if((*cau_iter)->GetMaxConstant() > (*place_iter)->GetMaxConstant()){
-						(*place_iter)->SetMaxConstant((*cau_iter)->GetMaxConstant());
+					if((*cau_iter)->getMaxConstant() > (*place_iter)->getMaxConstant()){
+						(*place_iter)->setMaxConstant((*cau_iter)->getMaxConstant());
 					}
 				}
 			}
 
 			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()->OutputPlace().GetMaxConstant() > -1){
+				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);
 						break;
 					}
@@ -206,10 +206,10 @@
 				if(**iter == p) return;
 			}
 			result->push_back(&p);
-			for(TransportArc::Vector::const_iterator iter = this->GetTransportArcs().begin(); iter != this->GetTransportArcs().end(); iter++){
-				if((*iter)->Source() == p){
-					if((*iter)->Interval().GetUpperBound() == std::numeric_limits<int>().max()){
-						calculateCausality((*iter)->Destination(), result);
+			for(TransportArc::Vector::const_iterator iter = this->getTransportArcs().begin(); iter != this->getTransportArcs().end(); iter++){
+				if((*iter)->getSource() == p){
+					if((*iter)->getInterval().getUpperBound() == std::numeric_limits<int>().max()){
+						calculateCausality((*iter)->getDestination(), result);
 					}
 				}
 			}
@@ -219,27 +219,27 @@
 			std::vector< int > placeNumbers;
 			boost::any context = placeNumbers;
 			DiscreteVerification::PlaceVisitor visitor;
-			query->Accept(visitor, context);
+			query->accept(visitor, context);
 			placeNumbers = boost::any_cast< std::vector< int > >(context);
 
 			for(TimedPlace::Vector::const_iterator iter = places.begin(); iter != places.end(); ++iter){
-				if(options.GetKeepDeadTokens() && (*iter)->GetType() == Dead){
-					(*iter)->SetType(Std);
+				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++){
-					if((*id_iter) == (*iter)->GetIndex() && (*iter)->GetType() == Dead){
-						(*iter)->SetType(Std);
+					if((*id_iter) == (*iter)->getIndex() && (*iter)->getType() == Dead){
+						(*iter)->setType(Std);
 						break;
 					}
 				}
 			}
 		}
 
-		void TimedArcPetriNet::UpdateMaxConstant(const TimeInterval& interval)
+		void TimedArcPetriNet::updateMaxConstant(const TimeInterval& interval)
 		{
-			int lowerBound = interval.GetLowerBound();
-			int upperBound = interval.GetUpperBound();
+			int lowerBound = interval.getLowerBound();
+			int upperBound = interval.getUpperBound();
 			if(lowerBound < std::numeric_limits<int>().max() && lowerBound > maxConstant)
 			{
 				maxConstant = lowerBound;
@@ -250,21 +250,21 @@
 			}
 		}
 
-		void TimedArcPetriNet::UpdateMaxConstant(const TimeInvariant& invariant)
+		void TimedArcPetriNet::updateMaxConstant(const TimeInvariant& invariant)
 		{
-			int bound = invariant.GetBound();
+			int bound = invariant.getBound();
 			if(bound < std::numeric_limits<int>().max() && bound > maxConstant)
 			{
 				maxConstant = bound;
 			}
 		}
 
-		int TimedArcPetriNet::GetPlaceIndex(const std::string& placeName) const
+		int TimedArcPetriNet::getPlaceIndex(const std::string& placeName) const
 		{
 				int idx = TimedPlace::BottomIndex();
 				for(unsigned int i = 0; i < places.size(); ++i)
 				{
-					if(places[i]->GetName() == placeName)
+					if(places[i]->getName() == placeName)
 					{
 						idx = i;
 						break;
@@ -274,7 +274,7 @@
 				return idx;
 		}
 
-		void TimedArcPetriNet::Print(std::ostream & out) const
+		void TimedArcPetriNet::print(std::ostream & out) const
 		{
 			out << "TAPN:" << std::endl << "  Places: ";
 			for(TimedPlace::Vector::const_iterator iter = places.begin();iter != places.end();iter++)
@@ -326,22 +326,11 @@
 			out << std::endl;
 		}
 
-
-		void TimedArcPetriNet::GeneratePairings()
-		{
-			for(TimedTransition::Vector::const_iterator iter = transitions.begin(); iter != transitions.end(); ++iter)
-			{
-				const TimedTransition& t = *(*iter);
-				Pairing p(*this, t);
-				pairings.insert(std::pair<TimedTransition, Pairing>(t, p));
-			}
-		}
-
-		bool TimedArcPetriNet::IsNonStrict() const{
+		bool TimedArcPetriNet::isNonStrict() const{
 
 			for(TimedInputArc::Vector::const_iterator iter = inputArcs.begin(); iter != inputArcs.end(); iter++){
 				TimedInputArc& ia = *(*iter);
-				if(ia.Interval().IsLowerBoundStrict() || (ia.Interval().IsUpperBoundStrict() && ia.Interval().GetUpperBound() != std::numeric_limits<int>().max())){
+				if(ia.getInterval().isLowerBoundStrict() || (ia.getInterval().isUpperBoundStrict() && ia.getInterval().getUpperBound() != std::numeric_limits<int>().max())){
 					return false;
 				}
 			}
@@ -349,14 +338,14 @@
 
 			for(TransportArc::Vector::const_iterator iter = transportArcs.begin(); iter != transportArcs.end(); iter++){
 				TransportArc& ta = *(*iter);
-				if(ta.Interval().IsLowerBoundStrict() || (ta.Interval().IsUpperBoundStrict() && ta.Interval().GetUpperBound() != std::numeric_limits<int>().max())){
+				if(ta.getInterval().isLowerBoundStrict() || (ta.getInterval().isUpperBoundStrict() && ta.getInterval().getUpperBound() != std::numeric_limits<int>().max())){
 					return false;
 				}
 			}
 
 			for(TimedPlace::Vector::const_iterator iter = places.begin(); iter != places.end(); iter++){
 				const TimedPlace& p = *(*iter);
-				if(p.GetInvariant().IsBoundStrict() && p.GetInvariant().GetBound() != std::numeric_limits<int>().max()){
+				if(p.getInvariant().isBoundStrict() && p.getInvariant().getBound() != std::numeric_limits<int>().max()){
 					return false;
 				}
 			}

=== modified file 'src/Core/TAPN/TimedArcPetriNet.hpp'
--- src/Core/TAPN/TimedArcPetriNet.hpp	2012-07-12 15:47:35 +0000
+++ src/Core/TAPN/TimedArcPetriNet.hpp	2013-05-15 15:27:27 +0000
@@ -11,7 +11,6 @@
 #include "boost/make_shared.hpp"
 #include "google/sparse_hash_map"
 #include "boost/functional/hash.hpp"
-#include "Pairing.hpp"
 #include "../QueryParser/AST.hpp"
 #include "../../DiscreteVerification/PlaceVisitor.hpp"
 #include "../VerificationOptions.hpp"
@@ -22,8 +21,7 @@
 
 		class TimedArcPetriNet
 		{
-		public: // typedefs
-			typedef google::sparse_hash_map<TimedTransition, VerifyTAPN::Pairing, boost::hash<TAPN::TimedTransition> > HashMap;
+
 		public:// construction
 			TimedArcPetriNet(const TimedPlace::Vector& places,
 				const TimedTransition::Vector& transitions,
@@ -35,37 +33,35 @@
 			virtual ~TimedArcPetriNet() { /* empty */ }
 
 		public: // inspectors
-			void Print(std::ostream& out) const;
-			inline int GetPlaceIndex(const TimedPlace& p) const { return p.GetIndex(); };
-			int GetPlaceIndex(const std::string& placeName) const;
-			const TimedPlace& GetPlace(const int placeIndex) const { return *places[placeIndex]; }
-			const TimedTransition::Vector& GetTransitions() const { return transitions; }
-			const TimedInputArc::Vector& GetInputArcs() const { return inputArcs; }
-			const TransportArc::Vector& GetTransportArcs() const { return transportArcs; }
-			const InhibitorArc::Vector& GetInhibitorArcs() const { return inhibitorArcs; }
-			const TimedPlace::Vector& GetPlaces() const { return places; };
-			const int GetNumberOfConsumingArcs() const { return inputArcs.size() + transportArcs.size(); }
-			const OutputArc::Vector& GetOutputArcs() const { return outputArcs; }
-			const int GetNumberOfOutputArcs() const { return outputArcs.size(); }
-			int NumberOfPlaces() const { return places.size(); };
-			const Pairing& GetPairing(const TimedTransition& t) const { return pairings.find(t)->second; }
-			inline int MaxConstant() const { return maxConstant; };
-			inline const bool IsPlaceUntimed(int index) const { return places[index]->IsUntimed(); }
-			bool IsNonStrict() const;
+			void print(std::ostream& out) const;
+			inline int getPlaceIndex(const TimedPlace& p) const { return p.getIndex(); };
+			int getPlaceIndex(const std::string& placeName) const;
+			const TimedPlace& getPlace(const int placeIndex) const { return *places[placeIndex]; }
+			const TimedTransition::Vector& getTransitions() const { return transitions; }
+			const TimedInputArc::Vector& getInputArcs() const { return inputArcs; }
+			const TransportArc::Vector& getTransportArcs() const { return transportArcs; }
+			const InhibitorArc::Vector& getInhibitorArcs() const { return inhibitorArcs; }
+			const TimedPlace::Vector& getPlaces() const { return places; };
+			const int getNumberOfConsumingArcs() const { return inputArcs.size() + transportArcs.size(); }
+			const OutputArc::Vector& getOutputArcs() const { return outputArcs; }
+			const int getNumberOfOutputArcs() const { return outputArcs.size(); }
+			int getNumberOfPlaces() const { return places.size(); };
+			inline int getMaxConstant() const { return maxConstant; };
+			inline const bool isPlaceAtIndexUntimed(int index) const { return places[index]->isUntimed(); }
+			bool isNonStrict() const;
 			void calculateCausality(TimedPlace& p, std::vector< TimedPlace* >* result) const;
 			void updatePlaceTypes(const AST::Query* query, VerificationOptions options);
 		public: // modifiers
-			void Initialize(bool useGlobalMaxConstant);
+			void initialize(bool useGlobalMaxConstant);
 			void removeOrphantedTransitions();
 
 
 		private: // modifiers
-			void MakeTAPNConservative();
-			void GeneratePairings();
-			void UpdateMaxConstant(const TimeInterval& interval);
-			void UpdateMaxConstant(const TimeInvariant& invariant);
-			void MarkUntimedPlaces();
-			void FindMaxConstants();
+			void makeTAPNConservative();
+			void updateMaxConstant(const TimeInterval& interval);
+			void updateMaxConstant(const TimeInvariant& invariant);
+			void markUntimedPlaces();
+			void findMaxConstants();
 
 		private: // data
 			const TimedPlace::Vector places;
@@ -74,20 +70,19 @@
 			const OutputArc::Vector outputArcs;
 			const TransportArc::Vector transportArcs;
 			const InhibitorArc::Vector inhibitorArcs;
-			mutable HashMap pairings;
 			int maxConstant;
 		};
 
 		inline std::ostream& operator<<(std::ostream& out, const VerifyTAPN::TAPN::TimedArcPetriNet& tapn)
 		{
-			tapn.Print( out );
+			tapn.print( out );
 			return out;
 		}
 
-		inline std::size_t hash_value(const TimedTransition& transition)
+		inline std::size_t getHashValue(const TimedTransition& transition)
 		{
 			boost::hash<std::string> hasher;
-			return hasher(transition.GetName());
+			return hasher(transition.getName());
 		}
 	}
 }

=== modified file 'src/Core/TAPN/TimedInputArc.cpp'
--- src/Core/TAPN/TimedInputArc.cpp	2012-04-16 10:37:52 +0000
+++ src/Core/TAPN/TimedInputArc.cpp	2013-05-15 15:27:27 +0000
@@ -4,9 +4,9 @@
 
 namespace VerifyTAPN {
 	namespace TAPN {
-		void TimedInputArc::Print(std::ostream& out) const
+		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	2012-04-16 10:22:56 +0000
+++ src/Core/TAPN/TimedInputArc.hpp	2013-05-15 15:27:27 +0000
@@ -21,13 +21,13 @@
 			virtual ~TimedInputArc() { /* empty */}
 
 		public: // modifiers
-			inline TimedPlace& InputPlace() { return *place; }
-			inline TimedTransition& OutputTransition() { return *transition; }
-			inline const TimeInterval& Interval() { return interval; }
+			inline TimedPlace& getInputPlace() { return *place; }
+			inline TimedTransition& getOutputTransition() { return *transition; }
+			inline const TimeInterval& getInterval() { return interval; }
 
 		public: // Inspectors
-			void Print(std::ostream& out) const;
-			inline const int GetWeight() const { return weight; }
+			void print(std::ostream& out) const;
+			inline const int getWeight() const { return weight; }
 		private:
 			const TimeInterval interval;
 			const boost::shared_ptr<TimedPlace> place;
@@ -37,7 +37,7 @@
 
 		inline std::ostream& operator<<(std::ostream& out, const TimedInputArc& arc)
 		{
-			arc.Print(out);
+			arc.print(out);
 			return out;
 		}
 	}

=== modified file 'src/Core/TAPN/TimedPlace.cpp'
--- src/Core/TAPN/TimedPlace.cpp	2012-04-11 11:13:01 +0000
+++ src/Core/TAPN/TimedPlace.cpp	2013-05-15 15:27:27 +0000
@@ -5,19 +5,19 @@
 
 		const std::string TimedPlace::BOTTOM_NAME = "*BOTTOM*";
 
-		const std::string& TimedPlace::GetName() const
+		const std::string& TimedPlace::getName() const
 		{
 			return name;
 		}
 
-		const std::string& TimedPlace::GetId() const
+		const std::string& TimedPlace::getId() const
 		{
 			return id;
 		}
 
-		void TimedPlace::Print(std::ostream& out) const
+		void TimedPlace::print(std::ostream& out) const
 		{
-			out << "(" << name << " (index: " << index << "), " << timeInvariant << ", Max Constant: " << maxConstant << ", Infinity Place: " << (isUntimed ? "true" : "false") << ", Type: " << (type == Std ? "Std" : (type == Inv ? "Inv" : "Dead")) << ")";
+			out << "(" << name << " (index: " << index << "), " << timeInvariant << ", Max Constant: " << maxConstant << ", Infinity Place: " << (untimed ? "true" : "false") << ", Type: " << (type == Std ? "Std" : (type == Inv ? "Inv" : "Dead")) << ")";
 		}
 	}
 }

=== modified file 'src/Core/TAPN/TimedPlace.hpp'
--- src/Core/TAPN/TimedPlace.hpp	2012-04-25 13:02:36 +0000
+++ src/Core/TAPN/TimedPlace.hpp	2013-05-15 15:27:27 +0000
@@ -36,33 +36,33 @@
 
 		public: // construction / destruction
 			TimedPlace(const std::string& name, const std::string& id, const TimeInvariant timeInvariant)
-			: name(name), id(id), timeInvariant(timeInvariant), index(-2), isUntimed(false), maxConstant(0), hasInhibitorArcs(false), inputArcs(), transportArcs(), inhibitorArcs()  { };
-			TimedPlace() : name(BOTTOM_NAME), timeInvariant(), index(BottomIndex()), isUntimed(false), maxConstant(0), hasInhibitorArcs(false), inputArcs(), transportArcs(), inhibitorArcs(){ };
+			: name(name), id(id), timeInvariant(timeInvariant), index(-2), untimed(false), maxConstant(0), containsInhibitorArcs(false), inputArcs(), transportArcs(), inhibitorArcs()  { };
+			TimedPlace() : name(BOTTOM_NAME), timeInvariant(), index(BottomIndex()), untimed(false), maxConstant(0), containsInhibitorArcs(false), inputArcs(), transportArcs(), inhibitorArcs(){ };
 			virtual ~TimedPlace() { /* empty */ };
 
 		public: // modifiers
-			inline void MarkPlaceAsUntimed() { isUntimed = true; }
-			inline void SetIndex(int i) { index = i; };
-			inline void SetMaxConstant(int max) { maxConstant = max; }
-			inline void SetHasInhibitorArcs(bool inhibitorArcs) { hasInhibitorArcs = 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 SetType(PlaceType type){ this->type = type; }
+			inline void markPlaceAsUntimed() { untimed = true; }
+			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 setType(PlaceType type){ this->type = type; }
 		public: // inspection
-			inline const PlaceType GetType() const { return type; }
-			const std::string& GetName() const;
-			const std::string& GetId() const;
-			void Print(std::ostream& out) const;
-			inline int GetIndex() const { return index; };
-			inline const bool IsUntimed() const { return isUntimed; }
-			inline const int GetMaxConstant() const { return maxConstant; }
-			inline const TAPN::TimeInvariant& GetInvariant() const { return timeInvariant; };
-			inline bool HasInhibitorArcs() const { return hasInhibitorArcs; };
-			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 PlaceType getType() const { return type; }
+			const std::string& getName() const;
+			const std::string& getId() const;
+			void print(std::ostream& out) const;
+			inline int getIndex() const { return index; };
+			inline const bool isUntimed() const { return untimed; }
+			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; }
 
 		private: // data
 			PlaceType type;
@@ -70,9 +70,9 @@
 			std::string id;
 			TimeInvariant timeInvariant;
 			int index;
-			bool isUntimed;
+			bool untimed;
 			int maxConstant;
-			bool hasInhibitorArcs;
+			bool containsInhibitorArcs;
 			TimedInputArc::WeakPtrVector inputArcs;
 			TransportArc::WeakPtrVector transportArcs;
 			InhibitorArc::WeakPtrVector inhibitorArcs;
@@ -81,7 +81,7 @@
 
 		inline std::ostream& operator<<(std::ostream& out, const TimedPlace& place)
 		{
-			place.Print(out);
+			place.print(out);
 			return out;
 		}
 
@@ -89,12 +89,12 @@
 		// thus it is enough to use the name to determine equality.
 		inline bool operator==(TimedPlace const& a, TimedPlace const& b)
 		{
-			return a.GetName() == b.GetName();
+			return a.getName() == b.getName();
 		}
 
 		inline bool operator!=(TimedPlace const& a, TimedPlace const& b)
 		{
-			return !(a.GetName() == b.GetName());
+			return !(a.getName() == b.getName());
 		}
 	}
 }

=== modified file 'src/Core/TAPN/TimedTransition.cpp'
--- src/Core/TAPN/TimedTransition.cpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPN/TimedTransition.cpp	2013-05-15 15:27:27 +0000
@@ -2,12 +2,12 @@
 
 namespace VerifyTAPN {
 	namespace TAPN {
-		void TimedTransition::Print(std::ostream& out) const
+		void TimedTransition::print(std::ostream& out) const
 		{
-			out << GetName() << "(" << index << ")";
+			out << getName() << "(" << index << ")";
 		}
 
-		void TimedTransition::AddToPreset(const boost::shared_ptr<TimedInputArc>& arc)
+		void TimedTransition::addToPreset(const boost::shared_ptr<TimedInputArc>& arc)
 		{
 			if(arc)
 			{
@@ -15,7 +15,7 @@
 			}
 		}
 
-		void TimedTransition::AddTransportArcGoingThrough(const boost::shared_ptr<TransportArc>& arc)
+		void TimedTransition::addTransportArcGoingThrough(const boost::shared_ptr<TransportArc>& arc)
 		{
 			if(arc)
 			{
@@ -23,7 +23,7 @@
 			}
 		}
 
-		void TimedTransition::AddIncomingInhibitorArc(const boost::shared_ptr<InhibitorArc>& arc)
+		void TimedTransition::addIncomingInhibitorArc(const boost::shared_ptr<InhibitorArc>& arc)
 		{
 			if(arc)
 			{
@@ -31,7 +31,7 @@
 			}
 		}
 
-		void TimedTransition::AddToPostset(const boost::shared_ptr<OutputArc>& arc)
+		void TimedTransition::addToPostset(const boost::shared_ptr<OutputArc>& arc)
 		{
 			if(arc)
 			{

=== modified file 'src/Core/TAPN/TimedTransition.hpp'
--- src/Core/TAPN/TimedTransition.hpp	2012-10-10 06:32:18 +0000
+++ src/Core/TAPN/TimedTransition.hpp	2013-05-15 15:27:27 +0000
@@ -26,27 +26,27 @@
 			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(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);
 
-			inline void SetIndex(int i) { index = i; };
+			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 const unsigned int GetPresetSize() const { return NumberOfInputArcs() + NumberOfTransportArcs(); }
-			inline const OutputArc::WeakPtrVector& GetPostset() const { return postset; }
-			inline const unsigned int GetPostsetSize() const { return postset.size() + transportArcs.size(); }
-			inline unsigned int NumberOfInputArcs() const { return preset.size(); };
-			inline unsigned int NumberOfTransportArcs() const { return transportArcs.size(); };
-		//	bool isEnabledBy(const TimedArcPetriNet& tapn, const VerifyTAPN::SymMarking& marking) const;
+			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 const unsigned int getPresetSize() const { return getNumberOfInputArcs() + getNumberOfTransportArcs(); }
+			inline const OutputArc::WeakPtrVector& 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 bool isConservative() const { return preset.size() == postset.size(); }
-			inline unsigned int GetIndex() const { return index; }
+			inline unsigned int getIndex() const { return index; }
 			inline const bool hasUntimedPostset() const { return untimedPostset; }
 			inline void setUntimedPostset(bool untimed){ untimedPostset = untimed; }
 
@@ -63,7 +63,7 @@
 
 		inline std::ostream& operator<<(std::ostream& out, const TimedTransition& transition)
 		{
-			transition.Print(out);
+			transition.print(out);
 			return out;
 		}
 
@@ -71,7 +71,7 @@
 		// thus it is enough to use the name to determine equality.
 		inline bool operator==(TimedTransition const& a, TimedTransition const& b)
 		{
-			return a.GetName() == b.GetName();
+			return a.getName() == b.getName();
 		}
 	}
 }

=== modified file 'src/Core/TAPN/TransportArc.cpp'
--- src/Core/TAPN/TransportArc.cpp	2012-04-16 10:37:52 +0000
+++ src/Core/TAPN/TransportArc.cpp	2013-05-15 15:27:27 +0000
@@ -6,9 +6,9 @@
 {
 	namespace TAPN
 	{
-		void TransportArc::Print(std::ostream& out) const
+		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	2012-04-16 10:22:56 +0000
+++ src/Core/TAPN/TransportArc.hpp	2013-05-15 15:27:27 +0000
@@ -28,14 +28,14 @@
 
 			virtual ~TransportArc() {};
 		public:
-			inline TimedPlace& Source() { return *source; }
-			inline TimedTransition& Transition() { return *transition; }
-			inline TimedPlace& Destination() { return *destination; }
-			inline const TimeInterval& Interval() { return interval; }
+			inline TimedPlace& getSource() { return *source; }
+			inline TimedTransition& getTransition() { return *transition; }
+			inline TimedPlace& getDestination() { return *destination; }
+			inline const TimeInterval& getInterval() { return interval; }
 
 		public: // Inspectors
-				void Print(std::ostream& out) const;
-				inline const int GetWeight() const { return weight; }
+				void print(std::ostream& out) const;
+				inline const int getWeight() const { return weight; }
 		private:
 			const TAPN::TimeInterval interval;
 			const boost::shared_ptr<TimedPlace> source;
@@ -46,7 +46,7 @@
 
 		inline std::ostream& operator<<(std::ostream& out, const TransportArc& arc)
 		{
-			arc.Print(out);
+			arc.print(out);
 			return out;
 		}
 	}

=== modified file 'src/Core/TAPNParser/TAPNXmlParser.cpp'
--- src/Core/TAPNParser/TAPNXmlParser.cpp	2012-07-02 06:52:57 +0000
+++ src/Core/TAPNParser/TAPNXmlParser.cpp	2013-05-15 15:27:27 +0000
@@ -9,9 +9,9 @@
 namespace VerifyTAPN {
 using namespace rapidxml;
 
-boost::shared_ptr<TimedArcPetriNet> TAPNXmlParser::Parse(const std::string & filename) const
+boost::shared_ptr<TimedArcPetriNet> TAPNXmlParser::parse(const std::string & filename) const
 {
-	const std::string contents = VerifyTAPN::ReadFile(filename);
+	const std::string contents = VerifyTAPN::readFile(filename);
 	std::vector<char> charArray(contents.begin(), contents.end());
 	charArray.push_back('\0');
 
@@ -24,12 +24,12 @@
 	xml_node<>* root = pnml->first_node("net");
 	if(root == 0) throw std::string("invalid file.");
 
-	return ParseTAPN(*root);
+	return parseTAPN(*root);
 }
 
-std::vector<int> TAPNXmlParser::ParseMarking(const std::string & filename, const TimedArcPetriNet& tapn) const
+std::vector<int> TAPNXmlParser::parseMarking(const std::string & filename, const TimedArcPetriNet& tapn) const
 {
-	const std::string contents = VerifyTAPN::ReadFile(filename); // not sure if this is a good idea, because it copies to string? Maybe the compiler is smart enough not to make a copy
+	const std::string contents = VerifyTAPN::readFile(filename); // not sure if this is a good idea, because it copies to string? Maybe the compiler is smart enough not to make a copy
 	std::vector<char> charArray(contents.begin(), contents.end());
 	charArray.push_back('\0');
 
@@ -38,28 +38,28 @@
 
 	xml_node<>* pnml = xmldoc.first_node("pnml"); // we don't need error handling here, since we are parsing the same file as above
 	xml_node<>* root = pnml->first_node("net");
-	return ParseInitialMarking(*root, tapn);
+	return parseInitialMarking(*root, tapn);
 }
 
-boost::shared_ptr<TimedArcPetriNet> TAPNXmlParser::ParseTAPN(const xml_node<>& root) const
+boost::shared_ptr<TimedArcPetriNet> TAPNXmlParser::parseTAPN(const xml_node<>& root) const
 {
-	TimedPlace::Vector places = ParsePlaces(root);
-	TimedTransition::Vector transitions = ParseTransitions(root);
+	TimedPlace::Vector places = parsePlaces(root);
+	TimedTransition::Vector transitions = parseTransitions(root);
 
-	TAPNXmlParser::ArcCollections arcs = ParseArcs(root, places, transitions);
+	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);
 
 	return tapn;
 }
 
-TimedPlace::Vector TAPNXmlParser::ParsePlaces(const xml_node<>& root) const
+TimedPlace::Vector TAPNXmlParser::parsePlaces(const xml_node<>& root) const
 {
 	TimedPlace::Vector places;
 
 	xml_node<>* placeNode = root.first_node("place");
 	while(placeNode != NULL){
-		boost::shared_ptr<TimedPlace> place = ParsePlace(*placeNode);
+		boost::shared_ptr<TimedPlace> place = parsePlace(*placeNode);
 		places.push_back(place);
 		placeNode = placeNode->next_sibling("place");
 	}
@@ -67,23 +67,23 @@
 	return places;
 }
 
-boost::shared_ptr<TimedPlace> TAPNXmlParser::ParsePlace(const xml_node<>& placeNode) const
+boost::shared_ptr<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);
+	TimeInvariant timeInvariant = TimeInvariant::createFor(invariantNode);
 	return boost::make_shared<TimedPlace>(name, id, timeInvariant);
 }
 
-TimedTransition::Vector TAPNXmlParser::ParseTransitions(const xml_node<>& root) const
+TimedTransition::Vector TAPNXmlParser::parseTransitions(const xml_node<>& root) const
 {
 	TimedTransition::Vector transitions;
 
 	xml_node<>* transitionNode = root.first_node("transition");
 	while(transitionNode != NULL){
-		boost::shared_ptr<TimedTransition> transition = ParseTransition(*transitionNode);
+		boost::shared_ptr<TimedTransition> transition = parseTransition(*transitionNode);
 		transitions.push_back(transition);
 		transitionNode = transitionNode->next_sibling("transition");
 	}
@@ -91,71 +91,71 @@
 	return transitions;
 }
 
-boost::shared_ptr<TimedTransition> TAPNXmlParser::ParseTransition(const xml_node<>& transitionNode) const
+boost::shared_ptr<TimedTransition> TAPNXmlParser::parseTransition(const xml_node<>& transitionNode) const
 {
 	std::string id(transitionNode.first_attribute("id")->value());
 	std::string name(transitionNode.first_attribute("name")->value());
 	return boost::make_shared<TimedTransition>(name, id);
 }
 
-TAPNXmlParser::ArcCollections TAPNXmlParser::ParseArcs(const xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+TAPNXmlParser::ArcCollections TAPNXmlParser::parseArcs(const xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
 {
 
-	TimedInputArc::Vector inputArcs = ParseInputArcs(root, places, transitions);
-	TransportArc::Vector transportArcs = ParseTransportArcs(root, places, transitions);
-	InhibitorArc::Vector inhibitorArcs = ParseInhibitorArcs(root,places,transitions);
-	OutputArc::Vector outputArcs = ParseOutputArcs(root, places, transitions);
+	TimedInputArc::Vector inputArcs = parseInputArcs(root, places, transitions);
+	TransportArc::Vector transportArcs = parseTransportArcs(root, places, transitions);
+	InhibitorArc::Vector inhibitorArcs = parseInhibitorArcs(root,places,transitions);
+	OutputArc::Vector outputArcs = parseOutputArcs(root, places, transitions);
 
 	return ArcCollections(inputArcs, outputArcs, transportArcs, inhibitorArcs);
 }
 
-TransportArc::Vector TAPNXmlParser::ParseTransportArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+TransportArc::Vector TAPNXmlParser::parseTransportArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
 {
 	TransportArc::Vector transportArcs;
 	xml_node<>* arcNode = root.first_node("transportArc");
 	while(arcNode != NULL){
-		transportArcs.push_back(ParseTransportArc(*arcNode, places, transitions));
+		transportArcs.push_back(parseTransportArc(*arcNode, places, transitions));
 		arcNode = arcNode->next_sibling("transportArc");
 	}
 	return transportArcs;
 }
 
-InhibitorArc::Vector TAPNXmlParser::ParseInhibitorArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+InhibitorArc::Vector TAPNXmlParser::parseInhibitorArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
 {
 	InhibitorArc::Vector inhibitorArcs;
 	xml_node<>* arcNode = root.first_node("inhibitorArc");
 	while(arcNode != NULL){
-		inhibitorArcs.push_back(ParseInhibitorArc(*arcNode, places, transitions));
+		inhibitorArcs.push_back(parseInhibitorArc(*arcNode, places, transitions));
 		arcNode = arcNode->next_sibling("inhibitorArc");
 	}
 	return inhibitorArcs;
 }
 
-TimedInputArc::Vector TAPNXmlParser::ParseInputArcs(const xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+TimedInputArc::Vector TAPNXmlParser::parseInputArcs(const xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
 {
 	TimedInputArc::Vector inputArcs;
 	xml_node<>* arcNode = root.first_node("inputArc");
 	while(arcNode != NULL){
-		inputArcs.push_back(ParseInputArc(*arcNode, places, transitions));
+		inputArcs.push_back(parseInputArc(*arcNode, places, transitions));
 		arcNode = arcNode->next_sibling("inputArc");
 	}
 
 	return inputArcs;
 }
 
-OutputArc::Vector TAPNXmlParser::ParseOutputArcs(const xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+OutputArc::Vector TAPNXmlParser::parseOutputArcs(const xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
 {
 	OutputArc::Vector outputArcs;
 	xml_node<>* arcNode = root.first_node("outputArc");
 	while(arcNode != NULL){
-		outputArcs.push_back(ParseOutputArc(*arcNode, places, transitions));
+		outputArcs.push_back(parseOutputArc(*arcNode, places, transitions));
 		arcNode = arcNode->next_sibling("outputArc");
 	}
 
 	return outputArcs;
 }
 
-boost::shared_ptr<TimedInputArc> TAPNXmlParser::ParseInputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const
+boost::shared_ptr<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();
@@ -166,13 +166,13 @@
 		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 = 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<TimedInputArc>(*place, *transition, weight, TimeInterval::CreateFor(interval));
+	return boost::make_shared<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
+boost::shared_ptr<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();
@@ -184,13 +184,13 @@
 		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);
+	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
+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();
@@ -200,13 +200,13 @@
 		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 = 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
+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();
@@ -216,14 +216,14 @@
 		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);
+	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);
 
 }
 
-std::vector<int> TAPNXmlParser::ParseInitialMarking(const rapidxml::xml_node<>& root, const TimedArcPetriNet& tapn) const
+std::vector<int> TAPNXmlParser::parseInitialMarking(const rapidxml::xml_node<>& root, const TimedArcPetriNet& tapn) const
 {
 	std::vector<int> markedPlaces;
 	xml_node<>* placeNode = root.first_node("place");
@@ -241,7 +241,7 @@
 		if(nTokens > 0)
 		{
 			for(int i = 0; i < nTokens; i++) {
-				markedPlaces.push_back(tapn.GetPlaceIndex(placeName));
+				markedPlaces.push_back(tapn.getPlaceIndex(placeName));
 			}
 		}
 

=== modified file 'src/Core/TAPNParser/TAPNXmlParser.hpp'
--- src/Core/TAPNParser/TAPNXmlParser.hpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPNParser/TAPNXmlParser.hpp	2013-05-15 15:27:27 +0000
@@ -27,27 +27,27 @@
 		virtual ~TAPNXmlParser() { /* empty */ };
 
 	public:
-		boost::shared_ptr<TimedArcPetriNet> Parse(const std::string & filename) const;
-		std::vector<int> ParseMarking(const std::string & filename, const TimedArcPetriNet& tapn) const;
+		boost::shared_ptr<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;
-
-		TimedPlace::Vector ParsePlaces(const rapidxml::xml_node<>& root) const;
-		boost::shared_ptr<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;
-
-		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;
-		std::vector<int> ParseInitialMarking(const rapidxml::xml_node<>& root, const TimedArcPetriNet& tapn) const;
+		boost::shared_ptr<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;
+
+		TimedTransition::Vector parseTransitions(const rapidxml::xml_node<>& root) const;
+		boost::shared_ptr<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;
+		std::vector<int> parseInitialMarking(const rapidxml::xml_node<>& root, const TimedArcPetriNet& tapn) const;
 	};
 }
 

=== modified file 'src/Core/TAPNParser/util.cpp'
--- src/Core/TAPNParser/util.cpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPNParser/util.cpp	2013-05-15 15:27:27 +0000
@@ -3,7 +3,7 @@
 
 namespace VerifyTAPN
 {
-	const std::string ReadFile(const std::string& filename)
+	const std::string readFile(const std::string& filename)
 	{
 		std::ifstream file (filename.c_str());
 		if(!file){

=== modified file 'src/Core/TAPNParser/util.hpp'
--- src/Core/TAPNParser/util.hpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPNParser/util.hpp	2013-05-15 15:27:27 +0000
@@ -6,10 +6,10 @@
 
 namespace VerifyTAPN
 {
-	const std::string ReadFile(const std::string& filename);
+	const std::string readFile(const std::string& filename);
 
 	template<class T>
-	const std::string ToString(T t)
+	const std::string toString(T t)
 	{
 		std::stringstream s;
 		s << t;

=== modified file 'src/Core/VerificationOptions.cpp'
--- src/Core/VerificationOptions.cpp	2013-02-16 19:21:05 +0000
+++ src/Core/VerificationOptions.cpp	2013-05-15 15:27:27 +0000
@@ -2,61 +2,60 @@
 #include <iostream>
 
 namespace VerifyTAPN {
-	std::string enumToString(Trace trace){
-		switch(trace)
-		{
-		case SOME:
-			return "some";
-		default:
-			return "no";
-		}
-	}
-
-	std::string SearchTypeEnumToString(SearchType s){
-		switch(s){
-		case COVERMOST:
-			return "Heuristic Search";
-		case RANDOM:
-			return "Random Search";
-		case DEPTHFIRST:
-			return "Depth-First Search";
-		default:
-			return "Breadth-First Search";
-		}
-	}
-
-	std::string VerificationTypeEnumToString(VerificationType s){
-			switch(s){
-			case TIMEDART:
-				return "Time darts";
-			default:
-				return "Default (discrete)";
-			}
-		}
-
-        std::string MemoryOptimizationEnumToString(MemoryOptimization m){
-            switch(m){
-                case NONE:
-                    return "None";
-                case PTRIE:
-                    return "PTrie ";
-                default:
-                    return "None";
-            }
-        }
-        
-	std::ostream& operator<<(std::ostream& out, const VerificationOptions& options)
-	{
-		out << "Search type: " << SearchTypeEnumToString(options.GetSearchType()) << std::endl;
-		out << "Verification method: " << VerificationTypeEnumToString(options.GetVerificationType()) << std::endl;
-                out << "Memory optimization: " << MemoryOptimizationEnumToString(options.GetMemoryOptimization()) << std::endl;
-		out << "k-bound is: " << options.GetKBound() << std::endl;
-		out << "Generating " << enumToString(options.GetTrace()) << " trace";
-		if(options.GetTrace() != NONE) out << " in " << (options.XmlTrace() ? "xml format" : "human readable format");
-		out << std::endl;
-		out << "Using " << (options.GetGlobalMaxConstantsEnabled() ? "global maximum constant" : "local maximum constants") << " for extrapolation" << std::endl;
-		out << "Model file is: " << options.GetInputFile() << std::endl;
-		out << "Query file is: " << options.QueryFile() << std::endl;
-		return out;
-	}
+
+    std::string enumToString(VerificationOptions::Trace trace) {
+        switch (trace) {
+            case VerificationOptions::SOME_TRACE:
+                return "some";
+            default:
+                return "no";
+        }
+    }
+
+    std::string SearchTypeEnumToString(VerificationOptions::SearchType s) {
+        switch (s) {
+            case VerificationOptions::COVERMOST:
+                return "Heuristic Search";
+            case VerificationOptions::RANDOM:
+                return "Random Search";
+            case VerificationOptions::DEPTHFIRST:
+                return "Depth-First Search";
+            default:
+                return "Breadth-First Search";
+        }
+    }
+
+    std::string VerificationTypeEnumToString(VerificationOptions::VerificationType s) {
+        switch (s) {
+            case VerificationOptions::TIMEDART:
+                return "Time darts";
+            default:
+                return "Default (discrete)";
+        }
+    }
+
+    std::string MemoryOptimizationEnumToString(VerificationOptions::MemoryOptimization m) {
+        switch (m) {
+            case VerificationOptions::NO_TRACE:
+                return "None";
+            case VerificationOptions::PTRIE:
+                return "PTrie ";
+            default:
+                return "None";
+        }
+    }
+
+    std::ostream& operator<<(std::ostream& out, const VerificationOptions& options) {
+        out << "Search type: " << SearchTypeEnumToString(options.getSearchType()) << std::endl;
+        out << "Verification method: " << VerificationTypeEnumToString(options.getVerificationType()) << std::endl;
+        out << "Memory optimization: " << MemoryOptimizationEnumToString(options.getMemoryOptimization()) << std::endl;
+        out << "k-bound is: " << options.getKBound() << std::endl;
+        out << "Generating " << enumToString(options.getTrace()) << " trace";
+        if (options.getTrace() != VerificationOptions::NO_TRACE) out << " in " << (options.getXmlTrace() ? "xml format" : "human readable format");
+        out << std::endl;
+        out << "Using " << (options.getGlobalMaxConstantsEnabled() ? "global maximum constant" : "local maximum constants") << " for extrapolation" << std::endl;
+        out << "Model file is: " << options.getInputFile() << std::endl;
+        out << "Query file is: " << options.getQueryFile() << std::endl;
+        return out;
+    }
 }

=== modified file 'src/Core/VerificationOptions.hpp'
--- src/Core/VerificationOptions.hpp	2013-02-16 19:21:05 +0000
+++ src/Core/VerificationOptions.hpp	2013-05-15 15:27:27 +0000
@@ -6,64 +6,108 @@
 #include <vector>
 
 namespace VerifyTAPN {
-	enum Trace { NONE, SOME };
-	enum SearchType { BREADTHFIRST, DEPTHFIRST, RANDOM, COVERMOST };
-	enum VerificationType { DISCRETE, TIMEDART };
-        enum MemoryOptimization { NO_MEMORY_OPTIMIZATION, PTRIE };
-
-	class VerificationOptions {
-		public:
-                        VerificationOptions(){}
-			VerificationOptions(
-				const std::string& inputFile,
-				const std::string& queryFile,
-				SearchType searchType,
-				VerificationType verificationType,
-                                MemoryOptimization memOptimization,
-				unsigned int k_bound,
-				Trace trace,
-				bool xml_trace,
-				bool useGlobalMaxConstants,
-				bool keepDeadTokens
-			) :	inputFile(inputFile),
-				queryFile(queryFile),
-				searchType(searchType),
-				verificationType(verificationType),
-                                memOptimization(memOptimization),
-				k_bound(k_bound),
-				trace(trace),
-				xml_trace(xml_trace),
-				useGlobalMaxConstants(useGlobalMaxConstants),
-				keepDeadTokens(keepDeadTokens)
-			{ 
-                        
-                        };
-
-		public: // inspectors
-			const std::string GetInputFile() const { return inputFile; }
-			const std::string QueryFile() const {return queryFile; }
-			inline const unsigned int GetKBound() const { return k_bound; }
-			inline const Trace GetTrace() const { return trace; };
-			inline const bool XmlTrace() const { return xml_trace; };
-			inline const bool GetGlobalMaxConstantsEnabled() const { return useGlobalMaxConstants; }
-			inline const SearchType GetSearchType() const { return searchType; }
-			inline const VerificationType GetVerificationType() const { return verificationType; }
-                        inline const MemoryOptimization GetMemoryOptimization() const { return memOptimization; }
-			inline const bool GetKeepDeadTokens() const { return keepDeadTokens; };
-		private:
-			std::string inputFile;
-			std::string queryFile;
-			SearchType searchType;
-			VerificationType verificationType;
-                        MemoryOptimization memOptimization;
-			unsigned int k_bound;
-			Trace trace;
-			bool xml_trace;
-			bool useGlobalMaxConstants;
-			bool keepDeadTokens;
-	};
-
-	std::ostream& operator<<(std::ostream& out, const VerificationOptions& options);
+
+    class VerificationOptions {
+    public:
+
+        enum Trace {
+            NO_TRACE, SOME_TRACE
+        };
+
+        enum SearchType {
+            BREADTHFIRST, DEPTHFIRST, RANDOM, COVERMOST
+        };
+
+        enum VerificationType {
+            DISCRETE, TIMEDART
+        };
+
+        enum MemoryOptimization {
+            NO_MEMORY_OPTIMIZATION, PTRIE
+        };
+
+        VerificationOptions() {
+        }
+
+        VerificationOptions(
+                const std::string& inputFile,
+                const std::string& queryFile,
+                SearchType searchType,
+                VerificationType verificationType,
+                MemoryOptimization memOptimization,
+                unsigned int k_bound,
+                Trace trace,
+                bool xml_trace,
+                bool useGlobalMaxConstants,
+                bool keepDeadTokens
+                ) : inputFile(inputFile),
+        queryFile(queryFile),
+        searchType(searchType),
+        verificationType(verificationType),
+        memOptimization(memOptimization),
+        k_bound(k_bound),
+        trace(trace),
+        xml_trace(xml_trace),
+        useGlobalMaxConstants(useGlobalMaxConstants),
+        keepDeadTokens(keepDeadTokens) {
+
+        };
+
+    public: // inspectors
+
+        const std::string getInputFile() const {
+            return inputFile;
+        }
+
+        const std::string getQueryFile() const {
+            return queryFile;
+        }
+
+        inline const unsigned int getKBound() const {
+            return k_bound;
+        }
+
+        inline const Trace getTrace() const {
+            return trace;
+        };
+
+        inline const bool getXmlTrace() const {
+            return xml_trace;
+        };
+
+        inline const bool getGlobalMaxConstantsEnabled() const {
+            return useGlobalMaxConstants;
+        }
+
+        inline const SearchType getSearchType() const {
+            return searchType;
+        }
+
+        inline const VerificationType getVerificationType() const {
+            return verificationType;
+        }
+
+        inline const MemoryOptimization getMemoryOptimization() const {
+            return memOptimization;
+        }
+
+        inline const bool getKeepDeadTokens() const {
+            return keepDeadTokens;
+        };
+    private:
+        std::string inputFile;
+        std::string queryFile;
+        SearchType searchType;
+        VerificationType verificationType;
+        MemoryOptimization memOptimization;
+        unsigned int k_bound;
+        Trace trace;
+        bool xml_trace;
+        bool useGlobalMaxConstants;
+        bool keepDeadTokens;
+    };
+
+    std::ostream& operator<<(std::ostream& out, const VerificationOptions& options);
 }
 
 #endif /* VERIFICATIONOPTIONS_HPP_ */

=== modified file 'src/DiscreteVerification/DataStructures/EncodingStructure.h'
--- src/DiscreteVerification/DataStructures/EncodingStructure.h	2012-12-09 14:16:04 +0000
+++ src/DiscreteVerification/DataStructures/EncodingStructure.h	2013-05-15 15:27:27 +0000
@@ -1,6 +1,6 @@
 /* 
  * File:   Encoding.h
- * Author: Peter Gjøl Jense
+ * Author: Peter Gjøl Jensen
  *
  * Created on 27. oktober 2012, 12:36
  */
@@ -28,54 +28,73 @@
             EncodingStructure(const EncodingStructure &other, uint size, uint offset, uint encsize);
             EncodingStructure(char* raw, uint size, uint offset, uint encsize);
             EncodingStructure(char* raw, uint size){
-                shadow = raw;
-                rsize = size;
+                binaryBlob = raw;
+                numberOfBytes = size;
             };
             virtual ~EncodingStructure();
 
-            EncodingStructure Clone() {
+            EncodingStructure clone() {
                 EncodingStructure s;
-                s.rsize = rsize;
-                s.shadow = new char[rsize + sizeof (T)];
-                memcpy(s.shadow, shadow, rsize + sizeof (T));
+                s.numberOfBytes = numberOfBytes;
+                s.binaryBlob = new char[numberOfBytes + sizeof (T)];
+                memcpy(s.binaryBlob, binaryBlob, numberOfBytes + sizeof (T));
                 return s;
             }
 
-            void Copy(const EncodingStructure &other, unsigned int offset) {
-                memcpy(&(shadow[offset / 8]), other.shadow, other.rsize);
+            inline void copy(const EncodingStructure &other, unsigned int offset) {
+                memcpy(&(binaryBlob[offset / 8]), other.binaryBlob, other.numberOfBytes);
             }
             
-            void Copy(const char* raw, unsigned int size){
-                shadow = new char[size + sizeof(T)];
-                memcpy(shadow, raw, size);
-            }
-
-            bool At(const uint place) const;
-            void Set(const uint place, const bool value) const;
-
-            void Zero() const {
-                memset(shadow, 0x0, rsize);
-            }
-
-            unsigned short int Size() const {
-                return rsize;
-            }
-
-            void Release() const {
-                delete[] shadow;
-            }
-
-            char* GetRaw() const {
-                return shadow;
-            }
-
-            void PrintEncoding() const {
-                for (unsigned short int i = 0; i < rsize * 8; i++)
-                    cout << this->At(i);
+            inline void copy(const char* raw, unsigned int size){
+                binaryBlob = new char[size + sizeof(T)];
+                memcpy(binaryBlob, raw, size);
+            }
+
+            inline bool at(const uint place) const {
+                uint offset = place % 8;
+                bool res2;
+                if (place / 8 < numberOfBytes)
+                    res2 = (binaryBlob[place / 8] & masks[offset]) != 0;
+                else
+                    res2 = false;
+
+                return res2;
+            }
+
+            inline void set(const uint place, const bool value) const {
+                uint offset = place % 8;
+                uint theplace = place / 8;
+                if (value) {
+                    binaryBlob[theplace] |= masks[offset];
+                } else {
+                    binaryBlob[theplace] &= ~masks[offset];
+                }
+
+            }
+
+            inline void zero() const {
+                memset(binaryBlob, 0x0, numberOfBytes);
+            }
+
+            inline unsigned short int Size() const {
+                return numberOfBytes;
+            }
+
+            inline void release() const {
+                delete[] binaryBlob;
+            }
+
+            inline char* getRaw() const {
+                return binaryBlob;
+            }
+
+            void printEncoding() const {
+                for (unsigned short int i = 0; i < numberOfBytes * 8; i++)
+                    cout << this->at(i);
                 cout << endl;
             }
 
-            inline static uint Overhead(uint size) {
+            inline static uint overhead(uint size) {
                 size = size % 8;
                 if (size == 0)
                     return 0;
@@ -83,47 +102,47 @@
                     return 8 - size;
             }
 
-            inline void SetMetaData(T data) const {
-                memcpy(&(shadow[rsize]), &data, sizeof (T));
+            inline void setMetaData(T data) const {
+                memcpy(&(binaryBlob[numberOfBytes]), &data, sizeof (T));
             }
 
-            inline T GetMetaData() const {
+            inline T getMetaData() const {
                 T res;
-                memcpy(&res, &(shadow[rsize]), sizeof (T));
+                memcpy(&res, &(binaryBlob[numberOfBytes]), sizeof (T));
                 return res;
             }
 
-            const char operator[](int i) {
+            inline const char operator[](int i) {
 
-                if (i >= rsize) {
+                if (i >= numberOfBytes) {
                     return 0x0;
                 }
-                return shadow[i];
+                return binaryBlob[i];
             }
             
-            friend bool operator==(const EncodingStructure &enc1, const EncodingStructure &enc2) {
-                if(enc1.rsize != enc2.rsize)
+            inline friend bool operator==(const EncodingStructure &enc1, const EncodingStructure &enc2) {
+                if(enc1.numberOfBytes != enc2.numberOfBytes)
                     return false;
-                for(int i = 0; i < enc1.rsize; i++)
-                    if(enc1.shadow[i] != enc2.shadow[i])
+                for(int i = 0; i < enc1.numberOfBytes; i++)
+                    if(enc1.binaryBlob[i] != enc2.binaryBlob[i])
                         return false;
                 return true;
             }
             
             
-            friend bool operator<(const EncodingStructure &enc1, const EncodingStructure &enc2) {
-                int count = enc1.rsize > enc2.rsize ? enc1.rsize : enc2.rsize;
+            inline friend bool operator<(const EncodingStructure &enc1, const EncodingStructure &enc2) {
+                int count = enc1.numberOfBytes > enc2.numberOfBytes ? enc1.numberOfBytes : enc2.numberOfBytes;
 
                 for (int i = 0; i < count; i++) {
-                    if (enc1.rsize > i && enc2.rsize > i && enc1.shadow[i] != enc2.shadow[i]) {
-                        return ((unsigned short int) enc1.shadow[i]) < ((unsigned short int) enc2.shadow[i]);
+                    if (enc1.numberOfBytes > i && enc2.numberOfBytes > i && enc1.binaryBlob[i] != enc2.binaryBlob[i]) {
+                        return ((unsigned short int) enc1.binaryBlob[i]) < ((unsigned short int) enc2.binaryBlob[i]);
                     }
 
                 }
-                if (enc1.rsize > enc2.rsize) {
+                if (enc1.numberOfBytes > enc2.numberOfBytes) {
                     return false;
 
-                } else if (enc1.rsize < enc2.rsize) {
+                } else if (enc1.numberOfBytes < enc2.numberOfBytes) {
                     return true;
                 }
 
@@ -131,44 +150,44 @@
             }
 
         private:
-            char* shadow;
-            unsigned short rsize;
+            char* binaryBlob;
+            unsigned short numberOfBytes;
             const static char masks[8];
         };
 
         template<class T>
         const char EncodingStructure<T>::masks[8] = {
-            0x01,
-            0x02,
-            0x04,
-            0x08,
-            0x10,
-            0x20,
-            0x40,
-            0x80
+            static_cast <char>(0x01),
+            static_cast <char>(0x02),
+            static_cast <char>(0x04),
+            static_cast <char>(0x08),
+            static_cast <char>(0x10),
+            static_cast <char>(0x20),
+            static_cast <char>(0x40),
+            static_cast <char>(0x80)
         };
 
         template<class T>
         EncodingStructure<T>::EncodingStructure(uint size) {
-            rsize = (size + Overhead(size)) / 8;
-            shadow = new char[rsize + sizeof (T)];
-            memset(shadow, 0x0, rsize + sizeof (T));
+            numberOfBytes = (size + overhead(size)) / 8;
+            binaryBlob = new char[numberOfBytes + sizeof (T)];
+            memset(binaryBlob, 0x0, numberOfBytes + sizeof (T));
         }
 
         template<class T>
         EncodingStructure<T>::EncodingStructure(const EncodingStructure &other, uint offset) {
             offset = offset / 8;
 
-            rsize = other.rsize;
-            if (rsize > offset)
-                rsize -= offset;
+            numberOfBytes = other.numberOfBytes;
+            if (numberOfBytes > offset)
+                numberOfBytes -= offset;
             else {
-                rsize = 0;
+                numberOfBytes = 0;
             }
 
-            shadow = new char[rsize + sizeof (T)];
-            memcpy(shadow, &(other.shadow[offset]), rsize);
-            SetMetaData(other.GetMetaData());
+            binaryBlob = new char[numberOfBytes + sizeof (T)];
+            memcpy(binaryBlob, &(other.binaryBlob[offset]), numberOfBytes);
+            setMetaData(other.getMetaData());
         }
 
         template<class T>
@@ -177,16 +196,16 @@
             uint so = size + offset;
             offset = ((so - 1) / 8) - ((size - 1) / 8);
 
-            rsize = ((encsize + this->Overhead(encsize)) / 8);
-            if (rsize > offset)
-                rsize -= offset;
+            numberOfBytes = ((encsize + this->overhead(encsize)) / 8);
+            if (numberOfBytes > offset)
+                numberOfBytes -= offset;
             else {
-                rsize = 0;
+                numberOfBytes = 0;
             }
 
-            shadow = new char[rsize + sizeof (T)];
-            memcpy(shadow, &(other.shadow[offset]), rsize);
-            SetMetaData(other.GetMetaData());
+            binaryBlob = new char[numberOfBytes + sizeof (T)];
+            memcpy(binaryBlob, &(other.binaryBlob[offset]), numberOfBytes);
+            setMetaData(other.getMetaData());
         }
 
         template<class T>
@@ -195,14 +214,14 @@
             uint so = size + offset;
             offset = ((so - 1) / 8) - ((size - 1) / 8);
 
-            rsize = ((encsize + this->Overhead(encsize)) / 8);
-            if (rsize > offset)
-                rsize -= offset;
+            numberOfBytes = ((encsize + this->overhead(encsize)) / 8);
+            if (numberOfBytes > offset)
+                numberOfBytes -= offset;
             else {
-                rsize = 0;
+                numberOfBytes = 0;
             }
 
-            shadow = &(raw[offset]);
+            binaryBlob = &(raw[offset]);
         }
 
         template<class T>
@@ -210,30 +229,7 @@
 
         }
 
-        template<class T>
-        bool EncodingStructure<T>::At(const uint place) const {
-            //    return data[place];
-            uint offset = place % 8;
-            bool res2;
-            if (place / 8 < rsize)
-                res2 = (shadow[place / 8] & masks[offset]) != 0;
-            else
-                res2 = false;
-
-            return res2;
-        }
-
-        template<class T>
-        void EncodingStructure<T>::Set(const uint place, const bool value) const {
-            uint offset = place % 8;
-            uint theplace = place / 8;
-            if (value) {
-                shadow[theplace] |= masks[offset];
-            } else {
-                shadow[theplace] &= ~masks[offset];
-            }
-
-        }
+
 
     }
 }

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarking.hpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2013-02-26 10:02:19 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2013-05-15 15:27:27 +0000
@@ -33,7 +33,7 @@
     
     // ugly forward declaration
     template<class MetaData>
-    class EncodingPointer;
+    struct EncodingPointer;
     
     struct MetaDataWithTraceAndEncoding : public MetaDataWithTrace {
         EncodingPointer<MetaData>* ep;

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2013-04-08 15:26:40 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2013-05-15 15:27:27 +0000
@@ -12,9 +12,10 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
+TokenList NonStrictMarkingBase::emptyTokenList = TokenList();
+    
 NonStrictMarkingBase::NonStrictMarkingBase() : children(0), generatedBy(NULL){
-	// TODO Auto-generated constructor stub
-
+    // empty constructor
 }
 
 NonStrictMarkingBase::NonStrictMarkingBase(const TAPN::TimedArcPetriNet& tapn, const std::vector<int>& v) :children(0), generatedBy(NULL){
@@ -30,7 +31,7 @@
 			}
 		}else{
 
-			Place p(&tapn.GetPlace(*iter));
+			Place p(&tapn.getPlace(*iter));
 			Token t(0,1);
 			p.tokens.push_back(t);
 			places.push_back(p);
@@ -40,12 +41,8 @@
 }
 
 NonStrictMarkingBase::NonStrictMarkingBase(const NonStrictMarkingBase& nsm) : children(0), generatedBy(NULL){
-	//for(PlaceList::const_iterator it = nsm.places.begin(); it != nsm.places.end(); it++){
-	//	places.push_back(Place(*it));
-	//}
 
 	places = nsm.places;
-
 	parent = nsm.parent;
 	generatedBy = nsm.generatedBy;
 }
@@ -60,18 +57,10 @@
 	return count;
 }
 
-//int NonStrictMarkingBase::NumberOfTokensInPlace(const Place& place) const{
-//	int count = 0;
-//	for(TokenList::const_iterator it = place.tokens.begin(); it != place.tokens.end(); it++){
-//		count = count + it->getCount();
-//	}
-//	return count;
-//}
-
-int NonStrictMarkingBase::NumberOfTokensInPlace(int placeId) const{
+int NonStrictMarkingBase::numberOfTokensInPlace(int placeId) const{
 	int count = 0;
 	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++){
-		if(iter->place->GetIndex() == placeId){
+		if(iter->place->getIndex() == placeId){
 			for(TokenList::const_iterator it = iter->tokens.begin(); it != iter->tokens.end(); it++){
 				count = count + it->getCount();
 			}
@@ -80,19 +69,19 @@
 	return count;
 }
 
-const TokenList& NonStrictMarkingBase::GetTokenList(int placeId) const{
+const TokenList& NonStrictMarkingBase::getTokenList(int placeId) const{
 	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++){
-		if(iter->place->GetIndex() == placeId) return iter->tokens;
+		if(iter->place->getIndex() == placeId) return iter->tokens;
 	}
 	return emptyTokenList;
 }
 
-bool NonStrictMarkingBase::RemoveToken(int placeId, int age){
+bool NonStrictMarkingBase::removeToken(int placeId, int age){
 	for(PlaceList::iterator pit = places.begin(); pit != places.end(); pit++){
-		if(pit->place->GetIndex() == placeId){
+		if(pit->place->getIndex() == placeId){
 			for(TokenList::iterator tit = pit->tokens.begin(); tit != pit->tokens.end(); tit++){
 				if(tit->getAge() == age){
-					return RemoveToken(*pit, *tit);
+					return removeToken(*pit, *tit);
 				}
 			}
 		}
@@ -100,11 +89,11 @@
 	return false;
 }
 
-void NonStrictMarkingBase::RemoveRangeOfTokens(Place& place, TokenList::iterator begin, TokenList::iterator end){
+void NonStrictMarkingBase::removeRangeOfTokens(Place& place, TokenList::iterator begin, TokenList::iterator end){
 	place.tokens.erase(begin, end);
 }
 
-bool NonStrictMarkingBase::RemoveToken(Place& place, Token& token){
+bool NonStrictMarkingBase::removeToken(Place& place, Token& token){
 	if(token.getCount() > 1){
 		token.remove(1);
 		return true;
@@ -114,7 +103,7 @@
 				place.tokens.erase(iter);
 				if(place.tokens.empty()){
 					for(PlaceList::iterator it = places.begin(); it != places.end(); it++){
-						if(it->place->GetIndex() == place.place->GetIndex()){
+						if(it->place->getIndex() == place.place->getIndex()){
 							places.erase(it);
 							return true;
 						}
@@ -127,29 +116,29 @@
 	return false;
 }
 
-void NonStrictMarkingBase::AddTokenInPlace(TAPN::TimedPlace& place, int age){
+void NonStrictMarkingBase::addTokenInPlace(TAPN::TimedPlace& place, int age){
 	for(PlaceList::iterator pit = places.begin(); pit != places.end(); pit++){
-		if(pit->place->GetIndex() == place.GetIndex()){
+		if(pit->place->getIndex() == place.getIndex()){
 			for(TokenList::iterator tit = pit->tokens.begin(); tit != pit->tokens.end(); tit++){
 				if(tit->getAge() == age){
 					Token t(age, 1);
-					AddTokenInPlace(*pit, t);
+					addTokenInPlace(*pit, t);
 					return;
 				}
 			}
 			Token t(age,1);
-			AddTokenInPlace(*pit, t);
+			addTokenInPlace(*pit, t);
 			return;
 		}
 	}
 	Token t(age,1);
 	Place p(&place);
-	AddTokenInPlace(p,t);
+	addTokenInPlace(p,t);
 
 	// Insert place
 	bool inserted = false;
 	for(PlaceList::iterator it = places.begin(); it != places.end(); it++){
-		if(it->place->GetIndex() > place.GetIndex()){
+		if(it->place->getIndex() > place.getIndex()){
 			places.insert(it, p);
 			inserted = true;
 			break;
@@ -160,21 +149,21 @@
 	}
 }
 
-void NonStrictMarkingBase::AddTokenInPlace(const TAPN::TimedPlace& place, Token& token){
+void NonStrictMarkingBase::addTokenInPlace(const TAPN::TimedPlace& place, Token& token){
 	for(PlaceList::iterator pit = places.begin(); pit != places.end(); pit++){
-		if(pit->place->GetIndex() == place.GetIndex()){
-			AddTokenInPlace(*pit, token);
+		if(pit->place->getIndex() == place.getIndex()){
+			addTokenInPlace(*pit, token);
 			return;
 		}
 	}
 
 	Place p(&place);
-	AddTokenInPlace(p,token);
+	addTokenInPlace(p,token);
 
 	// Insert place
 	bool inserted = false;
 	for(PlaceList::iterator it = places.begin(); it != places.end(); it++){
-		if(it->place->GetIndex() > place.GetIndex()){
+		if(it->place->getIndex() > place.getIndex()){
 			places.insert(it, p);
 			inserted = true;
 			break;
@@ -185,7 +174,7 @@
 	}
 }
 
-void NonStrictMarkingBase::AddTokenInPlace(Place& place, Token& token){
+void NonStrictMarkingBase::addTokenInPlace(Place& place, Token& token){
 	if(token.getCount() == 0) return;
 	for(TokenList::iterator iter = place.tokens.begin(); iter != place.tokens.end(); iter++){
 		if(iter->getAge() == token.getAge()){
@@ -207,24 +196,6 @@
 	}
 }
 
-void NonStrictMarkingBase::incrementAge(){
-	for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
-		iter->incrementAge();
-	}
-}
-
-void NonStrictMarkingBase::incrementAge(int age){
-	for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
-		iter->incrementAge(age);
-	}
-}
-
-void NonStrictMarkingBase::decrementAge(){
-	for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
-		iter->decrementAge();
-	}
-}
-
 NonStrictMarkingBase::~NonStrictMarkingBase() { }
 
 bool NonStrictMarkingBase::equals(const NonStrictMarkingBase &m1) const{
@@ -232,7 +203,7 @@
 
 	PlaceList::const_iterator p_iter = m1.places.begin();
 	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++, p_iter++){
-		if(iter->place->GetIndex() != p_iter->place->GetIndex())	return false;
+		if(iter->place->getIndex() != p_iter->place->getIndex())	return false;
 		if(iter->tokens.size() != p_iter->tokens.size())	return false;
 		TokenList::const_iterator pt_iter = p_iter->tokens.begin();
 		for(TokenList::const_iterator t_iter = iter->tokens.begin(); t_iter != iter->tokens.end(); t_iter++, pt_iter++){
@@ -246,7 +217,7 @@
 std::ostream& operator<<(std::ostream& out, NonStrictMarkingBase& x ) {
 	out << "-";
 	for(PlaceList::iterator iter = x.places.begin(); iter != x.places.end(); iter++){
-		out << "place " << iter->place->GetId() << " has tokens (age, count): ";
+		out << "place " << iter->place->getId() << " has tokens (age, count): ";
 		for(TokenList::iterator it = iter->tokens.begin(); it != iter->tokens.end(); it++){
 			out << "(" << it->getAge() << ", " << it->getCount() << ") ";
 		}
@@ -266,23 +237,23 @@
 		//set age of too old tokens to max age
 		int count = 0;
 		for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++) {
-                        if(token_iter->getAge() > place_iter->place->GetMaxConstant()){ // this will also removed dead tokens
+                        if(token_iter->getAge() > place_iter->place->getMaxConstant()){ // this will also removed dead tokens
 				TokenList::iterator beginDelete = token_iter;
-				if(place_iter->place->GetType() == TAPN::Std){
+				if(place_iter->place->getType() == TAPN::Std){
 					for(; token_iter != place_iter->tokens.end(); token_iter++){
 						count += token_iter->getCount();
 					}
 				}
-				this->RemoveRangeOfTokens(*place_iter, beginDelete, place_iter->tokens.end());
+				this->removeRangeOfTokens(*place_iter, beginDelete, place_iter->tokens.end());
 				break;
 			}
 		}
                 if(count){
-                        Token t(place_iter->place->GetMaxConstant()+1,count);
-                        this->AddTokenInPlace(*place_iter, t);
+                        Token t(place_iter->place->getMaxConstant()+1,count);
+                        this->addTokenInPlace(*place_iter, t);
                 }
 	}
-	this->CleanUp();
+	this->cleanUp();
 	#ifdef DEBUG
 		std::cout << "After cut: " << *this << std::endl;
 	#endif
@@ -290,8 +261,8 @@
 
 int NonStrictMarkingBase::getYoungest(){
     	int youngest = INT_MAX;
-	for(PlaceList::const_iterator place_iter = GetPlaceList().begin(); place_iter != GetPlaceList().end(); place_iter++){
-		if(youngest > place_iter->tokens.front().getAge() && place_iter->tokens.front().getAge() <= place_iter->place->GetMaxConstant()){
+	for(PlaceList::const_iterator place_iter = getPlaceList().begin(); place_iter != getPlaceList().end(); place_iter++){
+		if(youngest > place_iter->tokens.front().getAge() && place_iter->tokens.front().getAge() <= place_iter->place->getMaxConstant()){
 			youngest = place_iter->tokens.front().getAge();
 		}
 	}
@@ -310,11 +281,11 @@
 
 	for(PlaceList::iterator place_iter = places.begin(); place_iter != places.end(); place_iter++){
 		for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
-			if(token_iter->getAge() != place_iter->place->GetMaxConstant() + 1){
+			if(token_iter->getAge() != place_iter->place->getMaxConstant() + 1){
 				token_iter->setAge(token_iter->getAge()-youngest);
 			}
 #ifdef DEBUG
-			else if(token_iter->getAge() > place_iter->place->GetMaxConstant() + 1){
+			else if(token_iter->getAge() > place_iter->place->getMaxConstant() + 1){
 				assert(false);
 			}
 #endif

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp	2013-03-17 14:00:48 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp	2013-05-15 15:27:27 +0000
@@ -32,14 +32,14 @@
 	Token(int age, int count) : age(age), count(count) {  };
 	Token(const Token& t) : age(t.age), count(t.count) {  };
 
-	bool equals(const Token &t) const { return (this->age == t.age && this->count == t.count); };
+	inline bool equals(const Token &t) const { return (this->age == t.age && this->count == t.count); };
 
-	void add(int num){ count = count + num; };
-	int getCount() const { return count; };
-	int getAge() const { return age; };
-	void setAge(int i) { age = i; };
-	void setCount(int i) { count = i; };
-	void remove(int num){ count = count - num; };
+	inline void add(int num){ count = count + num; };
+	inline int getCount() const { return count; };
+	inline int getAge() const { return age; };
+	inline void setAge(int i) { age = i; };
+	inline void setCount(int i) { count = i; };
+	inline void remove(int num){ count = count - num; };
 
 	// Ages all tokens by 1
 	inline void incrementAge(){
@@ -78,12 +78,12 @@
 	friend std::size_t hash_value(Place const& p)
 	{
 		std::size_t seed = boost::hash_range(p.tokens.begin(), p.tokens.end());
-		boost::hash_combine(seed, p.place->GetIndex());
+		boost::hash_combine(seed, p.place->getIndex());
 
 		return seed;
 	}
 
-	int NumberOfTokens() const{
+	inline int numberOfTokens() const{
 		int count = 0;
 		for(TokenList::const_iterator iter = tokens.begin(); iter != tokens.end(); iter++){
 			count += iter->getCount();
@@ -91,7 +91,7 @@
 		return count;
 	}
 
-	int MaxTokenAge() const{
+	inline int maxTokenAge() const{
 		int max = -1;
 		for(TokenList::const_iterator iter = tokens.begin(); iter != tokens.end(); iter++){
 			if(iter->getAge() > max) max = iter->getAge();
@@ -100,19 +100,19 @@
 	}
 
 	// Ages all tokens by 1
-	void incrementAge(){
+	inline void incrementAge(){
 		for(TokenList::iterator iter = tokens.begin(); iter != tokens.end(); iter++){
 			iter->incrementAge();
 		}
 	}
 
-	void incrementAge(int age){
+	inline void incrementAge(int age){
 		for(TokenList::iterator iter = tokens.begin(); iter != tokens.end(); iter++){
 			iter->incrementAge(age);
 		}
 	}
 
-	void decrementAge(){
+	inline void decrementAge(){
 		for(TokenList::iterator iter = tokens.begin(); iter != tokens.end(); iter++){
 			iter->decrementAge();
 		}
@@ -133,38 +133,57 @@
 
 	virtual ~NonStrictMarkingBase();
 
-	virtual size_t HashKey() const { return boost::hash_range(places.begin(), places.end()); };
-
-	virtual NonStrictMarkingBase& Clone()
-		{
-			NonStrictMarkingBase* clone = new NonStrictMarkingBase(*this);
-			return *clone;
-		};
-
 	public: // inspectors
-		//int NumberOfTokensInPlace(const Place& palce) const;
-		int NumberOfTokensInPlace(int placeId) const;
-		const TokenList& GetTokenList(int placeId) const;
-		const PlaceList& GetPlaceList() const{ return places; }
+		int numberOfTokensInPlace(int placeId) const;
+		const TokenList& getTokenList(int placeId) const;
+		inline const PlaceList& getPlaceList() const{ return places; }
 		unsigned int size();
-		const NonStrictMarkingBase* GetParent() const { return parent; }
-		const TAPN::TimedTransition* GetGeneratedBy() const { return generatedBy; }
-
-
+		inline const NonStrictMarkingBase* getParent() const { return parent; }
+		inline const TAPN::TimedTransition* getGeneratedBy() const { return generatedBy; }
+		bool equals(const NonStrictMarkingBase &m1) const;
+                inline int getNumberOfChildren(){
+                    return children;
+                }
+                virtual size_t getHashKey() const { return boost::hash_range(places.begin(), places.end()); };
+                
 	public: // modifiers
-		void cut();
-		bool RemoveToken(int placeId, int age);
-		bool RemoveToken(Place& place, Token& token);
-		void AddTokenInPlace(TAPN::TimedPlace& place, int age);
-		void AddTokenInPlace(Place& place, Token& token);
-		void AddTokenInPlace(const TAPN::TimedPlace& place, Token& token);
-		void incrementAge();	// increment
-		void incrementAge(int age);
-		void decrementAge();	// decrement
-		void RemoveRangeOfTokens(Place& place, TokenList::iterator begin, TokenList::iterator end);
-		void SetParent(NonStrictMarkingBase* parent) { this->parent = parent; }
-		void SetGeneratedBy(const TAPN::TimedTransition* generatedBy) { this->generatedBy = generatedBy; }
-		void CleanUp() {
+
+                void cut();
+		bool removeToken(int placeId, int age);
+		bool removeToken(Place& place, Token& token);
+		void addTokenInPlace(TAPN::TimedPlace& place, int age);
+		void addTokenInPlace(Place& place, Token& token);
+		void addTokenInPlace(const TAPN::TimedPlace& place, Token& token);
+                inline void incrementAge(){
+                        for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
+                                iter->incrementAge();
+                        }
+                }
+
+                inline void incrementAge(int age){
+                        for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
+                                iter->incrementAge(age);
+                        }
+                }
+
+                inline void decrementAge(){
+                        for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
+                                iter->decrementAge();
+                        }
+                }
+		void removeRangeOfTokens(Place& place, TokenList::iterator begin, TokenList::iterator end);
+		inline void setParent(NonStrictMarkingBase* parent) { this->parent = parent; }
+		inline void setGeneratedBy(const TAPN::TimedTransition* generatedBy) { this->generatedBy = generatedBy; }
+                inline void setNumberOfChildren(int i){
+                    children = i;
+                }
+                inline  void incrementNumberOfChildren(){
+                    ++children;
+                }
+                inline void decrementNumberOfChildren(){
+                    --children;
+                }
+		inline void cleanUp() {
 			for(unsigned int i = 0; i < places.size(); i++){
 				if(places[i].tokens.empty()){
 					places.erase(places.begin()+i);
@@ -174,18 +193,19 @@
 		}
                 int getYoungest();
 		int makeBase(TAPN::TimedArcPetriNet* tapn);
-
-	public:
-		bool equals(const NonStrictMarkingBase &m1) const;
-
-	public:
+                virtual NonStrictMarkingBase& Clone()
+                {
+                        NonStrictMarkingBase* clone = new NonStrictMarkingBase(*this);
+                        return *clone;
+                };
+
+	private:
 		int children;
 		PlaceList places;
-		TokenList emptyTokenList;
-
-	public:
 		NonStrictMarkingBase* parent;
 		const TAPN::TimedTransition* generatedBy;
+
+        static TokenList emptyTokenList;
 };
 
 std::ostream& operator<<(std::ostream& out, NonStrictMarkingBase& x);

=== removed file 'src/DiscreteVerification/DataStructures/PData.h'
--- src/DiscreteVerification/DataStructures/PData.h	2013-04-08 13:45:17 +0000
+++ src/DiscreteVerification/DataStructures/PData.h	1970-01-01 00:00:00 +0000
@@ -1,430 +0,0 @@
-/* 
- * File:   PData.h
- * Author: Peter Gjøl Jensen
- *
- * Created on 5. november 2012, 10:22
- */
-
-
-#include "NonStrictMarking.hpp"
-#include "EncodingStructure.h"
-#include "TimeDart.hpp"
-
-#ifndef PDATA_H
-#define	PDATA_H
-namespace VerifyTAPN {
-    namespace DiscreteVerification {
-
-        // pointer containing enough data to reconstruct the stored data at any time!
-        template<typename T>
-        struct EncodingPointer {
-            // The part of the encoding not being represented by the path in the PTrie
-            EncodingStructure<T*> encoding;
-            // The coresponding node in the PTrie
-            unsigned int node;
-
-            // empty constructor
-            EncodingPointer() {
-            };
-            
-            // Construct a pointer with enough (persistent) data to recreate the marking. 
-            // The encoding is cloned as it is not persistant in the PTrie
-            EncodingPointer(EncodingStructure<T*> &en, unsigned int n) : encoding(en.Clone()), node(n) {
-            }
-        };
-        
-        template<typename T>
-        class PData {
-        public:
-            typedef unsigned int uint;
-            typedef EncodingStructure<T*> MarkingEncoding;
-
-            struct Result {
-                bool isNew;
-                MarkingEncoding encoding;
-                uint pos;
-
-                Result(bool ex, MarkingEncoding en, uint node) : isNew(ex), encoding(en), pos(node) {
-                };
-            };
-
-
-            PData(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, int knumber, int nplaces, int mage) :
-            k(knumber),
-            maxAge(mage + 1),
-            numberOfPlaces(nplaces),
-            countSize(ceil(log2((knumber ? knumber : 1)) + 1)),
-            enumeratedOffset(ceil(log2((nplaces * (mage + 1))) + 1) + countSize),
-            numberOfVariables(enumeratedOffset * (knumber ? knumber : 1)),
-            cachesize(128),
-            tapn(tapn) {
-                overhead = MarkingEncoding::Overhead(this->numberOfVariables);
-                this->numberOfVariables += overhead;
-                stored = 0;
-                bddsize = cachesize;
-                this->BDDArr.push_back(new PNode[this->bddsize]);
-                memset(this->BDDArr[0], 0xffffffff, this->bddsize * sizeof (PNode));
-                BDDArr[0][0].shadow = NULL;
-                BDDArr[0][0].highCount = BDDArr[0][0].lowCount = 0;
-                BDDArr[0][0].lowpos = BDDArr[0][0].highpos = 0;
-                BDDArr[0][0].parent = 0;
-                bddnext = 1;
-                encoding = MarkingEncoding(this->numberOfVariables);
-                listcount = 0;
-                maxCount = sizeof (PNode) * 4 + sizeof (std::list<PNode>) * 4;
-
-            };
-            virtual ~PData();
-
-            uint maxCount;
-
-            struct PNode {
-                MarkingEncoding* shadow;
-                uint highpos;
-
-                uint lowpos;
-
-                short int highCount;
-                short int lowCount;
-                uint parent;
-            };
-
-            bool search(MarkingEncoding* arr, MarkingEncoding en, int size) {
-                for (int i = 0; i < size; i++) {
-                    if (arr[i] == en)
-                        return true;
-                }
-                return false;
-            }
-            /*            bool equal(MarkingEncoding* arr, EncodingList* lst){
-                            EncodingList::const_iterator it = lst->begin();
-                            while(it != lst->end()){
-                                if(!search(arr, *it, lst->size()))
-                                    return false;
-                                it++;
-                            }
-                            return true;
-                        }*/
-
-            Result Add(NonStrictMarkingBase* marking);
-
-            unsigned int size() {
-                return stored;
-            }
-            void PrintMemStats();
-            void PrintEncoding(bool* encoding, int length);
-
-            inline PNode* FetchNode(uint i) {