diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index ebfa22e7c..ceddcc4b7 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -84,7 +84,20 @@ namespace storm { template void printResult(ValueType const& lowerBound, ValueType const& upperBound) { if (lowerBound == upperBound) { - STORM_PRINT_AND_LOG(lowerBound); + if (storm::utility::isInfinity(lowerBound)) { + STORM_PRINT_AND_LOG("inf"); + } else { + STORM_PRINT_AND_LOG(lowerBound); + } + } else if (storm::utility::isInfinity(-lowerBound)) { + if (storm::utility::isInfinity(upperBound)) { + STORM_PRINT_AND_LOG("[-inf, inf] (width=inf)"); + } else { + // Only upper bound is known + STORM_PRINT_AND_LOG("≤ " << upperBound); + } + } else if (storm::utility::isInfinity(upperBound)) { + STORM_PRINT_AND_LOG("≥ " << lowerBound); } else { STORM_PRINT_AND_LOG("[" << lowerBound << ", " << upperBound << "] (width=" << ValueType(upperBound - lowerBound) << ")"); } diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index 4f95793eb..f44eb3381 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -111,6 +111,14 @@ namespace storm { } else { computeReachabilityOTF(formulaInfo.getTargetStates().observations, formulaInfo.minimize(), rewardModelName, initialPomdpValueBounds.lower, initialPomdpValueBounds.upper, result); } + // "clear" results in case they were actually not requested (this will make the output a bit more clear) + if ((formulaInfo.minimize() && !options.discretize) || (formulaInfo.maximize() && !options.unfold)) { + result.lowerBound = -storm::utility::infinity(); + } + if ((formulaInfo.maximize() && !options.discretize) || (formulaInfo.minimize() && !options.unfold)) { + result.upperBound = storm::utility::infinity(); + } + if (storm::utility::resources::isTerminate()) { statistics.aborted = true; }