From c33ac18a5a63e391120bb1365b58130305e4916f Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 13 Mar 2019 09:35:07 +0100 Subject: [PATCH] Quantiles: Fixed a precision related issue in new implementation. --- .../prctl/helper/rewardbounded/EpochManager.cpp | 11 +++++++++++ .../prctl/helper/rewardbounded/EpochManager.h | 1 + .../MultiDimensionalRewardUnfolding.cpp | 6 +----- .../helper/rewardbounded/QuantileHelper.cpp | 16 ++++++++++------ 4 files changed, 23 insertions(+), 11 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.cpp index e248a74da..3537b618e 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.cpp +++ b/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))); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h index 6784cdac4..b1ff3e5ce 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h +++ b/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; diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 5d82672eb..fad4feda2 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -711,11 +711,7 @@ namespace storm { template ValueType MultiDimensionalRewardUnfolding::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(sumOfDimensions); + return precision / storm::utility::convertNumber(epochManager.getSumOfDimensions(startEpoch) + 1); } template diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index e78354752..d2f6c1c80 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/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 - std::pair getLowerUpperBound(storm::Environment const& env, ValueType const& value, bool minMax = true) { + std::pair 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(value * (1/(prec + 1)), value * (1 + prec/(prec +1))); + return std::make_pair((value * (1/(prec + 1))) * factor, (value * (1 + prec/(prec +1))) * factor); } else { - return std::make_pair(value - prec, value + prec); + return std::make_pair((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(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.