Quantiles: Fixed a precision related issue in new implementation.

src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.cpp

@@ -210,6 +210,17 @@ namespace storm {
                     return (epoch >> (dimension * bitsPerDimension)) & dimensionBitMask;
                 }
                 
+                uint64_t EpochManager::getSumOfDimensions(Epoch const& epoch) const {
+                    STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
+                    uint64_t sumOfDimensions = 0;
+                    for (uint64_t dim = 0; dim < getDimensionCount(); ++dim) {
+                        if (!isBottomDimension(epoch, dim)) {
+                            sumOfDimensions += getDimensionOfEpoch(epoch, dim) + 1;
+                        }
+                    }
+                    return sumOfDimensions;
+                }
+                
                 std::string EpochManager::toString(Epoch const& epoch) const {
                     STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                     std::string res = "<" + (isBottomDimension(epoch, 0) ? "_" : std::to_string(getDimensionOfEpoch(epoch, 0)));

src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h

@@ -45,6 +45,7 @@ namespace storm {
                     bool isBottomDimension(Epoch const& epoch, uint64_t const& dimension) const;
                     bool isBottomDimensionEpochClass(EpochClass const& epochClass, uint64_t const& dimension) const;
                     uint64_t getDimensionOfEpoch(Epoch const& epoch, uint64_t const& dimension) const; // assumes that the dimension is not bottom
+                    uint64_t getSumOfDimensions(Epoch const& epoch) const; // assumes that the dimension is not bottom
                     
                     std::string toString(Epoch const& epoch) const;
                     

src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp

@@ -711,11 +711,7 @@ namespace storm {
                 
                 template<typename ValueType, bool SingleObjectiveMode>
                 ValueType MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getRequiredEpochModelPrecision(Epoch const& startEpoch, ValueType const& precision) {
-                    uint64_t sumOfDimensions = 0;
-                    for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
-                        sumOfDimensions += epochManager.getDimensionOfEpoch(startEpoch, dim) + 1;
-                    }
-                    return precision / storm::utility::convertNumber<ValueType>(sumOfDimensions);
+                    return precision / storm::utility::convertNumber<ValueType>(epochManager.getSumOfDimensions(startEpoch) + 1);
                 }
                 
                 template<typename ValueType, bool SingleObjectiveMode>

src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp

@@ -64,9 +64,9 @@ namespace storm {
                     }
                     
                     // TODO
-                    // Fix precision increasing
                     // Multiple quantile formulas in the same file yield constants def clash
                     // ignore optimization direction for quantile variables
+                    // Test cases
                 }
 
                 enum class BoundTransformation {
@@ -139,9 +139,12 @@ namespace storm {
                     env.solver().minMax().setPrecision(env.solver().minMax().getPrecision() * factor);
                 }
                 
-                /// Computes a lower/ upper bound on the actual result of a minmax or linear equation solver
+                /*!
+                 * Computes a lower / upper bound on the actual result of a sound minmax or linear equation solver
+                 *
+                 */
                 template<typename ValueType>
-                std::pair<ValueType, ValueType> getLowerUpperBound(storm::Environment const& env, ValueType const& value, bool minMax = true) {
+                std::pair<ValueType, ValueType> getLowerUpperBound(storm::Environment const& env, ValueType const& factor, ValueType const& value, bool minMax = true) {
                     ValueType prec;
                     bool relative;
                     if (minMax) {
@@ -152,9 +155,9 @@ namespace storm {
                         relative = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType()).second.get();
                     }
                     if (relative) {
-                        return std::make_pair<ValueType, ValueType>(value * (1/(prec + 1)), value * (1 + prec/(prec +1)));
+                        return std::make_pair<ValueType, ValueType>((value * (1/(prec + 1))) * factor, (value * (1 + prec/(prec +1))) * factor);
                     } else {
-                        return std::make_pair<ValueType, ValueType>(value - prec, value + prec);
+                        return std::make_pair<ValueType, ValueType>((value - prec) * factor, (value + prec) * factor);
                     }
                 }
                 
@@ -402,7 +405,8 @@ namespace storm {
                                             ValueType currValue = rewardUnfolding.getInitialStateResult(epoch);
                                             bool propertySatisfied;
                                             if (env.solver().isForceSoundness()) {
-                                                auto lowerUpperValue = getLowerUpperBound(env, currValue);
+                                                ValueType  sumOfEpochDimensions = storm::utility::convertNumber<ValueType>(rewardUnfolding.getEpochManager().getSumOfDimensions(epoch) + 1);
+                                                auto lowerUpperValue = getLowerUpperBound(env, sumOfEpochDimensions, currValue);
                                                 propertySatisfied =  boundedUntilOperator.getBound().isSatisfied(lowerUpperValue.first);
                                                 if (propertySatisfied !=  boundedUntilOperator.getBound().isSatisfied(lowerUpperValue.second)) {
                                                     // unclear result due to insufficient precision.