Merge lp:~tapaal-contributor/verifypn/show-reduced-net into lp:verifypn

Proposed by Thomas Pedersen on 2020-09-18
Status: Merged
Approved by: Jiri Srba on 2020-10-31
Approved revision: no longer in the source branch.
Merged at revision: 228
Proposed branch: lp:~tapaal-contributor/verifypn/show-reduced-net
Merge into: lp:verifypn
Diff against target: 162 lines (+28/-2)
5 files modified
include/PetriEngine/PetriNet.h (+3/-0)
include/PetriEngine/PetriNetBuilder.h (+3/-0)
src/PetriEngine/PetriNet.cpp (+6/-0)
src/PetriEngine/PetriNetBuilder.cpp (+15/-2)
src/VerifyPN.cpp (+1/-0)
To merge this branch: bzr merge lp:~tapaal-contributor/verifypn/show-reduced-net
Reviewer Review Type Date Requested Status
Jiri Srba 2020-09-18 Approve on 2020-10-31
Peter Gjøl Jensen 2020-09-18 Pending
Review via email: mp+390959@code.launchpad.net

Commit message

Added place and transition locations to the petri net and include them when writing the reduced net.

This change was made to retain locations for the reduced net in the bug https://bugs.launchpad.net/tapaal/+bug/1879130

To post a comment you must log in.
227. By <email address hidden> on 2020-09-18

fixed compilation with static libraries for mac

Jiri Srba (srba) :
review: Approve
228. By Jiri Srba on 2020-10-31

merged in lp:~tapaal-contributor/verifypn/show-reduced-net adding x,y coordinates when eexporting reduced net

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'include/PetriEngine/PetriNet.h'
2--- include/PetriEngine/PetriNet.h 2020-04-22 07:57:20 +0000
3+++ include/PetriEngine/PetriNet.h 2020-10-19 19:48:12 +0000
4@@ -124,6 +124,9 @@
5 std::vector<std::string> _transitionnames;
6 std::vector<std::string> _placenames;
7
8+ std::vector< std::tuple<double, double> > _placelocations;
9+ std::vector< std::tuple<double, double> > _transitionlocations;
10+
11 friend class PetriNetBuilder;
12 friend class Reducer;
13 friend class SuccessorGenerator;
14
15=== modified file 'include/PetriEngine/PetriNetBuilder.h'
16--- include/PetriEngine/PetriNetBuilder.h 2020-03-02 21:03:24 +0000
17+++ include/PetriEngine/PetriNetBuilder.h 2020-10-19 19:48:12 +0000
18@@ -131,6 +131,9 @@
19 protected:
20 std::unordered_map<std::string, uint32_t> _placenames;
21 std::unordered_map<std::string, uint32_t> _transitionnames;
22+
23+ std::vector< std::tuple<double, double> > _placelocations;
24+ std::vector< std::tuple<double, double> > _transitionlocations;
25
26 std::vector<Transition> _transitions;
27 std::vector<Place> _places;
28
29=== modified file 'src/PetriEngine/PetriNet.cpp'
30--- src/PetriEngine/PetriNet.cpp 2020-03-13 13:35:25 +0000
31+++ src/PetriEngine/PetriNet.cpp 2020-10-19 19:48:12 +0000
32@@ -191,7 +191,10 @@
33 for(size_t i = 0; i < _nplaces; ++i)
34 {
35 auto& p = _placenames[i];
36+ auto& placelocation = _placelocations[i];
37 out << "<place id=\"" << p << "\">\n"
38+ << "<graphics><position x=\"" << get<0>(placelocation)
39+ << "\" y=\"" << get<1>(placelocation) << "\"/></graphics>\n"
40 << "<name><text>" << p << "</text></name>\n";
41 if(_initialMarking[i] > 0)
42 {
43@@ -201,8 +204,11 @@
44 }
45 for(size_t i = 0; i < _ntransitions; ++i)
46 {
47+ auto& transitionlocation = _transitionlocations[i];
48 out << "<transition id=\"" << _transitionnames[i] << "\">\n"
49 << "<name><text>" << _transitionnames[i] << "</text></name>\n";
50+ out << "<graphics><position x=\"" << get<0>(transitionlocation)
51+ << "\" y=\"" << get<1>(transitionlocation) << "\"/></graphics>\n";
52 out << "</transition>\n";
53 }
54 size_t id = 0;
55
56=== modified file 'src/PetriEngine/PetriNetBuilder.cpp'
57--- src/PetriEngine/PetriNetBuilder.cpp 2020-03-02 21:03:24 +0000
58+++ src/PetriEngine/PetriNetBuilder.cpp 2020-10-19 19:48:12 +0000
59@@ -38,18 +38,20 @@
60 }
61 PetriNetBuilder::PetriNetBuilder(const PetriNetBuilder& other)
62 : _placenames(other._placenames), _transitionnames(other._transitionnames),
63+ _placelocations(other._placelocations), _transitionlocations(other._transitionlocations),
64 _transitions(other._transitions), _places(other._places),
65 initialMarking(other.initialMarking), reducer(this)
66 {
67
68 }
69
70- void PetriNetBuilder::addPlace(const string &name, int tokens, double, double) {
71+ void PetriNetBuilder::addPlace(const string &name, int tokens, double x, double y) {
72 if(_placenames.count(name) == 0)
73 {
74 uint32_t next = _placenames.size();
75 _places.emplace_back();
76 _placenames[name] = next;
77+ _placelocations.push_back(std::tuple<double, double>(x,y));
78 }
79
80 uint32_t id = _placenames[name];
81@@ -60,12 +62,13 @@
82 }
83
84 void PetriNetBuilder::addTransition(const string &name,
85- double, double) {
86+ double x, double y) {
87 if(_transitionnames.count(name) == 0)
88 {
89 uint32_t next = _transitionnames.size();
90 _transitions.emplace_back();
91 _transitionnames[name] = next;
92+ _transitionlocations.push_back(std::tuple<double, double>(x,y));
93 }
94 }
95
96@@ -318,6 +321,7 @@
97 ++free;
98 next = nextPlaceId(place_cons_count, place_prod_count, place_idmap, reorder);
99 }
100+
101
102 // Reindex for great justice!
103 for(uint32_t i = 0; i < freeinv; i++)
104@@ -336,6 +340,9 @@
105 // std::cout << place_idmap[i] << " : " << initialMarking[i] << std::endl;
106 }
107 }
108+
109+ net->_placelocations = _placelocations;
110+ net->_transitionlocations = _transitionlocations;
111
112 // reindex place-names
113
114@@ -343,15 +350,18 @@
115 int rindex = _placenames.size() - 1;
116 for(auto& i : _placenames)
117 {
118+ auto& placelocation = _placelocations[i.second];
119 i.second = place_idmap[i.second];
120 if(i.second != std::numeric_limits<uint32_t>::max())
121 {
122 net->_placenames[i.second] = i.first;
123 assert(_placenames[net->_placenames[i.second]] == i.second);
124+ net->_placelocations[i.second] = placelocation;
125 }
126 else
127 {
128 net->_placenames[rindex] = i.first;
129+ net->_placelocations[rindex] = placelocation;
130 --rindex;
131 }
132 }
133@@ -360,14 +370,17 @@
134 int trindex = _transitionnames.size() - 1;
135 for(auto& i : _transitionnames)
136 {
137+ auto& transitionlocation = _transitionlocations[i.second];
138 i.second = trans_idmap[i.second];
139 if(i.second != std::numeric_limits<uint32_t>::max())
140 {
141 net->_transitionnames[i.second] = i.first;
142+ net->_transitionlocations[i.second] = transitionlocation;
143 }
144 else
145 {
146 net->_transitionnames[trindex] = i.first;
147+ net->_transitionlocations[trindex] = transitionlocation;
148 --trindex;
149 }
150 }
151
152=== modified file 'src/VerifyPN.cpp'
153--- src/VerifyPN.cpp 2020-04-28 20:13:40 +0000
154+++ src/VerifyPN.cpp 2020-10-19 19:48:12 +0000
155@@ -372,6 +372,7 @@
156 printf(" Søren Moss Nielsen <soren_moss@mac.com>\n");
157 printf(" Thomas Søndersø Nielsen <primogens@gmail.com>\n");
158 printf(" Samuel Pastva <daemontus@gmail.com>\n");
159+ printf(" Thomas Pedersen <thomas.pedersen@stofanet.dk\n");
160 printf(" Jiri Srba <srba.jiri@gmail.com>\n");
161 printf(" Lars Kærlund Østergaard <larsko@gmail.com>\n");
162 printf("GNU GPLv3 or later <http://gnu.org/licenses/gpl.html>\n");

Subscribers

People subscribed via source and target branches