update the observation trace unfolder towards generic support to compute conditional probs and fix bug in belief tracker

Author: sjunges

src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp

@@ -383,6 +383,7 @@ NondeterministicBeliefTracker<ValueType, BeliefState>::NondeterministicBeliefTra
 template<typename ValueType, typename BeliefState>
 bool NondeterministicBeliefTracker<ValueType, BeliefState>::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<ValueType, BeliefState>::hasTimedOut() const
 template class SparseBeliefState<double>;
 template bool operator==(SparseBeliefState<double> const&, SparseBeliefState<double> const&);
 template class NondeterministicBeliefTracker<double, SparseBeliefState<double>>;
-// template class ObservationDenseBeliefState<double>;
-// template bool operator==(ObservationDenseBeliefState<double> const&, ObservationDenseBeliefState<double> const&);
-// template class NondeterministicBeliefTracker<double, ObservationDenseBeliefState<double>>;
 
 template class SparseBeliefState<storm::RationalNumber>;
 template bool operator==(SparseBeliefState<storm::RationalNumber> const&, SparseBeliefState<storm::RationalNumber> const&);

src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp

@@ -1,30 +1,34 @@
 #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<typename ValueType>
 ObservationTraceUnfolder<ValueType>::ObservationTraceUnfolder(storm::models::sparse::Pomdp<ValueType> const& model, std::vector<ValueType> const& risk,
-                                                              std::shared_ptr<storm::expressions::ExpressionManager>& exprManager)
-    : model(model), risk(risk), exprManager(exprManager) {
+                                                              std::shared_ptr<storm::expressions::ExpressionManager>& exprManager,
+                                                              ObservationTraceUnfolderOptions const& options)
+    : model(model), risk(risk), exprManager(exprManager), options(options) {
     statesPerObservation = std::vector<storm::storage::BitVector>(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<typename ValueType>
 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<ValueType>::transform(const std::vector<uint32_t>& observations) {
     std::vector<uint32_t> 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,15 +40,17 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> 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
     std::cout << "build valution builder..\n";
 #endif
     storm::storage::sparse::StateValuationsBuilder svbuilder;
     svbuilder.addVariable(svvar);
+    svbuilder.addVariable(tsvar);
 
+    // TODO: Do we need this as ordered maps? Is it better to make them unordered?
     std::map<uint64_t, uint64_t> unfoldedToOld;
     std::map<uint64_t, uint64_t> unfoldedToOldNextStep;
     std::map<uint64_t, uint64_t> oldToUnfolded;
@@ -53,15 +59,30 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
     std::cout << "start buildiing matrix...\n";
 #endif
 
+    uint64_t newStateIndex = 0;
+    // TODO do not add violated state if we do rejection sampling.
+    uint64_t violatedState = newStateIndex;
+    ++newStateIndex;
     // Add this initial state state:
-    unfoldedToOldNextStep[0] = actualInitialStates.getNextSetIndex(0);
+    uint64_t initialState = newStateIndex;
+    ++newStateIndex;
 
+    unfoldedToOldNextStep[initialState] = actualInitialStates.getNextSetIndex(0);
+
+    uint64_t resetDestination = options.rejectionSampling ? initialState : violatedState;  // Should be initial state for the standard semantics.
     storm::storage::SparseMatrixBuilder<ValueType> 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
+    // the violated state is a sink state
+    transitionMatrixBuilder.newRowGroup(violatedState);
+    transitionMatrixBuilder.addNextValue(violatedState, violatedState, storm::utility::one<ValueType>());
+    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 +94,7 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
             std::cout << "\tconsider new state " << unfoldedToOldEntry.first << '\n';
 #endif
             assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1);
-            svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second)});
+            svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second), static_cast<int64_t>(step)});
             uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second];
             uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second + 1];
 
@@ -96,7 +117,7 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
 
                 // Add the resets
                 if (resetProb != storm::utility::zero<ValueType>()) {
-                    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 +146,20 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> 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<ValueType>();
+    [[maybe_unused]] auto cc = storm::utility::ConstantsComparator<ValueType>();
     for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) {
-        svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second)});
+        svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second), static_cast<int64_t>(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<ValueType>(), risk[unfoldedToOldEntry.second]), "Risk must be a probability");
         STORM_LOG_ASSERT(!cc.isLess(risk[unfoldedToOldEntry.second], storm::utility::zero<ValueType>()), "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<ValueType>() - risk[unfoldedToOldEntry.second]);
         }
@@ -152,13 +171,13 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
     // sink state
     transitionMatrixBuilder.newRowGroup(newRowGroupStart);
     transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, storm::utility::one<ValueType>());
-    svbuilder.addState(sinkState, {}, {-1});
+    svbuilder.addState(sinkState, {}, {-1, -1});
 
     newRowGroupStart++;
     transitionMatrixBuilder.newRowGroup(newRowGroupStart);
     // target state
     transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one<ValueType>());
-    svbuilder.addState(targetState, {}, {-1});
+    svbuilder.addState(targetState, {}, {-1, -1});
 #ifdef _VERBOSE_OBSERVATION_UNFOLDING
     std::cout << "build matrix...\n";
 #endif
@@ -168,14 +187,19 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
 #ifdef _VERBOSE_OBSERVATION_UNFOLDING
     std::cout << components.transitionMatrix << '\n';
 #endif
-    STORM_LOG_ASSERT(components.transitionMatrix.getRowGroupCount() == targetState + 1,
+    STORM_LOG_ASSERT(components.transitionMatrix.getRowGroupCount() == targetState + 2,
                      "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("_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<storm::models::sparse::Mdp<ValueType>>(std::move(components));
@@ -192,6 +216,11 @@ void ObservationTraceUnfolder<ValueType>::reset(uint32_t observation) {
     traceSoFar = {observation};
 }
 
+template<typename ValueType>
+bool ObservationTraceUnfolder<ValueType>::isRejectionSamplingSet() const {
+    return options.rejectionSampling;
+}
+
 template class ObservationTraceUnfolder<double>;
 template class ObservationTraceUnfolder<storm::RationalNumber>;
 template class ObservationTraceUnfolder<storm::RationalFunction>;

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<ValueType> const& model, std::vector<ValueType> const& risk,
-                             std::shared_ptr<storm::expressions::ExpressionManager>& exprManager);
+                             std::shared_ptr<storm::expressions::ExpressionManager>& exprManager, ObservationTraceUnfolderOptions const& options);
     /**
      * Transform in one shot
      * @param observations
@@ -36,13 +42,17 @@ class ObservationTraceUnfolder {
      */
     void reset(uint32_t observation);
 
+    bool isRejectionSamplingSet() const;
+
    private:
     storm::models::sparse::Pomdp<ValueType> const& model;
     std::vector<ValueType> risk;  // TODO reconsider holding this as a reference, but there were some strange bugs
     std::shared_ptr<storm::expressions::ExpressionManager>& exprManager;
     std::vector<storm::storage::BitVector> statesPerObservation;
     std::vector<uint32_t> 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