diff --git a/src/parser/GspnParser.cpp b/src/parser/GspnParser.cpp index a863ffb1a..3a1a1a3e9 100644 --- a/src/parser/GspnParser.cpp +++ b/src/parser/GspnParser.cpp @@ -1,7 +1,7 @@ #include -#include -#include #include +#include +#include #include "src/parser/GspnParser.h" storm::gspn::GSPN storm::parser::GspnParser::parse(const std::string &filename) { @@ -73,22 +73,21 @@ std::string storm::parser::GspnParser::XMLtoString(const XMLCh *xmlString) { } void storm::parser::GspnParser::parsePNML(xercesc::DOMElement *element) { - std::cout << "pnml" << std::endl; for (uint64_t i = 0; i < element->getChildNodes()->getLength(); ++i) { auto child = element->getChildNodes()->item(i); auto name = getName(child); if (name.compare("net") == 0) { parseNet(child); } else if (std::all_of(name.begin(), name.end(), isspace)) { - // TODO remove after adding DTD + // ignore node (contains only whitespace) } else { + std::cout << "pnml" << std::endl; std::cout << "unkown child: " << name << std::endl; } } } void storm::parser::GspnParser::parseNet(xercesc::DOMNode* node) { - std::cout << "net" << std::endl; for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { auto child = node->getChildNodes()->item(i); auto name = getName(child); @@ -101,17 +100,18 @@ void storm::parser::GspnParser::parseNet(xercesc::DOMNode* node) { } else if (name.compare("arc") == 0) { parseArc(child); } else if (std::all_of(name.begin(), name.end(), isspace)) { - // TODO remove after adding DTD - } else if (name.compare("name") == 0) { + // ignore node (contains only whitespace) + } else if (name.compare("name") == 0 || + name.compare("token") == 0) { // ignore these tags } else { + std::cout << "net" << std::endl; std::cout << "unkown child: " << name << std::endl; } } } void storm::parser::GspnParser::parsePage(xercesc::DOMNode *node) { - std::cout << "page" << std::endl; for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { auto child = node->getChildNodes()->item(i); auto name = getName(child); @@ -122,15 +122,15 @@ void storm::parser::GspnParser::parsePage(xercesc::DOMNode *node) { } else if (name.compare("arc") == 0) { parseArc(child); } else if (std::all_of(name.begin(), name.end(), isspace)) { - // TODO remove after adding DTD + // ignore node (contains only whitespace) } else { + std::cout << "page" << std::endl; std::cout << "unkown child: " << name << std::endl; } } } void storm::parser::GspnParser::parsePlace(xercesc::DOMNode *node) { - std::cout << "place" << std::endl; uint64_t place; for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) { auto attr = node->getAttributes()->item(i); @@ -138,37 +138,113 @@ void storm::parser::GspnParser::parsePlace(xercesc::DOMNode *node) { if (name.compare("id") == 0) { place = addNewPlace(XMLtoString(attr->getNodeValue())); } else { + std::cout << "place" << std::endl; std::cout << "unkown attr.: " << name << std::endl; } } - - //redo + for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { auto child = node->getChildNodes()->item(i); auto name = getName(child); if (name.compare("initialMarking") == 0) { auto tokens = parseInitialMarking(child); - gspn.setInitialTokens(place, tokens); + + std::cout << "place: " << place << "; tokens: " << tokens << std::endl; + //TODO search bug + gspn.setNumberOfPlaces(gspn.getNumberOfPlaces()+1); + //gspn.setInitialTokens(place, tokens); } else if (std::all_of(name.begin(), name.end(), isspace)) { - // TODO remove after adding DTD + // ignore node (contains only whitespace) } else if (name.compare("name") == 0 || - name.compare("graphics") == 0) { + name.compare("graphics") == 0) { // ignore these tags } else { + std::cout << "place" << std::endl; std::cout << "unkown child: " << name << std::endl; } } } void storm::parser::GspnParser::parseTransition(xercesc::DOMNode *node) { - //std::cout << "transition" << std::endl; // TODO bool timed = false; - //value for the rate + std::string rate, id; + + for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + if (name.compare("id") == 0) { + id = XMLtoString(attr->getNodeValue()); + } else { + std::cout << "transition" << std::endl; + std::cout << "unkown attr.: " << name << std::endl; + } + } + + for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("rate") == 0) { + rate = parseRate(child); + } else if (name.compare("timed") == 0) { + timed = parseTimed(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("graphics") == 0 || + name.compare("name") == 0 || + name.compare("orientation") == 0) { + // ignore these tags + } else { + std::cout << "transition" << std::endl; + std::cout << "unkown child: " << name << std::endl; + } + } + if (timed) { + auto transition = storm::gspn::TimedTransition(); + transition.setRate(std::stoull(rate)); + gspn.addTimedTransition(transition); + this->stringToTransition[id] = &transition; + } else { + auto transition = storm::gspn::ImmediateTransition(); + transition.setWeight(std::stoull(rate)); + gspn.addImmediateTransition(transition); + this->stringToTransition[id] = &transition; + } } void storm::parser::GspnParser::parseArc(xercesc::DOMNode *node) { - //std::cout << "arc" << std::endl; // TODO + std::string source, target, type; + + for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + if (name.compare("source") == 0) { + source = XMLtoString(attr->getNodeValue()); + } else if (name.compare("target") == 0) { + target = XMLtoString(attr->getNodeValue()); + } else if(name.compare("id") == 0) { + // ignore these tags + } else { + std::cout << "arc" << std::endl; + std::cout << "unkown attr.: " << name << std::endl; + } + } + + for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("type") == 0) { + type = parseType(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("graphics") == 0 || + name.compare("arcpath") == 0) { + // ignore these tags + } else { + std::cout << "arc" << std::endl; + std::cout << "unkown child: " << name << std::endl; + } + } } std::string storm::parser::GspnParser::getName(xercesc::DOMNode *node) { @@ -198,7 +274,6 @@ uint64_t storm::parser::GspnParser::addNewPlace(std::string id) { } uint64_t storm::parser::GspnParser::parseInitialMarking(xercesc::DOMNode *node) { - std::cout << "initialMarking" << std::endl; uint64_t result= 0; for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { auto child = node->getChildNodes()->item(i); @@ -207,15 +282,64 @@ uint64_t storm::parser::GspnParser::parseInitialMarking(xercesc::DOMNode *node) result = std::stoull(getName(child->getFirstChild())); } else if (name.compare("value") == 0) { auto value = getName(child->getFirstChild()); - value.substr(std::string("Default,").length()-1); + value = value.substr(std::string("Default,").length()); result = std::stoull(value); } else if (std::all_of(name.begin(), name.end(), isspace)) { - // TODO remove after adding DTD + // ignore node (contains only whitespace) } else if (name.compare("graphics") == 0) { // ignore these tags } else { + std::cout << "initialMarking" << std::endl; std::cout << "unkown child: " << name << std::endl; } } return result; } + +std::string storm::parser::GspnParser::parseRate(xercesc::DOMNode *node) { + std::string result = ""; + for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("value") == 0) { + result = getName(child->getFirstChild()); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + std::cout << "rate" << std::endl; + std::cout << "unkown child: " << name << std::endl; + } + } + return result; +} + +bool storm::parser::GspnParser::parseTimed(xercesc::DOMNode *node) { + bool result; + for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("value") == 0) { + result = getName(child->getFirstChild()).compare("true") ? true : false; + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + std::cout << "timed" << std::endl; + std::cout << "unkown child: " << name << std::endl; + } + } + return result; +} + +std::string storm::parser::GspnParser::parseType(xercesc::DOMNode *node) { + for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + if (name.compare("value") == 0) { + return XMLtoString(attr->getNodeValue()); + } else { + std::cout << "type" << std::endl; + std::cout << "unkown attr.: " << name << std::endl; + } + } + return ""; +} diff --git a/src/parser/GspnParser.h b/src/parser/GspnParser.h index f66d437b0..8e3978a33 100644 --- a/src/parser/GspnParser.h +++ b/src/parser/GspnParser.h @@ -34,6 +34,9 @@ namespace storm { // maps the original name of the state to its numerical representation std::map stringToState; + // maps the transition id to a pointer to the transition + std::map stringToTransition; + // the constructed gspn storm::gspn::GSPN gspn; @@ -41,49 +44,49 @@ namespace storm { uint64_t newNode; /*! - * Parses the root element (TagName = pnml). + * Parses the root element. * * @param element The root element. */ void parsePNML(xercesc::DOMElement* element); /*! - * Parses a net node (NodeName = net). + * Parses a net node. * * @param node The net node. */ void parseNet(xercesc::DOMNode* node); /*! - * Parses a page node (NodeName = page). + * Parses a page node. * * @param node The page node. a */ void parsePage(xercesc::DOMNode* node); /*! - * Parses a place node (NodeName = place). + * Parses a place node. * * @param node The place node. */ void parsePlace(xercesc::DOMNode* node); /*! - * Parses a transition node (NodeName = transition). + * Parses a transition node. * * @param node The transition node. */ void parseTransition(xercesc::DOMNode* node); /*! - * Parses an arc node (NodeName = arc). + * Parses an arc node. * * @param node The arc node. */ void parseArc(xercesc::DOMNode* node); /*! - * Parses an initial marking Node (Nodename = initialMarking) + * Parses an initial marking node . * * @param node the initial marking node. * @return The number of tokens. @@ -104,6 +107,21 @@ a */ * @return The name. */ std::string getName(xercesc::DOMNode* node); + + /*! + * Parses a rate node. + */ + std::string parseRate(xercesc::DOMNode* node); + + /*! + * Parse a timed node. + */ + bool parseTimed(xercesc::DOMNode* node); + + /*! + * Parse a type node. + */ + std::string parseType(xercesc::DOMNode* node); }; } } diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index 0ac6b1c77..409125f1a 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -9,3 +9,19 @@ void storm::gspn::GSPN::setInitialTokens(uint64_t place, uint64_t token) { } initialMarking.setNumberOfTokensAt(place, token); } + +void storm::gspn::GSPN::setNumberOfPlaces(uint64_t number) { + initialMarking.setNumberOfPlaces(number); +} + +uint64_t storm::gspn::GSPN::getNumberOfPlaces() { + return initialMarking.getNumberOfPlaces(); +} + +void storm::gspn::GSPN::addImmediateTransition(storm::gspn::ImmediateTransition &transition) { + this->immediateTransitions.push_back(transition); +} + +void storm::gspn::GSPN::addTimedTransition(storm::gspn::TimedTransition &transition) { + this->timedTransitions.push_back(transition); +} diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h index 7f6329eca..41221157e 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -27,6 +27,13 @@ namespace storm { * @param token */ void setInitialTokens(uint64_t place, uint64_t token); + + void setNumberOfPlaces(uint64_t number); + + uint64_t getNumberOfPlaces(); + + void addImmediateTransition(ImmediateTransition& transition); + void addTimedTransition(TimedTransition& transition); private: // set containing all immediate transitions std::vector> immediateTransitions; diff --git a/src/storage/gspn/Marking.cpp b/src/storage/gspn/Marking.cpp index 4d0763f6d..7f7c3ea43 100644 --- a/src/storage/gspn/Marking.cpp +++ b/src/storage/gspn/Marking.cpp @@ -81,8 +81,8 @@ namespace storm { marking.resize(getNumberOfPlaces() * newNumberOfBits); } else { marking.resize(getNumberOfPlaces() * newNumberOfBits); - for (uint_fast64_t i = getNumberOfPlaces()-1; i >= 0; --i) { - for (uint_fast64_t j = numberOfBits-1; j >= 0; --j) { + for (int_fast64_t i = getNumberOfPlaces()-1; i >= 0; --i) { + for (int_fast64_t j = numberOfBits-1; j >= 0; --j) { for (uint_fast64_t diff = 0; diff < newNumberOfBits-numberOfBits; ++diff) { marking.set(i*newNumberOfBits+j+diff+1, 0); } @@ -99,6 +99,9 @@ namespace storm { } uint_fast64_t Marking::calculateNumberOfBits(uint_fast64_t maxNumber) { + if (maxNumber == 0) { + return 1; + } return std::floor(std::log2(maxNumber)) + 1; } }