diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp index d6fed4ac45..792ef0ebbf 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -383,6 +383,7 @@ NondeterministicBeliefTracker::NondeterministicBeliefTra template bool NondeterministicBeliefTracker::reset(uint32_t observation) { bool hit = false; + beliefs.clear(); for (auto state : pomdp.getInitialStates()) { if (observation == pomdp.getObservation(state)) { hit = true; @@ -492,9 +493,6 @@ bool NondeterministicBeliefTracker::hasTimedOut() const 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 SparseBeliefState; template bool operator==(SparseBeliefState const&, SparseBeliefState const&); diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp index a6f834542c..18f93467cf 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -1,23 +1,25 @@ #include "storm-pomdp/transformer/ObservationTraceUnfolder.h" + +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/ConstantsComparator.h" -#include "storm/adapters/RationalFunctionAdapter.h" - #undef _VERBOSE_OBSERVATION_UNFOLDING namespace storm { namespace pomdp { template ObservationTraceUnfolder::ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, std::vector const& risk, - std::shared_ptr& exprManager) - : model(model), risk(risk), exprManager(exprManager) { + std::shared_ptr& exprManager, + ObservationTraceUnfolderOptions const& options) + : model(model), risk(risk), exprManager(exprManager), options(options) { statesPerObservation = std::vector(model.getNrObservations() + 1, 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"); + tsvar = exprManager->declareFreshIntegerVariable(false, "_t"); } template @@ -25,6 +27,7 @@ std::shared_ptr> ObservationTraceUnfolder< 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. + // We overwrite the observation with a non-existing obs z* modifiedObservations[0] = model.getNrObservations(); storm::storage::BitVector initialStates = model.getInitialStates(); @@ -36,7 +39,7 @@ std::shared_ptr> ObservationTraceUnfolder< } STORM_LOG_THROW(actualInitialStates.getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Must have unique initial state matching the observation"); - // + // For this z* that only exists in the initial state, we now also define the states for this observation. statesPerObservation[model.getNrObservations()] = actualInitialStates; #ifdef _VERBOSE_OBSERVATION_UNFOLDING @@ -44,24 +47,44 @@ std::shared_ptr> ObservationTraceUnfolder< #endif storm::storage::sparse::StateValuationsBuilder svbuilder; svbuilder.addVariable(svvar); + svbuilder.addVariable(tsvar); - std::map unfoldedToOld; - std::map unfoldedToOldNextStep; - std::map oldToUnfolded; + std::unordered_map unfoldedToOld; + std::unordered_map unfoldedToOldNextStep; + std::unordered_map oldToUnfolded; #ifdef _VERBOSE_OBSERVATION_UNFOLDING std::cout << "start buildiing matrix...\n"; #endif - // Add this initial state state: - unfoldedToOldNextStep[0] = actualInitialStates.getNextSetIndex(0); + uint64_t newStateIndex = 0; + uint64_t const violatedState = newStateIndex; + if (!options.rejectionSampling) { + // The violated state is only used if we do no use the rejection semantics. + ++newStateIndex; + } + // Add this initial state: + uint64_t const initialState = newStateIndex; + ++newStateIndex; + + unfoldedToOldNextStep[initialState] = actualInitialStates.getNextSetIndex(0); + uint64_t const resetDestination = options.rejectionSampling ? initialState : violatedState; // Should be initial state for the standard semantics. 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 + // TODO only add this state if it is actually reachable / rejection sampling + if (!options.rejectionSampling) { + // the violated state (only used when no rejection sampling) is a sink state + transitionMatrixBuilder.newRowGroup(violatedState); + transitionMatrixBuilder.addNextValue(violatedState, violatedState, storm::utility::one()); + svbuilder.addState(violatedState, {}, {-1, -1}); + } + + // Now we are starting to build the MDP from the initial state onwards. + uint64_t newRowGroupStart = initialState; + uint64_t newRowCount = initialState; + + // Notice that we are going to use a special last step for (uint64_t step = 0; step < observations.size() - 1; ++step) { oldToUnfolded.clear(); unfoldedToOld = unfoldedToOldNextStep; @@ -73,7 +96,7 @@ std::shared_ptr> ObservationTraceUnfolder< std::cout << "\tconsider new state " << unfoldedToOldEntry.first << '\n'; #endif assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1); - svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); + svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second), static_cast(step)}); uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second]; uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second + 1]; @@ -96,7 +119,7 @@ std::shared_ptr> ObservationTraceUnfolder< // Add the resets if (resetProb != storm::utility::zero()) { - transitionMatrixBuilder.addNextValue(newRowCount, 0, resetProb); + transitionMatrixBuilder.addNextValue(newRowCount, resetDestination, resetProb); } #ifdef _VERBOSE_OBSERVATION_UNFOLDING std::cout << "\t\t\t add other transitions...\n"; @@ -125,22 +148,20 @@ std::shared_ptr> ObservationTraceUnfolder< } newRowCount++; } - newRowGroupStart = transitionMatrixBuilder.getLastRow() + 1; } } // Now, take care of the last step. uint64_t sinkState = newStateIndex; uint64_t targetState = newStateIndex + 1; - auto cc = storm::utility::ConstantsComparator(); + [[maybe_unused]] auto cc = storm::utility::ConstantsComparator(); for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) { - svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); + svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second), static_cast(observations.size() - 1)}); transitionMatrixBuilder.newRowGroup(newRowGroupStart); STORM_LOG_ASSERT(risk.size() > unfoldedToOldEntry.second, "Must be a state"); 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] << '\n'; if (!storm::utility::isOne(risk[unfoldedToOldEntry.second])) { transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, storm::utility::one() - risk[unfoldedToOldEntry.second]); } @@ -152,13 +173,13 @@ std::shared_ptr> ObservationTraceUnfolder< // sink state transitionMatrixBuilder.newRowGroup(newRowGroupStart); transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, storm::utility::one()); - svbuilder.addState(sinkState, {}, {-1}); + svbuilder.addState(sinkState, {}, {-1, -1}); newRowGroupStart++; transitionMatrixBuilder.newRowGroup(newRowGroupStart); // target state transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one()); - svbuilder.addState(targetState, {}, {-1}); + svbuilder.addState(targetState, {}, {-1, -1}); #ifdef _VERBOSE_OBSERVATION_UNFOLDING std::cout << "build matrix...\n"; #endif @@ -168,22 +189,27 @@ std::shared_ptr> ObservationTraceUnfolder< #ifdef _VERBOSE_OBSERVATION_UNFOLDING std::cout << components.transitionMatrix << '\n'; #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()); labeling.addLabel("_goal"); labeling.addLabelToState("_goal", targetState); + if (!options.rejectionSampling) { + labeling.addLabel("_violated"); + labeling.addLabelToState("_violated", violatedState); + } + labeling.addLabel("_end"); + labeling.addLabelToState("_end", sinkState); + labeling.addLabelToState("_end", targetState); labeling.addLabel("init"); - labeling.addLabelToState("init", 0); + labeling.addLabelToState("init", initialState); components.stateLabeling = labeling; components.stateValuations = svbuilder.build(); return std::make_shared>(std::move(components)); } template -std::shared_ptr> ObservationTraceUnfolder::extend(uint32_t observation) { - traceSoFar.push_back(observation); +std::shared_ptr> ObservationTraceUnfolder::extend(std::vector const& observations) { + traceSoFar.insert(traceSoFar.end(), observations.begin(), observations.end()); return transform(traceSoFar); } @@ -192,8 +218,14 @@ void ObservationTraceUnfolder::reset(uint32_t observation) { traceSoFar = {observation}; } +template +bool ObservationTraceUnfolder::isRejectionSamplingSet() const { + return options.rejectionSampling; +} + template class ObservationTraceUnfolder; template class ObservationTraceUnfolder; template class ObservationTraceUnfolder; +template class ObservationTraceUnfolder; } // namespace pomdp } // namespace storm diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h index 9381c3c79d..55fce6e727 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h @@ -2,6 +2,12 @@ namespace storm { namespace pomdp { + +class ObservationTraceUnfolderOptions { + public: + bool rejectionSampling = true; +}; + /** * Observation-trace unrolling to allow model checking for monitoring. * This approach is outlined in Junges, Hazem, Seshia -- Runtime Monitoring for Markov Decision Processes @@ -17,7 +23,7 @@ class ObservationTraceUnfolder { * @param exprManager an Expression Manager */ ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, std::vector const& risk, - std::shared_ptr& exprManager); + std::shared_ptr& exprManager, ObservationTraceUnfolderOptions const& options); /** * Transform in one shot * @param observations @@ -29,20 +35,24 @@ class ObservationTraceUnfolder { * @param observation * @return */ - std::shared_ptr> extend(uint32_t observation); + std::shared_ptr> extend(std::vector const& observations); /** * When using the incremental approach, reset the observations made so far. * @param observation The new initial observation */ void reset(uint32_t observation); + bool isRejectionSamplingSet() const; + 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; + storm::expressions::Variable svvar; // Maps to the old state (explicit encoding) + storm::expressions::Variable tsvar; // Maps to the time step + ObservationTraceUnfolderOptions options; }; } // namespace pomdp