From 464bdc389c08f89c742e8c66924c79462633fb7c Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 24 May 2017 18:19:42 +0200 Subject: [PATCH] improved state valuations class --- src/storm/builder/BuilderOptions.cpp | 11 ++++++- src/storm/builder/BuilderOptions.h | 5 +++ src/storm/builder/ExplicitModelBuilder.cpp | 7 +++-- src/storm/builder/ExplicitModelBuilder.h | 13 +++----- src/storm/models/sparse/StateAnnotation.h | 2 +- src/storm/storage/sparse/StateValuations.cpp | 32 ++++++++++++++++++-- src/storm/storage/sparse/StateValuations.h | 28 ++++++++++++++--- 7 files changed, 77 insertions(+), 21 deletions(-) diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 1d291af02..453f2e548 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -35,7 +35,7 @@ namespace storm { return boost::get(labelOrExpression); } - BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildChoiceOrigins(false), explorationChecks(false) { + BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false) { // Intentionally left empty. } @@ -139,6 +139,10 @@ namespace storm { return buildChoiceLabels; } + bool BuilderOptions::isBuildStateValuationsSet() const { + return buildStateValuations; + } + bool BuilderOptions::isBuildChoiceOriginsSet() const { return buildChoiceOrigins; } @@ -201,6 +205,11 @@ namespace storm { buildChoiceLabels = newValue; return *this; } + + BuilderOptions& BuilderOptions::setBuildStateValuations(bool newValue) { + buildStateValuations = newValue; + return *this; + } BuilderOptions& BuilderOptions::setBuildChoiceOrigins(bool newValue) { buildChoiceOrigins = newValue; diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index 1485c1113..b2923f4f5 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -89,6 +89,7 @@ namespace storm { bool hasTerminalStates() const; void clearTerminalStates(); bool isBuildChoiceLabelsSet() const; + bool isBuildStateValuationsSet() const; bool isBuildChoiceOriginsSet() const; bool isBuildAllRewardModelsSet() const; bool isBuildAllLabelsSet() const; @@ -102,6 +103,7 @@ namespace storm { BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); BuilderOptions& addTerminalLabel(std::string const& label, bool value); BuilderOptions& setBuildChoiceLabels(bool newValue); + BuilderOptions& setBuildStateValuations(bool newValue); BuilderOptions& setBuildChoiceOrigins(bool newValue); BuilderOptions& setExplorationChecks(bool newValue); @@ -128,6 +130,9 @@ namespace storm { /// A flag indicating whether or not to build choice labels. bool buildChoiceLabels; + /// A flag indicating whether or not to build for each state the variable valuation from which it originates. + bool buildStateValuations; + // A flag that indicates whether or not to generate the information from which parts of the model specification // each choice originates. bool buildChoiceOrigins; diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index b932b86ef..1a3feb96b 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -308,11 +308,12 @@ namespace storm { modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount()); // if requested, build the state valuations and choice origins - if (options.buildStateValuations) { - modelComponents.stateValuations = std::make_shared(stateStorage.getNumberOfStates()); + if (generator->getOptions().isBuildStateValuationsSet()) { + std::vector valuations(modelComponents.transitionMatrix.getRowGroupCount()); for (auto const& bitVectorIndexPair : stateStorage.stateToId) { - modelComponents.stateValuations->valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first); + valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first); } + modelComponents.stateValuations = storm::storage::sparse::StateValuations(std::move(valuations)); } auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount()); modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData); diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index 9e540b32c..aa64be986 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -16,7 +16,6 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/BitVectorHashMap.h" #include "storm/logic/Formulas.h" -#include "storm/models/sparse/StateAnnotation.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/StateLabeling.h" #include "storm/models/sparse/ChoiceLabeling.h" @@ -70,11 +69,11 @@ namespace storm { // A vector that stores which states are markovian. boost::optional markovianStates; - // Stores for each state to which variable valuation it belongs (is nullptr if not generated) - std::shared_ptr stateValuations; + // If generated, stores for each state to which variable valuation it belongs + boost::optional stateValuations; - // Stores for each choice from which parts of the input model description it originates (is nullptr if not generated) - std::shared_ptr choiceOrigins; + // If generated, stores for each choice from which parts of the input model description it originates + boost::optional> choiceOrigins; }; @@ -86,10 +85,6 @@ namespace storm { // The order in which to explore the model. ExplorationOrder explorationOrder; - - // A flag that indicates whether or not to store the state information after successfully building the - // model. If it is to be preserved, it is contained in the result obtained from build - bool buildStateValuations; }; /*! diff --git a/src/storm/models/sparse/StateAnnotation.h b/src/storm/models/sparse/StateAnnotation.h index 114341d74..b42e2c9be 100644 --- a/src/storm/models/sparse/StateAnnotation.h +++ b/src/storm/models/sparse/StateAnnotation.h @@ -9,7 +9,7 @@ namespace storm { class StateAnnotation { public: - virtual std::string stateInfo(storm::storage::sparse::state_type const& state) const = 0; + virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const = 0; }; } diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp index 67fecba45..0ad9774b1 100644 --- a/src/storm/storage/sparse/StateValuations.cpp +++ b/src/storm/storage/sparse/StateValuations.cpp @@ -1,17 +1,43 @@ #include "storm/storage/sparse/StateValuations.h" +#include "storm/utility/vector.h" + namespace storm { namespace storage { namespace sparse { - StateValuations::StateValuations(state_type const& numberOfStates) : valuations(numberOfStates) { + StateValuations::StateValuations(std::vector const& valuations) : valuations(valuations) { // Intentionally left empty. } - std::string StateValuations::stateInfo(state_type const& state) const { - return valuations[state].toString(); + StateValuations::StateValuations(std::vector&& valuations) : valuations(std::move(valuations)) { + // Intentionally left empty. } + std::string StateValuations::getStateInfo(state_type const& state) const { + return getStateValuation(state).toString(); + } + + storm::expressions::SimpleValuation const& StateValuations::getStateValuation(storm::storage::sparse::state_type const& state) const { + return valuations[state]; + } + + StateValuations StateValuations::selectStates(storm::storage::BitVector const& selectedStates) const { + return StateValuations(storm::utility::vector::filterVector(valuations, selectedStates)); + } + + StateValuations StateValuations::selectStates(std::vector const& selectedStates) const { + std::vector selectedValuations; + selectedValuations.reserve(selectedStates.size()); + for (auto const& selectedState : selectedStates){ + if (selectedState < valuations.size()) { + selectedValuations.push_back(valuations[selectedState]); + } else { + selectedValuations.emplace_back(); + } + } + return StateValuations(std::move(selectedValuations)); + } } } } diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h index 58d28324f..e742505cb 100644 --- a/src/storm/storage/sparse/StateValuations.h +++ b/src/storm/storage/sparse/StateValuations.h @@ -5,8 +5,8 @@ #include #include "storm/storage/sparse/StateType.h" +#include "storm/storage/BitVector.h" #include "storm/storage/expressions/SimpleValuation.h" - #include "storm/models/sparse/StateAnnotation.h" namespace storm { @@ -14,18 +14,38 @@ namespace storm { namespace sparse { // A structure holding information about the reachable state space that can be retrieved from the outside. - struct StateValuations : public storm::models::sparse::StateAnnotation { + class StateValuations : public storm::models::sparse::StateAnnotation { + + public: /*! * Constructs a state information object for the given number of states. */ - StateValuations(state_type const& numberOfStates); + StateValuations(std::vector const& valuations); + StateValuations(std::vector&& valuations); virtual ~StateValuations() = default; + virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override; + storm::expressions::SimpleValuation const& getStateValuation(storm::storage::sparse::state_type const& state) const; + + /* + * Derive new state valuations from this by selecting the given states. + */ + StateValuations selectStates(storm::storage::BitVector const& selectedStates) const; + + /* + * Derive new state valuations from this by selecting the given states. + * If an invalid state index is selected, the corresponding valuation will be empty. + */ + StateValuations selectStates(std::vector const& selectedStates) const; + + + + private: + // A mapping from state indices to their variable valuations. std::vector valuations; - virtual std::string stateInfo(state_type const& state) const override; }; }