From dd7dc4b797c2956a21ab502d107dd0039cd89ba3 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 18 May 2020 11:21:13 +0200 Subject: [PATCH] Towards allowing CLN numbers for RationalNumbers again. --- .../settings/modules/BeliefExplorationSettings.cpp | 4 ++-- .../modelchecker/ApproximatePOMDPModelchecker.cpp | 2 +- src/storm-pomdp/storage/BeliefManager.h | 2 +- src/storm/abstraction/AbstractionInformation.cpp | 2 +- .../environment/solver/LongRunAverageSolverEnvironment.cpp | 2 +- .../environment/solver/TimeBoundedSolverEnvironment.cpp | 2 +- .../modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 4 ++-- .../deterministicScheds/DeterministicSchedsLpChecker.cpp | 4 ++-- .../DeterministicSchedsParetoExplorer.cpp | 4 ++-- .../prctl/helper/rewardbounded/QuantileHelper.cpp | 7 +++++-- src/storm/solver/GlpkLpSolver.cpp | 4 ++-- src/storm/storage/expressions/SimpleValuation.cpp | 2 +- 12 files changed, 21 insertions(+), 18 deletions(-) diff --git a/src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.cpp b/src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.cpp index dc42679aa..ca0d13a80 100644 --- a/src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.cpp @@ -136,7 +136,7 @@ namespace storm { template void BeliefExplorationSettings::setValuesInOptionsStruct(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions& options) const { options.refine = isRefineSet(); - options.refinePrecision = getRefinePrecision(); + options.refinePrecision = storm::utility::convertNumber(getRefinePrecision()); if (isRefineStepLimitSet()) { options.refineStepLimit = getRefineStepLimit(); } else { @@ -158,7 +158,7 @@ namespace storm { options.obsThresholdInit = storm::utility::convertNumber(getObservationScoreThresholdInit()); options.obsThresholdIncrementFactor = storm::utility::convertNumber(getObservationScoreThresholdFactor()); - options.numericPrecision = getNumericPrecision(); + options.numericPrecision = storm::utility::convertNumber(getNumericPrecision()); if (storm::NumberTraits::IsExact) { if (isNumericPrecisionSetFromDefault()) { STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "Setting numeric precision to zero because exact arithmethic is used."); diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index 2e8619819..d9d97273d 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -39,7 +39,7 @@ namespace storm { ApproximatePOMDPModelchecker::Result::diff(bool relative) const { ValueType diff = upperBound - lowerBound; if (diff < storm::utility::zero()) { - STORM_LOG_WARN_COND(diff >= 1e-6, "Upper bound '" << upperBound << "' is smaller than lower bound '" << lowerBound << "': Difference is " << diff << "."); + STORM_LOG_WARN_COND(diff >= storm::utility::convertNumber(1e-6), "Upper bound '" << upperBound << "' is smaller than lower bound '" << lowerBound << "': Difference is " << diff << "."); diff = storm::utility::zero(); } if (relative && !storm::utility::isZero(upperBound)) { diff --git a/src/storm-pomdp/storage/BeliefManager.h b/src/storm-pomdp/storage/BeliefManager.h index 4f9ca445c..dbe05d3e4 100644 --- a/src/storm-pomdp/storage/BeliefManager.h +++ b/src/storm-pomdp/storage/BeliefManager.h @@ -310,7 +310,7 @@ namespace storm { BeliefValueType x = resolution; for (auto const& entry : belief) { qsRow.push_back(storm::utility::floor(x)); // v - sorted_diffs.emplace(toOriginalIndicesMap.size(), x - qsRow.back()); // x-v + sorted_diffs.emplace(toOriginalIndicesMap.size(), ValueType(x - qsRow.back())); // x-v toOriginalIndicesMap.push_back(entry.first); x -= entry.second * resolution; } diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 23fb06985..8e97ccf22 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -465,7 +465,7 @@ namespace storm { std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const { std::map> result; - storm::dd::Add lowerChoiceAsAdd = choice.template toAdd(); + storm::dd::Add lowerChoiceAsAdd = choice.template toAdd(); for (auto const& successorValuePair : lowerChoiceAsAdd) { uint_fast64_t updateIndex = this->decodeAux(successorValuePair.first, 0, this->getAuxVariableCount()); diff --git a/src/storm/environment/solver/LongRunAverageSolverEnvironment.cpp b/src/storm/environment/solver/LongRunAverageSolverEnvironment.cpp index 83e9d4f7d..49f555f20 100644 --- a/src/storm/environment/solver/LongRunAverageSolverEnvironment.cpp +++ b/src/storm/environment/solver/LongRunAverageSolverEnvironment.cpp @@ -18,7 +18,7 @@ namespace storm { if (lraSettings.isMaximalIterationCountSet()) { maxIters = lraSettings.getMaximalIterationCount(); } - aperiodicFactor = lraSettings.getAperiodicFactor(); + aperiodicFactor = storm::utility::convertNumber(lraSettings.getAperiodicFactor()); } LongRunAverageSolverEnvironment::~LongRunAverageSolverEnvironment() { diff --git a/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp b/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp index 743474e4b..655fb87dd 100644 --- a/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp +++ b/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp @@ -13,7 +13,7 @@ namespace storm { maMethodSetFromDefault = tbSettings.isMaMethodSetFromDefaultValue(); precision = storm::utility::convertNumber(tbSettings.getPrecision()); relative = tbSettings.isRelativePrecision(); - unifPlusKappa = tbSettings.getUnifPlusKappa(); + unifPlusKappa = storm::utility::convertNumber(tbSettings.getUnifPlusKappa()); } TimeBoundedSolverEnvironment::~TimeBoundedSolverEnvironment() { diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index b9623a5ee..60c194c47 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -60,7 +60,7 @@ namespace storm { using detail::PreviousExplicitResult; template - GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, GameBasedMdpModelCheckerOptions const& options, std::shared_ptr const& smtSolverFactory) : options(options), smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision(), storm::settings::getModule().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()), debug(storm::settings::getModule().isDebugSet()) { + GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, GameBasedMdpModelCheckerOptions const& options, std::shared_ptr const& smtSolverFactory) : options(options), smtSolverFactory(smtSolverFactory), comparator(storm::utility::convertNumber(storm::settings::getModule().getPrecision()), storm::settings::getModule().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()), debug(storm::settings::getModule().isDebugSet()) { if (model.hasUndefinedConstants()) { auto undefinedConstants = model.getUndefinedConstants(); @@ -1119,7 +1119,7 @@ namespace storm { } if (sanityCheck) { - storm::utility::ConstantsComparator sanityComparator( 1e-6, true); + storm::utility::ConstantsComparator sanityComparator( storm::utility::convertNumber(1e-6), true); ///////// SANITY CHECK: apply lower strategy, obtain DTMC matrix and model check it. the values should ///////// still be the lower ones. diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index 17f9ebd1c..b4c97539f 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -663,7 +663,7 @@ namespace storm { // The issue has to be for some normal vector with a negative entry. Otherwise, the intersection with the downward closure wouldn't be empty bool normalVectorContainsNegative = false; for (auto const& hi : h.normalVector()) { - if (hi < storm::utility::zero()) { + if (hi < storm::utility::zero()) { normalVectorContainsNegative = true; break; } @@ -743,7 +743,7 @@ namespace storm { if (objectiveHelper[objIndex].minimizing()) { inducedValue = -inducedValue; } - inducedPoint.push_back(inducedValue); + inducedPoint.push_back(storm::utility::convertNumber(inducedValue)); // If this objective has weight zero, the lp solution is not necessarily correct if (!storm::utility::isZero(currentWeightVector[objIndex])) { ValueType lpValue = lpModel->getContinuousValue(currentObjectiveVariables[objIndex]); diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index 11f62e1f2..c1a6ff492 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -476,7 +476,7 @@ namespace storm { void DeterministicSchedsParetoExplorer::negateMinObjectives(std::vector& vector) const { for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { if (objectiveHelper[objIndex].minimizing()) { - vector[objIndex] *= -storm::utility::one(); + vector[objIndex] *= -storm::utility::one(); } } } @@ -484,7 +484,7 @@ namespace storm { template void DeterministicSchedsParetoExplorer::initializeFacets(Environment const& env) { for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - std::vector weightVector(objectives.size(), storm::utility::zero()); + std::vector weightVector(objectives.size(), storm::utility::zero()); weightVector[objIndex] = storm::utility::one(); std::vector point; if (wvChecker) { diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index b39eb2b27..fc2f39099 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -152,9 +152,12 @@ namespace storm { } prec *= factor; if (relative) { - return std::make_pair(value * (1/(prec + 1)), value * (1 + prec/(prec +1))); + ValueType one = storm::utility::one(); + ValueType lower = value * (one / (prec + one)); + ValueType upper = value * (one + prec / (prec + one)); + return std::make_pair(lower, upper); } else { - return std::make_pair(value - prec, value + prec); + return std::pair(value - prec, value + prec); } } diff --git a/src/storm/solver/GlpkLpSolver.cpp b/src/storm/solver/GlpkLpSolver.cpp index 032ab2e76..a4be10cd4 100644 --- a/src/storm/solver/GlpkLpSolver.cpp +++ b/src/storm/solver/GlpkLpSolver.cpp @@ -512,9 +512,9 @@ namespace storm { ValueType GlpkLpSolver::getMILPGap(bool relative) const { STORM_LOG_ASSERT(this->isOptimal(), "Asked for the MILP gap although there is no (bounded) solution."); if (relative) { - return this->actualRelativeMILPGap; + return storm::utility::convertNumber(this->actualRelativeMILPGap); } else { - return storm::utility::abs(this->actualRelativeMILPGap * getObjectiveValue()); + return storm::utility::abs(storm::utility::convertNumber(this->actualRelativeMILPGap) * getObjectiveValue()); } } diff --git a/src/storm/storage/expressions/SimpleValuation.cpp b/src/storm/storage/expressions/SimpleValuation.cpp index 4ed71239a..b91cd1f0f 100644 --- a/src/storm/storage/expressions/SimpleValuation.cpp +++ b/src/storm/storage/expressions/SimpleValuation.cpp @@ -152,7 +152,7 @@ namespace storm { } else if (variable.second.isIntegerType()) { result[variable.first.getName()] = this->getIntegerValue(variable.first); } else if (variable.second.isRationalType()) { - result[variable.first.getName()] = this->getRationalValue(variable.first); + result[variable.first.getName()] = storm::utility::convertNumber(this->getRationalValue(variable.first)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); }