From eacdec393989fb220779301607d364d9d1a6d501 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 8 Oct 2015 14:37:00 +0200 Subject: [PATCH 1/5] State Annotation and subMDP also restrichts choicelabelling now Former-commit-id: 0df7a93f3bfd376ef9edc5a9dd851af046b3a9c7 --- src/models/sparse/Mdp.cpp | 9 ++++++++- src/models/sparse/StateAnnotation.h | 16 ++++++++++++++++ 2 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 src/models/sparse/StateAnnotation.h 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 From ecb214bc10fbab7194a9fb03043c88c1b138ffd6 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 8 Oct 2015 14:37:26 +0200 Subject: [PATCH 2/5] StateInfo is a StateAnnotation now Former-commit-id: d65584b97da1ffe63c36ef699efe41cc0efd9919 --- src/builder/ExplicitPrismModelBuilder.h | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) 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; From f914c8a103da93ca393b3fcea1d4da9a4857219c Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 8 Oct 2015 14:38:13 +0200 Subject: [PATCH 3/5] Filter std::vector by bitvector, could not find such a method before :/ Former-commit-id: b401646d07f78d99bebeb436520b0c20f34ba1bc --- src/utility/vector.h | 11 +++++++++++ 1 file changed, 11 insertions(+) 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 From 66736c36264d53e6e53bfa980db6d7a1572012ae Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 8 Oct 2015 14:38:55 +0200 Subject: [PATCH 4/5] More to string methods for simplevaluation Former-commit-id: 487ed4a8d6bf62034f32a3a19191bfe04e699be0 --- src/storage/expressions/SimpleValuation.cpp | 68 +++++++++++++++------ src/storage/expressions/SimpleValuation.h | 4 +- 2 files changed, 51 insertions(+), 21 deletions(-) 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: From ee0e34146f68e4e0240cd31a5ab390717cacbeff Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 8 Oct 2015 14:40:37 +0200 Subject: [PATCH 5/5] build command index to action name mapping Former-commit-id: a9b6c19e68fe0acea0846403de37d95acfd01201 --- src/storage/prism/Program.cpp | 10 ++++++++++ src/storage/prism/Program.h | 5 +++++ 2 files changed, 15 insertions(+) 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: /*!