diff --git a/src/builder/ExplicitGspnModelBuilder.cpp b/src/builder/ExplicitGspnModelBuilder.cpp index 2843a197b..f3682de28 100644 --- a/src/builder/ExplicitGspnModelBuilder.cpp +++ b/src/builder/ExplicitGspnModelBuilder.cpp @@ -109,7 +109,7 @@ namespace storm { } } - + //auto labeling = getStateLabeling(); return storm::models::sparse::MarkovAutomaton(matrix, labeling, markovianStates, exitRates); diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index dfb9d0f57..4a5435dd0 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -1,4 +1,6 @@ #include "src/storage/gspn/GSPN.h" +#include +#include namespace storm { namespace gspn { @@ -11,7 +13,6 @@ namespace storm { } void GSPN::addPlace(Place const& place) { - //TODO check whether the name or id is already used by an place this->places.push_back(place); } @@ -162,6 +163,156 @@ namespace storm { std::string const& GSPN::getName() const { return this->name; } + + bool GSPN::isValid() const { + bool result = true; + result |= testPlaces(); + result |= testTransitions(); + + return result; + } + + bool GSPN::testPlaces() const { + std::vector namesOfPlaces; + std::vector idsOfPlaces; + bool result = true; + + for (auto const& place : this->getPlaces()) { + + if (std::find(namesOfPlaces.begin(), namesOfPlaces.end(), place.getName()) != namesOfPlaces.end()) { + STORM_PRINT_AND_LOG("duplicates states with the name \"" + place.getName() + "\"\n") + result = false; + } + + if (std::find(idsOfPlaces.begin(), idsOfPlaces.end(), place.getID()) != idsOfPlaces.end()) { + STORM_PRINT_AND_LOG("duplicates states with the id \"" + boost::lexical_cast(place.getID()) + "\"\n") + result = false; + } + + if (place.getNumberOfInitialTokens() > place.getNumberOfInitialTokens()) { + STORM_PRINT_AND_LOG("number of initial tokens is greater than the capacity for place \"" + place.getName() + "\"\n") + result = false; + } + } + + return result; + } + + bool GSPN::testTransitions() const { + bool result = true; + + for (auto const& transition : this->getImmediateTransitions()) { + if (transition->getInputPlacesCBegin() == transition->getInputPlacesCEnd() && + transition->getInhibitionPlacesCBegin() == transition->getInhibitionPlacesCEnd()) { + STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n") + result = false; + } + + if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) { + 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()) { + STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n") + result = false; + } + + if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) { + STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n") + result = false; + } + } + + //test if places exists in the gspn + for (auto const& transition : this->getImmediateTransitions()) { + for (auto it = transition->getInputPlacesCBegin(); it != transition->getInputPlacesCEnd(); ++it) { + bool foundPlace = false; + for (auto const& place : places) { + if (place.getName() == (*it)->getName()) { + foundPlace = true; + } + } + if (!foundPlace) { + STORM_PRINT_AND_LOG("input place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + result = false; + } + } + + for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) { + bool foundPlace = false; + for (auto const& place : places) { + if (place.getName() == (*it)->getName()) { + foundPlace = true; + } + } + if (!foundPlace) { + STORM_PRINT_AND_LOG("inhibition place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + result = false; + } + } + + for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) { + bool foundPlace = false; + for (auto const& place : places) { + if (place.getName() == (*it)->getName()) { + foundPlace = true; + } + } + if (!foundPlace) { + STORM_PRINT_AND_LOG("output place \"" + (*it)->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) { + bool foundPlace = false; + for (auto const& place : places) { + if (place.getName() == (*it)->getName()) { + foundPlace = true; + } + } + if (!foundPlace) { + STORM_PRINT_AND_LOG("input place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + result = false; + } + } + + for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) { + bool foundPlace = false; + for (auto const& place : places) { + if (place.getName() == (*it)->getName()) { + foundPlace = true; + } + } + if (!foundPlace) { + STORM_PRINT_AND_LOG("inhibition place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + result = false; + } + } + + for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) { + bool foundPlace = false; + for (auto const& place : places) { + if (place.getName() == (*it)->getName()) { + foundPlace = true; + } + } + if (!foundPlace) { + STORM_PRINT_AND_LOG("output place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + result = false; + } + } + } + + + return result; + } } } diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h index b8845cbff..49cf6cd33 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -133,7 +133,33 @@ namespace storm { * @return The name. */ std::string const& getName() const; + + /*! + * Performe some checks + * - testPlaces() + * - testTransitions() + * + * @return true if no errors are found + */ + bool isValid() const; private: + /*! + * Test + * - if places are unique (ids and names) + * - if the capacity is greater than the number of initial tokens + * + * @return true if no errors found + */ + bool testPlaces() const; + + /*! + * Test + * - if transition have at least on input/inhibitor and one output place + * + * @return true if no errors found + */ + bool testTransitions() const; + // set containing all immediate transitions std::vector>> immediateTransitions; diff --git a/src/storm-gspn.cpp b/src/storm-gspn.cpp index 706b9ce42..76b2be886 100644 --- a/src/storm-gspn.cpp +++ b/src/storm-gspn.cpp @@ -21,6 +21,7 @@ int main(const int argc, const char** argv) { // Parse GSPN from xml auto parser = storm::parser::GspnParser(); auto gspn = parser.parse(argv[1]); + gspn.isValid(); // //std::ofstream file;