diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index 4a5435dd0..b3d23a9ff 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -313,6 +313,203 @@ namespace storm { return result; } + + void GSPN::toPnpro(std::ostream &stream) const { + auto space = " "; + auto space2 = " "; + auto space3 = " "; + auto projectName = "storm-export"; // TODO add to args + stream << "" << std::endl; + stream << space << "" << std::endl; + + u_int32_t x = 1; + stream << space2 << "" << std::endl; + for (auto& place : places) { + stream << space3 << "" << std::endl; + x = x + 3; + } + x = 1; + for (auto& trans : timedTransitions) { + stream << space3 << "getName() << "\" "; + stream << "type=\"EXP\" "; + stream << "nservers-x=\"" << trans->getRate() << "\" "; + stream << "x=\"" << x << "\" "; + stream << "y=\"4\" "; + stream << "/>" << std::endl; + x = x + 3; + } + for (auto& trans : immediateTransitions) { + stream << space3 << "getName() << "\" "; + stream << "type=\"IMM\" "; + stream << "x=\"" << x << "\" "; + stream << "y=\"4\" "; + stream << "/>" << std::endl; + x = x + 3; + } + stream << space2 << "" << std::endl; + + stream << space2 << "" << std::endl; + for (auto& trans : timedTransitions) { + for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) { + stream << space3 << "getName() << "\" "; + stream << "tail=\"" << (*it)->getName() << "\" "; + stream << "kind=\"INPUT\" "; + stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" "; + stream << "/>" << std::endl; + } + for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) { + stream << space3 << "getName() << "\" "; + stream << "tail=\"" << (*it)->getName() << "\" "; + stream << "kind=\"INHIBITOR\" "; + stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" "; + stream << "/>" << std::endl; + } + for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) { + stream << space3 << "getName() << "\" "; + stream << "tail=\"" << trans->getName() << "\" "; + stream << "kind=\"OUTPUT\" "; + stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" "; + stream << "/>" << std::endl; + } + } + for (auto& trans : immediateTransitions) { + for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) { + stream << space3 << "getName() << "\" "; + stream << "tail=\"" << (*it)->getName() << "\" "; + stream << "kind=\"INPUT\" "; + stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" "; + stream << "/>" << std::endl; + } + for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) { + stream << space3 << "getName() << "\" "; + stream << "tail=\"" << (*it)->getName() << "\" "; + stream << "kind=\"INHIBITOR\" "; + stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" "; + stream << "/>" << std::endl; + } + for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) { + stream << space3 << "getName() << "\" "; + stream << "tail=\"" << trans->getName() << "\" "; + stream << "kind=\"OUTPUT\" "; + stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" "; + stream << "/>" << std::endl; + } + } + stream << space2 << "" << std::endl; + stream << space << "" << std::endl; + stream << "" << std::endl; + } + + void GSPN::toPnml(std::ostream &stream) const { + std::string space = " "; + std::string space2 = " "; + std::string space3 = " "; + std::string space4 = " "; + + stream << "" << std::endl; + stream << space << "" << std::endl; + + // add places + for (const auto &place : places) { + stream << space2 << "" << std::endl; + stream << space3 << "" << std::endl; + stream << space4 << "Default," << place.getNumberOfInitialTokens() << "" << std::endl; + stream << space3 << "" << std::endl; + stream << space2 << "" << std::endl; + } + + // add immediate transitions + for (const auto &trans : immediateTransitions) { + stream << space2 << "getName() << "\">" << std::endl; + stream << space3 << "" << std::endl; + stream << space4 << "" << trans->getWeight() << "" << std::endl; + stream << space3 << "" << std::endl; + stream << space3 << "" << std::endl; + stream << space4 << "false" << std::endl; + stream << space3 << "" << std::endl; + stream << space2 << "" << std::endl; + } + + // add timed transitions + for (const auto &trans : timedTransitions) { + stream << space2 << "getName() << "\">" << std::endl; + stream << space3 << "" << std::endl; + stream << space4 << "" << trans->getRate() << "" << std::endl; + stream << space3 << "" << std::endl; + stream << space3 << "" << std::endl; + stream << space4 << "true" << std::endl; + stream << space3 << "" << std::endl; + stream << space2 << "" << std::endl; + } + + uint_fast64_t i = 0; + // add arcs for immediate transitions + for (const auto &trans : immediateTransitions) { + // add input arcs + for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) { + stream << space2 << "getName() << "\" "; + stream << "target=\"" << trans->getName() << "\" "; + stream << ">" << std::endl; + + stream << space3 << "" << std::endl; + stream << space4 << "Default," << trans->getInputArcMultiplicity(**it) << "" << std::endl; + stream << space3 << "" << std::endl; + + stream << space3 << "" << std::endl; + + stream << space2 << "" << std::endl; + } + + // add inhibition arcs + for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) { + stream << space2 << "getName() << "\" "; + stream << "target=\"" << trans->getName() << "\" "; + stream << ">" << std::endl; + + stream << space3 << "" << std::endl; + stream << space4 << "Default," << trans->getInputArcMultiplicity(**it) << "" << std::endl; + stream << space3 << "" << std::endl; + + stream << space3 << "" << std::endl; + + stream << space2 << "" << std::endl; + } + + // add output arcs + for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) { + stream << space2 << "getName() << "\" "; + stream << "target=\"" << (*it)->getName() << "\" "; + stream << ">" << std::endl; + + stream << space3 << "" << std::endl; + stream << space4 << "Default," << trans->getInputArcMultiplicity(**it) << "" << std::endl; + stream << space3 << "" << std::endl; + + stream << space3 << "" << std::endl; + + stream << space2 << "" << std::endl; + } + } + + stream << space << "" << std::endl; + stream << "" << std::endl; + } } } diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h index 49cf6cd33..c2f2ab22d 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -1,6 +1,7 @@ #ifndef STORM_STORAGE_GSPN_GSPN_H #define STORM_STORAGE_GSPN_GSPN_H +#include #include #include #include @@ -142,6 +143,10 @@ namespace storm { * @return true if no errors are found */ bool isValid() const; + // TODO doc + void toPnpro(std::ostream &stream) const; + // TODO doc + void toPnml(std::ostream &stream) const; private: /*! * Test