From 896d4096024c8394a157b7fab7cfb8830ea6971a Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 6 May 2020 12:44:16 +0200
Subject: [PATCH] Implemented simple (but incomplete) check to display whether
 the belief MDP is finite.

---
 .../analysis/FiniteBeliefMdpDetection.h       | 59 +++++++++++++++++++
 .../ApproximatePOMDPModelchecker.cpp          |  8 ++-
 2 files changed, 66 insertions(+), 1 deletion(-)
 create mode 100644 src/storm-pomdp/analysis/FiniteBeliefMdpDetection.h

diff --git a/src/storm-pomdp/analysis/FiniteBeliefMdpDetection.h b/src/storm-pomdp/analysis/FiniteBeliefMdpDetection.h
new file mode 100644
index 000000000..e28b3a339
--- /dev/null
+++ b/src/storm-pomdp/analysis/FiniteBeliefMdpDetection.h
@@ -0,0 +1,59 @@
+#pragma once
+
+#include <boost/optional.hpp>
+
+#include "storm/models/sparse/Pomdp.h"
+#include "storm/storage/BitVector.h"
+#include "storm/storage/StronglyConnectedComponentDecomposition.h"
+
+namespace storm {
+    namespace pomdp {
+    
+        /*!
+         * This method tries to detect that the beliefmdp is finite.
+         * If this returns true, the beliefmdp is certainly finite.
+         * However, if this returns false, the beliefmdp might still be finite
+         * It is assumed that the belief MDP is not further explored when reaching a targetstate
+         */
+        template<typename ValueType>
+        bool detectFiniteBeliefMdp(storm::models::sparse::Pomdp<ValueType> const& pomdp, boost::optional<storm::storage::BitVector> const& targetStates) {
+            // All infinite paths of the POMDP (including the ones with prob. 0 ) either
+            //  - reach a target state after finitely many steps or
+            //  - after finitely many steps enter an SCC and do not leave it
+            // Hence, any path of the belief MDP will at some point either reach a target state or stay in a set of POMDP SCCs.
+            // Only in the latter case we can get infinitely many different belief states.
+            // Below, we check whether all SCCs only consist of Dirac distributions.
+            // If this is the case, no new belief states will be found at some point.
+            
+            // Get the SCC decomposition
+            storm::storage::StronglyConnectedComponentDecompositionOptions options;
+            options.dropNaiveSccs();
+            storm::storage::BitVector relevantStates;
+            if (targetStates) {
+                relevantStates = ~targetStates.get();
+                options.subsystem(&relevantStates);
+            }
+            storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccs(pomdp.getTransitionMatrix(), options);
+            
+            // Check whether all choices that stay within an SCC have Dirac distributions
+            for (auto const& scc : sccs) {
+                for (auto const& sccState : scc) {
+                    for (uint64_t rowIndex = pomdp.getNondeterministicChoiceIndices()[sccState]; rowIndex < pomdp.getNondeterministicChoiceIndices()[sccState + 1]; ++rowIndex) {
+                        for (auto const& entry : pomdp.getTransitionMatrix().getRow(rowIndex)) {
+                            if (!storm::utility::isOne(entry.getValue()) && !storm::utility::isZero(entry.getValue())) {
+                                if (scc.containsState(entry.getColumn())) {
+                                    // There is a non-dirac choice that stays in the SCC.
+                                    // This could still mean that the belief MDP is finite
+                                    // e.g., if at some point the branches merge back to the same state
+                                    return false;
+                                }
+                            }
+                        }
+                    }
+                }
+            }
+
+            return true;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
index 55b252225..81b2df397 100644
--- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
+++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
@@ -5,6 +5,7 @@
 #include <boost/algorithm/string.hpp>
 
 #include "storm-pomdp/analysis/FormulaInformation.h"
+#include "storm-pomdp/analysis/FiniteBeliefMdpDetection.h"
 
 #include "storm/utility/ConstantsComparator.h"
 #include "storm/utility/NumberTraits.h"
@@ -106,6 +107,9 @@ namespace storm {
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported formula '" << formula << "'.");
                 }
+                if (storm::pomdp::detectFiniteBeliefMdp(pomdp, formulaInfo.getTargetStates().states)) {
+                    STORM_PRINT_AND_LOG("Detected that the belief MDP is finite." << std::endl);
+                }
                 
                 if (options.refine) {
                     refineReachability(formulaInfo.getTargetStates().observations, formulaInfo.minimize(), rewardModelName, initialPomdpValueBounds.lower, initialPomdpValueBounds.upper, result);
@@ -172,7 +176,9 @@ namespace storm {
                         stream << ">=";
                     }
                     stream << statistics.underApproximationStates.get() << std::endl;
-                    stream << "# Exploration state limit for under-approximation: " << statistics.underApproximationStateLimit.get() << std::endl;
+                    if (statistics.underApproximationStateLimit) {
+                        stream << "# Exploration state limit for under-approximation: " << statistics.underApproximationStateLimit.get() << std::endl;
+                    }
                     stream << "# Time spend for building the under-approx grid MDP(s): " << statistics.underApproximationBuildTime << std::endl;
                     stream << "# Time spend for checking the under-approx grid MDP(s): " << statistics.underApproximationCheckTime << std::endl;
                 }