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

[Mathias Grund Sørensen]

Adds workflow soundness and strong soundness verification.

[Jiri Srba (srba)]

Tested and works as it should. Just make sure that the normal verification (EG, AG, EG, AF) is
not influenced in any way.

review: Approve

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

Line 701-702, why this change in access-level?
Is it reasonable to just ignore unused options, and give no warnings? (timedarts, ptries)?

The implementation of "getUnpassed" in the PW-list seems like a very inefficient waiting-list-ish thing.
"getCoveredMarking" also seems very inefficient, maybe a special hash-function would solve this problem (use only place/token-count as seed of the hash).
Also, why are these in the PWList implementation and not in WorkflowPWList?

line 984-991 and 999-1005, please make a variable instead of constantly casting to WorkflowSoundnessMetaData, it makes the code unreadable.
I am not entirely sure, but I think you need a delete marking at line 1323 (you don't add it to the PW-list and you don't use it anywhere else) - there is a delete in the original reachabilitysearch-addtoPW.

I agree with Jiri that the changes do not affect the normal verification.

review: Needs Information

[Jiri Srba (srba)]

Agree, timedarts and Ptrie should give a error (warning). Btw. we hope Peter that
you will be able to add Ptrie to this at some point. This should not be too difficult, correct?

The other remarks make also good sense to me, Mathias, can you take a look please?

The only thing I am not sure about is the hashing on token-count. I am not sure how
this can help with discovery of covered markings on the passed/waiting list?

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

> Line 701-702, why this change in access-level?
> Is it reasonable to just ignore unused options, and give no warnings?
> (timedarts, ptries)?

Yes, I will add a warning in this case.

> The implementation of "getUnpassed" in the PW-list seems like a very
> inefficient waiting-list-ish thing.

Yes, this is not very elaborate, but it will only be run once ever, so the overhead of doing something elaborate would most likely outweigh the benefit IMO.

> "getCoveredMarking" also seems very inefficient, maybe a special hash-function
> would solve this problem (use only place/token-count as seed of the hash).

Yes, this appears very simple. A more elaborate method which hashes on submarkings is used as an alternative in method checkForCoveringMarking, but it turns out the naive linear sweep is generally faster (due to growth in number of sub markings w.r.t. marking size).

But yes, I considered some kind of clever hashing, but due to time constraints I didn't have time come up with one. In any ways, I am not sure this will be as easy as it sounds. And also, I am not sure you will be able to get better performance than the method hashing on submarkings anyways, but you are welcome to see if you can come up with something clever.

Anyways, I will change this so that both methods are on WorkflowPWList to keep the logic together and use a flag for which one to use.

> Also, why are these in the PWList implementation and not in WorkflowPWList?

Yes, these could be moved to WorkflowPWList, I just made them in PWList in case I needed them for strong soundness (which uses normal PWList), but I didn't so I'll just move them.

> line 984-991 and 999-1005, please make a variable instead of constantly
> casting to WorkflowSoundnessMetaData, it makes the code unreadable.

OK, will do.

> I am not entirely sure, but I think you need a delete marking at line 1323
> (you don't add it to the PW-list and you don't use it anywhere else) - there
> is a delete in the original reachabilitysearch-addtoPW.

No, it shouldn't as the marking is looked up in the passed storage and this code is only executed if there is a match, thus a delete would delete it from the passed storage. However, I think the marking used to call AddToPW could be delete on line 1292 if there is a match is found.

> I agree with Jiri that the changes do not affect the normal verification.

Good. I'll implement the comments tomorrow and you can have another look.

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

I have implemented Peters comments now. I also found a bug in the covering check so apparently both types of checks would be run if there was no match due to missing return (woops...) - this should increase performance on the examples where covering check was slow.

You are welcome to take a look again to see how it looks.

The change in access modifier was due to a problem I had with overriding something, but I got it to work correctly, so I have reverted it to protected.

[Jiri Srba (srba)]

I just tested and all works fine. Peter and Jakob, please, take a quick look so that we can merge it to trunk.

review: Approve

[Jakob Taankvist (jakob-taankvist)]

I just had a quick look i think it looks good, however to avoid code redundancy shouldn't the lookup function (line 308) be used in all the addToPassed functions? And do we really need this many addToPassed functions (don't they all do the same)?

review: Needs Information

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

332. By Mathias Grund Sørensen on 2013-10-25

Refactored addToPassed to use the lookup method.

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

> I just had a quick look i think it looks good, however to avoid code
> redundancy shouldn't the lookup function (line 308) be used in all the
> addToPassed functions?

Yes, this will improve code quality, I have done that now.

> And do we really need this many addToPassed functions
> (don't they all do the same)?

Yes, the workflow algorithm handles metadata manually in the algorithm so the metadata should not be set in the AddToPassed method (this will cause problems as is) - this is the only difference.

I have now implemented all your comments (Jakob and Peter), so please, reconsider your review.

[Jakob Taankvist (jakob-taankvist)]

review: Approve

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

I think that the inheritance of Reachabilitysearch in Workflow is a bit unfortunate. It seems that the only methods really used from this inheritance is "getTrace" and "isDelayPossible", the rest are overwritten. Also, why is the pwList defined as a PWList instead of WorkflowPWList? And is there any reason for the new methods in PWList (they are all unused)?

I suggest to let Workflow inherit from Verification instead, define getTrace and isDelayPossible here, move pwList here also, but change the type to WorkflowPWList. This will allow you to remove the new methods from PWList and maintain a more concise inheritance model.

review: Needs Information

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

333. By Mathias Grund Sørensen on 2013-10-27

Changed workflow soundness PWList* to WorkflowPWList*

334. By Mathias Grund Sørensen on 2013-10-27

Removed workflow.cpp as it contained no implementations.

335. By Mathias Grund Sørensen on 2013-10-27

Removed unneeded methods for PWListBase.

336. By Mathias Grund Sørensen on 2013-10-27

Refactored to remove Workflow supertype.

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

> I think that the inheritance of Reachabilitysearch in Workflow is a bit
> unfortunate. It seems that the only methods really used from this inheritance
> is "getTrace" and "isDelayPossible", the rest are overwritten.

Yes, I agree the current inheritance hierarchy is not ideal. I have simplified it a little by removing the intermediate workflow class, but I think that to make the hierarchy nice, a larger refactoring has to be done, which I suggest is done in a new branch after merging.

I strongly suggest creating a DiscreteVerification class which contains shared methods + variables for all discrete methods (basically what TimeDartVerification does for semi-symbolic algorithms) and then workflow classes can just inherit from this.

Unless you strongly feel that this branch is too messy w.r.t. inheritance hierarchy, I think we should save it for a new branch as it will touch a lot of code.

> Also, why is
> the pwList defined as a PWList instead of WorkflowPWList? And is there any
> reason for the new methods in PWList (they are all unused)?

This has now been changed. Lookup still has to be global, as it is used in strong soundness search, which uses regular PWLists

> I suggest to let Workflow inherit from Verification instead, define getTrace
> and isDelayPossible here, move pwList here also, but change the type to
> WorkflowPWList. This will allow you to remove the new methods from PWList and
> maintain a more concise inheritance model.

I have made some changes to the inheritance model (not exactly those you suggest). Please consider my comment above and let me know if you still think the model should be improved before merging.

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

337. By Mathias Grund Sørensen on 2013-10-27

Removed code in comments.

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

> This has now been changed. Lookup still has to be global, as it is used in strong soundness search, which uses regular PWLists

No you don't. I just removed it and put it in the workflow-pw-list, it compiles just fine. (also if you search the diff, there is no "new PWList..-" anywhere)

I poked a bit around in the code and ended up doing something like this:
lp:~peter-gjoel/verifydtapn/workflowForTrunk

> Unless you strongly feel that this branch is too messy w.r.t. inheritance hierarchy, I think we should save it for a new branch as it will touch a lot of code.

Agreed. I will approve it for now, and then we can sort out the rest in the new branch.

review: Approve

=== modified file 'src/Core/ArgsParser.cpp'
--- src/Core/ArgsParser.cpp	2013-05-08 11:22:45 +0000
+++ src/Core/ArgsParser.cpp	2013-10-27 17:10:01 +0000
@@ -17,6 +17,7 @@
 static const std::string XML_TRACE_OPTION = "xml-trace";
 static const std::string LEGACY = "legacy";
 static const std::string KEEP_DEAD = "keep-dead-tokens";
+static const std::string WORKFLOW = "workflow";
 
 std::ostream& operator<<(std::ostream& out, const Switch& flag) {
 	flag.print(out);
@@ -162,6 +163,12 @@
     parsers.push_back(
             boost::make_shared<Switch > ("x", XML_TRACE_OPTION,
             "Output trace in xml format for TAPAAL."));
+
+    parsers.push_back(
+    		 boost::make_shared<SwitchWithArg > ("w", WORKFLOW,
+    		            "Workflow mode.\n - 0: Disabled\n - 1: Soundness (and min)\n - 2: Strong Soundness (and max)",
+    		            0));
+
 };
 
 void ArgsParser::printHelp() const {
@@ -309,6 +316,20 @@
 }
 
 
+VerificationOptions::WorkflowMode intToWorkflowTypeEnum(int i) {
+	switch (i) {
+	case 0:
+		return VerificationOptions::NOT_WORKFLOW;
+	case 1:
+		return VerificationOptions::WORKFLOW_SOUNDNESS;
+	case 2:
+		return VerificationOptions::WORKFLOW_STRONG_SOUNDNESS;
+	default:
+		std::cout << "Unknown workflow option specified." << std::endl;
+		exit(1);
+	}
+}
+
 VerificationOptions::Trace intToEnum(int i) {
 	switch (i) {
 	case 0:
@@ -370,8 +391,14 @@
 	assert(map.find(XML_TRACE_OPTION) != map.end());
 	bool xml_trace = boost::lexical_cast<bool>(
 			map.find(XML_TRACE_OPTION)->second);
+
+	assert(map.find(WORKFLOW) != map.end());
+	VerificationOptions::WorkflowMode workflow = intToWorkflowTypeEnum(
+			tryParseInt(*map.find(WORKFLOW)));
+
+
         
 	return VerificationOptions(modelFile, queryFile, search, verification, memoptimization, kbound, trace,
-			xml_trace, max_constant, keep_dead);
+			xml_trace, max_constant, keep_dead, workflow);
 }
 }

=== modified file 'src/Core/ArgsParser.hpp'
--- src/Core/ArgsParser.hpp	2013-08-13 20:59:28 +0000
+++ src/Core/ArgsParser.hpp	2013-10-27 17:10:01 +0000
@@ -80,7 +80,7 @@
 	class ArgsParser {
 		typedef std::vector< boost::shared_ptr<Switch> > parser_vec;
 	public:
-		ArgsParser() : parsers(), version(2,1,0) { initialize(); };
+		ArgsParser() : parsers(), version(2,2,0) { initialize(); };
 		virtual ~ArgsParser() {};
 
 		VerificationOptions parse(int argc, char* argv[]) const;

=== modified file 'src/Core/QueryParser/AST.hpp'
--- src/Core/QueryParser/AST.hpp	2013-08-09 21:47:22 +0000
+++ src/Core/QueryParser/AST.hpp	2013-10-27 17:10:01 +0000
@@ -218,6 +218,7 @@
 
 			Quantifier getQuantifier() const { return quantifier; }
 			const Expression& getChild() const { return *expr; }
+			void setQuantifier(Quantifier q){ quantifier = q; }
 		private:
 			Quantifier quantifier;
 			Expression* expr;

=== modified file 'src/Core/TAPN/TimedPlace.hpp'
--- src/Core/TAPN/TimedPlace.hpp	2013-07-25 21:04:53 +0000
+++ src/Core/TAPN/TimedPlace.hpp	2013-10-27 17:10:01 +0000
@@ -62,6 +62,7 @@
 			inline const TransportArc::Vector& getTransportArcs() const { return transportArcs; }
 			inline const InhibitorArc::Vector& getInhibitorArcs() const { return inhibitorArcs; }
 			inline const TimedInputArc::Vector& getInputArcs() const { return inputArcs; }
+			inline const OutputArc::Vector& getOutputArcs() const { return outputArcs; }
 
 		private: // data
 			PlaceType type;

=== modified file 'src/Core/VerificationOptions.hpp'
--- src/Core/VerificationOptions.hpp	2013-05-08 11:12:08 +0000
+++ src/Core/VerificationOptions.hpp	2013-10-27 17:10:01 +0000
@@ -26,6 +26,10 @@
             NO_MEMORY_OPTIMIZATION, PTRIE
         };
 
+        enum WorkflowMode{
+        	NOT_WORKFLOW, WORKFLOW_SOUNDNESS, WORKFLOW_STRONG_SOUNDNESS
+        };
+
         VerificationOptions() {
         }
 
@@ -39,8 +43,8 @@
                 Trace trace,
                 bool xml_trace,
                 bool useGlobalMaxConstants,
-                bool keepDeadTokens
-                ) : inputFile(inputFile),
+                bool keepDeadTokens,
+               	WorkflowMode workflow) : inputFile(inputFile),
         queryFile(queryFile),
         searchType(searchType),
         verificationType(verificationType),
@@ -49,7 +53,8 @@
         trace(trace),
         xml_trace(xml_trace),
         useGlobalMaxConstants(useGlobalMaxConstants),
-        keepDeadTokens(keepDeadTokens) {
+        keepDeadTokens(keepDeadTokens),
+        workflow(workflow){
 
         };
 
@@ -94,6 +99,15 @@
         inline const bool getKeepDeadTokens() const {
             return keepDeadTokens;
         };
+
+        inline const WorkflowMode getWorkflowMode() const {
+		   return workflow;
+	   };
+
+       inline bool isWorkflow() const{
+    	   return workflow != NOT_WORKFLOW;
+       }
+
     private:
         std::string inputFile;
         std::string queryFile;
@@ -105,6 +119,7 @@
         bool xml_trace;
         bool useGlobalMaxConstants;
         bool keepDeadTokens;
+        WorkflowMode workflow;
     };
 
     std::ostream& operator<<(std::ostream& out, const VerificationOptions& options);

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarking.hpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2013-08-01 21:55:57 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2013-10-27 17:10:01 +0000
@@ -18,6 +18,8 @@
 
 namespace VerifyTAPN {
 namespace DiscreteVerification {
+
+	class NonStrictMarking;
  
    struct MetaData {
     public:
@@ -30,6 +32,20 @@
         const TAPN::TimedTransition* generatedBy;
     };
     
+    struct WorkflowSoundnessMetaData : public MetaData {
+	   public:
+    	WorkflowSoundnessMetaData() : parents(new vector<NonStrictMarking*>), min(INT_MAX) {};
+		   vector<NonStrictMarking*>* parents;
+		   int min;
+	   };
+
+    struct WorkflowStrongSoundnessMetaData : public MetaData {
+   	   public:
+    	WorkflowStrongSoundnessMetaData() : parents(new vector<NonStrictMarking*>) {};
+   		   vector<NonStrictMarking*>* parents;
+   	   };
+
+
     // ugly forward declaration
     template<class MetaData>
     struct EncodingPointer;
@@ -42,17 +58,16 @@
     class NonStrictMarking : public NonStrictMarkingBase{
     public:
         NonStrictMarking():NonStrictMarkingBase(), meta(new MetaData()){}
-	NonStrictMarking(const TAPN::TimedArcPetriNet& tapn, const std::vector<int>& v):NonStrictMarkingBase(tapn, v){}
-	NonStrictMarking(const NonStrictMarkingBase& nsm):NonStrictMarkingBase(nsm){
+	NonStrictMarking(const TAPN::TimedArcPetriNet& tapn, const std::vector<int>& v): NonStrictMarkingBase(tapn, v), meta(NULL){}
+	NonStrictMarking(const NonStrictMarkingBase& nsm):NonStrictMarkingBase(nsm), meta(NULL){
 
         }
-        NonStrictMarking(const NonStrictMarking& nsm):NonStrictMarkingBase(nsm){
+        NonStrictMarking(const NonStrictMarking& nsm):NonStrictMarkingBase(nsm), meta(NULL){
 
         }
     public:
         MetaData* meta;
     };
-    
 
 } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2013-07-26 21:59:47 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2013-10-27 17:10:01 +0000
@@ -216,14 +216,12 @@
         }
 
         std::ostream& operator<<(std::ostream& out, NonStrictMarkingBase& x) {
-            out << "-";
             for (PlaceList::iterator iter = x.places.begin(); iter != x.places.end(); iter++) {
-                out << "place " << iter->place->getId() << " has tokens (age, count): ";
                 for (TokenList::iterator it = iter->tokens.begin(); it != iter->tokens.end(); it++) {
-                    out << "(" << it->getAge() << ", " << it->getCount() << ") ";
+                    out << "(" << iter->place->getName() << ", "<< it->getAge() << ", " << it->getCount() << ")";
                 }
                 if (iter != x.places.end() - 1) {
-                    out << endl;
+                	out << ", ";
                 }
             }
 

=== modified file 'src/DiscreteVerification/DataStructures/PWList.cpp'
--- src/DiscreteVerification/DataStructures/PWList.cpp	2013-08-26 14:17:55 +0000
+++ src/DiscreteVerification/DataStructures/PWList.cpp	2013-10-27 17:10:01 +0000
@@ -30,11 +30,24 @@
 	}
         stored++;
 	m.push_back(marking);
-        marking->meta = new MetaData();
+    marking->meta = new MetaData();
 	waiting_list->add(marking, marking);
 	return true;
 }
 
+NonStrictMarking* PWList::addToPassed(NonStrictMarking* marking){
+		NonStrictMarking* existing = lookup(marking);
+		if(existing != NULL){
+			return existing;
+		}else{
+			NonStrictMarkingList& m = markings_storage[marking->getHashKey()];
+			stored++;
+			m.push_back(marking);
+			marking->meta = new MetaData();
+			return marking;
+		}
+	}
+
 NonStrictMarking* PWList::getNextUnexplored(){
 	return waiting_list->pop();
 }

=== modified file 'src/DiscreteVerification/DataStructures/PWList.hpp'
--- src/DiscreteVerification/DataStructures/PWList.hpp	2013-08-10 20:30:06 +0000
+++ src/DiscreteVerification/DataStructures/PWList.hpp	2013-10-27 17:10:01 +0000
@@ -17,7 +17,7 @@
 
 namespace VerifyTAPN {
 namespace DiscreteVerification {
-    
+
     class PWListBase {
     public:
         PWListBase() : stored(0), discoveredMarkings(0), maxNumTokensInAnyMarking(-1), isLiveness(false) {};
@@ -26,16 +26,17 @@
     	int discoveredMarkings;
 	int maxNumTokensInAnyMarking;
         bool isLiveness;
-        
+
         virtual bool hasWaitingStates() = 0;
         virtual long long size() const = 0;
         virtual bool add(NonStrictMarking* marking) = 0;
-	virtual NonStrictMarking* getNextUnexplored() = 0;
+        virtual NonStrictMarking* lookup(NonStrictMarking* marking){ return NULL; }
+        virtual NonStrictMarking* getNextUnexplored() = 0;
         virtual long long explored()= 0;
         virtual ~PWListBase(){};
-	inline void setMaxNumTokensIfGreater(int i){ if(i>maxNumTokensInAnyMarking) maxNumTokensInAnyMarking = i; };
+	inline void setMaxNumTokensIfGreater(int i){ if(i>maxNumTokensInAnyMarking)	maxNumTokensInAnyMarking = i; };
     };
-    
+
 class PWList : public PWListBase {
 public:
 	typedef std::vector<NonStrictMarking*> NonStrictMarkingList;
@@ -51,14 +52,32 @@
 		return (waiting_list->size() > 0);
 	};
 
+	virtual NonStrictMarking* lookup(NonStrictMarking* marking){
+		NonStrictMarkingList& m = markings_storage[marking->getHashKey()];
+			for(NonStrictMarkingList::const_iterator iter = m.begin();
+					iter != m.end();
+					iter++){
+				if((*iter)->equals(*marking)){
+					return *iter;
+				}
+			}
+		return NULL;
+	}
+
+	virtual bool addToWaiting(NonStrictMarking* marking){
+		waiting_list->add(marking, marking);
+		return true;
+	}
+
 	virtual long long size() const {
 		return stored;
 	};
 
         virtual long long explored() {return waiting_list->size();};
-        
+
 public: // modifiers
 	virtual bool add(NonStrictMarking* marking);
+	virtual NonStrictMarking* addToPassed(NonStrictMarking* marking);
 	virtual NonStrictMarking* getNextUnexplored();
 
 public:

=== modified file 'src/DiscreteVerification/DataStructures/WaitingList.hpp'
--- src/DiscreteVerification/DataStructures/WaitingList.hpp	2013-08-26 14:17:55 +0000
+++ src/DiscreteVerification/DataStructures/WaitingList.hpp	2013-10-27 17:10:01 +0000
@@ -127,6 +127,24 @@
 };
 
 template <class T>
+class WorkflowMinFirstWaitingList : public WaitingList<T>{
+public:
+	typedef std::priority_queue<WeightedItem<T>, std::vector<WeightedItem<T> >, less<T> > priority_queue;
+public:
+	WorkflowMinFirstWaitingList(AST::Query* q) : queue(), query(q) { };
+	virtual ~WorkflowMinFirstWaitingList();
+public:
+	virtual void add(NonStrictMarkingBase* weight, T* payload);
+	virtual T* peek();
+	virtual T* pop();
+	virtual size_t size() { return queue.size(); };
+private:
+	int calculateWeight(NonStrictMarking* payload);
+	priority_queue queue;
+	AST::Query* query;
+};
+
+template <class T>
 class RandomStackWaitingList : public StackWaitingList<T>{
 public:
 	typedef std::priority_queue<WeightedItem<T>, std::vector<WeightedItem<T> >, less<T> > priority_queue;
@@ -336,6 +354,54 @@
 }
 
 template <class T>
+void WorkflowMinFirstWaitingList<T>::add(NonStrictMarkingBase* weight, T* payload)
+{
+	assert(false);
+	WeightedItem<T> weighted_item;
+	weighted_item.item = payload;
+	weighted_item.weight = 0;
+	queue.push(weighted_item);
+}
+
+template <>
+inline void WorkflowMinFirstWaitingList<NonStrictMarking>::add(NonStrictMarkingBase* weight, NonStrictMarking* payload)
+{
+	WeightedItem<NonStrictMarking> weighted_item;
+	weighted_item.item = payload;
+	weighted_item.weight = calculateWeight(payload);
+	queue.push(weighted_item);
+}
+
+template <class T>
+T* WorkflowMinFirstWaitingList<T>::pop()
+{
+	WeightedItem<T> weighted_item = queue.top();
+	T* marking = weighted_item.item;
+	queue.pop();
+	return marking;
+}
+
+template <class T>
+T* WorkflowMinFirstWaitingList<T>::peek()
+{
+	WeightedItem<T> weighted_item = queue.top();
+	T* marking = weighted_item.item;
+	return marking;
+}
+
+template <class T>
+int WorkflowMinFirstWaitingList<T>::calculateWeight(NonStrictMarking* payload)
+{
+	return ((WorkflowSoundnessMetaData*)payload->meta)->min;
+}
+
+template <class T>
+WorkflowMinFirstWaitingList<T>::~WorkflowMinFirstWaitingList()
+{
+}
+
+
+template <class T>
 void RandomWaitingList<T>::add(NonStrictMarkingBase* weight, T* payload)
 {
 	WeightedItem<T> weighted_item;

=== added file 'src/DiscreteVerification/DataStructures/WorkflowPWList.hpp'
--- src/DiscreteVerification/DataStructures/WorkflowPWList.hpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/WorkflowPWList.hpp	2013-10-27 17:10:01 +0000
@@ -0,0 +1,150 @@
+/*
+ * PWList.hpp
+ *
+ *  Created on: 01/03/2012
+ *      Author: MathiasGS
+ */
+
+#ifndef WORKFLOWPWLIST_HPP_
+#define WORKFLOWPWLIST_HPP_
+
+#include "WaitingList.hpp"
+#include <iostream>
+#include "google/sparse_hash_map"
+#include  "NonStrictMarking.hpp"
+#include "NonStrictMarking.hpp"
+#include "WaitingList.hpp"
+#include "PWList.hpp"
+
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+    class WorkflowPWList : public PWList {
+    public:
+    	NonStrictMarking* getCoveredMarking(NonStrictMarking* marking, bool useLinearSweep){
+			if(useLinearSweep){
+				for(HashMap::const_iterator iter = markings_storage.begin(); iter != markings_storage.end(); ++iter){
+					for(NonStrictMarkingList::const_iterator m_iter = iter->second.begin(); m_iter != iter->second.end(); m_iter++){
+						if((*m_iter)->size() >= marking->size()){
+							continue;
+						}
+
+						// Test if m_iter is covered by marking
+						PlaceList::const_iterator marking_place_iter = marking->getPlaceList().begin();
+
+						bool tokensCovered = true;
+						for(PlaceList::const_iterator m_place_iter = (*m_iter)->getPlaceList().begin(); m_place_iter != (*m_iter)->getPlaceList().end(); ++m_place_iter){
+							while(marking_place_iter != marking->getPlaceList().end() && marking_place_iter->place != m_place_iter->place){
+								++marking_place_iter;
+							}
+
+							if(marking_place_iter == marking->getPlaceList().end()){
+								tokensCovered = false;
+								break;	// Place not covered in marking
+							}
+
+							TokenList::const_iterator marking_token_iter = marking_place_iter->tokens.begin();
+							for(TokenList::const_iterator m_token_iter = m_place_iter->tokens.begin(); m_token_iter != m_place_iter->tokens.end(); ++m_token_iter){
+								while(marking_token_iter != marking_place_iter->tokens.end() && marking_token_iter->getAge() != m_token_iter->getAge()){
+									++marking_token_iter;
+								}
+
+								if(marking_token_iter == marking_place_iter->tokens.end() || marking_token_iter->getCount() < m_token_iter->getCount()){
+									tokensCovered = false;
+									break;
+								}
+							}
+
+							if(!tokensCovered)	break;
+						}
+
+						if(tokensCovered){
+							return *m_iter;
+						}
+					}
+				}
+			}else{
+				vector<NonStrictMarking*> coveredMarkings;
+				coveredMarkings.push_back(new NonStrictMarking(*marking));
+				for(PlaceList::const_iterator p_iter = marking->getPlaceList().begin(); p_iter != marking->getPlaceList().end(); ++p_iter){
+					for(TokenList::const_iterator t_iter = p_iter->tokens.begin(); t_iter != p_iter->tokens.end(); ++t_iter){
+						for(int i = 1; i <= t_iter->getCount(); ++i){
+							vector<NonStrictMarking*> toAdd;
+							for(vector<NonStrictMarking*>::iterator iter = coveredMarkings.begin(); iter != coveredMarkings.end(); ++iter){
+								NonStrictMarking* new_marking = new NonStrictMarking(**iter);
+								for(int ii = i; ii > 0; --ii){
+									new_marking->removeToken(p_iter->place->getIndex(), t_iter->getAge());
+								}
+								toAdd.push_back(new_marking);
+							}
+							for(vector<NonStrictMarking*>::iterator iter = toAdd.begin(); iter != toAdd.end(); ++iter){
+								coveredMarkings.push_back(*iter);
+							}
+						}
+					}
+				}
+
+				bool isFirst = true;
+				for(vector<NonStrictMarking*>::iterator iter = coveredMarkings.begin(); iter != coveredMarkings.end(); ++iter){
+					if(isFirst){
+						isFirst = false;
+						continue;
+					}
+					NonStrictMarking* covered = lookup(*iter);
+					if(covered != NULL){
+						return covered;
+					}
+					delete *iter;
+				}
+			}
+			return NULL;
+		}
+
+        NonStrictMarking* getUnpassed(){
+			for(HashMap::iterator hmiter = markings_storage.begin(); hmiter != markings_storage.end(); hmiter++){
+				for(NonStrictMarkingList::const_iterator iter = hmiter->second.begin();
+						iter != hmiter->second.end();
+						iter++){
+					if(!(*iter)->meta->passed){
+						return *iter;
+					}
+				}
+			}
+			return NULL;
+		}
+
+
+    	WorkflowPWList(WaitingList<NonStrictMarking>* w_l) : PWList(w_l, false) {};
+    	bool add(NonStrictMarking* marking){
+    		discoveredMarkings++;
+    		NonStrictMarkingList& m = markings_storage[marking->getHashKey()];
+    		for(NonStrictMarkingList::const_iterator iter = m.begin();
+    				iter != m.end();
+    				iter++){
+    			if((*iter)->equals(*marking)){
+ 	                    return false;
+    			}
+    		}
+    	        stored++;
+    		m.push_back(marking);
+    		waiting_list->add(marking, marking);
+    		return true;
+    	}
+
+    	NonStrictMarking* addToPassed(NonStrictMarking* marking){
+    		NonStrictMarking* existing = lookup(marking);
+    		if(existing != NULL){
+    			return existing;
+    		}else{
+    			NonStrictMarkingList& m = markings_storage[marking->getHashKey()];
+    			stored++;
+    			m.push_back(marking);
+    			return marking;
+    		}
+    	}
+
+    };
+
+} /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */
+#endif /* PWLIST_HPP_ */

=== modified file 'src/DiscreteVerification/DiscreteVerification.cpp'
--- src/DiscreteVerification/DiscreteVerification.cpp	2013-08-10 20:30:06 +0000
+++ src/DiscreteVerification/DiscreteVerification.cpp	2013-10-27 17:10:01 +0000
@@ -47,7 +47,49 @@
             std::cout << options << std::endl;
 
             // Select verification method
-            if (options.getVerificationType() == VerificationOptions::DISCRETE) {
+            if(options.getWorkflowMode() != VerificationOptions::NOT_WORKFLOW){
+            	if (options.getVerificationType() == VerificationOptions::TIMEDART) {
+					cout << "Workflow analysis currently only supports discrete exploration (i.e. not TimeDarts)." << endl;
+					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);
+
+					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(
+							*verifier,
+							options,
+							query);
+					verifier->printExecutionTime(cout);
+					verifier->printMessages(cout);
+            	}
+            	else{
+            		// Assumes correct structure of net!
+            		WorkflowStrongSoundnessReachability* verifier = new WorkflowStrongSoundnessReachability(tapn, *initialMarking, query, options, strategy);
+            		VerifyAndPrint(
+							*verifier,
+							options,
+							query);
+					verifier->printExecutionTime(cout);
+            	}
+
+            	delete strategy;
+
+            }
+            else if (options.getVerificationType() == VerificationOptions::DISCRETE) {
                 
                 if (options.getMemoryOptimization() == VerificationOptions::PTRIE) {
                     //TODO fix initialization
@@ -137,7 +179,7 @@
         }
 
         template<typename T> void VerifyAndPrint(Verification<T>& verifier, VerificationOptions& options, AST::Query* query) {
-            bool result = (query->getQuantifier() == AG || query->getQuantifier() == AF) ? !verifier.verify() : verifier.verify();
+            bool result = (!options.isWorkflow() && (query->getQuantifier() == AG || query->getQuantifier() == AF)) ? !verifier.verify() : verifier.verify();
 
             verifier.printStats();
             verifier.printTransitionStatistics();
@@ -150,7 +192,7 @@
                 std::cout << verifier.maxUsedTokens() << std::endl;
 
             if (options.getTrace() == VerificationOptions::SOME_TRACE) {
-                if ((query->getQuantifier() == EF && result) || (query->getQuantifier() == AG && !result) || (query->getQuantifier() == EG && result) || (query->getQuantifier() == AF && !result)) {
+                if ((query->getQuantifier() == EF && result) || (query->getQuantifier() == AG && !result) || (query->getQuantifier() == EG && result) || (query->getQuantifier() == AF && !result) || (options.isWorkflow())) {
                     verifier.getTrace();
                 } else {
                     std::cout << "A trace could not be generated due to the query result" << std::endl;

=== modified file 'src/DiscreteVerification/DiscreteVerification.hpp'
--- src/DiscreteVerification/DiscreteVerification.hpp	2013-07-26 21:59:47 +0000
+++ src/DiscreteVerification/DiscreteVerification.hpp	2013-10-27 17:10:01 +0000
@@ -23,6 +23,8 @@
 #include "VerificationTypes/ReachabilitySearch.hpp"
 #include "VerificationTypes/TimeDartReachabilitySearch.hpp"
 #include "VerificationTypes/TimeDartLiveness.hpp"
+#include "VerificationTypes/WorkflowSoundness.hpp"
+#include "VerificationTypes/WorkflowStrongSoundness.hpp"
 #include "SearchStrategies/SearchFactory.h"
 #include "DataStructures/PTrie.h"
 

=== modified file 'src/DiscreteVerification/SearchStrategies/SearchFactory.h'
--- src/DiscreteVerification/SearchStrategies/SearchFactory.h	2013-05-08 11:43:09 +0000
+++ src/DiscreteVerification/SearchStrategies/SearchFactory.h	2013-10-27 17:10:01 +0000
@@ -17,7 +17,10 @@
 template <class T>
 WaitingList<T>* getWaitingList(AST::Query* query, VerificationOptions& options){
 	WaitingList<T>* strategy = NULL;
-	if(query->getQuantifier() == EG || query->getQuantifier() == AF){
+	if(options.getWorkflowMode() == options.WORKFLOW_SOUNDNESS){
+		WorkflowMinFirst<T> s;
+		strategy = s.createWaitingList(query);
+	} else if(query->getQuantifier() == EG || query->getQuantifier() == AF){
 		//Liveness query, force DFS
 		switch(options.getSearchType()){
 		case VerificationOptions::DEPTHFIRST: {

=== modified file 'src/DiscreteVerification/SearchStrategies/SearchStrategies.hpp'
--- src/DiscreteVerification/SearchStrategies/SearchStrategies.hpp	2012-09-20 14:02:19 +0000
+++ src/DiscreteVerification/SearchStrategies/SearchStrategies.hpp	2013-10-27 17:10:01 +0000
@@ -9,5 +9,6 @@
 #include "NonStrictRandom.hpp"
 #include "NonStrictDFSHeuristic.hpp"
 #include "NonStrictDFSRandom.hpp"
+#include "WorkflowMinFirst.hpp"
 
 #endif /* TAPN_HPP_ */

=== added file 'src/DiscreteVerification/SearchStrategies/WorkflowMinFirst.hpp'
--- src/DiscreteVerification/SearchStrategies/WorkflowMinFirst.hpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/SearchStrategies/WorkflowMinFirst.hpp	2013-10-27 17:10:01 +0000
@@ -0,0 +1,42 @@
+/*
+ * NonStrictDFS.hpp
+ *
+ *  Created on: 05/03/2012
+ *      Author: MathiasGS
+ */
+
+#ifndef SMALLESTDELAYFIRST_HPP_
+#define SMALLESTDELAYFIRST_HPP_
+
+#include "../DataStructures/PWList.hpp"
+#include "../../Core/TAPN/TAPN.hpp"
+#include "../../Core/QueryParser/AST.hpp"
+#include "../../Core/VerificationOptions.hpp"
+
+#include "../../Core/TAPN/TimedPlace.hpp"
+#include "../../Core/TAPN/TimedTransition.hpp"
+#include "../../Core/TAPN/TimedInputArc.hpp"
+#include "../../Core/TAPN/TransportArc.hpp"
+#include "../../Core/TAPN/InhibitorArc.hpp"
+#include "../../Core/TAPN/OutputArc.hpp"
+
+#include "../SuccessorGenerator.hpp"
+
+#include "../QueryVisitor.hpp"
+
+#include <stack>
+#include "SearchStrategy.hpp"
+
+namespace VerifyTAPN {
+
+namespace DiscreteVerification {
+
+template <class T>
+class WorkflowMinFirst : public SearchStrategy<T> {
+public:
+	virtual WaitingList<T>* createWaitingList(AST::Query* query) const { return new WorkflowMinFirstWaitingList<T>(query); };
+};
+
+}
+}
+#endif /* NONSTRICTDFS_HPP_ */

=== added file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp	2013-10-27 17:10:01 +0000
@@ -0,0 +1,206 @@
+/*
+ * NonStrictSearch.cpp
+ *
+ *  Created on: 26/04/2012
+ *      Author: MathiasGS
+ */
+
+#include "WorkflowSoundness.hpp"
+
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+WorkflowSoundness::WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
+: ReachabilitySearch(tapn, initialMarking, query, options, waiting_list), pwList(new WorkflowPWList(waiting_list)), final_set(new vector<NonStrictMarking*>), min_exec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), in(NULL), out(NULL), modelType(calculateModelType()){
+	for(TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); iter != tapn.getPlaces().end(); iter++){
+		if((*iter)->getType() == Dead){
+			(*iter)->setType(Std);
+		}
+	}
+}
+
+bool WorkflowSoundness::verify(){
+	if(addToPW(&initialMarking, NULL)){
+		return false;
+	}
+
+	// Phase 1
+	while(pwList->hasWaitingStates()){
+		NonStrictMarking& next_marking = *pwList->getNextUnexplored();
+		tmpParent = &next_marking;
+		bool noDelay = false;
+		Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
+		if(res == QUERY_SATISFIED){
+			return false;
+		}  else if (res == URGENT_ENABLED) {
+			noDelay = true;
+		}
+
+		// Generate next markings
+		if(!noDelay && isDelayPossible(next_marking)){
+			NonStrictMarking* marking = new NonStrictMarking(next_marking);
+			marking->incrementAge();
+			marking->setGeneratedBy(NULL);
+			if(addToPW(marking, &next_marking)){
+				return false;
+			}
+		}
+	}
+
+	// Phase 2
+	for(vector<NonStrictMarking*>::iterator iter = final_set->begin(); iter != final_set->end(); iter++){
+		pwList->addToWaiting(*iter);
+		if(((WorkflowSoundnessMetaData*)(*iter)->meta)->min < min_exec){
+			min_exec = ((WorkflowSoundnessMetaData*)(*iter)->meta)->min;
+			lastMarking = (*iter);
+		}
+	}
+
+	while(pwList->hasWaitingStates()){
+		NonStrictMarking* next_marking = pwList->getNextUnexplored();
+		if(next_marking->meta->passed)	continue;
+		next_marking->meta->passed = true;
+		for(vector<NonStrictMarking*>::iterator iter = ((WorkflowSoundnessMetaData*)next_marking->meta)->parents->begin(); iter != ((WorkflowSoundnessMetaData*)next_marking->meta)->parents->end(); iter++){
+			pwList->addToWaiting(*iter);
+		}
+	}
+
+	NonStrictMarking* unpassed = pwList->getUnpassed();
+	if(unpassed == NULL){
+		return true;
+	}else{
+		lastMarking = unpassed;
+		return false;
+	}
+}
+
+bool WorkflowSoundness::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
+	marking->cut();
+
+	unsigned int size = marking->size();
+
+	// Check K-bound
+	pwList->setMaxNumTokensIfGreater(size);
+	if(modelType == ETAWFN && size > options.getKBound()) {
+		lastMarking = marking;
+		return true;	// Terminate false
+	}
+
+	// Map to existing marking if any
+	NonStrictMarking* lookup = pwList->lookup(marking);
+	if(lookup != NULL){
+		delete marking;
+		marking = lookup;
+	}else{
+		marking->meta = new WorkflowSoundnessMetaData();
+	}
+
+	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);
+		if(marking->getGeneratedBy() == NULL){
+			marking_meta_data->min = min(marking_meta_data->min, parent_meta_data->min+1);	// Delay
+		}else{
+			marking_meta_data->min = min(marking_meta_data->min, parent_meta_data->min);	// Transition
+		}
+	}else{
+		marking_meta_data->min = 0;
+	}
+
+
+
+	// Test if final place
+	if(marking->numberOfTokensInPlace(out->getIndex()) > 0){
+		if(size == 1){
+			marking = pwList->addToPassed(marking);
+			marking_meta_data = ((WorkflowSoundnessMetaData*)marking->meta);
+			marking_meta_data->parents->push_back(parent);
+			// Set min
+			marking_meta_data->min = min(marking_meta_data->min, ((WorkflowSoundnessMetaData*)parent->meta)->min);	// Transition
+			final_set->push_back(marking);
+		}else{
+			lastMarking = marking;
+			return true;	// Terminate false
+		}
+	}else{
+		// If new marking
+		if(pwList->add(marking)){
+			if(parent != NULL && marking->canDeadlock(tapn, 0)){
+				lastMarking = marking;
+				return true;
+			}
+			if(modelType == MTAWFN && checkForCoveredMarking(marking)){
+				lastMarking = marking;
+				return true;	// Terminate false
+			}
+		}
+	}
+
+	return false;
+}
+
+bool WorkflowSoundness::checkForCoveredMarking(NonStrictMarking* marking){
+	if(marking->size() <= options.getKBound()){
+		return false;	// Do not run check on small markings (invoke more rarely)
+	}
+
+	NonStrictMarking* covered = pwList->getCoveredMarking(marking, (marking->size() > linearSweepTreshold));
+	if(covered != NULL){
+		coveredMarking = covered;
+		return true;
+	}
+
+	return false;
+}
+
+void WorkflowSoundness::getTrace(NonStrictMarking* base){
+	stack < NonStrictMarking*> printStack;
+	NonStrictMarking* next = base;
+	do{
+		int min = INT_MAX;
+		NonStrictMarking* parent = NULL;
+		for(vector<NonStrictMarking*>::const_iterator iter = ((WorkflowSoundnessMetaData*)next->meta)->parents->begin(); iter != ((WorkflowSoundnessMetaData*)next->meta)->parents->end(); ++iter){
+			if(((WorkflowSoundnessMetaData*)(*iter)->meta)->min < min){
+				min = ((WorkflowSoundnessMetaData*)(*iter)->meta)->min;
+				parent = *iter;
+			}
+		}
+
+		if(((WorkflowSoundnessMetaData*)next->meta)->inTrace){ break;	}
+		((WorkflowSoundnessMetaData*)next->meta)->inTrace = true;
+		printStack.push(next);
+		next = parent;
+
+	}while(((WorkflowSoundnessMetaData*)next->meta)->parents != NULL && !((WorkflowSoundnessMetaData*)next->meta)->parents->empty());
+
+	if(printStack.top() != next){
+		printStack.push(next);
+	}
+
+	stack < NonStrictMarking*> tempStack;
+	while(!printStack.empty()){
+		printStack.top()->meta->inTrace = false;
+		tempStack.push(printStack.top());
+		printStack.pop();
+	}
+
+	while(!tempStack.empty()){
+		printStack.push(tempStack.top());
+		tempStack.pop();
+	}
+
+	if(options.getXmlTrace()){
+		printXMLTrace(lastMarking, printStack, query, tapn);
+	} else {
+		printHumanTrace(lastMarking, printStack, query->getQuantifier());
+	}
+}
+
+WorkflowSoundness::~WorkflowSoundness() {
+}
+
+} /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */

=== added file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp	2013-10-27 17:10:01 +0000
@@ -0,0 +1,180 @@
+/*
+ * NonStrictSearch.hpp
+ *
+ *  Created on: 26/04/2012
+ *      Author: MathiasGS
+ */
+
+#ifndef WORKFLOWSOUNDNESS_HPP_
+#define WORKFLOWSOUNDNESS_HPP_
+
+#include "../DataStructures/WorkflowPWList.hpp"
+#include "../../Core/TAPN/TAPN.hpp"
+#include "../../Core/QueryParser/AST.hpp"
+#include "../../Core/VerificationOptions.hpp"
+#include "../../Core/TAPN/TimedPlace.hpp"
+#include "../../Core/TAPN/TimedTransition.hpp"
+#include "../../Core/TAPN/TimedInputArc.hpp"
+#include "../../Core/TAPN/TransportArc.hpp"
+#include "../../Core/TAPN/InhibitorArc.hpp"
+#include "../../Core/TAPN/OutputArc.hpp"
+#include "../SuccessorGenerator.hpp"
+#include "../QueryVisitor.hpp"
+#include "../DataStructures/NonStrictMarking.hpp"
+#include <stack>
+#include "ReachabilitySearch.hpp"
+#include "../DataStructures/WaitingList.hpp"
+
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+class WorkflowSoundness : public ReachabilitySearch{
+public:
+	WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
+	virtual ~WorkflowSoundness();
+	bool verify();
+	void printStats(){
+		std::cout << "  discovered markings:\t" << pwList->discoveredMarkings << std::endl;
+		std::cout << "  explored markings:\t" << pwList->size()-pwList->explored() << std::endl;
+		std::cout << "  stored markings:\t" << pwList->size() << std::endl;
+	}
+
+	inline unsigned int maxUsedTokens(){ return pwList->maxNumTokensInAnyMarking; };
+protected:
+	virtual bool addToPW(NonStrictMarking* m){
+		return addToPW(m, tmpParent);
+	};
+	bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);
+	bool checkForCoveredMarking(NonStrictMarking* marking);
+	void getTrace(NonStrictMarking* base);
+public:
+	virtual void getTrace(){
+		return getTrace(lastMarking);
+	}
+	void printExecutionTime(ostream& stream){
+		stream << "Minimum execution time: " << min_exec << endl;
+	}
+	void printMessages(ostream& stream){
+		if(coveredMarking != NULL){
+			stream << "Covered marking: " << *coveredMarking << endl;
+			getTrace(coveredMarking);
+		}
+	}
+
+	enum ModelType{
+			MTAWFN, ETAWFN, NOTTAWFN
+		};
+
+		inline const ModelType getModelType() const{ return modelType; }
+
+		ModelType calculateModelType(){
+			bool isin, isout;
+			bool hasInvariant = false;
+			for(TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); iter != tapn.getPlaces().end(); iter++){
+				isin = isout = true;
+				TimedPlace* p = (*iter);
+				if(p->getInputArcs().empty() && p->getOutputArcs().empty() && p->getTransportArcs().empty()){
+					bool continueOuter = true;
+					// Test if really orphan place or if out place
+					for(TransportArc::Vector::const_iterator trans_i = tapn.getTransportArcs().begin(); trans_i != tapn.getTransportArcs().end(); ++trans_i){
+						if(&((*trans_i)->getDestination()) == p){
+							continueOuter = false;
+							break;
+						}
+					}
+					if(continueOuter)	continue;	// Fix orphan places
+				}
+
+				if(!hasInvariant && p->getInvariant() != p->getInvariant().LS_INF){
+					hasInvariant = true;
+				}
+
+				if(p->getInputArcs().size() > 0){
+					isout = false;
+				}
+
+				if(p->getOutputArcs().size() > 0){
+					isin = false;
+				}
+
+				if(isout){
+					for(TransportArc::Vector::const_iterator iter = p->getTransportArcs().begin(); iter != p->getTransportArcs().end(); iter++){
+						if(&(*iter)->getSource() == p){
+							isout = false;
+							break;
+						}
+					}
+				}
+
+				if(isin){
+					for(TransportArc::Vector::const_iterator iter = tapn.getTransportArcs().begin(); iter != tapn.getTransportArcs().end(); ++iter){		// TODO maybe transportArcs should contain both incoming and outgoing? Might break something though.
+						if(&(*iter)->getDestination() == p){
+							isin = false;
+							break;
+						}
+					}
+				}
+
+				if(isin){
+					if(in == NULL){
+						in = p;
+					}else{
+						return NOTTAWFN;
+					}
+				}
+
+				if(isout){
+					if(out == NULL){
+						out = p;
+					}else{
+						return NOTTAWFN;
+					}
+				}
+
+			}
+
+			if(in == NULL || out == NULL || in == out){
+				return NOTTAWFN;
+			}
+
+			if(initialMarking.size() != 1 || initialMarking.numberOfTokensInPlace(in->getIndex()) != 1){
+				return NOTTAWFN;
+			}
+
+			bool hasUrgent = false;
+			bool hasInhibitor = false;
+			// All transitions must have preset
+			for(TimedTransition::Vector::const_iterator iter = tapn.getTransitions().begin(); iter != tapn.getTransitions().end(); iter++){
+				if((*iter)->getPresetSize() == 0 && (*iter)->getNumberOfTransportArcs() == 0){
+					return NOTTAWFN;
+				}
+
+				if(!hasUrgent && (*iter)->isUrgent()){
+					hasUrgent = true;
+				}
+
+				if(!hasInhibitor && !(*iter)->getInhibitorArcs().empty()){
+					hasInhibitor = true;
+				}
+			}
+
+			if(hasUrgent || hasInvariant || hasInhibitor){
+				return ETAWFN;
+			}
+
+			return MTAWFN;
+		}
+protected:
+	WorkflowPWList* pwList;
+    vector<NonStrictMarking*>* final_set;
+    int min_exec;
+    unsigned int linearSweepTreshold;
+    NonStrictMarking* coveredMarking;
+    TimedPlace* in;
+	TimedPlace* out;
+	ModelType modelType;
+};
+
+} /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */
+#endif /* NONSTRICTSEARCH_HPP_ */

=== added file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp	2013-10-27 17:10:01 +0000
@@ -0,0 +1,119 @@
+/*
+ * NonStrictSearch.cpp
+ *
+ *  Created on: 26/04/2012
+ *      Author: MathiasGS
+ */
+
+#include "WorkflowStrongSoundness.hpp"
+
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+bool WorkflowStrongSoundnessReachability::verify(){
+		if(addToPW(&initialMarking, NULL)){
+			return true;
+		}
+
+		//Main loop
+		while(pwList->hasWaitingStates()){
+			NonStrictMarking& next_marking = *pwList->getNextUnexplored();
+	                tmpParent = &next_marking;
+
+	                bool noDelay = false;
+	                Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
+	                if(res == QUERY_SATISFIED){
+	                    return true;
+	                }  else if (res == URGENT_ENABLED) {
+	                    noDelay = true;
+	                }
+
+			// Generate next markings
+			if(!noDelay && isDelayPossible(next_marking)){
+				NonStrictMarking* marking = new NonStrictMarking(next_marking);
+				marking->incrementAge();
+				marking->setGeneratedBy(NULL);
+	                        if(addToPW(marking, &next_marking)){
+	                            return true;
+	                        }
+			}
+		}
+
+		return false;
+	}
+
+	void WorkflowStrongSoundnessReachability::getTrace(){
+		std::stack < NonStrictMarking*> printStack;
+		NonStrictMarking* next = lastMarking;
+		do{
+			NonStrictMarking* parent = ((WorkflowStrongSoundnessMetaData*) next->meta)->parents->at(0);
+			printStack.push(next);
+			next = parent;
+
+		}while(((WorkflowStrongSoundnessMetaData*)next->meta)->parents != NULL && !((WorkflowStrongSoundnessMetaData*)next->meta)->parents->empty());
+
+		if(printStack.top() != next){
+			printStack.push(next);
+		}
+
+		if(options.getXmlTrace()){
+			printXMLTrace(lastMarking, printStack, query, tapn);
+		} else {
+			printHumanTrace(lastMarking, printStack, query->getQuantifier());
+		}
+	}
+
+
+	bool WorkflowStrongSoundnessReachability::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
+		marking->cut();
+		marking->setParent(parent);
+
+		unsigned int size = marking->size();
+
+		pwList->setMaxNumTokensIfGreater(size);
+
+		if(size > options.getKBound()) {
+			delete marking;
+			return false;
+		}
+
+		/* Handle max */
+		// Map to existing marking if any
+		NonStrictMarking* lookup = pwList->lookup(marking);
+		if(lookup != NULL){
+			marking = lookup;
+		}else{
+			marking->meta = new WorkflowStrongSoundnessMetaData();
+		}
+
+		WorkflowStrongSoundnessMetaData* meta = (WorkflowStrongSoundnessMetaData*)marking->meta;
+
+		if(parent != NULL)	meta->parents->push_back(parent);
+
+		if(!marking->getTokenList(timer->getIndex()).empty() &&
+				(marking->getTokenList(timer->getIndex()).at(0).getAge() > max_value ||
+						(marking->getTokenList(timer->getIndex()).at(0).getAge() == max_value &&
+								(!marking->getTokenList(term1->getIndex()).empty() || !marking->getTokenList(term2->getIndex()).empty())))){
+			max_value = marking->getTokenList(timer->getIndex()).at(0).getAge();
+			lastMarking = marking;
+		}
+
+		// Add to passed
+		if(pwList->add(marking)){
+			QueryVisitor<NonStrictMarking> checker(*marking, tapn);
+			BoolResult context;
+
+			query->accept(checker, context);
+			if(context.value) {
+				lastMarking = marking;
+				return true;
+			} else {
+				return false;
+			}
+		}
+
+		return false;
+	}
+
+} /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */

=== added file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp	2013-10-27 17:10:01 +0000
@@ -0,0 +1,83 @@
+/*
+ * NonStrictSearch.hpp
+ *
+ *  Created on: 26/04/2012
+ *      Author: MathiasGS
+ */
+
+#ifndef WORKFLOWSTRONGSOUNDNESS_HPP_
+#define WORKFLOWSTRONGSOUNDNESS_HPP_
+
+#include "ReachabilitySearch.hpp"
+#include "../DataStructures/WorkflowPWList.hpp"
+#include <stack>
+
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+class WorkflowStrongSoundnessReachability : public ReachabilitySearch{
+public:
+	WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
+    : ReachabilitySearch(tapn,initialMarking, query, options, waiting_list), pwList(new WorkflowPWList(waiting_list)), max_value(-1), timer(NULL), term1(NULL), term2(NULL)
+    {
+		// Disable dead place optimization
+		for(TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); iter != tapn.getPlaces().end(); iter++){
+			if((*iter)->getType() == Dead){
+				(*iter)->setType(Std);
+			}
+		}
+
+		// Find timer place and store as out
+		for(TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); iter != tapn.getPlaces().end(); ++iter){
+			if((*iter)->getInvariant() != (*iter)->getInvariant().LS_INF){
+				if(timer == NULL || timer->getInvariant().getBound() < (*iter)->getInvariant().getBound()){
+					timer = *iter;
+				}
+			}
+
+			if(!(*iter)->getTransportArcs().empty() || !(*iter)->getInputArcs().empty()){
+				continue;
+			}
+
+			if(term1 == NULL){
+				term1 = *iter;
+			}else if(term2 == NULL){
+				term2 = *iter;
+			}else{
+				assert(false);
+			}
+		}
+    };
+
+	bool verify();
+	void getTrace();
+
+	void printExecutionTime(ostream& stream){
+		stream << "Maximum execution time: " << max_value << endl;
+	}
+
+	void printStats(){
+			std::cout << "  discovered markings:\t" << pwList->discoveredMarkings << std::endl;
+			std::cout << "  explored markings:\t" << pwList->size()-pwList->explored() << std::endl;
+			std::cout << "  stored markings:\t" << pwList->size() << std::endl;
+		}
+
+	inline unsigned int maxUsedTokens(){ return pwList->maxNumTokensInAnyMarking; };
+
+protected:
+	virtual bool addToPW(NonStrictMarking* m){
+			return addToPW(m, tmpParent);
+		};
+
+	bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);
+protected:
+	PWListBase* pwList;
+	int max_value;
+	TimedPlace* timer;
+	TimedPlace* term1;
+	TimedPlace* term2;
+};
+
+} /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */
+#endif /* NONSTRICTSEARCH_HPP_ */

=== modified file 'src/compile-mac-32-64.sh'
--- src/compile-mac-32-64.sh	2013-08-28 09:59:17 +0000
+++ src/compile-mac-32-64.sh	2013-10-27 17:10:01 +0000
@@ -7,9 +7,9 @@
 
 export CPLUS_INCLUDE_PATH=$HOME/dev/boost_1_46_1
 
-inc64="-I$HOME/dev/ia64/include"
+inc64="-I$HOME/dev/ia64/include -I/usr/local/include -I/opt/local/include"
 
-inc32="-I$HOME/dev/ia32/include"
+inc32="-I$HOME/dev/ia32/include -I/usr/local/include -I/opt/local/include"
 
 compatibility="-mmacosx-version-min=10.6"