Browse Source

refactor GspnBuilder

Former-commit-id: a399617611
tempestpy_adaptions
ThomasH 8 years ago
parent
commit
5fa7d3d399
  1. 13
      src/storage/gspn/GSPN.cpp
  2. 3
      src/storage/gspn/GSPN.h
  3. 32
      src/storage/gspn/GspnBuilder.cpp
  4. 21
      src/storage/gspn/GspnBuilder.h
  5. 8
      src/storage/gspn/Transition.h

13
src/storage/gspn/GSPN.cpp

@ -40,15 +40,24 @@ namespace storm {
return m;
}
std::pair<bool, storm::gspn::Place> GSPN::getPlace(std::string const& id) const {
std::pair<bool, storm::gspn::Place> GSPN::getPlace(uint_fast64_t const& id) const {
for (auto& place : places) {
if (id.compare(place.getName()) == 0) {
if (id == place.getID()) {
return std::make_pair<bool, storm::gspn::Place const&>(true, place);
}
}
return std::make_pair<bool, storm::gspn::Place>(false, storm::gspn::Place());
}
std::pair<bool, storm::gspn::Place> GSPN::getPlace(std::string const& id) const {
for (auto& place : places) {
if (id.compare(place.getName())) {
return std::make_pair<bool, storm::gspn::Place const&>(true, place);
}
}
return std::make_pair<bool, storm::gspn::Place>(false, storm::gspn::Place());
};
std::pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const> GSPN::getTimedTransition(std::string const& id) const {
for (auto& trans : timedTransitions) {
if (id.compare(trans->getName()) == 0) {

3
src/storage/gspn/GSPN.h

@ -83,8 +83,9 @@ namespace storm {
* If the first element is true, then the second element is the wanted place.
* If the first element is false, then the second element is not defined.
*/
std::pair<bool, storm::gspn::Place> getPlace(std::string const& id) const;
std::pair<bool, storm::gspn::Place> getPlace(uint_fast64_t const& id) const;
std::pair<bool, storm::gspn::Place> getPlace(std::string const& id) const;
/*!
* Returns the timed transition with the corresponding id.
*

32
src/storage/gspn/GspnBuilder.cpp

@ -7,37 +7,33 @@
namespace storm {
namespace gspn {
void GspnBuilder::addPlace(uint_fast64_t const& id, int_fast64_t const& capacity, uint_fast64_t const& initialTokens) {
addPlace(id, "place_" + std::to_string(id), capacity, initialTokens);
}
void GspnBuilder::addPlace(uint_fast64_t const& id, std::string const& name, int_fast64_t const& capacity, uint_fast64_t const& initialTokens) {
uint_fast64_t GspnBuilder::addPlace(int_fast64_t const& capacity, uint_fast64_t const& initialTokens) {
auto place = storm::gspn::Place();
place.setCapacity(capacity);
place.setID(id);
place.setName(name);
place.setID(nextStateID);
place.setNumberOfInitialTokens(initialTokens);
idToPlaceName.insert(std::pair<uint_fast64_t const, std::string const>(id, name));
gspn.addPlace(place);
return nextStateID++;
}
void GspnBuilder::addImmediateTransition(uint_fast64_t const& id, uint_fast64_t const& priority, double const& weight) {
uint_fast64_t GspnBuilder::addImmediateTransition(uint_fast64_t const& priority, double const& weight) {
auto trans = storm::gspn::ImmediateTransition<double>();
trans.setName(std::to_string(id));
trans.setName(std::to_string(nextTransitionID));
trans.setPriority(priority);
trans.setWeight(weight);
trans.setID(nextTransitionID);
gspn.addImmediateTransition(trans);
return nextTransitionID++;
}
void GspnBuilder::addTimedTransition(uint_fast64_t const &id, uint_fast64_t const &priority, double const &rate) {
uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate) {
auto trans = storm::gspn::TimedTransition<double>();
trans.setName(std::to_string(id));
trans.setName(std::to_string(nextTransitionID));
trans.setPriority(priority);
trans.setRate(rate);
trans.setID(nextTransitionID);
gspn.addTimedTransition(trans);
return nextTransitionID++;
}
void GspnBuilder::addInputArc(uint_fast64_t const &from, uint_fast64_t const &to,
@ -47,7 +43,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist.");
}
auto placePair = gspn.getPlace(idToPlaceName.at(from));
auto placePair = gspn.getPlace(from);
if (!std::get<0>(placePair)) {
STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist.");
}
@ -61,7 +57,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist.");
}
auto placePair = gspn.getPlace(idToPlaceName.at(from));
auto placePair = gspn.getPlace(from);
if (!std::get<0>(placePair)) {
STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist.");
}
@ -75,7 +71,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist.");
}
auto placePair = gspn.getPlace(idToPlaceName.at(to));
auto placePair = gspn.getPlace(to);
if (!std::get<0>(placePair)) {
STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist.");
}

21
src/storage/gspn/GspnBuilder.h

@ -11,15 +11,6 @@ namespace storm {
namespace gspn {
class GspnBuilder {
public:
/**
* Add a place to the gspn.
* @param id The id must be unique for the gspn.
* @param capacity The capacity is the limit of tokens in the place.
* A capacity of -1 indicates an unbounded place.
* @param initialTokens The number of inital tokens in the place.
*/
void addPlace(uint_fast64_t const& id, int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0);
/**
* Add a place to the gspn.
* @param id The id must be unique for the gspn.
@ -28,7 +19,7 @@ namespace storm {
* A capacity of -1 indicates an unbounded place.
* @param initialTokens The number of inital tokens in the place.
*/
void addPlace(uint_fast64_t const& id, std::string const& name, int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0);
uint_fast64_t addPlace(int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0);
/**
* Adds an immediate transition to the gspn.
@ -36,7 +27,7 @@ namespace storm {
* @param priority The priority for the transtion.
* @param weight The weight for the transition.
*/
void addImmediateTransition(uint_fast64_t const& id, uint_fast64_t const& priority = 0, double const& weight = 0);
uint_fast64_t addImmediateTransition(uint_fast64_t const& priority = 0, double const& weight = 0);
/**
* Adds an timed transition to the gspn.
@ -44,7 +35,7 @@ namespace storm {
* @param priority The priority for the transtion.
* @param weight The weight for the transition.
*/
void addTimedTransition(uint_fast64_t const &id, uint_fast64_t const &priority = 0, double const &rate = 0);
uint_fast64_t addTimedTransition(uint_fast64_t const &priority = 0, double const &rate = 0);
/**
* Adds an new input arc from a place to an transition.
@ -78,8 +69,10 @@ namespace storm {
private:
// gspn which is returned
storm::gspn::GSPN gspn;
// map from ids to names (for places)
std::map<uint_fast64_t const, std::string const> idToPlaceName;
// id for the next state which is added
uint_fast64_t nextStateID = 0;
// id for the next transition (timed or immediate) which is added
uint_fast64_t nextTransitionID = 0;
};
}
}

8
src/storage/gspn/Transition.h

@ -175,6 +175,10 @@ namespace storm {
* @return The priority.
*/
uint_fast64_t getPriority() const;
void setID(uint_fast64_t const& id) {
this->id = id;
}
private:
/*!
* Comparator which defines an total order on places.
@ -208,7 +212,9 @@ namespace storm {
std::vector<std::shared_ptr<storm::gspn::Place>> inhibitionPlaces;
// priority of this transition
uint_fast64_t priority;
uint_fast64_t priority = 0;
uint_fast64_t id;
};
}
}

Loading…
Cancel
Save