Merge lp:~peter-gjoel/verifydtapn/PTrieWorkflow into lp:verifydtapn

[Peter Gjøl Jensen]

Implementation of ptries for workflow verification.

[Jiri Srba (srba)]

Please, merge trunk to this branch and resolve the numerous conflicts.

review: Needs Fixing

[lp:~peter-gjoel/verifydtapn/PTrieWorkflow]

358. By Peter Gjøl Jensen on 2015-06-25

merged with trunk

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

Fixed.

[Jiri Srba (srba)]

Thanks. I am still getting some warnings:

In file included from src/DiscreteVerification/DataStructures/../SearchStrategies/../DataStructures/NonStrictMarking.hpp:15:
src/DiscreteVerification/DataStructures/ptrie.h:388:45: warning: variable 'node'
      is uninitialized when used within its own initialization [-Wuninitialized]
                    node_t* node = get_node(node->_lowpos);
                            ~~~~ ^~~~
src/DiscreteVerification/DataStructures/WorkflowPWList.cpp:192:20: note: in
      instantiation of member function
      'ptrie::ptrie_t<VerifyTAPN::DiscreteVerification::MetaData *>::visit'
      requested here
            passed.visit(visitor);
                   ^
In file included from src/DiscreteVerification/DataStructures/WorkflowPWList.cpp:3:
src/DiscreteVerification/DataStructures/WorkflowPWList.hpp:60:27: warning:
      private field 'last' is not used [-Wunused-private-field]
        NonStrictMarking* last;
                          ^
2 warnings generated.

review: Needs Fixing

[lp:~peter-gjoel/verifydtapn/PTrieWorkflow]

359. By Peter Gjøl Jensen on 2015-06-26

fixed warnings

360. By Peter Gjøl Jensen on 2015-06-29

fixed covered marking visitor

361. By Peter Gjøl Jensen on 2015-06-29

readded limit on cover-check

362. By Peter Gjøl Jensen on 2015-06-29

fixed problem with ptries and unbounded markings

363. By Peter Gjøl Jensen on 2015-08-20

merged with trunk

364. By Peter Gjøl Jensen on 2015-08-20

changed comparison function for ptries, simplifying code and giving a speedup on VERY large markings

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

Minor re-factoring, improving on code-quality and possibly giving speedup on very large markings (several hundreds of tokens).

[Jiri Srba (srba)]

Extensively tested and it works flawlessly on all my examples.

review: Approve

=== modified file 'makefile.linux64'
--- makefile.linux64	2015-06-17 10:05:28 +0000
+++ makefile.linux64	2015-08-20 13:27:24 +0000
@@ -8,9 +8,9 @@
 CUT				= cut
 
 # Compiler and linker flags
-CFLAGS 			= -fpermissive -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -O3 -Wall -mtune=core2
+CFLAGS 			=  -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -O3 -Wall -mtune=core2
 
-LDFLAGS 		= -fpermissive -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -O3 -Wall -mtune=core2
+LDFLAGS 		= -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -O3 -Wall -mtune=core2
 
 # Input files
 SOURCES			= $(shell find * -name "*.cpp")	

=== added file 'src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.cpp'
--- src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.cpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.cpp	2015-08-20 13:27:24 +0000
@@ -0,0 +1,190 @@
+/* 
+ * File:   CoveredMarkingVisitor.cpp
+ * Author: Peter G. Jensen
+ *
+ * Created on 18 June 2015, 14:23
+ */
+
+#include "CoveredMarkingVisitor.h"
+
+
+using namespace ptrie;
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+    CoveredMarkingVisitor::CoveredMarkingVisitor(
+                            MarkingEncoder<MetaData*, NonStrictMarking>& enc)
+    : encoder(enc), scratchpad(0)
+    {
+        
+    }
+    
+    
+    CoveredMarkingVisitor::~CoveredMarkingVisitor()
+    {
+        scratchpad.release();
+    }
+    
+    void CoveredMarkingVisitor::set_target(NonStrictMarking* m, ptriepointer_t<MetaData*> me)
+    {
+        target = m;
+        _found=false;
+        _targetencoding = me;
+        
+        if(encoder.scratchpad.size() > scratchpad.size())
+        {
+            scratchpad.release();
+            scratchpad = encoder.scratchpad.clone();
+        }
+    }
+    
+    bool CoveredMarkingVisitor::set(int index, bool value)
+    {
+        if(_found) return true;  // end
+        scratchpad.set(index, value);
+        // If we have enough bits to constitute a single token (with placement)
+        if((index + 1) % encoder.offsetBitSize == 0 && index > 0)
+        {
+            size_t begin = (index / encoder.offsetBitSize) * encoder.offsetBitSize;
+            unsigned long long data = 0;
+            uint count = 0;
+            uint cbit = index;
+            
+            while (cbit >= begin + encoder.countBitSize) {
+                data = data << 1;
+                if(scratchpad.at(cbit))
+                {
+                    data |= 1;
+                }
+                --cbit;
+            }
+            
+            while(cbit >= begin)
+            {
+                count = count << 1;
+                if(scratchpad.at(cbit))
+                {
+                    count |= 1;
+                }
+                if(cbit == 0) break;
+                cbit--;
+            }
+            
+            if (count) {
+                return !target_contains_token(data, count);
+            }
+            // should not really happen
+            assert(false);
+            return true;    // skip if happens!
+        }
+        else
+        {
+            return false;   // not enough info
+        }
+    }
+    
+    bool CoveredMarkingVisitor::set_remainder(int index, 
+                                            ptriepointer_t<MetaData*> pointer)
+    {
+        // special case, marking cannot cover itself
+        if(pointer.index == _targetencoding.index) return false;
+        if(_found) return true;  // end
+
+        encoding_t remainder = pointer.remainder();
+        uint offset = index - (index % 8);  // offset matches on a byte
+        uint begin = (index / encoder.offsetBitSize ) * encoder.offsetBitSize;   // start from whole token
+        // check inclusion 
+
+        bool bit;
+        
+        while(true)
+        {
+            uint cbit = begin;
+            unsigned long long data = 0;
+            uint count = 0;
+            cbit += encoder.offsetBitSize - 1;
+            // unpack place/age/count
+            while (cbit >= begin + encoder.countBitSize) {
+                data = data << 1;
+
+                if(cbit < offset) bit = scratchpad.at(cbit);
+                else bit = remainder.at(cbit - offset);
+
+                if(bit)
+                {
+                    data |= 1;
+                }
+                --cbit;
+            }
+
+            while(cbit >= begin)
+            {
+                count = count << 1;
+
+                if(cbit < offset) bit = scratchpad.at(cbit);
+                else bit = remainder.at(cbit - offset);
+
+                if(bit)
+                {
+                    count |= 1;
+                }
+                if(cbit == 0) break;
+                cbit--;                
+            }
+            begin += encoder.offsetBitSize;
+            if (count) 
+            {
+                if(!target_contains_token(data, count))
+                {
+                    return false;
+                }
+            }
+            else
+            {
+                break;
+            }
+        }
+        
+        match = pointer;
+        _found = true;
+        return true;
+    }
+    
+    bool CoveredMarkingVisitor::back(int index)
+    {
+        return false;
+    }
+    
+    bool CoveredMarkingVisitor::target_contains_token(unsigned long long placeage, uint count)
+    {
+        if(count == 0) return true;
+        
+        int age = floor(placeage / encoder.numberOfPlaces);
+        int place = (placeage % encoder.numberOfPlaces);
+        int cnt = count;
+        const TokenList& tokens = target->getTokenList(place);
+        
+
+        for(    TokenList::const_iterator it = tokens.begin();
+                it != tokens.end(); ++it)
+        {
+            if(it->getAge() == age)
+            {
+                if(it->getCount() >= cnt) return true; // continue
+                else return false; // skip branch
+            }
+            else if(it->getAge() > age) return false;  // skip branch
+        }
+
+        return false; // skip branch
+    }
+    
+    NonStrictMarking* CoveredMarkingVisitor::decode()
+    {
+        NonStrictMarking* m = encoder.decode(match);
+        m->meta = match.get_meta();
+        return m;
+    }
+    
+}
+}
\ No newline at end of file

=== added file 'src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.h'
--- src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.h	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.h	2015-08-20 13:27:24 +0000
@@ -0,0 +1,57 @@
+/* 
+ * File:   CoveredMarkingVisitor.h
+ * Author: Peter G. Jensen
+ *
+ * Created on 17 June 2015, 00:04
+ */
+
+#ifndef COVEREDMARKINGVISITOR_H
+#define	COVEREDMARKINGVISITOR_H
+
+#include "binarywrapper.h"
+#include <limits>
+#include <vector>
+#include "ptrie.h"
+#include "visitor.h"
+#include "MarkingEncoder.h"
+#include "NonStrictMarkingBase.hpp"
+#include "NonStrictMarking.hpp"
+
+
+using namespace ptrie;
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+    
+    class CoveredMarkingVisitor
+    : public visitor_t<MetaData*>
+    {
+        typedef binarywrapper_t<MetaData*> encoding_t;
+        private:
+            MarkingEncoder<MetaData*, NonStrictMarking>& encoder;
+            NonStrictMarking* target;
+            encoding_t scratchpad;
+            ptriepointer_t<MetaData*> match;
+            bool _found;
+            ptriepointer_t<MetaData*> _targetencoding;
+            
+        private:
+            bool target_contains_token(unsigned long long placeage, uint count);
+            
+        public:
+            CoveredMarkingVisitor(
+                            MarkingEncoder<MetaData*, NonStrictMarking>& enc);
+            ~CoveredMarkingVisitor();
+            virtual bool back(int index);
+            virtual bool set(int index, bool value);
+            virtual bool set_remainder(int index,
+                                            ptriepointer_t<MetaData*> pointer);
+            void set_target(NonStrictMarking* m, ptriepointer_t<MetaData*> me);
+            NonStrictMarking* decode();
+            bool found(){return _found;}
+    };
+    
+}
+}
+
+#endif	/* BINARYMARKINGVISITOR_H */
+

=== modified file 'src/DiscreteVerification/DataStructures/MarkingEncoder.h'
--- src/DiscreteVerification/DataStructures/MarkingEncoder.h	2015-06-22 21:03:26 +0000
+++ src/DiscreteVerification/DataStructures/MarkingEncoder.h	2015-08-20 13:27:24 +0000
@@ -20,9 +20,12 @@
 namespace VerifyTAPN {
     namespace DiscreteVerification {
 
+        class CoveredMarkingVisitor;
+        
         template<typename T, typename M = NonStrictMarkingBase>
         class MarkingEncoder
         {
+        friend class CoveredMarkingVisitor;
         typedef binarywrapper_t<T> encoding_t;
 
         private:
@@ -32,10 +35,9 @@
             const uint countBitSize;
             const uint placeAgeBitSize;
             const uint offsetBitSize; 
-            uint markingBitSize;
+            const uint markingBitSize;
             TAPN::TimedArcPetriNet& tapn;
             encoding_t scratchpad;
-            void* raw;
         public:
             MarkingEncoder(TAPN::TimedArcPetriNet& tapn, int knumber,
                                                         int nplaces, int mage);
@@ -58,8 +60,7 @@
             markingBitSize(offsetBitSize * (knumber ? knumber : 1)),
             tapn(tapn)
         {
-                scratchpad = encoding_t(markingBitSize);
-                raw = (void*)scratchpad.raw();
+                scratchpad = encoding_t(0);
         }
         
         template<typename T, typename M>
@@ -71,7 +72,10 @@
         template<typename T, typename M>
         M* MarkingEncoder<T, M>::decode(const ptriepointer_t<T>& pointer)
         {
-            assert(scratchpad.raw() == raw);
+            // we allready know here that the scratchpad is large enough,
+            // it is monotonically increased when we encode, ie; no marking
+            // taking up more bits are currently in the ptrie.
+            
             M* m = new M();
             assert(pointer.container->consistent());
             const encoding_t remainder = pointer.remainder();
@@ -81,12 +85,13 @@
             
             uint cbit = 0;
             // foreach token
-            uint data = 0;
-            uint count = 0;
+      
             bool bit;
             for (uint i = 0; i < maxNumberOfTokens; i++) {
                 uint offset = offsetBitSize * i;
                 cbit = offset + offsetBitSize - 1;
+                unsigned long long data = 0;
+                uint count = 0;
                 
                 while (cbit >= offset + countBitSize) {
                     data = data << 1;
@@ -137,8 +142,6 @@
                     uint place = (data % this->numberOfPlaces);
                     Token t = Token(age, count);
                     m->addTokenInPlace(tapn.getPlace(place), t);
-                    data = 0;
-                    count = 0;
                 }
                 else
                 {
@@ -157,6 +160,25 @@
         template<typename T, typename M>
         binarywrapper_t<T> MarkingEncoder<T, M>::encode(M* marking)
         {
+            // make sure we have space to encode marking
+            size_t count = 0;
+            for (vector<Place>::const_iterator pi = marking->getPlaceList().begin();
+                    pi != marking->getPlaceList().end();
+                    pi++) {
+                count += pi->tokens.size();
+            }
+            count *= offsetBitSize;
+            count /= 8;
+            count += 1;
+            
+            if(scratchpad.size() < count)
+            {
+                scratchpad.release();
+                scratchpad = encoding_t(count * 8);
+            }
+            
+
+
             scratchpad.zero();
             int tc = 0;
             uint bitcount = 0;

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarking.hpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2015-06-22 21:03:26 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2015-08-20 13:27:24 +0000
@@ -48,6 +48,18 @@
             MetaDataWithTraceAndEncoding* parent;
     };
     
+    struct WorkflowSoundnessMetaDataWithEncoding : public MetaDataWithTraceAndEncoding {
+    public:
+        WorkflowSoundnessMetaDataWithEncoding() : MetaDataWithTraceAndEncoding(), parents() 
+            { totalDelay = INT_MAX;};
+            virtual ~WorkflowSoundnessMetaDataWithEncoding()
+            {
+                parents.clear();
+            }
+            
+            vector<MetaData*> parents;
+    };
+    
     class NonStrictMarking : public NonStrictMarkingBase{
     public:
         NonStrictMarking():NonStrictMarkingBase(), meta(NULL){}

=== modified file 'src/DiscreteVerification/DataStructures/WorkflowPWList.cpp'
--- src/DiscreteVerification/DataStructures/WorkflowPWList.cpp	2015-06-22 22:10:16 +0000
+++ src/DiscreteVerification/DataStructures/WorkflowPWList.cpp	2015-08-20 13:27:24 +0000
@@ -88,7 +88,8 @@
                 }
 
                 bool isFirst = true;
-                for (vector<NonStrictMarking*>::iterator iter = coveredMarkings.begin(); iter != coveredMarkings.end(); ++iter) {
+                for (vector<NonStrictMarking*>::iterator iter = coveredMarkings.begin(); 
+                        iter != coveredMarkings.end(); ++iter) {
                     if (isFirst) {
                         isFirst = false;
                         continue;
@@ -96,22 +97,15 @@
                     NonStrictMarking* covered = lookup(*iter);
                     if (covered != NULL) {
                         // cleanup
-                        for (vector<NonStrictMarking*>::iterator del = coveredMarkings.begin();
-                                del != coveredMarkings.end(); ++del)
+                        for (;iter != coveredMarkings.end(); ++iter)
                         {
-                            delete *del;
+                            delete *iter;
                         }
                         return covered;
                     }
                     delete *iter;
                 }
                 
-                // Cleanup
-                for (vector<NonStrictMarking*>::iterator del = coveredMarkings.begin();
-                    del != coveredMarkings.end(); ++del)
-                {
-                    delete *del;
-                }
             }
             return NULL;
         }
@@ -163,6 +157,132 @@
         }
 
 
+        WorkflowPWListHybrid::WorkflowPWListHybrid(
+                            TAPN::TimedArcPetriNet& tapn,  
+                            WaitingList<ptriepointer_t<MetaData*> >* w_l, 
+                            int knumber, 
+                            int nplaces, 
+                            int mage) 
+            : PWListHybrid(tapn, w_l, knumber, nplaces, mage, false, true),
+                visitor(encoder)
+        {
+            
+        }
+        
+        WorkflowPWListHybrid::~WorkflowPWListHybrid()
+        {
+            ptriepointer_t<MetaData*> begin = passed.begin();
+            while(begin != passed.end())
+            {
+                delete begin.get_meta();
+                ++ begin;
+            }
+        }
+        
+    	NonStrictMarking* WorkflowPWListHybrid::getCoveredMarking
+                                (NonStrictMarking* marking, bool useLinearSweep)
+        {
+            visitor.set_target(marking, last_pointer);
+            passed.visit(visitor);
+            if(visitor.found())
+            {
+                NonStrictMarking* m = visitor.decode();
+                return m;
+            }
+            else
+            {
+                return NULL;
+            }
+        }
+        
+        NonStrictMarking* WorkflowPWListHybrid::getUnpassed()
+        {
+            ptriepointer_t<MetaData*> it = passed.last();
+            for(; it != passed.rend(); --it)
+            {
+                if(!it.get_meta()->passed)
+                {
+                    NonStrictMarking* m = encoder.decode(it);
+                    m->meta = it.get_meta();
+                    return m;
+                }
+            }
+            return NULL;
+        }
+        
+    	bool WorkflowPWListHybrid::add(NonStrictMarking* marking)
+        {
+            discoveredMarkings++;
+            std::pair<bool, ptriepointer_t<MetaData*> > res = 
+                                        passed.insert(encoder.encode(marking));
+            
+            if (!res.first) {
+                return false;
+            }
+            else
+            {
+                MetaDataWithTraceAndEncoding* meta = 
+                                        new MetaDataWithTraceAndEncoding();
+                meta->generatedBy = marking->getGeneratedBy();
+                meta->ep = res.second;
+                meta->parent = parent;
+                meta->totalDelay = marking->calculateTotalDelay();
+                
+                res.second.set_meta(meta);
+                
+                stored++;
+                
+                // using min first waiting-list, weight is allready in pointer
+                waiting_list->add(NULL, res.second);
+                return true;           
+            }
+        }
+        
+        NonStrictMarking* WorkflowPWListHybrid::addToPassed
+                                    (NonStrictMarking* marking, bool strong)
+        {
+            discoveredMarkings++;
+            std::pair<bool, ptriepointer_t<MetaData*> > res = 
+                                        passed.insert(encoder.encode(marking));
+
+
+            
+            if (!res.first) {
+                NonStrictMarking* old = encoder.decode(res.second);
+                
+                MetaDataWithTraceAndEncoding* meta = 
+                        (MetaDataWithTraceAndEncoding*)res.second.get_meta();
+                old->setGeneratedBy(meta->generatedBy);
+                old->meta = meta;
+                last_pointer = res.second;
+                return old;
+            } else {
+                stored++;
+
+                if(strong) marking->meta = new MetaDataWithTraceAndEncoding();
+                else marking->meta = new WorkflowSoundnessMetaDataWithEncoding();
+                
+                MetaDataWithTraceAndEncoding* meta = 
+                                (MetaDataWithTraceAndEncoding*) marking->meta;
+                meta->ep = res.second;
+                meta->parent = this->parent;
+                meta->generatedBy = marking->getGeneratedBy();
+                meta->totalDelay = marking->meta->totalDelay;
+                
+                res.second.set_meta(meta);
+                last_pointer = res.second;
+                return NULL;
+            }
+        }
+        
+        void WorkflowPWListHybrid::addLastToWaiting()
+        {
+            // using min first waiting-list, weight is allready in pointer
+            waiting_list->add(NULL, last_pointer);
+        }
+        
+        
+        
 
     }
 }

=== modified file 'src/DiscreteVerification/DataStructures/WorkflowPWList.hpp'
--- src/DiscreteVerification/DataStructures/WorkflowPWList.hpp	2015-06-22 22:10:16 +0000
+++ src/DiscreteVerification/DataStructures/WorkflowPWList.hpp	2015-08-20 13:27:24 +0000
@@ -15,6 +15,7 @@
 #include "NonStrictMarking.hpp"
 #include "WaitingList.hpp"
 #include "PWList.hpp"
+#include "CoveredMarkingVisitor.h"
 
 namespace VerifyTAPN {
 namespace DiscreteVerification {
@@ -51,6 +52,28 @@
         }
 
     };
+    
+    class WorkflowPWListHybrid : public WorkflowPWListBasic, public PWListHybrid {
+    private:
+        CoveredMarkingVisitor visitor;
+        ptriepointer_t<MetaData*> last_pointer;
+    public:
+        WorkflowPWListHybrid(TAPN::TimedArcPetriNet& tapn, 
+                                WaitingList<ptriepointer_t<MetaData*> >* w_l, 
+                                int knumber, 
+                                int nplaces, 
+                                int mage);
+        ~WorkflowPWListHybrid();
+    	virtual NonStrictMarking* getCoveredMarking(NonStrictMarking* marking, bool useLinearSweep);
+        virtual NonStrictMarking* getUnpassed();
+    	virtual bool add(NonStrictMarking* marking);
+        virtual NonStrictMarking* addToPassed(NonStrictMarking* marking, bool strong);
+        virtual void addLastToWaiting();
+        virtual void setParent(NonStrictMarking* marking, NonStrictMarking*)
+        {
+            ((MetaDataWithTraceAndEncoding*)marking->meta)->parent = parent;
+        }
+    };
 
 } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */

=== modified file 'src/DiscreteVerification/DataStructures/binarywrapper.h'
--- src/DiscreteVerification/DataStructures/binarywrapper.h	2015-06-17 09:03:12 +0000
+++ src/DiscreteVerification/DataStructures/binarywrapper.h	2015-08-20 13:27:24 +0000
@@ -9,6 +9,8 @@
 #include <stdio.h>
 #include <iostream>
 #include <string.h>
+#include <assert.h>
+#include <stdint.h>
 
 #ifndef BINARYWRAPPER_H
 #define	BINARYWRAPPER_H
@@ -17,44 +19,175 @@
     typedef unsigned int uint;
     typedef unsigned char uchar;
     
+    /**
+     * Wrapper for binary data. This provides easy access to individual bits, 
+     * heap allocation and comparison. Notice that one has to make sure to 
+     * explicitly call release() if one wishes to deallocate (possibly shared data).
+     * 
+     */
     template<class T>
     class binarywrapper_t
     {
     public:
         // Constructors
+        /**
+         * Empty constructor, no data is allocated
+         */
+        inline
         binarywrapper_t();        
+        
+        /**
+         Allocates a room for at least size bits
+         */
+        inline
         binarywrapper_t(uint size);
+        
+        /**
+         * Constructor for copying over data from latest the offset'th bit.
+         * Detects overflows.
+         * @param other: wrapper to copy from
+         * @param offset: maximal number of bits to skip.
+         */
+        inline
         binarywrapper_t(const binarywrapper_t& other, uint offset);
         binarywrapper_t(const binarywrapper_t& other, uint size, uint offset, 
                                                             uint encodingsize);
         binarywrapper_t(uchar* raw, uint size, uint offset, uint encsize);
+	
+	/**
+         * Assign (not copy) raw data to pointer. Set number of bytes to size
+         * @param raw: some memory to point to
+         * @param size: number of bytes.
+         */
+        inline
         binarywrapper_t(uchar* raw, uint size);
         
-        // Destructor
+        /**
+         * Empty destructor. Does NOT deallocate data - do this with explicit
+         * call to release().
+         */
+        inline
         ~binarywrapper_t();
         
-        // Copy and clones
+        /**
+         * Makes a complete copy, including new heap-allocation
+         * @return an exact copy, but in a different area of the heap.
+         */
+        inline
         binarywrapper_t clone() const;
+        
+        /**
+         * Copy over data and meta-data from other, but insert only into target
+         * after offset bits.
+         * Notice that this can cause memory-corruption if there is not enough
+         * room in target, or to many bits are skipped.
+         * @param other: wrapper to copy from
+         * @param offset: bits to skip 
+         */
+        inline
         void copy(const binarywrapper_t& other, uint offset);
+        
+        /**
+         * Copy over size bytes form raw data. Assumes that current wrapper has
+         * enough room.
+         * @param raw: source data
+         * @param size: number of bytes to copy
+         */
+        inline
         void copy(const uchar* raw, uint size);
         
         // accessors
+        /**
+         * Get value of the place'th bit
+         * @param place: bit index
+         * @return 
+         */
+        inline
         bool at(const uint place) const;
+        
+        /**
+         * number of bytes allocated in heap
+         * @return 
+         */
+        inline
         uint size() const;
-        uchar* raw() const;
+        
+        /**
+         * Raw access to data
+         * @return 
+         */
+        inline
+        uchar*& raw();
+        
+        /**
+         * Raw access to data when in const setting
+         * @return 
+         */
+        inline
+        uchar* const_raw() const;
+        
+        /**
+         * pretty print of content
+         */
+        inline
         void print() const;
+        
+        /**
+         * finds the overhead (unused number of bits) when allocating for size
+         * bits.
+         * @param size: number of bits
+         * @return 
+         */
+        inline
         static size_t overhead(uint size);
         
         // modifiers
+        /**
+         * Change value of place'th bit 
+         * @param place: index of bit to change
+         * @param value: desired value
+         */
+        inline
         void set(const uint place, const bool value) const;
+        
+        /**
+         * Sets all memory on heap to 0 
+         */
+        inline
         void zero() const;
-        void release() const;
+        
+        /**
+         * Deallocates memory stored on heap
+         */
+        inline
+        void release();
+
         void set_meta(T data);
         T get_meta() const;
+                
+        /**
+         * Nice access to single bits
+         * @param i: index to access
+         * @return 
+         */
+        inline
         uchar operator[](int i);
+        
+        /**
+         * Removes a number of bytes from end of heap-allocated data if any is 
+         * allocated nothing happens if not. Bound-checks.
+         * @param number of bytes to remove.
+         */
+        inline
         void pop_front(unsigned short);
         
-        inline int cmp(const binarywrapper_t &other)
+        /**
+         * Compares two wrappers. Assumes that smaller number of bytes also means
+         * a smaller wrapper. Otherwise compares byte by byte.
+         * @param other: wrapper to compare to
+         * @return -1 if other is smaller, 0 if same, 1 if other is larger
+         */
+        inline int cmp(const binarywrapper_t &other) const
         {
             if(_nbytes != other._nbytes)
             {
@@ -62,63 +195,33 @@
                 else return 1;
             }
                 
-            for(int i = _nbytes - 1; i >= 0; i--)
-            {
-                if(_blob[i] < other._blob[i])
-                    return -1;
-                else if (_blob[i] > other._blob[i])
-                    return 1;
-            }
+            return memcmp(_blob, other.const_raw(), other._nbytes );
+        }
             
-            return 0;
-        }
-        
-        // Operators
+        /**
+         * Compares wrappers bytes by bytes. If sizes do not match, they are not
+         * equal. If sizes match, compares byte by byte.
+         * @param enc1 
+         * @param enc2
+         * @return true if a match, false otherwise
+         */
         inline friend bool operator==(  const binarywrapper_t &enc1, 
                                         const binarywrapper_t &enc2) {
-            if(enc1._nbytes != enc2._nbytes)
-                return false;
-            
-            for(size_t i = 0; i < enc1._nbytes; i++)
-                if(enc1._blob[i] != enc2._blob[i])
-                    return false;
-            
-            return true;
-        }
-        
-       /* inline friend bool operator <=( const binarywrapper &enc1,
-                                        const binarywrapper &enc2)
-        {
-            if(enc1.numberOfBytes != enc2.numberOfBytes)
-                return enc1.numberOfBytes < enc2.numberOfBytes;
-            
-            for(size_t i = 0; i < enc1.numberOfBytes; i++)
-                if(enc1.blob[i] < enc2.blob[i])
-                    return true;
-                else if (enc1.blob[i] > enc2.blob[i])
-                    return false;
-            
-            return true;
-        }*/
-        
-        inline friend bool operator<(   const binarywrapper_t &enc1, 
-                                        const binarywrapper_t &enc2) {
-            if(enc1._nbytes != enc2._nbytes)
-                return enc1._nbytes < enc2._nbytes;
-            
-            for(size_t i = 0; i < enc1._nbytes; i++)
-                if(enc1._blob[i] < enc2._blob[i])
-                    return true;
-                else if (enc1._blob[i] > enc2._blob[i])
-                    return false;
-            
-            return false;
+            return enc1.cmp(enc2) == 0;
         }
         
     private:
+            
+        // blob of heap-allocated data
         uchar* _blob;
-        unsigned short _nbytes;
+            
+        // number of bytes allocated on heap
+         unsigned short _nbytes;
+        
+        // meta data to carry
         T _meta;
+            
+        // masks for single-bit access
         const static uchar _masks[8];
     };
     
@@ -273,7 +376,13 @@
     }
     
     template<class T>
-    uchar* binarywrapper_t<T>::raw() const
+    uchar*& binarywrapper_t<T>::raw()
+    {
+        return _blob; 
+    }
+    
+    template<class T>
+    uchar* binarywrapper_t<T>::const_raw() const
     {
         return _blob; 
     }
@@ -292,6 +401,8 @@
     {
         if(_nbytes == 0) return;  // Special case, nothing to do!
         unsigned short int nbytes;
+        
+        // make sure we do not remove to much, but as much as we can.
         if(topop >= _nbytes)
         {
             topop = _nbytes;
@@ -340,9 +451,10 @@
     }
     
     template<class T>
-    void binarywrapper_t<T>::release() const
+    void binarywrapper_t<T>::release()
     {
         delete[] _blob;
+        _blob = NULL;
     }
     
     template<class T>

=== modified file 'src/DiscreteVerification/DataStructures/ptrie.h'
--- src/DiscreteVerification/DataStructures/ptrie.h	2015-06-22 21:03:26 +0000
+++ src/DiscreteVerification/DataStructures/ptrie.h	2015-08-20 13:27:24 +0000
@@ -1,5 +1,5 @@
 /* 
- * File:   PTrie.h
+ * File:   ptrie.h
  * Author: Peter G. Jensen
  *
  * Created on 10 June 2015, 18:44
@@ -9,10 +9,12 @@
 #define	PTRIE_H
 
 #include "binarywrapper.h"
+#include "visitor.h"
 #include <assert.h>
 #include <limits>
 #include <vector>
 #include <stdint.h>
+#include <stack>
 
 namespace ptrie
 {
@@ -35,7 +37,15 @@
             void set_meta(T);
             uint write_partial_encoding(encoding_t&) const;
             encoding_t& remainder() const;
+            
             ptriepointer_t() : container(NULL), index(0) {};
+            
+            ptriepointer_t<T>& operator=(const ptriepointer_t<T>&);
+            ptriepointer_t<T>& operator++();
+            ptriepointer_t<T>& operator--();
+            bool operator==(const ptriepointer_t<T>& other);
+            bool operator!=(const ptriepointer_t<T>& other);
+            
     };
     
     template<typename T>
@@ -45,6 +55,55 @@
     }
     
     template<typename T>
+
+    ptriepointer_t<T>& ptriepointer_t<T>::operator=
+                                                (const ptriepointer_t<T>& other)
+    {
+        container = other.container;
+        index = other.index;
+        return *this;
+    }
+    
+    template<typename T>
+    ptriepointer_t<T>& ptriepointer_t<T>::operator++()
+    {
+        ++index;
+        assert(index <= container->_next_free_entry);
+        return *this;
+    }
+    
+    template<typename T>
+    ptriepointer_t<T>& ptriepointer_t<T>::operator--()
+    {
+        --index;
+        return *this;
+    }
+    
+    template<typename T>
+    bool ptriepointer_t<T>::operator==(const ptriepointer_t<T>& other)
+    {
+        return other.container == container && other.index == index;
+    }
+    
+    template<typename T>
+    bool ptriepointer_t<T>::operator!=(const ptriepointer_t<T>& other)
+    {
+        return !(*this == other);
+    }
+    
+    /*
+    template<typename T>
+    void swap(ptriepointer<T>& lhs, ptriepointer<T>& rhs)
+    {
+        ptrie<T>* container = lhs.container;
+        uint index = lhs.index;
+        lhs.container = rhs.container;
+        lhs.index = rhs.index;
+        rhs.index = index;
+        rhs.container = container;
+    }*/
+    
+    template<typename T>
     T ptriepointer_t<T>::get_meta() const
     {
         return container->get_entry(index)->_data.get_meta();
@@ -72,7 +131,7 @@
     class ptrie_t {
         typedef binarywrapper_t<T> encoding_t;  
         friend class ptriepointer_t<T>;
-        public:
+        private:
             
             // nodes in the tree
             struct node_t
@@ -123,6 +182,12 @@
             std::pair<bool, ptriepointer_t<T> > find(const encoding_t& encoding);
             bool consistent() const;
             uint size() const { return _next_free_entry; }
+            ptriepointer_t<T> begin();
+            ptriepointer_t<T> end();
+            ptriepointer_t<T> last();
+            ptriepointer_t<T> rend();
+            
+            void visit(visitor_t<T>&);
     };
     
     template<typename T>
@@ -173,6 +238,30 @@
     }
     
     template<typename T>
+    ptriepointer_t<T> ptrie_t<T>::begin()
+    {
+        return ptriepointer_t<T>(this, 0);
+    }
+    
+    template<typename T>
+    ptriepointer_t<T> ptrie_t<T>::end()
+    {
+        return ptriepointer_t<T>(this, _next_free_entry);
+    }
+    
+    template<typename T>
+    ptriepointer_t<T> ptrie_t<T>::last()
+    {
+        return ptriepointer_t<T>(this, _next_free_entry-1);
+    }
+    
+    template<typename T>
+    ptriepointer_t<T> ptrie_t<T>::rend()
+    {
+        return ptriepointer_t<T>(this, std::numeric_limits<uint>::max());
+    }
+    
+    template<typename T>
     typename ptrie_t<T>::node_t*
     ptrie_t<T>::get_node(uint index) const
     {
@@ -218,6 +307,8 @@
     bool ptrie_t<T>::consistent() const
     {
         return true;
+        assert(_next_free_node >= _nodevector.size());
+        assert(_next_free_entry >= _entryvector.size());
         for(size_t i = 0; i < _next_free_node; ++i)
         {
             node_t* node = get_node(i);
@@ -269,6 +360,61 @@
     }
     
     template<typename T>
+    void ptrie_t<T>::visit(visitor_t<T>& visitor)
+    {
+        std::stack<std::pair<uint, uint> > waiting;
+        waiting.push(std::pair<int, uint>(-1, 0));
+
+        bool stop = false;
+        do{
+            int distance = waiting.top().first;
+            uint n_index = waiting.top().second;
+            waiting.pop();
+            
+            if(distance > -1)
+            {
+                visitor.back(distance);
+                visitor.set(distance, true);    // only high on stack
+            }
+            
+            node_t* node = get_node(n_index);
+            bool skip = false;
+            do
+            {
+
+                if(node->_highpos != 0)
+                {
+                    waiting.push(std::pair<uint, uint>(distance + 1, node->_highpos));
+                }                 
+                
+                if(node->_lowpos == 0) break;
+                else
+                {
+                    ++distance;
+                    node = get_node(node->_lowpos);
+                    skip = visitor.set(distance, false);
+                }
+                
+            } while(!skip);
+            
+            distance += 1;
+            
+            uint bucketsize = 0;
+            if(!skip)
+            {
+                if(node->_highcount > 0) bucketsize += node->_highcount;
+                if(node->_lowcount > 0) bucketsize += node->_lowcount;
+                
+                for(uint i = 0; i < bucketsize && !stop; ++i)
+                {
+                    stop = visitor.set_remainder(distance,
+                                    ptriepointer_t<T>(this, node->_entries[i]));
+                }
+            }            
+        } while(!waiting.empty() && !stop);
+    }
+    
+    template<typename T>
     bool ptrie_t<T>::best_match(const encoding_t& encoding, uint& tree_pos, 
                 uint& e_index, uint& enc_pos, uint& b_index, uint& bucketsize)
     {
@@ -316,7 +462,7 @@
         // start by creating an encoding that "points" to the "unmatched"
         // part of the encoding. Notice, this is a shallow copy, no actual
         // heap-allocation happens!
-        encoding_t s_enc = encoding_t(  encoding.raw(), 
+        encoding_t s_enc = encoding_t(  encoding.const_raw(), 
                                         (encsize - enc_pos), 
                                         enc_pos, 
                                         encsize);
@@ -341,18 +487,18 @@
                     e_index = node->_entries[b_index];
                     break;
                 }
-                else if(cmp == 1)
+                else if(cmp > 0)
                 {
                     low = b_index + 1;
                 }
-                else //if cmp == -1
+                else //if cmp < 0
                 {
                     high = b_index - 1;
                 }
                 
                 if(low > high)
                 {
-                    if(cmp == 1)
+                    if(cmp > 0)
                         b_index += 1;
                     break;
                 }
@@ -367,13 +513,13 @@
         /*int tmp;// refference debug code!
         for(tmp = 0; tmp < bucketsize; ++tmp)
         {
-            entry_t* ent = getEntry(node->entries[tmp]);
-            if(ent->data < s_enc)
+            entry_t* ent = get_entry(node->_entries[tmp]);
+            if(ent->_data.cmp(s_enc) < 0)
             {
                 continue;
             }
             else
-            if(ent->data == s_enc)
+            if(ent->_data == s_enc)
             {
                 assert(found);
                 break;
@@ -491,8 +637,8 @@
         uint enc_pos;
         uint bucketsize;
         uint e_index;
-        
-        if(best_match(encoding, tree_pos, e_index, enc_pos, bucketsize))
+        uint b_index;
+        if(best_match(encoding, tree_pos, e_index, enc_pos, b_index,  bucketsize))
         {
             return std::pair<bool, ptriepointer_t<T> >(true, 
                                                 ptriepointer_t<T>(this, e_index));
@@ -534,7 +680,7 @@
                                     remainder_size, 
                                     enc_pos, 
                                     encsize);
-        assert(n_entry->_data.raw() != encoding.raw());
+        //assert(n_entry->_data.const_raw() != encoding.const_raw());
                 
         n_entry->_nodeindex = tree_pos;
         

=== added file 'src/DiscreteVerification/DataStructures/visitor.h'
--- src/DiscreteVerification/DataStructures/visitor.h	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/visitor.h	2015-08-20 13:27:24 +0000
@@ -0,0 +1,30 @@
+/* 
+ * File:   visitor.h
+ * Author: Peter G. Jensen
+ *
+ * Created on 16 June 2015, 23:15
+ */
+
+#ifndef VISITOR_H
+#define	VISITOR_H
+
+#include <stdint.h>
+
+namespace ptrie
+{
+    template<typename T>
+    class ptriepointer_t;
+    
+    template<typename T>
+    class visitor_t
+    {
+    public:
+        virtual bool back(int index) = 0;
+        virtual bool set(int index, bool value) = 0;
+        virtual bool set_remainder(int index, ptriepointer_t<T> pointer) = 0;
+    };
+}
+
+
+#endif	/* VISITOR_H */
+

=== modified file 'src/DiscreteVerification/DiscreteVerification.cpp'
--- src/DiscreteVerification/DiscreteVerification.cpp	2015-06-17 09:03:12 +0000
+++ src/DiscreteVerification/DiscreteVerification.cpp	2015-08-20 13:27:24 +0000
@@ -53,42 +53,63 @@
 					exit(1);
 				}
 
-            	if (options.getMemoryOptimization() != VerificationOptions::NO_MEMORY_OPTIMIZATION) {
-					cout << "Workflow analysis currently does not support any memory optimizations (i.e. no PTries)." << endl;
-					exit(1);
-				}
-            	WaitingList<NonStrictMarking*>* strategy = getWaitingList<NonStrictMarking* > (query, options);
             	if(options.getWorkflowMode() == VerificationOptions::WORKFLOW_SOUNDNESS){
-            		WorkflowSoundness* verifier = new WorkflowSoundness(tapn, *initialMarking, query, options, strategy);
+            		WorkflowSoundness* verifier;
+                        if(options.getMemoryOptimization() == VerificationOptions::NO_MEMORY_OPTIMIZATION)
+                        {
+                            verifier = new WorkflowSoundness(tapn, *initialMarking, query, options, 
+                                    getWaitingList<NonStrictMarking* > (query, options));
+                        }
+                        else
+                        {
+                            verifier = new WorkflowSoundnessPTrie(tapn, *initialMarking, query, options, 
+                                    getWaitingList<ptriepointer_t<MetaData*> > (query, options));
+                        }
 
-					if(verifier->getModelType() == verifier->NOTTAWFN){
-						std::cerr << "Model is not a TAWFN!" << std::endl;
-						return -1;
-					}else if(verifier->getModelType() == verifier->ETAWFN){
-						std::cout << "Model is a ETAWFN" << std::endl << std::endl;
-					}else if(verifier->getModelType() == verifier->MTAWFN){
-						std::cout << "Model is a MTAWFN" << std::endl << std::endl;
-					}
-					VerifyAndPrint(
-                                                        tapn,
-							*verifier,
-							options,
-							query);
-					verifier->printExecutionTime(cout);
-					verifier->printMessages(cout);
+                            if(verifier->getModelType() == verifier->NOTTAWFN){
+                                    std::cerr << "Model is not a TAWFN!" << std::endl;
+                                    return -1;
+                            }else if(verifier->getModelType() == verifier->ETAWFN){
+                                    std::cout << "Model is a ETAWFN" << std::endl << std::endl;
+                            }else if(verifier->getModelType() == verifier->MTAWFN){
+                                    std::cout << "Model is a MTAWFN" << std::endl << std::endl;
+                            }
+                            VerifyAndPrint(
+                                            tapn,
+                                            *verifier,
+                                            options,
+                                            query);
+                            verifier->printExecutionTime(cout);
+                            verifier->printMessages(cout);
+#ifdef CLEANUP
+                            delete verifier;
+#endif
             	}
             	else{
             		// Assumes correct structure of net!
-            		WorkflowStrongSoundnessReachability* verifier = new WorkflowStrongSoundnessReachability(tapn, *initialMarking, query, options, strategy);
+           		WorkflowStrongSoundnessReachability* verifier;
+                        if(options.getMemoryOptimization() == VerificationOptions::NO_MEMORY_OPTIMIZATION)
+                        {
+                            verifier = new  WorkflowStrongSoundnessReachability(tapn, *initialMarking, query, options, 
+                                    getWaitingList<NonStrictMarking* > (query, options));
+                        }
+                        else
+                        {
+                            verifier = new  WorkflowStrongSoundnessPTrie(tapn, *initialMarking, query, options, 
+                                    getWaitingList<ptriepointer_t<MetaData*> > (query, options));
+                        }
             		VerifyAndPrint(
                                                         tapn,
 							*verifier,
 							options,
 							query);
 					verifier->printExecutionTime(cout);
+#ifdef CLEANUP
+                        delete verifier;
+#endif
             	}
 
-            	delete strategy;
+                
                 return 0;
             }
             

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp	2015-06-22 22:10:16 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp	2015-08-20 13:27:24 +0000
@@ -6,6 +6,7 @@
  */
 
 #include "WorkflowSoundness.hpp"
+#include <limits>
 
 namespace VerifyTAPN {
 namespace DiscreteVerification {
@@ -13,6 +14,7 @@
 WorkflowSoundness::WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list)
 : Workflow(tapn, initialMarking, query, options), passedStack(), minExec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), modelType(calculateModelType()){
     pwList = new WorkflowPWList(waiting_list);
+
 }
 
 
@@ -21,6 +23,17 @@
     
 };
 
+WorkflowSoundnessPTrie::WorkflowSoundnessPTrie(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<ptriepointer_t<MetaData*> >* waiting_list)
+: WorkflowSoundness(tapn, initialMarking, query, options) {
+    int kbound = modelType == MTAWFN ? (std::numeric_limits<int>::max() - 1) : options.getKBound();
+    pwList = new WorkflowPWListHybrid(  tapn,
+                                        waiting_list, 
+                                        kbound, 
+                                        tapn.getNumberOfPlaces(), 
+                                        tapn.getMaxConstant());
+
+}
+
 
 bool WorkflowSoundness::verify(){
 	if(addToPW(&initialMarking, NULL)){
@@ -50,6 +63,7 @@
 				return false;
 			}
 		}
+                deleteMarking(next_marking);
 	}
 
 	// Phase 2
@@ -82,6 +96,25 @@
     return passed;
 }
 
+int WorkflowSoundnessPTrie::numberOfPassed()
+{
+    int passed = 0;
+    while(passedStack.size()){
+        WorkflowSoundnessMetaDataWithEncoding* next = 
+        static_cast<WorkflowSoundnessMetaDataWithEncoding*>(passedStack.top());
+        
+        passedStack.pop();
+        if(next->passed) continue;
+        next->passed = true;
+        ++passed;
+        for(vector<MetaData*>::iterator iter = next->parents.begin();
+                iter != next->parents.end(); iter++){
+                passedStack.push(*iter);
+        }
+    }
+    return passed;
+}
+
 
 bool WorkflowSoundness::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
 	marking->cut(placeStats);
@@ -91,7 +124,9 @@
 	// Check K-bound
 	pwList->setMaxNumTokensIfGreater(size);
 	if(modelType == ETAWFN && size > options.getKBound()) {
-		lastMarking = marking;
+                if(lastMarking != NULL) deleteMarking(lastMarking);
+                lastMarking = marking;
+                setMetaParent(lastMarking);
 		return true;	// Terminate false
 	}
 
@@ -101,8 +136,6 @@
         NonStrictMarking* old = pwList->addToPassed(marking, false);
 	if(old == NULL){
                 isNew = true;
-		marking->meta = new WorkflowSoundnessMetaData();
-                marking->setParent(parent);
 	} else  {
             delete marking;
             marking = old;
@@ -130,11 +163,14 @@
 			marking->meta->totalDelay = min(marking->meta->totalDelay, parent->meta->totalDelay);	// Transition
                         // keep track of shortest trace
                         if (marking->meta->totalDelay < minExec) {
+                            if(lastMarking != NULL) deleteMarking(lastMarking);
+
                             minExec = marking->meta->totalDelay;
                             lastMarking = marking;
                             return false;
                         }
 		}else{
+                        if(lastMarking != NULL) deleteMarking(lastMarking);
 			lastMarking = marking;
 			return true;	// Terminate false
 		}
@@ -143,15 +179,18 @@
 		if(isNew){
                         pwList->addLastToWaiting();
 			if(parent != NULL && marking->canDeadlock(tapn, 0)){
+                                if(lastMarking != NULL) deleteMarking(lastMarking);
 				lastMarking = marking;
 				return true;
 			}
 			if(modelType == MTAWFN && checkForCoveredMarking(marking)){
-				lastMarking = marking;
+                                if(lastMarking != NULL) deleteMarking(lastMarking);
+                                lastMarking = marking;
 				return true;	// Terminate false
 			}
 		}
 	}
+        deleteMarking(marking);
 	return false;
 }
 
@@ -162,6 +201,14 @@
 
 }
 
+void WorkflowSoundnessPTrie::addParentMeta(MetaData* meta, MetaData* parent)
+{
+    assert(meta != NULL);
+    assert(parent != NULL);
+    WorkflowSoundnessMetaDataWithEncoding* markingmeta = ((WorkflowSoundnessMetaDataWithEncoding*)meta);
+    markingmeta->parents.push_back(parent);
+
+}
 
 bool WorkflowSoundness::checkForCoveredMarking(NonStrictMarking* marking){
 	if(marking->size() <= options.getKBound()){
@@ -193,6 +240,64 @@
 }
 
 
+void WorkflowSoundnessPTrie::getTrace(NonStrictMarking* marking){
+
+        PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList);
+
+        stack < NonStrictMarking*> printStack;
+
+        if(marking != NULL){
+            printStack.push(marking);
+            
+            MetaDataWithTraceAndEncoding* meta = 
+                static_cast<MetaDataWithTraceAndEncoding*>(marking->meta);
+            if(meta)
+            {
+                marking->setGeneratedBy(meta->generatedBy);
+
+                meta = meta->parent;
+                while(meta != NULL)
+                {
+                    NonStrictMarking* next = pwhlist->decode(meta->ep);
+                    printStack.push(next);
+                    next->setGeneratedBy(meta->generatedBy);
+                    printStack.top()->setParent(next);
+                    meta = meta->parent;
+                }
+            }
+            printStack.top()->setGeneratedBy(NULL);
+        }
+
+#ifdef CLEANUP
+        stack < NonStrictMarking*> clearStack = printStack;
+#endif
+        printXMLTrace(marking, printStack, query, tapn);
+#ifdef CLEANUP
+        while(!clearStack.empty())
+        {
+            if(clearStack.top() == lastMarking) break;  // deleted elsewhere
+            delete clearStack.top();
+            clearStack.pop();
+        }
+#endif
+}
+
+
+void WorkflowSoundnessPTrie::setMetaParent(NonStrictMarking* marking){
+    PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList);
+    
+    if(marking->meta == NULL)
+    {
+        marking->meta = new MetaDataWithTraceAndEncoding();
+    }
+
+    MetaDataWithTraceAndEncoding* mte = 
+                static_cast<MetaDataWithTraceAndEncoding*>(marking->meta);
+    mte->parent = pwhlist->parent;
+    mte->generatedBy = marking->getGeneratedBy();
+}
+
+
 
 WorkflowSoundness::ModelType WorkflowSoundness::calculateModelType() {
             bool isin, isout;

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp	2015-06-22 22:10:16 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp	2015-08-20 13:27:24 +0000
@@ -26,6 +26,7 @@
 #include "../DataStructures/WaitingList.hpp"
 #include "Workflow.hpp"
 
+using namespace ptrie;
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
@@ -71,6 +72,23 @@
 
 };
 
+
+class WorkflowSoundnessPTrie : public WorkflowSoundness
+{
+public:
+	WorkflowSoundnessPTrie(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<ptriepointer_t<MetaData*> >* waiting_list);
+    
+        virtual void addParentMeta(MetaData* meta, MetaData* parent);
+        virtual int numberOfPassed();
+        virtual void deleteMarking(NonStrictMarking* marking)
+        {
+            delete marking;
+        }
+        virtual void getTrace(NonStrictMarking* marking);
+protected:
+        virtual void setMetaParent(NonStrictMarking*);
+};
+
 } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */
 #endif /* NONSTRICTSEARCH_HPP_ */

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp	2015-06-22 22:10:16 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp	2015-08-20 13:27:24 +0000
@@ -16,6 +16,10 @@
                 findInOut();
         };
         
+        WorkflowStrongSoundnessReachability::WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
+        : Workflow(tapn, initialMarking, query, options), maxValue(-1), outPlace(NULL){
+            findInOut();
+        };
         
         void WorkflowStrongSoundnessReachability::findInOut()
         {
@@ -25,8 +29,27 @@
                     break;
                 }
             }
-        };
-
+        }
+        
+        WorkflowStrongSoundnessPTrie::WorkflowStrongSoundnessPTrie(
+                                TAPN::TimedArcPetriNet& tapn,
+                                NonStrictMarking& initialMarking,
+                                AST::Query* query,
+                                VerificationOptions options,
+                                WaitingList<ptriepointer_t<MetaData*> >* waiting_list) :
+                                WorkflowStrongSoundnessReachability(
+                                    tapn, 
+                                    initialMarking, 
+                                    query, 
+                                    options)
+        {
+            pwList = new WorkflowPWListHybrid(  tapn,
+                                                waiting_list, 
+                                                options.getKBound(), 
+                                                tapn.getNumberOfPlaces(), 
+                                                tapn.getMaxConstant());
+        }
+       
         bool WorkflowStrongSoundnessReachability::verify() {
             
             if (outPlace == NULL)
@@ -53,6 +76,7 @@
                 bool noDelay = false;
                 Result res = successorGenerator.generateAndInsertSuccessors(*next_marking);
                 if (res == ADDTOPW_RETURNED_TRUE) {
+                    clearTrace();
                     return true;
                 } else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) {
                     noDelay = true;
@@ -65,7 +89,7 @@
                     marking->setGeneratedBy(NULL);
                    
                     if (addToPW(marking, next_marking)) {
-
+                        clearTrace();
                         lastMarking = marking;
                         return true;
                     }
@@ -77,6 +101,7 @@
                     // remove childless markings from stack
                     while(!trace.empty() && trace.top()->getNumberOfChildren() <= 1){
                             trace.top()->meta->inTrace = false;
+                            deleteMarking(trace.top());
                             trace.pop();
                     }
                     if(trace.empty()){
@@ -108,6 +133,64 @@
             printXMLTrace(lastMarking, printStack, query, tapn);
         }
 
+        void WorkflowStrongSoundnessPTrie::getTrace() {
+
+            PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList);
+            
+            std::stack < NonStrictMarking*> printStack;
+            
+            NonStrictMarking* next = lastMarking;
+            if(next != NULL)
+            {
+
+                printStack.push(next);
+                MetaDataWithTraceAndEncoding* meta = 
+                        static_cast<MetaDataWithTraceAndEncoding*>(next->meta);
+
+                if(meta == NULL)
+                {
+                    // We assume the parent was not deleted on return
+                    NonStrictMarking* parent = (NonStrictMarking*)lastMarking->getParent();                
+                    if(parent != NULL) meta = 
+                        static_cast<MetaDataWithTraceAndEncoding*>(parent->meta);
+                    delete parent;
+                }
+                else
+                {
+                    meta = meta->parent;
+                }
+                                
+                while(meta != NULL)
+                {
+                    next = pwhlist->decode(meta->ep);
+                    next->setGeneratedBy(meta->generatedBy);
+                    printStack.top()->setParent(next);
+                    printStack.push(next);                    
+                    meta = meta->parent;
+                }
+            }
+#ifdef CLEANUP
+            std::stack < NonStrictMarking*> cleanup = printStack;
+#endif
+            printXMLTrace(lastMarking, printStack, query, tapn);
+            
+#ifdef CLEANUP
+            while(!cleanup.empty())
+            {
+                if(cleanup.top() != lastMarking) // deleted elsewhere
+                {
+                    delete cleanup.top();
+                    cleanup.pop();
+                }
+                else
+                {
+                    break;
+                }
+            }
+#endif
+        }
+        
+        
         bool WorkflowStrongSoundnessReachability::addToPW(NonStrictMarking* marking, NonStrictMarking* parent) {
             marking->cut(placeStats);
             marking->setParent(parent);
@@ -135,6 +218,7 @@
                         // make sure we can print trace
                         marking->setNumberOfChildren(1);
                         maxValue = totalDelay;
+                        deleteMarking(old);
                         return true;
                     } else {
                         // search again to find maxdelay
@@ -145,12 +229,12 @@
                         // fall through on purpose
                     }
                 } else {
+                    deleteMarking(old);
                     delete marking;
                     // already seen this maxage/marking combination
                     return false;
                 }
             } else {
-                marking->meta = new MetaData();
                 marking->meta->totalDelay = totalDelay;
             }
             
@@ -166,10 +250,14 @@
                 // if terminal, update max_value and last marking of trace
                 if(maxValue < marking->meta->totalDelay) {
                     maxValue = marking->meta->totalDelay;
+                    if(lastMarking != NULL) deleteMarking(lastMarking);
                     lastMarking = marking;
                     return false;
                 }
             }
+            
+            deleteMarking(marking);
+            
             return false;
         }
         
@@ -179,5 +267,25 @@
             old->setParent(marking->getParent());
         }
 
+        void WorkflowStrongSoundnessPTrie::swapData(NonStrictMarking* marking, NonStrictMarking* parent)
+        {
+            PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList);
+            MetaDataWithTraceAndEncoding* meta = 
+                static_cast<MetaDataWithTraceAndEncoding*>(parent->meta);
+
+            meta->generatedBy = marking->getGeneratedBy();
+            meta->parent = pwhlist->parent;
+        }
+        
+        void WorkflowStrongSoundnessPTrie::clearTrace()
+        {
+            if(!trace.empty()) trace.pop(); // pop parent, used in getTrace
+            while(!trace.empty())
+            {
+                delete trace.top();
+                trace.pop();
+            }
+        }
+        
     } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp	2015-06-22 22:10:16 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp	2015-08-20 13:27:24 +0000
@@ -53,6 +53,26 @@
         int validChildren;
 };
 
+class WorkflowStrongSoundnessPTrie : public WorkflowStrongSoundnessReachability
+{
+public:
+    WorkflowStrongSoundnessPTrie(
+            TAPN::TimedArcPetriNet& tapn,
+            NonStrictMarking& initialMarking, 
+            AST::Query* query, 
+            VerificationOptions options, 
+            WaitingList<ptriepointer_t<MetaData*> >* waiting_list);
+    virtual void getTrace();
+    virtual void deleteMarking(NonStrictMarking* marking)
+    {
+        delete marking;
+    }
+
+protected:
+        virtual void swapData(NonStrictMarking* marking, NonStrictMarking* old);
+        virtual void clearTrace();
+};
+
 } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */
 #endif /* NONSTRICTSEARCH_HPP_ */