diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
index da2e94f71..cfc39912c 100644
--- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp
+++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
@@ -71,7 +71,7 @@ char* storm_rational_number_to_str(storm_rational_number_ptr val, char *buf, siz
storm::RationalNumber const& srn_a = *(storm::RationalNumber*)val;
ss << srn_a;
std::string s = ss.str();
- if (s.size() < buflen + 1) {
+ if (s.size() + 1 < buflen) {
std::memcpy(buf, s.c_str(), s.size() + 1);
return buf;
} else {
@@ -286,7 +286,6 @@ void print_storm_rational_number(storm_rational_number_ptr a) {
#endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
- std::cout << srn_a << std::flush;
}
void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out) {
@@ -334,7 +333,7 @@ int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational
return (srf_a == srf_b) ? 1 : 0;
}
-char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen) {
+char* storm_rational_function_to_str(storm_rational_function_ptr val, char* buf, size_t buflen) {
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif
@@ -343,12 +342,12 @@ char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf,
storm::RationalFunction const& srf_a = *(storm::RationalFunction*)val;
ss << srf_a;
std::string s = ss.str();
- if (s.size() < buflen + 1) {
- std::memcpy(buf, s.c_str(), s.size() + 1);
+ if (s.size() + 1 < buflen) {
+ std::strcpy(buf, s.c_str());
return buf;
} else {
char* result = (char*)malloc(s.size() + 1);
- std::memcpy(result, s.c_str(), s.size() + 1);
+ std::strcpy(result, s.c_str());
return result;
}
}
@@ -485,7 +484,7 @@ storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
- if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+ if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) {
throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be non-constant rational functions.";
}
throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational functions.";
@@ -522,11 +521,11 @@ int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_f
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
- if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+ if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) {
throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions.";
}
- if (srf_a.nominatorAsNumber() < srf_b.nominatorAsNumber()) {
+ if (storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a) < storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b)) {
return 1;
} else {
return 0;
@@ -541,11 +540,11 @@ int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_r
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
- if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+ if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) {
throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions.";
}
- if (srf_a.nominatorAsNumber() <= srf_b.nominatorAsNumber()) {
+ if (storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a) <= storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b)) {
return 1;
} else {
return 0;
@@ -569,10 +568,10 @@ storm_rational_function_ptr storm_rational_function_floor(storm_rational_functio
#endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
- if (!storm::utility::isInteger(srf_a)) {
+ if (!storm::utility::isConstant(srf_a)) {
throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be non-constant rational function.";
}
- storm::RationalFunction* result_srf = new storm::RationalFunction(carl::floor(srf_a.nominatorAsNumber()));
+ storm::RationalFunction* result_srf = new storm::RationalFunction(carl::floor(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a)));
return (storm_rational_function_ptr)result_srf;
}
@@ -582,10 +581,10 @@ storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function
#endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
- if (!storm::utility::isInteger(srf_a)) {
+ if (!storm::utility::isConstant(srf_a)) {
throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be non-constant rational function.";
}
- storm::RationalFunction* result_srf = new storm::RationalFunction(carl::ceil(srf_a.nominatorAsNumber()));
+ storm::RationalFunction* result_srf = new storm::RationalFunction(carl::ceil(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a)));
return (storm_rational_function_ptr)result_srf;
}
diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
index 93c2b0320..317361fe8 100644
--- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
+++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
@@ -38,8 +38,8 @@ static void sylvan_storm_rational_function_destroy(uint64_t val) {
storm_rational_function_destroy(x);
}
-static char* sylvan_storm_rational_function_to_str(int comp, uint64_t val, char *buf, size_t buflen) {
- return storm_rational_function_to_str((storm_rational_function_ptr)(size_t)val, *buf, buflen);
+static char* sylvan_storm_rational_function_to_str(int comp, uint64_t val, char* buf, size_t buflen) {
+ return storm_rational_function_to_str((storm_rational_function_ptr)(size_t)val, buf, buflen);
(void)comp;
}
@@ -66,7 +66,7 @@ MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val) {
storm_rational_function_ptr mtbdd_getstorm_rational_function_ptr(MTBDD terminal) {
uint64_t value = mtbdd_getvalue(terminal);
- return (storm_rational_function_ptr*)value;
+ return (storm_rational_function_ptr)value;
}
TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v) {
diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c
index 46470188b..55f14b4d4 100644
--- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c
+++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c
@@ -38,8 +38,8 @@ static void sylvan_storm_rational_number_destroy(uint64_t val) {
storm_rational_number_destroy(x);
}
-static char* sylvan_storm_rational_number_to_str(int comp, uint64_t val, char *buf, size_t buflen) {
- return storm_rational_number_to_str((storm_rational_number_ptr)(size_t)val, *buf, buflen);
+static char* sylvan_storm_rational_number_to_str(int comp, uint64_t val, char* buf, size_t buflen) {
+ return storm_rational_number_to_str((storm_rational_number_ptr)(size_t)val, buf, buflen);
(void)comp;
}
@@ -66,7 +66,7 @@ MTBDD mtbdd_storm_rational_number(storm_rational_number_ptr val) {
storm_rational_number_ptr mtbdd_getstorm_rational_number_ptr(MTBDD terminal) {
uint64_t value = mtbdd_getvalue(terminal);
- return (storm_rational_number_ptr*)value;
+ return (storm_rational_number_ptr)value;
}
TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_number, MTBDD, a, size_t, v) {
diff --git a/src/storm/adapters/CarlAdapter.h b/src/storm/adapters/CarlAdapter.h
index 41a1c0cde..27aa37960 100644
--- a/src/storm/adapters/CarlAdapter.h
+++ b/src/storm/adapters/CarlAdapter.h
@@ -41,11 +41,11 @@ namespace carl {
namespace storm {
typedef carl::Variable RationalFunctionVariable;
-#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_EA
+#if defined(STORM_HAVE_CLN) && defined(STORM_USE_CLN_RF)
typedef cln::cl_RA RationalFunctionCoefficient;
-#elif defined STORM_HAVE_GMP && !defined STORM_USE_CLN_EA
+#elif defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_RF)
typedef mpq_class RationalFunctionCoefficient;
-#elif defined STORM_USE_CLN_EA
+#elif defined(STORM_USE_CLN_RF)
#error CLN is to be used, but is not available.
#else
#error GMP is to be used, but is not available.
diff --git a/src/storm/adapters/NumberAdapter.h b/src/storm/adapters/NumberAdapter.h
index 3258dcb96..6d792e258 100644
--- a/src/storm/adapters/NumberAdapter.h
+++ b/src/storm/adapters/NumberAdapter.h
@@ -2,21 +2,21 @@
#include "storm-config.h"
-#if defined STORM_HAVE_CLN
+#if defined(STORM_HAVE_CLN)
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Wmismatched-tags"
#include <cln/cln.h>
#pragma clang diagnostic pop
#endif
-#if defined STORM_HAVE_GMP
+#if defined(STORM_HAVE_GMP)
#include <gmp.h>
#include <gmpxx.h>
#endif
#include <carl/numbers/numbers.h>
-#if defined STORM_HAVE_CLN && (defined STORM_USE_CLN_EA || defined STORM_USE_CLN_RF)
+#if defined(STORM_HAVE_CLN) && (defined(STORM_USE_CLN_EA) || defined(STORM_USE_CLN_RF))
namespace cln {
inline size_t hash_value(cl_RA const& n) {
std::hash<cln::cl_RA> h;
@@ -25,7 +25,7 @@ namespace cln {
}
#endif
-#if defined STORM_HAVE_GMP && (!defined STORM_USE_CLN_EA || !defined STORM_USE_CLN_RF)
+#if defined(STORM_HAVE_GMP) && (!defined(STORM_USE_CLN_EA) || !defined(STORM_USE_CLN_RF))
inline size_t hash_value(mpq_class const& q) {
std::hash<mpq_class> h;
return h(q);
@@ -33,11 +33,18 @@ inline size_t hash_value(mpq_class const& q) {
#endif
namespace storm {
-#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_EA
- typedef cln::cl_RA RationalNumber;
-#elif defined STORM_HAVE_GMP && !defined STORM_USE_CLN_EA
- typedef mpq_class RationalNumber;
-#elif defined STORM_USE_CLN_EA
+#if defined(STORM_HAVE_CLN)
+ typedef cln::cl_RA ClnRationalNumber;
+#endif
+#if defined(STORM_HAVE_GMP)
+ typedef mpq_class GmpRationalNumber;
+#endif
+
+#if defined(STORM_HAVE_CLN) && defined(STORM_USE_CLN_EA)
+ typedef ClnRationalNumber RationalNumber;
+#elif defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_EA)
+ typedef GmpRationalNumber RationalNumber;
+#elif defined(STORM_USE_CLN_EA)
#error CLN is to be used, but is not available.
#else
#error GMP is to be used, but is not available.
diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp
index ee6573f27..f8bc384c3 100644
--- a/src/storm/builder/DdPrismModelBuilder.cpp
+++ b/src/storm/builder/DdPrismModelBuilder.cpp
@@ -715,8 +715,6 @@ namespace storm {
commandDd += updateResultsIt->updateDd * probabilityDd;
}
- commandDd.exportToDot("command.dot");
-
return ActionDecisionDiagram(guard, guard.template toAdd<ValueType>() * commandDd, globalVariablesInSomeUpdate);
} else {
return ActionDecisionDiagram(*generationInfo.manager);
@@ -1395,9 +1393,7 @@ namespace storm {
// Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables);
storm::dd::Bdd<Type> deadlockStates = reachableStates && !statesWithTransition;
-
- transitionMatrix.exportToDot("trans.dot");
-
+
// If there are deadlocks, either fix them or raise an error.
if (!deadlockStates.isZero()) {
// If we need to fix deadlocks, we do so now.
diff --git a/src/storm/modelchecker/region/ApproximationModel.cpp b/src/storm/modelchecker/region/ApproximationModel.cpp
index 9646193f6..8666b9d0f 100644
--- a/src/storm/modelchecker/region/ApproximationModel.cpp
+++ b/src/storm/modelchecker/region/ApproximationModel.cpp
@@ -166,7 +166,7 @@ namespace storm {
if(this->maybeStates.get(oldEntry.getColumn())){
STORM_LOG_THROW(eqSysMatrixEntry->getColumn()==newIndices[oldEntry.getColumn()], storm::exceptions::UnexpectedException, "old and new entries do not match");
if(storm::utility::isConstant(oldEntry.getValue())){
- eqSysMatrixEntry->setValue(storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(oldEntry.getValue())));
+ eqSysMatrixEntry->setValue(storm::utility::convertNumber<ConstantType>(storm::utility::region::getConstantPart(oldEntry.getValue())));
} else {
auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(oldEntry.getValue(), this->matrixData.rowSubstitutions[curRow]), dummyNonZeroValue)).first;
this->matrixData.assignment.emplace_back(eqSysMatrixEntry, functionsIt->second);
@@ -181,7 +181,7 @@ namespace storm {
}
if(!this->computeRewards){
if(storm::utility::isConstant(storm::utility::simplify(targetProbability))){
- *vectorIt = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(targetProbability));
+ *vectorIt = storm::utility::convertNumber<ConstantType>(storm::utility::region::getConstantPart(targetProbability));
} else {
auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(targetProbability, this->matrixData.rowSubstitutions[curRow]), dummyNonZeroValue)).first;
this->vectorData.assignment.emplace_back(vectorIt, functionsIt->second);
@@ -212,7 +212,7 @@ namespace storm {
auto vectorIt = this->vectorData.vector.begin();
for(auto oldState : this->maybeStates){
if(storm::utility::isConstant(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState])){
- ConstantType reward = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState]));
+ ConstantType reward = storm::utility::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState]));
//Add one of these entries for every row in the row group of oldState
for(auto matrixRow=this->matrixData.matrix.getRowGroupIndices()[oldState]; matrixRow<this->matrixData.matrix.getRowGroupIndices()[oldState+1]; ++matrixRow){
*vectorIt = reward;
@@ -334,7 +334,7 @@ namespace storm {
instantiatedSubs[funcSub.second][vertexSub.first]=vertexSub.second;
}
//evaluate the function
- ConstantType currValue = storm::utility::region::convertNumber<ConstantType>(
+ ConstantType currValue = storm::utility::convertNumber<ConstantType>(
storm::utility::region::evaluateFunction(
funcSub.first,
instantiatedSubs[funcSub.second]
diff --git a/src/storm/modelchecker/region/ParameterRegion.cpp b/src/storm/modelchecker/region/ParameterRegion.cpp
index d328831fc..ecd0dee28 100644
--- a/src/storm/modelchecker/region/ParameterRegion.cpp
+++ b/src/storm/modelchecker/region/ParameterRegion.cpp
@@ -206,11 +206,11 @@ namespace storm {
std::string ParameterRegion<ParametricType>::toString() const {
std::stringstream regionstringstream;
for (auto var : this->getVariables()) {
- regionstringstream << storm::utility::region::convertNumber<double>(this->getLowerBoundary(var));
+ regionstringstream << storm::utility::convertNumber<double>(this->getLowerBoundary(var));
regionstringstream << "<=";
regionstringstream << storm::utility::region::getVariableName(var);
regionstringstream << "<=";
- regionstringstream << storm::utility::region::convertNumber<double>(this->getUpperBoundary(var));
+ regionstringstream << storm::utility::convertNumber<double>(this->getUpperBoundary(var));
regionstringstream << ",";
}
std::string regionstring = regionstringstream.str();
@@ -238,8 +238,8 @@ namespace storm {
STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter");
VariableType var = storm::utility::region::getVariableFromString<VariableType>(parameter);
- CoefficientType lb = storm::utility::region::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
- CoefficientType ub = storm::utility::region::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
+ CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
+ CoefficientType ub = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
lowerBoundaries.emplace(std::make_pair(var, lb));
upperBoundaries.emplace(std::make_pair(var, ub));
}
diff --git a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp
index b516515d0..2ed74794e 100644
--- a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp
+++ b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp
@@ -296,7 +296,7 @@ namespace storm {
}
if(isResultConstant){
STORM_LOG_WARN("For the given property, the reachability Value is constant, i.e., independent of the region");
- constantResult = storm::utility::region::convertNumber<ConstantType>(-1.0);
+ constantResult = storm::utility::convertNumber<ConstantType>(-1.0);
}
}
@@ -392,7 +392,7 @@ namespace storm {
}
if(isResultConstant){
STORM_LOG_WARN("For the given property, the reachability Value is constant, i.e., independent of the region");
- constantResult = storm::utility::region::convertNumber<ConstantType>(-1.0);
+ constantResult = storm::utility::convertNumber<ConstantType>(-1.0);
}
}
@@ -597,7 +597,7 @@ namespace storm {
storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions..
this->smtSolver = std::shared_ptr<storm::solver::SmtlibSmtSolver>(new storm::solver::SmtlibSmtSolver(manager, true));
- ParametricType bound= storm::utility::region::convertNumber<ParametricType>(this->getSpecifiedFormulaBound());
+ ParametricType bound= storm::utility::convertNumber<ParametricType>(this->getSpecifiedFormulaBound());
// To prove that the property is satisfied in the initial state for all parameters,
// we ask the solver whether the negation of the property is satisfiable and invert the answer.
diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp
index 31d4d5f79..57cf09fb5 100644
--- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp
+++ b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp
@@ -248,7 +248,7 @@ namespace storm {
}
if(isResultConstant){
STORM_LOG_WARN("For the given property, the reachability Value is constant, i.e., independent of the region");
- constantResult = storm::utility::region::convertNumber<ConstantType>(-1.0); //-1 denotes that the result is constant but not yet computed
+ constantResult = storm::utility::convertNumber<ConstantType>(-1.0); //-1 denotes that the result is constant but not yet computed
}
}
diff --git a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp
index e98ba6485..e056899bc 100644
--- a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp
+++ b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp
@@ -79,7 +79,7 @@ namespace storm {
template<typename ParametricSparseModelType, typename ConstantType>
ConstantType SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormulaBound() const {
- return storm::utility::region::convertNumber<ConstantType>(this->getSpecifiedFormula()->getThreshold());
+ return storm::utility::convertNumber<ConstantType>(this->getSpecifiedFormula()->getThreshold());
}
template<typename ParametricSparseModelType, typename ConstantType>
@@ -177,7 +177,7 @@ namespace storm {
(!settings.doSample() && settings.getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){
initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula());
}
- } else if (this->isResultConstant() && this->constantResult.get() == storm::utility::region::convertNumber<ConstantType>(-1.0)){
+ } else if (this->isResultConstant() && this->constantResult.get() == storm::utility::convertNumber<ConstantType>(-1.0)){
//In this case, the result is constant but has not been computed yet. so do it now!
STORM_LOG_DEBUG("The Result is constant and will be computed now.");
initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula());
@@ -241,7 +241,7 @@ namespace storm {
CoefficientType fractionOfUndiscoveredArea = storm::utility::one<CoefficientType>();
CoefficientType fractionOfAllSatArea = storm::utility::zero<CoefficientType>();
CoefficientType fractionOfAllViolatedArea = storm::utility::zero<CoefficientType>();
- while(fractionOfUndiscoveredArea > storm::utility::region::convertNumber<CoefficientType>(refinementThreshold)){
+ while(fractionOfUndiscoveredArea > storm::utility::convertNumber<CoefficientType>(refinementThreshold)){
STORM_LOG_THROW(indexOfCurrentRegion < regions.size(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left.");
ParameterRegion<ParametricType>& currentRegion = regions[indexOfCurrentRegion];
this->checkRegion(currentRegion);
@@ -263,7 +263,7 @@ namespace storm {
++indexOfCurrentRegion;
}
std::cout << " done! " << std::endl << "Fraction of ALLSAT;ALLVIOLATED;UNDISCOVERED area:" << std::endl;
- std::cout << "REFINEMENTRESULT;" <<storm::utility::region::convertNumber<double>(fractionOfAllSatArea) << ";" << storm::utility::region::convertNumber<double>(fractionOfAllViolatedArea) << ";" << storm::utility::region::convertNumber<double>(fractionOfUndiscoveredArea) << std::endl;
+ std::cout << "REFINEMENTRESULT;" <<storm::utility::convertNumber<double>(fractionOfAllSatArea) << ";" << storm::utility::convertNumber<double>(fractionOfAllViolatedArea) << ";" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) << std::endl;
}
@@ -487,7 +487,7 @@ namespace storm {
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::valueIsInBoundOfFormula(CoefficientType const& value){
- return valueIsInBoundOfFormula(storm::utility::region::convertNumber<ConstantType>(value));
+ return valueIsInBoundOfFormula(storm::utility::convertNumber<ConstantType>(value));
}
template<typename ParametricSparseModelType, typename ConstantType>
diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index 42b762b64..104e90e64 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -1605,16 +1605,29 @@ namespace storm {
template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<storm::storage::sparse::state_type> const& matrix) const;
#ifdef STORM_HAVE_CARL
- // Rat Number
- template class MatrixEntry<typename SparseMatrix<RationalNumber>::index_type, RationalNumber>;
- template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalNumber> const& entry);
- template class SparseMatrixBuilder<RationalNumber>;
- template class SparseMatrix<RationalNumber>;
- template std::ostream& operator<<(std::ostream& out, SparseMatrix<RationalNumber> const& matrix);
- template std::vector<storm::RationalNumber> SparseMatrix<RationalNumber>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalNumber> const& otherMatrix) const;
- template bool SparseMatrix<storm::RationalNumber>::isSubmatrixOf(SparseMatrix<storm::RationalNumber> const& matrix) const;
-
- // Rat Function
+ // Rational Numbers
+
+#if defined(STORM_HAVE_CLN)
+ template class MatrixEntry<typename SparseMatrix<ClnRationalNumber>::index_type, ClnRationalNumber>;
+ template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, ClnRationalNumber> const& entry);
+ template class SparseMatrixBuilder<ClnRationalNumber>;
+ template class SparseMatrix<ClnRationalNumber>;
+ template std::ostream& operator<<(std::ostream& out, SparseMatrix<ClnRationalNumber> const& matrix);
+ template std::vector<storm::ClnRationalNumber> SparseMatrix<ClnRationalNumber>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::ClnRationalNumber> const& otherMatrix) const;
+ template bool SparseMatrix<storm::ClnRationalNumber>::isSubmatrixOf(SparseMatrix<storm::ClnRationalNumber> const& matrix) const;
+#endif
+
+#if defined(STORM_HAVE_GMP)
+ template class MatrixEntry<typename SparseMatrix<GmpRationalNumber>::index_type, GmpRationalNumber>;
+ template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, GmpRationalNumber> const& entry);
+ template class SparseMatrixBuilder<GmpRationalNumber>;
+ template class SparseMatrix<GmpRationalNumber>;
+ template std::ostream& operator<<(std::ostream& out, SparseMatrix<GmpRationalNumber> const& matrix);
+ template std::vector<storm::GmpRationalNumber> SparseMatrix<GmpRationalNumber>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::GmpRationalNumber> const& otherMatrix) const;
+ template bool SparseMatrix<storm::GmpRationalNumber>::isSubmatrixOf(SparseMatrix<storm::GmpRationalNumber> const& matrix) const;
+#endif
+
+ // Rational Function
template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalFunction> const& entry);
template class SparseMatrixBuilder<RationalFunction>;
@@ -1625,7 +1638,7 @@ namespace storm {
template std::vector<storm::RationalFunction> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
template std::vector<storm::RationalFunction> SparseMatrix<int>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
template bool SparseMatrix<storm::RationalFunction>::isSubmatrixOf(SparseMatrix<storm::RationalFunction> const& matrix) const;
-
+
// Intervals
template std::vector<storm::Interval> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
template class MatrixEntry<typename SparseMatrix<Interval>::index_type, Interval>;
diff --git a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp
index 394e0fe08..a9367fa7c 100644
--- a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp
+++ b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp
@@ -11,7 +11,6 @@
#include <cmath>
#include "storm/adapters/CarlAdapter.h"
-#include "storm-config.h"
namespace storm {
namespace dd {
diff --git a/src/storm/utility/ConstantsComparator.cpp b/src/storm/utility/ConstantsComparator.cpp
index d212d8874..bbac60a50 100644
--- a/src/storm/utility/ConstantsComparator.cpp
+++ b/src/storm/utility/ConstantsComparator.cpp
@@ -111,10 +111,17 @@ namespace storm {
template class ConstantsComparator<storm::storage::sparse::state_type>;
#ifdef STORM_HAVE_CARL
+#if defined(STORM_HAVE_CLN)
+ template class ConstantsComparator<ClnRationalNumber>;
+#endif
+
+#if defined(STORM_HAVE_GMP)
+ template class ConstantsComparator<GmpRationalNumber>;
+#endif
+
template class ConstantsComparator<RationalFunction>;
template class ConstantsComparator<Polynomial>;
template class ConstantsComparator<Interval>;
- template class ConstantsComparator<RationalNumber>;
#endif
}
}
diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index 1e88b8dfc..3f3831293 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -1,5 +1,7 @@
#include "storm/utility/constants.h"
+#include <type_traits>
+
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/settings/SettingsManager.h"
@@ -42,6 +44,11 @@ namespace storm {
bool isConstant(ValueType const&) {
return true;
}
+
+ template<typename ValueType>
+ bool isInfinity(ValueType const& a) {
+ return a == infinity<ValueType>();
+ }
template<typename ValueType>
bool isInteger(ValueType const& number) {
@@ -49,132 +56,22 @@ namespace storm {
ValueType result = std::modf(number, &iPart);
return result == zero<ValueType>();
}
-
- template<typename ValueType>
- bool isInfinity(ValueType const& a) {
- return a == infinity<ValueType>();
- }
-
+
template<>
bool isInteger(int const&) {
return true;
}
-
- template<>
- bool isInteger(uint_fast64_t const&) {
- return true;
- }
-
- template<typename ValueType>
- std::string to_string(ValueType const& value) {
- std::stringstream ss;
- ss << value;
- return ss.str();
- }
-
- template<>
- std::string to_string(RationalFunction const& f) {
- std::stringstream ss;
- if (f.isConstant()) {
- if (f.denominator().isOne()) {
- ss << f.nominatorAsNumber();
- } else {
- ss << f.nominatorAsNumber() << "/" << f.denominatorAsNumber();
- }
- } else if (f.denominator().isOne()) {
- ss << f.nominatorAsPolynomial().coefficient() * f.nominatorAsPolynomial().polynomial();
- } else {
- ss << "(" << f.nominatorAsPolynomial() << ")/(" << f.denominatorAsPolynomial() << ")";
- }
- return ss.str();
- }
-
-#ifdef STORM_HAVE_CARL
- template<>
- bool isOne(storm::RationalNumber const& a) {
- return carl::isOne(a);
- }
-
- template<>
- bool isZero(storm::RationalNumber const& a) {
- return carl::isZero(a);
- }
- template<>
- bool isOne(storm::RationalFunction const& a) {
- return a.isOne();
- }
-
- template<>
- bool isZero(storm::RationalFunction const& a) {
- return a.isZero();
- }
-
- template<>
- bool isConstant(storm::RationalFunction const& a) {
- return a.isConstant();
- }
-
- template<>
- bool isOne(storm::Polynomial const& a) {
- return a.isOne();
- }
-
- template<>
- bool isZero(storm::Polynomial const& a) {
- return a.isZero();
- }
-
- template<>
- bool isConstant(storm::Polynomial const& a) {
- return a.isConstant();
- }
-
- template<>
- storm::RationalFunction infinity() {
- // FIXME: this should be treated more properly.
- return storm::RationalFunction(-1.0);
- }
-
- template<>
- bool isInfinity(storm::RationalFunction const& a) {
- // FIXME: this should be treated more properly.
- return a == infinity<storm::RationalFunction>();
- }
-
- template<>
- storm::RationalNumber infinity() {
- // FIXME: this should be treated more properly.
- return storm::RationalNumber(-1);
- }
template<>
- bool isInteger(storm::RationalNumber const& number) {
- return carl::isInteger(number);
+ bool isInteger(uint32_t const&) {
+ return true;
}
template<>
- bool isInteger(storm::RationalFunction const& func) {
- return storm::utility::isConstant(func) && storm::utility::isOne(func.denominator());
- }
-#endif
-
- template<typename ValueType>
- ValueType pow(ValueType const& value, uint_fast64_t exponent) {
- return std::pow(value, exponent);
+ bool isInteger(storm::storage::sparse::state_type const&) {
+ return true;
}
- template<typename ValueType>
- ValueType simplify(ValueType value) {
- // In the general case, we don't do anything here, but merely return the value. If something else is
- // supposed to happen here, the templated function can be specialized for this particular type.
- return value;
- }
-
- template<>
- double convertNumber(double const& number){
- return number;
- }
-
template<>
uint_fast64_t convertNumber(double const& number){
return std::llround(number);
@@ -185,29 +82,34 @@ namespace storm {
return number;
}
- template<typename ValueType>
- ValueType sqrt(ValueType const& number) {
- return std::sqrt(number);
+ template<>
+ double convertNumber(double const& number){
+ return number;
}
template<typename ValueType>
- ValueType abs(ValueType const& number) {
- return std::fabs(number);
+ ValueType simplify(ValueType value) {
+ // In the general case, we don't do anything here, but merely return the value. If something else is
+ // supposed to happen here, the templated function can be specialized for this particular type.
+ return value;
}
-
- template<typename ValueType>
- ValueType floor(ValueType const& number) {
- return std::floor(number);
+
+ template<typename IndexType, typename ValueType>
+ storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> matrixEntry) {
+ simplify(matrixEntry.getValue());
+ return matrixEntry;
}
- template<typename ValueType>
- ValueType ceil(ValueType const& number) {
- return std::ceil(number);
+ template<typename IndexType, typename ValueType>
+ storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
+ simplify(matrixEntry.getValue());
+ return matrixEntry;
}
- template<>
- std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::vector<storm::RationalFunction> const&) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum/maximum for rational functions is not defined.");
+ template<typename IndexType, typename ValueType>
+ storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
+ simplify(matrixEntry.getValue());
+ return std::move(matrixEntry);
}
template<typename ValueType>
@@ -226,51 +128,17 @@ namespace storm {
return std::make_pair(min, max);
}
- template<>
- std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::vector<storm::RationalNumber> const& values) {
- assert(!values.empty());
- storm::RationalNumber min = values.front();
- storm::RationalNumber max = values.front();
- for (auto const& vt : values) {
- if (vt == storm::utility::infinity<storm::RationalNumber>()) {
- max = vt;
- } else {
- if (vt < min) {
- min = vt;
- }
- if (vt > max) {
- max = vt;
- }
- }
- }
- return std::make_pair(min, max);
- }
-
- template<>
- storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined.");
- }
-
template<typename ValueType>
ValueType minimum(std::vector<ValueType> const& values) {
return minmax(values).first;
}
- template<>
- storm::RationalFunction maximum(std::vector<storm::RationalFunction> const&) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined.");
- }
template<typename ValueType>
ValueType maximum(std::vector<ValueType> const& values) {
return minmax(values).second;
}
-
- template<>
- std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::map<uint64_t, storm::RationalFunction> const&) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum/maximum for rational functions is not defined.");
- }
-
+
template<typename K, typename ValueType>
std::pair<ValueType, ValueType> minmax(std::map<K, ValueType> const& values) {
assert(!values.empty());
@@ -286,130 +154,374 @@ namespace storm {
}
return std::make_pair(min, max);
}
-
- template<>
- std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::map<uint64_t, storm::RationalNumber> const& values) {
- assert(!values.empty());
- storm::RationalNumber min = values.begin()->second;
- storm::RationalNumber max = values.begin()->second;
- for (auto const& vt : values) {
- if (vt.second == storm::utility::infinity<storm::RationalNumber>()) {
- max = vt.second;
- } else {
- if (vt.second < min) {
- min = vt.second;
- }
- if (vt.second > max) {
- max = vt.second;
- }
- }
- }
- return std::make_pair(min, max);
- }
-
- template<>
- storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined.");
- }
template< typename K, typename ValueType>
ValueType minimum(std::map<K, ValueType> const& values) {
return minmax(values).first;
}
- template<>
- storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const&) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined");
- }
-
template<typename K, typename ValueType>
ValueType maximum(std::map<K, ValueType> const& values) {
return minmax(values).second;
}
-#ifdef STORM_HAVE_CARL
- template<>
- RationalFunction& simplify(RationalFunction& value);
+ template<typename ValueType>
+ ValueType pow(ValueType const& value, uint_fast64_t exponent) {
+ return std::pow(value, exponent);
+ }
- template<>
- RationalFunction&& simplify(RationalFunction&& value);
+ template<typename ValueType>
+ ValueType sqrt(ValueType const& number) {
+ return std::sqrt(number);
+ }
+
+ template<typename ValueType>
+ ValueType abs(ValueType const& number) {
+ return std::fabs(number);
+ }
+
+ template<typename ValueType>
+ ValueType floor(ValueType const& number) {
+ return std::floor(number);
+ }
+
+ template<typename ValueType>
+ ValueType ceil(ValueType const& number) {
+ return std::ceil(number);
+ }
+ template<typename ValueType>
+ std::string to_string(ValueType const& value) {
+ std::stringstream ss;
+ ss << value;
+ return ss.str();
+ }
+
+#if defined(STORM_HAVE_CARL) && defined(STORM_HAVE_CLN)
template<>
- RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
- return carl::pow(value, exponent);
+ storm::ClnRationalNumber infinity() {
+ // FIXME: this should be treated more properly.
+ return storm::ClnRationalNumber(-1);
}
template<>
- RationalFunction simplify(RationalFunction value) {
- value.simplify();
- return value;
+ bool isOne(storm::ClnRationalNumber const& a) {
+ return carl::isOne(a);
}
template<>
- RationalFunction& simplify(RationalFunction& value) {
- value.simplify();
- return value;
+ bool isZero(storm::ClnRationalNumber const& a) {
+ return carl::isZero(a);
}
-
+
template<>
- RationalFunction&& simplify(RationalFunction&& value) {
- value.simplify();
- return std::move(value);
+ bool isInteger(storm::ClnRationalNumber const& number) {
+ return carl::isInteger(number);
+ }
+
+ template<>
+ std::pair<storm::ClnRationalNumber, storm::ClnRationalNumber> minmax(std::vector<storm::ClnRationalNumber> const& values) {
+ assert(!values.empty());
+ storm::ClnRationalNumber min = values.front();
+ storm::ClnRationalNumber max = values.front();
+ for (auto const& vt : values) {
+ if (vt == storm::utility::infinity<storm::ClnRationalNumber>()) {
+ max = vt;
+ } else {
+ if (vt < min) {
+ min = vt;
+ }
+ if (vt > max) {
+ max = vt;
+ }
+ }
+ }
+ return std::make_pair(min, max);
+ }
+
+ template<>
+ uint_fast64_t convertNumber(ClnRationalNumber const& number){
+ return carl::toInt<unsigned long>(number);
}
template<>
- double convertNumber(RationalNumber const& number){
+ ClnRationalNumber convertNumber(ClnRationalNumber const& number){
+ return number;
+ }
+
+ template<>
+ ClnRationalNumber convertNumber(double const& number){
+ return carl::rationalize<ClnRationalNumber>(number);
+ }
+
+ template<>
+ ClnRationalNumber convertNumber(int const& number){
+ return carl::rationalize<ClnRationalNumber>(number);
+ }
+
+ template<>
+ ClnRationalNumber convertNumber(uint_fast64_t const& number){
+ STORM_LOG_ASSERT(static_cast<carl::uint>(number) == number, "Rationalizing failed, because the number is too large.");
+ return carl::rationalize<ClnRationalNumber>(static_cast<carl::uint>(number));
+ }
+
+ template<>
+ ClnRationalNumber convertNumber(int_fast64_t const& number){
+ STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large.");
+ return carl::rationalize<ClnRationalNumber>(static_cast<carl::sint>(number));
+ }
+
+ template<>
+ double convertNumber(ClnRationalNumber const& number){
return carl::toDouble(number);
}
+
+ template<>
+ ClnRationalNumber convertNumber(std::string const& number) {
+ return carl::parse<ClnRationalNumber>(number);
+ }
template<>
- uint_fast64_t convertNumber(RationalNumber const& number){
+ ClnRationalNumber sqrt(ClnRationalNumber const& number) {
+ return carl::sqrt(number);
+ }
+
+ template<>
+ ClnRationalNumber abs(storm::ClnRationalNumber const& number) {
+ return carl::abs(number);
+ }
+
+ template<>
+ ClnRationalNumber floor(storm::ClnRationalNumber const& number) {
+ return carl::floor(number);
+ }
+
+ template<>
+ ClnRationalNumber ceil(storm::ClnRationalNumber const& number) {
+ return carl::ceil(number);
+ }
+
+ template<>
+ ClnRationalNumber pow(ClnRationalNumber const& value, uint_fast64_t exponent) {
+ return carl::pow(value, exponent);
+ }
+#endif
+
+#if defined(STORM_HAVE_CARL) && defined(STORM_HAVE_GMP)
+ template<>
+ storm::GmpRationalNumber infinity() {
+ // FIXME: this should be treated more properly.
+ return storm::GmpRationalNumber(-1);
+ }
+
+ template<>
+ bool isOne(storm::GmpRationalNumber const& a) {
+ return carl::isOne(a);
+ }
+
+ template<>
+ bool isZero(storm::GmpRationalNumber const& a) {
+ return carl::isZero(a);
+ }
+
+ template<>
+ bool isInteger(storm::GmpRationalNumber const& number) {
+ return carl::isInteger(number);
+ }
+
+ template<>
+ std::pair<storm::GmpRationalNumber, storm::GmpRationalNumber> minmax(std::vector<storm::GmpRationalNumber> const& values) {
+ assert(!values.empty());
+ storm::GmpRationalNumber min = values.front();
+ storm::GmpRationalNumber max = values.front();
+ for (auto const& vt : values) {
+ if (vt == storm::utility::infinity<storm::GmpRationalNumber>()) {
+ max = vt;
+ } else {
+ if (vt < min) {
+ min = vt;
+ }
+ if (vt > max) {
+ max = vt;
+ }
+ }
+ }
+ return std::make_pair(min, max);
+ }
+
+ template<>
+ std::pair<storm::GmpRationalNumber, storm::GmpRationalNumber> minmax(std::map<uint64_t, storm::GmpRationalNumber> const& values) {
+ assert(!values.empty());
+ storm::GmpRationalNumber min = values.begin()->second;
+ storm::GmpRationalNumber max = values.begin()->second;
+ for (auto const& vt : values) {
+ if (vt.second == storm::utility::infinity<storm::GmpRationalNumber>()) {
+ max = vt.second;
+ } else {
+ if (vt.second < min) {
+ min = vt.second;
+ }
+ if (vt.second > max) {
+ max = vt.second;
+ }
+ }
+ }
+ return std::make_pair(min, max);
+ }
+
+ template<>
+ uint_fast64_t convertNumber(GmpRationalNumber const& number){
return carl::toInt<unsigned long>(number);
}
-
+
template<>
- RationalNumber convertNumber(RationalNumber const& number){
+ GmpRationalNumber convertNumber(GmpRationalNumber const& number){
return number;
}
template<>
- RationalNumber convertNumber(double const& number){
- return carl::rationalize<RationalNumber>(number);
+ GmpRationalNumber convertNumber(double const& number){
+ return carl::rationalize<GmpRationalNumber>(number);
}
template<>
- RationalNumber convertNumber(uint_fast64_t const& number){
- STORM_LOG_ASSERT(static_cast<carl::uint>(number) == number, "Rationalizing failed, because the number is too large.");
- return carl::rationalize<RationalNumber>(static_cast<carl::uint>(number));
+ GmpRationalNumber convertNumber(int const& number){
+ return carl::rationalize<GmpRationalNumber>(number);
}
template<>
- RationalNumber convertNumber(int_fast64_t const& number){
+ GmpRationalNumber convertNumber(uint_fast64_t const& number){
+ STORM_LOG_ASSERT(static_cast<carl::uint>(number) == number, "Rationalizing failed, because the number is too large.");
+ return carl::rationalize<GmpRationalNumber>(static_cast<carl::uint>(number));
+ }
+
+ template<>
+ GmpRationalNumber convertNumber(int_fast64_t const& number){
STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large.");
- return carl::rationalize<RationalNumber>(static_cast<carl::sint>(number));
+ return carl::rationalize<GmpRationalNumber>(static_cast<carl::sint>(number));
+ }
+
+ template<>
+ double convertNumber(GmpRationalNumber const& number){
+ return carl::toDouble(number);
+ }
+
+ template<>
+ GmpRationalNumber convertNumber(std::string const& number) {
+ return carl::parse<GmpRationalNumber>(number);
+ }
+
+ template<>
+ GmpRationalNumber sqrt(GmpRationalNumber const& number) {
+ return carl::sqrt(number);
+ }
+
+ template<>
+ GmpRationalNumber abs(storm::GmpRationalNumber const& number) {
+ return carl::abs(number);
+ }
+
+ template<>
+ GmpRationalNumber floor(storm::GmpRationalNumber const& number) {
+ return carl::floor(number);
+ }
+
+ template<>
+ GmpRationalNumber ceil(storm::GmpRationalNumber const& number) {
+ return carl::ceil(number);
+ }
+
+ template<>
+ GmpRationalNumber pow(GmpRationalNumber const& value, uint_fast64_t exponent) {
+ return carl::pow(value, exponent);
+ }
+#endif
+
+#if defined(STORM_HAVE_CARL) && defined(STORM_HAVE_GMP) && defined(STORM_HAVE_CLN)
+ template<>
+ storm::GmpRationalNumber convertNumber(storm::ClnRationalNumber const& number) {
+ return carl::parse<storm::GmpRationalNumber>(to_string(number));
+ }
+
+ template<>
+ storm::ClnRationalNumber convertNumber(storm::GmpRationalNumber const& number) {
+ return carl::parse<storm::ClnRationalNumber>(to_string(number));
+ }
+#endif
+
+#ifdef STORM_HAVE_CARL
+ template<>
+ storm::RationalFunction infinity() {
+ // FIXME: this should be treated more properly.
+ return storm::RationalFunction(-1.0);
+ }
+
+ template<>
+ bool isOne(storm::RationalFunction const& a) {
+ return a.isOne();
}
template<>
- RationalFunction convertNumber(double const& number){
- return RationalFunction(carl::rationalize<RationalNumber>(number));
+ bool isOne(storm::Polynomial const& a) {
+ return a.isOne();
}
template<>
- RationalFunction convertNumber(int_fast64_t const& number){
- STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large.");
- return RationalFunction(carl::rationalize<RationalNumber>(static_cast<carl::sint>(number)));
+ bool isZero(storm::RationalFunction const& a) {
+ return a.isZero();
}
template<>
- RationalNumber convertNumber(std::string const& number) {
- return carl::parse<RationalNumber>(number);
+ bool isZero(storm::Polynomial const& a) {
+ return a.isZero();
}
template<>
- RationalFunction convertNumber(RationalNumber const& number) {
- return RationalFunction(number);
+ bool isConstant(storm::RationalFunction const& a) {
+ return a.isConstant();
}
+ template<>
+ bool isConstant(storm::Polynomial const& a) {
+ return a.isConstant();
+ }
+
+ template<>
+ bool isInfinity(storm::RationalFunction const& a) {
+ // FIXME: this should be treated more properly.
+ return a == infinity<storm::RationalFunction>();
+ }
+
+ template<>
+ bool isInteger(storm::RationalFunction const& func) {
+ return storm::utility::isConstant(func) && storm::utility::isOne(func.denominator());
+ }
+
+ template<>
+ RationalFunction convertNumber(double const& number){
+ return RationalFunction(carl::rationalize<RationalFunctionCoefficient>(number));
+ }
+
+ template<>
+ RationalFunction convertNumber(int_fast64_t const& number){
+ STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large.");
+ return RationalFunction(carl::rationalize<RationalFunctionCoefficient>(static_cast<carl::sint>(number)));
+ }
+
+#if defined(STORM_HAVE_CLN)
+ template<>
+ RationalFunction convertNumber(ClnRationalNumber const& number) {
+ return RationalFunction(convertNumber<storm::RationalFunctionCoefficient>(number));
+ }
+#endif
+
+#if defined(STORM_HAVE_GMP)
+ template<>
+ RationalFunction convertNumber(GmpRationalNumber const& number) {
+ return RationalFunction(convertNumber<storm::RationalFunctionCoefficient>(number));
+ }
+#endif
+
template<>
uint_fast64_t convertNumber(RationalFunction const& func) {
return carl::toInt<unsigned long>(func.nominatorAsNumber());
@@ -417,7 +529,7 @@ namespace storm {
template<>
double convertNumber(RationalFunction const& func) {
- return carl::toDouble(func.nominatorAsNumber());
+ return carl::toDouble(func.nominatorAsNumber()) / carl::toDouble(func.denominatorAsNumber());
}
template<>
@@ -426,217 +538,282 @@ namespace storm {
}
template<>
- RationalNumber sqrt(RationalNumber const& number) {
- return carl::sqrt(number);
+ RationalFunctionCoefficient convertNumber(RationalFunction const& number){
+ return number.nominatorAsNumber() / number.denominatorAsNumber();
}
-
+
template<>
- RationalNumber abs(storm::RationalNumber const& number) {
- return carl::abs(number);
+ RationalFunction& simplify(RationalFunction& value);
+
+ template<>
+ RationalFunction&& simplify(RationalFunction&& value);
+
+ template<>
+ RationalFunction simplify(RationalFunction value) {
+ value.simplify();
+ return value;
}
-
+
template<>
- RationalNumber floor(storm::RationalNumber const& number) {
- return carl::floor(number);
+ RationalFunction& simplify(RationalFunction& value) {
+ value.simplify();
+ return value;
}
-
+
template<>
- RationalNumber ceil(storm::RationalNumber const& number) {
- return carl::ceil(number);
+ RationalFunction&& simplify(RationalFunction&& value) {
+ value.simplify();
+ return std::move(value);
}
-
+
template<>
- RationalNumber pow(RationalNumber const& value, uint_fast64_t exponent) {
- return carl::pow(value, exponent);
+ std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::vector<storm::RationalFunction> const&) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum/maximum for rational functions is not defined.");
}
-#endif
-
- template<typename IndexType, typename ValueType>
- storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> matrixEntry) {
- simplify(matrixEntry.getValue());
- return matrixEntry;
+ template<>
+ storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined.");
+ }
+
+ template<>
+ storm::RationalFunction maximum(std::vector<storm::RationalFunction> const&) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined.");
+ }
+
+ template<>
+ std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::map<uint64_t, storm::RationalFunction> const&) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum/maximum for rational functions is not defined.");
+ }
+
+ template<>
+ storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined.");
+ }
+
+ template<>
+ storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const&) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined");
}
- template<typename IndexType, typename ValueType>
- storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
- simplify(matrixEntry.getValue());
- return matrixEntry;
+ template<>
+ RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
+ return carl::pow(value, exponent);
}
- template<typename IndexType, typename ValueType>
- storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
- simplify(matrixEntry.getValue());
- return std::move(matrixEntry);
+ template<>
+ std::string to_string(RationalFunction const& f) {
+ std::stringstream ss;
+ if (f.isConstant()) {
+ if (f.denominator().isOne()) {
+ ss << f.nominatorAsNumber();
+ } else {
+ ss << f.nominatorAsNumber() << "/" << f.denominatorAsNumber();
+ }
+ } else if (f.denominator().isOne()) {
+ ss << f.nominatorAsPolynomial().coefficient() * f.nominatorAsPolynomial().polynomial();
+ } else {
+ ss << "(" << f.nominatorAsPolynomial() << ")/(" << f.denominatorAsPolynomial() << ")";
+ }
+ return ss.str();
}
+
+#endif
+
// Explicit instantiations.
+
+ // double
+ template double one();
+ template double zero();
+ template double infinity();
template bool isOne(double const& value);
template bool isZero(double const& value);
template bool isConstant(double const& value);
template bool isInfinity(double const& value);
-
- template double one();
- template double zero();
- template double infinity();
-
- template double pow(double const& value, uint_fast64_t exponent);
-
+ template bool isInteger(double const& number);
template double simplify(double value);
-
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
-
+ template std::pair<double, double> minmax(std::vector<double> const&);
+ template double minimum(std::vector<double> const&);
+ template double maximum(std::vector<double> const&);
+ template std::pair<double, double> minmax(std::map<uint64_t, double> const&);
+ template double minimum(std::map<uint64_t, double> const&);
+ template double maximum(std::map<uint64_t, double> const&);
+ template double pow(double const& value, uint_fast64_t exponent);
template double sqrt(double const& number);
template double abs(double const& number);
+ template double floor(double const& number);
+ template double ceil(double const& number);
+ template std::string to_string(double const& value);
- template bool isInteger(double const& number);
-
+ // float
+ template float one();
+ template float zero();
+ template float infinity();
template bool isOne(float const& value);
template bool isZero(float const& value);
template bool isConstant(float const& value);
template bool isInfinity(float const& value);
-
- template float one();
- template float zero();
- template float infinity();
-
- template float pow(float const& value, uint_fast64_t exponent);
template bool isInteger(float const& number);
-
template float simplify(float value);
-
- template std::string to_string(float const& value);
- template std::string to_string(double const& value);
- template std::string to_string(storm::RationalNumber const& value);
- template std::string to_string(storm::RationalFunction const& value);
-
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
-
- template bool isOne(int const& value);
- template bool isZero(int const& value);
- template bool isConstant(int const& value);
- template bool isInfinity(int const& value);
+ template std::pair<float, float> minmax(std::vector<float> const&);
+ template float minimum(std::vector<float> const&);
+ template float maximum(std::vector<float> const&);
+ template std::pair<float, float> minmax(std::map<uint64_t, float> const&);
+ template float minimum(std::map<uint64_t, float> const&);
+ template float maximum(std::map<uint64_t, float> const&);
+ template float pow(float const& value, uint_fast64_t exponent);
+ template float sqrt(float const& number);
+ template float abs(float const& number);
+ template float floor(float const& number);
+ template float ceil(float const& number);
+ template std::string to_string(float const& value);
+ // int
template int one();
template int zero();
template int infinity();
-
- template int pow(int const& value, uint_fast64_t exponent);
-
+ template bool isOne(int const& value);
+ template bool isZero(int const& value);
+ template bool isConstant(int const& value);
+ template bool isInfinity(int const& value);
template bool isInteger(int const& number);
-
- template int simplify(int value);
-
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
-
- template bool isOne(storm::storage::sparse::state_type const& value);
- template bool isZero(storm::storage::sparse::state_type const& value);
- template bool isConstant(storm::storage::sparse::state_type const& value);
- template bool isInfinity(storm::storage::sparse::state_type const& value);
-
+
+ // uint32_t
template uint32_t one();
template uint32_t zero();
template uint32_t infinity();
-
+ template bool isOne(uint32_t const& value);
+ template bool isZero(uint32_t const& value);
+ template bool isConstant(uint32_t const& value);
+ template bool isInfinity(uint32_t const& value);
+ template bool isInteger(uint32_t const& number);
+
+ // storm::storage::sparse::state_type
template storm::storage::sparse::state_type one();
template storm::storage::sparse::state_type zero();
template storm::storage::sparse::state_type infinity();
-
- template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent);
-
- template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value);
-
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> matrixEntry);
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry);
-
- template std::pair<double, double> minmax(std::vector<double> const&);
- template double minimum(std::vector<double> const&);
- template double maximum(std::vector<double> const&);
+ template bool isOne(storm::storage::sparse::state_type const& value);
+ template bool isZero(storm::storage::sparse::state_type const& value);
+ template bool isConstant(storm::storage::sparse::state_type const& value);
+ template bool isInfinity(storm::storage::sparse::state_type const& value);
+ template bool isInteger(storm::storage::sparse::state_type const& number);
+
+#if defined(STORM_HAVE_CLN)
+ // Instantiations for (CLN) rational number.
+ template storm::ClnRationalNumber one();
+ template storm::ClnRationalNumber zero();
+ template storm::ClnRationalNumber infinity();
+ template bool isOne(storm::ClnRationalNumber const& value);
+ template bool isZero(storm::ClnRationalNumber const& value);
+ template bool isConstant(storm::ClnRationalNumber const& value);
+ template bool isInfinity(storm::ClnRationalNumber const& value);
+ template bool isInteger(storm::ClnRationalNumber const& number);
+ template double convertNumber(storm::ClnRationalNumber const& number);
+ template uint_fast64_t convertNumber(storm::ClnRationalNumber const& number);
+ template storm::ClnRationalNumber convertNumber(double const& number);
+ template storm::ClnRationalNumber convertNumber(storm::ClnRationalNumber const& number);
+ template ClnRationalNumber convertNumber(std::string const& number);
+ template storm::ClnRationalNumber simplify(storm::ClnRationalNumber value);
+ template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber> matrixEntry);
+ template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber>& matrixEntry);
+ template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber>&& matrixEntry);
+ template std::pair<storm::ClnRationalNumber, storm::ClnRationalNumber> minmax(std::map<uint64_t, storm::ClnRationalNumber> const&);
+ template storm::ClnRationalNumber minimum(std::map<uint64_t, storm::ClnRationalNumber> const&);
+ template storm::ClnRationalNumber maximum(std::map<uint64_t, storm::ClnRationalNumber> const&);
+ template std::pair<storm::ClnRationalNumber, storm::ClnRationalNumber> minmax(std::vector<storm::ClnRationalNumber> const&);
+ template storm::ClnRationalNumber minimum(std::vector<storm::ClnRationalNumber> const&);
+ template storm::ClnRationalNumber maximum(std::vector<storm::ClnRationalNumber> const&);
+ template storm::ClnRationalNumber pow(storm::ClnRationalNumber const& value, uint_fast64_t exponent);
+ template storm::ClnRationalNumber sqrt(storm::ClnRationalNumber const& number);
+ template storm::ClnRationalNumber abs(storm::ClnRationalNumber const& number);
+ template storm::ClnRationalNumber floor(storm::ClnRationalNumber const& number);
+ template storm::ClnRationalNumber ceil(storm::ClnRationalNumber const& number);
+ template std::string to_string(storm::ClnRationalNumber const& value);
+#endif
- template std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::vector<storm::RationalNumber> const&);
- template storm::RationalNumber minimum(std::vector<storm::RationalNumber> const&);
- template storm::RationalNumber maximum(std::vector<storm::RationalNumber> const&);
+#if defined(STORM_HAVE_GMP)
+ // Instantiations for (GMP) rational number.
+ template storm::GmpRationalNumber one();
+ template storm::GmpRationalNumber zero();
+ template storm::GmpRationalNumber infinity();
+ template bool isOne(storm::GmpRationalNumber const& value);
+ template bool isZero(storm::GmpRationalNumber const& value);
+ template bool isConstant(storm::GmpRationalNumber const& value);
+ template bool isInfinity(storm::GmpRationalNumber const& value);
+ template bool isInteger(storm::GmpRationalNumber const& number);
+ template double convertNumber(storm::GmpRationalNumber const& number);
+ template uint_fast64_t convertNumber(storm::GmpRationalNumber const& number);
+ template storm::GmpRationalNumber convertNumber(double const& number);
+ template storm::GmpRationalNumber convertNumber(storm::GmpRationalNumber const& number);
+ template GmpRationalNumber convertNumber(std::string const& number);
+ template storm::GmpRationalNumber simplify(storm::GmpRationalNumber value);
+ template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber> matrixEntry);
+ template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>& matrixEntry);
+ template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>&& matrixEntry);
+ template std::pair<storm::GmpRationalNumber, storm::GmpRationalNumber> minmax(std::map<uint64_t, storm::GmpRationalNumber> const&);
+ template storm::GmpRationalNumber minimum(std::map<uint64_t, storm::GmpRationalNumber> const&);
+ template storm::GmpRationalNumber maximum(std::map<uint64_t, storm::GmpRationalNumber> const&);
+ template std::pair<storm::GmpRationalNumber, storm::GmpRationalNumber> minmax(std::vector<storm::GmpRationalNumber> const&);
+ template storm::GmpRationalNumber minimum(std::vector<storm::GmpRationalNumber> const&);
+ template storm::GmpRationalNumber maximum(std::vector<storm::GmpRationalNumber> const&);
+ template storm::GmpRationalNumber pow(storm::GmpRationalNumber const& value, uint_fast64_t exponent);
+ template storm::GmpRationalNumber sqrt(storm::GmpRationalNumber const& number);
+ template storm::GmpRationalNumber abs(storm::GmpRationalNumber const& number);
+ template storm::GmpRationalNumber floor(storm::GmpRationalNumber const& number);
+ template storm::GmpRationalNumber ceil(storm::GmpRationalNumber const& number);
+ template std::string to_string(storm::GmpRationalNumber const& value);
+#endif
- template storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&);
- template storm::RationalFunction maximum(std::vector<storm::RationalFunction> const&);
+#if defined(STORM_HAVE_CARL) && defined(STORM_HAVE_GMP) && defined(STORM_HAVE_CLN)
+ template storm::GmpRationalNumber convertNumber(storm::ClnRationalNumber const& number);
+ template storm::ClnRationalNumber convertNumber(storm::GmpRationalNumber const& number);
+#endif
- template std::pair<double, double> minmax(std::map<uint64_t, double> const&);
- template double minimum(std::map<uint64_t, double> const&);
- template double maximum(std::map<uint64_t, double> const&);
-
#ifdef STORM_HAVE_CARL
- // Instantiations for rational number.
- template std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::map<uint64_t, storm::RationalNumber> const&);
- template storm::RationalNumber minimum(std::map<uint64_t, storm::RationalNumber> const&);
- template storm::RationalNumber maximum(std::map<uint64_t, storm::RationalNumber> const&);
-
- template bool isOne(storm::RationalNumber const& value);
- template bool isZero(storm::RationalNumber const& value);
- template bool isConstant(storm::RationalNumber const& value);
-
- template storm::RationalNumber one();
- template storm::RationalNumber zero();
- template storm::RationalNumber infinity();
-
- template double convertNumber(storm::RationalNumber const& number);
- template uint_fast64_t convertNumber(storm::RationalNumber const& number);
- template storm::RationalNumber convertNumber(double const& number);
- template storm::RationalNumber convertNumber(storm::RationalNumber const& number);
- RationalNumber convertNumber(std::string const& number);
-
- template storm::RationalNumber sqrt(storm::RationalNumber const& number);
- template storm::RationalNumber abs(storm::RationalNumber const& number);
- template storm::RationalNumber floor(storm::RationalNumber const& number);
- template storm::RationalNumber ceil(storm::RationalNumber const& number);
-
- template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
-
- template storm::RationalNumber simplify(storm::RationalNumber value);
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry);
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry);
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& matrixEntry);
-
// Instantiations for rational function.
+ template RationalFunction one();
+ template RationalFunction zero();
+ template storm::RationalFunction infinity();
template bool isOne(RationalFunction const& value);
template bool isZero(RationalFunction const& value);
template bool isConstant(RationalFunction const& value);
template bool isInfinity(RationalFunction const& value);
-
- template RationalFunction one();
- template RationalFunction zero();
- template storm::RationalFunction infinity();
-
+ template bool isInteger(RationalFunction const&);
template storm::RationalFunction convertNumber(storm::RationalFunction const& number);
-
- template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
+ template RationalFunctionCoefficient convertNumber(RationalFunction const& number);
+ template RationalFunction convertNumber(storm::RationalFunctionCoefficient const& number);
template RationalFunction simplify(RationalFunction value);
template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value);
+ template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
+ template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
+ template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);
+ template std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::map<uint64_t, storm::RationalFunction> const&);
+ template storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&);
+ template storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const&);
+ template std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::vector<storm::RationalFunction> const&);
+ template storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&);
+ template storm::RationalFunction maximum(std::vector<storm::RationalFunction> const&);
+ template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
+ // Instantiations for polynomials.
template Polynomial one();
template Polynomial zero();
+ // Instantiations for intervals.
+ template Interval one();
+ template Interval zero();
template bool isOne(Interval const& value);
template bool isZero(Interval const& value);
template bool isConstant(Interval const& value);
template bool isInfinity(Interval const& value);
-
- template Interval one();
- template Interval zero();
-
- template storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&);
- template storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const&);
-
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
- template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);
#endif
}
diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h
index afdee551d..69d253e81 100644
--- a/src/storm/utility/constants.h
+++ b/src/storm/utility/constants.h
@@ -47,37 +47,40 @@ namespace storm {
bool isInfinity(ValueType const& a);
template<typename ValueType>
- ValueType pow(ValueType const& value, uint_fast64_t exponent);
+ bool isInteger(ValueType const& number);
+
+ template<typename TargetType, typename SourceType>
+ TargetType convertNumber(SourceType const& number);
template<typename ValueType>
ValueType simplify(ValueType value);
+ template<typename IndexType, typename ValueType>
+ storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
+
+ template<typename IndexType, typename ValueType>
+ storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
+
template<typename ValueType>
std::pair<ValueType, ValueType> minmax(std::vector<ValueType> const& values);
-
+
template<typename ValueType>
ValueType minimum(std::vector<ValueType> const& values);
template<typename ValueType>
ValueType maximum(std::vector<ValueType> const& values);
-
+
template< typename K, typename ValueType>
std::pair<ValueType, ValueType> minmax(std::map<K, ValueType> const& values);
-
+
template< typename K, typename ValueType>
ValueType minimum(std::map<K, ValueType> const& values);
template<typename K, typename ValueType>
ValueType maximum(std::map<K, ValueType> const& values);
- template<typename IndexType, typename ValueType>
- storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
-
- template<typename IndexType, typename ValueType>
- storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
-
- template<typename TargetType, typename SourceType>
- TargetType convertNumber(SourceType const& number);
+ template<typename ValueType>
+ ValueType pow(ValueType const& value, uint_fast64_t exponent);
template<typename ValueType>
ValueType sqrt(ValueType const& number);
@@ -90,9 +93,6 @@ namespace storm {
template<typename ValueType>
ValueType ceil(ValueType const& number);
-
- template<typename ValueType>
- bool isInteger(ValueType const& number);
template<typename ValueType>
std::string to_string(ValueType const& value);
diff --git a/src/storm/utility/parametric.h b/src/storm/utility/parametric.h
index 46846f2f9..1e77eb426 100644
--- a/src/storm/utility/parametric.h
+++ b/src/storm/utility/parametric.h
@@ -31,7 +31,7 @@ namespace storm {
template<>
struct VariableType<storm::RationalFunction> { typedef storm::RationalFunctionVariable type; };
template<>
- struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; };
+ struct CoefficientType<storm::RationalFunction> { typedef storm::RationalFunctionCoefficient type; };
#endif
/*!
diff --git a/src/storm/utility/region.cpp b/src/storm/utility/region.cpp
index dd7f930bc..1c55e3cd4 100644
--- a/src/storm/utility/region.cpp
+++ b/src/storm/utility/region.cpp
@@ -17,53 +17,7 @@ namespace storm {
namespace utility{
namespace region {
- template<>
- double convertNumber<double, double>(double const& number){
- return number;
- }
-
- template<>
- double&& convertNumber<double>(double&& number){
- return std::move(number);
- }
-
- template<>
- double convertNumber<double, std::string>(std::string const& number){
- return std::stod(number);
- }
-
#ifdef STORM_HAVE_CARL
- template<>
- storm::RationalNumber convertNumber<storm::RationalNumber, double>(double const& number){
- return carl::rationalize<storm::RationalNumber>(number);
- }
-
- template<>
- storm::RationalFunction convertNumber<storm::RationalFunction, double>(double const& number){
- return storm::RationalFunction(convertNumber<storm::RationalNumber>(number));
- }
-
- template<>
- double convertNumber<double, storm::RationalNumber>(storm::RationalNumber const& number){
- return carl::toDouble(number);
- }
-
- template<>
- storm::RationalNumber convertNumber<storm::RationalNumber, storm::RationalNumber>(storm::RationalNumber const& number){
- return number;
- }
-
- template<>
- storm::RationalNumber&& convertNumber<storm::RationalNumber>(storm::RationalNumber&& number){
- return std::move(number);
- }
-
- template<>
- storm::RationalNumber convertNumber<storm::RationalNumber, std::string>(std::string const& number){
- //We parse the number as double and then convert it to a a rational number.
- return convertNumber<storm::RationalNumber>(convertNumber<double>(number));
- }
-
template<>
storm::RationalFunctionVariable getVariableFromString<storm::RationalFunctionVariable>(std::string variableString){
storm::RationalFunctionVariable const& var = carl::VariablePool::getInstance().findVariableWithName(variableString);
@@ -154,7 +108,7 @@ namespace storm {
}
template<>
- void addParameterBoundsToSmtSolver<storm::solver::SmtlibSmtSolver, storm::RationalFunctionVariable, storm::RationalNumber>(std::shared_ptr<storm::solver::SmtlibSmtSolver> solver, storm::RationalFunctionVariable const& variable, storm::logic::ComparisonType relation, storm::RationalNumber const& bound){
+ void addParameterBoundsToSmtSolver<storm::solver::SmtlibSmtSolver, storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>(std::shared_ptr<storm::solver::SmtlibSmtSolver> solver, storm::RationalFunctionVariable const& variable, storm::logic::ComparisonType relation, storm::RationalFunctionCoefficient const& bound){
storm::CompareRelation compRel;
switch (relation){
case storm::logic::ComparisonType::Greater:
@@ -184,7 +138,7 @@ namespace storm {
}
template<>
- storm::RationalFunction getNewFunction<storm::RationalFunction, storm::RationalNumber>(storm::RationalNumber initialValue) {
+ storm::RationalFunction getNewFunction<storm::RationalFunction, storm::RationalFunctionCoefficient>(storm::RationalFunctionCoefficient initialValue) {
std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>> cache(new carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>());
return storm::RationalFunction(storm::RationalFunction::PolyType(storm::RationalFunction::PolyType::PolyType(initialValue), cache));
}
diff --git a/src/storm/utility/region.h b/src/storm/utility/region.h
index 27a0544e3..d02c43413 100644
--- a/src/storm/utility/region.h
+++ b/src/storm/utility/region.h
@@ -37,20 +37,6 @@ namespace storm {
using CoefficientType = std::nullptr_t;
#endif
- /*
- * Converts a number from one type to a number from the other.
- * If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings.
- */
- template<typename TargetType, typename SourceType>
- TargetType convertNumber(SourceType const& number);
-
- /*
- * Converts a number from one type to a number from the other.
- * If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings.
- */
- template<typename ValueType>
- ValueType&& convertNumber(ValueType&& number);
-
/*
* retrieves the variable object from the given string
* Throws an exception if variable not found
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index e6dac0763..de9660744 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -523,7 +523,7 @@ namespace storm {
* @return true iff the specified formula is satisfied (i.e., iff the reachability value is within the bound of the formula)
*/
inline bool checkSamplingPoint(std::shared_ptr<storm::modelchecker::region::AbstractSparseRegionModelChecker<storm::RationalFunction, double>> regionModelChecker,
- std::map<storm::RationalFunctionVariable, storm::RationalNumber> const& point){
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> const& point){
return regionModelChecker->valueIsInBoundOfFormula(regionModelChecker->getReachabilityValue(point));
}
@@ -543,8 +543,8 @@ namespace storm {
* proveAllSat=false, return=false ==> the approximative value IS within the bound of the formula (either the approximation is too bad or there are points in the region that satisfy the property)
*/
inline bool checkRegionApproximation(std::shared_ptr<storm::modelchecker::region::AbstractSparseRegionModelChecker<storm::RationalFunction, double>> regionModelChecker,
- std::map<storm::RationalFunctionVariable, storm::RationalNumber> const& lowerBoundaries,
- std::map<storm::RationalFunctionVariable, storm::RationalNumber> const& upperBoundaries,
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> const& lowerBoundaries,
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> const& upperBoundaries,
bool proveAllSat){
storm::modelchecker::region::ParameterRegion<storm::RationalFunction> region(lowerBoundaries, upperBoundaries);
return regionModelChecker->checkRegionWithApproximation(region, proveAllSat);
diff --git a/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
index 97eadec47..8ec80c0b7 100644
--- a/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
@@ -132,10 +132,10 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
- std::map<storm::RationalFunctionVariable, storm::RationalNumber> instantiation;
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*dtmc);
ASSERT_EQ(variables.size(), 1ull);
- instantiation.emplace(*variables.begin(), storm::RationalNumber(1) / storm::RationalNumber(2));
+ instantiation.emplace(*variables.begin(), storm::utility::one<storm::RationalFunctionCoefficient>() / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(2));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc, std::make_unique<storm::solver::EigenLinearEquationSolverFactory<storm::RationalFunction>>());
@@ -144,28 +144,28 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
- EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult1[0].evaluate(instantiation));
+ EXPECT_EQ(storm::utility::one<storm::RationalFunctionCoefficient>() / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(6), quantitativeResult1[0].evaluate(instantiation));
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
- EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult2[0].evaluate(instantiation));
+ EXPECT_EQ(storm::utility::one<storm::RationalFunctionCoefficient>() / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(6), quantitativeResult2[0].evaluate(instantiation));
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
- EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult3[0].evaluate(instantiation));
+ EXPECT_EQ(storm::utility::one<storm::RationalFunctionCoefficient>() / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(6), quantitativeResult3[0].evaluate(instantiation));
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
- EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0].evaluate(instantiation));
+ EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(11) / storm::utility::convertNumber<storm::RationalFunctionCoefficient>(3), quantitativeResult4[0].evaluate(instantiation));
}
#endif
diff --git a/src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
index 6e71528af..220f7f437 100644
--- a/src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
+++ b/src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
@@ -40,17 +40,17 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
EXPECT_NEAR(0.8369631407, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.8369631407, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.0476784174, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.0476784174, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.0476784174, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.9987948367, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.9987948367, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.9987948367, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6020480995, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.6020480995, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1.0000000000, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(1.0000000000, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.8429289733, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.8429289733, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -111,21 +111,21 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
EXPECT_NEAR(4.367791292, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(4.367791292, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(4.367791292, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(3.044795147, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(3.044795147, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(3.044795147, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(3.182535759, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(3.182535759, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(3.182535759, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(2.609602197, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(2.609602197, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(2.609602197, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1.842551039, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(1.842551039, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(1.842551039, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(2.453500364, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(2.453500364, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(2.453500364, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6721974438, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.6721974438, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.6721974438, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1.308324558, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(1.308324558, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(1.308324558, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -243,11 +243,11 @@ TEST(SparseDtmcRegionModelCheckerTest, DISABLED_Brp_Rew_4Par) {
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
EXPECT_NEAR(4.834779705, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(4.834779705, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(4.834779705, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(4.674651623, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(4.674651623, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(4.674651623, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.4467496536, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.4467496536, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.4467496536, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -308,17 +308,17 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioHardRegion.getSomePoint()));
EXPECT_NEAR(0.1734086422, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.1734086422, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.1734086422, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.47178, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.47178, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.47178, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.7085157883, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.5095205203, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.5095205203, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.5095205203, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6819701472, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.6819701472, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.6819701472, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.999895897, dtmcModelchecker->getReachabilityValue(allVioHardRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.999895897, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.999895897, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -399,13 +399,13 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
EXPECT_NEAR(0.8430128158, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.8430128158, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.8430128158, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.7731321947, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.7731321947, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.7731321947, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.4732302663, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.4732302663, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.4732302663, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.7085157883, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
@@ -462,9 +462,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.6119660237, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
- EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ EXPECT_NEAR(0.6119660237, storm::utility::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
diff --git a/src/test/storage/SylvanDdTest.cpp b/src/test/storage/SylvanDdTest.cpp
index f480c6894..a4e4764b0 100644
--- a/src/test/storage/SylvanDdTest.cpp
+++ b/src/test/storage/SylvanDdTest.cpp
@@ -442,8 +442,8 @@ TEST(SylvanDd, RationalFunctionConstants) {
carl::StringParser parser;
parser.setVariables({"x", "y", "z"});
- storm::RationalFunction partA = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalNumber>("2*x+x*y"), cache));
- storm::RationalFunction partB = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalNumber>("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalNumber>("2*y"), cache));
+ storm::RationalFunction partA = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("2*x+x*y"), cache));
+ storm::RationalFunction partB = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("2*y"), cache));
storm::RationalFunction rationalFunction = storm::RationalFunction(partA + partB);
@@ -472,14 +472,14 @@ TEST(SylvanDd, RationalFunctionToDouble) {
storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZ1 = manager->getEncoding(zExpr.first, 1);
storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> complexAdd =
- ((bddX0 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(-1))))
- + ((bddX0 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(0))))
- + ((bddX0 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(2))))
- + ((bddX0 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(3))))
- + ((bddX1 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(100000))))
- + ((bddX1 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(3))))
- + ((bddX1 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(4))))
- + ((bddX1 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalNumber(0))));
+ ((bddX0 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(-1))))
+ + ((bddX0 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(0))))
+ + ((bddX0 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(1) / storm::RationalFunctionCoefficient(2))))
+ + ((bddX0 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(1) / storm::RationalFunctionCoefficient(3))))
+ + ((bddX1 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(100000))))
+ + ((bddX1 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(3))))
+ + ((bddX1 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(4))))
+ + ((bddX1 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() * manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(0))));
EXPECT_EQ(6ul, complexAdd.getNonZeroCount());
EXPECT_EQ(7ul, complexAdd.getLeafCount());
EXPECT_EQ(14ul, complexAdd.getNodeCount());
diff --git a/src/test/utility/ModelInstantiatorTest.cpp b/src/test/utility/ModelInstantiatorTest.cpp
index 145881598..11b89045c 100644
--- a/src/test/utility/ModelInstantiatorTest.cpp
+++ b/src/test/utility/ModelInstantiatorTest.cpp
@@ -36,13 +36,13 @@ TEST(ModelInstantiatorTest, BrpProb) {
EXPECT_FALSE(dtmc->hasRewardModel());
{
- std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
- valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.8)));
- valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
+ valuation.insert(std::make_pair(pL, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.8)));
+ valuation.insert(std::make_pair(pK, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.9)));
storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
@@ -69,13 +69,13 @@ TEST(ModelInstantiatorTest, BrpProb) {
}
{
- std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
- valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
- valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1.0)));
+ valuation.insert(std::make_pair(pL, storm::utility::one<storm::RationalFunctionCoefficient>()));
+ valuation.insert(std::make_pair(pK, storm::utility::one<storm::RationalFunctionCoefficient>()));
storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
@@ -102,13 +102,13 @@ TEST(ModelInstantiatorTest, BrpProb) {
}
{
- std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
- valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
- valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
+ valuation.insert(std::make_pair(pL, storm::utility::one<storm::RationalFunctionCoefficient>()));
+ valuation.insert(std::make_pair(pK, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.9)));
storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
@@ -153,7 +153,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
{
- std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
@@ -162,10 +162,10 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
storm::RationalFunctionVariable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
- valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.9)));
- valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.3)));
- valuation.insert(std::make_pair(TOMsg,carl::rationalize<storm::RationalNumber>(0.3)));
- valuation.insert(std::make_pair(TOAck,carl::rationalize<storm::RationalNumber>(0.5)));
+ valuation.insert(std::make_pair(pL, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.9)));
+ valuation.insert(std::make_pair(pK, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.3)));
+ valuation.insert(std::make_pair(TOMsg, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.3)));
+ valuation.insert(std::make_pair(TOAck, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.5)));
storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
@@ -222,13 +222,13 @@ TEST(ModelInstantiatorTest, Consensus) {
storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);
- std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
storm::RationalFunctionVariable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1");
ASSERT_NE(p1, carl::Variable::NO_VARIABLE);
storm::RationalFunctionVariable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2");
ASSERT_NE(p2, carl::Variable::NO_VARIABLE);
- valuation.insert(std::make_pair(p1,carl::rationalize<storm::RationalNumber>(0.51)));
- valuation.insert(std::make_pair(p2,carl::rationalize<storm::RationalNumber>(0.49)));
+ valuation.insert(std::make_pair(p1, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.51)));
+ valuation.insert(std::make_pair(p2, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.49)));
storm::models::sparse::Mdp<double> const& instantiated(modelInstantiator.instantiate(valuation));
ASSERT_EQ(mdp->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());