Merge lp:~tapaal-contributor/verifypn/Fix-partition-id-clash-1939939 into lp:verifypn

[Thomas Pedersen]

Fix place id clashing under unfolding

[Peter Gjøl Jensen (peter-gjoel)]

Passes the consistency check.

review: Approve

[Jiri Srba (srba)]

review: Approve

=== modified file 'include/PetriEngine/Colored/EquivalenceVec.h'
--- include/PetriEngine/Colored/EquivalenceVec.h	2021-06-21 09:39:53 +0000
+++ include/PetriEngine/Colored/EquivalenceVec.h	2021-08-18 16:43:45 +0000
@@ -26,6 +26,8 @@
                     return _equivalenceClasses;
                 }
 
+                const uint32_t getUniqueIdForColor(const Colored::Color *color) const; 
+
 
                 const std::vector<bool> & getDiagonalTuplePositions() const{
                     return _diagonalTuplePositions;

=== modified file 'src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp'
--- src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-07-17 13:05:59 +0000
+++ src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-08-18 16:43:45 +0000
@@ -519,17 +519,7 @@
                 transitionHasVarOutArcs = true;
             }
 
-            //If there is a varaible which was not found on an input arc or in the guard, we give it
-            //the full interval
-            for(auto* var : variables){
-                for(auto& varmap : transition.variableMaps){
-                    if(varmap.count(var) == 0){
-                        Colored::interval_vector_t intervalTuple;
-                        intervalTuple.addInterval(var->colorType->getFullInterval());
-                        varmap[var] = std::move(intervalTuple);
-                    }
-                }
-            }
+            
 
             //Apply partitioning to unbound outgoing variables such that 
             // bindings are only created for colors used in the rest of the net
@@ -545,6 +535,19 @@
                         }                    
                     }                
                 }
+            } else {
+                // Else if partitioning was not computed or diagonal
+                // and there is a varaible which was not found on an input arc or in the guard, 
+                // we give it the full interval
+                for(auto* var : variables){
+                    for(auto& varmap : transition.variableMaps){
+                        if(varmap.count(var) == 0){
+                            Colored::interval_vector_t intervalTuple;
+                            intervalTuple.addInterval(var->colorType->getFullInterval());
+                            varmap[var] = std::move(intervalTuple);
+                        }
+                    }
+                }
             }
 
             auto intervals = arc.expr->getOutputIntervals(transition.variableMaps);
@@ -712,7 +715,6 @@
 
     void ColoredPetriNetBuilder::unfoldTransition(uint32_t transitionId) {
         const Colored::Transition &transition = _transitions[transitionId];
-
         if(_fixpointDone || _partitionComputed){ 
             FixpointBindingGenerator gen(transition, _colors, symmetric_var_map[transitionId]);
             size_t i = 0;
@@ -811,13 +813,14 @@
             if(!_partitionComputed || _partition[arc.place].isDiagonal()){
                 id = newColor->getId();
             } else {
-                id = _partition[arc.place].getColorEqClassMap().find(newColor)->second->id() + newColor->getId();
+                id = _partition[arc.place].getUniqueIdForColor(newColor);                
             }
             const std::string& pName = _ptplacenames[place.name][id];
+
             if (pName.empty()) {                               
                 unfoldPlace(&place, newColor, arc.place, id);               
             }
-            
+
             if (arc.input) {
                 _ptBuilder.addInputArc(pName, tName, false, color.second);
             } else {

=== modified file 'src/PetriEngine/Colored/EquivalenceVec.cpp'
--- src/PetriEngine/Colored/EquivalenceVec.cpp	2021-06-22 13:10:13 +0000
+++ src/PetriEngine/Colored/EquivalenceVec.cpp	2021-08-18 16:43:45 +0000
@@ -23,7 +23,7 @@
                                     }
                                 }
                                 newIntervalTuple.addInterval(std::move(singleInterval));
-                                continue;
+                                break;
                             }
                         }
                     }
@@ -51,7 +51,7 @@
         }
 
         void EquivalenceVec::addColorToEqClassMap(const Color *color){
-            for(auto& eqClass : _equivalenceClasses){   
+            for(auto& eqClass : _equivalenceClasses){  
                 std::vector<uint32_t> colorIds;
                 color->getTupleId(colorIds);
                 if(eqClass.containsColor(colorIds, _diagonalTuplePositions)){
@@ -82,5 +82,31 @@
                 }
             }
         }
+
+        //Add color ids of diagonal positions as we represent partitions with diagonal postitions 
+        //as a single equivalence class to save space, but they should not be partition together
+        const uint32_t EquivalenceVec::getUniqueIdForColor(const Colored::Color *color) const {
+            PetriEngine::Colored::EquivalenceClass *eqClass = _colorEQClassMap.find(color)->second;
+            
+            std::vector<uint32_t> colorTupleIds;
+            std::vector<uint32_t> newColorTupleIds;
+            bool hasDiagonalPositions;
+            color->getTupleId(colorTupleIds);
+            for(uint32_t i = 0; i < colorTupleIds.size(); i++){
+                if(_diagonalTuplePositions[i]){
+                    newColorTupleIds.push_back(colorTupleIds[i]);
+                } else {
+                    hasDiagonalPositions = true;
+                    newColorTupleIds.push_back(eqClass->intervals().back().getLowerIds()[i]);
+                }
+            }
+
+            if(hasDiagonalPositions){
+                return eqClass->id() + color->getColorType()->getColor(newColorTupleIds)->getId();
+            }
+
+            return eqClass->id();
+            
+        }
     }
 }
\ No newline at end of file

=== modified file 'src/PetriEngine/Colored/IntervalGenerator.cpp'
--- src/PetriEngine/Colored/IntervalGenerator.cpp	2021-06-24 11:38:08 +0000
+++ src/PetriEngine/Colored/IntervalGenerator.cpp	2021-08-18 16:43:45 +0000
@@ -146,7 +146,8 @@
                     localVarMap[pair.first] = varIntervals;
                 }
 
-                if(validInterval){
+                //Only add valid intervals. Ensure one empty map is always added if there are intervals
+                if(validInterval && (!localVarMap.empty() || variableMaps.empty())){
                     variableMaps.push_back(std::move(localVarMap));
                 }                          
             }  
@@ -159,7 +160,7 @@
                     //If we have not found intervals for any place yet, we fill the intervals from this place
                     //Else we restrict the intervals we already found to only keep those that can also be matched in this place
                     if(variableMaps.empty()){                    
-                        fillVarMaps(variableMaps, placeArcInterval.second, intervalTupleSize, j);                                            
+                        fillVarMaps(variableMaps, placeArcInterval.second, intervalTupleSize, j);   
                     } else {
                         std::vector<VariableIntervalMap> newVarMapVec;
                         
@@ -177,13 +178,13 @@
                                     }
                                 }
 
-                                if(allVarsAssigned){
+                                if(allVarsAssigned && (!localVarMap.empty() || newVarMapVec.empty())){
                                     newVarMapVec.push_back(std::move(localVarMap));
                                 }
                                                             
                             }                                                                                    
-                        }               
-                        variableMaps = std::move(newVarMapVec);                    
+                        }
+                        variableMaps = std::move(newVarMapVec);                       
                     }
                     //If we did not find any intervals for an arc, then the transition cannot be activated
                     if(variableMaps.empty()){

=== modified file 'src/PetriEngine/Colored/PartitionBuilder.cpp'
--- src/PetriEngine/Colored/PartitionBuilder.cpp	2021-07-05 21:22:08 +0000
+++ src/PetriEngine/Colored/PartitionBuilder.cpp	2021-08-18 16:43:45 +0000
@@ -85,6 +85,7 @@
                 if(eqVec.second.isDiagonal()){
                     continue;
                 }
+                
                 const ColorType *colorType = _places[eqVec.first].type;
                 for(uint32_t i = 0; i < colorType->size(); i++){ 
                     const Color *color = &(*colorType)[i];