From 31c39d1dc7f2025f49642738d275b35389726fad Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 5 Jun 2020 16:50:35 +0200 Subject: [PATCH] storm-pomdp: Cleaned up output of belief exploration. Use --verbose to restore it. --- .../BeliefExplorationPomdpModelChecker.cpp | 70 ++++++++++++------- .../BeliefExplorationPomdpModelChecker.h | 3 + .../TrivialPomdpValueBoundsModelChecker.h | 2 +- 3 files changed, 47 insertions(+), 28 deletions(-) diff --git a/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp b/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp index ca98052f5..a24c5f76b 100644 --- a/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp +++ b/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp @@ -68,7 +68,7 @@ namespace storm { } template - BeliefExplorationPomdpModelChecker::Statistics::Statistics() : overApproximationBuildAborted(false), underApproximationBuildAborted(false), aborted(false) { + BeliefExplorationPomdpModelChecker::Statistics::Statistics() : beliefMdpDetectedToBeFinite(false), refinementFixpointDetected(false), overApproximationBuildAborted(false), underApproximationBuildAborted(false), aborted(false) { // intentionally left empty; } @@ -97,7 +97,7 @@ namespace storm { auto initialPomdpValueBounds = TrivialPomdpValueBoundsModelChecker>(pomdp()).getValueBounds(formula, formulaInfo); uint64_t initialPomdpState = pomdp().getInitialStates().getNextSetIndex(0); Result result(initialPomdpValueBounds.getHighestLowerBound(initialPomdpState), initialPomdpValueBounds.getSmallestUpperBound(initialPomdpState)); - STORM_PRINT_AND_LOG("Initial value bounds are [" << result.lowerBound << ", " << result.upperBound << "]" << std::endl); + STORM_LOG_INFO("Initial value bounds are [" << result.lowerBound << ", " << result.upperBound << "]"); boost::optional rewardModelName; std::set targetObservations; @@ -123,7 +123,8 @@ namespace storm { 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); + STORM_LOG_INFO("Detected that the belief MDP is finite."); + statistics.beliefMdpDetectedToBeFinite = true; } if (options.refine) { @@ -153,6 +154,9 @@ namespace storm { pomdp().printModelInformationToStream(stream); stream << "# Max. Number of states with same observation: " << pomdp().getMaxNrStatesWithSameObservation() << std::endl; + if (statistics.beliefMdpDetectedToBeFinite) { + stream << "# Pre-computations detected that the belief MDP is finite."; + } if (statistics.aborted) { stream << "# Computation aborted early" << std::endl; } @@ -163,6 +167,9 @@ namespace storm { if (statistics.refinementSteps) { stream << "# Number of refinement steps: " << statistics.refinementSteps.get() << std::endl; } + if (statistics.refinementFixpointDetected) { + stream << "# Detected a refinement fixpoint." << std::endl; + } // The overapproximation MDP: if (statistics.overApproximationStates) { @@ -219,8 +226,13 @@ namespace storm { buildOverApproximation(targetObservations, min, rewardModelName.is_initialized(), false, heuristicParameters, observationResolutionVector, manager, approx); if (approx->hasComputedValues()) { - STORM_PRINT_AND_LOG("Explored and checked Over-Approximation MDP:\n"); - approx->getExploredMdp()->printModelInformationToStream(std::cout); + auto printInfo = [&approx]() { + std::stringstream str; + str << "Explored and checked Over-Approximation MDP:" << std::endl; + approx->getExploredMdp()->printModelInformationToStream(str); + return str.str(); + }; + STORM_LOG_INFO(printInfo()); ValueType& resultValue = min ? result.lowerBound : result.upperBound; resultValue = approx->getComputedValueAtInitialState(); } @@ -240,13 +252,18 @@ namespace storm { heuristicParameters.sizeThreshold = std::numeric_limits::max(); } else { heuristicParameters.sizeThreshold = pomdp().getNumberOfStates() * pomdp().getMaxNrStatesWithSameObservation(); - STORM_PRINT_AND_LOG("Heuristically selected an under-approximation mdp size threshold of " << heuristicParameters.sizeThreshold << "." << std::endl); + STORM_LOG_INFO("Heuristically selected an under-approximation mdp size threshold of " << heuristicParameters.sizeThreshold << "."); } } buildUnderApproximation(targetObservations, min, rewardModelName.is_initialized(), false, heuristicParameters, manager, approx); if (approx->hasComputedValues()) { - STORM_PRINT_AND_LOG("Explored and checked Under-Approximation MDP:\n"); - approx->getExploredMdp()->printModelInformationToStream(std::cout); + auto printInfo = [&approx]() { + std::stringstream str; + str << "Explored and checked Under-Approximation MDP:" << std::endl; + approx->getExploredMdp()->printModelInformationToStream(str); + return str.str(); + }; + STORM_LOG_INFO(printInfo()); ValueType& resultValue = min ? result.upperBound : result.lowerBound; resultValue = approx->getComputedValueAtInitialState(); } @@ -280,7 +297,7 @@ namespace storm { ValueType const& newValue = overApproximation->getComputedValueAtInitialState(); bool betterBound = min ? result.updateLowerBound(newValue) : result.updateUpperBound(newValue); if (betterBound) { - STORM_PRINT_AND_LOG("Over-approx result for refinement improved after " << statistics.totalTime << " seconds in refinement step #" << statistics.refinementSteps.get() << ". New value is '" << newValue << "'." << std::endl); + STORM_LOG_INFO("Over-approx result for refinement improved after " << statistics.totalTime << " seconds in refinement step #" << statistics.refinementSteps.get() << ". New value is '" << newValue << "'." << std::endl); } } @@ -307,30 +324,29 @@ namespace storm { ValueType const& newValue = underApproximation->getComputedValueAtInitialState(); bool betterBound = min ? result.updateUpperBound(newValue) : result.updateLowerBound(newValue); if (betterBound) { - STORM_PRINT_AND_LOG("Under-approx result for refinement improved after " << statistics.totalTime << " seconds in refinement step #" << statistics.refinementSteps.get() << ". New value is '" << newValue << "'." << std::endl); + STORM_LOG_INFO("Under-approx result for refinement improved after " << statistics.totalTime << " seconds in refinement step #" << statistics.refinementSteps.get() << ". New value is '" << newValue << "'." << std::endl); } } // Do some output - STORM_PRINT_AND_LOG("Completed iteration #" << statistics.refinementSteps.get() << ". Current checktime is " << statistics.totalTime << "."); + STORM_LOG_INFO("Completed iteration #" << statistics.refinementSteps.get() << ". Current checktime is " << statistics.totalTime << "."); bool computingLowerBound = false; bool computingUpperBound = false; if (options.discretize) { - STORM_PRINT_AND_LOG(" Over-approx MDP has size " << overApproximation->getExploredMdp()->getNumberOfStates() << "."); + STORM_LOG_INFO("\tOver-approx MDP has size " << overApproximation->getExploredMdp()->getNumberOfStates() << "."); (min ? computingLowerBound : computingUpperBound) = true; } if (options.unfold) { - STORM_PRINT_AND_LOG(" Under-approx MDP has size " << underApproximation->getExploredMdp()->getNumberOfStates() << "."); + STORM_LOG_INFO("\tUnder-approx MDP has size " << underApproximation->getExploredMdp()->getNumberOfStates() << "."); (min ? computingUpperBound : computingLowerBound) = true; } if (computingLowerBound && computingUpperBound) { - STORM_PRINT_AND_LOG(" Current result is [" << result.lowerBound << ", " << result.upperBound << "]."); + STORM_LOG_INFO("\tCurrent result is [" << result.lowerBound << ", " << result.upperBound << "]."); } else if (computingLowerBound) { - STORM_PRINT_AND_LOG(" Current result is ≥" << result.lowerBound << "."); + STORM_LOG_INFO("\tCurrent result is ≥" << result.lowerBound << "."); } else if (computingUpperBound) { - STORM_PRINT_AND_LOG(" Current result is ≤" << result.upperBound << "."); + STORM_LOG_INFO("\tCurrent result is ≤" << result.upperBound << "."); } - STORM_PRINT_AND_LOG(std::endl); // Start refinement STORM_LOG_WARN_COND(options.refineStepLimit.is_initialized() || !storm::utility::isZero(options.refinePrecision), "No termination criterion for refinement given. Consider to specify a steplimit, a non-zero precisionlimit, or a timeout"); @@ -354,7 +370,7 @@ namespace storm { ValueType const& newValue = overApproximation->getComputedValueAtInitialState(); bool betterBound = min ? result.updateLowerBound(newValue) : result.updateUpperBound(newValue); if (betterBound) { - STORM_PRINT_AND_LOG("Over-approx result for refinement improved after " << statistics.totalTime << " in refinement step #" << (statistics.refinementSteps.get() + 1) << ". New value is '" << newValue << "'." << std::endl); + STORM_LOG_INFO("Over-approx result for refinement improved after " << statistics.totalTime << " in refinement step #" << (statistics.refinementSteps.get() + 1) << ". New value is '" << newValue << "'."); } } else { break; @@ -371,7 +387,7 @@ namespace storm { ValueType const& newValue = underApproximation->getComputedValueAtInitialState(); bool betterBound = min ? result.updateUpperBound(newValue) : result.updateLowerBound(newValue); if (betterBound) { - STORM_PRINT_AND_LOG("Under-approx result for refinement improved after " << statistics.totalTime << " in refinement step #" << (statistics.refinementSteps.get() + 1) << ". New value is '" << newValue << "'." << std::endl); + STORM_LOG_INFO("Under-approx result for refinement improved after " << statistics.totalTime << " in refinement step #" << (statistics.refinementSteps.get() + 1) << ". New value is '" << newValue << "'."); } } else { break; @@ -384,30 +400,30 @@ namespace storm { ++statistics.refinementSteps.get(); // Don't make too many outputs (to avoid logfile clutter) if (statistics.refinementSteps.get() <= 1000) { - STORM_PRINT_AND_LOG("Completed iteration #" << statistics.refinementSteps.get() << ". Current checktime is " << statistics.totalTime << "."); + STORM_LOG_INFO("Completed iteration #" << statistics.refinementSteps.get() << ". Current checktime is " << statistics.totalTime << "."); bool computingLowerBound = false; bool computingUpperBound = false; if (options.discretize) { - STORM_PRINT_AND_LOG(" Over-approx MDP has size " << overApproximation->getExploredMdp()->getNumberOfStates() << "."); + STORM_LOG_INFO("\tOver-approx MDP has size " << overApproximation->getExploredMdp()->getNumberOfStates() << "."); (min ? computingLowerBound : computingUpperBound) = true; } if (options.unfold) { - STORM_PRINT_AND_LOG(" Under-approx MDP has size " << underApproximation->getExploredMdp()->getNumberOfStates() << "."); + STORM_LOG_INFO("\tUnder-approx MDP has size " << underApproximation->getExploredMdp()->getNumberOfStates() << "."); (min ? computingUpperBound : computingLowerBound) = true; } if (computingLowerBound && computingUpperBound) { - STORM_PRINT_AND_LOG(" Current result is [" << result.lowerBound << ", " << result.upperBound << "]."); + STORM_LOG_INFO("\tCurrent result is [" << result.lowerBound << ", " << result.upperBound << "]."); } else if (computingLowerBound) { - STORM_PRINT_AND_LOG(" Current result is ≥" << result.lowerBound << "."); + STORM_LOG_INFO("\tCurrent result is ≥" << result.lowerBound << "."); } else if (computingUpperBound) { - STORM_PRINT_AND_LOG(" Current result is ≤" << result.upperBound << "."); + STORM_LOG_INFO("\tCurrent result is ≤" << result.upperBound << "."); } - STORM_PRINT_AND_LOG(std::endl); STORM_LOG_WARN_COND(statistics.refinementSteps.get() < 1000, "Refinement requires more than 1000 iterations."); } } if (overApproxFixPoint && underApproxFixPoint) { - STORM_PRINT_AND_LOG("Refinement fixpoint reached after " << statistics.refinementSteps.get() << " iterations." << std::endl); + STORM_LOG_INFO("Refinement fixpoint reached after " << statistics.refinementSteps.get() << " iterations." << std::endl); + statistics.refinementFixpointDetected = true; break; } } diff --git a/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h b/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h index 488bf2445..88e6121fb 100644 --- a/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h +++ b/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h @@ -101,6 +101,9 @@ namespace storm { boost::optional refinementSteps; storm::utility::Stopwatch totalTime; + bool beliefMdpDetectedToBeFinite; + bool refinementFixpointDetected; + boost::optional overApproximationStates; bool overApproximationBuildAborted; storm::utility::Stopwatch overApproximationBuildTime; diff --git a/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h b/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h index 0120f0817..08c232f70 100644 --- a/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h +++ b/src/storm-pomdp/modelchecker/TrivialPomdpValueBoundsModelChecker.h @@ -183,7 +183,7 @@ namespace storm { } } } - std::cout << "Keeping scheduler guesses " << keptGuesses << std::endl; + STORM_LOG_INFO("Keeping scheduler guesses " << keptGuesses); storm::utility::vector::filterVectorInPlace(guessedSchedulerValues, keptGuesses); // Finally prepare the result