diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index d8b56e74d..3945acb29 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -73,6 +73,40 @@ namespace storm { } } + template + void ApproximatePOMDPModelchecker::printStatisticsToStream(std::ostream& stream) const { + stream << "##### Grid Approximation Statistics ######" << std::endl; + stream << "# Input model: " << std::endl; + pomdp.printModelInformationToStream(stream); + stream << "# Max. Number of states with same observation: " << pomdp.getMaxNrStatesWithSameObservation() << std::endl; + + if (statistics.aborted) { + stream << "# Computation aborted early"; + } + + // Refinement information: + if (statistics.refinementSteps) { + stream << "# Number of refinement steps " << statistics.refinementSteps.get(); + } + + // The overapproximation MDP: + if (statistics.overApproximationStates) { + stream << "# Number of states in the "; + if (options.doRefinement) { + stream << "final "; + } + stream << "grid MDP for the over-approximation: "; + if (statistics.overApproximationBuildAborted) { + stream << ">="; + } + stream << statistics.overApproximationStates.get() << std::endl; + stream << "# Time spend for building the grid MDP(s): " << statistics.overApproximationBuildTime << std::endl; + stream << "# Time spend for checking the grid MDP(s): " << statistics.overApproximationCheckTime << std::endl; + } + + stream << "##########################################" << std::endl; + } + template std::unique_ptr> diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h index 6837151cd..df47c721a 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h @@ -66,6 +66,8 @@ namespace storm { std::unique_ptr> check(storm::logic::Formula const& formula); + void printStatisticsToStream(std::ostream& stream) const; + private: /** * Compute the reachability probability of given target observations on a POMDP using the automatic refinement loop @@ -240,7 +242,16 @@ namespace storm { */ ValueType getRewardAfterAction(uint64_t action, storm::pomdp::Belief &belief); - + struct Statistics { + boost::optional overApproximationStates; + bool overApproximationBuildAborted; + storm::utility::Stopwatch overApproximationBuildTime; + storm::utility::Stopwatch overApproximationCheckTime; + boost::optional refinementSteps; + bool aborted; + }; + Statistics statistics; + storm::models::sparse::Pomdp const& pomdp; Options options; storm::utility::ConstantsComparator cc; diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index aaad3a9e8..5b2e2a8a6 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -54,10 +54,27 @@ namespace storm { return nrObservations; } + template + uint64_t Pomdp::getMaxNrStatesWithSameObservation() const { + std::map counts; + for (auto const& obs : observations) { + auto insertionRes = counts.emplace(obs, 1ull); + if (!insertionRes.second) { + ++insertionRes.first->second; + } + } + uint64_t result = 0; + for (auto const& count : counts) { + result = std::max(result, count.second); + } + return result; + } + template std::vector const& Pomdp::getObservations() const { return observations; } + template std::string Pomdp::additionalDotStateInfo(uint64_t state) const { diff --git a/src/storm/models/sparse/Pomdp.h b/src/storm/models/sparse/Pomdp.h index a9e6c7e95..b09f87886 100644 --- a/src/storm/models/sparse/Pomdp.h +++ b/src/storm/models/sparse/Pomdp.h @@ -59,13 +59,17 @@ namespace storm { uint64_t getNrObservations() const; + /*! + * Returns the number of hidden values, i.e. the maximum number of states with the same observation + */ + uint64_t getMaxNrStatesWithSameObservation() const; + std::vector const& getObservations() const; std::vector getStatesWithObservation(uint32_t observation) const; + bool isCanonic() const; - - protected: /*! * Return a string that is additonally added to the state information in the dot stream.