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; };