diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index ac48327b5..6cca313e8 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -32,6 +32,8 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/NumberTraits.h" #include "storm/utility/Stopwatch.h" +#include "storm/utility/SignalHandler.h" +#include "storm/utility/NumberTraits.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/NotSupportedException.h" @@ -79,6 +81,20 @@ namespace storm { return preprocessingPerformed; } + template + void printResult(ValueType const& lowerBound, ValueType const& upperBound) { + if (lowerBound == upperBound) { + STORM_PRINT_AND_LOG(lowerBound); + } else { + STORM_PRINT_AND_LOG("[" << lowerBound << ", " << upperBound << "] (width=" << ValueType(upperBound - lowerBound) << ")"); + } + if (storm::NumberTraits::IsExact) { + STORM_PRINT_AND_LOG(" (approx. "); + printResult(storm::utility::convertNumber(lowerBound), storm::utility::convertNumber(upperBound)); + STORM_PRINT_AND_LOG(")"); + } + } + template bool performAnalysis(std::shared_ptr> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) { auto const& pomdpSettings = storm::settings::getModule(); @@ -103,14 +119,13 @@ namespace storm { } storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(*pomdp, options); std::unique_ptr> result = checker.check(formula); - ValueType overRes = result->overApproxValue; - ValueType underRes = result->underApproxValue; - if (overRes != underRes) { - STORM_PRINT("Overapproximation Result: " << overRes << std::endl); - STORM_PRINT("Underapproximation Result: " << underRes << std::endl); + checker.printStatisticsToStream(std::cout); + if (storm::utility::resources::isTerminate()) { + STORM_PRINT_AND_LOG("Result till abort: ") } else { - STORM_PRINT("Result: " << overRes << std::endl) + STORM_PRINT_AND_LOG("Result: ") } + printResult(result->underApproxValue, result->overApproxValue); analysisPerformed = true; } if (pomdpSettings.isMemlessSearchSet()) {