diff --git a/examples/gspn/pnpro_test1/project01.PNPRO b/examples/gspn/pnpro_test1/project01.PNPRO
new file mode 100644
index 000000000..d5c530dd6
--- /dev/null
+++ b/examples/gspn/pnpro_test1/project01.PNPRO
@@ -0,0 +1,14 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
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/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp
index b3d23a9ff..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) {
@@ -100,56 +109,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 +198,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 +225,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 +350,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 +452,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 +469,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 +486,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/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/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..4fb8cc7b9 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.
+ * Returns a list of places which are connected via a input arc.
+ * @return
*/
- std::vector>::const_iterator getInputPlacesCBegin() const;
+ const std::vector> &getInputPlaces() 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 output arc.
+ * @return
*/
- std::vector>::const_iterator getInputPlacesCEnd() const;
+ const std::vector> &getOutputPlaces() 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 inhibition arc.
+ * @return
*/
- std::vector>::const_iterator getOutputPlacesCBegin() 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.
- */
- std::vector>::const_iterator getInhibitionPlacesCEnd() const;
+ const std::vector> &getInhibitionPlaces() const;
/*!
* Returns the corresponding multiplicity.
@@ -199,25 +175,29 @@ 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.
* 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;
@@ -232,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;
};
}
}
diff --git a/src/storm-gspn.cpp b/src/storm-gspn.cpp
index 171d84766..0c1e7740b 100644
--- a/src/storm-gspn.cpp
+++ b/src/storm-gspn.cpp
@@ -13,71 +13,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;
- if (next == end) {
- return -1;
- } else {
+ 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) {
- return -1;
- } else {
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) {
- return -1;
- } else {
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) {
- return -1;
- } else {
outputType = *next;
+ } else {
+ return -1;
}
- break;
+ continue;
}
// parse help argument
@@ -99,7 +98,7 @@ 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;
}
void handleJani(storm::gspn::GSPN const& gspn) {
@@ -112,7 +111,7 @@ void handleJani(storm::gspn::GSPN const& gspn) {
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;
}
@@ -120,41 +119,41 @@ 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]
- gspn.isValid();
-
+ if (!gspn.isValid()) {
+ STORM_LOG_ERROR("The gspn is not valid.");
+ }
+
handleJani(gspn);
- //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;
-
-
- // 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;
-
-
-
-
+
+ return 0;
+
+
+ // construct ma
+ auto builder = storm::builder::ExplicitGspnModelBuilder<>();
+ 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();