sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

refactoring gspn 

Former-commit-id: c7c4764901
main
ThomasH 9 years ago
parent
ba50772eeb
commit
bd057da743
5 changed files with 121 additions and 171 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 153
      src/storage/gspn/GSPN.cpp
  2. 2
      src/storage/gspn/Place.cpp
  3. 10
      src/storage/gspn/Place.h
  4. 69
      src/storage/gspn/Transition.cpp
  5. 58
      src/storage/gspn/Transition.h

153
src/storage/gspn/GSPN.cpp
View File

@ -100,56 +100,43 @@ namespace storm {
// print arcs // print arcs
for (auto& trans : this->getImmediateTransitions()) { 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; 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; outStream << "\"];" << std::endl;
++it;
} }
} }
for (auto& trans : this->getTimedTransitions()) { 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; 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; 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; outStream << "\"];" << std::endl;
++it;
} }
} }
@ -202,26 +189,26 @@ namespace storm {
bool result = true; bool result = true;
for (auto const& transition : this->getImmediateTransitions()) { 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") STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n")
result = false; result = false;
} }
if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) {
if (transition->getOutputPlaces().empty()) {
STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n") STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n")
result = false; result = false;
} }
} }
for (auto const& transition : this->getTimedTransitions()) { 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") STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n")
result = false; result = false;
} }
if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) {
if (transition->getOutputPlaces().empty()) {
STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n") STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n")
result = false; result = false;
} }
@ -229,82 +216,82 @@ namespace storm {
//test if places exists in the gspn //test if places exists in the gspn
for (auto const& transition : this->getImmediateTransitions()) { for (auto const& transition : this->getImmediateTransitions()) {
for (auto it = transition->getInputPlacesCBegin(); it != transition->getInputPlacesCEnd(); ++it) {
for (auto &placePtr : transition->getInputPlaces()) {
bool foundPlace = false; bool foundPlace = false;
for (auto const& place : places) { for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
if (place.getName() == placePtr->getName()) {
foundPlace = true; foundPlace = true;
} }
} }
if (!foundPlace) { 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; result = false;
} }
} }
for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) {
for (auto &placePtr : transition->getInhibitionPlaces()) {
bool foundPlace = false; bool foundPlace = false;
for (auto const& place : places) { for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
if (place.getName() == placePtr->getName()) {
foundPlace = true; foundPlace = true;
} }
} }
if (!foundPlace) { 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; result = false;
} }
} }
for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) {
for (auto &placePtr : transition->getOutputPlaces()) {
bool foundPlace = false; bool foundPlace = false;
for (auto const& place : places) { for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
if (place.getName() == placePtr->getName()) {
foundPlace = true; foundPlace = true;
} }
} }
if (!foundPlace) { 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; result = false;
} }
} }
} }
for (auto const& transition : this->getTimedTransitions()) { for (auto const& transition : this->getTimedTransitions()) {
for (auto it = transition->getInputPlacesCBegin(); it != transition->getInputPlacesCEnd(); ++it) {
for (auto &placePtr : transition->getInputPlaces()) {
bool foundPlace = false; bool foundPlace = false;
for (auto const& place : places) { for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
if (place.getName() == placePtr->getName()) {
foundPlace = true; foundPlace = true;
} }
} }
if (!foundPlace) { 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; result = false;
} }
} }
for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) {
for (auto &placePtr : transition->getInhibitionPlaces()) {
bool foundPlace = false; bool foundPlace = false;
for (auto const& place : places) { for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
if (place.getName() == placePtr->getName()) {
foundPlace = true; foundPlace = true;
} }
} }
if (!foundPlace) { 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; result = false;
} }
} }
for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) {
for (auto &placePtr : transition->getOutputPlaces()) {
bool foundPlace = false; bool foundPlace = false;
for (auto const& place : places) { for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
if (place.getName() == placePtr->getName()) {
foundPlace = true; foundPlace = true;
} }
} }
if (!foundPlace) { 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; result = false;
} }
} }
@ -354,54 +341,54 @@ namespace storm {
stream << space2 << "<edges>" << std::endl; stream << space2 << "<edges>" << std::endl;
for (auto& trans : timedTransitions) { for (auto& trans : timedTransitions) {
for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) {
for (auto &placePtr : trans->getInputPlaces()) {
stream << space3 << "<arc "; stream << space3 << "<arc ";
stream << "head=\"" << trans->getName() << "\" "; stream << "head=\"" << trans->getName() << "\" ";
stream << "tail=\"" << (*it)->getName() << "\" ";
stream << "tail=\"" << placePtr->getName() << "\" ";
stream << "kind=\"INPUT\" "; stream << "kind=\"INPUT\" ";
stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" ";
stream << "mult=\"" << trans->getInputArcMultiplicity(*placePtr) << "\" ";
stream << "/>" << std::endl; stream << "/>" << std::endl;
} }
for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) {
for (auto &placePtr : trans->getInhibitionPlaces()) {
stream << space3 << "<arc "; stream << space3 << "<arc ";
stream << "head=\"" << trans->getName() << "\" "; stream << "head=\"" << trans->getName() << "\" ";
stream << "tail=\"" << (*it)->getName() << "\" ";
stream << "tail=\"" << placePtr->getName() << "\" ";
stream << "kind=\"INHIBITOR\" "; stream << "kind=\"INHIBITOR\" ";
stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" ";
stream << "mult=\"" << trans->getInhibitionArcMultiplicity(*placePtr) << "\" ";
stream << "/>" << std::endl; stream << "/>" << std::endl;
} }
for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) {
for (auto &placePtr : trans->getOutputPlaces()) {
stream << space3 << "<arc "; stream << space3 << "<arc ";
stream << "head=\"" << (*it)->getName() << "\" ";
stream << "head=\"" << placePtr->getName() << "\" ";
stream << "tail=\"" << trans->getName() << "\" "; stream << "tail=\"" << trans->getName() << "\" ";
stream << "kind=\"OUTPUT\" "; stream << "kind=\"OUTPUT\" ";
stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" ";
stream << "mult=\"" << trans->getOutputArcMultiplicity(*placePtr) << "\" ";
stream << "/>" << std::endl; stream << "/>" << std::endl;
} }
} }
for (auto& trans : immediateTransitions) { for (auto& trans : immediateTransitions) {
for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) {
for (auto &placePtr : trans->getInputPlaces()) {
stream << space3 << "<arc "; stream << space3 << "<arc ";
stream << "head=\"" << trans->getName() << "\" "; stream << "head=\"" << trans->getName() << "\" ";
stream << "tail=\"" << (*it)->getName() << "\" ";
stream << "tail=\"" << placePtr->getName() << "\" ";
stream << "kind=\"INPUT\" "; stream << "kind=\"INPUT\" ";
stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" ";
stream << "mult=\"" << trans->getInputArcMultiplicity(*placePtr) << "\" ";
stream << "/>" << std::endl; stream << "/>" << std::endl;
} }
for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) {
for (auto &placePtr : trans->getInhibitionPlaces()) {
stream << space3 << "<arc "; stream << space3 << "<arc ";
stream << "head=\"" << trans->getName() << "\" "; stream << "head=\"" << trans->getName() << "\" ";
stream << "tail=\"" << (*it)->getName() << "\" ";
stream << "tail=\"" << placePtr->getName() << "\" ";
stream << "kind=\"INHIBITOR\" "; stream << "kind=\"INHIBITOR\" ";
stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" ";
stream << "mult=\"" << trans->getInhibitionArcMultiplicity(*placePtr) << "\" ";
stream << "/>" << std::endl; stream << "/>" << std::endl;
} }
for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) {
for (auto &placePtr : trans->getOutputPlaces()) {
stream << space3 << "<arc "; stream << space3 << "<arc ";
stream << "head=\"" << (*it)->getName() << "\" ";
stream << "head=\"" << placePtr->getName() << "\" ";
stream << "tail=\"" << trans->getName() << "\" "; stream << "tail=\"" << trans->getName() << "\" ";
stream << "kind=\"OUTPUT\" "; stream << "kind=\"OUTPUT\" ";
stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" ";
stream << "mult=\"" << trans->getOutputArcMultiplicity(*placePtr) << "\" ";
stream << "/>" << std::endl; stream << "/>" << std::endl;
} }
} }
@ -456,15 +443,15 @@ namespace storm {
// add arcs for immediate transitions // add arcs for immediate transitions
for (const auto &trans : immediateTransitions) { for (const auto &trans : immediateTransitions) {
// add input arcs // add input arcs
for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) {
for (auto &placePtr : trans->getInputPlaces()) {
stream << space2 << "<arc "; stream << space2 << "<arc ";
stream << "id=\"arc" << i++ << "\" "; stream << "id=\"arc" << i++ << "\" ";
stream << "source=\"" << (*it)->getName() << "\" ";
stream << "source=\"" << placePtr->getName() << "\" ";
stream << "target=\"" << trans->getName() << "\" "; stream << "target=\"" << trans->getName() << "\" ";
stream << ">" << std::endl; stream << ">" << std::endl;
stream << space3 << "<inscription>" << std::endl; stream << space3 << "<inscription>" << std::endl;
stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(**it) << "</value>" << std::endl;
stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(*placePtr) << "</value>" << std::endl;
stream << space3 << "</inscription>" << std::endl; stream << space3 << "</inscription>" << std::endl;
stream << space3 << "<type value=\"normal\" />" << std::endl; stream << space3 << "<type value=\"normal\" />" << std::endl;
@ -473,15 +460,15 @@ namespace storm {
} }
// add inhibition arcs // add inhibition arcs
for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) {
for (auto &placePtr : trans->getInhibitionPlaces()) {
stream << space2 << "<arc "; stream << space2 << "<arc ";
stream << "id=\"arc" << i++ << "\" "; stream << "id=\"arc" << i++ << "\" ";
stream << "source=\"" << (*it)->getName() << "\" ";
stream << "source=\"" << placePtr->getName() << "\" ";
stream << "target=\"" << trans->getName() << "\" "; stream << "target=\"" << trans->getName() << "\" ";
stream << ">" << std::endl; stream << ">" << std::endl;
stream << space3 << "<inscription>" << std::endl; stream << space3 << "<inscription>" << std::endl;
stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(**it) << "</value>" << std::endl;
stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(*placePtr) << "</value>" << std::endl;
stream << space3 << "</inscription>" << std::endl; stream << space3 << "</inscription>" << std::endl;
stream << space3 << "<type value=\"inhibition\" />" << std::endl; stream << space3 << "<type value=\"inhibition\" />" << std::endl;
@ -490,15 +477,15 @@ namespace storm {
} }
// add output arcs // add output arcs
for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) {
for (auto &placePtr : trans->getOutputPlaces()) {
stream << space2 << "<arc "; stream << space2 << "<arc ";
stream << "id=\"arc" << i++ << "\" "; stream << "id=\"arc" << i++ << "\" ";
stream << "source=\"" << trans->getName() << "\" "; stream << "source=\"" << trans->getName() << "\" ";
stream << "target=\"" << (*it)->getName() << "\" ";
stream << "target=\"" << placePtr->getName() << "\" ";
stream << ">" << std::endl; stream << ">" << std::endl;
stream << space3 << "<inscription>" << std::endl; stream << space3 << "<inscription>" << std::endl;
stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(**it) << "</value>" << std::endl;
stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(*placePtr) << "</value>" << std::endl;
stream << space3 << "</inscription>" << std::endl; stream << space3 << "</inscription>" << std::endl;
stream << space3 << "<type value=\"normal\" />" << std::endl; stream << space3 << "<type value=\"normal\" />" << std::endl;

2
src/storage/gspn/Place.cpp
View File

@ -30,7 +30,7 @@ namespace storm {
} }
void Place::setCapacity(int_fast64_t const& capacity) { 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; this->capacity = capacity;
} }

10
src/storage/gspn/Place.h
View File

@ -11,7 +11,9 @@ namespace storm {
class Place { class Place {
public: 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. * @param name The new name for the place.
*/ */
@ -68,10 +70,10 @@ namespace storm {
int_fast64_t getCapacity() const; int_fast64_t getCapacity() const;
private: private:
// contains the number of initial tokens of this place // 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) // 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 // name which is used in pnml file
std::string name; std::string name;
@ -79,7 +81,7 @@ namespace storm {
// capacity of this place // capacity of this place
// -1 indicates that the capacity is not set // -1 indicates that the capacity is not set
// other non-negative values represents the capacity // other non-negative values represents the capacity
int_fast64_t capacity;
int_fast64_t capacity = -1;
}; };
} }
} }

69
src/storage/gspn/Transition.cpp
View File

@ -7,14 +7,14 @@ namespace storm {
void Transition::setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) { void Transition::setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
inputMultiplicities[ptr] = multiplicity;
inputMultiplicities[ptr->getID()] = multiplicity;
inputPlaces.push_back(ptr); inputPlaces.push_back(ptr);
} }
bool Transition::removeInputArc(storm::gspn::Place const& place) { bool Transition::removeInputArc(storm::gspn::Place const& place) {
if (existsInputArc(place)) { if (existsInputArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
inputMultiplicities.erase(ptr);
inputMultiplicities.erase(ptr->getID());
inputPlaces.erase(std::find(inputPlaces.begin(), inputPlaces.end(), ptr)); inputPlaces.erase(std::find(inputPlaces.begin(), inputPlaces.end(), ptr));
return true; return true;
} else { } else {
@ -24,19 +24,19 @@ namespace storm {
bool Transition::existsInputArc(storm::gspn::Place const& place) const { bool Transition::existsInputArc(storm::gspn::Place const& place) const {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(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) { void Transition::setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
outputMultiplicities[ptr] = multiplicity;
outputMultiplicities[ptr->getID()] = multiplicity;
outputPlaces.push_back(ptr); outputPlaces.push_back(ptr);
} }
bool Transition::removeOutputArc(storm::gspn::Place const& place) { bool Transition::removeOutputArc(storm::gspn::Place const& place) {
if (existsOutputArc(place)) { if (existsOutputArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
outputMultiplicities.erase(ptr);
outputMultiplicities.erase(ptr->getID());
outputPlaces.erase(std::find(outputPlaces.begin(), outputPlaces.end(), ptr)); outputPlaces.erase(std::find(outputPlaces.begin(), outputPlaces.end(), ptr));
return true; return true;
} else { } else {
@ -46,20 +46,20 @@ namespace storm {
bool Transition::existsOutputArc(storm::gspn::Place const& place) const { bool Transition::existsOutputArc(storm::gspn::Place const& place) const {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
return outputMultiplicities.end() != outputMultiplicities.find(ptr);
return outputMultiplicities.end() != outputMultiplicities.find(ptr->getID());
} }
void Transition::setInhibitionArcMultiplicity(storm::gspn::Place const& place, void Transition::setInhibitionArcMultiplicity(storm::gspn::Place const& place,
uint_fast64_t multiplicity) { uint_fast64_t multiplicity) {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
inhibitionMultiplicities[ptr] = multiplicity;
inhibitionMultiplicities[ptr->getID()] = multiplicity;
inhibitionPlaces.push_back(ptr); inhibitionPlaces.push_back(ptr);
} }
bool Transition::removeInhibitionArc(storm::gspn::Place const& place) { bool Transition::removeInhibitionArc(storm::gspn::Place const& place) {
if (existsInhibitionArc(place)) { if (existsInhibitionArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
inhibitionMultiplicities.erase(ptr);
inhibitionMultiplicities.erase(ptr->getID());
inhibitionPlaces.erase(std::find(inhibitionPlaces.begin(), inhibitionPlaces.end(), ptr)); inhibitionPlaces.erase(std::find(inhibitionPlaces.begin(), inhibitionPlaces.end(), ptr));
return true; return true;
} else { } else {
@ -69,13 +69,13 @@ namespace storm {
bool Transition::existsInhibitionArc(storm::gspn::Place const& place) const { bool Transition::existsInhibitionArc(storm::gspn::Place const& place) const {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr);
return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr->getID());
} }
bool Transition::isEnabled(storm::gspn::Marking const& marking) const { bool Transition::isEnabled(storm::gspn::Marking const& marking) const {
auto inputIterator = inputMultiplicities.cbegin(); auto inputIterator = inputMultiplicities.cbegin();
while (inputIterator != inputMultiplicities.cend()) { while (inputIterator != inputMultiplicities.cend()) {
if (marking.getNumberOfTokensAt(inputIterator->first->getID()) < inputIterator->second) {
if (marking.getNumberOfTokensAt(inputIterator->first) < inputIterator->second) {
return false; return false;
} }
@ -84,22 +84,19 @@ namespace storm {
auto inhibitionIterator = inhibitionMultiplicities.cbegin(); auto inhibitionIterator = inhibitionMultiplicities.cbegin();
while (inhibitionIterator != inhibitionMultiplicities.cend()) { while (inhibitionIterator != inhibitionMultiplicities.cend()) {
if (marking.getNumberOfTokensAt(inhibitionIterator->first->getID()) >= inhibitionIterator->second) {
if (marking.getNumberOfTokensAt(inhibitionIterator->first) >= inhibitionIterator->second) {
return false; return false;
} }
++inhibitionIterator; ++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; return false;
} }
} }
++outputIterator;
} }
return true; return true;
@ -110,15 +107,15 @@ namespace storm {
auto inputIterator = inputMultiplicities.cbegin(); auto inputIterator = inputMultiplicities.cbegin();
while (inputIterator != inputMultiplicities.cend()) { 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; ++inputIterator;
} }
auto outputIterator = outputMultiplicities.cbegin(); auto outputIterator = outputMultiplicities.cbegin();
while (outputIterator != outputMultiplicities.cend()) { 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; ++outputIterator;
} }
@ -133,34 +130,22 @@ namespace storm {
return this->name; return this->name;
} }
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInputPlacesCBegin() const {
return this->inputPlaces.cbegin();
}
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInputPlacesCEnd() const {
return this->inputPlaces.cend();
}
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getOutputPlacesCBegin() const {
return this->outputPlaces.cbegin();
}
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getOutputPlacesCEnd() const {
return this->outputPlaces.cend();
const std::vector<std::shared_ptr<storm::gspn::Place>> &Transition::getInputPlaces() const {
return inputPlaces;
} }
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInhibitionPlacesCBegin() const {
return this->inhibitionPlaces.cbegin();
const std::vector<std::shared_ptr<storm::gspn::Place>> &Transition::getOutputPlaces() const {
return outputPlaces;
} }
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInhibitionPlacesCEnd() const {
return this->inhibitionPlaces.cend();
const std::vector<std::shared_ptr<storm::gspn::Place>> &Transition::getInhibitionPlaces() const {
return inhibitionPlaces;
} }
uint_fast64_t Transition::getInputArcMultiplicity(storm::gspn::Place const& place) const { uint_fast64_t Transition::getInputArcMultiplicity(storm::gspn::Place const& place) const {
if (existsInputArc(place)) { if (existsInputArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
return inputMultiplicities.at(ptr);
return inputMultiplicities.at(ptr->getID());
} else { } else {
return 0; return 0;
} }
@ -169,7 +154,7 @@ namespace storm {
uint_fast64_t Transition::getInhibitionArcMultiplicity(storm::gspn::Place const& place) const { uint_fast64_t Transition::getInhibitionArcMultiplicity(storm::gspn::Place const& place) const {
if (existsInhibitionArc(place)) { if (existsInhibitionArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
return inhibitionMultiplicities.at(ptr);
return inhibitionMultiplicities.at(ptr->getID());
} else { } else {
return 0; return 0;
} }
@ -178,7 +163,7 @@ namespace storm {
uint_fast64_t Transition::getOutputArcMultiplicity(storm::gspn::Place const& place) const { uint_fast64_t Transition::getOutputArcMultiplicity(storm::gspn::Place const& place) const {
if (existsOutputArc(place)) { if (existsOutputArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place); auto ptr = std::make_shared<storm::gspn::Place>(place);
return outputMultiplicities.at(ptr);
return outputMultiplicities.at(ptr->getID());
} else { } else {
return 0; return 0;
} }

58
src/storage/gspn/Transition.h
View File

@ -121,46 +121,22 @@ namespace storm {
std::string const& getName() const; 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<std::shared_ptr<storm::gspn::Place>>::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<std::shared_ptr<storm::gspn::Place>>::const_iterator getInputPlacesCEnd() const;
const std::vector<std::shared_ptr<storm::gspn::Place>> &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<std::shared_ptr<storm::gspn::Place>>::const_iterator getOutputPlacesCBegin() const;
const std::vector<std::shared_ptr<storm::gspn::Place>> &getOutputPlaces() const;
/*! /*!
* Returns a constant iterator to the end of a vector which contains all output places.
*
* @return Returns iterator.
*/
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getOutputPlacesCEnd() const;
/*!
* Returns a constant iterator to the begin of a vector which contains all inhibition places.
*
* @return Returns iterator.
*/
std::vector<std::shared_ptr<storm::gspn::Place>>::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<std::shared_ptr<storm::gspn::Place>>::const_iterator getInhibitionPlacesCEnd() const;
const std::vector<std::shared_ptr<storm::gspn::Place>> &getInhibitionPlaces() const;
/*! /*!
* Returns the corresponding multiplicity. * 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. * A place is less than another place if the id is less than the id from the other place.
*/ */
struct PlaceComparator { struct PlaceComparator {
bool operator()(std::shared_ptr<storm::gspn::Place> const& lhs, std::shared_ptr<storm::gspn::Place> 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<std::shared_ptr<storm::gspn::Place>, 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<uint_fast64_t, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inputMultiplicities;
// maps places connected to this transition with an output arc to the corresponding multiplicities
std::map<std::shared_ptr<storm::gspn::Place>, 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<uint_fast64_t, uint_fast64_t, storm::gspn::Transition::PlaceComparator> outputMultiplicities;
// maps places connected to this transition with an inhibition arc to the corresponding multiplicity
std::map<std::shared_ptr<storm::gspn::Place>, 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<uint_fast64_t, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inhibitionMultiplicities;
// name of the transition // name of the transition
std::string name; std::string name;

Write Preview
Loading…
Cancel
Save