VerifyDTAPN

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

  1. CutOptimization
  2. Merge into trunk
Proposed by Peter Gjøl Jensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 279
Merged at revision: 278
Proposed branch: lp:~verifydtapn-contributers/verifydtapn/CutOptimization
Merge into: lp:verifydtapn
Diff against target: 163 lines (+8/-78)
5 files modified
src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp (+6/-12)
src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp (+1/-32)
src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp (+0/-1)
src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp (+1/-32)
src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp (+0/-1)
To merge this branch: bzr merge lp:~verifydtapn-contributers/verifydtapn/CutOptimization
Reviewer Review Type Date Requested Status
Mathias Grund Sørensen Approve
Jiri Srba Approve
Jakob Taankvist Approve
verifydtapn-contributers Pending
Review via email: mp+157861@code.launchpad.net
To post a comment you must log in.
Revision history for this message
Jakob Taankvist (jakob-taankvist) :
review: Approve
Revision history for this message
Jiri Srba (srba) :
review: Approve
Revision history for this message
Jiri Srba (srba) wrote :

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

Revision history for this message
Mathias Grund Sørensen (mathias.grund) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== 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 @@
263 std::cout << "Before cut: " << *this << std::endl;263 std::cout << "Before cut: " << *this << std::endl;
264#endif264#endif
265 for(PlaceList::iterator place_iter = this->places.begin(); place_iter != this->places.end(); place_iter++){265 for(PlaceList::iterator place_iter = this->places.begin(); place_iter != this->places.end(); place_iter++){
266 //remove dead tokens
267 if (place_iter->place->GetType() == TAPN::Dead) {
268 for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
269 if(token_iter->getAge() > place_iter->place->GetMaxConstant()){
270 token_iter->remove(token_iter->getCount());
271 }
272 }
273 }
274 //set age of too old tokens to max age266 //set age of too old tokens to max age
275 int count = 0;267 int count = 0;
276 for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){268 for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++) {
277 if(token_iter->getAge() > place_iter->place->GetMaxConstant()){269 if(token_iter->getAge() > place_iter->place->GetMaxConstant()){ // this will also removed dead tokens
278 TokenList::iterator beginDelete = token_iter;270 TokenList::iterator beginDelete = token_iter;
279 if(place_iter->place->GetType() == TAPN::Std){271 if(place_iter->place->GetType() == TAPN::Std){
280 for(; token_iter != place_iter->tokens.end(); token_iter++){272 for(; token_iter != place_iter->tokens.end(); token_iter++){
@@ -285,8 +277,10 @@
285 break;277 break;
286 }278 }
287 }279 }
288 Token t(place_iter->place->GetMaxConstant()+1,count);280 if(count){
289 this->AddTokenInPlace(*place_iter, t);281 Token t(place_iter->place->GetMaxConstant()+1,count);
282 this->AddTokenInPlace(*place_iter, t);
283 }
290 }284 }
291 this->CleanUp();285 this->CleanUp();
292 #ifdef DEBUG286 #ifdef DEBUG
293287
=== 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 @@
105}105}
106106
107bool LivenessSearch::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){107bool LivenessSearch::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
108 cut(marking);108 marking->cut();
109 marking->SetParent(parent);109 marking->SetParent(parent);
110 unsigned int size = marking->size();110 unsigned int size = marking->size();
111111
@@ -138,37 +138,6 @@
138 return false;138 return false;
139}139}
140140
141void LivenessSearch::cut(NonStrictMarking* m){
142 for(PlaceList::iterator place_iter = m->places.begin(); place_iter != m->places.end(); place_iter++){
143 const TimedPlace& place = tapn->GetPlace(place_iter->place->GetIndex());
144 //remove dead tokens
145 if (place_iter->place->GetType() == Dead) {
146 for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
147 if(token_iter->getAge() > place.GetMaxConstant()){
148 token_iter->remove(token_iter->getCount());
149 }
150 }
151 }
152 //set age of too old tokens to max age
153 int count = 0;
154 for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
155 if(token_iter->getAge() > place.GetMaxConstant()){
156 TokenList::iterator beginDelete = token_iter;
157 if(place.GetType() == Std){
158 for(; token_iter != place_iter->tokens.end(); token_iter++){
159 count += token_iter->getCount();
160 }
161 }
162 m->RemoveRangeOfTokens(*place_iter, beginDelete, place_iter->tokens.end());
163 break;
164 }
165 }
166 Token t(place.GetMaxConstant()+1,count);
167 m->AddTokenInPlace(*place_iter, t);
168 }
169 m->CleanUp();
170}
171
172void LivenessSearch::printStats(){141void LivenessSearch::printStats(){
173 std::cout << " discovered markings:\t" << pwList->discoveredMarkings << std::endl;142 std::cout << " discovered markings:\t" << pwList->discoveredMarkings << std::endl;
174 std::cout << " explored markings:\t" << pwList->Size()-pwList->Explored() << std::endl;143 std::cout << " explored markings:\t" << pwList->Size()-pwList->Explored() << std::endl;
175144
=== 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 @@
46 vector<NonStrictMarking*> getPossibleNextMarkings(const NonStrictMarking& marking);46 vector<NonStrictMarking*> getPossibleNextMarkings(const NonStrictMarking& marking);
47 bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);47 bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);
48 bool isDelayPossible(NonStrictMarking& marking);48 bool isDelayPossible(NonStrictMarking& marking);
49 void cut(NonStrictMarking* m);
5049
51protected:50protected:
52 int validChildren;51 int validChildren;
5352
=== 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 @@
79}79}
8080
81bool ReachabilitySearch::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){81bool ReachabilitySearch::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
82 cut(marking);82 marking->cut();
83 marking->SetParent(parent);83 marking->SetParent(parent);
8484
85 unsigned int size = marking->size();85 unsigned int size = marking->size();
@@ -109,37 +109,6 @@
109 return false;109 return false;
110}110}
111111
112void ReachabilitySearch::cut(NonStrictMarking* m){
113 for(PlaceList::iterator place_iter = m->places.begin(); place_iter != m->places.end(); place_iter++){
114 const TimedPlace& place = tapn->GetPlace(place_iter->place->GetIndex());
115 //remove dead tokens
116 if (place_iter->place->GetType() == Dead) {
117 for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
118 if(token_iter->getAge() > place.GetMaxConstant()){
119 token_iter->remove(token_iter->getCount());
120 }
121 }
122 }
123 //set age of too old tokens to max age
124 int count = 0;
125 for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
126 if(token_iter->getAge() > place.GetMaxConstant()){
127 TokenList::iterator beginDelete = token_iter;
128 if(place.GetType() == Std){
129 for(; token_iter != place_iter->tokens.end(); token_iter++){
130 count += token_iter->getCount();
131 }
132 }
133 m->RemoveRangeOfTokens(*place_iter, beginDelete, place_iter->tokens.end());
134 break;
135 }
136 }
137 Token t(place.GetMaxConstant()+1,count);
138 m->AddTokenInPlace(*place_iter, t);
139 }
140 m->CleanUp();
141}
142
143void ReachabilitySearch::printStats(){112void ReachabilitySearch::printStats(){
144 std::cout << " discovered markings:\t" << pwList->discoveredMarkings << std::endl;113 std::cout << " discovered markings:\t" << pwList->discoveredMarkings << std::endl;
145 std::cout << " explored markings:\t" << pwList->Size()-pwList->Explored() << std::endl;114 std::cout << " explored markings:\t" << pwList->Size()-pwList->Explored() << std::endl;
146115
=== 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 @@
47 vector<NonStrictMarking*> getPossibleNextMarkings(const NonStrictMarking& marking);47 vector<NonStrictMarking*> getPossibleNextMarkings(const NonStrictMarking& marking);
48 bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);48 bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);
49 bool isDelayPossible(NonStrictMarking& marking);49 bool isDelayPossible(NonStrictMarking& marking);
50 void cut(NonStrictMarking* marking);
5150
52protected:51protected:
53 int validChildren;52 int validChildren;

Subscribers

People subscribed via source and target branches