From fd00d495f78a74a96903da9375d055bedc7c5e2c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 24 Aug 2020 21:38:53 -0700 Subject: [PATCH 01/16] first version of the nondeterministcbelieftracker --- .../NondeterministicBeliefTracker.cpp | 202 ++++++++++++++++++ .../generator/NondeterministicBeliefTracker.h | 88 ++++++++ 2 files changed, 290 insertions(+) create mode 100644 src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp create mode 100644 src/storm-pomdp/generator/NondeterministicBeliefTracker.h diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp new file mode 100644 index 000000000..c0d3bd3e8 --- /dev/null +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -0,0 +1,202 @@ + +#include "storm-pomdp/generator/NondeterministicBeliefTracker.h" + +namespace storm { + namespace generator { + + template + BeliefStateManager::BeliefStateManager(storm::models::sparse::Pomdp const& pomdp) + : pomdp(pomdp) + { + numberActionsPerObservation = std::vector(pomdp.getNrObservations(), 0); + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { + numberActionsPerObservation[pomdp.getObservation(state)] = pomdp.getNumberOfChoices(state); + } + } + + template + uint64_t BeliefStateManager::getActionsForObservation(uint32_t observation) const { + return numberActionsPerObservation[observation]; + } + + template + ValueType BeliefStateManager::getRisk(uint64_t state) const { + return riskPerState.at(state); + } + + template + storm::models::sparse::Pomdp const& BeliefStateManager::getPomdp() const { + return pomdp; + } + + template + void BeliefStateManager::setRiskPerState(std::vector const& risk) { + riskPerState = risk; + } + + template + SparseBeliefState::SparseBeliefState(std::shared_ptr> const& manager, uint64_t state) + : manager(manager), belief() + { + belief[state] = storm::utility::one(); + risk = manager->getRisk(state); + } + + template + SparseBeliefState::SparseBeliefState(std::shared_ptr> const& manager, std::map const& belief, + std::size_t hash, ValueType const& risk) + : manager(manager), belief(belief), prestoredhash(hash), risk(risk) + { + // Intentionally left empty + } + + template + ValueType SparseBeliefState::get(uint64_t state) const { + return belief.at(state); + } + + template + ValueType SparseBeliefState::getRisk() const { + return risk; + } + + template + std::size_t SparseBeliefState::hash() const noexcept { + return prestoredhash; + } + + template + bool SparseBeliefState::isValid() const { + return !belief.empty(); + } + + template + std::string SparseBeliefState::toString() const { + std::stringstream sstr; + bool first = true; + for (auto const& beliefentry : belief) { + if (!first) { + sstr << ", "; + } else { + first = false; + } + sstr << beliefentry.first << " : " << beliefentry.second; + } + return sstr.str(); + } + + template + bool operator==(SparseBeliefState const& lhs, SparseBeliefState const& rhs) { + return lhs.hash() == rhs.hash() && lhs.belief == rhs.belief; + } + + template + SparseBeliefState SparseBeliefState::update(uint64_t action, uint32_t observation) const { + std::map newBelief; + ValueType sum = storm::utility::zero(); + for (auto const& beliefentry : belief) { + assert(manager->getPomdp().getNumberOfChoices(beliefentry.first) > action); + auto row = manager->getPomdp().getNondeterministicChoiceIndices()[beliefentry.first] + action; + for (auto const& transition : manager->getPomdp().getTransitionMatrix().getRow(row)) { + if (observation != manager->getPomdp().getObservation(transition.getColumn())) { + continue; + } + + if (newBelief.count(transition.getColumn()) == 0) { + newBelief[transition.getColumn()] = transition.getValue() * beliefentry.second; + } else { + newBelief[transition.getColumn()] += transition.getValue() * beliefentry.second; + } + sum += transition.getValue() * beliefentry.second; + } + } + std::size_t newHash = 0; + ValueType risk = storm::utility::zero(); + for(auto& entry : newBelief) { + assert(!storm::utility::isZero(sum)); + entry.second /= sum; + boost::hash_combine(newHash, std::hash()(entry.second)); + boost::hash_combine(newHash, entry.first); + risk += entry.second * manager->getRisk(entry.first); + } + return SparseBeliefState(manager, newBelief, newHash, risk); + } + + + template + NondeterministicBeliefTracker::NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp) : + pomdp(pomdp), manager(std::make_shared>(pomdp)), beliefs() { + // + } + + template + bool NondeterministicBeliefTracker::reset(uint32_t observation) { + bool hit = false; + for (auto state : pomdp.getInitialStates()) { + if (observation == pomdp.getObservation(state)) { + hit = true; + beliefs.emplace(manager, state); + } + } + lastObservation = observation; + return hit; + } + + template + bool NondeterministicBeliefTracker::track(uint64_t newObservation) { + STORM_LOG_THROW(!beliefs.empty(), storm::exceptions::InvalidOperationException, "Cannot track without a belief (need to reset)."); + std::unordered_set newBeliefs; + for (uint64_t action = 0; action < manager->getActionsForObservation(lastObservation); ++action) { + for (auto const& belief : beliefs) { + auto newBelief = belief.update(action, newObservation); + if (newBelief.isValid()) { + newBeliefs.insert(newBelief); + } + } + } + beliefs = newBeliefs; + lastObservation = newObservation; + return !beliefs.empty(); + } + + template + ValueType NondeterministicBeliefTracker::getCurrentRisk(bool max) { + STORM_LOG_THROW(!beliefs.empty(), storm::exceptions::InvalidOperationException, "Risk is only defined for beliefs (run reset() first)."); + ValueType result = beliefs.begin()->getRisk(); + if (max) { + for (auto const& belief : beliefs) { + if (belief.getRisk() > result) { + result = belief.getRisk(); + } + } + } else { + for (auto const& belief : beliefs) { + if (belief.getRisk() < result) { + result = belief.getRisk(); + } + } + } + return result; + } + + template + void NondeterministicBeliefTracker::setRisk(std::vector const& risk) { + manager->setRiskPerState(risk); + } + + template + std::unordered_set const& NondeterministicBeliefTracker::getCurrentBeliefs() const { + return beliefs; + } + + template + uint32_t NondeterministicBeliefTracker::getCurrentObservation() const { + return lastObservation; + } + + template class SparseBeliefState; + template bool operator==(SparseBeliefState const&, SparseBeliefState const&); + template class NondeterministicBeliefTracker>; + + } +} diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h new file mode 100644 index 000000000..4712f38c6 --- /dev/null +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h @@ -0,0 +1,88 @@ +#pragma once +#include "storm/models/sparse/Pomdp.h" + +namespace storm { + namespace generator { + template + class BeliefStateManager { + public: + BeliefStateManager(storm::models::sparse::Pomdp const& pomdp); + storm::models::sparse::Pomdp const& getPomdp() const; + uint64_t getActionsForObservation(uint32_t observation) const; + ValueType getRisk(uint64_t) const; + void setRiskPerState(std::vector const& risk); + private: + storm::models::sparse::Pomdp const& pomdp; + std::vector riskPerState; + std::vector numberActionsPerObservation; + }; + + template + class SparseBeliefState; + template + bool operator==(SparseBeliefState const& lhs, SparseBeliefState const& rhs); + template + class SparseBeliefState { + public: + SparseBeliefState(std::shared_ptr> const& manager, uint64_t state); + SparseBeliefState update(uint64_t action, uint32_t observation) const; + std::size_t hash() const noexcept; + ValueType get(uint64_t state) const; + ValueType getRisk() const; + std::string toString() const; + bool isValid() const; + + friend bool operator==<>(SparseBeliefState const& lhs, SparseBeliefState const& rhs); + private: + SparseBeliefState(std::shared_ptr> const& manager, std::map const& belief, std::size_t newHash, ValueType const& risk); + std::shared_ptr> manager; + + std::map belief; // map is ordered for unique hashing. + std::size_t prestoredhash = 0; + ValueType risk; + + }; + + + template + class ObservationDenseBeliefState { + public: + ObservationDenseBeliefState(std::shared_ptr> const& manager, uint64_t state); + ObservationDenseBeliefState update(uint64_t action, uint32_t observation) const; + private: + std::shared_ptr> manager; + std::unordered_map belief; + + void normalize(); + }; + + template + class NondeterministicBeliefTracker { + public: + NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp); + bool reset(uint32_t observation); + bool track(uint64_t newObservation); + std::unordered_set const& getCurrentBeliefs() const; + uint32_t getCurrentObservation() const; + ValueType getCurrentRisk(bool max=true); + void setRisk(std::vector const& risk); + + private: + + storm::models::sparse::Pomdp const& pomdp; + std::shared_ptr> manager; + std::unordered_set beliefs; + uint32_t lastObservation; + }; + } +} + +// +namespace std { + template + struct hash> { + std::size_t operator()(storm::generator::SparseBeliefState const& s) const noexcept { + return s.hash(); + } + }; +} From 9423d0163142edab015feb905bd155724ef9d2d7 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 27 Aug 2020 15:07:45 -0700 Subject: [PATCH 02/16] observation valuations added --- .../transformer/MakePOMDPCanonic.cpp | 1 + src/storm/builder/BuilderOptions.cpp | 13 +- src/storm/builder/BuilderOptions.h | 12 ++ src/storm/builder/ExplicitModelBuilder.cpp | 62 +-------- src/storm/generator/NextStateGenerator.cpp | 59 ++++++++- src/storm/generator/NextStateGenerator.h | 6 +- src/storm/generator/VariableInformation.cpp | 7 + src/storm/generator/VariableInformation.h | 11 +- src/storm/models/sparse/Pomdp.cpp | 19 ++- src/storm/models/sparse/Pomdp.h | 12 +- src/storm/storage/sparse/ModelComponents.h | 2 + src/storm/storage/sparse/StateValuations.cpp | 120 ++++++++++++++---- src/storm/storage/sparse/StateValuations.h | 44 +++++-- 13 files changed, 266 insertions(+), 102 deletions(-) diff --git a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp index 28f0d8c30..601ce6699 100644 --- a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp +++ b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp @@ -151,6 +151,7 @@ namespace storm { modelcomponents.stateValuations = pomdp.getOptionalStateValuations(); modelcomponents.choiceLabeling = pomdp.getChoiceLabeling(); modelcomponents.choiceLabeling->permuteItems(permutation); + modelcomponents.observationValuations = pomdp.getOptionalObservationValuations(); return std::make_shared>(modelcomponents, true); } diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 9831040c3..17de90355 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -130,10 +130,14 @@ namespace storm { bool BuilderOptions::isBuildChoiceLabelsSet() const { return buildChoiceLabels; } - - bool BuilderOptions::isBuildStateValuationsSet() const { + + bool BuilderOptions::isBuildStateValuationsSet() const { return buildStateValuations; } + + bool BuilderOptions::isBuildObservationValuationsSet() const { + return buildObservationValuations; + } bool BuilderOptions::isBuildChoiceOriginsSet() const { return buildChoiceOrigins; @@ -237,6 +241,11 @@ namespace storm { buildStateValuations = newValue; return *this; } + + BuilderOptions& BuilderOptions::setBuildObservationValuations(bool newValue) { + buildObservationValuations = 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 a06817816..af424497a 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -106,6 +106,7 @@ namespace storm { bool isApplyMaximalProgressAssumptionSet() const; bool isBuildChoiceLabelsSet() const; bool isBuildStateValuationsSet() const; + bool isBuildObservationValuationsSet() const; bool isBuildChoiceOriginsSet() const; bool isBuildAllRewardModelsSet() const; bool isBuildAllLabelsSet() const; @@ -159,6 +160,14 @@ namespace storm { * @return this */ BuilderOptions& setBuildStateValuations(bool newValue = true); + + /** + * Should a observation valuation mapping be built? + * @param newValue The new value (default true) + * @return this + */ + BuilderOptions& setBuildObservationValuations(bool newValue = true); + /** * Should the origins the different choices be built? * @param newValue The new value (default true) @@ -236,6 +245,9 @@ namespace storm { /// A flag indicating whether or not to build for each state the variable valuation from which it originates. bool buildStateValuations; + + /// A flag indicating whether or not to build observation valuations + bool buildObservationValuations; // A flag that indicates whether or not to generate the information from which parts of the model specification // each choice originates. diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 9f5c7d298..8fedf075b 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -358,69 +358,17 @@ namespace storm { } if (generator->isPartiallyObservable()) { std::vector classes; - uint32_t newObservation = 0; classes.resize(stateStorage.getNumberOfStates()); std::unordered_map, uint32_t>>> observationActions; for (auto const& bitVectorIndexPair : stateStorage.stateToId) { uint32_t varObservation = generator->observabilityClass(bitVectorIndexPair.first); - uint32_t observation = -1; // Is replaced later on. - bool checkActionNames = false; - if (checkActionNames) { - bool foundActionSet = false; - std::vector actionNames; - bool addedAnonymousAction = false; - for (uint64_t choice = modelComponents.transitionMatrix.getRowGroupIndices()[bitVectorIndexPair.second]; - choice < modelComponents.transitionMatrix.getRowGroupIndices()[bitVectorIndexPair.second + - 1]; ++choice) { - if (modelComponents.choiceLabeling.get().getLabelsOfChoice(choice).empty()) { - STORM_LOG_THROW(!addedAnonymousAction, storm::exceptions::WrongFormatException, - "Cannot have multiple anonymous actions, as these cannot be mapped correctly."); - actionNames.push_back(""); - addedAnonymousAction = true; - } else { - STORM_LOG_ASSERT( - modelComponents.choiceLabeling.get().getLabelsOfChoice(choice).size() == 1, - "Expect choice labelling to contain exactly one label at this point, but found " - << modelComponents.choiceLabeling.get().getLabelsOfChoice( - choice).size()); - actionNames.push_back( - *modelComponents.choiceLabeling.get().getLabelsOfChoice(choice).begin()); - } - } - STORM_LOG_TRACE("VarObservation: " << varObservation << " Action Names: " - << storm::utility::vector::toString(actionNames)); - auto it = observationActions.find(varObservation); - if (it == observationActions.end()) { - observationActions.emplace(varObservation, - std::vector, uint32_t>>()); - } else { - for (auto const &entries : it->second) { - STORM_LOG_TRACE(storm::utility::vector::toString(entries.first)); - if (entries.first == actionNames) { - observation = entries.second; - foundActionSet = true; - break; - } - } - - STORM_LOG_THROW( - generator->getOptions().isInferObservationsFromActionsSet() || foundActionSet, - storm::exceptions::WrongFormatException, - "Two states with the same observation have a different set of enabled actions, this is only allowed with a special option."); - - } - if (!foundActionSet) { - observation = newObservation; - observationActions.find(varObservation)->second.emplace_back(actionNames, newObservation); - ++newObservation; - } - - classes[bitVectorIndexPair.second] = observation; - } else { - classes[bitVectorIndexPair.second] = varObservation; - } + classes[bitVectorIndexPair.second] = varObservation; } + modelComponents.observabilityClasses = classes; + if(generator->getOptions().isBuildObservationValuationsSet()) { + modelComponents.observationValuations = generator->makeObservationValuation(); + } } return modelComponents; } diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index eb681382b..e62825d17 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -61,6 +61,25 @@ namespace storm { } return result; } + + template + storm::storage::sparse::StateValuationsBuilder NextStateGenerator::initializeObservationValuationsBuilder() const { + storm::storage::sparse::StateValuationsBuilder result; + for (auto const& v : variableInformation.booleanVariables) { + if(v.observable) { + result.addVariable(v.variable); + } + } + for (auto const& v : variableInformation.integerVariables) { + if(v.observable) { + result.addVariable(v.variable); + } + } + for (auto const& l : variableInformation.observationLabels) { + result.addObservationLabel(l.name); + } + return result; + } template void NextStateGenerator::load(CompressedState const& state) { @@ -93,7 +112,42 @@ namespace storm { extractVariableValues(*this->state, variableInformation, integerValues, booleanValues, integerValues); valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues)); } - + + template + storm::storage::sparse::StateValuations NextStateGenerator::makeObservationValuation() const { + storm::storage::sparse::StateValuationsBuilder valuationsBuilder = initializeObservationValuationsBuilder(); + for (auto const& observationEntry : observabilityMap) { + std::vector booleanValues; + booleanValues.reserve( + variableInformation.booleanVariables.size()); // TODO: use number of observable boolean variables + std::vector integerValues; + integerValues.reserve(variableInformation.locationVariables.size() + + variableInformation.integerVariables.size()); // TODO: use number of observable integer variables + std::vector observationLabelValues; + observationLabelValues.reserve(variableInformation.observationLabels.size()); + expressions::SimpleValuation val = unpackStateIntoValuation(observationEntry.first, variableInformation, *expressionManager); + for (auto const& v : variableInformation.booleanVariables) { + if (v.observable) { + booleanValues.push_back(val.getBooleanValue(v.variable)); + } + } + for (auto const& v : variableInformation.integerVariables) { + if (v.observable) { + integerValues.push_back(val.getIntegerValue(v.variable)); + } + } + for(uint64_t labelStart = variableInformation.getTotalBitOffset(true); labelStart < observationEntry.first.size(); labelStart += 64) { + observationLabelValues.push_back(observationEntry.first.getAsInt(labelStart, 64)); + } + valuationsBuilder.addState(observationEntry.second, std::move(booleanValues), std::move(integerValues), {}, std::move(observationLabelValues)); + } + return valuationsBuilder.build(observabilityMap.size()); + + } + + + + template storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions) { @@ -213,7 +267,8 @@ namespace storm { if (this->mask.size() == 0) { this->mask = computeObservabilityMask(variableInformation); } - return unpackStateToObservabilityClass(state, evaluateObservationLabels(state), observabilityMap, mask); + uint32_t classId = unpackStateToObservabilityClass(state, evaluateObservationLabels(state), observabilityMap, mask); + return classId; } template diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index b782ad908..59f50843e 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -64,7 +64,9 @@ namespace storm { /// 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; - + /// Adds the valuation for the currently loaded state + virtual storm::storage::sparse::StateValuations makeObservationValuation() const; + virtual std::size_t getNumberOfRewardModels() const = 0; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0; @@ -95,6 +97,8 @@ namespace storm { virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const =0; + virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const; + void postprocess(StateBehavior& result); /// The options to be used for next-state generation. diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 72a351250..91dcf30ee 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -29,6 +29,10 @@ namespace storm { 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. } + + ObservationLabelInformation::ObservationLabelInformation(const std::string &name) : name(name) { + // Intentionally left empty. + } VariableInformation::VariableInformation(storm::prism::Program const& program, bool outOfBoundsState) : totalBitOffset(0) { if (outOfBoundsState) { @@ -64,6 +68,9 @@ namespace storm { totalBitOffset += bitwidth; } } + for (auto const& oblab : program.getObservationLabels()) { + observationLabels.emplace_back(oblab.getName()); + } sortVariables(); } diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index b7be52200..be97290f8 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -89,6 +89,12 @@ namespace storm { bool observable; }; + + struct ObservationLabelInformation { + ObservationLabelInformation(std::string const& name); + std::string name; + bool deterministic = true; + }; // A structure storing information about the used variables of the program. struct VariableInformation { @@ -113,7 +119,10 @@ namespace storm { /// The integer variables. std::vector integerVariables; - + + /// The observation labels + std::vector observationLabels; + /// Replacements for each array variable std::unordered_map> arrayVariableToElementInformations; diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index dc5461120..659c13e2e 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -15,12 +15,12 @@ namespace storm { } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components, bool canonicFlag) : Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) { + Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components, bool canonicFlag) : Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) , observationValuations(components.observationValuations) { computeNrObservations(); } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components, bool canonicFlag): Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) { + Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components, bool canonicFlag): Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) , observationValuations(components.observationValuations) { computeNrObservations(); } @@ -100,6 +100,21 @@ namespace storm { return result; } + template + bool Pomdp::hasObservationValuations() const { + return static_cast(observationValuations); + } + + template + storm::storage::sparse::StateValuations const& Pomdp::getObservationValuations() const { + return observationValuations.get(); + } + + template + boost::optional const& Pomdp::getOptionalObservationValuations() const { + return observationValuations; + } + template bool Pomdp::isCanonic() const { return canonicFlag; diff --git a/src/storm/models/sparse/Pomdp.h b/src/storm/models/sparse/Pomdp.h index cacee0953..6b1165482 100644 --- a/src/storm/models/sparse/Pomdp.h +++ b/src/storm/models/sparse/Pomdp.h @@ -78,6 +78,12 @@ namespace storm { std::vector getStatesWithObservation(uint32_t observation) const; + bool hasObservationValuations() const; + + storm::storage::sparse::StateValuations const& getObservationValuations() const; + + boost::optional const& getOptionalObservationValuations() const; + bool isCanonic() const; void setIsCanonic(bool newValue = true); @@ -94,11 +100,13 @@ namespace storm { // TODO: consider a bitvector based presentation (depending on our needs). std::vector observations; - uint64_t nrObservations; - bool canonicFlag = false; + boost::optional observationValuations; + + + void computeNrObservations(); }; } diff --git a/src/storm/storage/sparse/ModelComponents.h b/src/storm/storage/sparse/ModelComponents.h index f71037f1a..ca325b73c 100644 --- a/src/storm/storage/sparse/ModelComponents.h +++ b/src/storm/storage/sparse/ModelComponents.h @@ -67,6 +67,8 @@ namespace storm { // The POMDP observations boost::optional> observabilityClasses; + boost::optional observationValuations; + // Continuous time specific components (CTMCs, Markov Automata): // True iff the transition values (for Markovian choices) are interpreted as rates. bool rateTransitions; diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp index 541e56b90..589a61ccd 100644 --- a/src/storm/storage/sparse/StateValuations.cpp +++ b/src/storm/storage/sparse/StateValuations.cpp @@ -10,7 +10,7 @@ namespace storm { namespace storage { namespace sparse { - StateValuations::StateValuation::StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)) { + StateValuations::StateValuation::StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues, std::vector&& observationLabelValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)), observationLabelValues(std::move(observationLabelValues)) { // Intentionally left empty } @@ -20,15 +20,46 @@ namespace storm { return valuations[stateIndex]; } - StateValuations::StateValueIterator::StateValueIterator(typename std::map::const_iterator variableIt, StateValuation const* valuation) : variableIt(variableIt), valuation(valuation) { + StateValuations::StateValueIterator::StateValueIterator(typename std::map::const_iterator variableIt, + typename std::map::const_iterator labelIt, + typename std::map::const_iterator variableBegin , + typename std::map::const_iterator variableEnd, + typename std::map::const_iterator labelBegin, + typename std::map::const_iterator labelEnd, + StateValuation const* valuation) : variableIt(variableIt), labelIt(labelIt), + variableBegin(variableBegin), variableEnd(variableEnd), + labelBegin(labelBegin), labelEnd(labelEnd), valuation(valuation) { // Intentionally left empty. } - storm::expressions::Variable const& StateValuations::StateValueIterator::getVariable() const { return variableIt->first; } - bool StateValuations::StateValueIterator::isBoolean() const { return getVariable().hasBooleanType(); } - bool StateValuations::StateValueIterator::isInteger() const { return getVariable().hasIntegerType(); } - bool StateValuations::StateValueIterator::isRational() const { return getVariable().hasRationalType(); } - + bool StateValuations::StateValueIterator::isVariableAssignment() const { + return variableIt != variableEnd; + } + + bool StateValuations::StateValueIterator::isLabelAssignment() const { + return variableIt == variableEnd; + } + + storm::expressions::Variable const& StateValuations::StateValueIterator::getVariable() const { + STORM_LOG_ASSERT(isVariableAssignment(), "Does not point to a variable"); + return variableIt->first; + } + std::string const& StateValuations::StateValueIterator::getLabel() const { + STORM_LOG_ASSERT(isLabelAssignment(), "Does not point to a label"); + return labelIt->first; + } + bool StateValuations::StateValueIterator::isBoolean() const { return isVariableAssignment() && getVariable().hasBooleanType(); } + bool StateValuations::StateValueIterator::isInteger() const { return isVariableAssignment() && getVariable().hasIntegerType(); } + bool StateValuations::StateValueIterator::isRational() const { return isVariableAssignment() && getVariable().hasRationalType(); } + + std::string const& StateValuations::StateValueIterator::getName() const { + if(isVariableAssignment()) { + return getVariable().getName(); + } else { + return getLabel(); + } + } + bool StateValuations::StateValueIterator::getBooleanValue() const { STORM_LOG_ASSERT(isBoolean(), "Variable has no boolean type."); return valuation->booleanValues[variableIt->second]; @@ -38,7 +69,13 @@ namespace storm { STORM_LOG_ASSERT(isInteger(), "Variable has no integer type."); return valuation->integerValues[variableIt->second]; } - + + int64_t StateValuations::StateValueIterator::getLabelValue() const { + STORM_LOG_ASSERT(isLabelAssignment(), "Not a label assignment"); + STORM_LOG_ASSERT(labelIt->second < valuation->observationLabelValues.size(), "Label index " << labelIt->second << " larger than number of labels " << valuation->observationLabelValues.size()); + return valuation->observationLabelValues[labelIt->second]; + } + storm::RationalNumber StateValuations::StateValueIterator::getRationalValue() const { STORM_LOG_ASSERT(isRational(), "Variable has no rational type."); return valuation->rationalValues[variableIt->second]; @@ -46,33 +83,41 @@ namespace storm { bool StateValuations::StateValueIterator::operator==(StateValueIterator const& other) { STORM_LOG_ASSERT(valuation == valuation, "Comparing iterators for different states"); - return variableIt == other.variableIt; + return variableIt == other.variableIt && labelIt == other.labelIt; } bool StateValuations::StateValueIterator::operator!=(StateValueIterator const& other) { - STORM_LOG_ASSERT(valuation == valuation, "Comparing iterators for different states"); - return variableIt != other.variableIt; + return !(*this == other); } typename StateValuations::StateValueIterator& StateValuations::StateValueIterator::operator++() { - ++variableIt; + if(variableIt != variableEnd ) { + ++variableIt; + } else { + ++labelIt; + } + return *this; } typename StateValuations::StateValueIterator& StateValuations::StateValueIterator::operator--() { - --variableIt; + if (labelIt != labelBegin) { + --labelIt; + } else { + --variableIt; + } return *this; } - StateValuations::StateValueIteratorRange::StateValueIteratorRange(std::map const& variableMap, StateValuation const* valuation) : variableMap(variableMap), valuation(valuation) { + StateValuations::StateValueIteratorRange::StateValueIteratorRange(std::map const& variableMap, std::map const& labelMap, StateValuation const* valuation) : variableMap(variableMap), labelMap(labelMap), valuation(valuation) { // Intentionally left empty. } StateValuations::StateValueIterator StateValuations::StateValueIteratorRange::begin() const { - return StateValueIterator(variableMap.cbegin(), valuation); + return StateValueIterator(variableMap.cbegin(), labelMap.cbegin(), variableMap.cbegin(), variableMap.cend(), labelMap.cbegin(), labelMap.cend(), valuation); } StateValuations::StateValueIterator StateValuations::StateValueIteratorRange::end() const { - return StateValueIterator(variableMap.cend(), valuation); + return StateValueIterator(variableMap.cend(), labelMap.cend(), variableMap.cbegin(), variableMap.cend(), labelMap.cbegin(), labelMap.cend(), valuation); } bool StateValuations::getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const { @@ -94,8 +139,8 @@ namespace storm { } bool StateValuations::isEmpty(storm::storage::sparse::state_type const& stateIndex) const { - auto const& valuation = getValuation(stateIndex); - return valuation.booleanValues.empty() && valuation.integerValues.empty() && valuation.rationalValues.empty(); + auto const& valuation = valuations[stateIndex]; // Do not use getValuations, as that is only valid after adding stuff. + return valuation.booleanValues.empty() && valuation.integerValues.empty() && valuation.rationalValues.empty() && valuation.observationLabelValues.empty(); } std::string StateValuations::toString(storm::storage::sparse::state_type const& stateIndex, bool pretty, boost::optional> const& selectedVariables) const { @@ -115,11 +160,13 @@ namespace storm { if (valIt.isBoolean() && !valIt.getBooleanValue()) { stream << "!"; } - stream << valIt.getVariable().getName(); + stream << valIt.getName(); if (valIt.isInteger()) { stream << "=" << valIt.getIntegerValue(); } else if (valIt.isRational()) { stream << "=" << valIt.getRationalValue(); + } else if (valIt.isLabelAssignment()) { + stream << "=" << valIt.getLabelValue(); } else { STORM_LOG_THROW(valIt.isBoolean(), storm::exceptions::InvalidTypeException, "Unexpected variable type."); } @@ -130,6 +177,8 @@ namespace storm { stream << valIt.getIntegerValue(); } else if (valIt.isRational()) { stream << valIt.getRationalValue(); + } else if (valIt.isLabelAssignment()) { + stream << valIt.getLabelValue(); } } assignments.push_back(stream.str()); @@ -161,12 +210,12 @@ namespace storm { } if (valIt.isBoolean()) { - result[valIt.getVariable().getName()] = valIt.getBooleanValue(); + result[valIt.getName()] = valIt.getBooleanValue(); } else if (valIt.isInteger()) { - result[valIt.getVariable().getName()] = valIt.getIntegerValue(); + result[valIt.getName()] = valIt.getIntegerValue(); } else { STORM_LOG_ASSERT(valIt.isRational(), "Unexpected variable type."); - result[valIt.getVariable().getName()] = valIt.getRationalValue(); + result[valIt.getName()] = valIt.getRationalValue(); } if (selectedVariables) { @@ -220,7 +269,7 @@ namespace storm { typename StateValuations::StateValueIteratorRange StateValuations::at(state_type const& state) const { STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index."); - return StateValueIteratorRange({variableToIndexMap, &(valuations[state])}); + return StateValueIteratorRange({variableToIndexMap, observationLabels, &(valuations[state])}); } uint_fast64_t StateValuations::getNumberOfStates() const { @@ -248,7 +297,7 @@ namespace storm { return StateValuations(variableToIndexMap, std::move(selectedValuations)); } - StateValuationsBuilder::StateValuationsBuilder() : booleanVarCount(0), integerVarCount(0), rationalVarCount(0) { + StateValuationsBuilder::StateValuationsBuilder() : booleanVarCount(0), integerVarCount(0), rationalVarCount(0), labelCount(0) { // Intentionally left empty. } @@ -265,24 +314,41 @@ namespace storm { currentStateValuations.variableToIndexMap[variable] = rationalVarCount++; } } + + void StateValuationsBuilder::addObservationLabel(const std::string &label) { + currentStateValuations.observationLabels[label] = labelCount++; + } - void StateValuationsBuilder::addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues) { + void StateValuationsBuilder::addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues,std::vector&& observationLabelValues) { 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)); + currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues), std::move(observationLabelValues)); } else { STORM_LOG_ASSERT(currentStateValuations.isEmpty(state), "Adding a valuation to the same state multiple times."); - currentStateValuations.valuations[state] = typename StateValuations::StateValuation(std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); + currentStateValuations.valuations[state] = typename StateValuations::StateValuation(std::move(booleanValues), std::move(integerValues), std::move(rationalValues), std::move(observationLabelValues)); } } + + uint64_t StateValuationsBuilder::getBooleanVarCount() const { + return booleanVarCount; + } + + uint64_t StateValuationsBuilder::getIntegerVarCount() const { + return integerVarCount; + } + + uint64_t StateValuationsBuilder::getLabelCount() const { + return labelCount; + } StateValuations StateValuationsBuilder::build(std::size_t totalStateCount) { return std::move(currentStateValuations); booleanVarCount = 0; integerVarCount = 0; rationalVarCount = 0; + labelCount = 0; } } } diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h index 07027d52b..58925b4c4 100644 --- a/src/storm/storage/sparse/StateValuations.h +++ b/src/storm/storage/sparse/StateValuations.h @@ -26,45 +26,65 @@ namespace storm { public: friend class StateValuations; StateValuation() = default; - StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues); + StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues, std::vector&& observationLabelValues = {}); private: std::vector booleanValues; std::vector integerValues; std::vector rationalValues; + std::vector observationLabelValues; }; class StateValueIterator { public: - StateValueIterator(typename std::map::const_iterator variableIt, StateValuation const* valuation); + StateValueIterator(typename std::map::const_iterator variableIt, + typename std::map::const_iterator labelIt, + typename std::map::const_iterator variableBegin , + typename std::map::const_iterator variableEnd, + typename std::map::const_iterator labelBegin, + typename std::map::const_iterator labelEnd, + StateValuation const* valuation); bool operator==(StateValueIterator const& other); bool operator!=(StateValueIterator const& other); StateValueIterator& operator++(); StateValueIterator& operator--(); - + + bool isVariableAssignment() const; + bool isLabelAssignment() const; storm::expressions::Variable const& getVariable() const; + std::string const& getLabel() const; bool isBoolean() const; bool isInteger() const; bool isRational() const; - + + std::string const& getName() const; + // These shall only be called if the variable has the correct type bool getBooleanValue() const; int64_t getIntegerValue() const; storm::RationalNumber getRationalValue() const; + int64_t getLabelValue() const; private: typename std::map::const_iterator variableIt; + typename std::map::const_iterator labelIt; + typename std::map::const_iterator variableBegin; + typename std::map::const_iterator variableEnd; + typename std::map::const_iterator labelBegin; + typename std::map::const_iterator labelEnd; + StateValuation const* const valuation; }; class StateValueIteratorRange { public: - StateValueIteratorRange(std::map const& variableMap, StateValuation const* valuation); + StateValueIteratorRange(std::map const& variableMap, std::map const& labelMap, StateValuation const* valuation); StateValueIterator begin() const; StateValueIterator end() const; private: std::map const& variableMap; + std::map const& labelMap; StateValuation const* const valuation; }; @@ -117,6 +137,7 @@ namespace storm { StateValuation const& getValuation(storm::storage::sparse::state_type const& stateIndex) const; std::map variableToIndexMap; + std::map observationLabels; // A mapping from state indices to their variable valuations. std::vector valuations; @@ -127,28 +148,35 @@ namespace storm { StateValuationsBuilder(); /*! Adds a new variable to keep track of for the state valuations. - *! All variables need to be added before adding new states. + * All variables need to be added before adding new states. */ void addVariable(storm::expressions::Variable const& variable); - + + void addObservationLabel(std::string const& label); + /*! * 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 = {}); + void addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues = {}, std::vector&& integerValues = {}, std::vector&& rationalValues = {}, std::vector&& observationLabelValues = {}); /*! * Creates the finalized state valuations object. */ StateValuations build(std::size_t totalStateCount); + uint64_t getBooleanVarCount() const; + uint64_t getIntegerVarCount() const; + uint64_t getLabelCount() const; + private: StateValuations currentStateValuations; uint64_t booleanVarCount; uint64_t integerVarCount; uint64_t rationalVarCount; + uint64_t labelCount; }; } } From 1b73f15ff94929e8a4c3b60aecfbe01a9ba1ed4b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 1 Sep 2020 22:09:29 -0700 Subject: [PATCH 03/16] fix == operator --- .../NondeterministicBeliefTracker.cpp | 22 +++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp index c0d3bd3e8..09bece2c7 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -1,5 +1,6 @@ #include "storm-pomdp/generator/NondeterministicBeliefTracker.h" +#include "storm/utility/ConstantsComparator.h" namespace storm { namespace generator { @@ -87,7 +88,24 @@ namespace storm { template bool operator==(SparseBeliefState const& lhs, SparseBeliefState const& rhs) { - return lhs.hash() == rhs.hash() && lhs.belief == rhs.belief; + if (lhs.hash() != rhs.hash()) { + return false; + } + if (lhs.belief.size() != rhs.belief.size()) { + return false; + } + storm::utility::ConstantsComparator cmp(0.00001, true); + auto lhsIt = lhs.belief.begin(); + auto rhsIt = rhs.belief.begin(); + while(lhsIt != lhs.belief.end()) { + if (lhsIt->first != rhsIt->first || !cmp.isEqual(lhsIt->second, rhsIt->second)) { + return false; + } + ++lhsIt; + ++rhsIt; + } + return true; + //return std::equal(lhs.belief.begin(), lhs.belief.end(), rhs.belief.begin()); } template @@ -115,7 +133,7 @@ namespace storm { for(auto& entry : newBelief) { assert(!storm::utility::isZero(sum)); entry.second /= sum; - boost::hash_combine(newHash, std::hash()(entry.second)); + //boost::hash_combine(newHash, std::hash()(entry.second)); boost::hash_combine(newHash, entry.first); risk += entry.second * manager->getRisk(entry.first); } From 7f5f263d7bbe291f86b3877d31050b4696f40065 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 1 Sep 2020 22:10:06 -0700 Subject: [PATCH 04/16] observation-trace-unfolder added --- .../transformer/ObservationTraceUnfolder.cpp | 158 ++++++++++++++++++ .../transformer/ObservationTraceUnfolder.h | 18 ++ 2 files changed, 176 insertions(+) create mode 100644 src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp create mode 100644 src/storm-pomdp/transformer/ObservationTraceUnfolder.h diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp new file mode 100644 index 000000000..a300e1880 --- /dev/null +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -0,0 +1,158 @@ +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm-pomdp/transformer/ObservationTraceUnfolder.h" + + +namespace storm { + namespace pomdp { + template + ObservationTraceUnfolder::ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model) : model(model) { + statesPerObservation = std::vector(model.getNrObservations(), storm::storage::BitVector(model.getNumberOfStates())); + for (uint64_t state = 0; state < model.getNumberOfStates(); ++state) { + statesPerObservation[model.getObservation(state)].set(state, true); + } + } + + template + std::shared_ptr> ObservationTraceUnfolder::transform( + const std::vector &observations, std::vector const& risk) { + std::vector modifiedObservations = observations; + // First observation should be special. + // This just makes the algorithm simpler because we do not treat the first step as a special case later. + modifiedObservations[0] = model.getNrObservations(); + + storm::storage::BitVector initialStates = model.getInitialStates(); + storm::storage::BitVector actualInitialStates = initialStates; + for (uint64_t state : initialStates) { + if (model.getObservation(state) != observations[0]) { + actualInitialStates.set(state, false); + } + } + STORM_LOG_THROW(actualInitialStates.getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Must have unique initial state matching the observation"); + // + statesPerObservation.resize(model.getNrObservations() + 1); + statesPerObservation[model.getNrObservations()] = actualInitialStates; + + + std::map unfoldedToOld; + std::map unfoldedToOldNextStep; + std::map oldToUnfolded; + + // Add this initial state state: + unfoldedToOldNextStep[0] = actualInitialStates.getNextSetIndex(0); + + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0,0,0,true,true); + uint64_t newStateIndex = 1; + uint64_t newRowGroupStart = 0; + uint64_t newRowCount = 0; + // Notice that we are going to use a special last step + + for (uint64_t step = 0; step < observations.size() - 1; ++step) { + std::cout << "step " << step << std::endl; + oldToUnfolded.clear(); + unfoldedToOld = unfoldedToOldNextStep; + unfoldedToOldNextStep.clear(); + + for (auto const& unfoldedToOldEntry : unfoldedToOld) { + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl; + assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1); + uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second]; + uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second+1]; + + for (uint64_t oldRowIndex = oldRowIndexStart; oldRowIndex != oldRowIndexEnd; oldRowIndex++) { + std::cout << "\t\tconsider old action " << oldRowIndex << std::endl; + std::cout << "\t\tconsider new row nr " << newRowCount << std::endl; + + ValueType resetProb = storm::utility::zero(); + // We first find the reset probability + for (auto const &oldRowEntry : model.getTransitionMatrix().getRow(oldRowIndex)) { + if (model.getObservation(oldRowEntry.getColumn()) != observations[step + 1]) { + resetProb += oldRowEntry.getValue(); + } + } + std::cout << "\t\t\t add reset" << std::endl; + + // Add the resets + if (resetProb != storm::utility::zero()) { + transitionMatrixBuilder.addNextValue(newRowCount, 0, resetProb); + } + + std::cout << "\t\t\t add other transitions..." << std::endl; + + // Now, we build the outgoing transitions. + for (auto const &oldRowEntry : model.getTransitionMatrix().getRow(oldRowIndex)) { + if (model.getObservation(oldRowEntry.getColumn()) != observations[step + 1]) { + continue;// already handled. + } + uint64_t column = 0; + + auto entryIt = oldToUnfolded.find(oldRowEntry.getColumn()); + if (entryIt == oldToUnfolded.end()) { + column = newStateIndex; + oldToUnfolded[oldRowEntry.getColumn()] = column; + unfoldedToOldNextStep[column] = oldRowEntry.getColumn(); + newStateIndex++; + } else { + column = entryIt->second; + } + std::cout << "\t\t\t\t transition to " << column << std::endl; + transitionMatrixBuilder.addNextValue(newRowCount, column, + oldRowEntry.getValue()); + } + newRowCount++; + } + + newRowGroupStart = transitionMatrixBuilder.getLastRow() + 1; + + } + } + std::cout << "Adding last step..." << std::endl; + // Now, take care of the last step. + uint64_t sinkState = newStateIndex; + uint64_t targetState = newStateIndex + 1; + for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) { + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + if (!storm::utility::isZero(storm::utility::one() - risk[unfoldedToOldEntry.second])) { + transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, + storm::utility::one() - risk[unfoldedToOldEntry.second]); + } + if (!storm::utility::isZero(risk[unfoldedToOldEntry.second])) { + transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, + risk[unfoldedToOldEntry.second]); + } + newRowGroupStart++; + } + // sink state + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, storm::utility::one()); + newRowGroupStart++; + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + // target state + transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one()); + + + + storm::storage::sparse::ModelComponents components; + components.transitionMatrix = transitionMatrixBuilder.build(); + std::cout << components.transitionMatrix << std::endl; + + STORM_LOG_ASSERT(components.transitionMatrix.getRowGroupCount() == targetState + 1, "Expect row group count (" << components.transitionMatrix.getRowGroupCount() << ") one more as target state index " << targetState << ")"); + + storm::models::sparse::StateLabeling labeling(components.transitionMatrix.getRowGroupCount()); + labeling.addLabel("_goal"); + labeling.addLabelToState("_goal", targetState); + labeling.addLabel("init"); + labeling.addLabelToState("init", 0); + components.stateLabeling = labeling; + return std::make_shared>(std::move(components)); + + + + + } + + template class ObservationTraceUnfolder; + template class ObservationTraceUnfolder; + + } +} \ No newline at end of file diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h new file mode 100644 index 000000000..feafe57e2 --- /dev/null +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h @@ -0,0 +1,18 @@ +#include "storm/models/sparse/Pomdp.h" + +namespace storm { + namespace pomdp { + template + class ObservationTraceUnfolder { + + public: + ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model); + std::shared_ptr> transform(std::vector const& observations, std::vector const& risk); + private: + storm::models::sparse::Pomdp const& model; + std::vector statesPerObservation; + + }; + + } +} \ No newline at end of file From bf4a7fca3b01e91024a5c5b9c9a60d0c7a38571b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 3 Sep 2020 16:02:55 -0700 Subject: [PATCH 05/16] Fixed tracker --- .../NondeterministicBeliefTracker.cpp | 91 ++++++++++++++++--- .../generator/NondeterministicBeliefTracker.h | 8 +- 2 files changed, 86 insertions(+), 13 deletions(-) diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp index 09bece2c7..065b5f127 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -35,20 +35,28 @@ namespace storm { riskPerState = risk; } + template + uint64_t BeliefStateManager::getFreshId() { + beliefIdCounter++; + std::cout << "provide " << beliefIdCounter; + return beliefIdCounter; + } + template SparseBeliefState::SparseBeliefState(std::shared_ptr> const& manager, uint64_t state) - : manager(manager), belief() + : manager(manager), belief(), id(0), prevId(0) { + id = manager->getFreshId(); belief[state] = storm::utility::one(); risk = manager->getRisk(state); } template SparseBeliefState::SparseBeliefState(std::shared_ptr> const& manager, std::map const& belief, - std::size_t hash, ValueType const& risk) - : manager(manager), belief(belief), prestoredhash(hash), risk(risk) + std::size_t hash, ValueType const& risk, uint64_t prevId) + : manager(manager), belief(belief), prestoredhash(hash), risk(risk), id(0), prevId(prevId) { - // Intentionally left empty + id = manager->getFreshId(); } template @@ -74,6 +82,7 @@ namespace storm { template std::string SparseBeliefState::toString() const { std::stringstream sstr; + sstr << "id: " << id << "; "; bool first = true; for (auto const& beliefentry : belief) { if (!first) { @@ -83,6 +92,7 @@ namespace storm { } sstr << beliefentry.first << " : " << beliefentry.second; } + sstr << " (from " << prevId << ")"; return sstr.str(); } @@ -137,7 +147,67 @@ namespace storm { boost::hash_combine(newHash, entry.first); risk += entry.second * manager->getRisk(entry.first); } - return SparseBeliefState(manager, newBelief, newHash, risk); + return SparseBeliefState(manager, newBelief, newHash, risk, id); + } + + template + void SparseBeliefState::update(uint32_t newObservation, std::unordered_set>& previousBeliefs) const { + updateHelper({{}}, {storm::utility::zero()}, belief.begin(), newObservation, previousBeliefs); + } + + template + void SparseBeliefState::updateHelper(std::vector> const& partialBeliefs, std::vector const& sums, typename std::map::const_iterator nextStateIt, uint32_t newObservation, std::unordered_set>& previousBeliefs) const { + if(nextStateIt == belief.end()) { + for (uint64_t i = 0; i < partialBeliefs.size(); ++i) { + auto const& partialBelief = partialBeliefs[i]; + auto const& sum = sums[i]; + if (storm::utility::isZero(sum)) { + continue; + } + std::size_t newHash = 0; + ValueType risk = storm::utility::zero(); + std::map finalBelief; + for (auto &entry : partialBelief) { + assert(!storm::utility::isZero(sum)); + finalBelief[entry.first] = entry.second / sum; + //boost::hash_combine(newHash, std::hash()(entry.second)); + boost::hash_combine(newHash, entry.first); + risk += entry.second / sum * manager->getRisk(entry.first); + } + previousBeliefs.insert(SparseBeliefState(manager, finalBelief, newHash, risk, id)); + } + } else { + uint64_t state = nextStateIt->first; + auto newNextStateIt = nextStateIt; + newNextStateIt++; + std::vector> newPartialBeliefs; + std::vector newSums; + for (uint64_t i = 0; i < partialBeliefs.size(); ++i) { + + for (auto row = manager->getPomdp().getNondeterministicChoiceIndices()[state]; + row < manager->getPomdp().getNondeterministicChoiceIndices()[state + 1]; ++row) { + std::map newPartialBelief = partialBeliefs[i]; + ValueType newSum = sums[i]; + for (auto const &transition : manager->getPomdp().getTransitionMatrix().getRow(row)) { + if (newObservation != manager->getPomdp().getObservation(transition.getColumn())) { + continue; + } + + if (newPartialBelief.count(transition.getColumn()) == 0) { + newPartialBelief[transition.getColumn()] = transition.getValue() * nextStateIt->second; + } else { + newPartialBelief[transition.getColumn()] += transition.getValue() * nextStateIt->second; + } + newSum += transition.getValue() * nextStateIt->second; + + } + newPartialBeliefs.push_back(newPartialBelief); + newSums.push_back(newSum); + } + } + updateHelper(newPartialBeliefs, newSums, newNextStateIt, newObservation, previousBeliefs); + + } } @@ -164,14 +234,11 @@ namespace storm { bool NondeterministicBeliefTracker::track(uint64_t newObservation) { STORM_LOG_THROW(!beliefs.empty(), storm::exceptions::InvalidOperationException, "Cannot track without a belief (need to reset)."); std::unordered_set newBeliefs; - for (uint64_t action = 0; action < manager->getActionsForObservation(lastObservation); ++action) { - for (auto const& belief : beliefs) { - auto newBelief = belief.update(action, newObservation); - if (newBelief.isValid()) { - newBeliefs.insert(newBelief); - } - } + //for (uint64_t action = 0; action < manager->getActionsForObservation(lastObservation); ++action) { + for (auto const& belief : beliefs) { + belief.update(newObservation, newBeliefs); } + //} beliefs = newBeliefs; lastObservation = newObservation; return !beliefs.empty(); diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h index 4712f38c6..462a33a93 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h @@ -11,10 +11,12 @@ namespace storm { uint64_t getActionsForObservation(uint32_t observation) const; ValueType getRisk(uint64_t) const; void setRiskPerState(std::vector const& risk); + uint64_t getFreshId(); private: storm::models::sparse::Pomdp const& pomdp; std::vector riskPerState; std::vector numberActionsPerObservation; + uint64_t beliefIdCounter = 0; }; template @@ -26,6 +28,7 @@ namespace storm { public: SparseBeliefState(std::shared_ptr> const& manager, uint64_t state); SparseBeliefState update(uint64_t action, uint32_t observation) const; + void update(uint32_t newObservation, std::unordered_set& previousBeliefs) const; std::size_t hash() const noexcept; ValueType get(uint64_t state) const; ValueType getRisk() const; @@ -34,12 +37,15 @@ namespace storm { friend bool operator==<>(SparseBeliefState const& lhs, SparseBeliefState const& rhs); private: - SparseBeliefState(std::shared_ptr> const& manager, std::map const& belief, std::size_t newHash, ValueType const& risk); + void updateHelper(std::vector> const& partialBeliefs, std::vector const& sums, typename std::map::const_iterator nextStateIt, uint32_t newObservation, std::unordered_set>& previousBeliefs) const; + SparseBeliefState(std::shared_ptr> const& manager, std::map const& belief, std::size_t newHash, ValueType const& risk, uint64_t prevId); std::shared_ptr> manager; std::map belief; // map is ordered for unique hashing. std::size_t prestoredhash = 0; ValueType risk; + uint64_t id; + uint64_t prevId; }; From a7c6b39f19c85f986097c9acf2fbdb0b2cf6dc61 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 3 Sep 2020 16:07:41 -0700 Subject: [PATCH 06/16] Added state valuations in unfolding. --- .../transformer/ObservationTraceUnfolder.cpp | 14 +++++++++++++- .../transformer/ObservationTraceUnfolder.h | 3 ++- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp index a300e1880..1d8ca5399 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -1,11 +1,13 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm-pomdp/transformer/ObservationTraceUnfolder.h" +#include "storm/storage/expressions/ExpressionManager.h" namespace storm { namespace pomdp { template - ObservationTraceUnfolder::ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model) : model(model) { + ObservationTraceUnfolder::ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, + std::shared_ptr& exprManager) : model(model), exprManager(exprManager) { statesPerObservation = std::vector(model.getNrObservations(), storm::storage::BitVector(model.getNumberOfStates())); for (uint64_t state = 0; state < model.getNumberOfStates(); ++state) { statesPerObservation[model.getObservation(state)].set(state, true); @@ -32,6 +34,9 @@ namespace storm { statesPerObservation.resize(model.getNrObservations() + 1); statesPerObservation[model.getNrObservations()] = actualInitialStates; + storm::storage::sparse::StateValuationsBuilder svbuilder; + auto svvar = exprManager->declareFreshIntegerVariable(false, "_s"); + svbuilder.addVariable(svvar); std::map unfoldedToOld; std::map unfoldedToOldNextStep; @@ -56,6 +61,7 @@ namespace storm { transitionMatrixBuilder.newRowGroup(newRowGroupStart); std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl; assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1); + svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second]; uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second+1]; @@ -111,6 +117,8 @@ namespace storm { uint64_t sinkState = newStateIndex; uint64_t targetState = newStateIndex + 1; for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) { + svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); + transitionMatrixBuilder.newRowGroup(newRowGroupStart); if (!storm::utility::isZero(storm::utility::one() - risk[unfoldedToOldEntry.second])) { transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, @@ -125,10 +133,13 @@ namespace storm { // sink state transitionMatrixBuilder.newRowGroup(newRowGroupStart); transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, storm::utility::one()); + svbuilder.addState(sinkState, {}, {-1}); + newRowGroupStart++; transitionMatrixBuilder.newRowGroup(newRowGroupStart); // target state transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one()); + svbuilder.addState(targetState, {}, {-1}); @@ -144,6 +155,7 @@ namespace storm { labeling.addLabel("init"); labeling.addLabelToState("init", 0); components.stateLabeling = labeling; + components.stateValuations = svbuilder.build( components.transitionMatrix.getRowGroupCount()); return std::make_shared>(std::move(components)); diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h index feafe57e2..421cb4db9 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h @@ -6,10 +6,11 @@ namespace storm { class ObservationTraceUnfolder { public: - ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model); + ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, std::shared_ptr& exprManager); std::shared_ptr> transform(std::vector const& observations, std::vector const& risk); private: storm::models::sparse::Pomdp const& model; + std::shared_ptr& exprManager; std::vector statesPerObservation; }; From a358af1264707f4e9441036b0613806a3cefe8c1 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 14 Sep 2020 14:23:26 -0700 Subject: [PATCH 07/16] set entries that are nonzero --- src/storm/utility/vector.h | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index b70453aaa..28c267223 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -84,6 +84,16 @@ namespace storm { } } + template + void setNonzeroIndices(std::vector const& vec, storm::storage::BitVector& bv) { + STORM_LOG_ASSERT(bv.size() == vec.size(), "Bitvector size should match vector size"); + for (uint64_t i = 0; i < vec.size(); ++i) { + if(!storm::utility::isZero(vec[i])) { + bv.set(i, true); + } + } + } + /*! * Iota function as a helper for efficient creating a range in a vector. * See also http://stackoverflow.com/questions/11965732/set-stdvectorint-to-a-range From d2e36e9db35e853453b0fcc6f425075f3236562f Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 14 Sep 2020 14:24:12 -0700 Subject: [PATCH 08/16] dense belief states --- .../NondeterministicBeliefTracker.cpp | 246 +++++++++++++++++- .../generator/NondeterministicBeliefTracker.h | 45 +++- 2 files changed, 286 insertions(+), 5 deletions(-) diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp index 065b5f127..e330b7f90 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -1,6 +1,8 @@ #include "storm-pomdp/generator/NondeterministicBeliefTracker.h" #include "storm/utility/ConstantsComparator.h" +#include "storm/storage/geometry/nativepolytopeconversion/QuickHull.h" +#include "storm/utility/vector.h" namespace storm { namespace generator { @@ -10,11 +12,24 @@ namespace storm { : pomdp(pomdp) { numberActionsPerObservation = std::vector(pomdp.getNrObservations(), 0); + statePerObservationAndOffset = std::vector>(pomdp.getNrObservations(), std::vector()); for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { numberActionsPerObservation[pomdp.getObservation(state)] = pomdp.getNumberOfChoices(state); + statePerObservationAndOffset[pomdp.getObservation(state)].push_back(state); + observationOffsetId.push_back(statePerObservationAndOffset[pomdp.getObservation(state)].size() - 1); } } + template + uint32_t BeliefStateManager::getObservation(uint64_t state) const { + return pomdp.getObservation(state); + } + + template + uint64_t BeliefStateManager::getNumberOfStates() const { + return pomdp.getNumberOfStates(); + } + template uint64_t BeliefStateManager::getActionsForObservation(uint32_t observation) const { return numberActionsPerObservation[observation]; @@ -38,10 +53,28 @@ namespace storm { template uint64_t BeliefStateManager::getFreshId() { beliefIdCounter++; - std::cout << "provide " << beliefIdCounter; return beliefIdCounter; } + template + uint64_t BeliefStateManager::getObservationOffset(uint64_t state) const { + STORM_LOG_ASSERT(state < observationOffsetId.size(), "State " << state << " not a state id"); + return observationOffsetId[state]; + } + + template + uint64_t BeliefStateManager::numberOfStatesPerObservation(uint32_t observation) const { + STORM_LOG_ASSERT(observation < observationOffsetId.size(), "Observation " << observation << " not an observation id"); + return statePerObservationAndOffset[observation].size(); + } + + template + uint64_t BeliefStateManager::getState(uint32_t obs, uint64_t offset) const { + STORM_LOG_ASSERT(obs < statePerObservationAndOffset.size(), "Obs " << obs << " not a known observatoin"); + STORM_LOG_ASSERT(offset < statePerObservationAndOffset[obs].size(), "Offset " << offset << " too high for observation " << obs); + return statePerObservationAndOffset[obs][offset]; + } + template SparseBeliefState::SparseBeliefState(std::shared_ptr> const& manager, uint64_t state) : manager(manager), belief(), id(0), prevId(0) @@ -155,6 +188,21 @@ namespace storm { updateHelper({{}}, {storm::utility::zero()}, belief.begin(), newObservation, previousBeliefs); } + template + Eigen::Matrix SparseBeliefState::toEigenVector(storm::storage::BitVector const& support) const { + assert(false); + } + + template + uint64_t SparseBeliefState::getSupportSize() const { + return manager->getNumberOfStates(); + } + + template + void SparseBeliefState::setSupport(storm::storage::BitVector& support) const { + assert(false); + } + template void SparseBeliefState::updateHelper(std::vector> const& partialBeliefs, std::vector const& sums, typename std::map::const_iterator nextStateIt, uint32_t newObservation, std::unordered_set>& previousBeliefs) const { if(nextStateIt == belief.end()) { @@ -210,6 +258,164 @@ namespace storm { } } + template + bool operator==(ObservationDenseBeliefState const& lhs, ObservationDenseBeliefState const& rhs) { + if (lhs.hash() != rhs.hash()) { + return false; + } + if (lhs.observation != rhs.observation) { + return false; + } + storm::utility::ConstantsComparator cmp(0.00001, true); + auto lhsIt = lhs.belief.begin(); + auto rhsIt = rhs.belief.begin(); + while(lhsIt != lhs.belief.end()) { + if (!cmp.isEqual(*lhsIt, *rhsIt)) { + return false; + } + ++lhsIt; + ++rhsIt; + } + return true; + //return std::equal(lhs.belief.begin(), lhs.belief.end(), rhs.belief.begin()); + } + + template + ObservationDenseBeliefState::ObservationDenseBeliefState(std::shared_ptr> const& manager, uint64_t state) + : manager(manager), belief(manager->numberOfStatesPerObservation(manager->getObservation(state))) + { + observation = manager->getObservation(state); + belief[manager->getObservationOffset(state)] = storm::utility::one(); + } + + template + ObservationDenseBeliefState::ObservationDenseBeliefState(std::shared_ptr> const& manager, uint32_t observation, std::vector const& belief, std::size_t newHash, ValueType const& risk, uint64_t prevId) + : manager(manager), belief(belief), observation(observation), prestoredhash(newHash), risk(risk), id(manager->getFreshId()), prevId(prevId) + { + // Intentionally left empty. + } + + + template + void ObservationDenseBeliefState::update(uint32_t newObservation, std::unordered_set& previousBeliefs) const { + updateHelper({{}}, {storm::utility::zero()}, 0, newObservation, previousBeliefs); + } + + template + void ObservationDenseBeliefState::updateHelper(std::vector> const& partialBeliefs, std::vector const& sums, uint64_t currentEntry, uint32_t newObservation, std::unordered_set>& previousBeliefs) const { + while(currentEntry != belief.size() && storm::utility::isZero(belief[currentEntry])) { + currentEntry++; + } + if(currentEntry == belief.size()) { + for (uint64_t i = 0; i < partialBeliefs.size(); ++i) { + auto const& partialBelief = partialBeliefs[i]; + auto const& sum = sums[i]; + if (storm::utility::isZero(sum)) { + continue; + } + std::size_t newHash = 0; + ValueType risk = storm::utility::zero(); + std::vector finalBelief(manager->numberOfStatesPerObservation(observation), storm::utility::zero()); + for (auto &entry : partialBelief) { + assert(!storm::utility::isZero(sum)); + finalBelief[manager->getObservationOffset(entry.first)] = (entry.second / sum); + //boost::hash_combine(newHash, std::hash()(entry.second)); + boost::hash_combine(newHash, entry.first); + risk += entry.second / sum * manager->getRisk(entry.first); + } + previousBeliefs.insert(ObservationDenseBeliefState(manager, newObservation, finalBelief, newHash, risk, id)); + } + } else { + uint64_t state = manager->getState(observation,currentEntry); + uint64_t nextEntry = currentEntry + 1; + std::vector> newPartialBeliefs; + std::vector newSums; + for (uint64_t i = 0; i < partialBeliefs.size(); ++i) { + + for (auto row = manager->getPomdp().getNondeterministicChoiceIndices()[state]; + row < manager->getPomdp().getNondeterministicChoiceIndices()[state + 1]; ++row) { + std::map newPartialBelief = partialBeliefs[i]; + ValueType newSum = sums[i]; + for (auto const &transition : manager->getPomdp().getTransitionMatrix().getRow(row)) { + if (newObservation != manager->getPomdp().getObservation(transition.getColumn())) { + continue; + } + + if (newPartialBelief.count(transition.getColumn()) == 0) { + newPartialBelief[transition.getColumn()] = transition.getValue() * belief[currentEntry]; + } else { + newPartialBelief[transition.getColumn()] += transition.getValue() * belief[currentEntry]; + } + newSum += transition.getValue() * belief[currentEntry]; + + } + newPartialBeliefs.push_back(newPartialBelief); + newSums.push_back(newSum); + } + } + updateHelper(newPartialBeliefs, newSums, nextEntry, newObservation, previousBeliefs); + } + } + + template + std::size_t ObservationDenseBeliefState::hash() const noexcept { + return prestoredhash; + } + + template + ValueType ObservationDenseBeliefState::get(uint64_t state) const { + if (manager->getObservation(state) != state) { + return storm::utility::zero(); + } + return belief[manager->getObservationOffset(state)]; + } + + template + ValueType ObservationDenseBeliefState::getRisk() const { + return risk; + } + + template + Eigen::Matrix ObservationDenseBeliefState::toEigenVector(storm::storage::BitVector const& support) const { + return storm::adapters::EigenAdapter::toEigenVector(storm::utility::vector::filterVector(belief, support)); + } + + template + uint64_t ObservationDenseBeliefState::getSupportSize() const { + return belief.size(); + } + + template + void ObservationDenseBeliefState::setSupport(storm::storage::BitVector& support) const { + storm::utility::vector::setNonzeroIndices(belief, support); + std::cout << "Belief is " << storm::utility::vector::toString(belief) << std::endl; + std::cout << "Support is now " << support << std::endl; + } + + + template + std::string ObservationDenseBeliefState::toString() const { + std::stringstream sstr; + sstr << "id: " << id << "; "; + bool first = true; + uint64_t i = 0; + for (auto const& beliefentry : belief) { + + if (!storm::utility::isZero(beliefentry)) { + if (!first) { + sstr << ", "; + } else { + first = false; + } + + sstr << manager->getState(observation, i) << " : " << beliefentry; + } + i++; + } + sstr << " (from " << prevId << ")"; + return sstr.str(); + } + template NondeterministicBeliefTracker::NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp) : @@ -279,9 +485,47 @@ namespace storm { return lastObservation; } +// +// template +// void NondeterministicBeliefTracker::reduce() { +// std::cout << "reduce" << std::endl; +// storm::storage::BitVector support(beliefs.begin()->getSupportSize()); +// std::cout << "supp generated" << std::endl; +// for(auto const& belief : beliefs) { +// belief.setSupport(support); +// } +// std::cout << "Support:" << support << std::endl; +// +// if (beliefs.size() <= support.getNumberOfSetBits()) { +// return; +// } +// +// std::vector::EigenVector> points; +// for(auto const& bel : beliefs) { +// std::cout << bel.toEigenVector(support) << std::endl; +// points.push_back(bel.toEigenVector(support)); +// } +// +// storm::storage::geometry::QuickHull qh; +// std::cout << "Run QH (dim=" << points[0].size() << ")" << std::endl; +// qh.generateHalfspacesFromPoints(points, true); +// std::cout << "End QH" << std::endl; +// auto filteredPoints = qh.getRelevantVertices(); +// //if (filteredPoints.size() < points.size()) { +// // for(auto const& fp : filteredPoints) { +// // beliefs.emplace(manager,filteredPoints); +// // } +// //} +// } + + template class SparseBeliefState; template bool operator==(SparseBeliefState const&, SparseBeliefState const&); template class NondeterministicBeliefTracker>; + template class ObservationDenseBeliefState; + template bool operator==(ObservationDenseBeliefState const&, ObservationDenseBeliefState const&); + template class NondeterministicBeliefTracker>; + } } diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h index 462a33a93..29f315322 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h @@ -1,5 +1,6 @@ #pragma once #include "storm/models/sparse/Pomdp.h" +#include "storm/adapters/EigenAdapter.h" namespace storm { namespace generator { @@ -12,11 +13,19 @@ namespace storm { ValueType getRisk(uint64_t) const; void setRiskPerState(std::vector const& risk); uint64_t getFreshId(); + uint32_t getObservation(uint64_t state) const; + uint64_t getObservationOffset(uint64_t state) const; + uint64_t getState(uint32_t obs, uint64_t offset) const; + uint64_t getNumberOfStates() const; + uint64_t numberOfStatesPerObservation(uint32_t observation) const; + private: storm::models::sparse::Pomdp const& pomdp; std::vector riskPerState; std::vector numberActionsPerObservation; uint64_t beliefIdCounter = 0; + std::vector observationOffsetId; + std::vector> statePerObservationAndOffset; }; template @@ -34,6 +43,9 @@ namespace storm { ValueType getRisk() const; std::string toString() const; bool isValid() const; + Eigen::Matrix toEigenVector(storm::storage::BitVector const& support) const; + uint64_t getSupportSize() const; + void setSupport(storm::storage::BitVector&) const; friend bool operator==<>(SparseBeliefState const& lhs, SparseBeliefState const& rhs); private: @@ -46,20 +58,38 @@ namespace storm { ValueType risk; uint64_t id; uint64_t prevId; - }; + template + class ObservationDenseBeliefState; + template + bool operator==(ObservationDenseBeliefState const& lhs, ObservationDenseBeliefState const& rhs); + template class ObservationDenseBeliefState { public: ObservationDenseBeliefState(std::shared_ptr> const& manager, uint64_t state); - ObservationDenseBeliefState update(uint64_t action, uint32_t observation) const; + void update(uint32_t newObservation, std::unordered_set& previousBeliefs) const; + std::size_t hash() const noexcept; + ValueType get(uint64_t state) const; + ValueType getRisk() const; + std::string toString() const; + Eigen::Matrix toEigenVector(storm::storage::BitVector const& support) const; + uint64_t getSupportSize() const; + void setSupport(storm::storage::BitVector&) const; + friend bool operator==<>(ObservationDenseBeliefState const& lhs, ObservationDenseBeliefState const& rhs); private: + void updateHelper(std::vector> const& partialBeliefs, std::vector const& sums, uint64_t currentEntry, uint32_t newObservation, std::unordered_set>& previousBeliefs) const; + ObservationDenseBeliefState(std::shared_ptr> const& manager, uint32_t observation, std::vector const& belief, std::size_t newHash, ValueType const& risk, uint64_t prevId); std::shared_ptr> manager; - std::unordered_map belief; - void normalize(); + std::vector belief; + uint64_t observation = 0; + std::size_t prestoredhash = 0; + ValueType risk; + uint64_t id; + uint64_t prevId; }; template @@ -72,6 +102,7 @@ namespace storm { uint32_t getCurrentObservation() const; ValueType getCurrentRisk(bool max=true); void setRisk(std::vector const& risk); + //void reduce(); private: @@ -91,4 +122,10 @@ namespace std { return s.hash(); } }; + template + struct hash> { + std::size_t operator()(storm::generator::ObservationDenseBeliefState const& s) const noexcept { + return s.hash(); + } + }; } From b6be0f335619910f625a9b616da52aa79e100412 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 16 Sep 2020 08:50:19 -0700 Subject: [PATCH 09/16] convex reduction --- .../NondeterministicBeliefTracker.cpp | 63 +++++----- .../generator/NondeterministicBeliefTracker.h | 3 +- .../transformer/ObservationTraceUnfolder.cpp | 13 +- .../storage/geometry/ReduceVertexCloud.cpp | 119 ++++++++++++++++++ .../storage/geometry/ReduceVertexCloud.h | 29 +++++ 5 files changed, 185 insertions(+), 42 deletions(-) create mode 100644 src/storm/storage/geometry/ReduceVertexCloud.cpp create mode 100644 src/storm/storage/geometry/ReduceVertexCloud.h diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp index e330b7f90..37147f4ce 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -2,6 +2,7 @@ #include "storm-pomdp/generator/NondeterministicBeliefTracker.h" #include "storm/utility/ConstantsComparator.h" #include "storm/storage/geometry/nativepolytopeconversion/QuickHull.h" +#include "storm/storage/geometry/ReduceVertexCloud.h" #include "storm/utility/vector.h" namespace storm { @@ -198,6 +199,12 @@ namespace storm { return manager->getNumberOfStates(); } + template + std::map const& SparseBeliefState::getBeliefMap() const { + return belief; + } + + template void SparseBeliefState::setSupport(storm::storage::BitVector& support) const { assert(false); @@ -486,45 +493,33 @@ namespace storm { } // -// template -// void NondeterministicBeliefTracker::reduce() { -// std::cout << "reduce" << std::endl; -// storm::storage::BitVector support(beliefs.begin()->getSupportSize()); -// std::cout << "supp generated" << std::endl; -// for(auto const& belief : beliefs) { -// belief.setSupport(support); -// } -// std::cout << "Support:" << support << std::endl; -// -// if (beliefs.size() <= support.getNumberOfSetBits()) { -// return; -// } -// -// std::vector::EigenVector> points; -// for(auto const& bel : beliefs) { -// std::cout << bel.toEigenVector(support) << std::endl; -// points.push_back(bel.toEigenVector(support)); -// } -// -// storm::storage::geometry::QuickHull qh; -// std::cout << "Run QH (dim=" << points[0].size() << ")" << std::endl; -// qh.generateHalfspacesFromPoints(points, true); -// std::cout << "End QH" << std::endl; -// auto filteredPoints = qh.getRelevantVertices(); -// //if (filteredPoints.size() < points.size()) { -// // for(auto const& fp : filteredPoints) { -// // beliefs.emplace(manager,filteredPoints); -// // } -// //} -// } + template + uint64_t NondeterministicBeliefTracker::reduce() { + std::shared_ptr solverFactory = std::make_shared(); + storm::storage::geometry::ReduceVertexCloud rvc(solverFactory); + std::vector> points; + std::vector::iterator> iterators; + for (auto it = beliefs.begin(); it != beliefs.end(); ++it) { + // TODO get rid of the getBeliefMap function. + points.push_back(it->getBeliefMap()); + iterators.push_back(it); + } + storm::storage::BitVector eliminate = ~rvc.eliminate(points, pomdp.getNumberOfStates()); + + auto selectedIterators = storm::utility::vector::filterVector(iterators, eliminate); + for (auto iter : selectedIterators) { + beliefs.erase(iter); + } + return eliminate.getNumberOfSetBits(); + } template class SparseBeliefState; template bool operator==(SparseBeliefState const&, SparseBeliefState const&); template class NondeterministicBeliefTracker>; - template class ObservationDenseBeliefState; - template bool operator==(ObservationDenseBeliefState const&, ObservationDenseBeliefState const&); - template class NondeterministicBeliefTracker>; + //template class ObservationDenseBeliefState; + //template bool operator==(ObservationDenseBeliefState const&, ObservationDenseBeliefState const&); + //template class NondeterministicBeliefTracker>; } diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h index 29f315322..ef3b75a03 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h @@ -46,6 +46,7 @@ namespace storm { Eigen::Matrix toEigenVector(storm::storage::BitVector const& support) const; uint64_t getSupportSize() const; void setSupport(storm::storage::BitVector&) const; + std::map const& getBeliefMap() const; friend bool operator==<>(SparseBeliefState const& lhs, SparseBeliefState const& rhs); private: @@ -102,7 +103,7 @@ namespace storm { uint32_t getCurrentObservation() const; ValueType getCurrentRisk(bool max=true); void setRisk(std::vector const& risk); - //void reduce(); + uint64_t reduce(); private: diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp index 1d8ca5399..c8f1348d0 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -59,15 +59,15 @@ namespace storm { for (auto const& unfoldedToOldEntry : unfoldedToOld) { transitionMatrixBuilder.newRowGroup(newRowGroupStart); - std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl; + //std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl; assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1); svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second]; uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second+1]; for (uint64_t oldRowIndex = oldRowIndexStart; oldRowIndex != oldRowIndexEnd; oldRowIndex++) { - std::cout << "\t\tconsider old action " << oldRowIndex << std::endl; - std::cout << "\t\tconsider new row nr " << newRowCount << std::endl; + //std::cout << "\t\tconsider old action " << oldRowIndex << std::endl; + //std::cout << "\t\tconsider new row nr " << newRowCount << std::endl; ValueType resetProb = storm::utility::zero(); // We first find the reset probability @@ -76,14 +76,14 @@ namespace storm { resetProb += oldRowEntry.getValue(); } } - std::cout << "\t\t\t add reset" << std::endl; + //std::cout << "\t\t\t add reset" << std::endl; // Add the resets if (resetProb != storm::utility::zero()) { transitionMatrixBuilder.addNextValue(newRowCount, 0, resetProb); } - std::cout << "\t\t\t add other transitions..." << std::endl; + //std::cout << "\t\t\t add other transitions..." << std::endl; // Now, we build the outgoing transitions. for (auto const &oldRowEntry : model.getTransitionMatrix().getRow(oldRowIndex)) { @@ -101,7 +101,7 @@ namespace storm { } else { column = entryIt->second; } - std::cout << "\t\t\t\t transition to " << column << std::endl; + //std::cout << "\t\t\t\t transition to " << column << std::endl; transitionMatrixBuilder.addNextValue(newRowCount, column, oldRowEntry.getValue()); } @@ -145,7 +145,6 @@ namespace storm { storm::storage::sparse::ModelComponents components; components.transitionMatrix = transitionMatrixBuilder.build(); - std::cout << components.transitionMatrix << std::endl; STORM_LOG_ASSERT(components.transitionMatrix.getRowGroupCount() == targetState + 1, "Expect row group count (" << components.transitionMatrix.getRowGroupCount() << ") one more as target state index " << targetState << ")"); diff --git a/src/storm/storage/geometry/ReduceVertexCloud.cpp b/src/storm/storage/geometry/ReduceVertexCloud.cpp new file mode 100644 index 000000000..8c092928d --- /dev/null +++ b/src/storm/storage/geometry/ReduceVertexCloud.cpp @@ -0,0 +1,119 @@ +#include "storm/storage/geometry/ReduceVertexCloud.h" +#include "storm/utility/Stopwatch.h" +#undef _DEBUG_REDUCE_VERTEX_CLOUD + + +namespace storm { + namespace storage { + namespace geometry { + + template + std::string toString(std::map const& point) { + std::stringstream sstr; + bool first = true; + for (auto const& entry : point) { + if (first) { + first = false; + } else { + sstr << ", "; + } + sstr << entry.first << " : " << entry.second; + } + return sstr.str(); + } + + template + storm::storage::BitVector ReduceVertexCloud::eliminate(std::vector> const& input, uint64_t maxdimension) { + std::shared_ptr expressionManager = std::make_shared(); + std::vector supports; + std::vector weightVariables; + std::vector weightVariableExpressions; + + for (uint64_t pointIndex = 0; pointIndex < input.size(); ++pointIndex) { + + // Compute the support vectors to quickly determine which input points could be relevant. + supports.push_back(storm::storage::BitVector(maxdimension)); + for (auto const& entry : input[pointIndex]) { + supports.back().set(entry.first, true); + } + // Add a weight variable for each input point + weightVariables.push_back(expressionManager->declareRationalVariable("w_"+ std::to_string(pointIndex))); + // For convenience and performance, obtain the expression. + weightVariableExpressions.push_back(weightVariables.back().getExpression()); + } + + std::unique_ptr smtSolver = smtSolverFactory->create(*expressionManager); + for (auto const& weightVariableExpr : weightVariableExpressions) { + //smtSolver->add((weightVariableExpr == expressionManager->rational(0.0)) || (weightVariableExpr > expressionManager->rational(0.00001))); + smtSolver->add((weightVariableExpr >= expressionManager->rational(0.0))); + smtSolver->add(weightVariableExpr < expressionManager->rational(1.0)); + } + smtSolver->add(storm::expressions::sum(weightVariableExpressions) <= expressionManager->rational(1.0 + wiggle)); + smtSolver->add(storm::expressions::sum(weightVariableExpressions) >= expressionManager->rational(1 - wiggle)); + + storm::utility::Stopwatch solverTime; + storm::utility::Stopwatch totalTime(true); + storm::storage::BitVector vertices(input.size()); + for (uint64_t pointIndex = 0; pointIndex < input.size(); ++pointIndex) { + std::cout << pointIndex << " out of " << input.size() << std::endl; + smtSolver->push(); + std::map> dimensionTerms; + for (auto const& entry : input[pointIndex]) { + dimensionTerms[entry.first] = {expressionManager->rational(-entry.second)}; + } + for (uint64_t potentialSupport = 0; potentialSupport < input.size(); ++potentialSupport) { + if (pointIndex == potentialSupport) { + smtSolver->add(weightVariableExpressions[potentialSupport] == expressionManager->rational(0.0)); + } else if (potentialSupport < pointIndex && !vertices.get(potentialSupport)) { + smtSolver->add(weightVariableExpressions[potentialSupport] == expressionManager->rational(0.0)); + } else if (supports[potentialSupport].isSubsetOf(supports[pointIndex])) { + for (auto const& entry : input[potentialSupport]) { + dimensionTerms[entry.first].push_back(weightVariableExpressions[potentialSupport] * expressionManager->rational(entry.second)); + } + } else { + smtSolver->add(weightVariableExpressions[potentialSupport] == expressionManager->rational(0.0)); + } + } + for (auto const& entry : dimensionTerms) { + smtSolver->add(storm::expressions::sum(entry.second) == expressionManager->rational(0.0)); + } + + solverTime.start(); + auto result = smtSolver->check(); + solverTime.stop(); + if (result == storm::solver::SmtSolver::CheckResult::Unsat) { +#ifdef _DEBUG_REDUCE_VERTEX_CLOUD + if (input[pointIndex].size() == 2) { + std::cout << "point " << toString(input[pointIndex]) << " is a vertex:"; + std::cout << smtSolver->getSmtLibString() << std::endl; + } +#endif + vertices.set(pointIndex, true); + } +#ifdef _DEBUG_REDUCE_VERTEX_CLOUD + else + { + std::cout << "point " << toString(input[pointIndex]) << " is a convex combination of "; + auto val = smtSolver->getModelAsValuation(); + uint64_t varIndex = 0; + for (auto const& wvar : weightVariables) { + if (!storm::utility::isZero(val.getRationalValue(wvar))) { + std::cout << toString(input[varIndex]) << " (weight: " << val.getRationalValue(wvar) << ")"; + } + varIndex++; + } + std::cout << std::endl; + } +#endif + smtSolver->pop(); + std::cout << "Solver time " << solverTime.getTimeInMilliseconds() << std::endl; + std::cout << "Total time " << totalTime.getTimeInMilliseconds() << std::endl; + } + return vertices; + + } + + template class ReduceVertexCloud; + } + } +} \ No newline at end of file diff --git a/src/storm/storage/geometry/ReduceVertexCloud.h b/src/storm/storage/geometry/ReduceVertexCloud.h new file mode 100644 index 000000000..b9132fa98 --- /dev/null +++ b/src/storm/storage/geometry/ReduceVertexCloud.h @@ -0,0 +1,29 @@ +#pragma once + +#include "storm/storage/BitVector.h" +#include "storm/solver/SmtSolver.h" +#include "storm/utility/solver.h" + +namespace storm { + namespace storage { + namespace geometry { + template + class ReduceVertexCloud { + public: + ReduceVertexCloud(std::shared_ptr& smtSolverFactory, ValueType wiggle = storm::utility::convertNumber(0.001)) + : smtSolverFactory(smtSolverFactory), wiggle(wiggle) + { + + } + + storm::storage::BitVector eliminate(std::vector> const& input, uint64_t maxdimension); + + private: + std::shared_ptr& smtSolverFactory; + ValueType wiggle; + + }; + + } + } +} \ No newline at end of file From b7ad55b34b9bfff8ec9e9d47faad0303d8279bef Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 30 Sep 2020 20:31:54 -0700 Subject: [PATCH 10/16] random prob generator for rationals --- src/storm/utility/random.cpp | 24 ++++++++++++++++++++++++ src/storm/utility/random.h | 15 +++++++++++++++ 2 files changed, 39 insertions(+) diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp index f13d403cd..9e2d0ae35 100644 --- a/src/storm/utility/random.cpp +++ b/src/storm/utility/random.cpp @@ -1,5 +1,7 @@ #include "storm/utility/random.h" +#include + namespace storm { namespace utility { RandomProbabilityGenerator::RandomProbabilityGenerator() @@ -23,6 +25,28 @@ namespace storm { return std::uniform_int_distribution(min, max)(engine); } + RandomProbabilityGenerator::RandomProbabilityGenerator() + : distribution(0, std::numeric_limits::max()) + { + std::random_device rd; + engine = std::mt19937(rd()); + } + + RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) + : distribution(0, std::numeric_limits::max()), engine(seed) + { + + } + + RationalNumber RandomProbabilityGenerator::random() { + return carl::rationalize(distribution(engine)) / carl::rationalize(std::numeric_limits::max()); + + } + + uint64_t RandomProbabilityGenerator::random_uint(uint64_t min, uint64_t max) { + return std::uniform_int_distribution(min, max)(engine); + } + } } diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h index 93bfad20c..7e6e015be 100644 --- a/src/storm/utility/random.h +++ b/src/storm/utility/random.h @@ -1,4 +1,5 @@ #include +#include "storm/adapters/RationalNumberAdapter.h" namespace storm { namespace utility { @@ -26,6 +27,20 @@ namespace storm { }; + template<> + class RandomProbabilityGenerator { + public: + RandomProbabilityGenerator(); + RandomProbabilityGenerator(uint64_t seed); + RationalNumber random(); + uint64_t random_uint(uint64_t min, uint64_t max); + private: + std::uniform_int_distribution distribution; + std::mt19937 engine; + + }; + + } } \ No newline at end of file From f9ee3d10e4a4ce026d5711c6f12f205a2c2f38c7 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 1 Oct 2020 00:23:22 -0700 Subject: [PATCH 11/16] simulating with rationals --- src/storm/models/ModelBase.cpp | 4 ++++ src/storm/models/ModelBase.h | 7 ++++++- src/storm/models/sparse/Pomdp.cpp | 5 +++++ src/storm/models/sparse/Pomdp.h | 2 ++ src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp | 4 +++- 5 files changed, 20 insertions(+), 2 deletions(-) diff --git a/src/storm/models/ModelBase.cpp b/src/storm/models/ModelBase.cpp index 7bf753ab8..37ef5c80d 100644 --- a/src/storm/models/ModelBase.cpp +++ b/src/storm/models/ModelBase.cpp @@ -35,6 +35,10 @@ namespace storm { } return false; } + + bool ModelBase::isPartiallyObservable() const { + return false; + } bool ModelBase::supportsParameters() const { return false; diff --git a/src/storm/models/ModelBase.h b/src/storm/models/ModelBase.h index ca275ed92..95bfdc9e5 100644 --- a/src/storm/models/ModelBase.h +++ b/src/storm/models/ModelBase.h @@ -140,7 +140,12 @@ namespace storm { * @return True iff the model is exact. */ virtual bool isExact() const; - + + /* + * Checks whether the model is partially observable + */ + virtual bool isPartiallyObservable() const; + /*! * Converts the transition rewards of all reward models to state-based rewards. For deterministic models, * this reduces the rewards to state rewards only. For nondeterminstic models, the reward models will diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index 659c13e2e..a304a1898 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -125,6 +125,11 @@ namespace storm { this->canonicFlag = newValue; } + template + bool Pomdp::isPartiallyObservable() const { + return true; + } + template std::size_t Pomdp::hash() const { diff --git a/src/storm/models/sparse/Pomdp.h b/src/storm/models/sparse/Pomdp.h index 6b1165482..1589ac49e 100644 --- a/src/storm/models/sparse/Pomdp.h +++ b/src/storm/models/sparse/Pomdp.h @@ -90,6 +90,8 @@ namespace storm { virtual std::size_t hash() const override; + virtual bool isPartiallyObservable() const override; + protected: /*! * Return a string that is additonally added to the state information in the dot stream. diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp index ba6ad778b..9822e8a71 100644 --- a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp +++ b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp @@ -18,7 +18,7 @@ namespace storm { template void DiscreteTimeSparseModelSimulator::setSeed(uint64_t seed) { - generator = storm::utility::RandomProbabilityGenerator(seed); + generator = storm::utility::RandomProbabilityGenerator(seed); } template @@ -89,5 +89,7 @@ namespace storm { } template class DiscreteTimeSparseModelSimulator; + template class DiscreteTimeSparseModelSimulator; + } } From 4760a128152b4d6e581a73b7a5a3d25b07c22cb2 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 1 Oct 2020 00:23:47 -0700 Subject: [PATCH 12/16] reset signal handler --- src/storm/utility/SignalHandler.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/storm/utility/SignalHandler.h b/src/storm/utility/SignalHandler.h index 1050dfcad..bcae6d7ed 100644 --- a/src/storm/utility/SignalHandler.h +++ b/src/storm/utility/SignalHandler.h @@ -103,6 +103,12 @@ namespace storm { int lastSignal; }; + + inline void resetTimeoutAlarm() { + SignalInformation::infos().setTerminate(false); + alarm(0); + } + /*! * Check whether the program should terminate (due to some abort signal). * From e513a3fb6229660533fc40d5bbe0b299f96203e9 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 1 Oct 2020 00:24:52 -0700 Subject: [PATCH 13/16] progress in monitoring with timeouts etc --- .../generator/BeliefSupportTracker.cpp | 2 + .../NondeterministicBeliefTracker.cpp | 46 +++++++++++-- .../generator/NondeterministicBeliefTracker.h | 15 ++++- .../transformer/ObservationTraceUnfolder.cpp | 67 ++++++++++++++----- .../transformer/ObservationTraceUnfolder.h | 9 ++- .../storage/expressions/ExpressionManager.cpp | 2 +- .../storage/geometry/ReduceVertexCloud.cpp | 27 ++++++-- .../storage/geometry/ReduceVertexCloud.h | 13 +++- 8 files changed, 146 insertions(+), 35 deletions(-) diff --git a/src/storm-pomdp/generator/BeliefSupportTracker.cpp b/src/storm-pomdp/generator/BeliefSupportTracker.cpp index be2138121..3ee6195ef 100644 --- a/src/storm-pomdp/generator/BeliefSupportTracker.cpp +++ b/src/storm-pomdp/generator/BeliefSupportTracker.cpp @@ -30,6 +30,8 @@ namespace storm { } template class BeliefSupportTracker; + template class BeliefSupportTracker; + } } \ No newline at end of file diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp index 37147f4ce..a2d47e721 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -4,6 +4,7 @@ #include "storm/storage/geometry/nativepolytopeconversion/QuickHull.h" #include "storm/storage/geometry/ReduceVertexCloud.h" #include "storm/utility/vector.h" +#include "storm/utility/Stopwatch.h" namespace storm { namespace generator { @@ -207,7 +208,9 @@ namespace storm { template void SparseBeliefState::setSupport(storm::storage::BitVector& support) const { - assert(false); + for(auto const& entry : belief) { + support.set(entry.first, true); + } } template @@ -425,8 +428,8 @@ namespace storm { template - NondeterministicBeliefTracker::NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp) : - pomdp(pomdp), manager(std::make_shared>(pomdp)), beliefs() { + NondeterministicBeliefTracker::NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp, typename NondeterministicBeliefTracker::Options options ) : + pomdp(pomdp), manager(std::make_shared>(pomdp)), beliefs(), options(options) { // } @@ -448,8 +451,12 @@ namespace storm { STORM_LOG_THROW(!beliefs.empty(), storm::exceptions::InvalidOperationException, "Cannot track without a belief (need to reset)."); std::unordered_set newBeliefs; //for (uint64_t action = 0; action < manager->getActionsForObservation(lastObservation); ++action) { + storm::utility::Stopwatch trackTimer(true); for (auto const& belief : beliefs) { belief.update(newObservation, newBeliefs); + if (options.trackTimeOut > 0 && trackTimer.getTimeInMilliseconds() > options.trackTimeOut) { + return false; + } } //} beliefs = newBeliefs; @@ -492,11 +499,28 @@ namespace storm { return lastObservation; } + template + uint64_t NondeterministicBeliefTracker::getNumberOfBeliefs() const { + return beliefs.size(); + } + + template + uint64_t NondeterministicBeliefTracker::getCurrentDimension() const { + storm::storage::BitVector support(beliefs.begin()->getSupportSize()); + for(auto const& belief : beliefs) { + belief.setSupport(support); + } + return support.getNumberOfSetBits(); + } + + + // template uint64_t NondeterministicBeliefTracker::reduce() { + reductionTimedOut = false; std::shared_ptr solverFactory = std::make_shared(); - storm::storage::geometry::ReduceVertexCloud rvc(solverFactory); + storm::storage::geometry::ReduceVertexCloud rvc(solverFactory, options.wiggle, options.timeOut); std::vector> points; std::vector::iterator> iterators; for (auto it = beliefs.begin(); it != beliefs.end(); ++it) { @@ -504,7 +528,11 @@ namespace storm { points.push_back(it->getBeliefMap()); iterators.push_back(it); } - storm::storage::BitVector eliminate = ~rvc.eliminate(points, pomdp.getNumberOfStates()); + auto res = rvc.eliminate(points, pomdp.getNumberOfStates()); + storm::storage::BitVector eliminate = ~res.first; + if (res.second) { + reductionTimedOut = true; + } auto selectedIterators = storm::utility::vector::filterVector(iterators, eliminate); for (auto iter : selectedIterators) { @@ -513,6 +541,11 @@ namespace storm { return eliminate.getNumberOfSetBits(); } + template + bool NondeterministicBeliefTracker::hasTimedOut() const { + return reductionTimedOut; + } + template class SparseBeliefState; template bool operator==(SparseBeliefState const&, SparseBeliefState const&); @@ -521,6 +554,9 @@ namespace storm { //template bool operator==(ObservationDenseBeliefState const&, ObservationDenseBeliefState const&); //template class NondeterministicBeliefTracker>; + template class SparseBeliefState; + template bool operator==(SparseBeliefState const&, SparseBeliefState const&); + template class NondeterministicBeliefTracker>; } } diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h index ef3b75a03..632c8f1aa 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h @@ -93,23 +93,34 @@ namespace storm { uint64_t prevId; }; + template class NondeterministicBeliefTracker { + public: - NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp); + struct Options { + uint64_t trackTimeOut = 0; + uint64_t timeOut = 0; // for reduction, in milliseconds, 0 is no timeout + ValueType wiggle; // tolerance, anything above 0 means that we are incomplete. + }; + NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp, typename NondeterministicBeliefTracker::Options options = Options()); bool reset(uint32_t observation); bool track(uint64_t newObservation); std::unordered_set const& getCurrentBeliefs() const; uint32_t getCurrentObservation() const; + uint64_t getNumberOfBeliefs() const; ValueType getCurrentRisk(bool max=true); void setRisk(std::vector const& risk); + uint64_t getCurrentDimension() const; uint64_t reduce(); + bool hasTimedOut() const; private: - storm::models::sparse::Pomdp const& pomdp; std::shared_ptr> manager; std::unordered_set beliefs; + bool reductionTimedOut = false; + Options options; uint32_t lastObservation; }; } diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp index c8f1348d0..e8e21b908 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -2,21 +2,23 @@ #include "storm-pomdp/transformer/ObservationTraceUnfolder.h" #include "storm/storage/expressions/ExpressionManager.h" +#undef _VERBOSE_OBSERVATION_UNFOLDING namespace storm { namespace pomdp { template - ObservationTraceUnfolder::ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, - std::shared_ptr& exprManager) : model(model), exprManager(exprManager) { + ObservationTraceUnfolder::ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, std::vector const& risk, + std::shared_ptr& exprManager) : model(model), risk(risk), exprManager(exprManager) { statesPerObservation = std::vector(model.getNrObservations(), storm::storage::BitVector(model.getNumberOfStates())); for (uint64_t state = 0; state < model.getNumberOfStates(); ++state) { statesPerObservation[model.getObservation(state)].set(state, true); } + svvar = exprManager->declareFreshIntegerVariable(false, "_s"); } template std::shared_ptr> ObservationTraceUnfolder::transform( - const std::vector &observations, std::vector const& risk) { + const std::vector &observations) { std::vector modifiedObservations = observations; // First observation should be special. // This just makes the algorithm simpler because we do not treat the first step as a special case later. @@ -34,14 +36,20 @@ namespace storm { statesPerObservation.resize(model.getNrObservations() + 1); statesPerObservation[model.getNrObservations()] = actualInitialStates; +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "build valution builder.." << std::endl; +#endif storm::storage::sparse::StateValuationsBuilder svbuilder; - auto svvar = exprManager->declareFreshIntegerVariable(false, "_s"); svbuilder.addVariable(svvar); std::map unfoldedToOld; std::map unfoldedToOldNextStep; std::map oldToUnfolded; +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "start buildiing matrix..." << std::endl; +#endif + // Add this initial state state: unfoldedToOldNextStep[0] = actualInitialStates.getNextSetIndex(0); @@ -52,22 +60,25 @@ namespace storm { // Notice that we are going to use a special last step for (uint64_t step = 0; step < observations.size() - 1; ++step) { - std::cout << "step " << step << std::endl; oldToUnfolded.clear(); unfoldedToOld = unfoldedToOldNextStep; unfoldedToOldNextStep.clear(); for (auto const& unfoldedToOldEntry : unfoldedToOld) { transitionMatrixBuilder.newRowGroup(newRowGroupStart); - //std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl; +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl; +#endif assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1); svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second]; uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second+1]; for (uint64_t oldRowIndex = oldRowIndexStart; oldRowIndex != oldRowIndexEnd; oldRowIndex++) { - //std::cout << "\t\tconsider old action " << oldRowIndex << std::endl; - //std::cout << "\t\tconsider new row nr " << newRowCount << std::endl; +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\t\tconsider old action " << oldRowIndex << std::endl; + std::cout << "\t\tconsider new row nr " << newRowCount << std::endl; +#endif ValueType resetProb = storm::utility::zero(); // We first find the reset probability @@ -76,14 +87,17 @@ namespace storm { resetProb += oldRowEntry.getValue(); } } - //std::cout << "\t\t\t add reset" << std::endl; +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\t\t\t add reset with probability " << resetProb << std::endl; +#endif // Add the resets if (resetProb != storm::utility::zero()) { transitionMatrixBuilder.addNextValue(newRowCount, 0, resetProb); } - - //std::cout << "\t\t\t add other transitions..." << std::endl; +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\t\t\t add other transitions..." << std::endl; +#endif // Now, we build the outgoing transitions. for (auto const &oldRowEntry : model.getTransitionMatrix().getRow(oldRowIndex)) { @@ -101,7 +115,9 @@ namespace storm { } else { column = entryIt->second; } - //std::cout << "\t\t\t\t transition to " << column << std::endl; +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\t\t\t\t transition to " << column << "with probability " << oldRowEntry.getValue() << std::endl; +#endif transitionMatrixBuilder.addNextValue(newRowCount, column, oldRowEntry.getValue()); } @@ -112,7 +128,6 @@ namespace storm { } } - std::cout << "Adding last step..." << std::endl; // Now, take care of the last step. uint64_t sinkState = newStateIndex; uint64_t targetState = newStateIndex + 1; @@ -120,7 +135,11 @@ namespace storm { svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); transitionMatrixBuilder.newRowGroup(newRowGroupStart); - if (!storm::utility::isZero(storm::utility::one() - risk[unfoldedToOldEntry.second])) { + STORM_LOG_ASSERT(risk.size() > unfoldedToOldEntry.second, "Must be a state"); + STORM_LOG_ASSERT(risk[unfoldedToOldEntry.second] <= storm::utility::one(), "Risk must be a probability"); + STORM_LOG_ASSERT(risk[unfoldedToOldEntry.second] >= storm::utility::zero(), "Risk must be a probability"); + //std::cout << "risk is" << risk[unfoldedToOldEntry.second] << std::endl; + if (!storm::utility::isOne(risk[unfoldedToOldEntry.second])) { transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, storm::utility::one() - risk[unfoldedToOldEntry.second]); } @@ -140,12 +159,15 @@ namespace storm { // target state transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one()); svbuilder.addState(targetState, {}, {-1}); - - +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "build matrix..." << std::endl; +#endif storm::storage::sparse::ModelComponents components; components.transitionMatrix = transitionMatrixBuilder.build(); - +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << components.transitionMatrix << std::endl; +#endif STORM_LOG_ASSERT(components.transitionMatrix.getRowGroupCount() == targetState + 1, "Expect row group count (" << components.transitionMatrix.getRowGroupCount() << ") one more as target state index " << targetState << ")"); storm::models::sparse::StateLabeling labeling(components.transitionMatrix.getRowGroupCount()); @@ -157,12 +179,21 @@ namespace storm { components.stateValuations = svbuilder.build( components.transitionMatrix.getRowGroupCount()); return std::make_shared>(std::move(components)); + } + template + std::shared_ptr> ObservationTraceUnfolder::extend(uint32_t observation) { + traceSoFar.push_back(observation); + return transform(traceSoFar); + } - + template + void ObservationTraceUnfolder::reset(uint32_t observation) { + traceSoFar = {observation}; } template class ObservationTraceUnfolder; + template class ObservationTraceUnfolder; template class ObservationTraceUnfolder; } diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h index 421cb4db9..55036739b 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h @@ -6,12 +6,17 @@ namespace storm { class ObservationTraceUnfolder { public: - ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, std::shared_ptr& exprManager); - std::shared_ptr> transform(std::vector const& observations, std::vector const& risk); + ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, std::vector const& risk, std::shared_ptr& exprManager); + std::shared_ptr> transform(std::vector const& observations); + std::shared_ptr> extend(uint32_t observation); + void reset(uint32_t observation); private: storm::models::sparse::Pomdp const& model; + std::vector risk; // TODO reconsider holding this as a reference, but there were some strange bugs std::shared_ptr& exprManager; std::vector statesPerObservation; + std::vector traceSoFar; + storm::expressions::Variable svvar; }; diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp index 07a44dd3b..777f4b9c7 100644 --- a/src/storm/storage/expressions/ExpressionManager.cpp +++ b/src/storm/storage/expressions/ExpressionManager.cpp @@ -296,7 +296,7 @@ namespace storm { Type const& ExpressionManager::getVariableType(uint_fast64_t index) const { auto indexTypePair = indexToTypeMapping.find(index); - STORM_LOG_ASSERT(indexTypePair != indexToTypeMapping.end(), "Unable to retrieve type of unknown variable index."); + STORM_LOG_ASSERT(indexTypePair != indexToTypeMapping.end(), "Unable to retrieve type of unknown variable index '" << index << "'."); return indexTypePair->second; } diff --git a/src/storm/storage/geometry/ReduceVertexCloud.cpp b/src/storm/storage/geometry/ReduceVertexCloud.cpp index 8c092928d..e3042ccaf 100644 --- a/src/storm/storage/geometry/ReduceVertexCloud.cpp +++ b/src/storm/storage/geometry/ReduceVertexCloud.cpp @@ -23,7 +23,7 @@ namespace storm { } template - storm::storage::BitVector ReduceVertexCloud::eliminate(std::vector> const& input, uint64_t maxdimension) { + std::pair ReduceVertexCloud::eliminate(std::vector> const& input, uint64_t maxdimension) { std::shared_ptr expressionManager = std::make_shared(); std::vector supports; std::vector weightVariables; @@ -48,14 +48,23 @@ namespace storm { smtSolver->add((weightVariableExpr >= expressionManager->rational(0.0))); smtSolver->add(weightVariableExpr < expressionManager->rational(1.0)); } - smtSolver->add(storm::expressions::sum(weightVariableExpressions) <= expressionManager->rational(1.0 + wiggle)); - smtSolver->add(storm::expressions::sum(weightVariableExpressions) >= expressionManager->rational(1 - wiggle)); + if (storm::utility::isZero(wiggle)) { + smtSolver->add(storm::expressions::sum(weightVariableExpressions) <= + expressionManager->rational(1)); + } else { + smtSolver->add(storm::expressions::sum(weightVariableExpressions) <= + expressionManager->rational(1.0 + wiggle)); + smtSolver->add(storm::expressions::sum(weightVariableExpressions) >= + expressionManager->rational(1 - wiggle)); + } storm::utility::Stopwatch solverTime; storm::utility::Stopwatch totalTime(true); storm::storage::BitVector vertices(input.size()); for (uint64_t pointIndex = 0; pointIndex < input.size(); ++pointIndex) { +#ifdef _DEBUG_REUCE_VERTEX_CLOUD std::cout << pointIndex << " out of " << input.size() << std::endl; +#endif smtSolver->push(); std::map> dimensionTerms; for (auto const& entry : input[pointIndex]) { @@ -104,16 +113,26 @@ namespace storm { } std::cout << std::endl; } + if (timeOut > ) #endif + if (timeOut > 0 && totalTime.getTimeInMilliseconds() > timeOut) { + for (uint64_t remainingPoint = pointIndex + 1; remainingPoint < input.size(); ++remainingPoint) { + vertices.set(remainingPoint); + } + return {vertices, true}; + } smtSolver->pop(); +#ifdef _DEBUG_REDUCE_VERTEX_CLOUD std::cout << "Solver time " << solverTime.getTimeInMilliseconds() << std::endl; std::cout << "Total time " << totalTime.getTimeInMilliseconds() << std::endl; +#endif } - return vertices; + return {vertices, false}; } template class ReduceVertexCloud; + template class ReduceVertexCloud; } } } \ No newline at end of file diff --git a/src/storm/storage/geometry/ReduceVertexCloud.h b/src/storm/storage/geometry/ReduceVertexCloud.h index b9132fa98..0877d2933 100644 --- a/src/storm/storage/geometry/ReduceVertexCloud.h +++ b/src/storm/storage/geometry/ReduceVertexCloud.h @@ -10,17 +10,24 @@ namespace storm { template class ReduceVertexCloud { public: - ReduceVertexCloud(std::shared_ptr& smtSolverFactory, ValueType wiggle = storm::utility::convertNumber(0.001)) - : smtSolverFactory(smtSolverFactory), wiggle(wiggle) + /*! + * + * @param smtSolverFactory + * @param wiggle + * @param timeout: Maximal time in milliseconds, 0 is no timeout + */ + ReduceVertexCloud(std::shared_ptr& smtSolverFactory, ValueType wiggle = storm::utility::convertNumber(0.0), uint64_t timeout = 0) + : smtSolverFactory(smtSolverFactory), wiggle(wiggle), timeOut(timeout) { } - storm::storage::BitVector eliminate(std::vector> const& input, uint64_t maxdimension); + std::pair eliminate(std::vector> const& input, uint64_t maxdimension); private: std::shared_ptr& smtSolverFactory; ValueType wiggle; + uint64_t timeOut; }; From 664484883af860aeae5fad3403d47997652d08c5 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 20 Oct 2020 11:48:23 -0700 Subject: [PATCH 14/16] allow termination in inner loop of OVI --- src/storm/solver/helper/OptimisticValueIterationHelper.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp index 296dd2ceb..4a94a9ad0 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp @@ -276,6 +276,9 @@ namespace storm { bool cancelGuess = false; while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + if (storm::utility::resources::isTerminate()) { + status = SolverStatus::Aborted; + } ++overallIterations; ++currentVerificationIterations; // Perform value iteration stepwise for lower bound and guessed upper bound From 32c88825e25616a6cefb23f256fc9d0423579efb Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 20 Oct 2020 14:07:24 -0700 Subject: [PATCH 15/16] cleanup --- CHANGELOG.md | 6 ++ .../NondeterministicBeliefTracker.cpp | 45 ---------- .../generator/NondeterministicBeliefTracker.h | 86 +++++++++++++++++-- .../transformer/ObservationTraceUnfolder.h | 25 ++++++ 4 files changed, 110 insertions(+), 52 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 43b7c547a..bec6b578c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,12 @@ The releases of major and minor versions contain an overview of changes since th Version 1.6.x ------------- +## Version 1.6.3 (20xx/xx) +- Simulator supports exact arithmetic +- `storm-pomdp`: States can be labelled with values for observable predicates +- `storm-pomdp`: (Only API) Track state estimates +- `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP + ## Version 1.6.2 (2020/09) - Prism program simplification improved. - Revamped implementation of long-run-average algorithms, including scheduler export for LRA properties on Markov automata. diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp index a2d47e721..c02074a6b 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -153,48 +153,12 @@ namespace storm { //return std::equal(lhs.belief.begin(), lhs.belief.end(), rhs.belief.begin()); } - template - SparseBeliefState SparseBeliefState::update(uint64_t action, uint32_t observation) const { - std::map newBelief; - ValueType sum = storm::utility::zero(); - for (auto const& beliefentry : belief) { - assert(manager->getPomdp().getNumberOfChoices(beliefentry.first) > action); - auto row = manager->getPomdp().getNondeterministicChoiceIndices()[beliefentry.first] + action; - for (auto const& transition : manager->getPomdp().getTransitionMatrix().getRow(row)) { - if (observation != manager->getPomdp().getObservation(transition.getColumn())) { - continue; - } - - if (newBelief.count(transition.getColumn()) == 0) { - newBelief[transition.getColumn()] = transition.getValue() * beliefentry.second; - } else { - newBelief[transition.getColumn()] += transition.getValue() * beliefentry.second; - } - sum += transition.getValue() * beliefentry.second; - } - } - std::size_t newHash = 0; - ValueType risk = storm::utility::zero(); - for(auto& entry : newBelief) { - assert(!storm::utility::isZero(sum)); - entry.second /= sum; - //boost::hash_combine(newHash, std::hash()(entry.second)); - boost::hash_combine(newHash, entry.first); - risk += entry.second * manager->getRisk(entry.first); - } - return SparseBeliefState(manager, newBelief, newHash, risk, id); - } template void SparseBeliefState::update(uint32_t newObservation, std::unordered_set>& previousBeliefs) const { updateHelper({{}}, {storm::utility::zero()}, belief.begin(), newObservation, previousBeliefs); } - template - Eigen::Matrix SparseBeliefState::toEigenVector(storm::storage::BitVector const& support) const { - assert(false); - } - template uint64_t SparseBeliefState::getSupportSize() const { return manager->getNumberOfStates(); @@ -385,11 +349,6 @@ namespace storm { return risk; } - template - Eigen::Matrix ObservationDenseBeliefState::toEigenVector(storm::storage::BitVector const& support) const { - return storm::adapters::EigenAdapter::toEigenVector(storm::utility::vector::filterVector(belief, support)); - } - template uint64_t ObservationDenseBeliefState::getSupportSize() const { return belief.size(); @@ -398,8 +357,6 @@ namespace storm { template void ObservationDenseBeliefState::setSupport(storm::storage::BitVector& support) const { storm::utility::vector::setNonzeroIndices(belief, support); - std::cout << "Belief is " << storm::utility::vector::toString(belief) << std::endl; - std::cout << "Support is now " << support << std::endl; } @@ -450,7 +407,6 @@ namespace storm { bool NondeterministicBeliefTracker::track(uint64_t newObservation) { STORM_LOG_THROW(!beliefs.empty(), storm::exceptions::InvalidOperationException, "Cannot track without a belief (need to reset)."); std::unordered_set newBeliefs; - //for (uint64_t action = 0; action < manager->getActionsForObservation(lastObservation); ++action) { storm::utility::Stopwatch trackTimer(true); for (auto const& belief : beliefs) { belief.update(newObservation, newBeliefs); @@ -458,7 +414,6 @@ namespace storm { return false; } } - //} beliefs = newBeliefs; lastObservation = newObservation; return !beliefs.empty(); diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h index 632c8f1aa..ad5b87143 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h @@ -1,9 +1,12 @@ #pragma once #include "storm/models/sparse/Pomdp.h" -#include "storm/adapters/EigenAdapter.h" namespace storm { namespace generator { + /** + * This class keeps track of common information of a set of beliefs. + * It also keeps a reference to the POMDP. The manager is referenced by all beliefs. + */ template class BeliefStateManager { public: @@ -28,22 +31,41 @@ namespace storm { std::vector> statePerObservationAndOffset; }; + template class SparseBeliefState; template bool operator==(SparseBeliefState const& lhs, SparseBeliefState const& rhs); + + /** + * SparseBeliefState stores beliefs in a sparse format. + */ template class SparseBeliefState { public: SparseBeliefState(std::shared_ptr> const& manager, uint64_t state); - SparseBeliefState update(uint64_t action, uint32_t observation) const; + /** + * Update the belief using the new observation + * @param newObservation + * @param previousBeliefs put the new belief in this set + */ void update(uint32_t newObservation, std::unordered_set& previousBeliefs) const; std::size_t hash() const noexcept; + /** + * Get the estimate to be in the given state + * @param state + * @return + */ ValueType get(uint64_t state) const; + /** + * Get the weighted risk + * @return + */ ValueType getRisk() const; + + // Various getters std::string toString() const; bool isValid() const; - Eigen::Matrix toEigenVector(storm::storage::BitVector const& support) const; uint64_t getSupportSize() const; void setSupport(storm::storage::BitVector&) const; std::map const& getBeliefMap() const; @@ -61,7 +83,9 @@ namespace storm { uint64_t prevId; }; - + /** + * ObservationDenseBeliefState stores beliefs in a dense format (per observation). + */ template class ObservationDenseBeliefState; template @@ -76,7 +100,6 @@ namespace storm { ValueType get(uint64_t state) const; ValueType getRisk() const; std::string toString() const; - Eigen::Matrix toEigenVector(storm::storage::BitVector const& support) const; uint64_t getSupportSize() const; void setSupport(storm::storage::BitVector&) const; friend bool operator==<>(ObservationDenseBeliefState const& lhs, ObservationDenseBeliefState const& rhs); @@ -93,10 +116,15 @@ namespace storm { uint64_t prevId; }; - + /** + * This tracker implements state estimation for POMDPs. + * This corresponds to forward filtering in Junges, Torfah, Seshia. + * + * @tparam ValueType How are probabilities stored + * @tparam BeliefState What format to use for beliefs + */ template class NondeterministicBeliefTracker { - public: struct Options { uint64_t trackTimeOut = 0; @@ -104,15 +132,59 @@ namespace storm { ValueType wiggle; // tolerance, anything above 0 means that we are incomplete. }; NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp, typename NondeterministicBeliefTracker::Options options = Options()); + /** + * Start with a new trace. + * @param observation The initial observation to start with. + * @return + */ bool reset(uint32_t observation); + /** + * Extend the observed trace with the new observation + * @param newObservation + * @return + */ bool track(uint64_t newObservation); + /** + * Provides access to the current beliefs. + * @return + */ std::unordered_set const& getCurrentBeliefs() const; + /** + * What was the last obervation that we made? + * @return + */ uint32_t getCurrentObservation() const; + /** + * How many beliefs are we currently tracking? + * @return + */ uint64_t getNumberOfBeliefs() const; + /** + * What is the (worst-case/best-case) risk over all beliefs + * @param max Should we take the max or the min? + * @return + */ ValueType getCurrentRisk(bool max=true); + /** + * Sets the state-risk to use for all beliefs. + * @param risk + */ void setRisk(std::vector const& risk); + /** + * What is the dimension of the current set of beliefs, i.e., + * what is the number of states we could possibly be in? + * @return + */ uint64_t getCurrentDimension() const; + /** + * Apply reductions to the belief state + * @return + */ uint64_t reduce(); + /** + * Did we time out during the computation? + * @return + */ bool hasTimedOut() const; private: diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h index 55036739b..68a4f73c5 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h @@ -2,13 +2,38 @@ namespace storm { namespace pomdp { + /** + * Observation-trace unrolling to allow model checking for monitoring. + * This approach is outlined in Junges, Hazem, Seshia -- Runtime Monitoring for Markov Decision Processes + * @tparam ValueType ValueType for probabilities + */ template class ObservationTraceUnfolder { public: + /** + * Initialize + * @param model the MDP with state-based observations + * @param risk the state risk + * @param exprManager an Expression Manager + */ ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, std::vector const& risk, std::shared_ptr& exprManager); + /** + * Transform in one shot + * @param observations + * @return + */ std::shared_ptr> transform(std::vector const& observations); + /** + * Transform incrementaly + * @param observation + * @return + */ std::shared_ptr> extend(uint32_t observation); + /** + * When using the incremental approach, reset the observations made so far. + * @param observation The new initial observation + */ void reset(uint32_t observation); private: storm::models::sparse::Pomdp const& model; From 8b05837e7701e05e522447786e32a321ed52d0b6 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 21 Oct 2020 10:09:45 +0200 Subject: [PATCH 16/16] Fixed assertion for RationalFunction --- src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp index e8e21b908..36901c3e9 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -1,6 +1,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm-pomdp/transformer/ObservationTraceUnfolder.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/ConstantsComparator.h" #undef _VERBOSE_OBSERVATION_UNFOLDING @@ -131,13 +132,14 @@ namespace storm { // Now, take care of the last step. uint64_t sinkState = newStateIndex; uint64_t targetState = newStateIndex + 1; + auto cc = storm::utility::ConstantsComparator(); for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) { svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); transitionMatrixBuilder.newRowGroup(newRowGroupStart); STORM_LOG_ASSERT(risk.size() > unfoldedToOldEntry.second, "Must be a state"); - STORM_LOG_ASSERT(risk[unfoldedToOldEntry.second] <= storm::utility::one(), "Risk must be a probability"); - STORM_LOG_ASSERT(risk[unfoldedToOldEntry.second] >= storm::utility::zero(), "Risk must be a probability"); + STORM_LOG_ASSERT(!cc.isLess(storm::utility::one(), risk[unfoldedToOldEntry.second]), "Risk must be a probability"); + STORM_LOG_ASSERT(!cc.isLess(risk[unfoldedToOldEntry.second], storm::utility::zero()), "Risk must be a probability"); //std::cout << "risk is" << risk[unfoldedToOldEntry.second] << std::endl; if (!storm::utility::isOne(risk[unfoldedToOldEntry.second])) { transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, @@ -197,4 +199,4 @@ namespace storm { template class ObservationTraceUnfolder; } -} \ No newline at end of file +}