Merge lp:~verifypn-cpn/verifypn/partitioning into lp:verifypn

[Thomas Pedersen]

Merge in parsing of vehicularWifi (Untested)

[lp:~verifypn-cpn/verifypn/partitioning]

276. By Thomas Pedersen <email address hidden> on 2021-04-26

Disable partitioning of unbound variables when partitioning is disabled

277. By Thomas Pedersen <email address hidden> on 2021-04-26

Disable partitioning when computing statespace

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

passes all tests on the competition script

[Jiri Srba (srba)]

review: Approve

=== modified file 'include/PetriEngine/Colored/Colors.h'
--- include/PetriEngine/Colored/Colors.h	2021-04-14 10:41:18 +0000
+++ include/PetriEngine/Colored/Colors.h	2021-04-26 08:36:24 +0000
@@ -207,6 +207,10 @@
             virtual void getColortypes(std::vector<ColorType *> &colorTypes){
                 colorTypes.push_back(this);
             }
+
+            virtual void printConstituents(){
+                std::cout << _name << std::endl;
+            }
             
             virtual const Color& operator[] (size_t index) {
                 return _colors[index];
@@ -322,6 +326,12 @@
                 return true;
             }
 
+            void printConstituents() override{
+                for(auto ct : constituents){
+                   ct->printConstituents();
+                }
+            }
+
             const ColorType* getNestedColorType(size_t index) {
                 return constituents[index];
             }
@@ -377,6 +387,11 @@
                 return true;
             }
         };
+
+        struct ColorTypePartition {
+            std::vector<const Color *> colors;
+            std::string name;
+        };
     }
 }
 

=== modified file 'include/PetriEngine/Colored/Expressions.h'
--- include/PetriEngine/Colored/Expressions.h	2021-04-14 11:51:52 +0000
+++ include/PetriEngine/Colored/Expressions.h	2021-04-26 08:36:24 +0000
@@ -62,6 +62,7 @@
             ProductType* findProductColorType(const std::vector<const ColorType*>& types) const {
                 for (auto& elem : colorTypes) {
                     auto* pt = dynamic_cast<ProductType*>(elem.second);
+
                     if (pt && pt->containsTypes(types)) {
                         return pt;
                     }
@@ -490,7 +491,7 @@
                     types.push_back(colors.back()->getColorType());
                 }
                 ProductType* pt = context.findProductColorType(types);
-
+                assert(pt != nullptr);
                 const Color* col = pt->getColor(colors);
                 assert(col != nullptr);
                 return col;
@@ -548,17 +549,24 @@
             }
 
             ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                
                 std::vector<const ColorType*> types;
+                if(_colorType != nullptr){
+                    return _colorType;
+                }
+
                 for (auto color : _colors) {
                     types.push_back(color->getColorType(colorTypes));
                 }
-                for (auto& elem : colorTypes) {
+                
+                for (auto elem : colorTypes) {
                     auto* pt = dynamic_cast<ProductType*>(elem.second);
                     if (pt && pt->containsTypes(types)) {
                         return pt;
                     }
                 }
                 std::cout << "COULD NOT FIND PRODUCT TYPE" << std::endl;
+                assert(false);
                 return nullptr;
             }
 
@@ -1160,7 +1168,6 @@
                 for (auto elem : _color) {
                     //TODO: can there be more than one element in a number of expression?
                     elem->getVariables(variables, varPositions, varModifierMap, index);
-                    //(*index)++;
                 }
             }
 
@@ -1168,13 +1175,13 @@
                 if (_all != nullptr) {
                     return _all->getArcIntervals(arcIntervals, cfp, index, modifier);
                 }
-                uint32_t i = 0;
+                //uint32_t i = 0;
                 for (auto elem : _color) {
-                    (*index) += i;
+                    //(*index) += i;
                     if(!elem->getArcIntervals(arcIntervals, cfp, index, modifier)){
                         return false;
                     }
-                    i++;
+                    //i++;
                 }
                 return true;
             }
@@ -1210,7 +1217,6 @@
                     for(auto pair : elemMap){
                         constantMap[pair.first].push_back(pair.second);
                     }
-                    index++;//not sure if index should be increased here, but no number expression have multiple elements
                 }
             }
 

=== modified file 'include/PetriEngine/Colored/Intervals.h'
--- include/PetriEngine/Colored/Intervals.h	2021-04-14 10:41:18 +0000
+++ include/PetriEngine/Colored/Intervals.h	2021-04-26 08:36:24 +0000
@@ -360,15 +360,9 @@
                     enum FoundPlace {undecided, greater, lower};
                     FoundPlace foundPlace = undecided;
 
-                    //uint32_t allowedDist = 1;
-
                     for(uint32_t k = 0; k < interval.size(); k++){
                         if(interval[k]._lower > localInterval[k]._upper  || localInterval[k]._lower > interval[k]._upper){
-                            //if(interval[k]._lower > localInterval[k]._upper + allowedDist  || localInterval[k]._lower > interval[k]._upper + allowedDist){
-                                extendsInterval = false;
-                            // } else {
-                            //     allowedDist = 0;
-                            // }
+                            extendsInterval = false;
                         }
                         if(interval[k]._lower < localInterval[k]._lower){
                             if(foundPlace == undecided){

=== modified file 'include/PetriEngine/Colored/PartitionBuilder.h'
--- include/PetriEngine/Colored/PartitionBuilder.h	2021-04-07 08:41:47 +0000
+++ include/PetriEngine/Colored/PartitionBuilder.h	2021-04-26 08:36:24 +0000
@@ -6,7 +6,17 @@
     namespace Colored {
         class PartitionBuilder {
             public:
-                PartitionBuilder(std::vector<Transition> *transitions, std::vector<Place> *places, std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap);
+                PartitionBuilder(std::vector<Transition> *transitions, 
+                                std::vector<Place> *places, 
+                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, 
+                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap);
+
+                PartitionBuilder(std::vector<Transition> *transitions, 
+                                std::vector<Place> *places, 
+                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, 
+                                std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap,
+                                std::vector<Colored::ColorFixpoint> *placeColorFixpoints);
+                
                 ~PartitionBuilder() {}
 
                 //void initPartition();

=== modified file 'include/PetriParse/PNMLParser.h'
--- include/PetriParse/PNMLParser.h	2021-04-14 10:41:18 +0000
+++ include/PetriParse/PNMLParser.h	2021-04-26 08:36:24 +0000
@@ -83,6 +83,7 @@
     void parseArc(rapidxml::xml_node<>* element, bool inhibitor = false);
     void parseTransition(rapidxml::xml_node<>* element);
     void parseDeclarations(rapidxml::xml_node<>* element);
+    void parsePartitions(rapidxml::xml_node<>* element);
     void parseNamedSort(rapidxml::xml_node<>* element);
     PetriEngine::Colored::ArcExpression_ptr parseArcExpression(rapidxml::xml_node<>* element);
     PetriEngine::Colored::GuardExpression_ptr parseGuardExpression(rapidxml::xml_node<>* element, bool notFlag);
@@ -99,6 +100,7 @@
     void parseQueries(rapidxml::xml_node<>* element);
     const PetriEngine::Colored::Color* findColor(const char* name) const;
     const PetriEngine::Colored::Color* findColorForIntRange(const char* value, uint32_t start, uint32_t end) const;
+    std::vector<PetriEngine::Colored::ColorExpression_ptr> findPartitionColors(rapidxml::xml_node<>* element) const;
     std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> cartesianProduct(std::vector<PetriEngine::Colored::ColorExpression_ptr> rightVector, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftVector);
     std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> cartesianProduct(std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> rightVector, std::vector<PetriEngine::Colored::ColorExpression_ptr> leftVector);
     PetriEngine::AbstractPetriNetBuilder* builder;
@@ -110,6 +112,8 @@
     VariableMap variables;
     bool isColored;
     std::vector<Query> queries;
+    std::vector<PetriEngine::Colored::ColorTypePartition> partitions;
+    std::vector<std::pair<char *, PetriEngine::Colored::ProductType*>> missingCTs;
 };
 
 #endif // PNMLPARSER_H
\ No newline at end of file

=== modified file 'src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp'
--- src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-04-14 11:51:52 +0000
+++ src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2021-04-26 08:36:24 +0000
@@ -138,6 +138,21 @@
     void ColoredPetriNetBuilder::sort() {
     }
 
+    //----------------------- Partitioning -----------------------//
+
+    void ColoredPetriNetBuilder::computePartition(){
+        auto partitionStart = std::chrono::high_resolution_clock::now();
+        Colored::PartitionBuilder pBuilder = _fixpointDone? Colored::PartitionBuilder(&_transitions, &_places, &_placePostTransitionMap, &_placePreTransitionMap, &_placeColorFixpoints) : Colored::PartitionBuilder(&_transitions, &_places, &_placePostTransitionMap, &_placePreTransitionMap);
+        
+        pBuilder.partitionNet();
+        //pBuilder.printPartion();
+        _partition = pBuilder.getPartition();
+        pBuilder.assignColorMap(_partition);
+        _partitionComputed = true;
+        auto partitionEnd = std::chrono::high_resolution_clock::now();
+        _partitionTimer = (std::chrono::duration_cast<std::chrono::microseconds>(partitionEnd - partitionStart).count())*0.000001;
+    }
+
     //----------------------- Color fixpoint -----------------------//
 
     void ColoredPetriNetBuilder::printPlaceTable() {
@@ -157,17 +172,7 @@
         }
     }
 
-    void ColoredPetriNetBuilder::computePartition(){
-        auto partitionStart = std::chrono::high_resolution_clock::now();
-        Colored::PartitionBuilder pBuilder = Colored::PartitionBuilder(&_transitions, &_places, &_placePostTransitionMap, &_placePreTransitionMap);
-        pBuilder.partitionNet();
-        //pBuilder.printPartion();
-        _partition = pBuilder.getPartition();
-        pBuilder.assignColorMap(_partition);
-        _partitionComputed = true;
-        auto partitionEnd = std::chrono::high_resolution_clock::now();
-        _partitionTimer = (std::chrono::duration_cast<std::chrono::microseconds>(partitionEnd - partitionStart).count())*0.000001;
-    }
+
       
     void ColoredPetriNetBuilder::computePlaceColorFixpoint(uint32_t maxIntervals, uint32_t maxIntervalsReduced, int32_t timeout) {
         //Start timers for timing color fixpoint creation and max interval reduction steps
@@ -334,7 +339,6 @@
 
     void ColoredPetriNetBuilder::processOutputArcs(Colored::Transition& transition) {
         bool transitionHasVarOutArcs = false;
-
         for (auto& arc : transition.output_arcs) {
             Colored::ColorFixpoint& placeFixpoint = _placeColorFixpoints[arc.place];
             //used to check if colors are added to the place. The total distance between upper and
@@ -351,7 +355,7 @@
 
             //Apply partitioning to unbound outgoing variables such that 
             // bindings are only created for colors used in the rest of the net
-            if(!_partition[arc.place].diagonal){
+            if(_partitionComputed && !_partition[arc.place].diagonal){
                 for(auto outVar : variables){
                     for(auto& varMap : transition.variableMaps){
                         if(varMap.count(outVar) == 0){

=== modified file 'src/PetriEngine/Colored/PartitionBuilder.cpp'
--- src/PetriEngine/Colored/PartitionBuilder.cpp	2021-04-14 10:41:18 +0000
+++ src/PetriEngine/Colored/PartitionBuilder.cpp	2021-04-26 08:36:24 +0000
@@ -22,6 +22,20 @@
             }
         }
 
+        PartitionBuilder::PartitionBuilder(std::vector<Transition> *transitions, std::vector<Place> *places, std::unordered_map<uint32_t,std::vector<uint32_t>> *placePostTransitionMap, std::unordered_map<uint32_t,std::vector<uint32_t>> *placePreTransitionMap, std::vector<Colored::ColorFixpoint> *placeColorFixpoints) 
+        : _transitions(transitions), _places(places), _placePostTransitionMap(placePostTransitionMap), _placePreTransitionMap(placePreTransitionMap) {
+
+            //Instantiate partitions
+            for(uint32_t i = 0; i < _places->size(); i++){
+                auto place = _places->operator[](i);
+                EquivalenceClass fullClass = EquivalenceClass(place.type);
+                fullClass._colorIntervals = placeColorFixpoints->operator[](i).constraints;
+                _partition[i]._equivalenceClasses.push_back(fullClass);
+                _placeQueue.push_back(i);
+                _inQueue[i] = true;
+            }
+        }
+
         void PartitionBuilder::printPartion() {
             for(auto equivalenceVec : _partition){
                 std::cout << "Partition for place " << _places->operator[](equivalenceVec.first).name << std::endl;

=== modified file 'src/PetriParse/PNMLParser.cpp'
--- src/PetriParse/PNMLParser.cpp	2021-04-14 10:41:18 +0000
+++ src/PetriParse/PNMLParser.cpp	2021-04-26 08:36:24 +0000
@@ -154,8 +154,33 @@
                 parseUserSort(it)
             };
             variables[it->first_attribute("id")->value()] = var;
+        } else if (strcmp(it->name(), "partition") == 0) {
+            parsePartitions(it);
         } else {
-            parseDeclarations(element->first_node());
+            parseDeclarations(it);
+        }
+    }
+
+    for(auto missingCTPair : missingCTs){
+        if(colorTypes.count(missingCTPair.first) == 0){
+            std::cerr << "Unable to find colortype " << missingCTPair.first << " used in product type " << missingCTPair.second->getName() << std::endl;
+            exit(ErrorCode);
+        }
+        missingCTPair.second->addType(colorTypes[missingCTPair.first]);
+    }
+    missingCTs.clear();
+}
+
+void PNMLParser::parsePartitions(rapidxml::xml_node<>* element){
+    auto partitionCT = parseUserSort(element);
+    for (auto it = element->first_node(); it; it = it->next_sibling()) {
+        if (strcmp(it->name(), "partitionelement") == 0) {
+            auto id = it->first_attribute("id")->value();
+            std::vector<const PetriEngine::Colored::Color *> colors;
+            for(auto partitionElement = it->first_node(); partitionElement; partitionElement = partitionElement->next_sibling()){
+                colors.push_back(partitionCT->operator[](partitionElement->first_attribute("declaration")->value()));
+            }
+            partitions.push_back({colors, id});
         }
     }
 }
@@ -177,9 +202,16 @@
     if (strcmp(type->name(), "dot") == 0) {
         ct->addDot();
     } else if (strcmp(type->name(), "productsort") == 0) {
+        bool missingType = false;
         for (auto it = type->first_node(); it; it = it->next_sibling()) {
             if (strcmp(it->name(), "usersort") == 0) {
-                ((PetriEngine::Colored::ProductType*)ct)->addType(colorTypes[it->first_attribute("declaration")->value()]);
+                auto ctName = it->first_attribute("declaration")->value();
+                if(!missingType && colorTypes.count(ctName)){
+                    ((PetriEngine::Colored::ProductType*)ct)->addType(colorTypes[ctName]);
+                } else {
+                    missingType = true;
+                    missingCTs.push_back(std::make_pair(ctName, (PetriEngine::Colored::ProductType*)ct));
+                }                
             }
         }
     } else if (strcmp(type->name(), "finiteintrange") == 0) {	
@@ -232,7 +264,6 @@
 		std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> collectedColors;	
 		collectColorsInTuple(element, collectedColors);	
 		auto expr = constructAddExpressionFromTupleExpression(element, collectedColors, 1);	
-		std::cout << expr->toString() << std::endl;	
 		return expr;	
 	}
     printf("Could not parse '%s' as an arc expression\n", element->name());
@@ -280,8 +311,9 @@
 	std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> returnSet;	
 	for(auto set : rightSet){	
 		for(auto expr2 : leftSet){	
-			set.push_back(expr2);	
-			returnSet.push_back(set);	
+            auto setCopy = set;
+			setCopy.push_back(expr2);	
+			returnSet.push_back(std::move(setCopy));	
 		}	
 	}	
 	return returnSet;	
@@ -304,19 +336,43 @@
 			}            	
 		}	
 		collectedColors.push_back(expressionsToAdd);	
-		return;	
+	} else if (strcmp(element->name(), "add") == 0) {
+        std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> intermediateColors;	
+        std::vector<std::vector<PetriEngine::Colored::ColorExpression_ptr>> intermediateColors2;
+        for(auto it = element->first_node(); it; it = it->next_sibling()){
+            collectColorsInTuple(it, intermediateColors2);
+            if(intermediateColors.empty()){
+                intermediateColors = intermediateColors2;
+            } else {
+                for(uint32_t i = 0; i < intermediateColors.size(); i++){
+                    intermediateColors[i].insert(intermediateColors[i].end(), intermediateColors2[i].begin(), intermediateColors2[i].end());
+                }
+            }
+            
+        }
+        for(auto &colorVec : intermediateColors){
+            collectedColors.push_back(std::move(colorVec));
+        }		
 	} else if (strcmp(element->name(), "subterm") == 0 || strcmp(element->name(), "structure") == 0) {	
 		collectColorsInTuple(element->first_node(), collectedColors);	
-	} else if (strcmp(element->name(), "userOperator") == 0 || strcmp(element->name(), "dotconstant") == 0 || strcmp(element->name(), "variable") == 0 	
+	} else if (strcmp(element->name(), "finiteintrangeconstant") == 0){	
+        std::vector<PetriEngine::Colored::ColorExpression_ptr> expressionsToAdd;
+		auto value = element->first_attribute("value")->value();	
+		auto intRangeElement = element->first_node("finiteintrange");	
+		uint32_t start = (uint32_t)atoll(intRangeElement->first_attribute("start")->value());	
+		uint32_t end = (uint32_t)atoll(intRangeElement->first_attribute("end")->value());	
+		expressionsToAdd.push_back(std::make_shared<PetriEngine::Colored::UserOperatorExpression>(findColorForIntRange(value, start,end)));	
+        collectedColors.push_back(expressionsToAdd);
+	} else if (strcmp(element->name(), "useroperator") == 0 || strcmp(element->name(), "dotconstant") == 0 || strcmp(element->name(), "variable") == 0 	
 					|| strcmp(element->name(), "successor") == 0 || strcmp(element->name(), "predecessor") == 0) {	
-		std::vector<PetriEngine::Colored::ColorExpression_ptr> expressionsToAdd;	
-		auto color = parseColorExpression(element);	
-		expressionsToAdd.push_back(color);	
+		std::vector<PetriEngine::Colored::ColorExpression_ptr> expressionsToAdd = findPartitionColors(element);
+        if(expressionsToAdd.empty()){
+            auto color = parseColorExpression(element);	
+            expressionsToAdd.push_back(color);	
+        }
 		collectedColors.push_back(expressionsToAdd);	
-		return;	
 	} else{	
-		printf("Could not parse '%s' as an arc expression\n", element->name());	
-		return;	
+		printf("Could not parse '%s' as an arc expression when collecting tuple colors\n", element->name());	
 	}	
 }	
 	
@@ -563,6 +619,8 @@
             std::unordered_map<const PetriEngine::Colored::Variable*, const PetriEngine::Colored::Color*> binding;
             PetriEngine::Colored::EquivalenceVec placePartition;
 			PetriEngine::Colored::ExpressionContext context {binding, colorTypes, placePartition};
+            for(auto ct : colorTypes){
+            }
             hlinitialMarking = parseArcExpression(it->first_node("structure"))->eval(context);
         } else if (strcmp(it->name(), "type") == 0) {
             type = parseUserSort(it);
@@ -769,6 +827,42 @@
     exit(ErrorCode);
 }
 
+std::vector<PetriEngine::Colored::ColorExpression_ptr> PNMLParser::findPartitionColors(rapidxml::xml_node<>* element) const {
+    std::vector<PetriEngine::Colored::ColorExpression_ptr> colorExpressions;
+    char *name;
+    if (strcmp(element->name(), "useroperator") == 0) {
+         name = element->first_attribute("declaration")->value();
+    } else if (strcmp(element->name(), "successor") == 0) {
+        auto colorExpressionVec = findPartitionColors(element->first_node());
+        for(auto &colorExpression : colorExpressionVec){
+            colorExpressions.push_back(std::make_shared<PetriEngine::Colored::SuccessorExpression>(std::move(colorExpression)));
+        }
+        return colorExpressions;
+    } else if (strcmp(element->name(), "predecessor") == 0) {
+        auto colorExpressionVec = findPartitionColors(element->first_node());
+        for(auto &colorExpression : colorExpressionVec){
+            colorExpressions.push_back(std::make_shared<PetriEngine::Colored::PredecessorExpression>(std::move(colorExpression)));
+        }
+        return colorExpressions;
+    } else if (strcmp(element->name(), "variable") == 0 || strcmp(element->name(), "dotconstant") == 0 || strcmp(element->name(), "finiteintrangeconstant") == 0) {
+        return colorExpressions;
+    } else if (strcmp(element->name(), "subterm") == 0) {
+        return findPartitionColors(element->first_node());
+    } else {
+        printf("Could not find color expression in expression: %s\nCANNOT_COMPUTE\n", element->name());	
+	    exit(ErrorCode);
+    }
+
+    for (auto partition : partitions) {
+        if (strcmp(partition.name.c_str(), name) == 0){
+            for(auto color : partition.colors){
+                colorExpressions.push_back(std::make_shared<PetriEngine::Colored::UserOperatorExpression>(color));
+            }
+        }   
+    }
+    return colorExpressions;
+}
+
 const PetriEngine::Colored::Color* PNMLParser::findColorForIntRange(const char* value, uint32_t start, uint32_t end) const{	
 	for (const auto& elem : colorTypes) {	
 		auto col = (*elem.second)[value];	

=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp	2021-04-16 18:53:36 +0000
+++ src/VerifyPN.cpp	2021-04-26 08:36:24 +0000
@@ -191,6 +191,7 @@
             }
         } else if (strcmp(argv[i], "-e") == 0 || strcmp(argv[i], "--state-space-exploration") == 0) {
             options.statespaceexploration = true;
+            options.computePartition = false;
         } else if (strcmp(argv[i], "-n") == 0 || strcmp(argv[i], "--no-statistics") == 0) {
             options.printstatistics = false;
         } else if (strcmp(argv[i], "-t") == 0 || strcmp(argv[i], "--trace") == 0) {