VerifyTAPN

Merge lp:~verifytapn-contributers/verifytapn/transition_statistics into lp:verifytapn

  1. transition_statistics
  2. Merge into trunk
Proposed by Jiri Srba
Status: Merged
Approved by: Jiri Srba
Approved revision: 153
Merged at revision: 147
Proposed branch: lp:~verifytapn-contributers/verifytapn/transition_statistics
Merge into: lp:verifytapn
Diff against target: 203 lines (+48/-3)
7 files modified
src/Core/ArgsParser.hpp (+1/-1)
src/Core/TAPN/TimedArcPetriNet.hpp (+1/-0)
src/ReachabilityChecker/Search/SearchStrategy.cpp (+5/-0)
src/ReachabilityChecker/Search/SearchStrategy.hpp (+2/-0)
src/ReachabilityChecker/SuccessorGenerator.cpp (+27/-0)
src/ReachabilityChecker/SuccessorGenerator.hpp (+11/-2)
src/main.cpp (+1/-0)
To merge this branch: bzr merge lp:~verifytapn-contributers/verifytapn/transition_statistics
Reviewer Review Type Date Requested Status
Morten Jacobsen (community) Needs Fixing
Mathias Grund Sørensen (community) Approve
Jiri Srba Approve
Review via email: mp+113589@code.launchpad.net

Commit message

In successor generator it is now recorded how many times was every transition enabled.

Description of the change

In successor generator it is now recorded how many times was every transition enabled.

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) :
review: Approve
Revision history for this message
Mathias Grund Sørensen (mathias.grund) :
review: Approve
Revision history for this message
Jiri Srba (srba) wrote :

The problem is that it reports that a transition is enabled for each of the permutations of
tokens. This should count just as one, irrelevant of the number of tokens that enable the transition.

Revision history for this message
Jiri Srba (srba) wrote :

I have now fixed the counting so that it happens for each transition only once.

Revision history for this message
Morten Jacobsen (mortenja) wrote :

You are missing a delete statement in the destructor of SuccessorGenerator.hpp (like "delete [] arcsArray;" in line 30) for the transition statistic array.. Other than that it looks fine..

review: Needs Fixing
lp:~verifytapn-contributers/verifytapn/transition_statistics updated
153. By Jiri Srba

added a destructor for the array transitionStatistics

Revision history for this message
Jiri Srba (srba) wrote :

The destructor of the transition array has been added.

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/Core/ArgsParser.hpp'
2--- src/Core/ArgsParser.hpp 2011-11-21 04:34:49 +0000
3+++ src/Core/ArgsParser.hpp 2012-07-06 19:00:26 +0000
4@@ -80,7 +80,7 @@
5 class ArgsParser {
6 typedef std::vector< boost::shared_ptr<Switch> > parser_vec;
7 public:
8- ArgsParser() : parsers(), version(1,1,0) { Initialize(); };
9+ ArgsParser() : parsers(), version(1,2,0) { Initialize(); };
10 virtual ~ArgsParser() {};
11
12 VerificationOptions Parse(int argc, char* argv[]) const;
13
14=== modified file 'src/Core/TAPN/TimedArcPetriNet.hpp'
15--- src/Core/TAPN/TimedArcPetriNet.hpp 2011-11-25 20:48:31 +0000
16+++ src/Core/TAPN/TimedArcPetriNet.hpp 2012-07-06 19:00:26 +0000
17@@ -44,6 +44,7 @@
18 const int GetNumberOfConsumingArcs() const { return inputArcs.size() + transportArcs.size(); }
19 const OutputArc::Vector& GetOutputArcs() const { return outputArcs; }
20 const int GetNumberOfOutputArcs() const { return outputArcs.size(); }
21+ const int GetNumberOfTransitions() const { return transitions.size(); }
22 int NumberOfPlaces() const { return places.size(); };
23 const Pairing& GetPairing(const TimedTransition& t) const { return pairings.find(t)->second; }
24 inline int MaxConstant() const { return maxConstant; };
25
26=== modified file 'src/ReachabilityChecker/Search/SearchStrategy.cpp'
27--- src/ReachabilityChecker/Search/SearchStrategy.cpp 2011-06-14 13:52:39 +0000
28+++ src/ReachabilityChecker/Search/SearchStrategy.cpp 2012-07-06 19:00:26 +0000
29@@ -157,4 +157,9 @@
30 }
31 }
32 }
33+
34+ void DefaultSearchStrategy::PrintTransitionStatistics() const {
35+ succGen.PrintTransitionStatistics(std::cout);
36+ return;
37+ }
38 }
39
40=== modified file 'src/ReachabilityChecker/Search/SearchStrategy.hpp'
41--- src/ReachabilityChecker/Search/SearchStrategy.hpp 2011-06-14 13:52:39 +0000
42+++ src/ReachabilityChecker/Search/SearchStrategy.hpp 2012-07-06 19:00:26 +0000
43@@ -30,6 +30,7 @@
44 virtual unsigned int MaxUsedTokens() const = 0;
45 virtual Stats GetStats() const = 0;
46 virtual void PrintTraceIfAny(bool result) const = 0;
47+ virtual void PrintTransitionStatistics() const = 0;
48 };
49
50
51@@ -54,6 +55,7 @@
52 virtual unsigned int MaxUsedTokens() const { return succGen.MaxUsedTokens(); };
53 virtual Stats GetStats() const;
54 virtual void PrintTraceIfAny(bool result) const;
55+ virtual void PrintTransitionStatistics() const;
56 protected:
57 virtual WaitingList* CreateWaitingList() const = 0;
58 private:
59
60=== modified file 'src/ReachabilityChecker/SuccessorGenerator.cpp'
61--- src/ReachabilityChecker/SuccessorGenerator.cpp 2012-06-30 10:52:07 +0000
62+++ src/ReachabilityChecker/SuccessorGenerator.cpp 2012-07-06 19:00:26 +0000
63@@ -10,6 +10,8 @@
64 {
65 ClearAll();
66
67+ //this->Print(std::cout);
68+
69 const TAPN::TimedTransition::Vector& transitions = tapn.GetTransitions();
70
71 CollectArcsAndAppropriateTokens(transitions, &marking);
72@@ -79,6 +81,7 @@
73 void SuccessorGenerator::GenerateSuccessors(const TAPN::TimedTransition::Vector& transitions, const SymbolicMarking* marking, std::vector<Successor>& succ)
74 {
75 int currentTransitionIndex = 0;
76+ int realCurrentTransitionIndex = 0;
77 for(TAPN::TimedTransition::Vector::const_iterator iter = transitions.begin(); iter != transitions.end(); ++iter)
78 {
79 unsigned int presetSize = (*iter)->GetPresetSize();
80@@ -92,8 +95,10 @@
81 indicesOfCurrentPermutation[i] = 0;
82
83 bool done = false;
84+ transitionStatistics[realCurrentTransitionIndex]++;
85 while(true)
86 {
87+
88 GenerateSuccessorForCurrentPermutation(*(*iter), indicesOfCurrentPermutation, currentTransitionIndex, presetSize, marking, succ);
89
90 // Generate next permutation of input tokens
91@@ -118,6 +123,7 @@
92 }
93 }
94
95+ realCurrentTransitionIndex++;
96 currentTransitionIndex += presetSize; // jump to next start of next transition in arcsArray
97 }
98 }
99@@ -394,9 +400,30 @@
100 out << i << ": " << arcsArray[i] << "\n";
101 }
102
103+ out << "\nTransitions Array:\n";
104+ out << "------------------\n";
105+ for(int j =0;j< numberOfTransitions;j++){
106+ out << j << ": " << transitionStatistics[j] << "\n";
107+ }
108+
109 out << "\n\nToken Indices:\n";
110 out << "----------------------\n";
111
112 out << *tokenIndices << "\n";
113 }
114+
115+ void SuccessorGenerator::PrintTransitionStatistics(std::ostream& out) const {
116+ out << std::endl << "TRANSITION STATISTICS";
117+ for (int i=0;i<tapn.GetNumberOfTransitions();i++) {
118+ if ((i) % 6 == 0) {
119+ out << std::endl;
120+ out << "<" << tapn.GetTransitions()[i]->GetName() << ":" << transitionStatistics[i] << ">";
121+ }
122+ else {
123+ out << " <" <<tapn.GetTransitions()[i]->GetName() << ":" << transitionStatistics[i] << ">";
124+ }
125+ }
126+ out << std::endl;
127+ out << std::endl;
128+ }
129 }
130
131=== modified file 'src/ReachabilityChecker/SuccessorGenerator.hpp'
132--- src/ReachabilityChecker/SuccessorGenerator.hpp 2011-05-20 18:12:01 +0000
133+++ src/ReachabilityChecker/SuccessorGenerator.hpp 2012-07-06 19:00:26 +0000
134@@ -16,10 +16,12 @@
135 class SuccessorGenerator {
136 public:
137 SuccessorGenerator(const TAPN::TimedArcPetriNet & tapn, const MarkingFactory & factory, const VerificationOptions & options, unsigned int tokensInInitialMarking)
138- :tapn(tapn), factory(factory), arcsArray(), nInputArcs(tapn.GetNumberOfConsumingArcs()), options(options), tokenIndices(), maxUsedTokens(tokensInInitialMarking)
139+ :tapn(tapn), factory(factory), arcsArray(), nInputArcs(tapn.GetNumberOfConsumingArcs()), transitionStatistics(), numberOfTransitions(tapn.GetNumberOfTransitions()), options(options), tokenIndices(), maxUsedTokens(tokensInInitialMarking)
140 {
141 arcsArray = new unsigned [nInputArcs];
142+ transitionStatistics = new unsigned [numberOfTransitions];
143 tokenIndices = new boost::numeric::ublas::matrix<int>(nInputArcs, options.GetKBound());
144+ ClearTransitionsArray();
145 }
146
147 ;
148@@ -27,6 +29,7 @@
149 {
150 delete [] arcsArray;
151 delete tokenIndices;
152+ delete [] transitionStatistics;
153 }
154
155 ;
156@@ -34,6 +37,7 @@
157 void GenerateDiscreteTransitionsSuccessors(const SymbolicMarking & marking, std::vector<VerifyTAPN::Successor> & succ);
158 public:
159 void Print(std::ostream & out) const;
160+ void PrintTransitionStatistics(std::ostream & out) const;
161 public:
162 inline void ClearAll()
163 {
164@@ -46,6 +50,10 @@
165 memset(arcsArray, 0, nInputArcs * sizeof (arcsArray[0]));
166 }
167
168+ inline void ClearTransitionsArray() {
169+ memset(transitionStatistics, 0, numberOfTransitions * sizeof (transitionStatistics[0]));
170+ }
171+
172 inline void ClearTokenIndices()
173 {
174 tokenIndices->clear();
175@@ -55,7 +63,6 @@
176 {
177 return maxUsedTokens;
178 }
179-
180 private:
181 void CollectArcsAndAppropriateTokens(const TAPN::TimedTransition::Vector & transitions, const SymbolicMarking *marking);
182 void GenerateSuccessors(const TAPN::TimedTransition::Vector & transitions, const SymbolicMarking *marking, std::vector<Successor> & succ);
183@@ -71,6 +78,8 @@
184 const MarkingFactory& factory;
185 unsigned int* arcsArray;
186 unsigned int nInputArcs;
187+ unsigned int* transitionStatistics;
188+ const int numberOfTransitions;
189 const VerificationOptions& options;
190 boost::numeric::ublas::matrix<int>* tokenIndices;
191 unsigned int maxUsedTokens;
192
193=== modified file 'src/main.cpp'
194--- src/main.cpp 2011-11-25 20:48:31 +0000
195+++ src/main.cpp 2012-07-06 19:00:26 +0000
196@@ -148,6 +148,7 @@
197 std::cout << options << std::endl;
198 bool result = strategy->Verify();
199 std::cout << strategy->GetStats() << std::endl;
200+ strategy->PrintTransitionStatistics();
201 std::cout << "Query is " << (result ? "satisfied" : "NOT satisfied") << "." << std::endl;
202 std::cout << "Max number of tokens found in any reachable marking: ";
203 if(strategy->MaxUsedTokens() == options.GetKBound() + 1)

Subscribers

People subscribed via source and target branches