Browse Source

several minor fixes in gspn parser

Former-commit-id: 07a02340c9 [formerly 4e361502a5]
Former-commit-id: a574b2631d
main
sjunges 9 years ago
parent
commit
806a8febd4
  1. 55
      src/parser/GspnParser.cpp
  2. 9
      src/storage/gspn/GSPN.cpp
  3. 6
      src/storm-gspn.cpp

55
src/parser/GspnParser.cpp

@ -7,6 +7,7 @@
#include <xercesc/util/PlatformUtils.hpp> #include <xercesc/util/PlatformUtils.hpp>
#include "src/exceptions/UnexpectedException.h" #include "src/exceptions/UnexpectedException.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/storage/gspn/Place.h" #include "src/storage/gspn/Place.h"
#include "src/storage/gspn/ImmediateTransition.h" #include "src/storage/gspn/ImmediateTransition.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
@ -709,6 +710,15 @@ namespace storm {
} }
} }
} }
bool ignorePlaceAttribute(std::string const& name) {
// TODO we should probably not ignore x-servers but check that it is 0.5.
if ((name == "label-x") || (name == "label-y") || (name == "x") || (name == "y")) {
return true;
}
return false;
}
void GspnParser::traversePlaceElement(xercesc::DOMNode const* const node) { void GspnParser::traversePlaceElement(xercesc::DOMNode const* const node) {
storm::gspn::Place place; storm::gspn::Place place;
@ -725,8 +735,7 @@ namespace storm {
place.setName(XMLtoString(attr->getNodeValue())); place.setName(XMLtoString(attr->getNodeValue()));
} else if (name.compare("marking") == 0) { } else if (name.compare("marking") == 0) {
place.setNumberOfInitialTokens(std::stoull(XMLtoString(attr->getNodeValue()))); place.setNumberOfInitialTokens(std::stoull(XMLtoString(attr->getNodeValue())));
} else if (name.compare("x") == 0 ||
name.compare("y") == 0) {
} else if (ignorePlaceAttribute(name)) {
// ignore node // ignore node
} else { } else {
// Found node or attribute which is at the moment not handled by this parser. // Found node or attribute which is at the moment not handled by this parser.
@ -752,6 +761,14 @@ namespace storm {
gspn.addPlace(place); gspn.addPlace(place);
} }
bool ignoreTransitionAttribute(std::string const& name) {
// TODO we should probably not ignore x-servers but check that it is 0.5.
if ((name == "label-x") || (name == "label-y") || (name == "x") || (name == "y") || (name == "nservers-x")) {
return true;
}
return false;
}
void GspnParser::traverseTransitionElement(xercesc::DOMNode const* const node) { void GspnParser::traverseTransitionElement(xercesc::DOMNode const* const node) {
std::string transitionName; std::string transitionName;
@ -771,10 +788,9 @@ namespace storm {
} else { } else {
immediateTransition = true; immediateTransition = true;
} }
} else if(name.compare("nservers-x") == 0) {
} else if(name.compare("delay") == 0) {
rate = std::stod(XMLtoString(attr->getNodeValue())); rate = std::stod(XMLtoString(attr->getNodeValue()));
} else if (name.compare("x") == 0 ||
name.compare("y") == 0) {
} else if (ignoreTransitionAttribute(name)) {
// ignore node // ignore node
} else { } else {
// Found node or attribute which is at the moment not handled by this parser. // Found node or attribute which is at the moment not handled by this parser.
@ -809,9 +825,25 @@ namespace storm {
} }
} }
} }
bool ignoreArcAttribute(std::string const& name) {
if ((name == "mult-x") || (name == "mult-y") || (name == "mult-k")) {
return true;
}
return false;
}
bool ignoreArcChild(std::string const& name) {
if (name == "point") {
return true;
}
return false;
}
void GspnParser::traverseArcElement(xercesc::DOMNode const* const node) { void GspnParser::traverseArcElement(xercesc::DOMNode const* const node) {
std::string head, tail, kind;
std::string head = "____NOT_SET____";
std::string tail = "____NOT_SET____";
std::string kind = "____NOT_SET____";
uint_fast64_t mult = 1; uint_fast64_t mult = 1;
// traverse attributes // traverse attributes
@ -827,9 +859,7 @@ namespace storm {
kind = XMLtoString(attr->getNodeValue()); kind = XMLtoString(attr->getNodeValue());
} else if (name.compare("mult") == 0) { } else if (name.compare("mult") == 0) {
mult = std::stoull(XMLtoString(attr->getNodeValue())); mult = std::stoull(XMLtoString(attr->getNodeValue()));
} else if (name.compare("mult-x") == 0 ||
name.compare("mult-y") == 0 ||
name.compare("mult-k") == 0) {
} else if (ignoreArcAttribute(name)) {
// ignore node // ignore node
} else { } else {
// Found node or attribute which is at the moment not handled by this parser. // Found node or attribute which is at the moment not handled by this parser.
@ -838,6 +868,11 @@ namespace storm {
"unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
} }
} }
STORM_LOG_THROW(head.compare("____NOT_SET____") != 0, storm::exceptions::WrongFormatException, "Arc must have a head");
STORM_LOG_THROW(tail.compare("____NOT_SET____") != 0, storm::exceptions::WrongFormatException, "Arc must have a tail");
STORM_LOG_THROW(kind.compare("____NOT_SET____") != 0, storm::exceptions::WrongFormatException, "Arc must have a kind");
if (kind.compare("INPUT") == 0) { if (kind.compare("INPUT") == 0) {
auto transition = gspn.getTransition(head); auto transition = gspn.getTransition(head);
@ -868,6 +903,8 @@ namespace storm {
if (std::all_of(name.begin(), name.end(), isspace)) { if (std::all_of(name.begin(), name.end(), isspace)) {
// ignore node (contains only whitespace) // ignore node (contains only whitespace)
} else if(ignoreArcChild(name)) {
// ignore
} else { } else {
// Found node or attribute which is at the moment nod handled by this parser. // Found node or attribute which is at the moment nod handled by this parser.
// Notify the user and continue the parsing. // Notify the user and continue the parsing.

9
src/storage/gspn/GSPN.cpp

@ -1,5 +1,8 @@
#include "src/storage/gspn/GSPN.h" #include "src/storage/gspn/GSPN.h"
#include <src/utility/macros.h>
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
#include <boost/lexical_cast.hpp> #include <boost/lexical_cast.hpp>
namespace storm { namespace storm {
@ -51,11 +54,11 @@ namespace storm {
std::pair<bool, storm::gspn::Place> GSPN::getPlace(std::string const& id) const { std::pair<bool, storm::gspn::Place> GSPN::getPlace(std::string const& id) const {
for (auto& place : places) { for (auto& place : places) {
if (id.compare(place.getName())) {
if (id.compare(place.getName()) == 0) {
return std::make_pair<bool, storm::gspn::Place const&>(true, place); return std::make_pair<bool, storm::gspn::Place const&>(true, place);
} }
} }
return std::make_pair<bool, storm::gspn::Place>(false, storm::gspn::Place());
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "No place with name " << id);
}; };
std::pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const> GSPN::getTimedTransition(std::string const& id) const { std::pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const> GSPN::getTimedTransition(std::string const& id) const {

6
src/storm-gspn.cpp

@ -127,7 +127,13 @@ int main(const int argc, const char **argv) {
STORM_LOG_ERROR("The gspn is not valid."); STORM_LOG_ERROR("The gspn is not valid.");
} }
std::ofstream file;
file.open("gspn.dot");
gspn.writeDotToStream(file);
handleJani(gspn); handleJani(gspn);
return 0; return 0;

Loading…
Cancel
Save