From 3229f07d430e9dddaab5ec401f16ba48c94befa8 Mon Sep 17 00:00:00 2001
From: ThomasH <thomas.henn@rwth-aachen.de>
Date: Sat, 7 Nov 2015 17:02:58 +0100
Subject: [PATCH] partial implemetation of the non-validating pnml parser
Former-commit-id: 0371967187c90e3957cf5cf2424ce7b37f217c28
---
src/parser/GspnParser.cpp | 217 ++++++++++++++++++++++++++++++++++-
src/parser/GspnParser.h | 88 +++++++++++++-
src/storage/gspn/GSPN.cpp | 9 +-
src/storage/gspn/GSPN.h | 8 ++
src/storage/gspn/Marking.cpp | 62 +++++++++-
src/storage/gspn/Marking.h | 13 +++
src/storm-gspn.cpp | 3 +-
7 files changed, 391 insertions(+), 9 deletions(-)
diff --git a/src/parser/GspnParser.cpp b/src/parser/GspnParser.cpp
index ded4f7cf1..a863ffb1a 100644
--- a/src/parser/GspnParser.cpp
+++ b/src/parser/GspnParser.cpp
@@ -1,8 +1,221 @@
+#include <string>
+#include <memory>
+#include <iosfwd>
+#include <bitset>
#include "src/parser/GspnParser.h"
storm::gspn::GSPN storm::parser::GspnParser::parse(const std::string &filename) {
+ // initialize xerces
+ try {
+ xercesc::XMLPlatformUtils::Initialize();
+ }
+ catch (const xercesc::XMLException& toCatch) {
+ // TODO do something
+ }
- //xercesc::XercesDOMParser;
- return storm::gspn::GSPN();
+
+ auto parser = new xercesc::XercesDOMParser();
+ parser->setValidationScheme(xercesc::XercesDOMParser::Val_Always);
+ parser->setDoNamespaces(false);
+ parser->setDoSchema(false);
+ parser->setLoadExternalDTD(false);
+ parser->setIncludeIgnorableWhitespace(false);
+ //parser->loadGrammar(source, type);
+
+ auto errHandler = (xercesc::ErrorHandler*) new xercesc::HandlerBase();
+ parser->setErrorHandler(errHandler);
+
+ try {
+ parser->parse(filename.c_str());
+ }
+ catch (const xercesc::XMLException& toCatch) {
+ auto message = xercesc::XMLString::transcode(toCatch.getMessage());
+ std::cout << "Exception message is: \n"
+ << message << "\n";
+ xercesc::XMLString::release(&message);
+ }
+ catch (const xercesc::DOMException& toCatch) {
+ auto message = xercesc::XMLString::transcode(toCatch.msg);
+ std::cout << "Exception message is: \n"
+ << message << "\n";
+ xercesc::XMLString::release(&message);
+ }
+ catch (...) {
+ std::cout << "Unexpected Exception \n" ;
+ }
+
+
+ parser->getDocument()->normalizeDocument();
+ xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement();
+ if (getName(elementRoot).compare("pnml") != 0) {
+ std::cout << "expected: pnml" << std::endl;
+ std::cout << "found: " << XMLtoString(elementRoot->getTagName()) << std::endl;
+ // TODO error
+ }
+ parsePNML(elementRoot);
+
+ delete parser;
+ delete errHandler;
+
+
+ // clean up
+ xercesc::XMLPlatformUtils::Terminate();
+
+ return gspn;
+}
+
+std::string storm::parser::GspnParser::XMLtoString(const XMLCh *xmlString) {
+ char* tmp = xercesc::XMLString::transcode(xmlString);
+ auto result = std::string(tmp);
+ delete tmp;
+ return result;
+}
+
+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
+ } else {
+ 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);
+ if (name.compare("page") == 0) {
+ parsePage(child);
+ } else if (name.compare("place") == 0) {
+ parsePlace(child);
+ } else if (name.compare("transition") == 0) {
+ parseTransition(child);
+ } 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 these tags
+ } else {
+ 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);
+ if (name.compare("place") == 0) {
+ parsePlace(child);
+ } else if (name.compare("transition") == 0) {
+ parseTransition(child);
+ } else if (name.compare("arc") == 0) {
+ parseArc(child);
+ } else if (std::all_of(name.begin(), name.end(), isspace)) {
+ // TODO remove after adding DTD
+ } else {
+ 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);
+ auto name = getName(attr);
+ if (name.compare("id") == 0) {
+ place = addNewPlace(XMLtoString(attr->getNodeValue()));
+ } else {
+ 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);
+ } else if (std::all_of(name.begin(), name.end(), isspace)) {
+ // TODO remove after adding DTD
+ } else if (name.compare("name") == 0 ||
+ name.compare("graphics") == 0) {
+ // ignore these tags
+ } else {
+ 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
+
+}
+
+void storm::parser::GspnParser::parseArc(xercesc::DOMNode *node) {
+ //std::cout << "arc" << std::endl; // TODO
+}
+
+std::string storm::parser::GspnParser::getName(xercesc::DOMNode *node) {
+ switch (node->getNodeType()) {
+ case xercesc::DOMNode::NodeType::ELEMENT_NODE: {
+ auto elementNode = (xercesc::DOMElement *) node;
+ return XMLtoString(elementNode->getTagName());
+ }
+ case xercesc::DOMNode::NodeType::TEXT_NODE: {
+ return XMLtoString(node->getNodeValue());
+ }
+ case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: {
+ return XMLtoString(node->getNodeName());
+ }
+ default: {
+ std::cout << "unknown NodeType: " << node->getNodeType() << std::endl;
+ return "";
+ }
+ }
+}
+
+uint64_t storm::parser::GspnParser::addNewPlace(std::string id) {
+ auto place = newNode;
+ ++newNode;
+ stringToState[id] = place;// TODO check whether the id is already in the map
+ return place;
+}
+
+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);
+ auto name = getName(child);
+ if (name.compare("text") == 0) {
+ result = std::stoull(getName(child->getFirstChild()));
+ } else if (name.compare("value") == 0) {
+ auto value = getName(child->getFirstChild());
+ value.substr(std::string("Default,").length()-1);
+ result = std::stoull(value);
+ } else if (std::all_of(name.begin(), name.end(), isspace)) {
+ // TODO remove after adding DTD
+ } else if (name.compare("graphics") == 0) {
+ // ignore these tags
+ } else {
+ std::cout << "unkown child: " << name << std::endl;
+ }
+ }
+ return result;
}
diff --git a/src/parser/GspnParser.h b/src/parser/GspnParser.h
index 4675f80f4..f66d437b0 100644
--- a/src/parser/GspnParser.h
+++ b/src/parser/GspnParser.h
@@ -1,8 +1,13 @@
#ifndef STORM_GSPNPARSER_H
#define STORM_GSPNPARSER_H
+#include <iostream>
#include <string>
#include <xercesc/parsers/XercesDOMParser.hpp>
+#include <xercesc/dom/DOM.hpp>
+#include <xercesc/sax/HandlerBase.hpp>
+#include <xercesc/util/XMLString.hpp>
+#include <xercesc/util/PlatformUtils.hpp>
#include "src/storage/gspn/GSPN.h"
namespace storm {
@@ -16,8 +21,89 @@ namespace storm {
* @param filename The name of the file to parse
* @return The resulting GSPN.
*/
- static storm::gspn::GSPN parse(std::string const& filename);
+ storm::gspn::GSPN parse(std::string const& filename);
+
+ /*!
+ * Transforms the given XML String to a normal string.
+ *
+ * @param xmlString The given String in the XML format
+ * @return The corresponding standard string.
+ */
+ static std::string XMLtoString(const XMLCh* xmlString);
private:
+ // maps the original name of the state to its numerical representation
+ std::map<std::string,uint64_t> stringToState;
+
+ // the constructed gspn
+ storm::gspn::GSPN gspn;
+
+ // has the new id for a new node
+ uint64_t newNode;
+
+ /*!
+ * Parses the root element (TagName = pnml).
+ *
+ * @param element The root element.
+ */
+ void parsePNML(xercesc::DOMElement* element);
+
+ /*!
+ * Parses a net node (NodeName = net).
+ *
+ * @param node The net node.
+ */
+ void parseNet(xercesc::DOMNode* node);
+
+ /*!
+ * Parses a page node (NodeName = page).
+ *
+ * @param node The page node.
+a */
+ void parsePage(xercesc::DOMNode* node);
+
+ /*!
+ * Parses a place node (NodeName = place).
+ *
+ * @param node The place node.
+ */
+ void parsePlace(xercesc::DOMNode* node);
+
+ /*!
+ * Parses a transition node (NodeName = transition).
+ *
+ * @param node The transition node.
+ */
+ void parseTransition(xercesc::DOMNode* node);
+
+ /*!
+ * Parses an arc node (NodeName = arc).
+ *
+ * @param node The arc node.
+ */
+ void parseArc(xercesc::DOMNode* node);
+
+ /*!
+ * Parses an initial marking Node (Nodename = initialMarking)
+ *
+ * @param node the initial marking node.
+ * @return The number of tokens.
+ */
+ uint64_t parseInitialMarking(xercesc::DOMNode* node);
+
+ /*!
+ * Adds a new entry in the mapping from string to places.
+ *
+ * @param id The string id for the new place
+ * @return The new place.
+ */
+ uint64_t addNewPlace(std::string id);
+
+ /*!
+ * Gives the name of the current node.
+ * @param node Current node.
+ * @return The name.
+ */
+ std::string getName(xercesc::DOMNode* node);
};
}
}
diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp
index f32dded64..0ac6b1c77 100644
--- a/src/storage/gspn/GSPN.cpp
+++ b/src/storage/gspn/GSPN.cpp
@@ -1,4 +1,11 @@
#include "src/storage/gspn/GSPN.h"
storm::gspn::GSPN::GSPN() : initialMarking(0, 0) {
-}
\ No newline at end of file
+}
+
+void storm::gspn::GSPN::setInitialTokens(uint64_t place, uint64_t token) {
+ if (initialMarking.getMaxNumberOfTokens() < token) {
+ initialMarking.setMaxNumberOfTokens(token);
+ }
+ initialMarking.setNumberOfTokensAt(place, token);
+}
diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h
index 711b69140..7f6329eca 100644
--- a/src/storage/gspn/GSPN.h
+++ b/src/storage/gspn/GSPN.h
@@ -19,6 +19,14 @@ namespace storm {
* The empty constructor creates an GSPN without transition and places
*/
GSPN();
+
+ /*!
+ * Set the number of tokens for a given place.
+ *
+ * @param place
+ * @param token
+ */
+ void setInitialTokens(uint64_t place, uint64_t token);
private:
// set containing all immediate transitions
std::vector<storm::gspn::ImmediateTransition<WeightType>> immediateTransitions;
diff --git a/src/storage/gspn/Marking.cpp b/src/storage/gspn/Marking.cpp
index e17c3d8df..4d0763f6d 100644
--- a/src/storage/gspn/Marking.cpp
+++ b/src/storage/gspn/Marking.cpp
@@ -6,7 +6,7 @@ namespace storm {
this->numberOfPlaces = numberOfPlaces;
this->maxNumberOfTokens = maxNumberOfTokens;
- this->numberOfBits = std::floor(std::log2(maxNumberOfTokens)) + 1;
+ this->numberOfBits = calculateNumberOfBits(maxNumberOfTokens);
this->marking = storm::storage::BitVector(numberOfBits * numberOfPlaces);
}
@@ -19,7 +19,7 @@ namespace storm {
}
void Marking::setNumberOfTokensAt(uint_fast64_t place, uint_fast64_t numberOfTokens) {
- //TODO check range (place < getNumberOfPlaces(), numberOfTokens < getMaxNumberOfTokens())
+ // TODO check range (place < getNumberOfPlaces(), numberOfTokens < getMaxNumberOfTokens())
for (uint_fast64_t i = place * numberOfBits; i <(place * numberOfBits) + numberOfBits; ++i) {
if (numberOfTokens % 2 == 0) {
marking.set(i, false);
@@ -41,11 +41,65 @@ namespace storm {
}
bool Marking::setNumberOfPlaces(uint_fast64_t numberOfPlaces) {
- return false;
+ if (numberOfPlaces == this->numberOfPlaces) {
+ return true;
+ }
+ if (numberOfPlaces > this->numberOfPlaces) {
+ marking.resize(numberOfPlaces * numberOfBits);
+ return true;
+ } else {
+ auto diff = this->numberOfPlaces - numberOfPlaces;
+ for (uint64_t i = 0; i < diff; ++i) {
+ if (getNumberOfTokensAt(numberOfPlaces-1-i) != 0) {
+ // TODO error
+ return false;
+ }
+ }
+ marking.resize(numberOfPlaces * numberOfBits);
+ return true;
+ }
}
bool Marking::setMaxNumberOfTokens(uint_fast64_t maxNumberOfTokens) {
- return false;
+ for (uint64_t i = 0; i < getNumberOfPlaces(); ++i) {
+ if (getNumberOfTokensAt(i) > maxNumberOfTokens) {
+ return false;
+ }
+ }
+
+ if (maxNumberOfTokens == getMaxNumberOfTokens()) {
+ return true;
+ }
+
+ uint_fast64_t newNumberOfBits = calculateNumberOfBits(maxNumberOfTokens);
+ if (maxNumberOfTokens < getMaxNumberOfTokens()) {
+ for (uint_fast64_t i = 0; i < getNumberOfPlaces(); ++i) {
+ for (uint_fast64_t j = 0; j < numberOfBits; ++j) {
+ marking.set(i*newNumberOfBits + j , marking.get(i*numberOfBits + j));
+ }
+ }
+ 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 (uint_fast64_t diff = 0; diff < newNumberOfBits-numberOfBits; ++diff) {
+ marking.set(i*newNumberOfBits+j+diff+1, 0);
+ }
+ marking.set(i*newNumberOfBits+j, marking.get(i*numberOfBits+j));
+ }
+ }
+ }
+ numberOfBits = newNumberOfBits;
+ return true;
+ }
+
+ void Marking::incNumberOfPlaces() {
+ setNumberOfPlaces(getNumberOfPlaces()+1);
+ }
+
+ uint_fast64_t Marking::calculateNumberOfBits(uint_fast64_t maxNumber) {
+ return std::floor(std::log2(maxNumber)) + 1;
}
}
}
\ No newline at end of file
diff --git a/src/storage/gspn/Marking.h b/src/storage/gspn/Marking.h
index 8f5e1400c..5d312c88c 100644
--- a/src/storage/gspn/Marking.h
+++ b/src/storage/gspn/Marking.h
@@ -58,6 +58,11 @@ namespace storm {
*/
bool setNumberOfPlaces(uint_fast64_t numberOfPlaces);
+ /*!
+ * Increases the number of places by one.
+ */
+ void incNumberOfPlaces();
+
/*!
*
*/
@@ -74,6 +79,14 @@ namespace storm {
// number of bits which are needed to store the tokens for one place
uint_fast64_t numberOfBits;
+
+ /*!
+ * Calculates the number of bits needed to store at least the given number.
+ *
+ * @param maxNumber The maximal value which can be stored
+ * @return The number of bits needed.
+ */
+ uint_fast64_t calculateNumberOfBits(uint_fast64_t maxNumber);
};
}
}
diff --git a/src/storm-gspn.cpp b/src/storm-gspn.cpp
index 8cb7211c4..450d57652 100644
--- a/src/storm-gspn.cpp
+++ b/src/storm-gspn.cpp
@@ -16,7 +16,8 @@ int main(const int argc, const char** argv) {
storm::utility::setUp();
// Parse GSPN from xml
- storm::gspn::GSPN gspn = storm::parser::GspnParser::parse(argv[1]);
+ auto parser = storm::parser::GspnParser();
+ auto gspn = parser.parse(argv[1]);
// Construct MA