Browse Source

Only display the bound that was requested.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
2d94e77f2a
  1. 13
      src/storm-pomdp-cli/storm-pomdp.cpp
  2. 8
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp

13
src/storm-pomdp-cli/storm-pomdp.cpp

@ -84,7 +84,20 @@ namespace storm {
template<typename ValueType>
void printResult(ValueType const& lowerBound, ValueType const& upperBound) {
if (lowerBound == upperBound) {
if (storm::utility::isInfinity(lowerBound)) {
STORM_PRINT_AND_LOG("inf");
} else {
STORM_PRINT_AND_LOG(lowerBound);
}
} else if (storm::utility::isInfinity<ValueType>(-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) << ")");
}

8
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<ValueType>();
}
if ((formulaInfo.maximize() && !options.discretize) || (formulaInfo.minimize() && !options.unfold)) {
result.upperBound = storm::utility::infinity<ValueType>();
}
if (storm::utility::resources::isTerminate()) {
statistics.aborted = true;
}

Loading…
Cancel
Save