diff --git a/src/builder/ExplicitGspnModelBuilder.cpp b/src/builder/ExplicitGspnModelBuilder.cpp new file mode 100644 index 000000000..98f76ad1d --- /dev/null +++ b/src/builder/ExplicitGspnModelBuilder.cpp @@ -0,0 +1,249 @@ +#include "src/builder/ExplicitGspnModelBuilder.h" + +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace builder { + + template + storm::models::sparse::MarkovAutomaton ExplicitGspnModelBuilder::translateGspn(storm::gspn::GSPN const& gspn) { + // set the given gspn and compute the limits of the net + this->gspn = gspn; + computeCapacities(gspn); + + // markings maps markings to their corresponding rowgroups (indices) + markings = storm::storage::BitVectorHashMap(numberOfTotalBits, 100); + builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, true); + + // add initial marking to todo list + auto bitvector = gspn.getInitialMarking(numberOfBits, numberOfTotalBits)->getBitVector(); + findOrAddBitvectorToMarkings(*bitvector); + currentRowIndex = 0; + + // vector marking markovian states (vector contains an 1 if the state is markovian) + storm::storage::BitVector markovianStates(0); + + // vector containing the exit rates for the markovian states + std::vector exitRates; + + + while (!todo.empty()) { + // take next element from the todo list + auto currentBitvector = todo.front(); + todo.pop_front(); + auto currentMarking = storm::gspn::Marking(gspn.getNumberOfPlaces(), numberOfBits, *currentBitvector); + + // increment list of states by one + markovianStates.resize(markovianStates.size() + 1, 0); + + // create new row group for the current marking + builder.newRowGroup(markings.getValue(*currentBitvector)); + + std::cout << "work on: " << *currentBitvector << std::endl; + + auto enabledImmediateTransitions = getEnabledImmediateTransition(currentMarking); + if (!enabledImmediateTransitions.empty()) { + markovianStates.set(currentRowIndex, 0); + exitRates.push_back(0); + + auto partitions = partitonEnabledImmediateTransitions(currentMarking, enabledImmediateTransitions); + addRowForPartitions(partitions, currentMarking); + } else { + + auto enabledTimedTransitions = getEnabledTimedTransition(currentMarking); + if (!enabledTimedTransitions.empty()) { + markovianStates.set(currentRowIndex, 1); + + auto accRate = getAccumulatedRate(enabledTimedTransitions); + std::cout << "\t\tacc. rate: " << accRate << std::endl; + exitRates.push_back(accRate); + + addRowForTimedTransitions(enabledTimedTransitions, currentMarking, accRate); + } else { + markovianStates.set(currentRowIndex, 0); + } + } + ++currentRowIndex; + } + + auto matrix = builder.build(); + const storm::models::sparse::StateLabeling labeling; // TODO + + return storm::models::sparse::MarkovAutomaton(matrix, labeling, markovianStates, exitRates); + } + + template + void ExplicitGspnModelBuilder::addRowForPartitions(std::vector>>> const& partitions, storm::gspn::Marking const& currentMarking) { + for (auto& partition : partitions) { + std::cout << "\tnew partition:" << std::endl; + auto accWeight = getAccumulatedWeight(partition); + std::cout << "\t\tacc. weight: " << accWeight << std::endl; + + std::map::cmpByIndex> weights; + for (auto& trans : partition) { + std::cout << "\t\ttransname: " << trans->getName() << std::endl; + auto newMarking = trans->fire(currentMarking); + std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << std::endl; + + findOrAddBitvectorToMarkings(*newMarking.getBitVector()); + + auto it = weights.find(markings.getValue(*newMarking.getBitVector())); + double currentWeight = 0; + if (it != weights.end()) { + currentWeight = weights.at(markings.getValue(*newMarking.getBitVector())); + } + currentWeight += trans->getWeight() / accWeight; + weights[markings.getValue(*newMarking.getBitVector())] = currentWeight; + } + + addValuesToBuilder(weights); + } + } + + template + void ExplicitGspnModelBuilder::addRowForTimedTransitions(std::vector>> const& enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate) { + std::map::cmpByIndex> rates; + for (auto& trans : enabledTimedTransitions) { + std::cout << "\t\ttransname: " << trans->getName() << std::endl; + auto newMarking = trans->fire(currentMarking); + std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << std::endl; + + findOrAddBitvectorToMarkings(*newMarking.getBitVector()); + + auto it = rates.find(markings.getValue(*newMarking.getBitVector())); + double currentWeightRate = 0; + if (it != rates.end()) { + currentWeightRate = rates.at(markings.getValue(*newMarking.getBitVector())); + } + currentWeightRate += trans->getRate() / accRate; + rates[markings.getValue(*newMarking.getBitVector())] = currentWeightRate; + + } + + addValuesToBuilder(rates); + } + + template + void ExplicitGspnModelBuilder::addValuesToBuilder(std::map::cmpByIndex> const& values) { + for (auto& it : values) { + std::cout << "\t\tadd value \"" << it.second << "\" to " << getBitvector(it.first) << std::endl; + builder.addNextValue(currentRowIndex, it.first, it.second); + } + } + + template + std::vector>>> ExplicitGspnModelBuilder::partitonEnabledImmediateTransitions( + storm::gspn::Marking const& marking, + std::vector>> const& enabledImmediateTransitions) { + decltype(partitonEnabledImmediateTransitions(marking, enabledImmediateTransitions)) result; + + std::vector>> weightedTransitions; + + for (auto& trans : enabledImmediateTransitions) { + if (trans->getWeight() == 0) { + decltype(weightedTransitions) singleton; + singleton.push_back(trans); + result.push_back(singleton); + } else { + weightedTransitions.push_back(trans); + } + } + + if (weightedTransitions.size() != 0) { + result.push_back(weightedTransitions); + } + + return result; + } + + template + double ExplicitGspnModelBuilder::getAccumulatedWeight(std::vector>> const& vector) const { + double result = 0; + + for (auto &trans : vector) { + result += trans->getWeight(); + } + + return result; + } + + template + void ExplicitGspnModelBuilder::computeCapacities(storm::gspn::GSPN const& gspn) { + uint_fast64_t sum = 0; + for (auto& place : gspn.getPlaces()) {//TODO + numberOfBits[place.getID()] = 1; + sum += numberOfBits[place.getID()]; + } + + // compute next multiple of 64 + uint_fast64_t rem = sum % 64; + numberOfTotalBits = sum + 64 - rem; + } + + template + std::vector>> ExplicitGspnModelBuilder::getEnabledTimedTransition( + storm::gspn::Marking const& marking) { + std::vector>>result; + + for (auto& trans_ptr : gspn.getTimedTransitions()) { + if (trans_ptr->isEnabled(marking)) { + result.push_back(trans_ptr); + } + } + + return result; + } + + template + std::vector>> ExplicitGspnModelBuilder::getEnabledImmediateTransition( + storm::gspn::Marking const& marking) { + std::vector>>result; + + for (auto& trans_ptr : gspn.getImmediateTransitions()) { + if (trans_ptr->isEnabled(marking)) { + result.push_back(trans_ptr); + } + } + + return result; + } + + template + double ExplicitGspnModelBuilder::getAccumulatedRate(std::vector>> const& vector) { + double result = 0; + for (auto trans_ptr : vector) { + result += trans_ptr->getRate(); + } + + return result; + } + + template + storm::storage::BitVector ExplicitGspnModelBuilder::getBitvector(uint_fast64_t const& index) { + for (auto it = markings.begin(); it != markings.end(); ++it) { + if (std::get<1>(*it) == index) { + return std::get<0>(*it); + } + } + return storm::storage::BitVector(); + } + + template + uint_fast64_t ExplicitGspnModelBuilder::findOrAddBitvectorToMarkings(storm::storage::BitVector const &bitvector) { + auto index = markings.findOrAdd(bitvector, nextRowGroupIndex); + + if (index == nextRowGroupIndex) { + // bitvector was not already in the map + ++nextRowGroupIndex; + // bitvector was also never in the todo list + todo.push_back(std::make_shared(bitvector)); + } + return index; + } + + template class ExplicitGspnModelBuilder; + } +} diff --git a/src/builder/ExplicitGspnModelBuilder.h b/src/builder/ExplicitGspnModelBuilder.h index 3d8159c1d..1b7fe4d8e 100644 --- a/src/builder/ExplicitGspnModelBuilder.h +++ b/src/builder/ExplicitGspnModelBuilder.h @@ -1,11 +1,161 @@ -#ifndef STORM_EXPLICITGSPNMODELBUILDER_H -#define STORM_EXPLICITGSPNMODELBUILDER_H +#ifndef STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ +#define STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ +#include "src/models/sparse/MarkovAutomaton.h" +#include "src/models/sparse/StandardRewardModel.h" +#include "src/storage/Bitvector.h" +#include "src/storage/BitvectorHashMap.h" +#include "src/storage/gspn/GSPN.h" +#include "src/storage/gspn/ImmediateTransition.h" +#include "src/storage/gspn/TimedTransition.h" namespace storm { namespace builder { - // Takes a GSPN, builds an MA. + + /*! + * This class provides the facilities for building an markov automaton. + */ + template + class ExplicitGspnModelBuilder { + public: + + /*! + * Builds an MarkovAutomaton from the given GSPN. + * + * @param gspn The gspn whose semantic is covered by the MarkovAutomaton + * @return The resulting MarkovAutomaton + */ + storm::models::sparse::MarkovAutomaton translateGspn(storm::gspn::GSPN const& gspn); + private: + + /*! + * Add for each partition a new row in the probability matrix. + * + * @param partitions The partitioned immediate transitions. + * @param currentMarking The current marking which is considered at the moment. + */ + void addRowForPartitions(std::vector>>> const& partitions, storm::gspn::Marking const& currentMarking); + + + /*! + * Add row for a markovian state. + * + * @param enabledTimedTransitions List of enabled timed transitions. + * @param currentMarking The current marking which is considered at the moment. + * @param accRate The sum of all rates of the enabled timed transisitons + */ + void addRowForTimedTransitions(std::vector>> const& enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate); + + /*! + * Struct for comparing unsigned integer for maps + */ + struct cmpByIndex { + bool operator()(const uint_fast64_t &a, const uint_fast64_t &b) const { + return a < b; + } + }; + + /*! + * This method insert the values from a map into the matrix + * + * @param values The values which are inserted + */ + void addValuesToBuilder(std::map::cmpByIndex> const& values); + + + /*! + * This method partitions all enabled immediate transitions w.r.t. a marking. + * All enabled weighted immediate transitions are in one vector. Between these transitions + * is chosen probabilistically by the weights. + * + * All other enabled non-weighted immediate transitions are in an singleton vector. + * Between different vectors is chosen non-deterministically. + * + * @param marking The current marking which is considered. + * @param enabledImmediateTransistions A vector of enabled immediate transitions. + * @return The vector of vectors which is described above. + */ + std::vector>>> partitonEnabledImmediateTransitions(storm::gspn::Marking const& marking, std::vector>> const& enabledImmediateTransitions); + + /*! + * Computes the accumulated weight of immediate transisions which are stored in a list. + * + * @param vector List of immediate transisitions. + */ + double getAccumulatedWeight(std::vector>> const& vector) const; + + /*! + * Compute the upper bound for the number of tokens in each place. + * Also computes the number of bits which are used to store a marking. + * + * @param gspn The corresponding gspn. + */ + void computeCapacities(storm::gspn::GSPN const& gspn); + + /*! + * Returns the vector of enabled timed transition. + * + * @param marking The current marking which is considered. + * @return The vector of enabled timed transitions. + */ + std::vector>> getEnabledTimedTransition( + storm::gspn::Marking const& marking); + + /*! + * Returns the vector of active immediate transition + * + * @param marking The current marking which is considered. + * @return The vector of enabled immediate transitions. + */ + std::vector>> getEnabledImmediateTransition( + storm::gspn::Marking const& marking); + + /*! + * Computes the accumulated rate of a vector of timed transitions. + * + * @param vector The vector of timed transitions. + * @return The accumulated rate. + */ + double getAccumulatedRate(std::vector>> const& vector); + + // is only needed for debugging purposes + // since markings is injective, we can determine the bitvector + storm::storage::BitVector getBitvector(uint_fast64_t const& index); + + /*! + * Adds the bitvector to the marking-map. + * If the bitvector corresponds to a new marking the bitvector is added to the todo list. + * + * @return The rowGroup index for the bitvector. + */ + uint_fast64_t findOrAddBitvectorToMarkings(storm::storage::BitVector const& bitvector); + + + // contains the number of bits which are used the store the number of tokens at each place + std::map numberOfBits; + + // contains the number of bits used to create markings + uint_fast64_t numberOfTotalBits; + + // maps bitvectors (markings w.r.t. the capacity) to their rowgroup + storm::storage::BitVectorHashMap markings = storm::storage::BitVectorHashMap(64, 1); + + // a list of markings for which the outgoing edges need to be computed + std::deque> todo; + + //the gspn which is transformed + storm::gspn::GSPN gspn; + + // the next index for a new rowgroup + uint_fast64_t nextRowGroupIndex = 0; + + // builder object which is used to create the probability matrix + storm::storage::SparseMatrixBuilder builder; + + // contains the current row index during the computation + uint_fast64_t currentRowIndex; + }; } } -#endif //STORM_EXPLICITGSPNMODELBUILDER_H +#endif //STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ diff --git a/src/parser/GspnParser.cpp b/src/parser/GspnParser.cpp index fe0feac4f..18042b237 100644 --- a/src/parser/GspnParser.cpp +++ b/src/parser/GspnParser.cpp @@ -1,399 +1,478 @@ -#include -#include -#include -#include #include "src/parser/GspnParser.h" -storm::gspn::GSPN storm::parser::GspnParser::parse(const std::string &filename) { - // initialize xerces - try { - xercesc::XMLPlatformUtils::Initialize(); - } - catch (const xercesc::XMLException& toCatch) { - // TODO do something - } +#include +#include +#include +#include "src/exceptions/UnexpectedException.h" +#include "src/storage/gspn/Place.h" +#include "src/storage/gspn/ImmediateTransition.h" +#include "src/utility/macros.h" +namespace storm { + namespace parser { + storm::gspn::GSPN const& GspnParser::parse(std::string const& filename) { + // initialize parser + newNode = 0; + gspn = storm::gspn::GSPN(); - auto parser = new xercesc::XercesDOMParser(); - parser->setValidationScheme(xercesc::XercesDOMParser::Val_Always); - parser->setDoNamespaces(false); - parser->setDoSchema(false); - parser->setLoadExternalDTD(false); - parser->setIncludeIgnorableWhitespace(false); - //parser->loadGrammar(source, type); + // initialize xercesc + try { + xercesc::XMLPlatformUtils::Initialize(); + } + catch (xercesc::XMLException const& toCatch) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to initialize xercesc\n"); + } - auto errHandler = (xercesc::ErrorHandler*) new xercesc::HandlerBase(); - parser->setErrorHandler(errHandler); + auto parser = new xercesc::XercesDOMParser(); + parser->setValidationScheme(xercesc::XercesDOMParser::Val_Always); + parser->setDoNamespaces(false); + parser->setDoSchema(false); + parser->setLoadExternalDTD(false); + parser->setIncludeIgnorableWhitespace(false); - try { - parser->parse(filename.c_str()); - } - catch (const xercesc::XMLException& toCatch) { - auto message = xercesc::XMLString::transcode(toCatch.getMessage()); - std::cout << "Exception message is: \n" - << message << "\n"; - xercesc::XMLString::release(&message); - } - catch (const xercesc::DOMException& toCatch) { - auto message = xercesc::XMLString::transcode(toCatch.msg); - std::cout << "Exception message is: \n" - << message << "\n"; - xercesc::XMLString::release(&message); - } - catch (...) { - std::cout << "Unexpected Exception \n" ; - } + auto errHandler = (xercesc::ErrorHandler*) new xercesc::HandlerBase(); + parser->setErrorHandler(errHandler); + // parse file + try { + parser->parse(filename.c_str()); + } + catch (xercesc::XMLException const& toCatch) { + auto message = xercesc::XMLString::transcode(toCatch.getMessage()); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, message); + xercesc::XMLString::release(&message); + } + catch (const xercesc::DOMException& toCatch) { + auto message = xercesc::XMLString::transcode(toCatch.msg); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, message); + xercesc::XMLString::release(&message); + } + catch (...) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to parse pnml file.\n"); + } - parser->getDocument()->normalizeDocument(); - xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement(); - if (getName(elementRoot).compare("pnml") != 0) { - std::cout << "expected: pnml" << std::endl; - std::cout << "found: " << XMLtoString(elementRoot->getTagName()) << std::endl; - // TODO error - } - parsePNML(elementRoot); + // build gspn by traversing the DOM object + parser->getDocument()->normalizeDocument(); + xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement(); + STORM_LOG_THROW(getName(elementRoot).compare("pnml") == 0, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n"); + traversePnmlElement(elementRoot); - delete parser; - delete errHandler; + // clean up + delete parser; + delete errHandler; + xercesc::XMLPlatformUtils::Terminate(); + return gspn; + } - // clean up - xercesc::XMLPlatformUtils::Terminate(); + void GspnParser::traversePnmlElement(xercesc::DOMElement const* const element) { + // traverse attributes + for (uint_fast64_t i = 0; i < element->getAttributes()->getLength(); ++i) { + auto attr = element->getAttributes()->item(i); + auto name = getName(attr); - return gspn; -} + STORM_PRINT_AND_LOG("unknown attribute (node=pnml): " + name + "\n"); + } -std::string storm::parser::GspnParser::XMLtoString(const XMLCh *xmlString) { - char* tmp = xercesc::XMLString::transcode(xmlString); - auto result = std::string(tmp); - delete tmp; - return result; -} + // traverse children + for (uint_fast64_t i = 0; i < element->getChildNodes()->getLength(); ++i) { + auto child = element->getChildNodes()->item(i); + auto name = getName(child); -void storm::parser::GspnParser::parsePNML(xercesc::DOMElement *element) { - for (uint64_t i = 0; i < element->getChildNodes()->getLength(); ++i) { - auto child = element->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("net") == 0) { - parseNet(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - std::cout << "pnml" << std::endl; - std::cout << "unkown child: " << name << std::endl; + if (name.compare("net") == 0) { + traverseNetOrPage(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + STORM_PRINT_AND_LOG("unknown child (node=pnml): " + name + "\n"); + } + } } - } -} -void storm::parser::GspnParser::parseNet(xercesc::DOMNode* node) { - for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("page") == 0) { - parsePage(child); - } else if (name.compare("place") == 0) { - parsePlace(child); - } else if (name.compare("transition") == 0) { - parseTransition(child); - } else if (name.compare("arc") == 0) { - parseArc(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("name") == 0 || - name.compare("token") == 0) { - // ignore these tags - } else { - std::cout << "net" << std::endl; - std::cout << "unkown child: " << name << std::endl; - } - } -} + void GspnParser::traverseNetOrPage(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); -void storm::parser::GspnParser::parsePage(xercesc::DOMNode *node) { - for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("place") == 0) { - parsePlace(child); - } else if (name.compare("transition") == 0) { - parseTransition(child); - } else if (name.compare("arc") == 0) { - parseArc(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - std::cout << "page" << std::endl; - std::cout << "unkown child: " << name << std::endl; - } - } -} + if (name.compare("id") == 0) { + gspn.setName(XMLtoString(attr->getNodeValue())); + } else { + STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } -void storm::parser::GspnParser::parsePlace(xercesc::DOMNode *node) { - uint64_t place; - for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - if (name.compare("id") == 0) { - place = addNewPlace(XMLtoString(attr->getNodeValue())); - } else { - std::cout << "place" << std::endl; - std::cout << "unkown attr.: " << name << std::endl; - } - } - - for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("initialMarking") == 0) { - auto tokens = parseInitialMarking(child); - gspn.setNumberOfPlaces(gspn.getNumberOfPlaces()+1); - gspn.setInitialTokens(place, tokens); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("name") == 0 || - name.compare("graphics") == 0) { - // ignore these tags - } else { - std::cout << "place" << std::endl; - std::cout << "unkown child: " << name << std::endl; - } - } -} + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); -void storm::parser::GspnParser::parseTransition(xercesc::DOMNode *node) { - bool timed = false; - std::string rate, id; - - for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - if (name.compare("id") == 0) { - id = XMLtoString(attr->getNodeValue()); - } else { - std::cout << "transition" << std::endl; - std::cout << "unkown attr.: " << name << std::endl; + if (name.compare("place") == 0) { + traversePlace(child); + } else if (name.compare("transition") == 0) { + traverseTransition(child); + } else if (name.compare("arc") == 0) { + traverseArc(child); + } else if (name.compare("page") == 0) { + // Some pnml files have a child named page. + // The page node has the same children like the net node (e.g., place, transition, arc) + traverseNetOrPage(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } } - } - for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("rate") == 0) { - rate = parseRate(child); - } else if (name.compare("timed") == 0) { - timed = parseTimed(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("graphics") == 0 || - name.compare("name") == 0 || - name.compare("orientation") == 0) { - // ignore these tags - } else { - std::cout << "transition" << std::endl; - std::cout << "unkown child: " << name << std::endl; - } - } + void GspnParser::traversePlace(xercesc::DOMNode const* const node) { + std::string placeName; + // the first entry is false if the corresponding information was not found in the pnml file + std::pair numberOfInitialTokens(false, defaultNumberOfInitialTokens); + std::pair capacity(false, defaultCapacity); - if (timed) { - auto transition = std::make_shared>(); - transition->setRate(std::stoull(rate)); - gspn.addTimedTransition(transition); - this->stringToTransition[id] = transition; - } else { - auto transition = std::make_shared>(); - transition->setWeight(std::stoull(rate)); - gspn.addImmediateTransition(transition); - this->stringToTransition[id] = transition; - } -} + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); -void storm::parser::GspnParser::parseArc(xercesc::DOMNode *node) { - std::string source, target, type; - uint64_t cardinality; - - for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - if (name.compare("source") == 0) { - source = XMLtoString(attr->getNodeValue()); - } else if (name.compare("target") == 0) { - target = XMLtoString(attr->getNodeValue()); - } else if (name.compare("id") == 0) { - // ignore these tags - } else { - std::cout << "arc" << std::endl; - std::cout << "unkown attr.: " << name << std::endl; - } - } + if (name.compare("id") == 0) { + placeName = XMLtoString(attr->getNodeValue()); + } else { + STORM_PRINT_AND_LOG("unknown attribute (node=place): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + + if (name.compare("initialMarking") == 0) { + numberOfInitialTokens.first = true; + numberOfInitialTokens.second = traverseInitialMarking(child); + } else if(name.compare("capacity") == 0) { + capacity.first = true; + capacity.second = traverseCapacity(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("name") == 0 || + name.compare("graphics") == 0) { + // ignore these tags + } else { + STORM_PRINT_AND_LOG("unknown child (node=place): " + name + "\n"); + } + } - for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("type") == 0) { - type = parseType(child); - } else if(name.compare("inscription") == 0) { - cardinality = parseCapacity(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("graphics") == 0 || - name.compare("arcpath") == 0) { - // ignore these tags - } else { - std::cout << "arc" << std::endl; - std::cout << "unkown child: " << name << std::endl; + // build place and add it to the gspn + storm::gspn::Place place; + place.setName(placeName); + if (!numberOfInitialTokens.first) { + STORM_PRINT_AND_LOG("unknown numberOfInitialTokens (place=" + placeName + ")\n"); + } + place.setNumberOfInitialTokens(numberOfInitialTokens.second); + if (!capacity.first) { + STORM_PRINT_AND_LOG("unknown capacity (place=" + placeName + ")\n"); + } + place.setCapacity(capacity.second); + place.setID(newNode); + ++newNode; + gspn.addPlace(place); } - } - //determine if it is an outgoing or incoming arc - { - auto it1 = stringToState.find(source); - auto it2 = stringToTransition.find(target); - if (it1 != stringToState.end() && it2 != stringToTransition.end()) { - // incoming arc - if (type.compare("normal") == 0) { - auto transition = stringToTransition[target]; - transition->setInputArcCardinality(stringToState[source], cardinality); + + void GspnParser::traverseTransition(xercesc::DOMNode const* const node) { + // the first entry is false if the corresponding information was not found in the pnml file + std::pair timed(false, defaultTransitionType); + std::pair value(false, defaultTransitionValue); + std::string id; + + // parse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + + if (name.compare("id") == 0) { + id = XMLtoString(attr->getNodeValue()); + } else { + STORM_PRINT_AND_LOG("unknown attribute (node=transition): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + + if (name.compare("rate") == 0) { + value.first =true; + value.second = traverseTransitionValue(child); + } else if (name.compare("timed") == 0) { + timed.first = true; + timed.second = traverseTransitionType(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("graphics") == 0 || + name.compare("name") == 0 || + name.compare("orientation") == 0) { + // ignore these tags + } else { + STORM_PRINT_AND_LOG("unknown child (node=transition): " + name + "\n"); + } + } + + // build transition and add it to the gspn + if (!timed.first) { + STORM_PRINT_AND_LOG("unknown transition type (transition=" + id + ")\n"); + } + + if (timed.second) { + storm::gspn::TimedTransition transition; + if (!value.first) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown transition rate (transition=" + id + ")\n"); + } + transition.setRate(std::stod(value.second)); + transition.setName(id); + gspn.addTimedTransition(transition); } else { - std::cout << "arc" << std::endl; - std::cout << "unkown type: " << type << std::endl; + storm::gspn::ImmediateTransition transition; + if (!value.first) { + STORM_PRINT_AND_LOG("unknown transition weight (transition=" + id + ")\n"); + } + transition.setWeight(std::stod(value.second)); + transition.setName(id); + gspn.addImmediateTransition(transition); } - return; } - } - { - auto it1 = stringToTransition.find(source); - auto it2 = stringToState.find(target); - if (it1 != stringToTransition.end() && it2 != stringToState.end()) { - // outgoing arc - if (type.compare("normal") == 0) { - auto transition = stringToTransition[source]; - transition->setOutputArcCardinality(stringToState[target], cardinality); - } else { - std::cout << "arc" << std::endl; - std::cout << "unkown type: " << type << std::endl; + + void GspnParser::traverseArc(xercesc::DOMNode const* const node) { + // the first entry is false if the corresponding information was not found in the pnml file + std::pair source(false, ""); + std::pair target(false, ""); + std::pair type(false, defaultArcType); + std::pair multiplicity(false, defaultMultiplicity); + std::string id; + + // parse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + + if (name.compare("source") == 0) { + source.first = true; + source.second = XMLtoString(attr->getNodeValue()); + } else if (name.compare("target") == 0) { + target.first = true; + target.second = XMLtoString(attr->getNodeValue()); + } else if (name.compare("id") == 0) { + id = XMLtoString(attr->getNodeValue()); + } else { + STORM_PRINT_AND_LOG("unknown attribute (node=arc): " + name + "\n"); + } + } + + // parse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("type") == 0) { + type.first = true; + type.second = traverseArcType(child); + } else if(name.compare("inscription") == 0) { + multiplicity.first = true; + multiplicity.second = traverseMultiplicity(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("graphics") == 0 || + name.compare("arcpath") == 0 || + name.compare("tagged") == 0) { + // ignore these tags + } else { + STORM_PRINT_AND_LOG("unknown child (node=arc): " + name + "\n"); + } + } + + // check if all necessary information where stored in the pnml file + if (!source.first) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc source (arc=" + id + ")\n"); + } + if (!target.first) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc target (arc=" + id + ")\n"); } - return; + if (!multiplicity.first) { + STORM_PRINT_AND_LOG("unknown multiplicity (node=arc): " + id + "\n"); + } + + //determine if it is an outgoing or incoming arc + { + auto place = gspn.getPlace(source.second); + auto trans = gspn.getTransition(target.second); + if (true == place.first && true == trans.first) { + if (!type.first) { + STORM_PRINT_AND_LOG("unknown arc type (arc=" + id + ")\n"); + } + + // incoming arc + if (type.second.compare("normal") == 0) { + trans.second->setInputArcMultiplicity(place.second, multiplicity.second); + } else if (type.second.compare("inhibition") == 0) { + trans.second->setInhibitionArcMultiplicity(place.second, multiplicity.second); + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "unknown arc type (arc=" + id + ")\n"); + } + return; + } + } + { + auto trans = gspn.getTransition(source.second); + auto place = gspn.getPlace(target.second); + if (true == place.first && true == trans.first) { + // outgoing arc + trans.second->setOutputArcMultiplicity(place.second, multiplicity.second); + return; + } + } + + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc source or target (arc=" + id + ")\n"); } - } - // TODO add error message - std::cout << "found an arc with no correpsonding transition" << std::endl; -} -std::string storm::parser::GspnParser::getName(xercesc::DOMNode *node) { - switch (node->getNodeType()) { - case xercesc::DOMNode::NodeType::ELEMENT_NODE: { - auto elementNode = (xercesc::DOMElement *) node; - return XMLtoString(elementNode->getTagName()); + std::string GspnParser::getName(xercesc::DOMNode *node) { + switch (node->getNodeType()) { + case xercesc::DOMNode::NodeType::ELEMENT_NODE: { + auto elementNode = (xercesc::DOMElement *) node; + return XMLtoString(elementNode->getTagName()); + } + case xercesc::DOMNode::NodeType::TEXT_NODE: { + return XMLtoString(node->getNodeValue()); + } + case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: { + return XMLtoString(node->getNodeName()); + } + default: { + STORM_PRINT_AND_LOG("unknown node type \n"); + return ""; + } + } } - case xercesc::DOMNode::NodeType::TEXT_NODE: { - return XMLtoString(node->getNodeValue()); + + uint_fast64_t GspnParser::traverseInitialMarking(xercesc::DOMNode const* const node) { + uint_fast64_t result = defaultNumberOfInitialTokens; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("text") == 0) { + result = std::stoull(getName(child->getFirstChild())); + } else if (name.compare("value") == 0) { + auto value = getName(child->getFirstChild()); + value = value.substr(std::string("Default,").length()); + result = std::stoull(value); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("graphics") == 0) { + // ignore these tags + } else { + STORM_PRINT_AND_LOG("unknown child (node=initialMarking): " + name + "\n"); + } + } + return result; } - case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: { - return XMLtoString(node->getNodeName()); + + int_fast64_t GspnParser::traverseCapacity(xercesc::DOMNode const* const node) { + int_fast64_t result= defaultCapacity; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("value") == 0) { + auto value = getName(child->getFirstChild()); + if (value.find("Default,") == 0) { + value = value.substr(std::string("Default,").length()); + } + result = std::stoull(value); + } else if (name.compare("graphics") == 0) { + // ignore these nodes + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + STORM_PRINT_AND_LOG("unknown child (node=capacity): " + name + "\n"); + } + } + return result; } - default: { - std::cout << "unknown NodeType: " << node->getNodeType() << std::endl; - return ""; + + uint_fast64_t GspnParser::traverseMultiplicity(xercesc::DOMNode const* const node) { + uint_fast64_t result = defaultMultiplicity; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("value") == 0) { + auto value = getName(child->getFirstChild()); + if (value.find("Default,") == 0) { + value = value.substr(std::string("Default,").length()); + } + result = std::stoull(value); + } else if (name.compare("graphics") == 0) { + // ignore these nodes + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + STORM_PRINT_AND_LOG("unknown child (node=inscription): " + name + "\n"); + } + } + return result; } - } -} -uint64_t storm::parser::GspnParser::addNewPlace(std::string id) { - auto place = newNode; - ++newNode; - stringToState[id] = place;// TODO check whether the id is already in the map - return place; -} -uint64_t storm::parser::GspnParser::parseInitialMarking(xercesc::DOMNode *node) { - uint64_t result= 0; - for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("text") == 0) { - result = std::stoull(getName(child->getFirstChild())); - } else if (name.compare("value") == 0) { - auto value = getName(child->getFirstChild()); - value = value.substr(std::string("Default,").length()); - result = std::stoull(value); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("graphics") == 0) { - // ignore these tags - } else { - std::cout << "initialMarking" << std::endl; - std::cout << "unkown child: " << name << std::endl; + std::string GspnParser::traverseTransitionValue(xercesc::DOMNode const* const node) { + std::string result = defaultTransitionValue; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("value") == 0) { + result = getName(child->getFirstChild()); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + STORM_PRINT_AND_LOG("unknown child (node=rate): " + name + "\n"); + } + } + return result; } - } - return result; -} -std::string storm::parser::GspnParser::parseRate(xercesc::DOMNode *node) { - std::string result = ""; - for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("value") == 0) { - result = getName(child->getFirstChild()); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - std::cout << "rate" << std::endl; - std::cout << "unkown child: " << name << std::endl; + bool GspnParser::traverseTransitionType(xercesc::DOMNode const* const node) { + bool result; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = getName(child); + if (name.compare("value") == 0) { + result = getName(child->getFirstChild()).compare("true") == 0 ? true : false; + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + STORM_PRINT_AND_LOG("unknown child (node=timed): " + name + "\n"); + } + } + return result; } - } - return result; -} -bool storm::parser::GspnParser::parseTimed(xercesc::DOMNode *node) { - bool result; - for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("value") == 0) { - result = getName(child->getFirstChild()).compare("true") ? true : false; - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - std::cout << "timed" << std::endl; - std::cout << "unkown child: " << name << std::endl; + std::string GspnParser::traverseArcType(xercesc::DOMNode const* const node) { + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = getName(attr); + if (name.compare("value") == 0) { + return XMLtoString(attr->getNodeValue()); + } else { + STORM_PRINT_AND_LOG("unknown child (node=type): " + name + "\n"); + } + } + return defaultArcType; } - } - return result; -} -std::string storm::parser::GspnParser::parseType(xercesc::DOMNode *node) { - for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - if (name.compare("value") == 0) { - return XMLtoString(attr->getNodeValue()); - } else { - std::cout << "type" << std::endl; - std::cout << "unkown attr.: " << name << std::endl; + std::string GspnParser::XMLtoString(const XMLCh *xmlString) { + char* tmp = xercesc::XMLString::transcode(xmlString); + auto result = std::string(tmp); + delete tmp; + return result; } } - return ""; } -uint64_t storm::parser::GspnParser::parseCapacity(xercesc::DOMNode *node) { - uint64_t result= 0; - for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("value") == 0) { - auto value = getName(child->getFirstChild()); - value = value.substr(std::string("Default,").length()); - result = std::stoull(value); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("graphics") == 0) { - // ignore these tags - } else { - std::cout << "capacity" << std::endl; - std::cout << "unkown child: " << name << std::endl; - } - } - return result; -} diff --git a/src/parser/GspnParser.h b/src/parser/GspnParser.h index 23758704a..d910d405a 100644 --- a/src/parser/GspnParser.h +++ b/src/parser/GspnParser.h @@ -1,134 +1,155 @@ -#ifndef STORM_GSPNPARSER_H -#define STORM_GSPNPARSER_H +#ifndef STORM_PARSER_GSPNPARSER_H_ +#define STORM_PARSER_GSPNPARSER_H_ -#include #include + #include -#include -#include #include -#include + #include "src/storage/gspn/GSPN.h" namespace storm { namespace parser { - // Parses a GSPN in xml format + + /* Parses a pnml-file to a gspn. + IMPORTANT: The names of places, transitions and arcs must differ from each other. + */ class GspnParser { public: - /*! - * Parses the given file into the GSPN storage class assuming it complies with the PNML. - * - * @param filename The name of the file to parse - * @return The resulting GSPN. - */ - storm::gspn::GSPN parse(std::string const& filename); /*! - * Transforms the given XML String to a normal string. + * Parses the given file into the GSPN. * - * @param xmlString The given String in the XML format - * @return The corresponding standard string. + * @param filename The name of the file to parse. + * @return The resulting GSPN. */ - static std::string XMLtoString(const XMLCh* xmlString); + storm::gspn::GSPN const& parse(std::string const& filename); private: - // maps the original name of the state to its numerical representation - std::map stringToState; - - // maps the transition id to a pointer to the transition - std::map> stringToTransition; - - // the constructed gspn - storm::gspn::GSPN gspn; - - // has the new id for a new node - uint64_t newNode; /*! - * Parses the root element. + * Traverse the root element. * - * @param element The root element. + * @param element The root element of the DOM object. */ - void parsePNML(xercesc::DOMElement* element); + void traversePnmlElement(xercesc::DOMElement const* const element); /*! - * Parses a net node. + * Traverse a net or page node. * - * @param node The net node. + * @param node The net or page node. */ - void parseNet(xercesc::DOMNode* node); - - /*! - * Parses a page node. - * - * @param node The page node. -a */ - void parsePage(xercesc::DOMNode* node); + void traverseNetOrPage(xercesc::DOMNode const* const node); /*! - * Parses a place node. + * Traverse a place node. * * @param node The place node. */ - void parsePlace(xercesc::DOMNode* node); + void traversePlace(xercesc::DOMNode const* const node); /*! - * Parses a transition node. + * Traverse a transition node. * * @param node The transition node. */ - void parseTransition(xercesc::DOMNode* node); + void traverseTransition(xercesc::DOMNode const* const node); /*! - * Parses an arc node. + * Traverse an arc node. * * @param node The arc node. */ - void parseArc(xercesc::DOMNode* node); + void traverseArc(xercesc::DOMNode const* const node); /*! - * Parses an initial marking node . + * Traverse an initial marking node. * * @param node the initial marking node. - * @return The number of tokens. + * @return The number of initial tokens. */ - uint64_t parseInitialMarking(xercesc::DOMNode* node); + uint_fast64_t traverseInitialMarking(xercesc::DOMNode const* const node); /*! - * Adds a new entry in the mapping from string to places. + * Traverse a capacity node. * - * @param id The string id for the new place - * @return The new place. + * @param node The capacity node. + * @return The capacity for the place. */ - uint64_t addNewPlace(std::string id); + int_fast64_t traverseCapacity(xercesc::DOMNode const* const node); /*! - * Gives the name of the current node. - * @param node Current node. - * @return The name. + * Traverse a inscription node. + * + * @param node The inscription node. + * @return The multiplicty for the arc. */ - std::string getName(xercesc::DOMNode* node); + uint_fast64_t traverseMultiplicity(xercesc::DOMNode const* const node); /*! - * Parses a rate node. + * Traverse a rate node. + * + * @param node The rate node. + * @return The rate or weight of the transition. */ - std::string parseRate(xercesc::DOMNode* node); + std::string traverseTransitionValue(xercesc::DOMNode const* const node); /*! - * Parse a timed node. + * Traverse a timed node. + * + * @param node The timed node. + * @return False if the tranisition is immediate */ - bool parseTimed(xercesc::DOMNode* node); + bool traverseTransitionType(xercesc::DOMNode const* const node); /*! - * Parse a type node. + * Traverse a type node. + * + * @param node The type node. + * @return Returns a string with the arc type. */ - std::string parseType(xercesc::DOMNode* node); + std::string traverseArcType(xercesc::DOMNode const* const node); /*! - * Parse a capacity node. + * Gives the name of the current node. + * + * @param node The node. + * @return The name of the node. */ - uint64_t parseCapacity(xercesc::DOMNode* node); + std::string getName(xercesc::DOMNode* node); + + /*! + * Transforms the given XML String to a std::string. + * + * @param xmlString The given String in the XML format + * @return The corresponding std::string. + */ + static std::string XMLtoString(const XMLCh* xmlString); + + // the constructed gspn + storm::gspn::GSPN gspn; + + // contains the id for a new node + uint_fast64_t newNode = 0; + + // default value for initial tokens + uint_fast64_t defaultNumberOfInitialTokens = 0; + + // default value for capacities + int_fast64_t defaultCapacity = -1; + + // default value for the transition type (false == immediate transition) + bool defaultTransitionType = false; + + // default value for the transition weight or rate + std::string defaultTransitionValue = "1"; // TODO set to 0 + + // default value for the arc type + std::string defaultArcType = "normal"; + + // default multiplicity for arcs + uint_fast64_t defaultMultiplicity = 1; }; } } -#endif //STORM_GSPNPARSER_H +#endif //STORM_PARSER_GSPNPARSER_H_ diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index cea9aa313..0ea8deeb9 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -1,27 +1,168 @@ #include "src/storage/gspn/GSPN.h" -storm::gspn::GSPN::GSPN() : initialMarking(0, 0) { -} +namespace storm { + namespace gspn { + void GSPN::addImmediateTransition(storm::gspn::ImmediateTransition const& transition) { + this->immediateTransitions.push_back(std::make_shared>(transition)); + } -void storm::gspn::GSPN::setInitialTokens(uint64_t place, uint64_t token) { - if (initialMarking.getMaxNumberOfTokens() < token) { - initialMarking.setMaxNumberOfTokens(token); - } - initialMarking.setNumberOfTokensAt(place, token); -} + void GSPN::addTimedTransition(storm::gspn::TimedTransition const& transition) { + this->timedTransitions.push_back(std::make_shared>(transition)); + } -void storm::gspn::GSPN::setNumberOfPlaces(uint64_t number) { - initialMarking.setNumberOfPlaces(number); -} + void GSPN::addPlace(Place const& place) { + //TODO check whether the name or id is already used by an place + this->places.push_back(place); + } -uint64_t storm::gspn::GSPN::getNumberOfPlaces() { - return initialMarking.getNumberOfPlaces(); -} + uint_fast64_t GSPN::getNumberOfPlaces() const { + return places.size(); + } -void storm::gspn::GSPN::addImmediateTransition(std::shared_ptr> transition) { - this->immediateTransitions.push_back(transition); -} + std::vector>> const& GSPN::getTimedTransitions() const { + return this->timedTransitions; + } + + std::vector>> const& GSPN::getImmediateTransitions() const { + return this->immediateTransitions; + } + + std::vector const& GSPN::getPlaces() const { + return places; + } + + std::shared_ptr GSPN::getInitialMarking(std::map& numberOfBits, uint_fast64_t const& numberOfTotalBits) const { + auto m = std::make_shared(getNumberOfPlaces(), numberOfBits, numberOfTotalBits); + for (auto& place : getPlaces()) { + m->setNumberOfTokensAt(place.getID(), place.getNumberOfInitialTokens()); + } + return m; + } + + std::pair GSPN::getPlace(std::string const& id) const { + for (auto& place : places) { + if (id.compare(place.getName()) == 0) { + return std::make_pair(true, place); + } + } + return std::make_pair(false, storm::gspn::Place()); + } + + std::pair> const> GSPN::getTimedTransition(std::string const& id) const { + for (auto& trans : timedTransitions) { + if (id.compare(trans->getName()) == 0) { + return std::make_pair> const>(true, static_cast> const>(trans)); + } + } + return std::make_pair> const>(false, nullptr); + } + + std::pair> const> GSPN::getImmediateTransition(std::string id) const { + for (auto& trans : immediateTransitions) { + if (id.compare(trans->getName()) == 0) { + return std::make_pair> const>(true, static_cast> const>(trans)); + } + } + return std::make_pair> const>(false, nullptr); + } + + std::pair const> GSPN::getTransition(std::string const& id) const { + auto trans = getTimedTransition(id); + if (trans.first == true) { + return trans; + } + + return getImmediateTransition(id); + } + + void GSPN::writeDotToStream(std::ostream& outStream) { + outStream << "digraph " << this->getName() << " {" << std::endl; + + // print places with initial marking (not printed is the capacity) + outStream << "\t" << "node [shape=ellipse]" << std::endl; + for (auto& place : this->getPlaces()) { + outStream << "\t" << place.getName() << " [label=\"" << place.getName() << "(" << place.getNumberOfInitialTokens(); + outStream << ")\"];" << std::endl; + } -void storm::gspn::GSPN::addTimedTransition(std::shared_ptr> transition) { - this->timedTransitions.push_back(transition); + // print transitions with weight/rate + outStream << "\t" << "node [shape=box]" << std::endl; + for (auto& trans : this->getImmediateTransitions()) { + outStream << "\t" << trans->getName() << " [label=\"" << trans->getName(); + outStream << "(immediate:" << trans->getWeight() << ")\"];" << std::endl; + } + + for (auto& trans : this->getTimedTransitions()) { + outStream << "\t" << trans->getName() << " [label=\"" << trans->getName(); + outStream << "(timed:" << trans->getRate() << ")\"];" << std::endl; + } + + // print arcs + for (auto& trans : this->getImmediateTransitions()) { + auto it = trans->getInputPlacesCBegin(); + while (it != trans->getInputPlacesCEnd()) { + outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"normal:" << + trans->getInputArcMultiplicity(**it); + outStream << "\"];" << std::endl; + + ++it; + } + + it = trans->getInhibitionPlacesCBegin(); + while (it != trans->getInhibitionPlacesCEnd()) { + outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" << + trans->getInhibitionArcMultiplicity(**it); + outStream << "\"];" << std::endl; + ++it; + } + + it = trans->getOutputPlacesCBegin(); + while (it != trans->getOutputPlacesCEnd()) { + outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" << + trans->getOutputArcMultiplicity(**it); + outStream << "\"];" << std::endl; + ++it; + } + } + + for (auto& trans : this->getTimedTransitions()) { + auto it = trans->getInputPlacesCBegin(); + while (it != trans->getInputPlacesCEnd()) { + outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"normal:" << + trans->getInputArcMultiplicity(**it); + outStream << "\"];" << std::endl; + ++it; + } + + + it = trans->getInhibitionPlacesCBegin(); + while (it != trans->getInhibitionPlacesCEnd()) { + outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" << + trans->getInhibitionArcMultiplicity(**it); + outStream << "\"];" << std::endl; + ++it; + } + + it = trans->getOutputPlacesCBegin(); + while (it != trans->getOutputPlacesCEnd()) { + outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" << + trans->getOutputArcMultiplicity(**it); + outStream << "\"];" << std::endl; + ++it; + } + } + + outStream << "}" << std::endl; + } + + void GSPN::setName(std::string const& name) { + this->name = name; + } + + std::string const& GSPN::getName() const { + return this->name; + } + } } + + diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h index 6da283a01..3217af882 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -1,10 +1,13 @@ -#ifndef STORM_GSPN_H -#define STORM_GSPN_H +#ifndef STORM_STORAGE_GSPN_GSPN_H +#define STORM_STORAGE_GSPN_GSPN_H +#include #include + #include "src/storage/gspn/ImmediateTransition.h" -#include "src/storage/gspn/TimedTransition.h" #include "src/storage/gspn/Marking.h" +#include "src/storage/gspn/Place.h" +#include "src/storage/gspn/TimedTransition.h" namespace storm { namespace gspn { @@ -16,24 +19,119 @@ namespace storm { typedef double WeightType; /*! - * The empty constructor creates an GSPN without transition and places + * Adds an immediate transition to the gspn. + * + * @param transition The transition which is added to the gspn. + */ + void addImmediateTransition(ImmediateTransition const& transition); + + /*! + * Adds a timed transition to the gspn. + * + * @param transition The transition which is added to the gspn. + */ + void addTimedTransition(TimedTransition const& transition); + + /*! + * Adds a place to the gspn. + * + * @param place The place which is added to the gspn. + */ + void addPlace(Place const& place); + + /*! + * Returns the number of places in this gspn. + * + * @return The number of places. + */ + uint_fast64_t getNumberOfPlaces() const; + + /*! + * Returns the vector of timed transitions in this gspn. + * + * @return The vector of timed transitions. + */ + std::vector>> const& getTimedTransitions() const; + + /*! + * Returns the vector of immediate transitions in this gspn. + * + * @return The vector of immediate tansitions. + */ + std::vector>> const& getImmediateTransitions() const; + + /*! + * Returns the places of this gspn + */ + std::vector const& getPlaces() const; + + /* + * Computes the initial marking of the gspn. + * + * @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; + + /*! + * Returns the place with the corresponding id. + * + * @param id The ID of the place. + * @return The first element is true if the place was found. + * 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 getPlace(std::string const& id) const; + + /*! + * Returns the timed transition with the corresponding id. + * + * @param id The ID of the timed transition. + * @return The first element is true if the transition was found. + * If the first element is true, then the second element is the wanted transition. + * If the first element is false, then the second element is the nullptr. + */ + std::pair> const> getTimedTransition(std::string const& id) const; + + /*! + * Returns the immediate transition with the corresponding id. + * + * @param id The ID of the timed transition. + * @return The first element is true if the transition was found. + * If the first element is true, then the second element is the wanted transition. + * If the first element is false, then the second element is the nullptr. */ - GSPN(); + std::pair> const> getImmediateTransition(std::string id) const; /*! - * Set the number of tokens for a given place. + * Returns the transition with the corresponding id. * - * @param place - * @param token + * @param id The ID of the transition. + * @return Pointer to the corresponding transition or nullptr if the place does not exists. */ - void setInitialTokens(uint64_t place, uint64_t token); + // std::shared_ptr getTransition(std::string const& id) const; + std::pair const> getTransition(std::string const& id) const; - void setNumberOfPlaces(uint64_t number); + /*! + * Write the gspn in a dot(graphviz) configuration. + * + * @param outStream The stream to which the output is written to. + */ + void writeDotToStream(std::ostream& outStream); - uint64_t getNumberOfPlaces(); + /*! + * Set the name of the gspn to the given name. + * + * @param name The new name. + */ + void setName(std::string const& name); - void addImmediateTransition(std::shared_ptr> transition); - void addTimedTransition(std::shared_ptr> transition); + /*! + * Returns the name of the gspn. + * + * @return The name. + */ + std::string const& getName() const; private: // set containing all immediate transitions std::vector>> immediateTransitions; @@ -41,10 +139,13 @@ namespace storm { // set containing all timed transitions std::vector>> timedTransitions; - // initial marking - storm::gspn::Marking initialMarking; + // set containing all places + std::vector places; + + // name of the gspn + std::string name; }; } } -#endif //STORM_GSPN_H +#endif //STORM_STORAGE_GSPN_GSPN_H diff --git a/src/storage/gspn/ImmediateTransition.h b/src/storage/gspn/ImmediateTransition.h index d3c29129e..ea79d57bf 100644 --- a/src/storage/gspn/ImmediateTransition.h +++ b/src/storage/gspn/ImmediateTransition.h @@ -1,5 +1,5 @@ -#ifndef STORM_IMMEDIATETRANSITION_H -#define STORM_IMMEDIATETRANSITION_H +#ifndef STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_ +#define STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_ #include "src/storage/gspn/Transition.h" @@ -13,7 +13,7 @@ namespace storm { * * @param weight The new weight for this transition. */ - void setWeight(WeightType weight) { + void setWeight(WeightType const& weight) { this->weight = weight; } @@ -22,7 +22,7 @@ namespace storm { * * @return The weight of this transition. */ - WeightType getWeight() { + WeightType getWeight() const { return this->weight; } private: @@ -32,4 +32,4 @@ namespace storm { } } -#endif //STORM_IMMEDIATETRANSITION_H +#endif //STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_ diff --git a/src/storage/gspn/Marking.cpp b/src/storage/gspn/Marking.cpp index 994d2a4f1..7ea71476e 100644 --- a/src/storage/gspn/Marking.cpp +++ b/src/storage/gspn/Marking.cpp @@ -1,110 +1,59 @@ +#include #include "src/storage/gspn/Marking.h" namespace storm { namespace gspn { - Marking::Marking(uint_fast64_t numberOfPlaces, uint_fast64_t maxNumberOfTokens) { + Marking::Marking(uint_fast64_t const& numberOfPlaces, std::map const& numberOfBits, uint_fast64_t const& numberOfTotalBits) { this->numberOfPlaces = numberOfPlaces; - this->maxNumberOfTokens = maxNumberOfTokens; - - this->numberOfBits = calculateNumberOfBits(maxNumberOfTokens); - this->marking = storm::storage::BitVector(numberOfBits * numberOfPlaces); + this->numberOfBits = numberOfBits; + this->marking = storm::storage::BitVector(numberOfTotalBits); } - uint_fast64_t Marking::getNumberOfPlaces() { - return this->numberOfPlaces; + Marking::Marking(uint_fast64_t const& numberOfPlaces, std::map const& numberOfBits, storm::storage::BitVector const& bitvector) { + this->numberOfPlaces = numberOfPlaces; + this->numberOfBits = numberOfBits; + this->marking = bitvector; } - uint_fast64_t Marking::getMaxNumberOfTokens() { - return this->maxNumberOfTokens; + uint_fast64_t Marking::getNumberOfPlaces() const { + return this->numberOfPlaces; } - void Marking::setNumberOfTokensAt(uint_fast64_t place, uint_fast64_t numberOfTokens) { - // TODO check range (place < getNumberOfPlaces(), numberOfTokens < getMaxNumberOfTokens()) - for (uint_fast64_t i = place * numberOfBits; i <(place * numberOfBits) + numberOfBits; ++i) { - if (numberOfTokens % 2 == 0) { - marking.set(i, false); - } else { - marking.set(i, true); - } - numberOfTokens /= 2; + void Marking::setNumberOfTokensAt(uint_fast64_t const& place, uint_fast64_t const& numberOfTokens) { + uint_fast64_t index = 0; + for (uint_fast64_t i=0; i < place; ++i) { + index += numberOfBits[i]; } + marking.setFromInt(index, numberOfBits[place], numberOfTokens); } - uint_fast64_t Marking::getNumberOfTokensAt(uint_fast64_t place) { - uint_fast64_t tokens = 0; - for (uint_fast64_t i = place * numberOfBits, mult = 0; i < (place * numberOfBits) + numberOfBits; ++i, ++mult) { - if (marking.get(i)) { - tokens += std::pow(2, mult); - } + uint_fast64_t Marking::getNumberOfTokensAt(uint_fast64_t const& place) const { + uint_fast64_t index = 0; + for (uint_fast64_t i=0; i < place; ++i) { + index += numberOfBits.at(i); } - return tokens; + return marking.getAsInt(index, numberOfBits.at(place)); } - bool Marking::setNumberOfPlaces(uint_fast64_t numberOfPlaces) { - if (numberOfPlaces == this->numberOfPlaces) { - return true; - } - if (numberOfPlaces > this->numberOfPlaces) { - marking.resize(numberOfPlaces * numberOfBits); - this->numberOfPlaces = numberOfPlaces; - return true; - } else { - auto diff = this->numberOfPlaces - numberOfPlaces; - for (uint64_t i = 0; i < diff; ++i) { - if (getNumberOfTokensAt(numberOfPlaces-1-i) != 0) { - // TODO error - return false; - } - } - marking.resize(numberOfPlaces * numberOfBits); - this->numberOfPlaces = numberOfPlaces; - return true; - } + std::shared_ptr Marking::getBitVector() const { + auto result = std::make_shared(); + *result = storm::storage::BitVector(marking); + return result; } - bool Marking::setMaxNumberOfTokens(uint_fast64_t maxNumberOfTokens) { - for (uint64_t i = 0; i < getNumberOfPlaces(); ++i) { - if (getNumberOfTokensAt(i) > maxNumberOfTokens) { - return false; - } + bool Marking::operator==(const Marking& other) const { + if (getNumberOfPlaces() != other.getNumberOfPlaces()) { + return false; } - - if (maxNumberOfTokens == getMaxNumberOfTokens()) { - return true; + if (&numberOfBits == &other.numberOfBits) { + return marking == other.marking; } - - uint_fast64_t newNumberOfBits = calculateNumberOfBits(maxNumberOfTokens); - if (maxNumberOfTokens < getMaxNumberOfTokens()) { - for (uint_fast64_t i = 0; i < getNumberOfPlaces(); ++i) { - for (uint_fast64_t j = 0; j < numberOfBits; ++j) { - marking.set(i*newNumberOfBits + j , marking.get(i*numberOfBits + j)); - } - } - marking.resize(getNumberOfPlaces() * newNumberOfBits); - } else { - marking.resize(getNumberOfPlaces() * newNumberOfBits); - for (int_fast64_t i = getNumberOfPlaces()-1; i >= 0; --i) { - for (int_fast64_t j = numberOfBits-1; j >= 0; --j) { - for (uint_fast64_t diff = 0; diff < newNumberOfBits-numberOfBits; ++diff) { - marking.set(i*newNumberOfBits+j+diff+1, 0); - } - marking.set(i*newNumberOfBits+j, marking.get(i*numberOfBits+j)); - } + for (uint_fast64_t i=0; i < getNumberOfPlaces(); ++i) { + if (getNumberOfTokensAt(i) != other.getNumberOfTokensAt(i)) { + return false; } } - numberOfBits = newNumberOfBits; return true; } - - void Marking::incNumberOfPlaces() { - setNumberOfPlaces(getNumberOfPlaces()+1); - } - - uint_fast64_t Marking::calculateNumberOfBits(uint_fast64_t maxNumber) { - if (maxNumber == 0) { - return 1; - } - return std::floor(std::log2(maxNumber)) + 1; - } } } \ No newline at end of file diff --git a/src/storage/gspn/Marking.h b/src/storage/gspn/Marking.h index 5d312c88c..2e5095e50 100644 --- a/src/storage/gspn/Marking.h +++ b/src/storage/gspn/Marking.h @@ -1,35 +1,39 @@ -#ifndef STORM_MARKING_H -#define STORM_MARKING_H +#ifndef STORM_STORAGE_GSPN_MARKING_H_ +#define STORM_STORAGE_GSPN_MARKING_H_ #include - +#include #include "src/storage/BitVector.h" namespace storm { namespace gspn { class Marking { public: + /*! - * Creates an empty marking (at all places are 0 tokens). + * Creates an empty marking (at all places contain 0 tokens). * - * @param numberOfPlaces The number of places in the gspn. - * @param maxNumberOfTokens The maximal number of tokens in one place. + * @param numberOfPlaces The number of places of the gspn. + * @param numberOfBits The number of bits used to store the number of tokens for each place + * @param numberOfTotalBits The length of the internal bitvector */ - Marking(uint_fast64_t numberOfPlaces, uint_fast64_t maxNumberOfTokens); + Marking(uint_fast64_t const& numberOfPlaces, std::map const& numberOfBits, uint_fast64_t const& numberOfTotalBits); /*! - * Retrieves the number of places for which the tokens are stored. + * Create the marking described by the bitvector. * - * @return The number of places. + * @param numberOfPlaces The number of places of the gspn. + * @param numberOfBits The number of bits used to store the number of tokens for each place + * @param bitvector The bitvector encoding the marking. */ - uint_fast64_t getNumberOfPlaces(); + Marking(uint_fast64_t const&numberOfPlaces, std::map const& numberOfBits, storm::storage::BitVector const& bitvector); /*! - * Retrieves the maximal number of tokens which can be stored in one place. + * Retrieves the number of places for which the tokens are stored. * - * @return The maximal number of tokens. + * @return The number of places. */ - uint_fast64_t getMaxNumberOfTokens(); + uint_fast64_t getNumberOfPlaces() const; /*! * Set the number of tokens for the given place to the given amount. @@ -37,7 +41,7 @@ namespace storm { * @param place Place must be a valid place for which the number of tokens is changed. * @param numberOfTokens The new number of tokens at the place. */ - void setNumberOfTokensAt(uint_fast64_t place, uint_fast64_t numberOfTokens); + void setNumberOfTokensAt(uint_fast64_t const& place, uint_fast64_t const& numberOfTokens); /*! * Get the number of tokens for the given place. @@ -45,51 +49,31 @@ namespace storm { * @param place The place from which the tokens are counted. * @return The number of tokens at the place. */ - uint_fast64_t getNumberOfTokensAt(uint_fast64_t place); + uint_fast64_t getNumberOfTokensAt(uint_fast64_t const& place) const; /*! - * Reset the number of places. - * If the new number of places is larger than the old one, the new places start with 0 tokens. - * If the new number of places is smaller than the old one, the places which are going to be - * erased must not contain any tokens. + * Returns a copy of the bitvector * - * @param numberOfPlaces The new number of places. - * @return Return True if the change is made. + * @return The bitvector which encodes the marking */ - bool setNumberOfPlaces(uint_fast64_t numberOfPlaces); + std::shared_ptr getBitVector() const; /*! - * Increases the number of places by one. + * Overload equality operator */ - void incNumberOfPlaces(); - - /*! - * - */ - bool setMaxNumberOfTokens(uint_fast64_t maxNumberOfTokens); + bool operator==(const Marking& other) const; private: // the maximal number of places in the gspn uint_fast64_t numberOfPlaces; - // the maximal number of tokens in one place - uint_fast64_t maxNumberOfTokens; + // number of bits for each place + std::map numberOfBits; // contains the information of the marking storm::storage::BitVector marking; - - // number of bits which are needed to store the tokens for one place - uint_fast64_t numberOfBits; - - /*! - * Calculates the number of bits needed to store at least the given number. - * - * @param maxNumber The maximal value which can be stored - * @return The number of bits needed. - */ - uint_fast64_t calculateNumberOfBits(uint_fast64_t maxNumber); }; } } -#endif //STORM_MARKING_H +#endif //STORM_STORAGE_GSPN_MARKING_H_ diff --git a/src/storage/gspn/Place.cpp b/src/storage/gspn/Place.cpp new file mode 100644 index 000000000..443766bf0 --- /dev/null +++ b/src/storage/gspn/Place.cpp @@ -0,0 +1,41 @@ +#include "Place.h" + +#include "src/exceptions/IllegalArgumentValueException.h" +#include "src/utility/macros.h" + +namespace storm { + namespace gspn { + void Place::setName(std::string const& name) { + this->name = name; + } + + std::string Place::getName() const { + return this->name; + } + + void Place::setID(uint_fast64_t const& id) { + this->id = id; + } + + uint_fast64_t Place::getID() const { + return this->id; + } + + void Place::setNumberOfInitialTokens(uint_fast64_t const& tokens) { + this->numberOfInitialTokens = tokens; + } + + uint_fast64_t Place::getNumberOfInitialTokens() const { + return this->numberOfInitialTokens; + } + + void Place::setCapacity(int_fast64_t const& capacity) { + STORM_LOG_THROW(capacity >= -1, storm::exceptions::IllegalArgumentValueException, "The capacity cannot be less than -1."); + this->capacity = capacity; + } + + int_fast64_t Place::getCapacity() const { + return this->capacity; + } + } +} \ No newline at end of file diff --git a/src/storage/gspn/Place.h b/src/storage/gspn/Place.h new file mode 100644 index 000000000..f7182f7c7 --- /dev/null +++ b/src/storage/gspn/Place.h @@ -0,0 +1,87 @@ +#ifndef STORM_STORAGE_GSPN_PLACE_H_ +#define STORM_STORAGE_GSPN_PLACE_H_ + +#include + +namespace storm { + namespace gspn { + /*! + * This class provides methods to store and retrieve data for a place in a gspn. + */ + class Place { + public: + /*! + * Sets the name of this place. The name must be unique for a gspn. + * + * @param name The new name for the place. + */ + void setName(std::string const& name); + + /*! + * Returns the name of this place. + * + * @return The name of this place. + */ + std::string getName() const; + + /*! + * Sets the id of this place. The id must be unique for a gspn. + * + * @param id The new id of this place. + */ + void setID(uint_fast64_t const& id); + + /*! + * Returns the id of this place. + * + * @return The id of this place. + */ + uint_fast64_t getID() const; + + /*! + * Sets the number of initial tokens of this place. + * + * @param tokens The number of initial tokens. + */ + void setNumberOfInitialTokens(uint_fast64_t const& tokens); + + /*! + * Returns the number of initial tokens of this place. + * + * @return The number of initial tokens of this place. + */ + uint_fast64_t getNumberOfInitialTokens() const; + + /*! + * Sets the capacity of tokens of this place. + * + * @param capacity The capacity of this place. A non-negative number represents the capacity. + * The value -1 indicates that the capacity is not set. + */ + void setCapacity(int_fast64_t const& capacity); + + /*! + * Returns the capacity of tokens of this place. + * + * @return The capacity of the place. The value -1 indicates that the capacity is not set. + */ + int_fast64_t getCapacity() const; + private: + // contains the number of initial tokens of this place + uint_fast64_t numberOfInitialTokens; + + // unique id (is used to refer to a specific place in a bitvector) + uint_fast64_t id; + + // name which is used in pnml file + std::string name; + + // capacity of this place + // -1 indicates that the capacity is not set + // other non-negative values represents the capacity + int_fast64_t capacity; + }; + } +} + +#endif //STORM_STORAGE_GSPN_PLACE_H_ diff --git a/src/storage/gspn/TimedTransition.h b/src/storage/gspn/TimedTransition.h index 86e0b3451..886fa2e2d 100644 --- a/src/storage/gspn/TimedTransition.h +++ b/src/storage/gspn/TimedTransition.h @@ -1,5 +1,5 @@ -#ifndef STORM_TIMEDTRANSITION_H -#define STORM_TIMEDTRANSITION_H +#ifndef STORM_STORAGE_GSPN_TIMEDTRANSITION_H_ +#define STORM_STORAGE_GSPN_TIMEDTRANSITION_H_ #include "src/storage/gspn/Transition.h" @@ -13,7 +13,7 @@ namespace storm { * * @param rate The new rate for this transition. */ - void setRate(RateType rate) { + void setRate(RateType const& rate) { this->rate = rate; } @@ -22,7 +22,7 @@ namespace storm { * * @return The rate of this transition. */ - RateType getRate() { + RateType getRate() const { return this->rate; } @@ -33,4 +33,4 @@ namespace storm { } } -#endif //STORM_TIMEDTRANSITION_H +#endif //STORM_STORAGE_GSPN_TIMEDTRANSITION_H_ diff --git a/src/storage/gspn/Transition.cpp b/src/storage/gspn/Transition.cpp index 7e1b6ed8f..f790788f4 100644 --- a/src/storage/gspn/Transition.cpp +++ b/src/storage/gspn/Transition.cpp @@ -1,63 +1,81 @@ #include "src/storage/gspn/Transition.h" +#include "src/utility/macros.h" + namespace storm { namespace gspn { - void Transition::setInputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity) { - inputMultiplicities[place] = multiplicity; + void Transition::setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) { + auto ptr = std::make_shared(place); + inputMultiplicities[ptr] = multiplicity; + inputPlaces.push_back(ptr); } - bool Transition::removeInputArc(uint_fast64_t place) { + bool Transition::removeInputArc(storm::gspn::Place const& place) { if (existsInputArc(place)) { - inputMultiplicities.erase(place); + auto ptr = std::make_shared(place); + inputMultiplicities.erase(ptr); + inputPlaces.erase(std::find(inputPlaces.begin(), inputPlaces.end(), ptr)); return true; } else { return false; } } - bool Transition::existsInputArc(uint_fast64_t place) { - return inputMultiplicities.end() != inputMultiplicities.find(place); + bool Transition::existsInputArc(storm::gspn::Place const& place) const { + auto ptr = std::make_shared(place); + return inputMultiplicities.end() != inputMultiplicities.find(ptr); } - void Transition::setOutputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity) { - outputMultiplicities[place] = multiplicity; + void Transition::setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) { + auto ptr = std::make_shared(place); + outputMultiplicities[ptr] = multiplicity; + outputPlaces.push_back(ptr); } - bool Transition::removeOutputArc(uint_fast64_t place) { + bool Transition::removeOutputArc(storm::gspn::Place const& place) { if (existsOutputArc(place)) { - outputMultiplicities.erase(place); + auto ptr = std::make_shared(place); + outputMultiplicities.erase(ptr); + outputPlaces.erase(std::find(outputPlaces.begin(), outputPlaces.end(), ptr)); return true; } else { return false; } } - bool Transition::existsOutputArc(uint_fast64_t place) { - return outputMultiplicities.end() != outputMultiplicities.find(place); + bool Transition::existsOutputArc(storm::gspn::Place const& place) const { + auto ptr = std::make_shared(place); + return outputMultiplicities.end() != outputMultiplicities.find(ptr); } - void Transition::setInhibitionArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity) { - inhibitionMultiplicities[place] = multiplicity; + void Transition::setInhibitionArcMultiplicity(storm::gspn::Place const& place, + uint_fast64_t multiplicity) { + auto ptr = std::make_shared(place); + inhibitionMultiplicities[ptr] = multiplicity; + inhibitionPlaces.push_back(ptr); } - bool Transition::removeInhibitionArc(uint_fast64_t place) { + bool Transition::removeInhibitionArc(storm::gspn::Place const& place) { if (existsInhibitionArc(place)) { - inhibitionMultiplicities.erase(place); + auto ptr = std::make_shared(place); + inhibitionMultiplicities.erase(ptr); + inhibitionPlaces.erase(std::find(inhibitionPlaces.begin(), inhibitionPlaces.end(), ptr)); return true; } else { return false; } } - bool Transition::existsInhibitionArc(uint_fast64_t place) { - return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(place); + bool Transition::existsInhibitionArc(storm::gspn::Place const& place) const { + auto ptr = std::make_shared(place); + return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr); } - bool Transition::isEnabled(storm::gspn::Marking marking) { + bool Transition::isEnabled(storm::gspn::Marking const& marking) const { auto inputIterator = inputMultiplicities.cbegin(); while (inputIterator != inputMultiplicities.cend()) { - if (marking.getNumberOfTokensAt(inputIterator->first) < inputIterator->second) { + if (marking.getNumberOfTokensAt(inputIterator->first->getID()) < inputIterator->second) { return false; } @@ -66,20 +84,104 @@ namespace storm { auto inhibitionIterator = inhibitionMultiplicities.cbegin(); while (inhibitionIterator != inhibitionMultiplicities.cend()) { - if (marking.getNumberOfTokensAt(inhibitionIterator->first) >= inhibitionIterator->second) { + if (marking.getNumberOfTokensAt(inhibitionIterator->first->getID()) >= inhibitionIterator->second) { return false; } ++inhibitionIterator; } + auto outputIterator = outputMultiplicities.cbegin(); + while (outputIterator != outputMultiplicities.cend()) { + if (outputIterator->first->getCapacity() >= 0) { + if (marking.getNumberOfTokensAt(outputIterator->first->getID()) + outputIterator->second > outputIterator->first->getCapacity()) { + return false; + } + } + + ++outputIterator; + } + return true; } - storm::gspn::Marking Transition::fire(const storm::gspn::Marking marking) { - //check if transition is enabled + storm::gspn::Marking Transition::fire(storm::gspn::Marking const& marking) const { + storm::gspn::Marking newMarking(marking); + + auto inputIterator = inputMultiplicities.cbegin(); + while (inputIterator != inputMultiplicities.cend()) { + newMarking.setNumberOfTokensAt(inputIterator->first->getID(), + newMarking.getNumberOfTokensAt(inputIterator->first->getID()) - inputIterator->second); + ++inputIterator; + } + + auto outputIterator = outputMultiplicities.cbegin(); + while (outputIterator != outputMultiplicities.cend()) { + newMarking.setNumberOfTokensAt(outputIterator->first->getID(), + newMarking.getNumberOfTokensAt(outputIterator->first->getID()) + outputIterator->second); + ++outputIterator; + } + + return newMarking; + } + + void Transition::setName(std::string const& name) { + this->name = name; + } + + std::string const& Transition::getName() const { + return this->name; + } + + std::vector>::const_iterator Transition::getInputPlacesCBegin() const { + return this->inputPlaces.cbegin(); + } + + std::vector>::const_iterator Transition::getInputPlacesCEnd() const { + return this->inputPlaces.cend(); + } - return gspn::Marking(0, 0); + std::vector>::const_iterator Transition::getOutputPlacesCBegin() const { + return this->outputPlaces.cbegin(); + } + + std::vector>::const_iterator Transition::getOutputPlacesCEnd() const { + return this->outputPlaces.cend(); + } + + std::vector>::const_iterator Transition::getInhibitionPlacesCBegin() const { + return this->inhibitionPlaces.cbegin(); + } + + std::vector>::const_iterator Transition::getInhibitionPlacesCEnd() const { + return this->inhibitionPlaces.cend(); + } + + uint_fast64_t Transition::getInputArcMultiplicity(storm::gspn::Place const& place) const { + if (existsInputArc(place)) { + auto ptr = std::make_shared(place); + return inputMultiplicities.at(ptr); + } else { + return 0; + } + } + + uint_fast64_t Transition::getInhibitionArcMultiplicity(storm::gspn::Place const& place) const { + if (existsInhibitionArc(place)) { + auto ptr = std::make_shared(place); + return inhibitionMultiplicities.at(ptr); + } else { + return 0; + } + } + + uint_fast64_t Transition::getOutputArcMultiplicity(storm::gspn::Place const& place) const { + if (existsOutputArc(place)) { + auto ptr = std::make_shared(place); + return outputMultiplicities.at(ptr); + } else { + return 0; + } } } } diff --git a/src/storage/gspn/Transition.h b/src/storage/gspn/Transition.h index 986c7a48a..86471f2fc 100644 --- a/src/storage/gspn/Transition.h +++ b/src/storage/gspn/Transition.h @@ -1,11 +1,16 @@ -#ifndef STORM_TRANSITION_H -#define STORM_TRANSITION_H +#ifndef STORM_STORAGE_GSPN_TRANSITION_H_ +#define STORM_STORAGE_GSPN_TRANSITION_H_ #include -#include "Marking.h" +#include +#include "src/storage/gspn/Marking.h" +#include "src/storage/gspn/Place.h" namespace storm { namespace gspn { + /*! + * This class represents a transition in a gspn. + */ class Transition { public: /*! @@ -16,7 +21,7 @@ namespace storm { * @param place The place connected by an input arc. * @param multiplicity The multiplicity of the specified arc. */ - void setInputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity); + void setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity); /*! * Removes an input arc connected to a given place. @@ -24,7 +29,7 @@ namespace storm { * @param place The place from which the input arc is originating. * @return True if the arc existed. */ - bool removeInputArc(uint_fast64_t place); + bool removeInputArc(storm::gspn::Place const& place); /*! * Checks whether the given place is connected to this transition via an input arc. @@ -32,7 +37,7 @@ namespace storm { * @param place The place which is going to be checked. * @return True if the place is connected via an input arc. */ - bool existsInputArc(uint_fast64_t place); + bool existsInputArc(storm::gspn::Place const& place) const; /*! * Set the multiplicity of the output arc going to the place. @@ -42,7 +47,7 @@ namespace storm { * @param place The place connected by an output arc. * @param multiplicity The multiplicity of the specified arc. */ - void setOutputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity); + void setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity); /*! * Removes an output arc connected to a given place. @@ -50,7 +55,7 @@ namespace storm { * @param place The place from which the output arc is leading to. * @return True if the arc existed. */ - bool removeOutputArc(uint_fast64_t place); + bool removeOutputArc(storm::gspn::Place const& place); /*! * Checks whether the given place is connected to this transition via an output arc. @@ -58,7 +63,7 @@ namespace storm { * @param place The place which is going to be checked. * @return True if the place is connected via an output arc. */ - bool existsOutputArc(uint_fast64_t place); + bool existsOutputArc(storm::gspn::Place const& place) const; /*! * Set the multiplicity of the inhibition arc originating from the place. @@ -68,7 +73,7 @@ namespace storm { * @param place The place connected by an inhibition arc. * @param multiplicity The multiplicity of the specified arc. */ - void setInhibitionArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity); + void setInhibitionArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity); /*! * Removes an inhibition arc connected to a given place. @@ -76,7 +81,7 @@ namespace storm { * @param place The place from which the inhibition arc is originating. * @return True if the arc existed. */ - bool removeInhibitionArc(uint_fast64_t place); + bool removeInhibitionArc(storm::gspn::Place const& place); /*! * Checks whether the given place is connected to this transition via an inhibition arc. @@ -84,14 +89,14 @@ namespace storm { * @param place The place which is going to be checked. * @return True if the place is connected via an inhibition arc. */ - bool existsInhibitionArc(uint_fast64_t place); + bool existsInhibitionArc(storm::gspn::Place const& place) const; /*! * Checks if the given marking enables the transition. * * @return True if the transition is enabled. */ - bool isEnabled(storm::gspn::Marking marking); + bool isEnabled(storm::gspn::Marking const& marking) const; /*! * Fire the transition if possible. @@ -99,18 +104,120 @@ namespace storm { * @param marking The current marking before the transition is fired. * @return The marking after the transition was fired. */ - storm::gspn::Marking fire(const storm::gspn::Marking marking); + storm::gspn::Marking fire(storm::gspn::Marking const& marking) const; + + /*! + * Set the name of the transition. + * + * @param name New name of the transition. + */ + void setName(std::string const& name); + + /*! + * Returns the name of the transition. + * + * @return The name of the transition. + */ + std::string const& getName() const; + + /*! + * Returns a constant iterator to the begin of a vector which contains all input places. + * + * @return Returns iterator. + */ + std::vector>::const_iterator getInputPlacesCBegin() const; + + /*! + * Returns a constant iterator to the end of a vector which contains all input places. + * + * @return Returns iterator. + */ + std::vector>::const_iterator getInputPlacesCEnd() const; + + /*! + * Returns a constant iterator to the begin of a vector which contains all output places. + * + * @return Returns iterator. + */ + std::vector>::const_iterator getOutputPlacesCBegin() const; + + /*! + * Returns a constant iterator to the end of a vector which contains all output places. + * + * @return Returns iterator. + */ + std::vector>::const_iterator getOutputPlacesCEnd() const; + + /*! + * Returns a constant iterator to the begin of a vector which contains all inhibition places. + * + * @return Returns iterator. + */ + std::vector>::const_iterator getInhibitionPlacesCBegin() const; + + /*! + * Returns a constant iterator to the end of a vector which contains all inhibition places. + * + * @return Returns iterator. + */ + std::vector>::const_iterator getInhibitionPlacesCEnd() const; + + /*! + * Returns the corresponding multiplicity. + * + * @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; + + /*! + * Returns the corresponding multiplicity. + * + * @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; + + /*! + * Returns the corresponding multiplicity. + * + * @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; 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()(std::shared_ptr const& lhs, std::shared_ptr const& rhs) const { + return lhs->getID() < rhs->getID(); + } + }; + // maps places connected to this transition with an input arc to the corresponding multiplicity - std::map inputMultiplicities; + std::map, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inputMultiplicities; // maps places connected to this transition with an output arc to the corresponding multiplicities - std::map outputMultiplicities; + std::map, uint_fast64_t, storm::gspn::Transition::PlaceComparator> outputMultiplicities; // maps places connected to this transition with an inhibition arc to the corresponding multiplicity - std::map inhibitionMultiplicities; + std::map, uint_fast64_t, storm::gspn::Transition::PlaceComparator> 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; }; } } -#endif //STORM_TRANSITION_H \ No newline at end of file +#endif //STORM_STORAGE_GSPN_TRANSITION_H_ \ No newline at end of file