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

[Thomas Pedersen]

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

[lp:~tapaal-contributor/verifypn/show-reduced-net]

227. By <email address hidden> on 2020-09-18

fixed compilation with static libraries for mac

[Jiri Srba (srba)]

review: Approve

[lp:~tapaal-contributor/verifypn/show-reduced-net]

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

=== modified file 'include/PetriEngine/PetriNet.h'
--- include/PetriEngine/PetriNet.h	2020-04-22 07:57:20 +0000
+++ include/PetriEngine/PetriNet.h	2020-10-19 19:48:12 +0000
@@ -124,6 +124,9 @@
         std::vector<std::string> _transitionnames;
         std::vector<std::string> _placenames;
 
+        std::vector< std::tuple<double, double> > _placelocations;
+        std::vector< std::tuple<double, double> > _transitionlocations;
+
         friend class PetriNetBuilder;
         friend class Reducer;
         friend class SuccessorGenerator;

=== modified file 'include/PetriEngine/PetriNetBuilder.h'
--- include/PetriEngine/PetriNetBuilder.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/PetriNetBuilder.h	2020-10-19 19:48:12 +0000
@@ -131,6 +131,9 @@
     protected:
         std::unordered_map<std::string, uint32_t> _placenames;
         std::unordered_map<std::string, uint32_t> _transitionnames;
+
+        std::vector< std::tuple<double, double> > _placelocations;
+        std::vector< std::tuple<double, double> > _transitionlocations;
         
         std::vector<Transition> _transitions;
         std::vector<Place> _places;

=== modified file 'src/PetriEngine/PetriNet.cpp'
--- src/PetriEngine/PetriNet.cpp	2020-03-13 13:35:25 +0000
+++ src/PetriEngine/PetriNet.cpp	2020-10-19 19:48:12 +0000
@@ -191,7 +191,10 @@
         for(size_t i = 0; i < _nplaces; ++i)
         {
             auto& p = _placenames[i];
+            auto& placelocation = _placelocations[i];
             out << "<place id=\"" << p << "\">\n"
+                << "<graphics><position x=\"" << get<0>(placelocation) 
+                << "\" y=\"" << get<1>(placelocation) << "\"/></graphics>\n"
                 << "<name><text>" << p << "</text></name>\n";
             if(_initialMarking[i] > 0)
             {
@@ -201,8 +204,11 @@
         }
         for(size_t i = 0; i < _ntransitions; ++i)
         {
+            auto& transitionlocation = _transitionlocations[i];
             out << "<transition id=\"" << _transitionnames[i] << "\">\n"
                 << "<name><text>" << _transitionnames[i] << "</text></name>\n";
+            out << "<graphics><position x=\"" << get<0>(transitionlocation) 
+                << "\" y=\"" << get<1>(transitionlocation) << "\"/></graphics>\n";
             out << "</transition>\n";
         }
         size_t id = 0;

=== modified file 'src/PetriEngine/PetriNetBuilder.cpp'
--- src/PetriEngine/PetriNetBuilder.cpp	2020-03-02 21:03:24 +0000
+++ src/PetriEngine/PetriNetBuilder.cpp	2020-10-19 19:48:12 +0000
@@ -38,18 +38,20 @@
     }
     PetriNetBuilder::PetriNetBuilder(const PetriNetBuilder& other)
     : _placenames(other._placenames), _transitionnames(other._transitionnames),
+       _placelocations(other._placelocations), _transitionlocations(other._transitionlocations),
        _transitions(other._transitions), _places(other._places), 
        initialMarking(other.initialMarking), reducer(this)
     {
 
     }
 
-    void PetriNetBuilder::addPlace(const string &name, int tokens, double, double) {
+    void PetriNetBuilder::addPlace(const string &name, int tokens, double x, double y) {
         if(_placenames.count(name) == 0)
         {
             uint32_t next = _placenames.size();
             _places.emplace_back();
             _placenames[name] = next;
+            _placelocations.push_back(std::tuple<double, double>(x,y));
         }
         
         uint32_t id = _placenames[name];
@@ -60,12 +62,13 @@
     }
 
     void PetriNetBuilder::addTransition(const string &name,
-            double, double) {
+            double x, double y) {
         if(_transitionnames.count(name) == 0)
         {
             uint32_t next = _transitionnames.size();
             _transitions.emplace_back();
             _transitionnames[name] = next;
+            _transitionlocations.push_back(std::tuple<double, double>(x,y));
         }
     }
 
@@ -318,6 +321,7 @@
             ++free;
             next = nextPlaceId(place_cons_count, place_prod_count, place_idmap, reorder);
         }
+
         
         // Reindex for great justice!
         for(uint32_t i = 0; i < freeinv; i++)
@@ -336,6 +340,9 @@
 //                std::cout << place_idmap[i] << " : " << initialMarking[i] << std::endl;
             }
         }
+
+        net->_placelocations = _placelocations;
+        net->_transitionlocations = _transitionlocations;
         
         // reindex place-names
 
@@ -343,15 +350,18 @@
         int rindex = _placenames.size() - 1;
         for(auto& i : _placenames)
         {
+            auto& placelocation = _placelocations[i.second];
             i.second = place_idmap[i.second];
             if(i.second != std::numeric_limits<uint32_t>::max())
             {
                 net->_placenames[i.second] = i.first;
                 assert(_placenames[net->_placenames[i.second]] == i.second);
+                net->_placelocations[i.second] = placelocation;
             }
             else
             {
                 net->_placenames[rindex] = i.first;
+                net->_placelocations[rindex] = placelocation;
                 --rindex;
             }
         }
@@ -360,14 +370,17 @@
         int trindex = _transitionnames.size() - 1;
         for(auto& i : _transitionnames)
         {
+            auto& transitionlocation = _transitionlocations[i.second];
             i.second = trans_idmap[i.second];
             if(i.second != std::numeric_limits<uint32_t>::max())
             {
                 net->_transitionnames[i.second] = i.first;
+                net->_transitionlocations[i.second] = transitionlocation;
             }
             else
             {
                 net->_transitionnames[trindex] = i.first;
+                net->_transitionlocations[trindex] = transitionlocation;
                 --trindex;
             }
         }

=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp	2020-04-28 20:13:40 +0000
+++ src/VerifyPN.cpp	2020-10-19 19:48:12 +0000
@@ -372,6 +372,7 @@
             printf("                        Søren Moss Nielsen <[e-mail]>\n");
             printf("                        Thomas Søndersø Nielsen <[e-mail]>\n");
             printf("                        Samuel Pastva <[e-mail]>\n");
+            printf("                        Thomas Pedersen <[e-mail]\n");
             printf("                        Jiri Srba <[e-mail]>\n");
             printf("                        Lars Kærlund Østergaard <[e-mail]>\n");
             printf("GNU GPLv3 or later <http://gnu.org/licenses/gpl.html>\n");