From 57eb947e089307bca4d384b56345ac52becf491c Mon Sep 17 00:00:00 2001 From: MathiasMehl <33687173+MathiasMehl@users.noreply.github.com> Date: Thu, 7 Apr 2022 11:09:11 +0200 Subject: [PATCH] fixes the case where we have 0 of something in an add expressions (#42) Fixes pnmlwriter, such that it can better handle all-expressions, and find color for places --- include/PetriEngine/AbstractPetriNetBuilder.h | 9 +++ include/PetriEngine/Colored/PnmlWriter.h | 4 +- include/PetriParse/PNMLParser.h | 2 + src/PetriEngine/Colored/PnmlWriter.cpp | 76 +++++++++++-------- src/PetriParse/PNMLParser.cpp | 66 +++++++++++++++- src/main.cpp | 5 ++ 6 files changed, 129 insertions(+), 33 deletions(-) diff --git a/include/PetriEngine/AbstractPetriNetBuilder.h b/include/PetriEngine/AbstractPetriNetBuilder.h index 6ee7bd803..7001217df 100644 --- a/include/PetriEngine/AbstractPetriNetBuilder.h +++ b/include/PetriEngine/AbstractPetriNetBuilder.h @@ -31,6 +31,7 @@ namespace PetriEngine { class AbstractPetriNetBuilder { protected: bool _isColored = false; + bool _hasPartition = false; public: void parse_model(const std::string&& model); @@ -108,6 +109,14 @@ namespace PetriEngine { return _isColored; } + virtual void enablePartition() { + _hasPartition = true; + } + + virtual bool hasPartition() const { + return _hasPartition; + } + virtual void sort() = 0; virtual ~AbstractPetriNetBuilder() { diff --git a/include/PetriEngine/Colored/PnmlWriter.h b/include/PetriEngine/Colored/PnmlWriter.h index 9060a1d82..70b3096bc 100644 --- a/include/PetriEngine/Colored/PnmlWriter.h +++ b/include/PetriEngine/Colored/PnmlWriter.h @@ -85,11 +85,11 @@ namespace PetriEngine::Colored { void handleProducts(std::vector productSorts); - void handleMarking(Multiset multiset); - void handleTuple(const PetriEngine::Colored::Color *const c); void handleOtherColor(const Color *const c); + + void handleNumberOf(std::pair numberOff); }; } diff --git a/include/PetriParse/PNMLParser.h b/include/PetriParse/PNMLParser.h index a4dff1b62..fd7fa1484 100644 --- a/include/PetriParse/PNMLParser.h +++ b/include/PetriParse/PNMLParser.h @@ -112,6 +112,8 @@ class PNMLParser { ColorTypeMap colorTypes; VariableMap variables; bool isColored; + std::string placeTypeContext; + bool hasPartition; std::vector queries; std::vector partitions; std::vector> missingCTs; diff --git a/src/PetriEngine/Colored/PnmlWriter.cpp b/src/PetriEngine/Colored/PnmlWriter.cpp index a832362a5..d04dc7eb0 100644 --- a/src/PetriEngine/Colored/PnmlWriter.cpp +++ b/src/PetriEngine/Colored/PnmlWriter.cpp @@ -9,6 +9,7 @@ namespace PetriEngine { namespace Colored { void PnmlWriter::toColPNML() { + //TODO cannot handle nets with partitions metaInfo(); declarations(); page(); @@ -47,7 +48,6 @@ namespace PetriEngine { std::vector types; colortype->getColortypes(types); if (types.size() > 1 && colortype->productSize() == 1) { - std::cout << colortype->getName(); throw base_error("types.size was over 1"); } if (colortype->productSize() > 1) { @@ -202,42 +202,58 @@ namespace PetriEngine { _out << getTabs() << "\n"; _out << increaseTabs() << "" << marking.toString() << "\n"; _out << getTabs() << "\n"; - _out << increaseTabs() << "\n"; - handleMarking(marking); - _out << decreaseTabs() << "\n"; + + if (marking.size() > 1) { + bool first = true; + _out << increaseTabs() << "\n"; + + for (const auto &p: marking) { + if (p.second == 0) { + continue; + } + if (first) { + _out << increaseTabs() << "\n"; + } else { + _out << getTabs() << "\n"; + } + handleNumberOf(p); + _out << decreaseTabs() << "\n"; + first = false; + } + _out << decreaseTabs() << "\n"; + } else { + for (const auto &p: marking) { + if (p.second == 0) { + continue; + } + handleNumberOf(p); + } + } + _out << decreaseTabs() << "\n"; _out << decreaseTabs() << "\n"; } - void PnmlWriter::handleMarking(Multiset marking) { - bool first = true; - for (const auto &p: marking) { - const auto &c = p.first; - const auto &m = p.second; - if (first) { - _out << increaseTabs() << "\n"; - } else { - _out << getTabs() << "\n"; - } - _out << increaseTabs() << "\n"; - _out << increaseTabs() << "" << "\n"; - _out << increaseTabs() << "\n"; - _out << increaseTabs() << "\n"; - _out << decreaseTabs() << "\n"; + void PnmlWriter::handleNumberOf(std::pair numberOff) { + const auto &c = numberOff.first; + const auto &m = numberOff.second; + + _out << increaseTabs() << "\n"; + _out << increaseTabs() << "" << "\n"; + _out << increaseTabs() << "\n"; + _out << increaseTabs() << "\n"; + _out << decreaseTabs() << "\n"; + _out << decreaseTabs() << "" << "\n"; + if (c->isTuple()) { + _out << getTabs() << "" << "\n"; + handleTuple(c); _out << decreaseTabs() << "" << "\n"; - if (c->isTuple()) { - _out << getTabs() << "" << "\n"; - handleTuple(c); - _out << decreaseTabs() << "" << "\n"; - } else { - _out << getTabs() << "\n"; - handleOtherColor(c); - _out << decreaseTabs() << "\n"; - } - _out << decreaseTabs() << "\n"; + } else { + _out << getTabs() << "\n"; + handleOtherColor(c); _out << decreaseTabs() << "\n"; - first = false; } + _out << decreaseTabs() << "\n"; } void PnmlWriter::handleTuple(const PetriEngine::Colored::Color *const c) { diff --git a/src/PetriParse/PNMLParser.cpp b/src/PetriParse/PNMLParser.cpp index bf7a0bf55..31c1d70cb 100644 --- a/src/PetriParse/PNMLParser.cpp +++ b/src/PetriParse/PNMLParser.cpp @@ -41,6 +41,8 @@ void PNMLParser::parse(std::istream& xml, arcs.clear(); _transitions.clear(); colorTypes.clear(); + placeTypeContext = ""; + hasPartition = false; //Set the builder this->builder = builder; @@ -144,6 +146,8 @@ void PNMLParser::parseDeclarations(rapidxml::xml_node<>* element) { variables[it->first_attribute("id")->value()] = var; builder->addVariable(var); } else if (strcmp(it->name(), "partition") == 0) { + builder->enablePartition(); + hasPartition = true; parsePartitions(it); } else { parseDeclarations(it); @@ -620,6 +624,8 @@ void PNMLParser::parsePlace(rapidxml::xml_node<>* element) { hlinitialMarking = PetriEngine::Colored::EvaluationVisitor::evaluate(*ae, context); } else if (strcmp(it->name(), "type") == 0) { type = parseUserSort(it); + placeTypeContext = type->getName(); + } } @@ -644,6 +650,7 @@ void PNMLParser::parsePlace(rapidxml::xml_node<>* element) { nn.id = id; nn.isPlace = true; id2name[id] = nn; + placeTypeContext = ""; } void PNMLParser::parseArc(rapidxml::xml_node<>* element, bool inhibitor) { @@ -814,7 +821,34 @@ void PNMLParser::parsePosition(rapidxml::xml_node<>* element, double& x, double& } const PetriEngine::Colored::Color* PNMLParser::findColor(const char* name) const { + bool placeTypeIsTuple = false; + if (!hasPartition && !placeTypeContext.empty()) { + auto &placeColorType = colorTypes.find(placeTypeContext)->second; + placeTypeIsTuple = placeColorType->productSize() > 1; + } + for (const auto& elem : colorTypes) { + if (!hasPartition && !placeTypeContext.empty()) { + //If we are finding color for a place, and the type of place is tuple + if (placeTypeIsTuple) { + auto &placeColorType = colorTypes.find(placeTypeContext)->second; + const auto *pt = dynamic_cast (placeColorType); + //go through all colotypes in the tuple + for (uint32_t i = 0; i < placeColorType->productSize(); i++) { + const auto &nestedColorType = pt->getNestedColorType(i); + if (nestedColorType->productSize() > 1) { + throw base_error("Nested products when finding colors: ", nestedColorType->getName()); + } + auto col = (*nestedColorType)[name]; + if (col) { + return col; + } + } + //type of place is not a tuple + } else if (elem.first != placeTypeContext) { + continue; + } + } auto col = (*elem.second)[name]; if (col) return col; @@ -846,11 +880,12 @@ std::vector PNMLParser::findPartition } else { throw base_error("Could not find color expression in expression: ", element->name(), "\nCANNOT_COMPUTE\n"); } - for (auto partition : partitions) { if (strcmp(partition.name.c_str(), name) == 0){ for(auto color : partition.colors){ + colorExpressions.push_back(std::make_shared(color)); + } } } @@ -858,7 +893,36 @@ std::vector PNMLParser::findPartition } const PetriEngine::Colored::Color* PNMLParser::findColorForIntRange(const char* value, uint32_t start, uint32_t end) const{ + bool placeTypeIsTuple = false; + if (!hasPartition && !placeTypeContext.empty()) { + auto &placeColorType = colorTypes.find(placeTypeContext)->second; + placeTypeIsTuple = placeColorType->productSize() > 1; + } + + for (const auto& elem : colorTypes) { + if (!hasPartition && !placeTypeContext.empty()) { + if (placeTypeIsTuple) { + auto &placeColorType = colorTypes.find(placeTypeContext)->second; + const auto *pt = dynamic_cast (placeColorType); + //go through all colotypes in the tuple + for (uint32_t i = 0; i < placeColorType->productSize(); i++) { + const auto &nestedColorType = pt->getNestedColorType(i); + if (nestedColorType->productSize() > 1) { + throw base_error("Nested products when finding colors: ", nestedColorType->getName()); + } + auto col = (*nestedColorType)[value]; + if (col) { + if ((*nestedColorType).operator[](0).getId() == (start - 1) && + (*elem.second).operator[]((*elem.second).size() - 1).getId() == end - 1) + return col; + } + } + //type of place is not a tuple + } else if (elem.first != placeTypeContext) { + continue; + } + } auto col = (*elem.second)[value]; if (col){ if((*elem.second).operator[](0).getId() == (start -1) && (*elem.second).operator[]((*elem.second).size()-1).getId() == end -1) diff --git a/src/main.cpp b/src/main.cpp index 341d08841..bd1eb65de 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -76,6 +76,11 @@ int main(int argc, const char** argv) { throw base_error("CANNOT_COMPUTE\nError parsing the model\n", err.what()); } + if (!options.model_col_out_file.empty() && cpnBuilder.hasPartition()) { + std::cerr << "Cannot write colored PNML as the original net has partitions. Not supported (yet)" << std::endl; + return to_underlying(ReturnValue::UnknownCode); + } + if (options.cpnOverApprox && !cpnBuilder.isColored()) { std::cerr << "CPN OverApproximation is only usable on colored models" << std::endl; return to_underlying(ReturnValue::UnknownCode);