From 09dcb149c253b9e781b4fd4495156fe1ed8262d6 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 17 Aug 2017 23:48:01 +0200 Subject: [PATCH] storm parses and builds pomdps --- src/storm/builder/ExplicitModelBuilder.cpp | 9 ++++- src/storm/generator/CompressedState.cpp | 40 +++++++++++++++++++++ src/storm/generator/CompressedState.h | 6 +++- src/storm/generator/NextStateGenerator.cpp | 11 ++++++ src/storm/generator/NextStateGenerator.h | 11 +++++- src/storm/generator/VariableInformation.cpp | 24 ++++++------- src/storm/generator/VariableInformation.h | 14 +++++--- src/storm/models/sparse/Pomdp.cpp | 26 ++++++++++++-- src/storm/models/sparse/Pomdp.h | 10 +++++- src/storm/storage/sparse/ModelComponents.h | 2 +- 10 files changed, 129 insertions(+), 24 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 34c56ca04..79d6fc15d 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -328,7 +328,14 @@ namespace storm { auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount()); modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData); } - + if (generator->isPartiallyObservable()) { + std::vector classes; + classes.resize(stateStorage.getNumberOfStates()); + for (auto const& bitVectorIndexPair : stateStorage.stateToId) { + classes[bitVectorIndexPair.second] = generator->observabilityClass(bitVectorIndexPair.first); + } + modelComponents.observabilityClasses = classes; + } return modelComponents; } diff --git a/src/storm/generator/CompressedState.cpp b/src/storm/generator/CompressedState.cpp index a785f1c79..1711242b9 100644 --- a/src/storm/generator/CompressedState.cpp +++ b/src/storm/generator/CompressedState.cpp @@ -43,6 +43,46 @@ namespace storm { return result; } + storm::storage::BitVector computeObservabilityMask(VariableInformation const& variableInformation) { + storm::storage::BitVector result(variableInformation.getTotalBitOffset(true)); + for (auto const& locationVariable : variableInformation.locationVariables) { + if (locationVariable.observable) { + for (uint64_t i = locationVariable.bitOffset; i < locationVariable.bitOffset + locationVariable.bitWidth; ++i) { + result.set(i, true); + } + } + } + + for (auto const& booleanVariable : variableInformation.booleanVariables) { + if (booleanVariable.observable) { + result.set(booleanVariable.bitOffset, true); + } + } + + for (auto const& integerVariable : variableInformation.integerVariables) { + if (integerVariable.observable) { + for (uint64_t i = integerVariable.bitOffset; i < integerVariable.bitOffset + integerVariable.bitWidth; ++i) { + result.set(i, true); + } + } + } + return result; + } + + uint32_t unpackStateToObservabilityClass(CompressedState const& state, std::unordered_map& observabilityMap, storm::storage::BitVector const& mask) { + STORM_LOG_ASSERT(state.size() == mask.size(), "Mask should be as long as state."); + storm::storage::BitVector observeClass = state & mask; + auto it = observabilityMap.find(observeClass); + if (it != observabilityMap.end()) { + return it->second; + } else { + uint32_t newClassIndex = observabilityMap.size(); + observabilityMap.emplace(observeClass, newClassIndex); + return newClassIndex; + } + } + + template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager); diff --git a/src/storm/generator/CompressedState.h b/src/storm/generator/CompressedState.h index 1a785dbaa..3cbac6e79 100644 --- a/src/storm/generator/CompressedState.h +++ b/src/storm/generator/CompressedState.h @@ -2,6 +2,7 @@ #define STORM_GENERATOR_COMPRESSEDSTATE_H_ #include "storm/storage/BitVector.h" +#include namespace storm { namespace expressions { @@ -12,7 +13,6 @@ namespace storm { } namespace generator { - typedef storm::storage::BitVector CompressedState; struct VariableInformation; @@ -36,6 +36,10 @@ namespace storm { * @return A valuation that corresponds to the compressed state. */ storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager); + + storm::storage::BitVector computeObservabilityMask(VariableInformation const& variableInformation); + uint32_t unpackStateToObservabilityClass(CompressedState const& state, std::unordered_map& observabilityMap, storm::storage::BitVector const& mask); + } } diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index 15c6048c3..faaadf1ed 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -154,6 +154,17 @@ namespace storm { return nullptr; } + template + uint32_t NextStateGenerator::observabilityClass(CompressedState const &state) const { + if (this->mask.size() == 0) { + this->mask = computeObservabilityMask(variableInformation); + std::cout << mask.size() << std::endl; + } + std::cout << state.size() << std::endl; + + return unpackStateToObservabilityClass(state, observabilityMap, mask); + } + template class NextStateGenerator; #ifdef STORM_HAVE_CARL diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 678584730..ebd2a83f1 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -62,7 +62,9 @@ namespace storm { virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0; storm::expressions::SimpleValuation toValuation(CompressedState const& state) const; - + + uint32 observabilityClass(CompressedState const& state) const; + virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) = 0; NextStateGeneratorOptions const& getOptions() const; @@ -97,6 +99,13 @@ namespace storm { /// A comparator used to compare constants. storm::utility::ConstantsComparator comparator; + + /// The mask to compute the observability class (Constructed upon first use) + mutable storm::storage::BitVector mask; + + /// The observability classes handed out so far. + // TODO consider using a BitVectorHashMap for this? + mutable std::unordered_map observabilityMap; }; } } diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index e691300c6..62894270b 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -17,40 +17,40 @@ namespace storm { namespace generator { - BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global) : variable(variable), bitOffset(bitOffset), global(global) { + BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global, bool observable) : variable(variable), bitOffset(bitOffset), global(global), observable(observable) { // Intentionally left empty. } - IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth), global(global) { + IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global, bool observable) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth), global(global), observable(observable) { // Intentionally left empty. } - LocationVariableInformation::LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) { + LocationVariableInformation::LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool observable) : variable(variable), highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth), observable(observable) { // Intentionally left empty. } VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) { for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { - booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, true); + booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, true, booleanVariable.isObservable()); ++totalBitOffset; } for (auto const& integerVariable : program.getGlobalIntegerVariables()) { int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable()); totalBitOffset += bitwidth; } for (auto const& module : program.getModules()) { for (auto const& booleanVariable : module.getBooleanVariables()) { - booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset); + booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, false, booleanVariable.isObservable()); ++totalBitOffset; } for (auto const& integerVariable : module.getIntegerVariables()) { int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable()); totalBitOffset += bitwidth; } } @@ -69,7 +69,7 @@ namespace storm { for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { if (!variable.isTransient()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true, true); ++totalBitOffset; } } @@ -78,7 +78,7 @@ namespace storm { int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, true); totalBitOffset += bitwidth; } } @@ -92,12 +92,12 @@ namespace storm { void VariableInformation::createVariablesForAutomaton(storm::jani::Automaton const& automaton) { uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); - locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth); + locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth, true); totalBitOffset += bitwidth; for (auto const& variable : automaton.getVariables().getBooleanVariables()) { if (!variable.isTransient()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, false, true); ++totalBitOffset; } } @@ -106,7 +106,7 @@ namespace storm { int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, true); totalBitOffset += bitwidth; } } diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index 764881e80..98e846caf 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -17,10 +17,9 @@ namespace storm { } namespace generator { - // A structure storing information about the boolean variables of the model. struct BooleanVariableInformation { - BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global = false); + BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global, bool observable); // The boolean variable. storm::expressions::Variable variable; @@ -30,11 +29,14 @@ namespace storm { // A flag indicating whether the variable is a global one. bool global; + + // + bool observable; }; // A structure storing information about the integer variables of the model. struct IntegerVariableInformation { - IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global = false); + IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global, bool observable); // The integer variable. storm::expressions::Variable variable; @@ -53,11 +55,13 @@ namespace storm { // A flag indicating whether the variable is a global one. bool global; + + bool observable; }; // A structure storing information about the location variables of the model. struct LocationVariableInformation { - LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth); + LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool observable); // The expression variable for this location. storm::expressions::Variable variable; @@ -70,6 +74,8 @@ namespace storm { // Its bit width in the compressed state. uint_fast64_t bitWidth; + + bool observable; }; // A structure storing information about the used variables of the program. diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index 182374fac..b49e72cb4 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -15,13 +15,33 @@ namespace storm { } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components) : Mdp(components, storm::models::ModelType::Pomdp) { - + Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components) : Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()) { + computeNrObservations(); } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components): Mdp(components, storm::models::ModelType::Pomdp) { + Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components): Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()) { + computeNrObservations(); + } + + template + void Pomdp::printModelInformationToStream(std::ostream& out) const { + this->printModelInformationHeaderToStream(out); + out << "Choices: \t" << this->getNumberOfChoices() << std::endl; + out << "Observations: \t" << this->nrObservations << std::endl; + this->printModelInformationFooterToStream(out); + } + template + void Pomdp::computeNrObservations() { + uint64_t highestEntry = 0; + for (uint32_t entry : observations) { + if (entry > highestEntry) { + highestEntry = entry; + } + } + nrObservations = highestEntry; + // In debug mode, ensure that every observability is used. } diff --git a/src/storm/models/sparse/Pomdp.h b/src/storm/models/sparse/Pomdp.h index c981562e0..7be220743 100644 --- a/src/storm/models/sparse/Pomdp.h +++ b/src/storm/models/sparse/Pomdp.h @@ -53,8 +53,16 @@ namespace storm { Pomdp &operator=(Pomdp &&other) = default; + virtual void printModelInformationToStream(std::ostream& out) const override; + + protected: - StateLabeling observations; + // TODO: consider a bitvector based presentation (depending on our needs). + std::vector observations; + + uint64_t nrObservations; + + void computeNrObservations(); }; } } diff --git a/src/storm/storage/sparse/ModelComponents.h b/src/storm/storage/sparse/ModelComponents.h index b3e7e4f92..59d538f63 100644 --- a/src/storm/storage/sparse/ModelComponents.h +++ b/src/storm/storage/sparse/ModelComponents.h @@ -63,7 +63,7 @@ namespace storm { // stores for each choice from which parts of the input model description it originates boost::optional> choiceOrigins; - + boost::optional> observabilityClasses; // Continuous time specific components (CTMCs, Markov Automata): // True iff the transition values (for Markovian choices) are interpreted as rates.