From 3dfe4640e9f905454f296b3d0a1c1bf041c8d1a5 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 15 Nov 2016 10:53:34 +0100 Subject: [PATCH] cleaning gspns Former-commit-id: 6da157d91579c523a2351d7fbda348bb4349116e [formerly d83f1ab30f15e645e7ddd5ee1ee20eefb81cabb7] Former-commit-id: b0753441c37d051ab25b883eed262c773bf8c697 --- src/builder/JaniGSPNBuilder.h | 50 ++--- src/storage/gspn/GSPN.cpp | 318 +++++++++++++++----------------- src/storage/gspn/GSPN.h | 9 +- src/storage/gspn/Transition.cpp | 80 +++----- src/storage/gspn/Transition.h | 75 +++----- 5 files changed, 232 insertions(+), 300 deletions(-) diff --git a/src/builder/JaniGSPNBuilder.h b/src/builder/JaniGSPNBuilder.h index e7da0e776..30b5c3b6f 100644 --- a/src/builder/JaniGSPNBuilder.h +++ b/src/builder/JaniGSPNBuilder.h @@ -63,15 +63,15 @@ namespace storm { for (auto const& trans : gspn.getImmediateTransitions()) { if (ignoreWeights || trans.noWeightAttached()) { std::vector assignments; - for (auto const& inPlace : trans.getInputPlaces()) { - guard = guard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans.getInputArcMultiplicity(*inPlace)); - assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans.getInputArcMultiplicity(*inPlace)) ); + for (auto const& inPlaceEntry : trans.getInputPlaces()) { + guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); + assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second); } - for (auto const& inhibPlace : trans.getInhibitionPlaces()) { - guard = guard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans.getInhibitionArcMultiplicity(*inhibPlace)); + for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { + guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); } - for (auto const& outputPlace : trans.getOutputPlaces()) { - assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans.getOutputArcMultiplicity(*outputPlace)) ); + for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { + assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second ); } storm::jani::OrderedAssignments oa(assignments); storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa); @@ -93,11 +93,11 @@ namespace storm { continue; } storm::expressions::Expression destguard = expressionManager->boolean(true); - for (auto const& inPlace : trans.getInputPlaces()) { - destguard = destguard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans.getInputArcMultiplicity(*inPlace)); + for (auto const& inPlaceEntry : trans.getInputPlaces()) { + destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); } - for (auto const& inhibPlace : trans.getInhibitionPlaces()) { - destguard = destguard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans.getInhibitionArcMultiplicity(*inhibPlace)); + for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { + destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); } totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0)); @@ -110,15 +110,15 @@ namespace storm { } storm::expressions::Expression destguard = expressionManager->boolean(true); std::vector assignments; - for (auto const& inPlace : trans.getInputPlaces()) { - destguard = destguard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans.getInputArcMultiplicity(*inPlace)); - assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans.getInputArcMultiplicity(*inPlace)) ); + for (auto const& inPlaceEntry : trans.getInputPlaces()) { + destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); + assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) ); } - for (auto const& inhibPlace : trans.getInhibitionPlaces()) { - destguard = destguard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans.getInhibitionArcMultiplicity(*inhibPlace)); + for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { + destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); } - for (auto const& outputPlace : trans.getOutputPlaces()) { - assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans.getOutputArcMultiplicity(*outputPlace)) ); + for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { + assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) ); } destguard = destguard.simplify(); guard = guard || destguard; @@ -133,15 +133,15 @@ namespace storm { storm::expressions::Expression guard = expressionManager->boolean(true); std::vector assignments; - for (auto const& inPlace : trans.getInputPlaces()) { - guard = guard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans.getInputArcMultiplicity(*inPlace)); - assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans.getInputArcMultiplicity(*inPlace)) ); + for (auto const& inPlaceEntry : trans.getInputPlaces()) { + guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); + assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) ); } - for (auto const& inhibPlace : trans.getInhibitionPlaces()) { - guard = guard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans.getInhibitionArcMultiplicity(*inhibPlace)); + for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { + guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); } - for (auto const& outputPlace : trans.getOutputPlaces()) { - assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans.getOutputArcMultiplicity(*outputPlace)) ); + for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { + assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) ); } storm::jani::OrderedAssignments oa(assignments); storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa); diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index 7e7ffbe37..c692b2b13 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -30,7 +30,7 @@ namespace storm { } - uint_fast64_t GSPN::getNumberOfPlaces() const { + uint64_t GSPN::getNumberOfPlaces() const { return places.size(); } @@ -46,7 +46,7 @@ namespace storm { return places; } - std::shared_ptr GSPN::getInitialMarking(std::map& numberOfBits, uint_fast64_t const& numberOfTotalBits) const { + std::shared_ptr GSPN::getInitialMarking(std::map& numberOfBits, uint64_t const& numberOfTotalBits) const { auto m = std::make_shared(getNumberOfPlaces(), numberOfBits, numberOfTotalBits); for (auto& place : getPlaces()) { m->setNumberOfTokensAt(place.getID(), place.getNumberOfInitialTokens()); @@ -158,42 +158,30 @@ namespace storm { // print arcs for (auto& trans : this->getImmediateTransitions()) { - for (auto &placePtr : trans.getInputPlaces()) { - outStream << "\t" << placePtr->getName() << " -> " << trans.getName() << "[label=\"" << - trans.getInputArcMultiplicity(*placePtr); - outStream << "\"];" << std::endl; + for (auto const& inEntry : trans.getInputPlaces()) { + outStream << "\t" << places.at(inEntry.first).getName() << " -> " << trans.getName() << "[label=\"" << inEntry.second << "\"];" << std::endl; } - for (auto &placePtr : trans.getInhibitionPlaces()) { - outStream << "\t" << placePtr->getName() << " -> " << trans.getName() << "[arrowhead=\"dot\", label=\"" << - trans.getInhibitionArcMultiplicity(*placePtr); - outStream << "\"];" << std::endl; + for (auto const& inhEntry : trans.getInhibitionPlaces()) { + outStream << "\t" << places.at(inhEntry.first).getName() << " -> " << trans.getName() << "[arrowhead=\"dot\", label=\"" << inhEntry.second << "\"];" << std::endl; } - for (auto &placePtr : trans.getOutputPlaces()) { - outStream << "\t" << trans.getName() << " -> " << placePtr->getName() << "[label=\"" << - trans.getOutputArcMultiplicity(*placePtr); - outStream << "\"];" << std::endl; + for (auto const& outEntry : trans.getOutputPlaces()) { + outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[label=\"" << outEntry.second << "\"];" << std::endl; } } for (auto& trans : this->getTimedTransitions()) { - for (auto &placePtr : trans.getInputPlaces()) { - outStream << "\t" << placePtr->getName() << " -> " << trans.getName() << "[label=\"" << - trans.getInputArcMultiplicity(*placePtr); - outStream << "\"];" << std::endl; + for (auto const& inEntry : trans.getInputPlaces()) { + outStream << "\t" << places.at(inEntry.first).getName() << " -> " << trans.getName() << "[label=\"" << inEntry.second << "\"];" << std::endl; } - - for (auto &placePtr : trans.getInhibitionPlaces()) { - outStream << "\t" << placePtr->getName() << " -> " << trans.getName() << "[arrowhead=\"dot\", label=\"" << - trans.getInhibitionArcMultiplicity(*placePtr); - outStream << "\"];" << std::endl; + + for (auto const& inhEntry : trans.getInhibitionPlaces()) { + outStream << "\t" << places.at(inhEntry.first).getName() << " -> " << trans.getName() << "[arrowhead=\"dot\", label=\"" << inhEntry.second << "\"];" << std::endl; } - - for (auto &placePtr : trans.getOutputPlaces()) { - outStream << "\t" << trans.getName() << " -> " << placePtr->getName() << "[label=\"" << - trans.getOutputArcMultiplicity(*placePtr); - outStream << "\"];" << std::endl; + + for (auto const& outEntry : trans.getOutputPlaces()) { + outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[label=\"" << outEntry.second << "\"];" << std::endl; } } @@ -218,7 +206,7 @@ namespace storm { bool GSPN::testPlaces() const { std::vector namesOfPlaces; - std::vector idsOfPlaces; + std::vector idsOfPlaces; bool result = true; for (auto const& place : this->getPlaces()) { @@ -245,114 +233,114 @@ namespace storm { bool GSPN::testTransitions() const { bool result = true; - for (auto const& transition : this->getImmediateTransitions()) { - 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.getOutputPlaces().empty()) { - STORM_PRINT_AND_LOG("transition \"" + transition.getName() + "\" has no output place\n") - result = false; - } - } - - for (auto const& transition : this->getTimedTransitions()) { - 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.getOutputPlaces().empty()) { - 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 &placePtr : transition.getInputPlaces()) { - bool foundPlace = false; - for (auto const& place : places) { - if (place.getName() == placePtr->getName()) { - foundPlace = true; - } - } - if (!foundPlace) { - STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") - result = false; - } - } - - for (auto &placePtr : transition.getInhibitionPlaces()) { - bool foundPlace = false; - for (auto const& place : places) { - if (place.getName() == placePtr->getName()) { - foundPlace = true; - } - } - if (!foundPlace) { - STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") - result = false; - } - } - - for (auto &placePtr : transition.getOutputPlaces()) { - bool foundPlace = false; - for (auto const& place : places) { - if (place.getName() == placePtr->getName()) { - foundPlace = true; - } - } - if (!foundPlace) { - 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 &placePtr : transition.getInputPlaces()) { - bool foundPlace = false; - for (auto const& place : places) { - if (place.getName() == placePtr->getName()) { - foundPlace = true; - } - } - if (!foundPlace) { - STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") - result = false; - } - } - - for (auto &placePtr : transition.getInhibitionPlaces()) { - bool foundPlace = false; - for (auto const& place : places) { - if (place.getName() == placePtr->getName()) { - foundPlace = true; - } - } - if (!foundPlace) { - STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") - result = false; - } - } - - for (auto &placePtr : transition.getOutputPlaces()) { - bool foundPlace = false; - for (auto const& place : places) { - if (place.getName() == placePtr->getName()) { - foundPlace = true; - } - } - if (!foundPlace) { - STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") - result = false; - } - } - } +// for (auto const& transition : this->getImmediateTransitions()) { +// 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.getOutputPlaces().empty()) { +// STORM_PRINT_AND_LOG("transition \"" + transition.getName() + "\" has no output place\n") +// result = false; +// } +// } +// +// for (auto const& transition : this->getTimedTransitions()) { +// 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.getOutputPlaces().empty()) { +// 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 &placePtr : transition.getInputPlaces()) { +// bool foundPlace = false; +// for (auto const& place : places) { +// if (place.getName() == placePtr->getName()) { +// foundPlace = true; +// } +// } +// if (!foundPlace) { +// STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") +// result = false; +// } +// } +// +// for (auto &placePtr : transition.getInhibitionPlaces()) { +// bool foundPlace = false; +// for (auto const& place : places) { +// if (place.getName() == placePtr->getName()) { +// foundPlace = true; +// } +// } +// if (!foundPlace) { +// STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") +// result = false; +// } +// } +// +// for (auto &placePtr : transition.getOutputPlaces()) { +// bool foundPlace = false; +// for (auto const& place : places) { +// if (place.getName() == placePtr->getName()) { +// foundPlace = true; +// } +// } +// if (!foundPlace) { +// 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 &placePtr : transition.getInputPlaces()) { +// bool foundPlace = false; +// for (auto const& place : places) { +// if (place.getName() == placePtr->getName()) { +// foundPlace = true; +// } +// } +// if (!foundPlace) { +// STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") +// result = false; +// } +// } +// +// for (auto &placePtr : transition.getInhibitionPlaces()) { +// bool foundPlace = false; +// for (auto const& place : places) { +// if (place.getName() == placePtr->getName()) { +// foundPlace = true; +// } +// } +// if (!foundPlace) { +// STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") +// result = false; +// } +// } +// +// for (auto &placePtr : transition.getOutputPlaces()) { +// bool foundPlace = false; +// for (auto const& place : places) { +// if (place.getName() == placePtr->getName()) { +// foundPlace = true; +// } +// } +// if (!foundPlace) { +// STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") +// result = false; +// } +// } +// } return result; @@ -398,54 +386,54 @@ namespace storm { stream << space2 << "" << std::endl; for (auto& trans : timedTransitions) { - for (auto &placePtr : trans.getInputPlaces()) { + for (auto const& inEntry : trans.getInputPlaces()) { stream << space3 << "getName() << "\" "; + stream << "tail=\"" << places.at(inEntry.first).getName() << "\" "; stream << "kind=\"INPUT\" "; - stream << "mult=\"" << trans.getInputArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << inEntry.second << "\" "; stream << "/>" << std::endl; } - for (auto &placePtr : trans.getInhibitionPlaces()) { + for (auto const& inhEntry : trans.getInhibitionPlaces()) { stream << space3 << "getName() << "\" "; + stream << "tail=\"" << places.at(inhEntry.first).getName() << "\" "; stream << "kind=\"INHIBITOR\" "; - stream << "mult=\"" << trans.getInhibitionArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << inhEntry.second << "\" "; stream << "/>" << std::endl; } - for (auto &placePtr : trans.getOutputPlaces()) { + for (auto const& outEntry : trans.getOutputPlaces()) { stream << space3 << "getName() << "\" "; + stream << "head=\"" << places.at(outEntry.first).getName() << "\" "; stream << "tail=\"" << trans.getName() << "\" "; stream << "kind=\"OUTPUT\" "; - stream << "mult=\"" << trans.getOutputArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << outEntry.second << "\" "; stream << "/>" << std::endl; } } for (auto& trans : immediateTransitions) { - for (auto &placePtr : trans.getInputPlaces()) { + for (auto const& inEntry : trans.getInputPlaces()) { stream << space3 << "getName() << "\" "; + stream << "tail=\"" << places.at(inEntry.first).getName() << "\" "; stream << "kind=\"INPUT\" "; - stream << "mult=\"" << trans.getInputArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << inEntry.second << "\" "; stream << "/>" << std::endl; } - for (auto &placePtr : trans.getInhibitionPlaces()) { + for (auto const& inhEntry : trans.getInhibitionPlaces()) { stream << space3 << "getName() << "\" "; + stream << "tail=\"" << places.at(inhEntry.first).getName() << "\" "; stream << "kind=\"INHIBITOR\" "; - stream << "mult=\"" << trans.getInhibitionArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << inhEntry.second << "\" "; stream << "/>" << std::endl; } - for (auto &placePtr : trans.getOutputPlaces()) { + for (auto const& outEntry : trans.getOutputPlaces()) { stream << space3 << "getName() << "\" "; + stream << "head=\"" << places.at(outEntry.first).getName() << "\" "; stream << "tail=\"" << trans.getName() << "\" "; stream << "kind=\"OUTPUT\" "; - stream << "mult=\"" << trans.getOutputArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << outEntry.second << "\" "; stream << "/>" << std::endl; } } @@ -496,19 +484,19 @@ namespace storm { stream << space2 << "" << std::endl; } - uint_fast64_t i = 0; + uint64_t i = 0; // add arcs for immediate transitions for (const auto &trans : immediateTransitions) { // add input arcs - for (auto &placePtr : trans.getInputPlaces()) { + for (auto const& inEntry : trans.getInputPlaces()) { stream << space2 << "getName() << "\" "; + stream << "source=\"" << places.at(inEntry.first).getName() << "\" "; stream << "target=\"" << trans.getName() << "\" "; stream << ">" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "Default," << trans.getInputArcMultiplicity(*placePtr) << "" << std::endl; + stream << space4 << "Default," << inEntry.second << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; @@ -517,15 +505,15 @@ namespace storm { } // add inhibition arcs - for (auto &placePtr : trans.getInhibitionPlaces()) { + for (auto const& inhEntry : trans.getInhibitionPlaces()) { stream << space2 << "getName() << "\" "; + stream << "source=\"" << places.at(inhEntry.first).getName() << "\" "; stream << "target=\"" << trans.getName() << "\" "; stream << ">" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "Default," << trans.getInputArcMultiplicity(*placePtr) << "" << std::endl; + stream << space4 << "Default," << inhEntry.second << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; @@ -534,15 +522,15 @@ namespace storm { } // add output arcs - for (auto &placePtr : trans.getOutputPlaces()) { + for (auto const& outEntry : trans.getOutputPlaces()) { stream << space2 << "getName() << "\" "; + stream << "target=\"" << places.at(outEntry.first).getName() << "\" "; stream << ">" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "Default," << trans.getInputArcMultiplicity(*placePtr) << "" << std::endl; + stream << space4 << "Default," << outEntry.second << "" << 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 9a9a301b7..7ff2fdc2c 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -34,7 +34,7 @@ namespace storm { * * @return The number of places. */ - uint_fast64_t getNumberOfPlaces() const; + uint64_t getNumberOfPlaces() const; /*! * Returns the vector of timed transitions in this gspn. @@ -61,7 +61,7 @@ namespace storm { * @param map The Map determines the number of bits for each place. * @return The initial Marking */ - std::shared_ptr getInitialMarking(std::map& numberOfBits, uint_fast64_t const& numberOfTotalBits) const; + std::shared_ptr getInitialMarking(std::map& numberOfBits, uint64_t const& numberOfTotalBits) const; /*! * Returns the place with the corresponding id. @@ -156,6 +156,9 @@ namespace storm { bool testTransitions() const; + // name of the gspn + std::string name; + // set containing all places std::vector places; @@ -166,8 +169,6 @@ namespace storm { std::vector> timedTransitions; - // name of the gspn - std::string name; }; } } \ No newline at end of file diff --git a/src/storage/gspn/Transition.cpp b/src/storage/gspn/Transition.cpp index c9f2fb823..e2941aa0e 100644 --- a/src/storage/gspn/Transition.cpp +++ b/src/storage/gspn/Transition.cpp @@ -5,17 +5,13 @@ namespace storm { namespace gspn { - void Transition::setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) { - auto ptr = std::make_shared(place); - inputMultiplicities[ptr->getID()] = multiplicity; - inputPlaces.push_back(ptr); + void Transition::setInputArcMultiplicity(storm::gspn::Place const& place, uint64_t multiplicity) { + inputMultiplicities[place.getID()] = multiplicity; } bool Transition::removeInputArc(storm::gspn::Place const& place) { if (existsInputArc(place)) { - auto ptr = std::make_shared(place); - inputMultiplicities.erase(ptr->getID()); - inputPlaces.erase(std::find(inputPlaces.begin(), inputPlaces.end(), ptr)); + inputMultiplicities.erase(place.getID()); return true; } else { return false; @@ -23,21 +19,16 @@ namespace storm { } bool Transition::existsInputArc(storm::gspn::Place const& place) const { - auto ptr = std::make_shared(place); - return inputMultiplicities.end() != inputMultiplicities.find(ptr->getID()); + return inputMultiplicities.end() != inputMultiplicities.find(place.getID()); } - void Transition::setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) { - auto ptr = std::make_shared(place); - outputMultiplicities[ptr->getID()] = multiplicity; - outputPlaces.push_back(ptr); + void Transition::setOutputArcMultiplicity(storm::gspn::Place const& place, uint64_t multiplicity) { + outputMultiplicities[place.getID()] = multiplicity; } bool Transition::removeOutputArc(storm::gspn::Place const& place) { if (existsOutputArc(place)) { - auto ptr = std::make_shared(place); - outputMultiplicities.erase(ptr->getID()); - outputPlaces.erase(std::find(outputPlaces.begin(), outputPlaces.end(), ptr)); + outputMultiplicities.erase(place.getID()); return true; } else { return false; @@ -45,22 +36,17 @@ namespace storm { } bool Transition::existsOutputArc(storm::gspn::Place const& place) const { - auto ptr = std::make_shared(place); - return outputMultiplicities.end() != outputMultiplicities.find(ptr->getID()); + return outputMultiplicities.end() != outputMultiplicities.find(place.getID()); } - void Transition::setInhibitionArcMultiplicity(storm::gspn::Place const& place, - uint_fast64_t multiplicity) { - auto ptr = std::make_shared(place); - inhibitionMultiplicities[ptr->getID()] = multiplicity; - inhibitionPlaces.push_back(ptr); + void Transition::setInhibitionArcMultiplicity(storm::gspn::Place const& place, uint64_t multiplicity) { + + inhibitionMultiplicities[place.getID()] = multiplicity; } bool Transition::removeInhibitionArc(storm::gspn::Place const& place) { if (existsInhibitionArc(place)) { - auto ptr = std::make_shared(place); - inhibitionMultiplicities.erase(ptr->getID()); - inhibitionPlaces.erase(std::find(inhibitionPlaces.begin(), inhibitionPlaces.end(), ptr)); + inhibitionMultiplicities.erase(place.getID()); return true; } else { return false; @@ -68,8 +54,7 @@ namespace storm { } bool Transition::existsInhibitionArc(storm::gspn::Place const& place) const { - auto ptr = std::make_shared(place); - return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr->getID()); + return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(place.getID()); } bool Transition::isEnabled(storm::gspn::Marking const& marking) const { @@ -91,14 +76,6 @@ namespace storm { ++inhibitionIterator; } - for (auto &placePtr : getOutputPlaces()) { - if (placePtr->hasRestrictedCapacity()) { - if (marking.getNumberOfTokensAt(placePtr->getID()) + getOutputArcMultiplicity(*placePtr) > placePtr->getCapacity()) { - return false; - } - } - } - return true; } @@ -130,50 +107,47 @@ namespace storm { return this->name; } - const std::vector> &Transition::getInputPlaces() const { - return inputPlaces; + std::unordered_map const& Transition::getInputPlaces() const { + return inputMultiplicities; } - const std::vector> &Transition::getOutputPlaces() const { - return outputPlaces; + std::unordered_map const& Transition::getOutputPlaces() const { + return outputMultiplicities; } - const std::vector> &Transition::getInhibitionPlaces() const { - return inhibitionPlaces; + std::unordered_map const& Transition::getInhibitionPlaces() const { + return inhibitionMultiplicities; } - uint_fast64_t Transition::getInputArcMultiplicity(storm::gspn::Place const& place) const { + uint64_t Transition::getInputArcMultiplicity(storm::gspn::Place const& place) const { if (existsInputArc(place)) { - auto ptr = std::make_shared(place); - return inputMultiplicities.at(ptr->getID()); + return inputMultiplicities.at(place.getID()); } else { return 0; } } - uint_fast64_t Transition::getInhibitionArcMultiplicity(storm::gspn::Place const& place) const { + uint64_t Transition::getInhibitionArcMultiplicity(storm::gspn::Place const& place) const { if (existsInhibitionArc(place)) { - auto ptr = std::make_shared(place); - return inhibitionMultiplicities.at(ptr->getID()); + return inhibitionMultiplicities.at(place.getID()); } else { return 0; } } - uint_fast64_t Transition::getOutputArcMultiplicity(storm::gspn::Place const& place) const { + uint64_t Transition::getOutputArcMultiplicity(storm::gspn::Place const& place) const { if (existsOutputArc(place)) { - auto ptr = std::make_shared(place); - return outputMultiplicities.at(ptr->getID()); + return outputMultiplicities.at(place.getID()); } else { return 0; } } - void Transition::setPriority(uint_fast64_t const& priority) { + void Transition::setPriority(uint64_t const& priority) { this->priority = priority; } - uint_fast64_t Transition::getPriority() const { + uint64_t Transition::getPriority() const { return this->priority; } } diff --git a/src/storage/gspn/Transition.h b/src/storage/gspn/Transition.h index fb1247e0e..421d4b70e 100644 --- a/src/storage/gspn/Transition.h +++ b/src/storage/gspn/Transition.h @@ -1,7 +1,7 @@ -#ifndef STORM_STORAGE_GSPN_TRANSITION_H_ -#define STORM_STORAGE_GSPN_TRANSITION_H_ +#pragma once #include +#include #include #include "src/storage/gspn/Marking.h" #include "src/storage/gspn/Place.h" @@ -21,7 +21,7 @@ namespace storm { * @param place The place connected by an input arc. * @param multiplicity The multiplicity of the specified arc. */ - void setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity); + void setInputArcMultiplicity(storm::gspn::Place const& place, uint64_t multiplicity); /*! * Removes an input arc connected to a given place. @@ -47,7 +47,7 @@ namespace storm { * @param place The place connected by an output arc. * @param multiplicity The multiplicity of the specified arc. */ - void setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity); + void setOutputArcMultiplicity(storm::gspn::Place const& place, uint64_t multiplicity); /*! * Removes an output arc connected to a given place. @@ -73,7 +73,7 @@ namespace storm { * @param place The place connected by an inhibition arc. * @param multiplicity The multiplicity of the specified arc. */ - void setInhibitionArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity); + void setInhibitionArcMultiplicity(storm::gspn::Place const& place, uint64_t multiplicity); /*! * Removes an inhibition arc connected to a given place. @@ -120,23 +120,12 @@ namespace storm { */ std::string const& getName() const; - /*! - * Returns a list of places which are connected via a input arc. - * @return - */ - std::vector> const& getInputPlaces() const; - - /*! - * Returns a list of places which are connected via a output arc. - * @return - */ - std::vector> const& getOutputPlaces() const; - - /*! - * Returns a list of places which are connected via a inhibition arc. - * @return - */ - std::vector> const& getInhibitionPlaces() const; + + std::unordered_map const& getInputPlaces() const; + + std::unordered_map const& getOutputPlaces() const; + + std::unordered_map const& getInhibitionPlaces() const; /*! * Returns the corresponding multiplicity. @@ -144,7 +133,7 @@ namespace storm { * @param place connected to this transition by an input arc * @return cardinality or 0 if the arc does not exists */ - uint_fast64_t getInputArcMultiplicity(storm::gspn::Place const& place) const; + uint64_t getInputArcMultiplicity(storm::gspn::Place const& place) const; /*! * Returns the corresponding multiplicity. @@ -152,7 +141,7 @@ namespace storm { * @param place connected to this transition by an inhibition arc * @return cardinality or 0 if the arc does not exists */ - uint_fast64_t getInhibitionArcMultiplicity(storm::gspn::Place const& place) const; + uint64_t getInhibitionArcMultiplicity(storm::gspn::Place const& place) const; /*! * Returns the corresponding multiplicity. @@ -160,63 +149,43 @@ namespace storm { * @param place connected to this transition by an output arc * @return cardinality or 0 if the arc does not exists */ - uint_fast64_t getOutputArcMultiplicity(storm::gspn::Place const& place) const; + uint64_t getOutputArcMultiplicity(storm::gspn::Place const& place) const; /*! * Sets the priority of this transtion. * * @param priority The new priority. */ - void setPriority(uint_fast64_t const& priority); + void setPriority(uint64_t const& priority); /*! * Returns the priority of this transition. * * @return The priority. */ - uint_fast64_t getPriority() const; + uint64_t getPriority() const; - void setID(uint_fast64_t const& id) { + void setID(uint64_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()(uint_fast64_t const& lhs, uint_fast64_t const& rhs) const { - return lhs < rhs; - } - }; // maps place ids connected to this transition with an input arc to the corresponding multiplicity - std::map inputMultiplicities; + std::unordered_map inputMultiplicities; // maps place ids connected to this transition with an output arc to the corresponding multiplicities - std::map outputMultiplicities; + std::unordered_map outputMultiplicities; // maps place ids connected to this transition with an inhibition arc to the corresponding multiplicity - std::map inhibitionMultiplicities; + std::unordered_map inhibitionMultiplicities; // name of the transition std::string name; - // list of all places connected to this transition via an input arc - std::vector> inputPlaces; - - // list of all places connected to this transition via an output arc - std::vector> outputPlaces; - - // list of all places connected to this transition via an inhibition arc - std::vector> inhibitionPlaces; - // priority of this transition - uint_fast64_t priority = 0; + uint64_t priority = 0; - uint_fast64_t id; + uint64_t id; }; } } - -#endif //STORM_STORAGE_GSPN_TRANSITION_H_ \ No newline at end of file