Browse Source

partial implemetation of the non-validating pnml parser

Former-commit-id: 0371967187
tempestpy_adaptions
ThomasH 9 years ago
parent
commit
3229f07d43
  1. 217
      src/parser/GspnParser.cpp
  2. 88
      src/parser/GspnParser.h
  3. 9
      src/storage/gspn/GSPN.cpp
  4. 8
      src/storage/gspn/GSPN.h
  5. 62
      src/storage/gspn/Marking.cpp
  6. 13
      src/storage/gspn/Marking.h
  7. 3
      src/storm-gspn.cpp

217
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;
}

88
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);
};
}
}

9
src/storage/gspn/GSPN.cpp

@ -1,4 +1,11 @@
#include "src/storage/gspn/GSPN.h"
storm::gspn::GSPN::GSPN() : initialMarking(0, 0) {
}
}
void storm::gspn::GSPN::setInitialTokens(uint64_t place, uint64_t token) {
if (initialMarking.getMaxNumberOfTokens() < token) {
initialMarking.setMaxNumberOfTokens(token);
}
initialMarking.setNumberOfTokensAt(place, token);
}

8
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;

62
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;
}
}
}

13
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);
};
}
}

3
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

Loading…
Cancel
Save