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

[Peter Gjøl Jensen]

[Jakob Taankvist (jakob-taankvist)]

review: Approve

[Jiri Srba (srba)]

review: Approve

[Jiri Srba (srba)]

Btw. this gives about 5% speedup in verification time.

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

review: Approve

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2013-03-17 14:00:48 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2013-04-09 12:42:25 +0000
@@ -263,18 +263,10 @@
 	std::cout << "Before cut: " << *this << std::endl;
 #endif
 	for(PlaceList::iterator place_iter = this->places.begin(); place_iter != this->places.end(); place_iter++){
-		//remove dead tokens
-		if (place_iter->place->GetType() ==  TAPN::Dead) {
-			for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
-				if(token_iter->getAge() > place_iter->place->GetMaxConstant()){
-					token_iter->remove(token_iter->getCount());
-				}
-			}
-		}
 		//set age of too old tokens to max age
 		int count = 0;
-		for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
-			if(token_iter->getAge() > place_iter->place->GetMaxConstant()){
+		for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++) {
+                        if(token_iter->getAge() > place_iter->place->GetMaxConstant()){ // this will also removed dead tokens
 				TokenList::iterator beginDelete = token_iter;
 				if(place_iter->place->GetType() == TAPN::Std){
 					for(; token_iter != place_iter->tokens.end(); token_iter++){
@@ -285,8 +277,10 @@
 				break;
 			}
 		}
-		Token t(place_iter->place->GetMaxConstant()+1,count);
-		this->AddTokenInPlace(*place_iter, t);
+                if(count){
+                        Token t(place_iter->place->GetMaxConstant()+1,count);
+                        this->AddTokenInPlace(*place_iter, t);
+                }
 	}
 	this->CleanUp();
 	#ifdef DEBUG

=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp'
--- src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2013-03-25 14:03:05 +0000
+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2013-04-09 12:42:25 +0000
@@ -105,7 +105,7 @@
 }
 
 bool LivenessSearch::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
-	cut(marking);
+	marking->cut();
 	marking->SetParent(parent);
 	unsigned int size = marking->size();
 
@@ -138,37 +138,6 @@
 	return false;
 }
 
-void LivenessSearch::cut(NonStrictMarking* m){
-	for(PlaceList::iterator place_iter = m->places.begin(); place_iter != m->places.end(); place_iter++){
-		const TimedPlace& place = tapn->GetPlace(place_iter->place->GetIndex());
-		//remove dead tokens
-		if (place_iter->place->GetType() == Dead) {
-			for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
-				if(token_iter->getAge() > place.GetMaxConstant()){
-					token_iter->remove(token_iter->getCount());
-				}
-			}
-		}
-		//set age of too old tokens to max age
-		int count = 0;
-		for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
-			if(token_iter->getAge() > place.GetMaxConstant()){
-				TokenList::iterator beginDelete = token_iter;
-				if(place.GetType() == Std){
-					for(; token_iter != place_iter->tokens.end(); token_iter++){
-						count += token_iter->getCount();
-					}
-				}
-				m->RemoveRangeOfTokens(*place_iter, beginDelete, place_iter->tokens.end());
-				break;
-			}
-		}
-		Token t(place.GetMaxConstant()+1,count);
-		m->AddTokenInPlace(*place_iter, t);
-	}
-	m->CleanUp();
-}
-
 void LivenessSearch::printStats(){
 	std::cout << "  discovered markings:\t" << pwList->discoveredMarkings << std::endl;
 	std::cout << "  explored markings:\t" << pwList->Size()-pwList->Explored() << std::endl;

=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp'
--- src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp	2013-03-25 14:03:05 +0000
+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp	2013-04-09 12:42:25 +0000
@@ -46,7 +46,6 @@
 	vector<NonStrictMarking*> getPossibleNextMarkings(const NonStrictMarking& marking);
 	bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);
 	bool isDelayPossible(NonStrictMarking& marking);
-	void cut(NonStrictMarking* m);
 
 protected:
 	int validChildren;

=== modified file 'src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp'
--- src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2013-03-25 14:03:05 +0000
+++ src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2013-04-09 12:42:25 +0000
@@ -79,7 +79,7 @@
 }
 
 bool ReachabilitySearch::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
-	cut(marking);
+	marking->cut();
 	marking->SetParent(parent);
 
 	unsigned int size = marking->size();
@@ -109,37 +109,6 @@
 	return false;
 }
 
-void ReachabilitySearch::cut(NonStrictMarking* m){
-	for(PlaceList::iterator place_iter = m->places.begin(); place_iter != m->places.end(); place_iter++){
-		const TimedPlace& place = tapn->GetPlace(place_iter->place->GetIndex());
-		//remove dead tokens
-		if (place_iter->place->GetType() == Dead) {
-			for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
-				if(token_iter->getAge() > place.GetMaxConstant()){
-					token_iter->remove(token_iter->getCount());
-				}
-			}
-		}
-		//set age of too old tokens to max age
-		int count = 0;
-		for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
-			if(token_iter->getAge() > place.GetMaxConstant()){
-				TokenList::iterator beginDelete = token_iter;
-				if(place.GetType() == Std){
-					for(; token_iter != place_iter->tokens.end(); token_iter++){
-						count += token_iter->getCount();
-					}
-				}
-				m->RemoveRangeOfTokens(*place_iter, beginDelete, place_iter->tokens.end());
-				break;
-			}
-		}
-		Token t(place.GetMaxConstant()+1,count);
-		m->AddTokenInPlace(*place_iter, t);
-	}
-	m->CleanUp();
-}
-
 void ReachabilitySearch::printStats(){
 	std::cout << "  discovered markings:\t" << pwList->discoveredMarkings << std::endl;
 	std::cout << "  explored markings:\t" << pwList->Size()-pwList->Explored() << std::endl;

=== modified file 'src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp'
--- src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp	2013-03-25 14:03:05 +0000
+++ src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp	2013-04-09 12:42:25 +0000
@@ -47,7 +47,6 @@
 	vector<NonStrictMarking*> getPossibleNextMarkings(const NonStrictMarking& marking);
 	bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);
 	bool isDelayPossible(NonStrictMarking& marking);
-	void cut(NonStrictMarking* marking);
 
 protected:
 	int validChildren;