diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 6e087822f..1867978c5 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -363,7 +363,9 @@ namespace storm { storm::utility::outputFixedWidth(outStream, this->getLabelsOfState(state), maxWidthLabel); outStream << "}"; } - + + outStream << this->additionalDotStateInfo(state); + // If we are to include some values for the state as well, we do so now. if (firstValue != nullptr || secondValue != nullptr) { outStream << " ["; @@ -397,7 +399,12 @@ namespace storm { outStream << "}" << std::endl; } } - + + template + std::string Model::additionalDotStateInfo(uint64_t state) const { + return ""; + } + template std::set Model::getLabelsOfState(storm::storage::sparse::state_type state) const { return this->stateLabeling.getLabelsOfState(state); diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index d1ef45bc1..962fda437 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -333,8 +333,8 @@ namespace storm { * @param finalizeOutput A flag that sets whether or not the dot stream is closed with a curly brace. * @return A string containing the exported model in dot-format. */ - virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; - + virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; + /*! * Retrieves the set of labels attached to the given state. * @@ -394,6 +394,13 @@ namespace storm { * @param out The stream the information is to be printed to. */ void printRewardModelsInformationToStream(std::ostream& out) const; + + /*! + * Return a string that is additonally added to the state information in the dot stream. + * @param state + * @return + */ + virtual std::string additionalDotStateInfo(uint64_t state) const; private: diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index babc81e6b..6dbe7b365 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -59,6 +59,12 @@ namespace storm { return observations; } + template + std::string Pomdp::additionalDotStateInfo(uint64_t state) const { + return "<" + std::to_string(getObservation(state)) + ">"; + } + + template std::vector Pomdp::getStatesWithObservation(uint32_t observation) const { @@ -71,6 +77,8 @@ namespace storm { return result; } + + template class Pomdp; template class Pomdp; template class Pomdp>; diff --git a/src/storm/models/sparse/Pomdp.h b/src/storm/models/sparse/Pomdp.h index d480deebc..6ceea00f9 100644 --- a/src/storm/models/sparse/Pomdp.h +++ b/src/storm/models/sparse/Pomdp.h @@ -64,6 +64,13 @@ namespace storm { std::vector getStatesWithObservation(uint32_t observation) const; protected: + /*! + * Return a string that is additonally added to the state information in the dot stream. + * @param state + * @return + */ + virtual std::string additionalDotStateInfo(uint64_t state) const override; + // TODO: consider a bitvector based presentation (depending on our needs). std::vector observations;