From ee90c51b2abebdc549e9037b8e952ccdf1129912 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 25 Mar 2017 22:11:04 +0100 Subject: [PATCH] cleaned up constants.cpp to finalize separation of rational functions and rational numbers --- .../3rdparty/sylvan/src/storm_wrapper.cpp | 29 +- .../src/sylvan_storm_rational_function.c | 6 +- .../sylvan/src/sylvan_storm_rational_number.c | 6 +- src/storm/adapters/CarlAdapter.h | 6 +- src/storm/adapters/NumberAdapter.h | 25 +- src/storm/builder/DdPrismModelBuilder.cpp | 6 +- .../region/ApproximationModel.cpp | 8 +- .../modelchecker/region/ParameterRegion.cpp | 8 +- .../region/SparseDtmcRegionModelChecker.cpp | 6 +- .../region/SparseMdpRegionModelChecker.cpp | 2 +- .../region/SparseRegionModelChecker.cpp | 10 +- src/storm/storage/SparseMatrix.cpp | 35 +- .../storage/dd/sylvan/SylvanAddIterator.cpp | 1 - src/storm/utility/ConstantsComparator.cpp | 9 +- src/storm/utility/constants.cpp | 927 +++++++++++------- src/storm/utility/constants.h | 30 +- src/storm/utility/parametric.h | 2 +- src/storm/utility/region.cpp | 50 +- src/storm/utility/region.h | 14 - src/storm/utility/storm.h | 6 +- .../EigenDtmcPrctlModelCheckerTest.cpp | 12 +- .../SparseDtmcRegionModelCheckerTest.cpp | 58 +- src/test/storage/SylvanDdTest.cpp | 20 +- src/test/utility/ModelInstantiatorTest.cpp | 34 +- 24 files changed, 724 insertions(+), 586 deletions(-) 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 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(srf_a) < storm::utility::convertNumber(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(srf_a) <= storm::utility::convertNumber(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(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(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 #pragma clang diagnostic pop #endif -#if defined STORM_HAVE_GMP +#if defined(STORM_HAVE_GMP) #include #include #endif #include -#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 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 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() * 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 statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); storm::dd::Bdd 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(storm::utility::region::getConstantPart(oldEntry.getValue()))); + eqSysMatrixEntry->setValue(storm::utility::convertNumber(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(storm::utility::region::getConstantPart(targetProbability)); + *vectorIt = storm::utility::convertNumber(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(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState])); + ConstantType reward = storm::utility::convertNumber(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]; matrixRowmatrixData.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 currValue = storm::utility::convertNumber( 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::toString() const { std::stringstream regionstringstream; for (auto var : this->getVariables()) { - regionstringstream << storm::utility::region::convertNumber(this->getLowerBoundary(var)); + regionstringstream << storm::utility::convertNumber(this->getLowerBoundary(var)); regionstringstream << "<="; regionstringstream << storm::utility::region::getVariableName(var); regionstringstream << "<="; - regionstringstream << storm::utility::region::convertNumber(this->getUpperBoundary(var)); + regionstringstream << storm::utility::convertNumber(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(parameter); - CoefficientType lb = storm::utility::region::convertNumber(parameterBoundariesString.substr(0,positionOfFirstRelation)); - CoefficientType ub = storm::utility::region::convertNumber(parameterBoundariesString.substr(positionOfSecondRelation+2)); + CoefficientType lb = storm::utility::convertNumber(parameterBoundariesString.substr(0,positionOfFirstRelation)); + CoefficientType ub = storm::utility::convertNumber(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(-1.0); + constantResult = storm::utility::convertNumber(-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(-1.0); + constantResult = storm::utility::convertNumber(-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(new storm::solver::SmtlibSmtSolver(manager, true)); - ParametricType bound= storm::utility::region::convertNumber(this->getSpecifiedFormulaBound()); + ParametricType bound= storm::utility::convertNumber(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(-1.0); //-1 denotes that the result is constant but not yet computed + constantResult = storm::utility::convertNumber(-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 ConstantType SparseRegionModelChecker::getSpecifiedFormulaBound() const { - return storm::utility::region::convertNumber(this->getSpecifiedFormula()->getThreshold()); + return storm::utility::convertNumber(this->getSpecifiedFormula()->getThreshold()); } template @@ -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(-1.0)){ + } else if (this->isResultConstant() && this->constantResult.get() == storm::utility::convertNumber(-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 fractionOfAllSatArea = storm::utility::zero(); CoefficientType fractionOfAllViolatedArea = storm::utility::zero(); - while(fractionOfUndiscoveredArea > storm::utility::region::convertNumber(refinementThreshold)){ + while(fractionOfUndiscoveredArea > storm::utility::convertNumber(refinementThreshold)){ STORM_LOG_THROW(indexOfCurrentRegion < regions.size(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left."); ParameterRegion& 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;" <(fractionOfAllSatArea) << ";" << storm::utility::region::convertNumber(fractionOfAllViolatedArea) << ";" << storm::utility::region::convertNumber(fractionOfUndiscoveredArea) << std::endl; + std::cout << "REFINEMENTRESULT;" <(fractionOfAllSatArea) << ";" << storm::utility::convertNumber(fractionOfAllViolatedArea) << ";" << storm::utility::convertNumber(fractionOfUndiscoveredArea) << std::endl; } @@ -487,7 +487,7 @@ namespace storm { template bool SparseRegionModelChecker::valueIsInBoundOfFormula(CoefficientType const& value){ - return valueIsInBoundOfFormula(storm::utility::region::convertNumber(value)); + return valueIsInBoundOfFormula(storm::utility::convertNumber(value)); } template 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::isSubmatrixOf(SparseMatrix const& matrix) const; #ifdef STORM_HAVE_CARL - // Rat Number - template class MatrixEntry::index_type, RationalNumber>; - template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); - template class SparseMatrixBuilder; - template class SparseMatrix; - template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); - template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; - template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - - // Rat Function + // Rational Numbers + +#if defined(STORM_HAVE_CLN) + template class MatrixEntry::index_type, ClnRationalNumber>; + template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); + template class SparseMatrixBuilder; + template class SparseMatrix; + template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; +#endif + +#if defined(STORM_HAVE_GMP) + template class MatrixEntry::index_type, GmpRationalNumber>; + template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); + template class SparseMatrixBuilder; + template class SparseMatrix; + template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; +#endif + + // Rational Function template class MatrixEntry::index_type, RationalFunction>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; @@ -1625,7 +1638,7 @@ namespace storm { template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - + // Intervals template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template class MatrixEntry::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 #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; #ifdef STORM_HAVE_CARL +#if defined(STORM_HAVE_CLN) + template class ConstantsComparator; +#endif + +#if defined(STORM_HAVE_GMP) + template class ConstantsComparator; +#endif + template class ConstantsComparator; template class ConstantsComparator; template class ConstantsComparator; - template class ConstantsComparator; #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 + #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 + bool isInfinity(ValueType const& a) { + return a == infinity(); + } template bool isInteger(ValueType const& number) { @@ -49,132 +56,22 @@ namespace storm { ValueType result = std::modf(number, &iPart); return result == zero(); } - - template - bool isInfinity(ValueType const& a) { - return a == infinity(); - } - + template<> bool isInteger(int const&) { return true; } - - template<> - bool isInteger(uint_fast64_t const&) { - return true; - } - - template - 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(); - } - - 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 - 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 - 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 - ValueType sqrt(ValueType const& number) { - return std::sqrt(number); + template<> + double convertNumber(double const& number){ + return number; } template - 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 - ValueType floor(ValueType const& number) { - return std::floor(number); + + template + storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; } - template - ValueType ceil(ValueType const& number) { - return std::ceil(number); + template + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; } - template<> - std::pair minmax(std::vector const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum/maximum for rational functions is not defined."); + template + storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry) { + simplify(matrixEntry.getValue()); + return std::move(matrixEntry); } template @@ -226,51 +128,17 @@ namespace storm { return std::make_pair(min, max); } - template<> - std::pair minmax(std::vector 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()) { - 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 const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined."); - } - template ValueType minimum(std::vector const& values) { return minmax(values).first; } - template<> - storm::RationalFunction maximum(std::vector const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined."); - } template ValueType maximum(std::vector const& values) { return minmax(values).second; } - - template<> - std::pair minmax(std::map const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum/maximum for rational functions is not defined."); - } - + template std::pair minmax(std::map const& values) { assert(!values.empty()); @@ -286,130 +154,374 @@ namespace storm { } return std::make_pair(min, max); } - - template<> - std::pair minmax(std::map 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()) { - 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 const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined."); - } template< typename K, typename ValueType> ValueType minimum(std::map const& values) { return minmax(values).first; } - template<> - storm::RationalFunction maximum(std::map const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); - } - template ValueType maximum(std::map const& values) { return minmax(values).second; } -#ifdef STORM_HAVE_CARL - template<> - RationalFunction& simplify(RationalFunction& value); + template + ValueType pow(ValueType const& value, uint_fast64_t exponent) { + return std::pow(value, exponent); + } - template<> - RationalFunction&& simplify(RationalFunction&& value); + template + ValueType sqrt(ValueType const& number) { + return std::sqrt(number); + } + + template + ValueType abs(ValueType const& number) { + return std::fabs(number); + } + + template + ValueType floor(ValueType const& number) { + return std::floor(number); + } + + template + ValueType ceil(ValueType const& number) { + return std::ceil(number); + } + template + 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 minmax(std::vector 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()) { + 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(number); } template<> - double convertNumber(RationalNumber const& number){ + ClnRationalNumber convertNumber(ClnRationalNumber const& number){ + return number; + } + + template<> + ClnRationalNumber convertNumber(double const& number){ + return carl::rationalize(number); + } + + template<> + ClnRationalNumber convertNumber(int const& number){ + return carl::rationalize(number); + } + + template<> + ClnRationalNumber convertNumber(uint_fast64_t const& number){ + STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); + return carl::rationalize(static_cast(number)); + } + + template<> + ClnRationalNumber convertNumber(int_fast64_t const& number){ + STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); + return carl::rationalize(static_cast(number)); + } + + template<> + double convertNumber(ClnRationalNumber const& number){ return carl::toDouble(number); } + + template<> + ClnRationalNumber convertNumber(std::string const& number) { + return carl::parse(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 minmax(std::vector 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()) { + max = vt; + } else { + if (vt < min) { + min = vt; + } + if (vt > max) { + max = vt; + } + } + } + return std::make_pair(min, max); + } + + template<> + std::pair minmax(std::map 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()) { + 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(number); } - + template<> - RationalNumber convertNumber(RationalNumber const& number){ + GmpRationalNumber convertNumber(GmpRationalNumber const& number){ return number; } template<> - RationalNumber convertNumber(double const& number){ - return carl::rationalize(number); + GmpRationalNumber convertNumber(double const& number){ + return carl::rationalize(number); } template<> - RationalNumber convertNumber(uint_fast64_t const& number){ - STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); - return carl::rationalize(static_cast(number)); + GmpRationalNumber convertNumber(int const& number){ + return carl::rationalize(number); } template<> - RationalNumber convertNumber(int_fast64_t const& number){ + GmpRationalNumber convertNumber(uint_fast64_t const& number){ + STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); + return carl::rationalize(static_cast(number)); + } + + template<> + GmpRationalNumber convertNumber(int_fast64_t const& number){ STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); - return carl::rationalize(static_cast(number)); + return carl::rationalize(static_cast(number)); + } + + template<> + double convertNumber(GmpRationalNumber const& number){ + return carl::toDouble(number); + } + + template<> + GmpRationalNumber convertNumber(std::string const& number) { + return carl::parse(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(to_string(number)); + } + + template<> + storm::ClnRationalNumber convertNumber(storm::GmpRationalNumber const& number) { + return carl::parse(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(number)); + bool isOne(storm::Polynomial const& a) { + return a.isOne(); } template<> - RationalFunction convertNumber(int_fast64_t const& number){ - STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); - return RationalFunction(carl::rationalize(static_cast(number))); + bool isZero(storm::RationalFunction const& a) { + return a.isZero(); } template<> - RationalNumber convertNumber(std::string const& number) { - return carl::parse(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(); + } + + 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(number)); + } + + template<> + RationalFunction convertNumber(int_fast64_t const& number){ + STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); + return RationalFunction(carl::rationalize(static_cast(number))); + } + +#if defined(STORM_HAVE_CLN) + template<> + RationalFunction convertNumber(ClnRationalNumber const& number) { + return RationalFunction(convertNumber(number)); + } +#endif + +#if defined(STORM_HAVE_GMP) + template<> + RationalFunction convertNumber(GmpRationalNumber const& number) { + return RationalFunction(convertNumber(number)); + } +#endif + template<> uint_fast64_t convertNumber(RationalFunction const& func) { return carl::toInt(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 minmax(std::vector const&) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum/maximum for rational functions is not defined."); } -#endif - - template - storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { - simplify(matrixEntry.getValue()); - return matrixEntry; + template<> + storm::RationalFunction minimum(std::vector const&) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined."); + } + + template<> + storm::RationalFunction maximum(std::vector const&) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined."); + } + + template<> + std::pair minmax(std::map const&) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum/maximum for rational functions is not defined."); + } + + template<> + storm::RationalFunction minimum(std::map const&) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined."); + } + + template<> + storm::RationalFunction maximum(std::map const&) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); } - template - storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { - simplify(matrixEntry.getValue()); - return matrixEntry; + template<> + RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { + return carl::pow(value, exponent); } - template - storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& 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 simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - + template std::pair minmax(std::vector const&); + template double minimum(std::vector const&); + template double maximum(std::vector const&); + template std::pair minmax(std::map const&); + template double minimum(std::map const&); + template double maximum(std::map 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 simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& 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 minmax(std::vector const&); + template float minimum(std::vector const&); + template float maximum(std::vector const&); + template std::pair minmax(std::map const&); + template float minimum(std::map const&); + template float maximum(std::map 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 simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& 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 simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template std::pair minmax(std::vector const&); - template double minimum(std::vector const&); - template double maximum(std::vector 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 simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + template std::pair minmax(std::map const&); + template storm::ClnRationalNumber minimum(std::map const&); + template storm::ClnRationalNumber maximum(std::map const&); + template std::pair minmax(std::vector const&); + template storm::ClnRationalNumber minimum(std::vector const&); + template storm::ClnRationalNumber maximum(std::vector 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 minmax(std::vector const&); - template storm::RationalNumber minimum(std::vector const&); - template storm::RationalNumber maximum(std::vector 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 simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + template std::pair minmax(std::map const&); + template storm::GmpRationalNumber minimum(std::map const&); + template storm::GmpRationalNumber maximum(std::map const&); + template std::pair minmax(std::vector const&); + template storm::GmpRationalNumber minimum(std::vector const&); + template storm::GmpRationalNumber maximum(std::vector 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 const&); - template storm::RationalFunction maximum(std::vector 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 minmax(std::map const&); - template double minimum(std::map const&); - template double maximum(std::map const&); - #ifdef STORM_HAVE_CARL - // Instantiations for rational number. - template std::pair minmax(std::map const&); - template storm::RationalNumber minimum(std::map const&); - template storm::RationalNumber maximum(std::map 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 simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& 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 simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + template std::pair minmax(std::map const&); + template storm::RationalFunction minimum(std::map const&); + template storm::RationalFunction maximum(std::map const&); + template std::pair minmax(std::vector const&); + template storm::RationalFunction minimum(std::vector const&); + template storm::RationalFunction maximum(std::vector 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 const&); - template storm::RationalFunction maximum(std::map const&); - - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& 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 - ValueType pow(ValueType const& value, uint_fast64_t exponent); + bool isInteger(ValueType const& number); + + template + TargetType convertNumber(SourceType const& number); template ValueType simplify(ValueType value); + template + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + + template + storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + template std::pair minmax(std::vector const& values); - + template ValueType minimum(std::vector const& values); template ValueType maximum(std::vector const& values); - + template< typename K, typename ValueType> std::pair minmax(std::map const& values); - + template< typename K, typename ValueType> ValueType minimum(std::map const& values); template ValueType maximum(std::map const& values); - template - storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - - template - storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template - TargetType convertNumber(SourceType const& number); + template + ValueType pow(ValueType const& value, uint_fast64_t exponent); template ValueType sqrt(ValueType const& number); @@ -90,9 +93,6 @@ namespace storm { template ValueType ceil(ValueType const& number); - - template - bool isInteger(ValueType const& number); template 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 { typedef storm::RationalFunctionVariable type; }; template<> - struct CoefficientType { typedef storm::RationalNumber type; }; + struct CoefficientType { 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 const& number){ - return number; - } - - template<> - double&& convertNumber(double&& number){ - return std::move(number); - } - - template<> - double convertNumber(std::string const& number){ - return std::stod(number); - } - #ifdef STORM_HAVE_CARL - template<> - storm::RationalNumber convertNumber(double const& number){ - return carl::rationalize(number); - } - - template<> - storm::RationalFunction convertNumber(double const& number){ - return storm::RationalFunction(convertNumber(number)); - } - - template<> - double convertNumber(storm::RationalNumber const& number){ - return carl::toDouble(number); - } - - template<> - storm::RationalNumber convertNumber(storm::RationalNumber const& number){ - return number; - } - - template<> - storm::RationalNumber&& convertNumber(storm::RationalNumber&& number){ - return std::move(number); - } - - template<> - storm::RationalNumber convertNumber(std::string const& number){ - //We parse the number as double and then convert it to a a rational number. - return convertNumber(convertNumber(number)); - } - template<> storm::RationalFunctionVariable getVariableFromString(std::string variableString){ storm::RationalFunctionVariable const& var = carl::VariablePool::getInstance().findVariableWithName(variableString); @@ -154,7 +108,7 @@ namespace storm { } template<> - void addParameterBoundsToSmtSolver(std::shared_ptr solver, storm::RationalFunctionVariable const& variable, storm::logic::ComparisonType relation, storm::RationalNumber const& bound){ + void addParameterBoundsToSmtSolver(std::shared_ptr 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::RationalNumber initialValue) { + storm::RationalFunction getNewFunction(storm::RationalFunctionCoefficient initialValue) { std::shared_ptr>> cache(new carl::Cache>()); 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 - 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 - 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> regionModelChecker, - std::map const& point){ + std::map 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> regionModelChecker, - std::map const& lowerBoundaries, - std::map const& upperBoundaries, + std::map const& lowerBoundaries, + std::map const& upperBoundaries, bool proveAllSat){ storm::modelchecker::region::ParameterRegion 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 instantiation; + std::map instantiation; std::set 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::utility::convertNumber(2)); storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); @@ -144,28 +144,28 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult1[0].evaluate(instantiation)); + EXPECT_EQ(storm::utility::one() / storm::utility::convertNumber(6), quantitativeResult1[0].evaluate(instantiation)); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult2[0].evaluate(instantiation)); + EXPECT_EQ(storm::utility::one() / storm::utility::convertNumber(6), quantitativeResult2[0].evaluate(instantiation)); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult3[0].evaluate(instantiation)); + EXPECT_EQ(storm::utility::one() / storm::utility::convertNumber(6), quantitativeResult3[0].evaluate(instantiation)); formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0].evaluate(instantiation)); + EXPECT_EQ(storm::utility::convertNumber(11) / storm::utility::convertNumber(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().getPrecision()); - EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.8369631407, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.0476784174, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0476784174, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.0476784174, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.9987948367, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9987948367, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.9987948367, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.6020480995, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6020480995, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(1.0000000000, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1.0000000000, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.8429289733, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.8429289733, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().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().getPrecision()); - EXPECT_NEAR(4.367791292, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.367791292, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(3.044795147, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.044795147, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(3.044795147, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(3.182535759, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.182535759, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(3.182535759, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(2.609602197, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.609602197, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(2.609602197, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(1.842551039, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.842551039, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1.842551039, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(2.453500364, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.453500364, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(2.453500364, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.6721974438, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6721974438, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6721974438, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(1.308324558, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.308324558, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1.308324558, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().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().getPrecision()); - EXPECT_NEAR(4.834779705, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.834779705, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(4.674651623, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.674651623, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.674651623, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.4467496536, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.4467496536, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.4467496536, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().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().getPrecision()); - EXPECT_NEAR(0.1734086422, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.1734086422, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.47178, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.47178, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.47178, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.7085157883, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.5095205203, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.5095205203, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.5095205203, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.6819701472, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6819701472, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6819701472, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.999895897, dtmcModelchecker->getReachabilityValue(allVioHardRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.999895897, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.999895897, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())), storm::settings::getModule().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().getPrecision()); - EXPECT_NEAR(0.8430128158, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.8430128158, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.7731321947, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.7731321947, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.7731321947, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.4732302663, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.4732302663, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.4732302663, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.7085157883, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().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().getPrecision()); - EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6119660237, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.6119660237, storm::utility::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().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("2*x+x*y"), cache)); - storm::RationalFunction partB = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("2*y"), cache)); + storm::RationalFunction partA = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("2*x+x*y"), cache)); + storm::RationalFunction partB = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("2*y"), cache)); storm::RationalFunction rationalFunction = storm::RationalFunction(partA + partB); @@ -472,14 +472,14 @@ TEST(SylvanDd, RationalFunctionToDouble) { storm::dd::Bdd bddZ1 = manager->getEncoding(zExpr.first, 1); storm::dd::Add complexAdd = - ((bddX0 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(-1)))) - + ((bddX0 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(0)))) - + ((bddX0 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(2)))) - + ((bddX0 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(3)))) - + ((bddX1 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(100000)))) - + ((bddX1 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(3)))) - + ((bddX1 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(4)))) - + ((bddX1 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(0)))); + ((bddX0 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalFunctionCoefficient(-1)))) + + ((bddX0 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalFunctionCoefficient(0)))) + + ((bddX0 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalFunctionCoefficient(1) / storm::RationalFunctionCoefficient(2)))) + + ((bddX0 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalFunctionCoefficient(1) / storm::RationalFunctionCoefficient(3)))) + + ((bddX1 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalFunctionCoefficient(100000)))) + + ((bddX1 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalFunctionCoefficient(3)))) + + ((bddX1 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalFunctionCoefficient(4)))) + + ((bddX1 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(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 valuation; + std::map 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(0.8))); - valuation.insert(std::make_pair(pK,carl::rationalize(0.9))); + valuation.insert(std::make_pair(pL, storm::utility::convertNumber(0.8))); + valuation.insert(std::make_pair(pK, storm::utility::convertNumber(0.9))); storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); @@ -69,13 +69,13 @@ TEST(ModelInstantiatorTest, BrpProb) { } { - std::map valuation; + std::map 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(1.0))); - valuation.insert(std::make_pair(pK,carl::rationalize(1.0))); + valuation.insert(std::make_pair(pL, storm::utility::one())); + valuation.insert(std::make_pair(pK, storm::utility::one())); storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); @@ -102,13 +102,13 @@ TEST(ModelInstantiatorTest, BrpProb) { } { - std::map valuation; + std::map 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(1.0))); - valuation.insert(std::make_pair(pK,carl::rationalize(0.9))); + valuation.insert(std::make_pair(pL, storm::utility::one())); + valuation.insert(std::make_pair(pK, storm::utility::convertNumber(0.9))); storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); @@ -153,7 +153,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) { storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); { - std::map valuation; + std::map 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(0.9))); - valuation.insert(std::make_pair(pK,carl::rationalize(0.3))); - valuation.insert(std::make_pair(TOMsg,carl::rationalize(0.3))); - valuation.insert(std::make_pair(TOAck,carl::rationalize(0.5))); + valuation.insert(std::make_pair(pL, storm::utility::convertNumber(0.9))); + valuation.insert(std::make_pair(pK, storm::utility::convertNumber(0.3))); + valuation.insert(std::make_pair(TOMsg, storm::utility::convertNumber(0.3))); + valuation.insert(std::make_pair(TOAck, storm::utility::convertNumber(0.5))); storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); @@ -222,13 +222,13 @@ TEST(ModelInstantiatorTest, Consensus) { storm::utility::ModelInstantiator, storm::models::sparse::Mdp> modelInstantiator(*mdp); - std::map valuation; + std::map 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(0.51))); - valuation.insert(std::make_pair(p2,carl::rationalize(0.49))); + valuation.insert(std::make_pair(p1, storm::utility::convertNumber(0.51))); + valuation.insert(std::make_pair(p2, storm::utility::convertNumber(0.49))); storm::models::sparse::Mdp const& instantiated(modelInstantiator.instantiate(valuation)); ASSERT_EQ(mdp->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());