diff --git a/src/storm-pomdp/analysis/OneShotPolicySearch.h b/src/storm-pomdp/analysis/OneShotPolicySearch.h index 46d566d16..188abf3e4 100644 --- a/src/storm-pomdp/analysis/OneShotPolicySearch.h +++ b/src/storm-pomdp/analysis/OneShotPolicySearch.h @@ -21,7 +21,10 @@ namespace storm { template class OneShotPolicySearch { - // Implements to the Chatterjee, Chmelik, Davies (AAAI-16) paper. + /*! + * Implements to the Chatterjee, Chmelik, Davies (AAAI-16) paper. + * Tries to find a memoryless policy. + */ class Statistics { public: Statistics() = default; @@ -49,6 +52,11 @@ namespace storm { surelyReachSinkStates = surelyReachSink; } + /*! + * Check if you can find a memoryless policy from the initial states + * @param k The used lookahed + * @return Replies true, if a memoryless policy is found. Notice that the algorithm is not complete. + */ bool analyzeForInitialStates(uint64_t k) { STORM_LOG_TRACE("Bad states: " << surelyReachSinkStates); STORM_LOG_TRACE("Target states: " << targetStates); @@ -56,12 +64,11 @@ namespace storm { return analyze(k, ~surelyReachSinkStates & ~targetStates, pomdp.getInitialStates()); } + private: bool analyze(uint64_t k, storm::storage::BitVector const& oneOfTheseStates, storm::storage::BitVector const& allOfTheseStates = storm::storage::BitVector()); - private: void initialize(uint64_t k); - Statistics stats; std::unique_ptr smtSolver; storm::models::sparse::Pomdp const& pomdp; @@ -78,9 +85,6 @@ namespace storm { std::vector reachVars; std::vector reachVarExpressions; std::vector> pathVars; - - - }; } } diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp index 29c7da99e..8e00800dd 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -196,6 +196,5 @@ namespace storm { template class ObservationTraceUnfolder; template class ObservationTraceUnfolder; template class ObservationTraceUnfolder; - } }