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

[Peter Gjøl Jensen]

Refactorings to ease ptrie-implementation.

[Jiri Srba (srba)]

I get these warnings:

src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp:14:4: note:
      in instantiation of member function
      'VerifyTAPN::DiscreteVerification::AbstractNaiveVerification<VerifyTAPN::DiscreteVerification::PWListBase,
      VerifyTAPN::DiscreteVerification::NonStrictMarking>::AbstractNaiveVerification'
      requested here
        : AbstractNaiveVerification<PWListBase,NonStrictMarking>(tapn, i...
          ^

and

src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp:71:66: warning:
      field 'lastMarking' will be initialized after field 'successorGenerator'
      [-Wreorder]
        : Verification<U>(tapn, initialMarking, query, options), lastMar...
                                                                 ^
src/DiscreteVerification/VerificationTypes/Workflow.hpp:36:11: note: in
      instantiation of member function
      'VerifyTAPN::DiscreteVerification::AbstractNaiveVerification<VerifyTAPN::DiscreteVerification::WorkflowPWListBasic,
      VerifyTAPN::DiscreteVerification::NonStrictMarking>::AbstractNaiveVerification'
      requested here
        : AbstractNaiveVerification<WorkflowPWListBasic,NonStrictMarking...
          ^

review: Needs Fixing

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

348. By Peter Gjøl Jensen on 2015-06-24

Warning fix

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

Should be fixed now.

=== modified file 'src/DiscreteVerification/DataStructures/PWList.hpp'
--- src/DiscreteVerification/DataStructures/PWList.hpp	2015-06-22 21:03:26 +0000
+++ src/DiscreteVerification/DataStructures/PWList.hpp	2015-06-24 13:24:40 +0000
@@ -40,7 +40,7 @@
 	inline void setMaxNumTokensIfGreater(int i){ if(i>maxNumTokensInAnyMarking)	maxNumTokensInAnyMarking = i; };
     };
 
-class PWList : public PWListBase {
+class PWList : public virtual PWListBase {
 public:
 	typedef std::vector<NonStrictMarking*> NonStrictMarkingList;
 	typedef google::sparse_hash_map<size_t, NonStrictMarkingList> HashMap;
@@ -55,11 +55,6 @@
 		return (waiting_list->size() > 0);
 	};
 
-	virtual bool addToWaiting(NonStrictMarking* marking){
-		waiting_list->add(marking, marking);
-		return true;
-	}
-
 	virtual long long size() const {
 		return stored;
 	};
@@ -76,13 +71,19 @@
 	WaitingList<NonStrictMarking*>* waiting_list;
 };
 
-class PWListHybrid : public PWListBase {
+class PWListHybrid : public virtual PWListBase {
         public:
             typedef unsigned int uint;
 
         public:
 
-            PWListHybrid(TAPN::TimedArcPetriNet& tapn, WaitingList<ptriepointer_t<MetaData*> >* w_l, int knumber, int nplaces, int mage, bool isLiveness, bool makeTrace) :
+            PWListHybrid(   TAPN::TimedArcPetriNet& tapn,  
+                            WaitingList<ptriepointer_t<MetaData*> >* w_l, 
+                            int knumber, 
+                            int nplaces, 
+                            int mage, 
+                            bool isLiveness, 
+                            bool makeTrace) :
             PWListBase(isLiveness),
             waiting_list(w_l),
             makeTrace(makeTrace),
@@ -121,10 +122,11 @@
             virtual bool add(NonStrictMarking* marking);
             virtual NonStrictMarking* getNextUnexplored();
 
-        public:
+        protected:
 
             WaitingList<ptriepointer_t<MetaData*> >* waiting_list;
             bool makeTrace;
+        public:
             MetaDataWithTraceAndEncoding* parent;             
             ptrie_t<MetaData*> passed;
             MarkingEncoder<MetaData*, NonStrictMarking> encoder;

=== modified file 'src/DiscreteVerification/DataStructures/WaitingList.cpp'
--- src/DiscreteVerification/DataStructures/WaitingList.cpp	2015-06-17 09:03:12 +0000
+++ src/DiscreteVerification/DataStructures/WaitingList.cpp	2015-06-24 13:24:40 +0000
@@ -11,7 +11,7 @@
     template <>
     int MinFirstWaitingList<NonStrictMarking*>::calculateWeight(NonStrictMarking* marking)
     {
-            return marking->meta->totalDelay;
+        return marking->meta->totalDelay;
     }
 
     template <>

=== modified file 'src/DiscreteVerification/DataStructures/WaitingList.hpp'
--- src/DiscreteVerification/DataStructures/WaitingList.hpp	2015-06-22 21:03:26 +0000
+++ src/DiscreteVerification/DataStructures/WaitingList.hpp	2015-06-24 13:24:40 +0000
@@ -136,8 +136,7 @@
 	virtual T pop();
 	virtual size_t size() { return queue.size(); };
 protected:
-        virtual int calculateWeight(T payload);
-        virtual int calculateWeight(NonStrictMarkingBase* marking);       
+        virtual int calculateWeight(T payload); 
 
 	priority_queue queue;
 	AST::Query* query;
@@ -342,20 +341,18 @@
 	queue.push(weighted_item);
 }
 
-
-template <class T>
-int MinFirstWaitingList<T>::calculateWeight(NonStrictMarkingBase* marking)
-{
-    assert(false);
-    return 0;
-}
-
-template <class T>
-int MinFirstWaitingList<T>::calculateWeight(T)
-{
-    assert(false);
-    return 0;
-}
+template <class T>
+int MinFirstWaitingList<T>::calculateWeight(T tmp)
+{
+    assert(false);
+    return 0;
+}
+
+template <>
+int MinFirstWaitingList<NonStrictMarking*>::calculateWeight(NonStrictMarking* tmp);
+
+template <>
+int MinFirstWaitingList<ptriepointer_t<MetaData*> >::calculateWeight(ptriepointer_t<MetaData*> );
 
 template <class T>
 T MinFirstWaitingList<T>::pop()

=== modified file 'src/DiscreteVerification/DataStructures/WorkflowPWList.cpp'
--- src/DiscreteVerification/DataStructures/WorkflowPWList.cpp	2015-06-22 21:03:26 +0000
+++ src/DiscreteVerification/DataStructures/WorkflowPWList.cpp	2015-06-24 13:24:40 +0000
@@ -129,15 +129,23 @@
             return NULL;
         }
 
-        NonStrictMarking* WorkflowPWList::addToPassed(NonStrictMarking* marking) {
+        NonStrictMarking* WorkflowPWList::addToPassed(
+                                        NonStrictMarking* marking, bool strong) 
+        {  
             discoveredMarkings++;
             NonStrictMarking* existing = lookup(marking);
             if (existing != NULL) {
+                last = existing;                
                 return existing;
             } else {
+                last = marking;
                 NonStrictMarkingList& m = markings_storage[marking->getHashKey()];
                 stored++;
                 m.push_back(marking);
+
+                if(strong) marking->meta = new MetaData();
+                else marking->meta = new WorkflowSoundnessMetaData();
+
                 return NULL;
             }
         }

=== modified file 'src/DiscreteVerification/DataStructures/WorkflowPWList.hpp'
--- src/DiscreteVerification/DataStructures/WorkflowPWList.hpp	2015-06-14 22:27:50 +0000
+++ src/DiscreteVerification/DataStructures/WorkflowPWList.hpp	2015-06-24 13:24:40 +0000
@@ -19,15 +19,36 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-    class WorkflowPWList : public PWList {
-
+    class WorkflowPWListBasic : virtual public PWListBase
+    {
+    public:
+    	virtual NonStrictMarking* getCoveredMarking(NonStrictMarking* marking, bool useLinearSweep) = 0;
+        virtual NonStrictMarking* getUnpassed() = 0;
+    	virtual bool add(NonStrictMarking* marking) = 0;
+        virtual NonStrictMarking* addToPassed(NonStrictMarking* marking, bool strong) = 0;
+        virtual void addLastToWaiting() = 0;
+        virtual void setParent(NonStrictMarking*, NonStrictMarking*) = 0;
+    };
+    
+    class WorkflowPWList : public WorkflowPWListBasic, public PWList {
+    private:
+        NonStrictMarking* last;
     public:
         WorkflowPWList(WaitingList<NonStrictMarking*>* w_l);
-    	NonStrictMarking* getCoveredMarking(NonStrictMarking* marking, bool useLinearSweep);
-        NonStrictMarking* getUnpassed();
-    	bool add(NonStrictMarking* marking);
-        NonStrictMarking* addToPassed(NonStrictMarking* marking);
+    	virtual NonStrictMarking* getCoveredMarking(NonStrictMarking* marking, bool useLinearSweep);
+        virtual NonStrictMarking* getUnpassed();
+    	virtual bool add(NonStrictMarking* marking);
+        virtual NonStrictMarking* addToPassed(NonStrictMarking* marking, bool strong);
         NonStrictMarking* lookup(NonStrictMarking* marking);
+        
+        virtual void addLastToWaiting(){
+		waiting_list->add(last, last);
+	}
+        
+        virtual void setParent(NonStrictMarking* marking, NonStrictMarking* parent)
+        {
+            marking->setParent(parent);
+        }
 
     };
 

=== modified file 'src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp'
--- src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp	2015-06-22 21:03:26 +0000
+++ src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp	2015-06-24 13:24:40 +0000
@@ -68,7 +68,7 @@
 
         template<typename T,typename U>
         AbstractNaiveVerification<T,U>::AbstractNaiveVerification(TAPN::TimedArcPetriNet& tapn, U& initialMarking, AST::Query* query, VerificationOptions options, T* pwList)
-        : Verification<U>(tapn, initialMarking, query, options), lastMarking(NULL), successorGenerator(tapn, *this), pwList(pwList) {
+        : Verification<U>(tapn, initialMarking, query, options), successorGenerator(tapn, *this), lastMarking(NULL), pwList(pwList) {
 
         };
 

=== modified file 'src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp'
--- src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2015-06-16 18:44:21 +0000
+++ src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2015-06-24 13:24:40 +0000
@@ -98,7 +98,7 @@
 
 void ReachabilitySearchPTrie::getTrace(){
 	stack < NonStrictMarking*> printStack;
-        PWListHybrid* pwhlist = (PWListHybrid*)(this->pwList);
+        PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList);
         MetaDataWithTraceAndEncoding* next = pwhlist->parent;
         NonStrictMarking* last = lastMarking;
         printStack.push(lastMarking);

=== modified file 'src/DiscreteVerification/VerificationTypes/Workflow.hpp'
--- src/DiscreteVerification/VerificationTypes/Workflow.hpp	2015-06-14 22:27:50 +0000
+++ src/DiscreteVerification/VerificationTypes/Workflow.hpp	2015-06-24 13:24:40 +0000
@@ -29,27 +29,29 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-template<typename T>
-class Workflow : public AbstractNaiveVerification<WorkflowPWList,T> {
+
+class Workflow : public AbstractNaiveVerification<WorkflowPWListBasic,NonStrictMarking> {
 public:    
-	Workflow(TAPN::TimedArcPetriNet& tapn, T& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list);
+	Workflow(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
+        : AbstractNaiveVerification<WorkflowPWListBasic,NonStrictMarking>(tapn, initialMarking, query, options, NULL), in(NULL), out(NULL){
+    
+            for (TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); 
+                    iter != tapn.getPlaces().end(); iter++) {
+                if ((*iter)->getType() == Dead) {
+                    (*iter)->setType(Std);
+                }
+            }
+        }
 	virtual void printExecutionTime(ostream& stream) = 0;
         
 protected:
+    virtual void deleteMarking(NonStrictMarking* marking){
+
+    };
 	TimedPlace* in;
 	TimedPlace* out;
 };
 
-template<typename T>
-Workflow<T>::Workflow(TAPN::TimedArcPetriNet& tapn, T& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list)
-: AbstractNaiveVerification<WorkflowPWList,T>(tapn, initialMarking, query, options, new WorkflowPWList(waiting_list)), in(NULL), out(NULL){
-    for (TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); iter != tapn.getPlaces().end(); iter++) {
-        if ((*iter)->getType() == Dead) {
-            (*iter)->setType(Std);
-        }
-    }
-}
-
 } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */
 #endif /* NONSTRICTSEARCH_HPP_ */
\ No newline at end of file

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp	2015-06-22 21:34:37 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp	2015-06-24 13:24:40 +0000
@@ -11,10 +11,17 @@
 namespace DiscreteVerification {
 
 WorkflowSoundness::WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list)
-: Workflow<NonStrictMarking>(tapn, initialMarking, query, options, waiting_list), passedStack(), minExec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), modelType(calculateModelType()){
-
+: Workflow(tapn, initialMarking, query, options), passedStack(), minExec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), modelType(calculateModelType()){
+    pwList = new WorkflowPWList(waiting_list);
 }
 
+
+WorkflowSoundness::WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
+: Workflow(tapn, initialMarking, query, options), passedStack(), minExec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), modelType(calculateModelType()){
+    
+};
+
+
 bool WorkflowSoundness::verify(){
 	if(addToPW(&initialMarking, NULL)){
 		return false;
@@ -22,10 +29,12 @@
 
 	// Phase 1
 	while(pwList->hasWaitingStates()){
-		NonStrictMarking& next_marking = *pwList->getNextUnexplored();
-		tmpParent = &next_marking;
+
+		NonStrictMarking* next_marking = pwList->getNextUnexplored();
+		tmpParent = next_marking;
 		bool noDelay = false;
-		Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
+
+		Result res = successorGenerator.generateAndInsertSuccessors(*next_marking);
 		if(res == ADDTOPW_RETURNED_TRUE){
 			return false;
 		}  else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) {
@@ -33,11 +42,11 @@
 		}
 
 		// Generate next markings
-		if(!noDelay && isDelayPossible(next_marking)){
-			NonStrictMarking* marking = new NonStrictMarking(next_marking);
+		if(!noDelay && isDelayPossible(*next_marking)){
+			NonStrictMarking* marking = new NonStrictMarking(*next_marking);
 			marking->incrementAge();
 			marking->setGeneratedBy(NULL);
-			if(addToPW(marking, &next_marking)){
+			if(addToPW(marking, next_marking)){
 				return false;
 			}
 		}
@@ -45,18 +54,7 @@
 
 	// Phase 2
         // mark all as passed which ends in a final marking        
-        int passed = 0;
-        while(passedStack.size()){
-            WorkflowSoundnessMetaData* next = 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((WorkflowSoundnessMetaData*)*iter);
-            }
-        }
+        int passed = numberOfPassed();
         
         if(passed < pwList->stored){
                 lastMarking = pwList->getUnpassed();
@@ -66,6 +64,25 @@
 	}
 }
 
+int WorkflowSoundness::numberOfPassed()
+{
+    int passed = 0;
+    while(passedStack.size()){
+        WorkflowSoundnessMetaData* next = 
+                    static_cast<WorkflowSoundnessMetaData*>(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);
 
@@ -79,8 +96,9 @@
 	}
 
 	// Map to existing marking if any
-	NonStrictMarking* old = pwList->addToPassed(marking);
         bool isNew = false;
+        marking->setParent(parent);
+        NonStrictMarking* old = pwList->addToPassed(marking, false);
 	if(old == NULL){
                 isNew = true;
 		marking->meta = new WorkflowSoundnessMetaData();
@@ -89,20 +107,17 @@
             delete marking;
             marking = old;
         }
-
-	WorkflowSoundnessMetaData* marking_meta_data = ((WorkflowSoundnessMetaData*)marking->meta);
-
+ 
 	// add to parents_set
 	if(parent != NULL){
-		WorkflowSoundnessMetaData* parent_meta_data = ((WorkflowSoundnessMetaData*)parent->meta);
-		marking_meta_data->parents.push_back(parent_meta_data);
+                addParentMeta(marking->meta, parent->meta);
 		if(marking->getGeneratedBy() == NULL){
-			marking_meta_data->totalDelay = min(marking_meta_data->totalDelay, parent_meta_data->totalDelay+1);	// Delay
+			marking->meta->totalDelay = min(marking->meta->totalDelay, parent->meta->totalDelay+1);	// Delay
 		}else{
-			marking_meta_data->totalDelay = min(marking_meta_data->totalDelay, parent_meta_data->totalDelay);	// Transition
+			marking->meta->totalDelay = min(marking->meta->totalDelay, parent->meta->totalDelay);	// Transition
 		}
 	}else{
-		marking_meta_data->totalDelay = 0;
+		marking->meta->totalDelay = 0;
 	}
 
 
@@ -110,15 +125,14 @@
 	// Test if final place
 	if(marking->numberOfTokensInPlace(out->getIndex()) > 0){
 		if(size == 1){
-			marking_meta_data = ((WorkflowSoundnessMetaData*)marking->meta);
-			marking_meta_data->parents.push_back(((WorkflowSoundnessMetaData*)parent->meta));
+                        passedStack.push(marking->meta);
 			// Set min
-			marking_meta_data->totalDelay = min(marking_meta_data->totalDelay, ((WorkflowSoundnessMetaData*)parent->meta)->totalDelay);	// Transition
-                        passedStack.push(marking_meta_data);
+			marking->meta->totalDelay = min(marking->meta->totalDelay, parent->meta->totalDelay);	// Transition
                         // keep track of shortest trace
-                        if (marking_meta_data->totalDelay < minExec) {
-                            minExec = marking_meta_data->totalDelay;
+                        if (marking->meta->totalDelay < minExec) {
+                            minExec = marking->meta->totalDelay;
                             lastMarking = marking;
+                            return false;
                         }
 		}else{
 			lastMarking = marking;
@@ -127,7 +141,7 @@
 	}else{
 		// If new marking
 		if(isNew){
-                        pwList->addToWaiting(marking);
+                        pwList->addLastToWaiting();
 			if(parent != NULL && marking->canDeadlock(tapn, 0)){
 				lastMarking = marking;
 				return true;
@@ -141,6 +155,14 @@
 	return false;
 }
 
+void WorkflowSoundness::addParentMeta(MetaData* meta, MetaData* parent)
+{
+    WorkflowSoundnessMetaData* markingmeta = ((WorkflowSoundnessMetaData*)meta);
+    markingmeta->parents.push_back(parent);
+
+}
+
+
 bool WorkflowSoundness::checkForCoveredMarking(NonStrictMarking* marking){
 	if(marking->size() <= options.getKBound()){
 		return false;	// Do not run check on small markings (invoke more rarely)
@@ -148,16 +170,17 @@
 
 	NonStrictMarking* covered = pwList->getCoveredMarking(marking, (marking->size() > linearSweepTreshold));
 	if(covered != NULL){
-		coveredMarking = covered;
-		return true;
+            coveredMarking = covered;
+            return true;
 	}
 
 	return false;
 }
 
-void WorkflowSoundness::getTrace(NonStrictMarking* base){
+void WorkflowSoundness::getTrace(NonStrictMarking* marking){
+
 	stack < NonStrictMarking*> printStack;
-        NonStrictMarking* next = lastMarking;
+        NonStrictMarking* next = marking;
         if(next != NULL){
             do{
                 printStack.push(next);
@@ -165,13 +188,12 @@
             } while(next);
         }
         
-	if(options.getXmlTrace()){
-		printXMLTrace(lastMarking, printStack, query, tapn);
-	} else {
-		printHumanTrace(lastMarking, printStack, query->getQuantifier());
-	}
+        printXMLTrace(marking, printStack, query, tapn);
+
 }
 
+
+
 WorkflowSoundness::ModelType WorkflowSoundness::calculateModelType() {
             bool isin, isout;
             bool hasInvariant = false;

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp	2015-06-14 22:27:50 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp	2015-06-24 13:24:40 +0000
@@ -29,18 +29,20 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-class WorkflowSoundness : public Workflow<NonStrictMarking> {
+class WorkflowSoundness : public Workflow {
 public:
         enum ModelType{
 		MTAWFN, ETAWFN, NOTTAWFN
 	};
         
 	WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list);
+	WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options);
+
 	virtual ~WorkflowSoundness();
 	bool verify();
-	virtual void getTrace(){
-		return getTrace(lastMarking);
-	}
+        virtual void getTrace(NonStrictMarking* marking);
+	virtual void getTrace() {this->getTrace(lastMarking);};
+        
 	void printExecutionTime(ostream& stream){
 		stream << "Minimum execution time: " << minExec << endl;
 	}
@@ -51,14 +53,17 @@
 		}
 	}
         inline const ModelType getModelType() const{ return modelType; }
+        virtual int numberOfPassed();
+        
 protected:
 	bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);
 	bool checkForCoveredMarking(NonStrictMarking* marking);
-	void getTrace(NonStrictMarking* base);
         ModelType calculateModelType();
+        virtual void addParentMeta(MetaData* meta, MetaData* parent);
+        virtual void setMetaParent(NonStrictMarking*){};
         
 protected:
-    stack<WorkflowSoundnessMetaData*> passedStack;
+    stack<MetaData*> passedStack;
     int minExec;
     unsigned int linearSweepTreshold;
     NonStrictMarking* coveredMarking;

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp	2015-06-14 22:27:50 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp	2015-06-24 13:24:40 +0000
@@ -11,8 +11,14 @@
     namespace DiscreteVerification {
 
         WorkflowStrongSoundnessReachability::WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list)
-        : Workflow<NonStrictMarking>(tapn, initialMarking, query, options, waiting_list), maxValue(-1), outPlace(NULL){
-            // Find timer place and store as out
+        : Workflow(tapn, initialMarking, query, options), maxValue(-1), outPlace(NULL){
+                pwList = new WorkflowPWList(waiting_list);
+                findInOut();
+        };
+        
+        
+        void WorkflowStrongSoundnessReachability::findInOut()
+        {
             for (TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); iter != tapn.getPlaces().end(); ++iter) {
                 if ((*iter)->getTransportArcs().empty() && (*iter)->getInputArcs().empty()) {
                     outPlace = *iter;
@@ -22,23 +28,30 @@
         };
 
         bool WorkflowStrongSoundnessReachability::verify() {
+            
+            if (outPlace == NULL)
+            {
+                lastMarking = &initialMarking;
+                return true;
+            }
+                
             if (addToPW(&initialMarking, NULL)) {
                 return true;
             }
 
             //Main loop
             while (pwList->hasWaitingStates()) {
-                NonStrictMarking& next_marking = 
-                        static_cast<NonStrictMarking&>(*pwList->getNextUnexplored());
-                tmpParent = &next_marking;
+                NonStrictMarking* next_marking = 
+                        static_cast<NonStrictMarking*>(pwList->getNextUnexplored());
+                tmpParent = next_marking;
                 
                 // push onto trace
-                trace.push(&next_marking);
-                next_marking.meta->inTrace = true;
+                trace.push(next_marking);
+                next_marking->meta->inTrace = true;
                 validChildren = 0;
 
                 bool noDelay = false;
-                Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
+                Result res = successorGenerator.generateAndInsertSuccessors(*next_marking);
                 if (res == ADDTOPW_RETURNED_TRUE) {
                     return true;
                 } else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) {
@@ -46,26 +59,20 @@
                 }
 
                 // Generate delays markings
-                if (!noDelay && isDelayPossible(next_marking)) {
-                    NonStrictMarking* marking = new NonStrictMarking(next_marking);
+                if (!noDelay && isDelayPossible(*next_marking)) {
+                    NonStrictMarking* marking = new NonStrictMarking(*next_marking);
                     marking->incrementAge();
                     marking->setGeneratedBy(NULL);
                    
-                    if (addToPW(marking, &next_marking)) {
+                    if (addToPW(marking, next_marking)) {
+
                         lastMarking = marking;
                         return true;
                     }
                     
-                    if(marking->meta &&
-                       marking->meta->totalDelay > options.getWorkflowBound()){
-                        // if the bound is exceeded, terminate
-                        marking->setParent(&next_marking);
-                        lastMarking = marking;
-                        return true;
-                    }
                 }
                 if(validChildren != 0){
-                    next_marking.setNumberOfChildren(validChildren);
+                    next_marking->setNumberOfChildren(validChildren);
                 } else {
                     // remove childless markings from stack
                     while(!trace.empty() && trace.top()->getNumberOfChildren() <= 1){
@@ -94,15 +101,11 @@
 
             } while (next != NULL && next->getParent() != NULL);
 
-            if (printStack.top() != next) {
+            if (next != NULL && printStack.top() != next) {
                 printStack.push(next);
             }
 
-            if (options.getXmlTrace()) {
-                printXMLTrace(lastMarking, printStack, query, tapn);
-            } else {
-                    printHumanTrace(lastMarking, printStack, query->getQuantifier());
-            }
+            printXMLTrace(lastMarking, printStack, query, tapn);
         }
 
         bool WorkflowStrongSoundnessReachability::addToPW(NonStrictMarking* marking, NonStrictMarking* parent) {
@@ -122,7 +125,8 @@
 
             /* Handle max */
             // Map to existing marking if any
-            NonStrictMarking* old = (NonStrictMarking*)pwList->addToPassed(marking);
+            NonStrictMarking* old = (NonStrictMarking*)pwList->addToPassed(marking, true);
+            
             if(old != NULL) {
                 if(old->meta->totalDelay < totalDelay) {
                     if(old->meta->inTrace){
@@ -130,14 +134,11 @@
                         lastMarking = marking;
                         // make sure we can print trace
                         marking->setNumberOfChildren(1);
-                        trace.push(marking);
                         maxValue = totalDelay;
                         return true;
                     } else {
                         // search again to find maxdelay
-                        // copy data from new
-                        old->setParent(marking->getParent());
-                        old->setGeneratedBy(marking->getGeneratedBy());
+                        swapData(marking, old);
                         old->meta->totalDelay = totalDelay;
                         delete marking;
                         marking = old;
@@ -153,19 +154,30 @@
                 marking->meta->totalDelay = totalDelay;
             }
             
+            // if we reached bound
+            if(marking->meta->totalDelay > options.getWorkflowBound()) return true;
+            
+            
             if(marking->numberOfTokensInPlace(outPlace->getIndex()) == 0){
                 // if nonterminal, add to waiting
-                pwList->addToWaiting(marking);
+                pwList->addLastToWaiting();
                 ++validChildren;
             } else {
                 // if terminal, update max_value and last marking of trace
                 if(maxValue < marking->meta->totalDelay) {
                     maxValue = marking->meta->totalDelay;
                     lastMarking = marking;
+                    return false;
                 }
             }
             return false;
         }
+        
+        void WorkflowStrongSoundnessReachability::swapData(NonStrictMarking* marking, NonStrictMarking* old)
+        {
+            old->setGeneratedBy(marking->getGeneratedBy());
+            old->setParent(marking->getParent());
+        }
 
     } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp	2015-06-14 22:27:50 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp	2015-06-24 13:24:40 +0000
@@ -17,21 +17,36 @@
 namespace VerifyTAPN {
 namespace DiscreteVerification {
 
-class WorkflowStrongSoundnessReachability : public Workflow<NonStrictMarking>{
+class WorkflowStrongSoundnessReachability : public Workflow{
 public:
 
 	WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list);
 
+        WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options);
+        
+        ~WorkflowStrongSoundnessReachability()
+        {
+            pwList->deleteWaitingList();
+            delete lastMarking;
+            delete pwList;
+        }
+        
 	bool verify();
-	void getTrace();
+	virtual void getTrace();
 
 	void printExecutionTime(ostream& stream){
 		stream << "Maximum execution time: " << (maxValue * tapn.getGCD()) << endl;
 	}
         
 
+        
+
 protected:
+        void findInOut();
 	bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);
+        virtual void swapData(NonStrictMarking* marking, NonStrictMarking* old);
+        virtual void clearTrace(){};    // cleanup
+        
 protected:
 	int maxValue;
 	TimedPlace* outPlace;