From adfdf8c572db808493ce1f47c5b12d93b0387fed Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 25 May 2020 16:38:58 +0200 Subject: [PATCH] Refactored state valuations. They now store values for transient jani variables and do not store values for constants (solving Github issue #73) --- src/storm/builder/ExplicitModelBuilder.cpp | 23 +- src/storm/builder/ExplicitModelBuilder.h | 5 +- .../generator/JaniNextStateGenerator.cpp | 90 +++++++- src/storm/generator/JaniNextStateGenerator.h | 10 +- src/storm/generator/NextStateGenerator.cpp | 29 ++- src/storm/generator/NextStateGenerator.h | 9 +- src/storm/storage/Scheduler.cpp | 2 +- src/storm/storage/sparse/StateValuations.cpp | 217 +++++++++++++++++- src/storm/storage/sparse/StateValuations.h | 99 ++++++-- 9 files changed, 433 insertions(+), 51 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 0dad59191..b4be0dd6a 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -105,7 +105,7 @@ namespace storm { } template - void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianStates) { + void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianStates, boost::optional& stateValuationsBuilder) { // Create markovian states bit vector, if required. if (generator->getModelType() == storm::generator::ModelType::MA) { @@ -154,6 +154,9 @@ namespace storm { } generator->load(currentState); + if (stateValuationsBuilder) { + generator->addStateValuation(currentIndex, stateValuationsBuilder.get()); + } storm::generator::StateBehavior behavior = generator->expand(stateToIdCallback); // If there is no behavior, we might have to introduce a self-loop. @@ -188,7 +191,7 @@ namespace storm { ++currentRow; ++currentRowGroup; } else { - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state (" << generator->toValuation(currentState).toString(true) << "). For fixing these, please provide the appropriate option."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state (" << generator->stateToString(currentState) << "). For fixing these, please provide the appropriate option."); } } else { // Add the state rewards to the corresponding reward models. @@ -314,7 +317,13 @@ namespace storm { ChoiceInformationBuilder choiceInformationBuilder; boost::optional markovianStates; - buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates); + // If we need to build state valuations, initialize them now. + boost::optional stateValuationsBuilder; + if (generator->getOptions().isBuildStateValuationsSet()) { + stateValuationsBuilder = generator->initializeStateValuationsBuilder(); + } + + buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, stateValuationsBuilder); // Initialize the model components with the obtained information. storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); @@ -327,12 +336,8 @@ namespace storm { modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount()); // If requested, build the state valuations and choice origins - if (generator->getOptions().isBuildStateValuationsSet()) { - std::vector valuations(modelComponents.transitionMatrix.getRowGroupCount()); - for (auto const& bitVectorIndexPair : stateStorage.stateToId) { - valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first); - } - modelComponents.stateValuations = storm::storage::sparse::StateValuations(std::move(valuations)); + if (stateValuationsBuilder) { + modelComponents.stateValuations = stateValuationsBuilder->build(modelComponents.transitionMatrix.getRowGroupCount()); } if (generator->getOptions().isBuildChoiceOriginsSet()) { auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount()); diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index 58be400ab..4a94ad724 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -107,9 +107,10 @@ namespace storm { * @param transitionMatrixBuilder The builder of the transition matrix. * @param rewardModelBuilders The builders for the selected reward models. * @param choiceInformationBuilder The builder for the requested information of the choices - * @param markovianChoices is set to a bit vector storing whether a choice is markovian (is only set if the model type requires this information). + * @param markovianChoices is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information). + * @param stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states */ - void buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianChoices); + void buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianChoices, boost::optional& stateValuationsBuilder); /*! * Explores the state space of the given program and returns the components of the model as a result. diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 87baa0b98..0506629f1 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -394,7 +394,7 @@ namespace storm { } template - void JaniNextStateGenerator::applyTransientUpdate(TransientVariableValuation& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator const& expressionEvaluator) { + void JaniNextStateGenerator::applyTransientUpdate(TransientVariableValuation& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator const& expressionEvaluator) const { auto assignmentIt = transientAssignments.begin(); auto assignmentIte = transientAssignments.end(); @@ -457,15 +457,7 @@ namespace storm { } template - StateBehavior JaniNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { - // Prepare the result, in case we return early. - StateBehavior result; - - // Retrieve the locations from the state. - std::vector locations = getLocations(*this->state); - - // First, construct the state rewards, as we may return early if there are no choices later and we already - // need the state rewards then. + TransientVariableValuation JaniNextStateGenerator::getTransientVariableValuationAtLocations(std::vector const& locations) const { uint64_t automatonIndex = 0; TransientVariableValuation transientVariableValuation; for (auto const& automatonRef : this->parallelAutomata) { @@ -476,6 +468,84 @@ namespace storm { applyTransientUpdate(transientVariableValuation, location.getAssignments().getTransientAssignments(), *this->evaluator); ++automatonIndex; } + return transientVariableValuation; + } + + template + storm::storage::sparse::StateValuationsBuilder JaniNextStateGenerator::initializeStateValuationsBuilder() const { + auto result = NextStateGenerator::initializeStateValuationsBuilder(); + // Also add information for transient variables + for (auto const& varInfo : transientVariableInformation.booleanVariableInformation) { + result.addVariable(varInfo.variable); + } + for (auto const& varInfo : transientVariableInformation.integerVariableInformation) { + result.addVariable(varInfo.variable); + } + for (auto const& varInfo : transientVariableInformation.rationalVariableInformation) { + result.addVariable(varInfo.variable); + } + return result; + } + + template + void JaniNextStateGenerator::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const { + std::vector booleanValues; + booleanValues.reserve(this->variableInformation.booleanVariables.size() + transientVariableInformation.booleanVariableInformation.size()); + std::vector integerValues; + integerValues.reserve(this->variableInformation.locationVariables.size() + this->variableInformation.integerVariables.size() + transientVariableInformation.integerVariableInformation.size()); + std::vector rationalValues; + rationalValues.reserve(transientVariableInformation.rationalVariableInformation.size()); + + // Add values for non-transient variables + extractVariableValues(*this->state, this->variableInformation, integerValues, booleanValues, integerValues); + + // Add values for transient variables + auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(*this->state)); + { + auto varIt = transientVariableValuation.booleanValues.begin(); + for (auto const& varInfo : transientVariableInformation.booleanVariableInformation) { + if (varIt->first->variable == varInfo.variable) { + booleanValues.push_back(varIt->second); + } else { + booleanValues.push_back(varInfo.defaultValue); + } + } + } + { + auto varIt = transientVariableValuation.integerValues.begin(); + for (auto const& varInfo : transientVariableInformation.integerVariableInformation) { + if (varIt->first->variable == varInfo.variable) { + integerValues.push_back(varIt->second); + } else { + integerValues.push_back(varInfo.defaultValue); + } + } + } + { + auto varIt = transientVariableValuation.rationalValues.begin(); + for (auto const& varInfo : transientVariableInformation.rationalVariableInformation) { + if (varIt->first->variable == varInfo.variable) { + rationalValues.push_back(storm::utility::convertNumber(varIt->second)); + } else { + rationalValues.push_back(storm::utility::convertNumber(varInfo.defaultValue)); + } + } + } + + valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); + } + + template + StateBehavior JaniNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { + // Prepare the result, in case we return early. + StateBehavior result; + + // Retrieve the locations from the state. + std::vector locations = getLocations(*this->state); + + // First, construct the state rewards, as we may return early if there are no choices later and we already + // need the state rewards then. + auto transientVariableValuation = getTransientVariableValuationAtLocations(locations); transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); result.addStateRewards(evaluateRewardExpressions()); this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 74ead73e6..de4fe24ed 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -50,8 +50,14 @@ namespace storm { virtual bool isPartiallyObservable() const override; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; + /// Initializes a builder for state valuations by adding the appropriate variables. + virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const override; + virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; + /// Adds the valuation for the currently loaded state to the given builder + virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const override; + virtual std::size_t getNumberOfRewardModels() const override; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; @@ -102,7 +108,7 @@ namespace storm { * @params assignmentLevel The assignmentLevel that is to be considered for the update. * @return The resulting state. */ - void applyTransientUpdate(TransientVariableValuation& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator const& expressionEvaluator); + void applyTransientUpdate(TransientVariableValuation& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator const& expressionEvaluator) const; /** * Required method to overload, but currently throws an error as POMDPs are not yet specified in JANI. @@ -113,6 +119,8 @@ namespace storm { */ virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const override; + TransientVariableValuation getTransientVariableValuationAtLocations(std::vector const& locations) const; + /*! * Retrieves all choices possible from the given state. * diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index fd4578235..e83c9338d 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -47,6 +47,21 @@ namespace storm { return variableInformation.getTotalBitOffset(true); } + template + storm::storage::sparse::StateValuationsBuilder NextStateGenerator::initializeStateValuationsBuilder() const { + storm::storage::sparse::StateValuationsBuilder result; + for (auto const& v : variableInformation.locationVariables) { + result.addVariable(v.variable); + } + for (auto const& v : variableInformation.booleanVariables) { + result.addVariable(v.variable); + } + for (auto const& v : variableInformation.integerVariables) { + result.addVariable(v.variable); + } + return result; + } + template void NextStateGenerator::load(CompressedState const& state) { // Since almost all subsequent operations are based on the evaluator, we load the state into it now. @@ -64,6 +79,16 @@ namespace storm { return evaluator->asBool(expression); } + template + void NextStateGenerator::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const { + std::vector booleanValues; + booleanValues.reserve(variableInformation.booleanVariables.size()); + std::vector integerValues; + integerValues.reserve(variableInformation.locationVariables.size() + variableInformation.integerVariables.size()); + extractVariableValues(*this->state, variableInformation, integerValues, booleanValues, integerValues); + valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues)); + } + template storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions) { @@ -168,8 +193,8 @@ namespace storm { } template - storm::expressions::SimpleValuation NextStateGenerator::toValuation(CompressedState const& state) const { - return unpackStateIntoValuation(state, variableInformation, *expressionManager); + std::string NextStateGenerator::stateToString(CompressedState const& state) const { + return toString(state, variableInformation); } template diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index fb72de23f..c329f34d6 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -10,6 +10,7 @@ #include "storm/storage/sparse/StateStorage.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/sparse/ChoiceOrigins.h" +#include "storm/storage/sparse/StateValuations.h" #include "storm/builder/BuilderOptions.h" #include "storm/builder/RewardModelInformation.h" @@ -54,14 +55,20 @@ namespace storm { virtual bool isPartiallyObservable() const = 0; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) = 0; + /// Initializes a builder for state valuations by adding the appropriate variables. + virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const; + void load(CompressedState const& state); virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) = 0; bool satisfies(storm::expressions::Expression const& expression) const; + /// Adds the valuation for the currently loaded state to the given builder + virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const; + virtual std::size_t getNumberOfRewardModels() const = 0; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0; - storm::expressions::SimpleValuation toValuation(CompressedState const& state) const; + std::string stateToString(CompressedState const& state) const; uint32_t observabilityClass(CompressedState const& state) const; diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 673a64173..5fbf8bd94 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -241,7 +241,7 @@ namespace storm { } storm::json stateChoicesJson; if (model && model->hasStateValuations()) { - stateChoicesJson["s"] = model->getStateValuations().getStateValuation(state).toJson(); + stateChoicesJson["s"] = model->getStateValuations()[state].toJson(model->getStateValuations()); } else { stateChoicesJson["s"] = state; } diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp index 833ed9399..93409c860 100644 --- a/src/storm/storage/sparse/StateValuations.cpp +++ b/src/storm/storage/sparse/StateValuations.cpp @@ -1,24 +1,184 @@ #include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/BitVector.h" + #include "storm/utility/vector.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidTypeException.h" namespace storm { namespace storage { namespace sparse { - StateValuations::StateValuations(std::vector const& valuations) : valuations(valuations) { - // Intentionally left empty. + StateValuation::StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)) { + // Intentionally left empty } - - StateValuations::StateValuations(std::vector&& valuations) : valuations(std::move(valuations)) { - // Intentionally left empty. + + bool StateValuation::getBooleanValue(StateValuations const& valuations, storm::expressions::Variable const& booleanVariable) const { + STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations"); + STORM_LOG_ASSERT(valuations.variableToIndexMap.count(booleanVariable) > 0, "Variable " << booleanVariable.getName() << " is not part of this valuation."); + return booleanValues[valuations.variableToIndexMap.at(booleanVariable)]; + } + + int64_t const& StateValuation::getIntegerValue(StateValuations const& valuations, storm::expressions::Variable const& integerVariable) const { + STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations"); + STORM_LOG_ASSERT(valuations.variableToIndexMap.count(integerVariable) > 0, "Variable " << integerVariable.getName() << " is not part of this valuation."); + return integerValues[valuations.variableToIndexMap.at(integerVariable)]; + } + + storm::RationalNumber const& StateValuation::getRationalValue(StateValuations const& valuations, storm::expressions::Variable const& rationalVariable) const { + STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations"); + STORM_LOG_ASSERT(valuations.variableToIndexMap.count(rationalVariable) > 0, "Variable " << rationalVariable.getName() << " is not part of this valuation."); + return rationalValues[valuations.variableToIndexMap.at(rationalVariable)]; + } + + bool StateValuation::isEmpty() const { + return booleanValues.empty() && integerValues.empty() && rationalValues.empty(); + } + + std::string StateValuation::toString(StateValuations const& valuations, bool pretty, boost::optional> const& selectedVariables) const { + STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations"); + typename std::map::const_iterator mapIt = valuations.variableToIndexMap.begin(); + typename std::set::const_iterator setIt; + if (selectedVariables) { + setIt = selectedVariables->begin(); + } + std::vector assignments; + while (mapIt != valuations.variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) { + + // Move Map iterator to next relevant position + if (selectedVariables) { + while (mapIt->first != *setIt) { + ++mapIt; + STORM_LOG_ASSERT(mapIt != valuations.variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << "."); + } + } + + auto const& variable = mapIt->first; + std::stringstream stream; + if (pretty) { + if (variable.hasBooleanType() && !booleanValues[mapIt->second]) { + stream << "!"; + } + stream << variable.getName(); + if (variable.hasIntegerType()) { + stream << "=" << integerValues[mapIt->second]; + } else if (variable.hasRationalType()) { + stream << "=" << rationalValues[mapIt->second]; + } else { + STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidTypeException, "Unexpected variable type."); + } + } else { + if (variable.hasBooleanType()) { + stream << std::boolalpha << booleanValues[mapIt->second] << std::noboolalpha; + } else if (variable.hasIntegerType()) { + stream << integerValues[mapIt->second]; + } else if (variable.hasRationalType()) { + stream << rationalValues[mapIt->second]; + } + } + assignments.push_back(stream.str()); + + // Go to next position + if (selectedVariables) { + ++setIt; + } else { + ++mapIt; + } + } + if (pretty) { + return "[" + boost::join(assignments, "\t& ") + "]"; + } else { + return "[" + boost::join(assignments, "\t") + "]"; + } + } + + typename StateValuation::Json StateValuation::toJson(StateValuations const& valuations, boost::optional> const& selectedVariables) const { + STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations"); + typename std::map::const_iterator mapIt = valuations.variableToIndexMap.begin(); + typename std::set::const_iterator setIt; + if (selectedVariables) { + setIt = selectedVariables->begin(); + } + Json result; + while (mapIt != valuations.variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) { + // Move Map iterator to next relevant position + if (selectedVariables) { + while (mapIt->first != *setIt) { + ++mapIt; + STORM_LOG_ASSERT(mapIt != valuations.variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << "."); + } + } + + auto const& variable = mapIt->first; + if (variable.hasBooleanType()) { + result[variable.getName()] = bool(booleanValues[mapIt->second]); + } else if (variable.hasIntegerType()) { + result[variable.getName()] = integerValues[mapIt->second]; + } else if (variable.hasRationalType()) { + result[variable.getName()] = rationalValues[mapIt->second]; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); + } + + // Go to next position + if (selectedVariables) { + ++setIt; + } else { + ++mapIt; + } + } + return result; + } + + bool StateValuation::assertValuations(StateValuations const& valuations) const { + storm::storage::BitVector foundBooleanValues(booleanValues.size(), false); + storm::storage::BitVector foundIntegerValues(integerValues.size(), false); + storm::storage::BitVector foundRationalValues(rationalValues.size(), false); + for (auto const& varIndex : valuations.variableToIndexMap) { + storm::storage::BitVector* bv; + if (varIndex.first.hasBooleanType()) { + bv = &foundBooleanValues; + } else if (varIndex.first.hasIntegerType()) { + bv = &foundIntegerValues; + } else if (varIndex.first.hasRationalType()) { + bv = &foundRationalValues; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); + } + if (varIndex.second < bv->size()) { + if (bv->get(varIndex.second)) { + STORM_LOG_ERROR("Multiple variables refer to the same value index"); + return false; + } + bv->set(varIndex.second, true); + } else { + STORM_LOG_ERROR("Valuation does not provide a value for all variables"); + return false; + } + } + if (!(foundBooleanValues.full() && foundIntegerValues.full() && foundRationalValues.full())) { + STORM_LOG_ERROR("Valuation has too many entries."); + } + return true; + } + + StateValuations::StateValuations(std::map const& variableToIndexMap, std::vector&& valuations) : variableToIndexMap(variableToIndexMap), valuations(valuations) { + // Intentionally left empty } std::string StateValuations::getStateInfo(state_type const& state) const { - return getStateValuation(state).toString(); + STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index."); + return (*this)[state].toString(*this); + } + + StateValuation& StateValuations::operator[](storm::storage::sparse::state_type const& state) { + STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index."); + return valuations[state]; } - storm::expressions::SimpleValuation const& StateValuations::getStateValuation(storm::storage::sparse::state_type const& state) const { + StateValuation const& StateValuations::operator[](storm::storage::sparse::state_type const& state) const { + STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index."); return valuations[state]; } @@ -27,11 +187,11 @@ namespace storm { } StateValuations StateValuations::selectStates(storm::storage::BitVector const& selectedStates) const { - return StateValuations(storm::utility::vector::filterVector(valuations, selectedStates)); + return StateValuations(variableToIndexMap, storm::utility::vector::filterVector(valuations, selectedStates)); } StateValuations StateValuations::selectStates(std::vector const& selectedStates) const { - std::vector selectedValuations; + std::vector selectedValuations; selectedValuations.reserve(selectedStates.size()); for (auto const& selectedState : selectedStates){ if (selectedState < valuations.size()) { @@ -40,7 +200,44 @@ namespace storm { selectedValuations.emplace_back(); } } - return StateValuations(std::move(selectedValuations)); + return StateValuations(variableToIndexMap, std::move(selectedValuations)); + } + + StateValuationsBuilder::StateValuationsBuilder() : booleanVarCount(0), integerVarCount(0), rationalVarCount(0) { + // Intentionally left empty. + } + + void StateValuationsBuilder::addVariable(storm::expressions::Variable const& variable) { + STORM_LOG_ASSERT(currentStateValuations.valuations.empty(), "Tried to add a variable, although a state has already been added before."); + STORM_LOG_ASSERT(currentStateValuations.variableToIndexMap.count(variable) == 0, "Variable " << variable.getName() << " already added."); + if (variable.hasBooleanType()) { + currentStateValuations.variableToIndexMap[variable] = booleanVarCount++; + } + if (variable.hasIntegerType()) { + currentStateValuations.variableToIndexMap[variable] = integerVarCount++; + } + if (variable.hasRationalType()) { + currentStateValuations.variableToIndexMap[variable] = rationalVarCount++; + } + } + + void StateValuationsBuilder::addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues) { + if (state > currentStateValuations.valuations.size()) { + currentStateValuations.valuations.resize(state); + } + if (state == currentStateValuations.valuations.size()) { + currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); + } else { + STORM_LOG_ASSERT(currentStateValuations[state].isEmpty(), "Adding a valuation to the same state multiple times."); + currentStateValuations[state] = StateValuation(std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); + } + } + + StateValuations StateValuationsBuilder::build(std::size_t totalStateCount) { + return std::move(currentStateValuations); + booleanVarCount = 0; + integerVarCount = 0; + rationalVarCount = 0; } } } diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h index 84d5b7c2d..873f49f33 100644 --- a/src/storm/storage/sparse/StateValuations.h +++ b/src/storm/storage/sparse/StateValuations.h @@ -1,35 +1,77 @@ -#ifndef STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ -#define STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ +#pragma once #include #include #include "storm/storage/sparse/StateType.h" #include "storm/storage/BitVector.h" -#include "storm/storage/expressions/SimpleValuation.h" +#include "storm/storage/expressions/Variable.h" #include "storm/models/sparse/StateAnnotation.h" +#include "storm/adapters/JsonAdapter.h" namespace storm { namespace storage { namespace sparse { - // A structure holding information about the reachable state space that can be retrieved from the outside. - class StateValuations : public storm::models::sparse::StateAnnotation { + class StateValuations; + class StateValuationsBuilder; + class StateValuation { public: + typedef storm::json Json; + StateValuation() = default; + StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues); + + bool getBooleanValue(StateValuations const& valuations, storm::expressions::Variable const& booleanVariable) const; + int64_t const& getIntegerValue(StateValuations const& valuations, storm::expressions::Variable const& integerVariable) const; + storm::RationalNumber const& getRationalValue(StateValuations const& valuations, storm::expressions::Variable const& rationalVariable) const; + + // Returns true, if this valuation does not contain any value. + bool isEmpty() const; + /*! - * Constructs a state information object for the given number of states. + * Returns a string representation of the valuation. + * + * @param selectedVariables If given, only the informations for the variables in this set are processed. + * @return The string representation. */ - StateValuations(std::vector const& valuations); - StateValuations(std::vector&& valuations); + std::string toString(StateValuations const& valuations, bool pretty = true, boost::optional> const& selectedVariables = boost::none) const; - virtual ~StateValuations() = default; + /*! + * Returns a JSON representation of this valuation + * @param selectedVariables If given, only the informations for the variables in this set are processed. + * @return + */ + Json toJson(StateValuations const& valuations, boost::optional> const& selectedVariables = boost::none) const; + + private: + // Asserts whether the variable and value counts for each type match. + bool assertValuations(StateValuations const& valuations) const; + + std::vector booleanValues; + std::vector integerValues; + std::vector rationalValues; + }; + + // A structure holding information about the reachable state space that can be retrieved from the outside. + class StateValuations : public storm::models::sparse::StateAnnotation { + public: + friend class StateValuation; + friend class StateValuationsBuilder; + + StateValuations() = default; + 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; + /*! + * Returns the valuation at the specific state + */ + StateValuation& operator[](storm::storage::sparse::state_type const& state); + StateValuation const& operator[](storm::storage::sparse::state_type const& state) const; + - // Returns the number of states that this object describes. + // Returns the (current) number of states that this object describes. uint_fast64_t getNumberOfStates() const; /* @@ -45,14 +87,41 @@ namespace storm { private: - + StateValuations(std::map const& variableToIndexMap, std::vector&& valuations); + std::map variableToIndexMap; // A mapping from state indices to their variable valuations. - std::vector valuations; + std::vector valuations; }; + class StateValuationsBuilder { + public: + StateValuationsBuilder(); + + /*! Adds a new variable to keep track of for the state valuations. + *! All variables need to be added before adding new states. + */ + void addVariable(storm::expressions::Variable const& variable); + + /*! + * Adds a new state. + * The variable values have to be given in the same order as the variables have been added. + * The number of given variable values for each type needs to match the number of added variables. + * After calling this method, no more variables should be added. + */ + void addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues = {}, std::vector&& integerValues = {}, std::vector&& rationalValues = {}); + + /*! + * Creates the finalized state valuations object. + */ + StateValuations build(std::size_t totalStateCount); + + private: + StateValuations currentStateValuations; + uint64_t booleanVarCount; + uint64_t integerVarCount; + uint64_t rationalVarCount; + }; } } } - -#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */