diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index 61d2e18fa..8680c0d7b 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -16,6 +16,7 @@ #include "src/storage/expressions/ExpressionEvaluator.h" #include "src/storage/BitVectorHashMap.h" #include "src/logic/Formulas.h" +#include "src/models/sparse/StateAnnotation.h" #include "src/models/sparse/Model.h" #include "src/models/sparse/StateLabeling.h" #include "src/storage/SparseMatrix.h" @@ -59,7 +60,7 @@ namespace storm { }; // A structure holding information about the reachable state space that can be retrieved from the outside. - struct StateInformation { + struct StateInformation : public storm::models::sparse::StateAnnotation { /*! * Constructs a state information object for the given number of states. */ @@ -67,6 +68,12 @@ namespace storm { // A mapping from state indices to their variable valuations. std::vector valuations; + + std::string stateInfo(uint_fast64_t state) const override { + return valuations[state].toString(); + } + + }; // A structure storing information about the used variables of the program. @@ -195,7 +202,7 @@ namespace storm { bool buildAllRewardModels; // A flag that indicates whether or not to store the state information after successfully building the - // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successfull + // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful // call to translateProgram. bool buildStateInformation; diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp index 6396af48d..4a4b37d60 100644 --- a/src/models/sparse/Mdp.cpp +++ b/src/models/sparse/Mdp.cpp @@ -2,6 +2,7 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/utility/constants.h" +#include "src/utility/vector.h" #include "src/adapters/CarlAdapter.h" #include "src/models/sparse/StandardRewardModel.h" @@ -81,7 +82,13 @@ namespace storm { for (auto const& rewardModel : this->getRewardModels()) { newRewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledChoices)); } - return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling()); + if(this->hasChoiceLabeling()) { + return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, boost::optional>(storm::utility::vector::filterVector(this->getChoiceLabeling(), enabledChoices))); + } else { + return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, boost::optional>()); + } + + } template diff --git a/src/models/sparse/StateAnnotation.h b/src/models/sparse/StateAnnotation.h new file mode 100644 index 000000000..42067bf76 --- /dev/null +++ b/src/models/sparse/StateAnnotation.h @@ -0,0 +1,16 @@ +#ifndef STORM_STATEANNOTATION_H +#define STORM_STATEANNOTATION_H + +namespace storm { + namespace models { + namespace sparse { + class StateAnnotation { + public: + virtual std::string stateInfo(uint_fast64_t s) const = 0; + }; + } + } + +} + +#endif //STORM_STATEANNOTATION_H \ No newline at end of file diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index 57035b397..3a7a995dc 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -109,30 +109,58 @@ namespace storm { } return "[" + boost::join(assignments, ", ") + "]"; } - - std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation) { - out << "valuation {" << std::endl; - out << valuation.getManager() << std::endl; - if (!valuation.booleanValues.empty()) { - for (auto const& element : valuation.booleanValues) { - out << element << " "; + + + std::string SimpleValuation::toString(bool pretty) const { + + + std::stringstream sstr; + if(pretty) { + sstr << "valuation {" << std::endl; + for(auto const& e : getManager()) { + sstr << e.first.getName() << "="; + if (e.first.hasBooleanType()) { + sstr << std::boolalpha << this->getBooleanValue(e.first) << std::noboolalpha; + } else if (e.first.hasIntegerType()) { + sstr << this->getIntegerValue(e.first); + } else if (e.first.hasRationalType()) { + sstr << this->getRationalValue(e.first); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); + } + sstr << std::endl; } - out << std::endl; - } - if (!valuation.integerValues.empty()) { - for (auto const& element : valuation.integerValues) { - out << element << " "; + sstr << "}"; + } else { + sstr << "valuation {" << std::endl; + sstr << getManager() << std::endl; + if (!booleanValues.empty()) { + for (auto const& element : booleanValues) { + sstr << element << " "; + } + sstr << std::endl; } - out << std::endl; - } - if (!valuation.rationalValues.empty()) { - for (auto const& element : valuation.rationalValues) { - out << element << " "; + if (!integerValues.empty()) { + for (auto const& element : integerValues) { + sstr << element << " "; + } + sstr << std::endl; + } + if (!rationalValues.empty()) { + for (auto const& element : rationalValues) { + sstr << element << " "; + } + sstr << std::endl; } - out << std::endl; + sstr << "}"; } - out << "}" << std::endl; - + + + return sstr.str(); + } + + std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation) { + out << valuation.toString(false) << std::endl; return out; } diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 47278e1ee..d9477b41e 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -61,7 +61,9 @@ namespace storm { * @return The string representation. */ virtual std::string toPrettyString(std::set const& selectedVariables) const; - + + virtual std::string toString(bool pretty = true) const; + friend std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation); private: diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 9ac73881e..8e3fae0cf 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1066,6 +1066,16 @@ namespace storm { storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0); return Program(manager, this->getModelType(), this->getConstants(), std::vector(), std::vector(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels(), this->getFilename(), 0, true); } + + std::unordered_map Program::buildCommandIndexToActionNameMap() const { + std::unordered_map res; + for(auto const& m : this->modules) { + for(auto const& c : m.getCommands()) { + res.emplace(c.getGlobalIndex(), c.getActionName()); + } + } + return res; + } Command Program::synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector> const& commands) const { // To construct the synchronous product of the commands, we need to store a list of its updates. diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index f2b13781d..1b6f994e9 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -443,6 +443,11 @@ namespace storm { * @return The manager responsible for the expressions of this program. */ storm::expressions::ExpressionManager& getManager(); + + /*! + * + */ + std::unordered_map buildCommandIndexToActionNameMap() const; private: /*! diff --git a/src/utility/vector.h b/src/utility/vector.h index 621c84b2f..badb75c48 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -654,6 +654,17 @@ namespace storm { return resultVector; } + + template + std::vector filterVector(std::vector const& in, storm::storage::BitVector const& filter) { + std::vector result; + result.reserve(filter.getNumberOfSetBits()); + for(auto index : filter) { + result.push_back(in[index]); + } + assert(result.size() == filter.getNumberOfSetBits()); + return result; + } } // namespace vector } // namespace utility } // namespace storm