Merge lp:~verifypn-cpn/verifypn/color-fixpoint into lp:~tapaal-ltl/verifypn/mcc2021

[Thomas Pedersen]

Merge color fixpoint into MCC2021

Colored net unfolding has been tested, but the LTL code still needs to be tested

We believe the previous errors have been corrected

=== modified file 'include/PetriEngine/Colored/ColoredPetriNetBuilder.h'
--- include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2021-03-17 13:16:57 +0000
+++ include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2021-03-26 10:35:05 +0000
@@ -182,7 +182,7 @@
         
         void unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color);
         void unfoldTransition(Colored::Transition& transition);
-        void handleOrphanPlace(Colored::Place& place);
+        void handleOrphanPlace(Colored::Place& place, std::unordered_map<std::string, uint32_t> unfoldedPlaceMap);
 
         void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name, bool input);
     };

=== modified file 'include/PetriEngine/Colored/Intervals.h'
--- include/PetriEngine/Colored/Intervals.h	2021-03-15 10:04:47 +0000
+++ include/PetriEngine/Colored/Intervals.h	2021-03-26 10:35:05 +0000
@@ -475,7 +475,6 @@
 
             void applyModifier(int32_t modifier, std::vector<size_t> sizes){
                 std::vector<interval_t> collectedIntervals;
-
                 for(auto& interval : _intervals){
                     std::vector<interval_t> newIntervals;
                     newIntervals.push_back(std::move(interval));
@@ -494,15 +493,15 @@
                                 newInterval[i]._upper = sizes[i]-1;
                                 tempIntervals.push_back(std::move(newInterval));
                             }else {
-                                interval[i]._lower = shiftedInterval.first;
-                                interval[i]._upper = shiftedInterval.second;
+                                interval1[i]._lower = shiftedInterval.first;
+                                interval1[i]._upper = shiftedInterval.second;
                             }
                         }
                         newIntervals.insert(newIntervals.end(), tempIntervals.begin(), tempIntervals.end());                                                
                     }
                     collectedIntervals.insert(collectedIntervals.end(), newIntervals.begin(), newIntervals.end());
                 }
-
+                
                 _intervals = std::move(collectedIntervals);
             }
 

=== modified file 'src/PetriEngine/Colored/BindingGenerator.cpp'
--- src/PetriEngine/Colored/BindingGenerator.cpp	2021-03-15 10:04:47 +0000
+++ src/PetriEngine/Colored/BindingGenerator.cpp	2021-03-26 10:35:05 +0000
@@ -105,18 +105,19 @@
         while (!test) {
             bool next = true;
 
-            for (auto& _binding : _bindings) {
-                auto varInterval = _transition.variableMaps[_nextIndex][_binding.first];
+            for (auto& _binding : _bindings) {               
+                auto varInterval = _transition.variableMaps[_nextIndex][_binding.first];                
                 std::vector<uint32_t> colorIds;
                 _binding.second->getTupleId(&colorIds);
                 auto nextIntervalBinding = varInterval.isRangeEnd(colorIds);
 
-                if (nextIntervalBinding.size() == 0){
+                if (nextIntervalBinding.size() == 0){                    
                     _binding.second = &_binding.second->operator++();
                     next = false;
                     break;                    
                 } else {
                     _binding.second = _binding.second->getColorType()->getColor(nextIntervalBinding.getLowerIds());
+                    
                     if(!nextIntervalBinding.equals(varInterval.getFirst())){
                         next = false;
                         break;
@@ -132,10 +133,8 @@
                 for(auto& _binding : _bindings){
                     _binding.second =  _binding.second->getColorType()->getColor(_transition.variableMaps[_nextIndex][_binding.first].getFirst().getLowerIds());
                 }
-            }
-                 
+            }                 
             test = eval();
-        
         }
         
         return _bindings;

=== modified file 'src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp'
--- src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-03-17 13:16:57 +0000
+++ src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-03-26 10:35:05 +0000
@@ -197,7 +197,7 @@
 
         _fixPointCreationTime = (std::chrono::duration_cast<std::chrono::microseconds>(end - start).count())*0.000001;
 
-        // printPlaceTable();
+        //printPlaceTable();
         _placeColorFixpoints.clear();
     }
 
@@ -331,8 +331,9 @@
             for (auto& transition : _transitions) {
                 unfoldTransition(transition);
             }
+            auto unfoldedPlaceMap = _ptBuilder.getPlaceNames();
             for (auto& place : _places) {
-               handleOrphanPlace(place);
+               handleOrphanPlace(place, unfoldedPlaceMap);
             }
             _unfolded = true;
             auto end = std::chrono::high_resolution_clock::now();
@@ -345,17 +346,33 @@
     //However, in queries asking about orphan places it cannot find these, as they have not been unfolded
     //so we make a placeholder place which just has tokens equal to the number of colored tokens
     //Ideally, orphan places should just be translated to a constant in the query
-    void ColoredPetriNetBuilder::handleOrphanPlace(Colored::Place& place) {
-        if(_ptplacenames.count(place.name) <= 0){   
-            std::string name = place.name + "_" + std::to_string(place.marking.size());
+    void ColoredPetriNetBuilder::handleOrphanPlace(Colored::Place& place, std::unordered_map<std::string, uint32_t> unfoldedPlaceMap) {
+        if(_ptplacenames.count(place.name) <= 0){
+            
+            std::string name = place.name + "_orphan";
             _ptBuilder.addPlace(name, place.marking.size(), 0.0, 0.0);
             _ptplacenames[place.name][0] = std::move(name);
+        } else {
+            uint32_t usedTokens = 0;
+            
+            for(std::pair<const uint32_t, std::string> unfoldedPlace : _ptplacenames[place.name]){                
+                auto unfoldedMarking = _ptBuilder.initMarking();
+                
+                auto unfoldedPlaceId = unfoldedPlaceMap[unfoldedPlace.second];
+                usedTokens += unfoldedMarking[unfoldedPlaceId];
+            }
+            
+            if(place.marking.size() > usedTokens){
+                std::string name = place.name + "_orphan";
+                _ptBuilder.addPlace(name, place.marking.size() - usedTokens, 0.0, 0.0);
+                _ptplacenames[place.name][UINT32_MAX] = std::move(name);
+            }
         }
         
         //++_nptplaces;        
     }
     
-    void ColoredPetriNetBuilder::unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color) {
+    void ColoredPetriNetBuilder::unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color) {        
         std::string name = place->name + "_" + std::to_string(color->getId());
         _ptBuilder.addPlace(name, place->marking[color], 0.0, 0.0);
         _ptplacenames[place->name][color->getId()] = std::move(name);
@@ -365,7 +382,7 @@
     void ColoredPetriNetBuilder::unfoldTransition(Colored::Transition& transition) {
         FixpointBindingGenerator gen(transition, _colors);
         size_t i = 0;
-        for (auto b : gen) {                  
+        for (auto b : gen) { 
             std::string name = transition.name + "_" + std::to_string(i++);
             _ptBuilder.addTransition(name, 0.0, 0.0);
             _pttransitionnames[transition.name].push_back(name);

=== modified file 'src/PetriEngine/Colored/GuardRestrictor.cpp'
--- src/PetriEngine/Colored/GuardRestrictor.cpp	2021-03-15 10:04:47 +0000
+++ src/PetriEngine/Colored/GuardRestrictor.cpp	2021-03-26 10:35:05 +0000
@@ -244,7 +244,7 @@
                         //comparing vars of same size
                         if(varPositionPair.second->colorType->productSize() == varPositionsR->operator[](index)->colorType->productSize()){
                             intervalTuple_t newIntervalTuple = getIntervalOverlap(&leftTupleIntervalVal._intervals, &rightTupleIntervalVal._intervals);
-                        
+
                             *leftTupleInterval = newIntervalTuple;
                             *rightTupleInterval = newIntervalTuple;
                             leftTupleInterval->applyModifier(leftVarModifier, varPositionPair.second->colorType->getConstituentsSizes());