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

cleaning gspns 

Former-commit-id: 6da157d915 [formerly d83f1ab30f]
Former-commit-id: b0753441c3
tempestpy_adaptions
sjunges 8 years ago
parent
1fd89f3922
commit
3dfe4640e9
5 changed files with 232 additions and 300 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 50
      src/builder/JaniGSPNBuilder.h
  2. 318
      src/storage/gspn/GSPN.cpp
  3. 9
      src/storage/gspn/GSPN.h
  4. 80
      src/storage/gspn/Transition.cpp
  5. 75
      src/storage/gspn/Transition.h

50
src/builder/JaniGSPNBuilder.h
View File

@ -63,15 +63,15 @@ namespace storm {
for (auto const& trans : gspn.getImmediateTransitions()) {
if (ignoreWeights || trans.noWeightAttached()) {
std::vector<storm::jani::Assignment> 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<storm::jani::Assignment> 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<storm::jani::Assignment> 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);

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

@ -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<storm::gspn::Marking> GSPN::getInitialMarking(std::map<uint_fast64_t, uint_fast64_t>& numberOfBits, uint_fast64_t const& numberOfTotalBits) const {
std::shared_ptr<storm::gspn::Marking> GSPN::getInitialMarking(std::map<uint64_t, uint64_t>& numberOfBits, uint64_t const& numberOfTotalBits) const {
auto m = std::make_shared<storm::gspn::Marking>(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<std::string> namesOfPlaces;
std::vector<uint_fast64_t> idsOfPlaces;
std::vector<uint64_t> 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 << "<edges>" << std::endl;
for (auto& trans : timedTransitions) {
for (auto &placePtr : trans.getInputPlaces()) {
for (auto const& inEntry : trans.getInputPlaces()) {
stream << space3 << "<arc ";
stream << "head=\"" << trans.getName() << "\" ";
stream << "tail=\"" << placePtr->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 << "<arc ";
stream << "head=\"" << trans.getName() << "\" ";
stream << "tail=\"" << placePtr->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 << "<arc ";
stream << "head=\"" << placePtr->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 << "<arc ";
stream << "head=\"" << trans.getName() << "\" ";
stream << "tail=\"" << placePtr->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 << "<arc ";
stream << "head=\"" << trans.getName() << "\" ";
stream << "tail=\"" << placePtr->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 << "<arc ";
stream << "head=\"" << placePtr->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 << "</transition>" << 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 << "<arc ";
stream << "id=\"arc" << i++ << "\" ";
stream << "source=\"" << placePtr->getName() << "\" ";
stream << "source=\"" << places.at(inEntry.first).getName() << "\" ";
stream << "target=\"" << trans.getName() << "\" ";
stream << ">" << std::endl;
stream << space3 << "<inscription>" << std::endl;
stream << space4 << "<value>Default," << trans.getInputArcMultiplicity(*placePtr) << "</value>" << std::endl;
stream << space4 << "<value>Default," << inEntry.second << "</value>" << std::endl;
stream << space3 << "</inscription>" << std::endl;
stream << space3 << "<type value=\"normal\" />" << std::endl;
@ -517,15 +505,15 @@ namespace storm {
}
// add inhibition arcs
for (auto &placePtr : trans.getInhibitionPlaces()) {
for (auto const& inhEntry : trans.getInhibitionPlaces()) {
stream << space2 << "<arc ";
stream << "id=\"arc" << i++ << "\" ";
stream << "source=\"" << placePtr->getName() << "\" ";
stream << "source=\"" << places.at(inhEntry.first).getName() << "\" ";
stream << "target=\"" << trans.getName() << "\" ";
stream << ">" << std::endl;
stream << space3 << "<inscription>" << std::endl;
stream << space4 << "<value>Default," << trans.getInputArcMultiplicity(*placePtr) << "</value>" << std::endl;
stream << space4 << "<value>Default," << inhEntry.second << "</value>" << std::endl;
stream << space3 << "</inscription>" << std::endl;
stream << space3 << "<type value=\"inhibition\" />" << std::endl;
@ -534,15 +522,15 @@ namespace storm {
}
// add output arcs
for (auto &placePtr : trans.getOutputPlaces()) {
for (auto const& outEntry : trans.getOutputPlaces()) {
stream << space2 << "<arc ";
stream << "id=\"arc" << i++ << "\" ";
stream << "source=\"" << trans.getName() << "\" ";
stream << "target=\"" << placePtr->getName() << "\" ";
stream << "target=\"" << places.at(outEntry.first).getName() << "\" ";
stream << ">" << std::endl;
stream << space3 << "<inscription>" << std::endl;
stream << space4 << "<value>Default," << trans.getInputArcMultiplicity(*placePtr) << "</value>" << std::endl;
stream << space4 << "<value>Default," << outEntry.second << "</value>" << std::endl;
stream << space3 << "</inscription>" << std::endl;
stream << space3 << "<type value=\"normal\" />" << std::endl;

9
src/storage/gspn/GSPN.h
View File

@ -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<storm::gspn::Marking> getInitialMarking(std::map<uint_fast64_t, uint_fast64_t>& numberOfBits, uint_fast64_t const& numberOfTotalBits) const;
std::shared_ptr<storm::gspn::Marking> getInitialMarking(std::map<uint64_t, uint64_t>& 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<storm::gspn::Place> places;
@ -166,8 +169,6 @@ namespace storm {
std::vector<storm::gspn::TimedTransition<RateType>> timedTransitions;
// name of the gspn
std::string name;
};
}
}

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

@ -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<storm::gspn::Place>(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<storm::gspn::Place>(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<storm::gspn::Place>(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<storm::gspn::Place>(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<storm::gspn::Place>(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<storm::gspn::Place>(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<storm::gspn::Place>(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<storm::gspn::Place>(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<storm::gspn::Place>(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<std::shared_ptr<storm::gspn::Place>> &Transition::getInputPlaces() const {
return inputPlaces;
std::unordered_map<uint64_t, uint64_t> const& Transition::getInputPlaces() const {
return inputMultiplicities;
}
const std::vector<std::shared_ptr<storm::gspn::Place>> &Transition::getOutputPlaces() const {
return outputPlaces;
std::unordered_map<uint64_t, uint64_t> const& Transition::getOutputPlaces() const {
return outputMultiplicities;
}
const std::vector<std::shared_ptr<storm::gspn::Place>> &Transition::getInhibitionPlaces() const {
return inhibitionPlaces;
std::unordered_map<uint64_t, uint64_t> 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<storm::gspn::Place>(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<storm::gspn::Place>(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<storm::gspn::Place>(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;
}
}

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

@ -1,7 +1,7 @@
#ifndef STORM_STORAGE_GSPN_TRANSITION_H_
#define STORM_STORAGE_GSPN_TRANSITION_H_
#pragma once
#include <map>
#include <unordered_map>
#include <vector>
#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<std::shared_ptr<storm::gspn::Place>> const& getInputPlaces() const;
/*!
* Returns a list of places which are connected via a output arc.
* @return
*/
std::vector<std::shared_ptr<storm::gspn::Place>> const& getOutputPlaces() const;
/*!
* Returns a list of places which are connected via a inhibition arc.
* @return
*/
std::vector<std::shared_ptr<storm::gspn::Place>> const& getInhibitionPlaces() const;
std::unordered_map<uint64_t, uint64_t> const& getInputPlaces() const;
std::unordered_map<uint64_t, uint64_t> const& getOutputPlaces() const;
std::unordered_map<uint64_t, uint64_t> 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<uint_fast64_t, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inputMultiplicities;
std::unordered_map<uint64_t, uint64_t> inputMultiplicities;
// 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;
std::unordered_map<uint64_t, uint64_t> outputMultiplicities;
// 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;
std::unordered_map<uint64_t, uint64_t> inhibitionMultiplicities;
// name of the transition
std::string name;
// list of all places connected to this transition via an input arc
std::vector<std::shared_ptr<storm::gspn::Place>> inputPlaces;
// list of all places connected to this transition via an output arc
std::vector<std::shared_ptr<storm::gspn::Place>> outputPlaces;
// list of all places connected to this transition via an inhibition arc
std::vector<std::shared_ptr<storm::gspn::Place>> 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_
Write Preview
Loading…
Cancel
Save