From bd057da74310a4e32bacab940be48282a044f388 Mon Sep 17 00:00:00 2001 From: ThomasH Date: Mon, 26 Sep 2016 12:31:29 +0200 Subject: [PATCH] refactoring gspn Former-commit-id: c7c4764901cb47d859c07511f7ea4d694ec51790 --- src/storage/gspn/GSPN.cpp | 153 +++++++++++++++----------------- src/storage/gspn/Place.cpp | 2 +- src/storage/gspn/Place.h | 10 ++- src/storage/gspn/Transition.cpp | 69 ++++++-------- src/storage/gspn/Transition.h | 58 ++++-------- 5 files changed, 121 insertions(+), 171 deletions(-) diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index b3d23a9ff..b63fa0e39 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -100,56 +100,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 +189,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 +216,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 +341,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 +443,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 +460,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 +477,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/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..adda20253 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. - */ - std::vector>::const_iterator getInputPlacesCBegin() 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 input arc. + * @return */ - std::vector>::const_iterator getInputPlacesCEnd() const; + const std::vector> &getInputPlaces() 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 output arc. + * @return */ - std::vector>::const_iterator getOutputPlacesCBegin() const; + const std::vector> &getOutputPlaces() 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. + * Returns a list of places which are connected via a inhibition arc. + * @return */ - std::vector>::const_iterator getInhibitionPlacesCEnd() const; + const std::vector> &getInhibitionPlaces() const; /*! * Returns the corresponding multiplicity. @@ -205,19 +181,19 @@ namespace storm { * 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;