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

[Peter Gjøl Jensen]

implemented place-bound-statistics. The changes should be fairly obvious and easy to read.

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

315. By Jiri Srba on 2014-07-13

fixed an explanation in a comment

316. By Jiri Srba on 2014-07-14

changed some formating issues in place-statistic print

[Jiri Srba (srba)]

tested and works in the same way as statistics for the untimed engine

review: Approve

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2014-07-08 18:26:00 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2014-07-14 09:32:30 +0000
@@ -6,6 +6,7 @@
  */
 
 #include "NonStrictMarkingBase.hpp"
+#include <limits>
 
 using namespace std;
 
@@ -357,7 +358,7 @@
         }
 
         
-        int NonStrictMarkingBase::cut() {
+        int NonStrictMarkingBase::cut(std::vector<int>& placeCount) {
 #ifdef DEBUG
             std::cout << "Before cut: " << *this << std::endl;
 #endif
@@ -374,6 +375,7 @@
                 }
                 //set age of too old tokens to max age
                 int count = 0;
+                int total = 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()) { // this will also removed dead tokens
                         TokenList::iterator beginDelete = token_iter;
@@ -381,15 +383,29 @@
                             for (; token_iter != place_iter->tokens.end(); token_iter++) {
                                 count += token_iter->getCount();
                             }
+                        } 
+                        else if(place_iter->place->getType() == TAPN::Dead)
+                        { 
+                            // if we remove some dead tokens update place statistics
+                            if(place_iter->tokens.size() > 0) {
+                                placeCount[place_iter->place->getIndex()] = std::numeric_limits<int>::max();
+                            }   
                         }
                         this->removeRangeOfTokens(*place_iter, beginDelete, place_iter->tokens.end());
                         break;
+                    } else {
+                        total += token_iter->getCount();
                     }
                 }
+                
                 if (count) {
                     Token t(place_iter->place->getMaxConstant() + 1, count);
                     this->addTokenInPlace(*place_iter, t);
                 }
+                
+                // update place statistics
+                total += count;
+                placeCount[place_iter->place->getIndex()] = max(total, placeCount[place_iter->place->getIndex()]);
             }
             this->cleanUp();
             return maxDelay;

=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp	2013-07-26 21:59:47 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp	2014-07-14 09:32:30 +0000
@@ -159,7 +159,7 @@
                 
 	public: // modifiers
 
-                int cut();
+                int cut(std::vector<int>&);
 		bool removeToken(int placeId, int age);
 		bool removeToken(Place& place, Token& token);
 		void addTokenInPlace(TAPN::TimedPlace& place, int age);

=== modified file 'src/DiscreteVerification/DiscreteVerification.cpp'
--- src/DiscreteVerification/DiscreteVerification.cpp	2014-06-18 19:39:40 +0000
+++ src/DiscreteVerification/DiscreteVerification.cpp	2014-07-14 09:32:30 +0000
@@ -215,6 +215,7 @@
             
             verifier.printStats();
             verifier.printTransitionStatistics();
+            verifier.printPlaceStatistics();
 
             std::cout << "Query is " << (result ? "satisfied" : "NOT satisfied") << "." << std::endl;
             std::cout << "Max number of tokens found in any reachable marking: ";

=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp'
--- src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2014-07-04 17:38:14 +0000
+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2014-07-14 09:32:30 +0000
@@ -92,7 +92,7 @@
 }
 
 bool LivenessSearch::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
-	marking->cut();
+	marking->cut(placeStats);
 	marking->setParent(parent);
 	unsigned int size = marking->size();
 

=== modified file 'src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp'
--- src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2014-06-15 09:02:10 +0000
+++ src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2014-07-14 09:32:30 +0000
@@ -57,7 +57,7 @@
 }
 
 bool ReachabilitySearch::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
-	marking->cut();
+	marking->cut(placeStats);
 	marking->setParent(parent);
         
 	unsigned int size = marking->size();

=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartLiveness.cpp'
--- src/DiscreteVerification/VerificationTypes/TimeDartLiveness.cpp	2013-09-01 17:37:24 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartLiveness.cpp	2014-07-14 09:32:30 +0000
@@ -125,7 +125,7 @@
             if(options.getTrace() == VerificationOptions::SOME_TRACE){
                 start = marking->getYoungest();
             }
-            marking->cut();
+            marking->cut(placeStats);
             const TimedTransition* transition = marking->getGeneratedBy();
             unsigned int size = marking->size();
 

=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.cpp'
--- src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.cpp	2014-06-14 14:17:03 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartReachabilitySearch.cpp	2014-07-14 09:32:30 +0000
@@ -74,7 +74,7 @@
         if(options.getTrace() != VerificationOptions::NO_TRACE){
             start = marking->getYoungest();
         }
-	int maxDelay = marking->cut();
+	int maxDelay = marking->cut(placeStats);
 
 	unsigned int size = marking->size();
 

=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp'
--- src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp	2014-07-05 10:15:17 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp	2014-07-14 09:32:30 +0000
@@ -216,7 +216,7 @@
                         }
 
                         last = mc;
-                        mc->cut();
+                        mc->cut(placeStats);
                         if(l == NULL) {                  // set specific last marking to last marking in delay if deadlock
                             l = mc;
                         }
@@ -230,7 +230,7 @@
                 l = new NonStrictMarkingBase(*getBase(lastMarking->dart));
                 trace = ((TraceDart*) lastMarking);
                 l->incrementAge(trace->start);
-                l->cut();
+                l->cut(placeStats);
                 l->setParent(NULL);
                 l->setGeneratedBy( ((TraceDart*)lastMarking)->generatedBy);
             }
@@ -261,7 +261,7 @@
                             l->setParent(mc);
                         }
                         last = mc;
-                        mc->cut();
+                        mc->cut(placeStats);
                         traceStack.push(mc);            // add delay marking to the trace
                         diff--;
                     }
@@ -272,7 +272,7 @@
                 if(!l->getParent()) {
                     l->setParent(m);
                 }
-                m->cut();
+                m->cut(placeStats);
                 last = m;
                 traceStack.push(m); // add the marking to the trace
 

=== modified file 'src/DiscreteVerification/VerificationTypes/Verification.hpp'
--- src/DiscreteVerification/VerificationTypes/Verification.hpp	2014-07-07 19:03:13 +0000
+++ src/DiscreteVerification/VerificationTypes/Verification.hpp	2014-07-14 09:32:30 +0000
@@ -7,6 +7,7 @@
 #include <stack>
 #include "../../Core/TAPNParser/util.hpp"
 #include "../DeadlockVisitor.hpp"
+#include "../../Core/TAPN/TimedPlace.hpp"
 
 
 
@@ -22,6 +23,7 @@
             virtual bool verify() = 0;
             virtual void printStats() = 0;
             virtual void printTransitionStatistics() const = 0;
+            virtual void printPlaceStatistics();
             virtual unsigned int maxUsedTokens() = 0;
             virtual bool addToPW(T* marking) = 0;
 
@@ -42,14 +44,32 @@
             T& initialMarking;
             AST::Query* query;
             VerificationOptions options;
+            std::vector<int> placeStats;
 
          };
 
         template<typename T>
         Verification<T>::Verification(TAPN::TimedArcPetriNet& tapn, T& initialMarking, AST::Query* query, VerificationOptions options)
-        : tapn(tapn), initialMarking(initialMarking), query(query), options(options){
+        : tapn(tapn), initialMarking(initialMarking), query(query), options(options), placeStats(tapn.getNumberOfPlaces()){
             
         }
+
+        template<typename T>
+        void Verification<T>::printPlaceStatistics() {
+            fprintf(stdout, "PLACE-BOUND STATISTICS\n");
+            for (size_t p = 0; p < placeStats.size(); ++p) {
+                // report maximum bounds for each place (? means that the place had some deadlock tokens that were removed)
+                int count = placeStats[p];
+                const TAPN::TimedPlace place = tapn.getPlace(p);
+                if (count == std::numeric_limits<int>::max()) {
+                    fprintf(stdout, "<%s;?> ", place.getName().c_str());
+                } else {
+                    fprintf(stdout, "<%s;%i> ", place.getName().c_str(), count);
+                }
+            }
+            fprintf(stdout, "\n\n");
+        }
+        
         template<typename T>
         void Verification<T>::printHumanTrace(T* m, std::stack<T*>& stack, AST::Quantifier query) {
             std::cout << "Trace: " << std::endl;

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp	2014-06-12 21:47:38 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp	2014-07-14 09:32:30 +0000
@@ -67,7 +67,7 @@
 }
 
 bool WorkflowSoundness::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){
-	marking->cut();
+	marking->cut(placeStats);
 
 	unsigned int size = marking->size();
 

=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp'
--- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp	2014-06-17 10:13:39 +0000
+++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp	2014-07-14 09:32:30 +0000
@@ -106,7 +106,7 @@
         }
 
         bool WorkflowStrongSoundnessReachability::addToPW(NonStrictMarking* marking, NonStrictMarking* parent) {
-            marking->cut();
+            marking->cut(placeStats);
             marking->setParent(parent);
             
             int totalDelay = marking->calculateTotalDelay();