From c9d961c479de55989506589c43a73cbff2c7e230 Mon Sep 17 00:00:00 2001 From: ThomasH Date: Wed, 21 Sep 2016 21:32:02 +0200 Subject: [PATCH 1/7] fix bug in argument parser Former-commit-id: 6e6b56c7498e545d7b595155d1fe02d959ca9fa0 --- src/storm-gspn.cpp | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/storm-gspn.cpp b/src/storm-gspn.cpp index 40802218e..1f0240b0e 100644 --- a/src/storm-gspn.cpp +++ b/src/storm-gspn.cpp @@ -34,10 +34,10 @@ bool parseArguments(const int argc, const char **argv, std::string &inputFile, s if (currentArg == "--input_file" || currentArg == "-i") { auto next = it + 1; if (next != end) { - return -1; - } else { inputFile = *next; result = true; + } else { + return -1; } break; } @@ -46,9 +46,9 @@ bool parseArguments(const int argc, const char **argv, std::string &inputFile, s if (currentArg == "--formula" || currentArg == "-f") { auto next = it + 1; if (next != end) { - return -1; - } else { formula = *next; + } else { + return -1; } break; } @@ -57,9 +57,9 @@ bool parseArguments(const int argc, const char **argv, std::string &inputFile, s if (currentArg == "--output_file" || currentArg == "-o") { auto next = it + 1; if (next != end) { - return -1; - } else { outputFile = *next; + } else { + return -1; } break; } @@ -68,9 +68,9 @@ bool parseArguments(const int argc, const char **argv, std::string &inputFile, s if (currentArg == "--output_type" || currentArg == "-ot") { auto next = it + 1; if (next != end) { - return -1; - } else { outputType = *next; + } else { + return -1; } break; } @@ -109,11 +109,12 @@ int main(const int argc, const char **argv) { // parse GSPN from file auto parser = storm::parser::GspnParser(); + std::cout << "input_file: " << inputFile << std::endl; auto gspn = parser.parse(inputFile); // todo ------[marker] - gspn.isValid(); - + std::cout << "valid? = " << gspn.isValid() << std::endl; + /* storm::gspn::GspnBuilder builder2; builder2.addPlace(2); @@ -138,7 +139,7 @@ int main(const int argc, const char **argv) { std::cout << "number of states: " << ma.getNumberOfStates() << std::endl; std::cout << "number of transitions: " << ma.getNumberOfTransitions() << std::endl << std::endl; - + */ From 3a63d2d3b21e586afecf74cd3b98d62fa518dcab Mon Sep 17 00:00:00 2001 From: ThomasH Date: Wed, 21 Sep 2016 21:32:32 +0200 Subject: [PATCH 2/7] add pnpro example Former-commit-id: 914058a7111dccbd1dc06969a4fac7b6f7f59dc6 --- examples/gspn/pnpro_test1/project01.PNPRO | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 examples/gspn/pnpro_test1/project01.PNPRO diff --git a/examples/gspn/pnpro_test1/project01.PNPRO b/examples/gspn/pnpro_test1/project01.PNPRO new file mode 100644 index 000000000..3648b6e96 --- /dev/null +++ b/examples/gspn/pnpro_test1/project01.PNPRO @@ -0,0 +1,20 @@ + + + + + + + + + + + + + + + + + + + + From dc8382bad54f99c1e7ce83f70defedc20cc2080e Mon Sep 17 00:00:00 2001 From: ThomasH Date: Wed, 21 Sep 2016 23:40:44 +0200 Subject: [PATCH 3/7] add parser for pnpro files Former-commit-id: 5b43a19ba5c4ccaaf3cea98f63736322deb9e077 --- src/parser/GspnParser.cpp | 321 +++++++++++++++++++++++++++++++++++++- src/parser/GspnParser.h | 12 ++ src/storm-gspn.cpp | 1 - 3 files changed, 330 insertions(+), 4 deletions(-) diff --git a/src/parser/GspnParser.cpp b/src/parser/GspnParser.cpp index 82d1bcf98..27000bab6 100644 --- a/src/parser/GspnParser.cpp +++ b/src/parser/GspnParser.cpp @@ -64,9 +64,19 @@ namespace storm { // build gspn by traversing the DOM object parser->getDocument()->normalizeDocument(); xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement(); - // If the top-level node is not a "pnml" node, then throw an exception. - STORM_LOG_THROW(getName(elementRoot).compare("pnml") == 0, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n"); - traversePnmlElement(elementRoot); + + if (getName(elementRoot).compare("pnml") == 0) { + traversePnmlElement(elementRoot); + } else if (getName(elementRoot).compare("project") == 0) { + traverseProjectElement(elementRoot); + } else { + // If the top-level node is not a "pnml" or "" node, then throw an exception. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n"); + } + + + + // clean up delete parser; @@ -568,6 +578,311 @@ namespace storm { delete tmp; return result; } + + void GspnParser::traverseProjectElement(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + + if (name.compare("version") == 0 || + name.compare("name") == 0) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + + if (name.compare("gspn") == 0) { + traverseGspnElement(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + void GspnParser::traverseGspnElement(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + + if (name.compare("name") == 0) { + gspn.setName(XMLtoString(attr->getNodeValue())); + } else if (name.compare("show-color-cmd") == 0 || + name.compare("show-fluid-cmd") == 0) { + // ignore node + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG( + "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + + if (name.compare("nodes") == 0) { + traverseNodesElement(child); + } else if (name.compare("edges") == 0) { + traverseEdgesElement(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + void GspnParser::traverseNodesElement(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + + if (name.compare("place") == 0) { + traversePlaceElement(child); + } else if(name.compare("transition") == 0) { + traverseTransitionElement(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + void GspnParser::traverseEdgesElement(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + + + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + + if (name.compare("arc") == 0) { + traverseArcElement(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + void GspnParser::traversePlaceElement(xercesc::DOMNode const* const node) { + storm::gspn::Place place; + place.setID(newNode); + ++newNode; + + + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + + if (name.compare("name") == 0) { + place.setName(XMLtoString(attr->getNodeValue())); + } else if (name.compare("marking") == 0) { + place.setNumberOfInitialTokens(std::stoull(XMLtoString(attr->getNodeValue()))); + } else if (name.compare("x") == 0 || + name.compare("y") == 0) { + // ignore node + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG( + "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + + if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + gspn.addPlace(place); + } + + void GspnParser::traverseTransitionElement(xercesc::DOMNode const* const node) { + std::string transitionName; + bool immediateTransition; + double rate; + + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + + if (name.compare("name") == 0) { + transitionName = XMLtoString(attr->getNodeValue()); + } else if (name.compare("type") == 0) { + if (XMLtoString(attr->getNodeValue()).compare("EXP") == 0) { + immediateTransition = false; + } else { + immediateTransition = true; + } + } else if(name.compare("nservers-x") == 0) { + rate = std::stod(XMLtoString(attr->getNodeValue())); + } else if (name.compare("x") == 0 || + name.compare("y") == 0) { + // ignore node + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG( + "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + if (immediateTransition) { + auto transition = storm::gspn::ImmediateTransition(); + transition.setName(transitionName); + gspn.addImmediateTransition(transition); + } else { + auto transition = storm::gspn::TimedTransition(); + transition.setName(transitionName); + transition.setRate(rate); + gspn.addTimedTransition(transition); + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + + if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + void GspnParser::traverseArcElement(xercesc::DOMNode const* const node) { + std::string head, tail, kind; + uint_fast64_t mult = 1; + + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + + if (name.compare("head") == 0) { + head = XMLtoString(attr->getNodeValue()); + } else if (name.compare("tail") == 0) { + tail = XMLtoString(attr->getNodeValue()); + } else if (name.compare("kind") == 0) { + kind = XMLtoString(attr->getNodeValue()); + } else if (name.compare("mult") == 0) { + mult = std::stoull(XMLtoString(attr->getNodeValue())); + } else if (name.compare("mult-x") == 0 || + name.compare("mult-y") == 0 || + name.compare("mult-k") == 0) { + // ignore node + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG( + "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + if (kind.compare("INPUT") == 0) { + auto transition = gspn.getTransition(head); + if (!transition.first) { + std::cout << "transition not found" << std::endl; + } + auto place = gspn.getPlace(tail); + if (!place.first) { + std::cout << "place not found" << std::endl; + } + transition.second->setInputArcMultiplicity(place.second, mult); + } else if (kind.compare("INHIBITOR") == 0) { + auto transition = gspn.getTransition(head); + auto place = gspn.getPlace(tail); + transition.second->setInhibitionArcMultiplicity(place.second, mult); + } else if (kind.compare("OUTPUT") == 0) { + auto transition = gspn.getTransition(tail); + auto place = gspn.getPlace(head); + transition.second->setOutputArcMultiplicity(place.second, mult); + } else { + // TODO error! + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + + if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + + + + + + + } } diff --git a/src/parser/GspnParser.h b/src/parser/GspnParser.h index 920a99b9f..81b28c40d 100644 --- a/src/parser/GspnParser.h +++ b/src/parser/GspnParser.h @@ -132,6 +132,18 @@ namespace storm { */ static std::string XMLtoString(const XMLCh* xmlString); + + void traverseProjectElement(xercesc::DOMNode const* const node); + + void traverseGspnElement(xercesc::DOMNode const* const node); + void traverseNodesElement(xercesc::DOMNode const* const node); + void traverseEdgesElement(xercesc::DOMNode const* const node); + + void traversePlaceElement(xercesc::DOMNode const* const node); + void traverseTransitionElement(xercesc::DOMNode const* const node); + void traverseArcElement(xercesc::DOMNode const* const node); + + // the constructed gspn storm::gspn::GSPN gspn; diff --git a/src/storm-gspn.cpp b/src/storm-gspn.cpp index 1f0240b0e..83230b785 100644 --- a/src/storm-gspn.cpp +++ b/src/storm-gspn.cpp @@ -109,7 +109,6 @@ int main(const int argc, const char **argv) { // parse GSPN from file auto parser = storm::parser::GspnParser(); - std::cout << "input_file: " << inputFile << std::endl; auto gspn = parser.parse(inputFile); // todo ------[marker] From c5bbceebdaa5473bf7a1ae4a60f68c1a9419e548 Mon Sep 17 00:00:00 2001 From: ThomasH Date: Mon, 26 Sep 2016 12:30:34 +0200 Subject: [PATCH 4/7] fix project file Former-commit-id: 881bc6905618c88c57ee110cc2f119414607fd62 --- examples/gspn/pnpro_test1/project01.PNPRO | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/examples/gspn/pnpro_test1/project01.PNPRO b/examples/gspn/pnpro_test1/project01.PNPRO index 3648b6e96..d5c530dd6 100644 --- a/examples/gspn/pnpro_test1/project01.PNPRO +++ b/examples/gspn/pnpro_test1/project01.PNPRO @@ -2,19 +2,13 @@ - - - - - + + + - - - - - - + + From ba50772eebfbac639d4eafeb8a47c3053ca22db1 Mon Sep 17 00:00:00 2001 From: ThomasH Date: Mon, 26 Sep 2016 12:30:59 +0200 Subject: [PATCH 5/7] fix more bugs with argument parser Former-commit-id: a271ef25f45e453aa252cb99dd52a233e0300ca4 --- src/storm-gspn.cpp | 87 ++++++++++++++++++++++------------------------ 1 file changed, 41 insertions(+), 46 deletions(-) diff --git a/src/storm-gspn.cpp b/src/storm-gspn.cpp index 83230b785..d24f0d59b 100644 --- a/src/storm-gspn.cpp +++ b/src/storm-gspn.cpp @@ -8,71 +8,70 @@ #include #include #include -// TODO clean-up includes after doing all other todos + /*! * Parses the arguments to storm-gspn * The read data is stored in the different arguments (e.g., inputFile, formula, ...) * - * @param argc number of arguments passed to storm-gspn - * @param argv array of arguments + * @param begin pointer to the first argument passed to storm-gspn + * @param end pointer to one past the last argument passed to storm-gspn * @param inputFile the input file is stored in this object * @param formula the formula is stored in this object * @param outputFile the output file is stored in this object * @param outputType the output type is stored in this object * @return false if the help flag is set or the input file is missing */ -bool parseArguments(const int argc, const char **argv, std::string &inputFile, std::string &formula, +bool parseArguments(const char **begin, const char **end, std::string &inputFile, std::string &formula, std::string &outputFile, std::string &outputType) { - auto end = argv + argc; bool result = false; - for (auto it = argv; it != end; ++it) { - std::string currentArg = *it; + for (; begin != end; ++begin) { + std::string currentArg = *begin; // parse input file argument if (currentArg == "--input_file" || currentArg == "-i") { - auto next = it + 1; + auto next = begin + 1; if (next != end) { inputFile = *next; result = true; } else { return -1; } - break; + continue; } // parse formula argument if (currentArg == "--formula" || currentArg == "-f") { - auto next = it + 1; + auto next = begin + 1; if (next != end) { formula = *next; } else { return -1; } - break; + continue; } // parse output file argument if (currentArg == "--output_file" || currentArg == "-o") { - auto next = it + 1; + auto next = begin + 1; if (next != end) { outputFile = *next; } else { return -1; } - break; + continue; } // parse output file type argument if (currentArg == "--output_type" || currentArg == "-ot") { - auto next = it + 1; + auto next = begin + 1; if (next != end) { outputType = *next; } else { return -1; } - break; + continue; } // parse help argument @@ -94,12 +93,12 @@ void printHelp() { std::cout << "-f, --formula: formula which should be checked on the gspn" << std::endl; std::cout << "-o, -output_file: file in which the gspn/markov automaton should be stored" << std::endl << " requires the option -ot to be set" << std::endl; - std::cout << "-ot, --output_type: possible output types are: pnml, pnpro or ma" << std::endl; + std::cout << "-ot, --output_type: possible output types are: pnml, pnpro, dot or ma" << std::endl; } int main(const int argc, const char **argv) { std::string inputFile, formula, outputFile, outputType; - if (!parseArguments(argc, argv, inputFile, formula, outputFile, outputType)) { + if (!parseArguments(argv+1, argv+argc, inputFile, formula, outputFile, outputType)) { printHelp(); return 1; } @@ -107,40 +106,36 @@ int main(const int argc, const char **argv) { try { storm::utility::setUp(); - // parse GSPN from file + // parse gspn from file auto parser = storm::parser::GspnParser(); auto gspn = parser.parse(inputFile); - // todo ------[marker] - std::cout << "valid? = " << gspn.isValid() << std::endl; - /* - storm::gspn::GspnBuilder builder2; - builder2.addPlace(2); - - // - //std::ofstream file; - //file.open("/Users/thomas/Desktop/storm.dot"); - //gspn.writeDotToStream(file); - //file.close(); - - std::ofstream file; - file.open("/Users/thomas/Desktop/gspn.pnpro"); - gspn.toPnpro(file); - file.close(); - - std::cout << "Parsing complete!" << std::endl; - + if (!gspn.isValid()) { + STORM_LOG_ERROR("The gspn is not valid."); + } - // Construct MA + // construct ma auto builder = storm::builder::ExplicitGspnModelBuilder<>(); - auto ma = builder.translateGspn(gspn, argv[2]); - std::cout << "Markov Automaton: " << std::endl; - std::cout << "number of states: " << ma.getNumberOfStates() << std::endl; - std::cout << "number of transitions: " << ma.getNumberOfTransitions() << std::endl << std::endl; - - */ - - + auto ma = builder.translateGspn(gspn, formula); + + // write gspn into output file + if (!outputFile.empty()) { + std::ofstream file; + file.open(outputFile); + if (outputType == "pnml") { + gspn.toPnml(file); + } + if (outputType == "pnpro") { + gspn.toPnpro(file); + } + if (outputType == "dot") { + gspn.writeDotToStream(file); + } + if (outputType == "ma") { + ma.writeDotToStream(file); + } + file.close(); + } // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp(); From bd057da74310a4e32bacab940be48282a044f388 Mon Sep 17 00:00:00 2001 From: ThomasH Date: Mon, 26 Sep 2016 12:31:29 +0200 Subject: [PATCH 6/7] refactoring gspn Former-commit-id: c7c4764901cb47d859c07511f7ea4d694ec51790 --- src/storage/gspn/GSPN.cpp | 153 +++++++++++++++----------------- src/storage/gspn/Place.cpp | 2 +- src/storage/gspn/Place.h | 10 ++- src/storage/gspn/Transition.cpp | 69 ++++++-------- src/storage/gspn/Transition.h | 58 ++++-------- 5 files changed, 121 insertions(+), 171 deletions(-) diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index b3d23a9ff..b63fa0e39 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -100,56 +100,43 @@ namespace storm { // print arcs for (auto& trans : this->getImmediateTransitions()) { - auto it = trans->getInputPlacesCBegin(); - while (it != trans->getInputPlacesCEnd()) { - outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"normal:" << - trans->getInputArcMultiplicity(**it); - outStream << "\"];" << std::endl; - ++it; + for (auto &placePtr : trans->getInputPlaces()) { + outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"normal:" << + trans->getInputArcMultiplicity(*placePtr); + outStream << "\"];" << std::endl; } - it = trans->getInhibitionPlacesCBegin(); - while (it != trans->getInhibitionPlacesCEnd()) { - outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" << - trans->getInhibitionArcMultiplicity(**it); + for (auto &placePtr : trans->getInhibitionPlaces()) { + outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"inhibition:" << + trans->getInhibitionArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; - ++it; } - it = trans->getOutputPlacesCBegin(); - while (it != trans->getOutputPlacesCEnd()) { - outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" << - trans->getOutputArcMultiplicity(**it); + for (auto &placePtr : trans->getOutputPlaces()) { + outStream << "\t" << trans->getName() << " -> " << placePtr->getName() << "[label=\"" << + trans->getOutputArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; - ++it; } } for (auto& trans : this->getTimedTransitions()) { - auto it = trans->getInputPlacesCBegin(); - while (it != trans->getInputPlacesCEnd()) { - outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"normal:" << - trans->getInputArcMultiplicity(**it); + for (auto &placePtr : trans->getInputPlaces()) { + outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"normal:" << + trans->getInputArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; - ++it; } - - it = trans->getInhibitionPlacesCBegin(); - while (it != trans->getInhibitionPlacesCEnd()) { - outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" << - trans->getInhibitionArcMultiplicity(**it); + for (auto &placePtr : trans->getInhibitionPlaces()) { + outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"inhibition:" << + trans->getInhibitionArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; - ++it; } - it = trans->getOutputPlacesCBegin(); - while (it != trans->getOutputPlacesCEnd()) { - outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" << - trans->getOutputArcMultiplicity(**it); + for (auto &placePtr : trans->getOutputPlaces()) { + outStream << "\t" << trans->getName() << " -> " << placePtr->getName() << "[label=\"" << + trans->getOutputArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; - ++it; } } @@ -202,26 +189,26 @@ namespace storm { bool result = true; for (auto const& transition : this->getImmediateTransitions()) { - if (transition->getInputPlacesCBegin() == transition->getInputPlacesCEnd() && - transition->getInhibitionPlacesCBegin() == transition->getInhibitionPlacesCEnd()) { + if (transition->getInputPlaces().empty() && + transition->getInhibitionPlaces().empty()) { STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n") result = false; } - if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) { + if (transition->getOutputPlaces().empty()) { STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n") result = false; } } for (auto const& transition : this->getTimedTransitions()) { - if (transition->getInputPlacesCBegin() == transition->getInputPlacesCEnd() && - transition->getInhibitionPlacesCBegin() == transition->getInhibitionPlacesCEnd()) { + if (transition->getInputPlaces().empty() && + transition->getInputPlaces().empty()) { STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n") result = false; } - if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) { + if (transition->getOutputPlaces().empty()) { STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n") result = false; } @@ -229,82 +216,82 @@ namespace storm { //test if places exists in the gspn for (auto const& transition : this->getImmediateTransitions()) { - for (auto it = transition->getInputPlacesCBegin(); it != transition->getInputPlacesCEnd(); ++it) { + for (auto &placePtr : transition->getInputPlaces()) { bool foundPlace = false; for (auto const& place : places) { - if (place.getName() == (*it)->getName()) { + if (place.getName() == placePtr->getName()) { foundPlace = true; } } if (!foundPlace) { - STORM_PRINT_AND_LOG("input place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") result = false; } } - for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) { + for (auto &placePtr : transition->getInhibitionPlaces()) { bool foundPlace = false; for (auto const& place : places) { - if (place.getName() == (*it)->getName()) { + if (place.getName() == placePtr->getName()) { foundPlace = true; } } if (!foundPlace) { - STORM_PRINT_AND_LOG("inhibition place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") result = false; } } - for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) { + for (auto &placePtr : transition->getOutputPlaces()) { bool foundPlace = false; for (auto const& place : places) { - if (place.getName() == (*it)->getName()) { + if (place.getName() == placePtr->getName()) { foundPlace = true; } } if (!foundPlace) { - STORM_PRINT_AND_LOG("output place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") result = false; } } } for (auto const& transition : this->getTimedTransitions()) { - for (auto it = transition->getInputPlacesCBegin(); it != transition->getInputPlacesCEnd(); ++it) { + for (auto &placePtr : transition->getInputPlaces()) { bool foundPlace = false; for (auto const& place : places) { - if (place.getName() == (*it)->getName()) { + if (place.getName() == placePtr->getName()) { foundPlace = true; } } if (!foundPlace) { - STORM_PRINT_AND_LOG("input place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") result = false; } } - for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) { + for (auto &placePtr : transition->getInhibitionPlaces()) { bool foundPlace = false; for (auto const& place : places) { - if (place.getName() == (*it)->getName()) { + if (place.getName() == placePtr->getName()) { foundPlace = true; } } if (!foundPlace) { - STORM_PRINT_AND_LOG("inhibition place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") result = false; } } - for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) { + for (auto &placePtr : transition->getOutputPlaces()) { bool foundPlace = false; for (auto const& place : places) { - if (place.getName() == (*it)->getName()) { + if (place.getName() == placePtr->getName()) { foundPlace = true; } } if (!foundPlace) { - STORM_PRINT_AND_LOG("output place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") result = false; } } @@ -354,54 +341,54 @@ namespace storm { stream << space2 << "" << std::endl; for (auto& trans : timedTransitions) { - for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) { + for (auto &placePtr : trans->getInputPlaces()) { stream << space3 << "getName() << "\" "; - stream << "tail=\"" << (*it)->getName() << "\" "; + stream << "tail=\"" << placePtr->getName() << "\" "; stream << "kind=\"INPUT\" "; - stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" "; + stream << "mult=\"" << trans->getInputArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } - for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) { + for (auto &placePtr : trans->getInhibitionPlaces()) { stream << space3 << "getName() << "\" "; - stream << "tail=\"" << (*it)->getName() << "\" "; + stream << "tail=\"" << placePtr->getName() << "\" "; stream << "kind=\"INHIBITOR\" "; - stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" "; + stream << "mult=\"" << trans->getInhibitionArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } - for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) { + for (auto &placePtr : trans->getOutputPlaces()) { stream << space3 << "getName() << "\" "; + stream << "head=\"" << placePtr->getName() << "\" "; stream << "tail=\"" << trans->getName() << "\" "; stream << "kind=\"OUTPUT\" "; - stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" "; + stream << "mult=\"" << trans->getOutputArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } } for (auto& trans : immediateTransitions) { - for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) { + for (auto &placePtr : trans->getInputPlaces()) { stream << space3 << "getName() << "\" "; - stream << "tail=\"" << (*it)->getName() << "\" "; + stream << "tail=\"" << placePtr->getName() << "\" "; stream << "kind=\"INPUT\" "; - stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" "; + stream << "mult=\"" << trans->getInputArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } - for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) { + for (auto &placePtr : trans->getInhibitionPlaces()) { stream << space3 << "getName() << "\" "; - stream << "tail=\"" << (*it)->getName() << "\" "; + stream << "tail=\"" << placePtr->getName() << "\" "; stream << "kind=\"INHIBITOR\" "; - stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" "; + stream << "mult=\"" << trans->getInhibitionArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } - for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) { + for (auto &placePtr : trans->getOutputPlaces()) { stream << space3 << "getName() << "\" "; + stream << "head=\"" << placePtr->getName() << "\" "; stream << "tail=\"" << trans->getName() << "\" "; stream << "kind=\"OUTPUT\" "; - stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" "; + stream << "mult=\"" << trans->getOutputArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } } @@ -456,15 +443,15 @@ namespace storm { // add arcs for immediate transitions for (const auto &trans : immediateTransitions) { // add input arcs - for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) { + for (auto &placePtr : trans->getInputPlaces()) { stream << space2 << "getName() << "\" "; + stream << "source=\"" << placePtr->getName() << "\" "; stream << "target=\"" << trans->getName() << "\" "; stream << ">" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "Default," << trans->getInputArcMultiplicity(**it) << "" << std::endl; + stream << space4 << "Default," << trans->getInputArcMultiplicity(*placePtr) << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; @@ -473,15 +460,15 @@ namespace storm { } // add inhibition arcs - for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) { + for (auto &placePtr : trans->getInhibitionPlaces()) { stream << space2 << "getName() << "\" "; + stream << "source=\"" << placePtr->getName() << "\" "; stream << "target=\"" << trans->getName() << "\" "; stream << ">" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "Default," << trans->getInputArcMultiplicity(**it) << "" << std::endl; + stream << space4 << "Default," << trans->getInputArcMultiplicity(*placePtr) << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; @@ -490,15 +477,15 @@ namespace storm { } // add output arcs - for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) { + for (auto &placePtr : trans->getOutputPlaces()) { stream << space2 << "getName() << "\" "; - stream << "target=\"" << (*it)->getName() << "\" "; + stream << "target=\"" << placePtr->getName() << "\" "; stream << ">" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "Default," << trans->getInputArcMultiplicity(**it) << "" << std::endl; + stream << space4 << "Default," << trans->getInputArcMultiplicity(*placePtr) << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; diff --git a/src/storage/gspn/Place.cpp b/src/storage/gspn/Place.cpp index 443766bf0..430acb9c9 100644 --- a/src/storage/gspn/Place.cpp +++ b/src/storage/gspn/Place.cpp @@ -30,7 +30,7 @@ namespace storm { } void Place::setCapacity(int_fast64_t const& capacity) { - STORM_LOG_THROW(capacity >= -1, storm::exceptions::IllegalArgumentValueException, "The capacity cannot be less than -1."); + STORM_LOG_THROW(capacity <= -1, storm::exceptions::IllegalArgumentValueException, "The capacity cannot be less than -1."); this->capacity = capacity; } diff --git a/src/storage/gspn/Place.h b/src/storage/gspn/Place.h index f7182f7c7..09b52ef57 100644 --- a/src/storage/gspn/Place.h +++ b/src/storage/gspn/Place.h @@ -11,7 +11,9 @@ namespace storm { class Place { public: /*! - * Sets the name of this place. The name must be unique for a gspn. + * Sets the name of this place. The name is not used to identify a place (and therefore do not have to be unique). + * Some input and output formats use the name to identify a place. If you want to use the export or import + * features make sure that the names a unique if necessary. * * @param name The new name for the place. */ @@ -68,10 +70,10 @@ namespace storm { int_fast64_t getCapacity() const; private: // contains the number of initial tokens of this place - uint_fast64_t numberOfInitialTokens; + uint_fast64_t numberOfInitialTokens = 0; // unique id (is used to refer to a specific place in a bitvector) - uint_fast64_t id; + uint_fast64_t id = 0; // name which is used in pnml file std::string name; @@ -79,7 +81,7 @@ namespace storm { // capacity of this place // -1 indicates that the capacity is not set // other non-negative values represents the capacity - int_fast64_t capacity; + int_fast64_t capacity = -1; }; } } diff --git a/src/storage/gspn/Transition.cpp b/src/storage/gspn/Transition.cpp index a94e222d8..a90e70c50 100644 --- a/src/storage/gspn/Transition.cpp +++ b/src/storage/gspn/Transition.cpp @@ -7,14 +7,14 @@ namespace storm { void Transition::setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) { auto ptr = std::make_shared(place); - inputMultiplicities[ptr] = multiplicity; + inputMultiplicities[ptr->getID()] = multiplicity; inputPlaces.push_back(ptr); } bool Transition::removeInputArc(storm::gspn::Place const& place) { if (existsInputArc(place)) { auto ptr = std::make_shared(place); - inputMultiplicities.erase(ptr); + inputMultiplicities.erase(ptr->getID()); inputPlaces.erase(std::find(inputPlaces.begin(), inputPlaces.end(), ptr)); return true; } else { @@ -24,19 +24,19 @@ namespace storm { bool Transition::existsInputArc(storm::gspn::Place const& place) const { auto ptr = std::make_shared(place); - return inputMultiplicities.end() != inputMultiplicities.find(ptr); + return inputMultiplicities.end() != inputMultiplicities.find(ptr->getID()); } void Transition::setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) { auto ptr = std::make_shared(place); - outputMultiplicities[ptr] = multiplicity; + outputMultiplicities[ptr->getID()] = multiplicity; outputPlaces.push_back(ptr); } bool Transition::removeOutputArc(storm::gspn::Place const& place) { if (existsOutputArc(place)) { auto ptr = std::make_shared(place); - outputMultiplicities.erase(ptr); + outputMultiplicities.erase(ptr->getID()); outputPlaces.erase(std::find(outputPlaces.begin(), outputPlaces.end(), ptr)); return true; } else { @@ -46,20 +46,20 @@ namespace storm { bool Transition::existsOutputArc(storm::gspn::Place const& place) const { auto ptr = std::make_shared(place); - return outputMultiplicities.end() != outputMultiplicities.find(ptr); + return outputMultiplicities.end() != outputMultiplicities.find(ptr->getID()); } void Transition::setInhibitionArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) { auto ptr = std::make_shared(place); - inhibitionMultiplicities[ptr] = multiplicity; + inhibitionMultiplicities[ptr->getID()] = multiplicity; inhibitionPlaces.push_back(ptr); } bool Transition::removeInhibitionArc(storm::gspn::Place const& place) { if (existsInhibitionArc(place)) { auto ptr = std::make_shared(place); - inhibitionMultiplicities.erase(ptr); + inhibitionMultiplicities.erase(ptr->getID()); inhibitionPlaces.erase(std::find(inhibitionPlaces.begin(), inhibitionPlaces.end(), ptr)); return true; } else { @@ -69,13 +69,13 @@ namespace storm { bool Transition::existsInhibitionArc(storm::gspn::Place const& place) const { auto ptr = std::make_shared(place); - return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr); + return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr->getID()); } bool Transition::isEnabled(storm::gspn::Marking const& marking) const { auto inputIterator = inputMultiplicities.cbegin(); while (inputIterator != inputMultiplicities.cend()) { - if (marking.getNumberOfTokensAt(inputIterator->first->getID()) < inputIterator->second) { + if (marking.getNumberOfTokensAt(inputIterator->first) < inputIterator->second) { return false; } @@ -84,22 +84,19 @@ namespace storm { auto inhibitionIterator = inhibitionMultiplicities.cbegin(); while (inhibitionIterator != inhibitionMultiplicities.cend()) { - if (marking.getNumberOfTokensAt(inhibitionIterator->first->getID()) >= inhibitionIterator->second) { + if (marking.getNumberOfTokensAt(inhibitionIterator->first) >= inhibitionIterator->second) { return false; } ++inhibitionIterator; } - auto outputIterator = outputMultiplicities.cbegin(); - while (outputIterator != outputMultiplicities.cend()) { - if (outputIterator->first->getCapacity() >= 0) { - if (marking.getNumberOfTokensAt(outputIterator->first->getID()) + outputIterator->second > outputIterator->first->getCapacity()) { + for (auto &placePtr : getOutputPlaces()) { + if (placePtr->getCapacity() >= 0) { + if (marking.getNumberOfTokensAt(placePtr->getID()) + getOutputArcMultiplicity(*placePtr) > placePtr->getCapacity()) { return false; } } - - ++outputIterator; } return true; @@ -110,15 +107,15 @@ namespace storm { auto inputIterator = inputMultiplicities.cbegin(); while (inputIterator != inputMultiplicities.cend()) { - newMarking.setNumberOfTokensAt(inputIterator->first->getID(), - newMarking.getNumberOfTokensAt(inputIterator->first->getID()) - inputIterator->second); + newMarking.setNumberOfTokensAt(inputIterator->first, + newMarking.getNumberOfTokensAt(inputIterator->first) - inputIterator->second); ++inputIterator; } auto outputIterator = outputMultiplicities.cbegin(); while (outputIterator != outputMultiplicities.cend()) { - newMarking.setNumberOfTokensAt(outputIterator->first->getID(), - newMarking.getNumberOfTokensAt(outputIterator->first->getID()) + outputIterator->second); + newMarking.setNumberOfTokensAt(outputIterator->first, + newMarking.getNumberOfTokensAt(outputIterator->first) + outputIterator->second); ++outputIterator; } @@ -133,34 +130,22 @@ namespace storm { return this->name; } - std::vector>::const_iterator Transition::getInputPlacesCBegin() const { - return this->inputPlaces.cbegin(); - } - - std::vector>::const_iterator Transition::getInputPlacesCEnd() const { - return this->inputPlaces.cend(); - } - - std::vector>::const_iterator Transition::getOutputPlacesCBegin() const { - return this->outputPlaces.cbegin(); - } - - std::vector>::const_iterator Transition::getOutputPlacesCEnd() const { - return this->outputPlaces.cend(); + const std::vector> &Transition::getInputPlaces() const { + return inputPlaces; } - std::vector>::const_iterator Transition::getInhibitionPlacesCBegin() const { - return this->inhibitionPlaces.cbegin(); + const std::vector> &Transition::getOutputPlaces() const { + return outputPlaces; } - std::vector>::const_iterator Transition::getInhibitionPlacesCEnd() const { - return this->inhibitionPlaces.cend(); + const std::vector> &Transition::getInhibitionPlaces() const { + return inhibitionPlaces; } uint_fast64_t Transition::getInputArcMultiplicity(storm::gspn::Place const& place) const { if (existsInputArc(place)) { auto ptr = std::make_shared(place); - return inputMultiplicities.at(ptr); + return inputMultiplicities.at(ptr->getID()); } else { return 0; } @@ -169,7 +154,7 @@ namespace storm { uint_fast64_t Transition::getInhibitionArcMultiplicity(storm::gspn::Place const& place) const { if (existsInhibitionArc(place)) { auto ptr = std::make_shared(place); - return inhibitionMultiplicities.at(ptr); + return inhibitionMultiplicities.at(ptr->getID()); } else { return 0; } @@ -178,7 +163,7 @@ namespace storm { uint_fast64_t Transition::getOutputArcMultiplicity(storm::gspn::Place const& place) const { if (existsOutputArc(place)) { auto ptr = std::make_shared(place); - return outputMultiplicities.at(ptr); + return outputMultiplicities.at(ptr->getID()); } else { return 0; } diff --git a/src/storage/gspn/Transition.h b/src/storage/gspn/Transition.h index e4d287e00..adda20253 100644 --- a/src/storage/gspn/Transition.h +++ b/src/storage/gspn/Transition.h @@ -121,46 +121,22 @@ namespace storm { std::string const& getName() const; /*! - * Returns a constant iterator to the begin of a vector which contains all input places. - * - * @return Returns iterator. - */ - std::vector>::const_iterator getInputPlacesCBegin() const; - - /*! - * Returns a constant iterator to the end of a vector which contains all input places. - * - * @return Returns iterator. + * Returns a list of places which are connected via a input arc. + * @return */ - std::vector>::const_iterator getInputPlacesCEnd() const; + const std::vector> &getInputPlaces() const; /*! - * Returns a constant iterator to the begin of a vector which contains all output places. - * - * @return Returns iterator. + * Returns a list of places which are connected via a output arc. + * @return */ - std::vector>::const_iterator getOutputPlacesCBegin() const; + const std::vector> &getOutputPlaces() const; /*! - * Returns a constant iterator to the end of a vector which contains all output places. - * - * @return Returns iterator. - */ - std::vector>::const_iterator getOutputPlacesCEnd() const; - - /*! - * Returns a constant iterator to the begin of a vector which contains all inhibition places. - * - * @return Returns iterator. - */ - std::vector>::const_iterator getInhibitionPlacesCBegin() const; - - /*! - * Returns a constant iterator to the end of a vector which contains all inhibition places. - * - * @return Returns iterator. + * Returns a list of places which are connected via a inhibition arc. + * @return */ - std::vector>::const_iterator getInhibitionPlacesCEnd() const; + const std::vector> &getInhibitionPlaces() const; /*! * Returns the corresponding multiplicity. @@ -205,19 +181,19 @@ namespace storm { * A place is less than another place if the id is less than the id from the other place. */ struct PlaceComparator { - bool operator()(std::shared_ptr const& lhs, std::shared_ptr const& rhs) const { - return lhs->getID() < rhs->getID(); + bool operator()(uint_fast64_t const& lhs, uint_fast64_t const& rhs) const { + return lhs < rhs; } }; - // maps places connected to this transition with an input arc to the corresponding multiplicity - std::map, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inputMultiplicities; + // maps place ids connected to this transition with an input arc to the corresponding multiplicity + std::map inputMultiplicities; - // maps places connected to this transition with an output arc to the corresponding multiplicities - std::map, uint_fast64_t, storm::gspn::Transition::PlaceComparator> outputMultiplicities; + // maps place ids connected to this transition with an output arc to the corresponding multiplicities + std::map outputMultiplicities; - // maps places connected to this transition with an inhibition arc to the corresponding multiplicity - std::map, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inhibitionMultiplicities; + // maps place ids connected to this transition with an inhibition arc to the corresponding multiplicity + std::map inhibitionMultiplicities; // name of the transition std::string name; From 5fa7d3d3998a3aa00589a1e99a29c716a70944ba Mon Sep 17 00:00:00 2001 From: ThomasH Date: Thu, 29 Sep 2016 22:30:12 +0200 Subject: [PATCH 7/7] refactor GspnBuilder Former-commit-id: a399617611c500b99a61633229968f70456d28d8 --- src/storage/gspn/GSPN.cpp | 13 +++++++++++-- src/storage/gspn/GSPN.h | 3 ++- src/storage/gspn/GspnBuilder.cpp | 32 ++++++++++++++------------------ src/storage/gspn/GspnBuilder.h | 21 +++++++-------------- src/storage/gspn/Transition.h | 8 +++++++- 5 files changed, 41 insertions(+), 36 deletions(-) diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index b63fa0e39..c40f58d2b 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -40,15 +40,24 @@ namespace storm { return m; } - std::pair GSPN::getPlace(std::string const& id) const { + std::pair GSPN::getPlace(uint_fast64_t const& id) const { for (auto& place : places) { - if (id.compare(place.getName()) == 0) { + if (id == place.getID()) { return std::make_pair(true, place); } } return std::make_pair(false, storm::gspn::Place()); } + std::pair GSPN::getPlace(std::string const& id) const { + for (auto& place : places) { + if (id.compare(place.getName())) { + return std::make_pair(true, place); + } + } + return std::make_pair(false, storm::gspn::Place()); + }; + std::pair> const> GSPN::getTimedTransition(std::string const& id) const { for (auto& trans : timedTransitions) { if (id.compare(trans->getName()) == 0) { diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h index c2f2ab22d..f1b8c8881 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -83,8 +83,9 @@ namespace storm { * If the first element is true, then the second element is the wanted place. * If the first element is false, then the second element is not defined. */ - std::pair getPlace(std::string const& id) const; + std::pair getPlace(uint_fast64_t const& id) const; + std::pair getPlace(std::string const& id) const; /*! * Returns the timed transition with the corresponding id. * diff --git a/src/storage/gspn/GspnBuilder.cpp b/src/storage/gspn/GspnBuilder.cpp index cdf4ae26d..38c1b773b 100644 --- a/src/storage/gspn/GspnBuilder.cpp +++ b/src/storage/gspn/GspnBuilder.cpp @@ -7,37 +7,33 @@ namespace storm { namespace gspn { - void GspnBuilder::addPlace(uint_fast64_t const& id, int_fast64_t const& capacity, uint_fast64_t const& initialTokens) { - addPlace(id, "place_" + std::to_string(id), capacity, initialTokens); - } - - void GspnBuilder::addPlace(uint_fast64_t const& id, std::string const& name, int_fast64_t const& capacity, uint_fast64_t const& initialTokens) { + uint_fast64_t GspnBuilder::addPlace(int_fast64_t const& capacity, uint_fast64_t const& initialTokens) { auto place = storm::gspn::Place(); place.setCapacity(capacity); - place.setID(id); - place.setName(name); + place.setID(nextStateID); place.setNumberOfInitialTokens(initialTokens); - - idToPlaceName.insert(std::pair(id, name)); gspn.addPlace(place); + return nextStateID++; } - void GspnBuilder::addImmediateTransition(uint_fast64_t const& id, uint_fast64_t const& priority, double const& weight) { + uint_fast64_t GspnBuilder::addImmediateTransition(uint_fast64_t const& priority, double const& weight) { auto trans = storm::gspn::ImmediateTransition(); - trans.setName(std::to_string(id)); + trans.setName(std::to_string(nextTransitionID)); trans.setPriority(priority); trans.setWeight(weight); - + trans.setID(nextTransitionID); gspn.addImmediateTransition(trans); + return nextTransitionID++; } - void GspnBuilder::addTimedTransition(uint_fast64_t const &id, uint_fast64_t const &priority, double const &rate) { + uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate) { auto trans = storm::gspn::TimedTransition(); - trans.setName(std::to_string(id)); + trans.setName(std::to_string(nextTransitionID)); trans.setPriority(priority); trans.setRate(rate); - + trans.setID(nextTransitionID); gspn.addTimedTransition(trans); + return nextTransitionID++; } void GspnBuilder::addInputArc(uint_fast64_t const &from, uint_fast64_t const &to, @@ -47,7 +43,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist."); } - auto placePair = gspn.getPlace(idToPlaceName.at(from)); + auto placePair = gspn.getPlace(from); if (!std::get<0>(placePair)) { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist."); } @@ -61,7 +57,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist."); } - auto placePair = gspn.getPlace(idToPlaceName.at(from)); + auto placePair = gspn.getPlace(from); if (!std::get<0>(placePair)) { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist."); } @@ -75,7 +71,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist."); } - auto placePair = gspn.getPlace(idToPlaceName.at(to)); + auto placePair = gspn.getPlace(to); if (!std::get<0>(placePair)) { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist."); } diff --git a/src/storage/gspn/GspnBuilder.h b/src/storage/gspn/GspnBuilder.h index f11b8c0dc..c5fcf6a5d 100644 --- a/src/storage/gspn/GspnBuilder.h +++ b/src/storage/gspn/GspnBuilder.h @@ -11,15 +11,6 @@ namespace storm { namespace gspn { class GspnBuilder { public: - /** - * Add a place to the gspn. - * @param id The id must be unique for the gspn. - * @param capacity The capacity is the limit of tokens in the place. - * A capacity of -1 indicates an unbounded place. - * @param initialTokens The number of inital tokens in the place. - */ - void addPlace(uint_fast64_t const& id, int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0); - /** * Add a place to the gspn. * @param id The id must be unique for the gspn. @@ -28,7 +19,7 @@ namespace storm { * A capacity of -1 indicates an unbounded place. * @param initialTokens The number of inital tokens in the place. */ - void addPlace(uint_fast64_t const& id, std::string const& name, int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0); + uint_fast64_t addPlace(int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0); /** * Adds an immediate transition to the gspn. @@ -36,7 +27,7 @@ namespace storm { * @param priority The priority for the transtion. * @param weight The weight for the transition. */ - void addImmediateTransition(uint_fast64_t const& id, uint_fast64_t const& priority = 0, double const& weight = 0); + uint_fast64_t addImmediateTransition(uint_fast64_t const& priority = 0, double const& weight = 0); /** * Adds an timed transition to the gspn. @@ -44,7 +35,7 @@ namespace storm { * @param priority The priority for the transtion. * @param weight The weight for the transition. */ - void addTimedTransition(uint_fast64_t const &id, uint_fast64_t const &priority = 0, double const &rate = 0); + uint_fast64_t addTimedTransition(uint_fast64_t const &priority = 0, double const &rate = 0); /** * Adds an new input arc from a place to an transition. @@ -78,8 +69,10 @@ namespace storm { private: // gspn which is returned storm::gspn::GSPN gspn; - // map from ids to names (for places) - std::map idToPlaceName; + // id for the next state which is added + uint_fast64_t nextStateID = 0; + // id for the next transition (timed or immediate) which is added + uint_fast64_t nextTransitionID = 0; }; } } diff --git a/src/storage/gspn/Transition.h b/src/storage/gspn/Transition.h index adda20253..4fb8cc7b9 100644 --- a/src/storage/gspn/Transition.h +++ b/src/storage/gspn/Transition.h @@ -175,6 +175,10 @@ namespace storm { * @return The priority. */ uint_fast64_t getPriority() const; + + void setID(uint_fast64_t const& id) { + this->id = id; + } private: /*! * Comparator which defines an total order on places. @@ -208,7 +212,9 @@ namespace storm { std::vector> inhibitionPlaces; // priority of this transition - uint_fast64_t priority; + uint_fast64_t priority = 0; + + uint_fast64_t id; }; } }