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<typename ValueType>
void BeliefExplorationSettings::setValuesInOptionsStruct(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) const {
options.refine = isRefineSet();
- options.refinePrecision = getRefinePrecision();
+ options.refinePrecision = storm::utility::convertNumber<ValueType>(getRefinePrecision());
if (isRefineStepLimitSet()) {
options.refineStepLimit = getRefineStepLimit();
} else {
@@ -158,7 +158,7 @@ namespace storm {
options.obsThresholdInit = storm::utility::convertNumber<ValueType>(getObservationScoreThresholdInit());
options.obsThresholdIncrementFactor = storm::utility::convertNumber<ValueType>(getObservationScoreThresholdFactor());
- options.numericPrecision = getNumericPrecision();
+ options.numericPrecision = storm::utility::convertNumber<ValueType>(getNumericPrecision());
if (storm::NumberTraits<ValueType>::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<PomdpModelType, BeliefValueType>::Result::diff(bool relative) const {
ValueType diff = upperBound - lowerBound;
if (diff < storm::utility::zero<ValueType>()) {
- 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<ValueType>(1e-6), "Upper bound '" << upperBound << "' is smaller than lower bound '" << lowerBound << "': Difference is " << diff << ".");
diff = storm::utility::zero<ValueType >();
}
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<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>> AbstractionInformation<DdType>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const {
std::map<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>> result;
- storm::dd::Add<DdType, double> lowerChoiceAsAdd = choice.template toAdd<double>();
+ storm::dd::Add<DdType, ValueType> lowerChoiceAsAdd = choice.template toAdd<ValueType>();
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<storm::RationalNumber>(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<storm::RationalNumber>(tbSettings.getPrecision());
relative = tbSettings.isRelativePrecision();
- unifPlusKappa = tbSettings.getUnifPlusKappa();
+ unifPlusKappa = storm::utility::convertNumber<storm::RationalNumber>(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<storm::dd::DdType Type, typename ModelType>
- GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, GameBasedMdpModelCheckerOptions const& options, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : options(options), smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision(), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()), debug(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isDebugSet()) {
+ GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, GameBasedMdpModelCheckerOptions const& options, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : options(options), smtSolverFactory(smtSolverFactory), comparator(storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()), debug(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isDebugSet()) {
if (model.hasUndefinedConstants()) {
auto undefinedConstants = model.getUndefinedConstants();
@@ -1119,7 +1119,7 @@ namespace storm {
}
if (sanityCheck) {
- storm::utility::ConstantsComparator<ValueType> sanityComparator( 1e-6, true);
+ storm::utility::ConstantsComparator<ValueType> sanityComparator( storm::utility::convertNumber<ValueType>(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<ValueType>()) {
+ if (hi < storm::utility::zero<GeometryValueType>()) {
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<GeometryValueType>(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<SparseModelType, GeometryValueType>::negateMinObjectives(std::vector<GeometryValueType>& vector) const {
for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
if (objectiveHelper[objIndex].minimizing()) {
- vector[objIndex] *= -storm::utility::one<ModelValueType>();
+ vector[objIndex] *= -storm::utility::one<GeometryValueType>();
}
}
}
@@ -484,7 +484,7 @@ namespace storm {
template <class SparseModelType, typename GeometryValueType>
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::initializeFacets(Environment const& env) {
for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
- std::vector<GeometryValueType> weightVector(objectives.size(), storm::utility::zero<ModelValueType>());
+ std::vector<GeometryValueType> weightVector(objectives.size(), storm::utility::zero<GeometryValueType>());
weightVector[objIndex] = storm::utility::one<GeometryValueType>();
std::vector<GeometryValueType> 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<ValueType, ValueType>(value * (1/(prec + 1)), value * (1 + prec/(prec +1)));
+ ValueType one = storm::utility::one<ValueType>();
+ ValueType lower = value * (one / (prec + one));
+ ValueType upper = value * (one + prec / (prec + one));
+ return std::make_pair(lower, upper);
} else {
- return std::make_pair<ValueType, ValueType>(value - prec, value + prec);
+ return std::pair<ValueType, ValueType>(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<ValueType>::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<ValueType>(this->actualRelativeMILPGap);
} else {
- return storm::utility::abs<ValueType>(this->actualRelativeMILPGap * getObjectiveValue());
+ return storm::utility::abs<ValueType>(storm::utility::convertNumber<ValueType>(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<storm::RationalNumber>(this->getRationalValue(variable.first));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
}