From e0e5cd9f0e37d42e99bae93169fd54e931064b60 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 20 Jul 2016 18:45:16 +0200 Subject: [PATCH] progress on support for gmp, with cln everything should be fine Former-commit-id: c91b5a7cef8e9743c923a44639bdec54b86e2d41 --- CMakeLists.txt | 2 +- .../stateelimination/EliminatorBase.cpp | 10 +- .../LongRunAverageEliminator.cpp | 9 +- src/utility/constants.cpp | 613 +++++++++--------- src/utility/constants.h | 177 +---- src/utility/vector.h | 6 +- 6 files changed, 341 insertions(+), 476 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index aae1745a7..411de9dca 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -374,7 +374,7 @@ find_package(CLN QUIET) set(STORM_USE_CLN_NUMBERS OFF) if(CLN_FOUND) set(STORM_HAVE_CLN ON) - set(STORM_USE_CLN_NUMBERS OFF) + set(STORM_USE_CLN_NUMBERS ON) message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}") include_directories("${CLN_INCLUDE_DIR}") list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES}) diff --git a/src/solver/stateelimination/EliminatorBase.cpp b/src/solver/stateelimination/EliminatorBase.cpp index 43f94f329..25907ca8c 100644 --- a/src/solver/stateelimination/EliminatorBase.cpp +++ b/src/solver/stateelimination/EliminatorBase.cpp @@ -49,7 +49,8 @@ namespace storm { } else if (Mode == ScalingMode::DivideOneMinus) { if (hasEntryInColumn) { STORM_LOG_ASSERT(columnValue != storm::utility::one(), "The scaling mode 'divide-one-minus' requires a non-one value in the given column."); - columnValue = storm::utility::simplify(storm::utility::one() / (storm::utility::one() - columnValue)); + columnValue = storm::utility::one() / (storm::utility::one() - columnValue); + columnValue = storm::utility::simplify(columnValue); } } @@ -57,7 +58,8 @@ namespace storm { for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) { // Only scale the entries in a different column. if (entryIt->getColumn() != column) { - entryIt->setValue(storm::utility::simplify(entryIt->getValue() * columnValue)); + auto tmpVal = entryIt->getValue() * columnValue; + entryIt->setValue(storm::utility::simplify(tmpVal)); } } updateValue(column, columnValue); @@ -145,7 +147,9 @@ namespace storm { *result = *first1; ++first1; } else { - auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue())); + ValueType sprod = multiplyFactor * first2->getValue(); + ValueType sum = first1->getValue() + storm::utility::simplify(sprod); + auto probability = storm::utility::simplify(sum); *result = storm::storage::MatrixEntry::index_type, typename storm::storage::FlexibleSparseMatrix::value_type>(first1->getColumn(), probability); newBackwardEntries[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability); ++first1; diff --git a/src/solver/stateelimination/LongRunAverageEliminator.cpp b/src/solver/stateelimination/LongRunAverageEliminator.cpp index 758f71a14..88e5b5faa 100644 --- a/src/solver/stateelimination/LongRunAverageEliminator.cpp +++ b/src/solver/stateelimination/LongRunAverageEliminator.cpp @@ -12,13 +12,16 @@ namespace storm { template void LongRunAverageEliminator::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) { - this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]); - averageTimeInStates[state] = storm::utility::simplify(loopProbability * averageTimeInStates[state]); + this->stateValues[state] = loopProbability * this->stateValues[state]; + this->stateValues[state] = storm::utility::simplify(this->stateValues[state]); + averageTimeInStates[state] = loopProbability * averageTimeInStates[state]; + averageTimeInStates[state] = storm::utility::simplify(averageTimeInStates[state]); } template void LongRunAverageEliminator::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) { - this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state])); + this->stateValues[predecessor] = this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]); + this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor]); averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state])); } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 00b6e1154..f3db552ed 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -1,306 +1,307 @@ -//#include "src/utility/constants.h" -// -//#include "src/storage/sparse/StateType.h" -#include "src/storage/SparseMatrix.h" -//#include "src/settings/SettingsManager.h" -//#include "src/settings/modules/GeneralSettings.h" -// -//#include "src/adapters/CarlAdapter.h" -// -namespace storm { - namespace utility { - -// template -// ValueType one() { -// return ValueType(1); -// } -// -// template -// ValueType zero() { -// return ValueType(0); -// } -// -// template -// ValueType infinity() { -// return std::numeric_limits::infinity(); -// } -// -// template -// bool isOne(ValueType const& a) { -// return a == one(); -// } -// -// template -// bool isZero(ValueType const& a) { -// return a == zero(); -// } -// -// template -// bool isConstant(ValueType const& a) { -// return true; -// } -// -// template<> -// bool isOne(storm::RationalNumber const& a) { -// return carl::isOne(a); -// } -// -// template<> -// bool isZero(storm::RationalNumber const& a) { -// return carl::isZero(a); -// } -// -// template<> -// storm::RationalNumber infinity() { -// // FIXME: this should be treated more properly. -// return storm::RationalNumber(-1); -// } -// -// 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 -// ValueType pow(ValueType const& value, uint_fast64_t exponent) { -// return std::pow(value, exponent); -// } -// -// 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 -// ValueType abs(ValueType const& number) { -// return carl::abs(number); -// } -// -// template<> -// RationalFunction& simplify(RationalFunction& value); -// -// template<> -// RationalFunction&& simplify(RationalFunction&& value); -// -// template<> -// RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { -// return carl::pow(value, exponent); -// } -// -// template<> -// RationalFunction simplify(RationalFunction value) { -// value.simplify(); -// return value; -// } -// -// template<> -// RationalFunction& simplify(RationalFunction& value) { -// value.simplify(); -// return value; -// } -// -// template<> -// RationalFunction&& simplify(RationalFunction&& value) { -// value.simplify(); -// return std::move(value); -// } -// -// template<> -// double convertNumber(RationalNumber const& number){ -// return carl::toDouble(number); -// } -// -// template<> -// RationalNumber convertNumber(double const& number){ -// return carl::rationalize(number); -// } -// -// template<> -// RationalFunction convertNumber(double const& number){ -// return RationalFunction(carl::rationalize(number)); -// } -//// -//// template<> -//// storm::RationalNumber abs(storm::RationalNumber const& number) { -//// return carl::abs(number); -//// } -// - template - storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { - simplify(matrixEntry.getValue()); - return matrixEntry; - } - - template - storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { - simplify(matrixEntry.getValue()); - return matrixEntry; - } - - template - storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry) { - simplify(matrixEntry.getValue()); - return std::move(matrixEntry); - } -// -// // Explicit instantiations. -// template bool isOne(double const& value); -// template bool isZero(double const& value); -// template bool isConstant(double const& value); -// -// template double one(); -// template double zero(); -// template double infinity(); -// -// template double pow(double const& value, uint_fast64_t exponent); -// -// 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 double abs(double const& number); -// -// template bool isOne(float const& value); -// template bool isZero(float const& value); -// template bool isConstant(float const& value); -// -// template float one(); -// template float zero(); -// template float infinity(); -// -// template float pow(float const& value, uint_fast64_t exponent); -// -// template float simplify(float 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 int one(); -// template int zero(); -// template int infinity(); -// -// template int pow(int const& value, uint_fast64_t exponent); -// -// 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 uint32_t one(); -// template uint32_t zero(); -// template uint32_t infinity(); -// -// 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); -// -// // Instantiations for rational number. -// 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 storm::RationalNumber convertNumber(double const& number); -// -// template storm::RationalNumber abs(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); - -#ifdef STORM_HAVE_CARL -// template bool isOne(RationalFunction const& value); -// template bool isZero(RationalFunction const& value); -// template bool isConstant(RationalFunction const& value); -// -// template RationalFunction one(); -// template RationalFunction zero(); -// template storm::RationalFunction infinity(); -// -// template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); -// template RationalFunction simplify(RationalFunction value); -// template RationalFunction& simplify(RationalFunction& value); -// template RationalFunction&& simplify(RationalFunction&& value); -// -// template Polynomial one(); -// template Polynomial zero(); -// -// template bool isOne(Interval const& value); -// template bool isZero(Interval const& value); -// template bool isConstant(Interval const& value); -// -// template Interval one(); -// template Interval zero(); - - 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 -// - } -} + #include "src/utility/constants.h" + + #include "src/storage/sparse/StateType.h" + #include "src/storage/SparseMatrix.h" + #include "src/settings/SettingsManager.h" + #include "src/settings/modules/GeneralSettings.h" + + #include "src/adapters/CarlAdapter.h" + + namespace storm { + namespace utility { + + template + ValueType one() { + return ValueType(1); + } + + template + ValueType zero() { + return ValueType(0); + } + + template + ValueType infinity() { + return std::numeric_limits::infinity(); + } + + template + bool isOne(ValueType const& a) { + return a == one(); + } + + template + bool isZero(ValueType const& a) { + return a == zero(); + } + + template + bool isConstant(ValueType const& a) { + return true; + } + + template<> + bool isOne(storm::RationalNumber const& a) { + return carl::isOne(a); + } + + template<> + bool isZero(storm::RationalNumber const& a) { + return carl::isZero(a); + } + + template<> + storm::RationalNumber infinity() { + // FIXME: this should be treated more properly. + return storm::RationalNumber(-1); + } + + 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 + ValueType pow(ValueType const& value, uint_fast64_t exponent) { + assert(false); + //return std::pow(value, exponent); + } + + 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 + ValueType abs(ValueType const& number) { + return carl::abs(number); + } + + template<> + RationalFunction& simplify(RationalFunction& value); + + template<> + RationalFunction&& simplify(RationalFunction&& value); + + template<> + RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { + return carl::pow(value, exponent); + } + + template<> + RationalFunction simplify(RationalFunction value) { + value.simplify(); + return value; + } + + template<> + RationalFunction& simplify(RationalFunction& value) { + value.simplify(); + return value; + } + + template<> + RationalFunction&& simplify(RationalFunction&& value) { + value.simplify(); + return std::move(value); + } + + template<> + double convertNumber(RationalNumber const& number){ + return carl::toDouble(number); + } + + template<> + RationalNumber convertNumber(double const& number){ + return carl::rationalize(number); + } + + template<> + RationalFunction convertNumber(double const& number){ + return RationalFunction(carl::rationalize(number)); + } + + template<> + storm::RationalNumber abs(storm::RationalNumber const& number) { + return carl::abs(number); + } + + template + storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; + } + + template + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; + } + + template + storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry) { + simplify(matrixEntry.getValue()); + return std::move(matrixEntry); + } + + // Explicit instantiations. + template bool isOne(double const& value); + template bool isZero(double const& value); + template bool isConstant(double const& value); + + template double one(); + template double zero(); + template double infinity(); + + template double pow(double const& value, uint_fast64_t exponent); + + 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 double abs(double const& number); + + template bool isOne(float const& value); + template bool isZero(float const& value); + template bool isConstant(float const& value); + + template float one(); + template float zero(); + template float infinity(); + + template float pow(float const& value, uint_fast64_t exponent); + + template float simplify(float 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 int one(); + template int zero(); + template int infinity(); + + template int pow(int const& value, uint_fast64_t exponent); + + 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 uint32_t one(); + template uint32_t zero(); + template uint32_t infinity(); + + 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); + + // Instantiations for rational number. + 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 storm::RationalNumber convertNumber(double const& number); + + template storm::RationalNumber abs(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); + + #ifdef STORM_HAVE_CARL + template bool isOne(RationalFunction const& value); + template bool isZero(RationalFunction const& value); + template bool isConstant(RationalFunction const& value); + + template RationalFunction one(); + template RationalFunction zero(); + template storm::RationalFunction infinity(); + + template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); + template RationalFunction simplify(RationalFunction value); + template RationalFunction& simplify(RationalFunction& value); + template RationalFunction&& simplify(RationalFunction&& value); + + template Polynomial one(); + template Polynomial zero(); + + template bool isOne(Interval const& value); + template bool isZero(Interval const& value); + template bool isConstant(Interval const& value); + + template Interval one(); + template Interval zero(); + + 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/utility/constants.h b/src/utility/constants.h index 7f97acdb4..f1d150ed6 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -11,196 +11,51 @@ #include #include -#include "src/storage/sparse/StateType.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" - -#include "src/adapters/CarlAdapter.h" namespace storm { - + // Forward-declare MatrixEntry class. namespace storage { template class MatrixEntry; } - - namespace utility { - template - ValueType one() { - return ValueType(1); - } + namespace utility { template - ValueType zero() { - return ValueType(0); - } + ValueType one(); template - ValueType infinity() { - return std::numeric_limits::infinity(); - } + ValueType zero(); template - bool isOne(ValueType const& a) { - return a == one(); - } + ValueType infinity(); template - bool isZero(ValueType const& a) { - return a == zero(); - } + bool isOne(ValueType const& a); template - bool isConstant(ValueType const& a) { - return true; - } - - template<> - bool isOne(storm::RationalNumber const& a) { - return carl::isOne(a); - } - - template<> - bool isZero(storm::RationalNumber const& a) { - return carl::isZero(a); - } - - template<> - storm::RationalNumber infinity() { - // FIXME: this should be treated more properly. - return storm::RationalNumber(-1); - } - - 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); - } + bool isZero(ValueType const& a); template - ValueType pow(ValueType const& value, uint_fast64_t exponent) { - return std::pow(value, exponent); - } + bool isConstant(ValueType const& a); 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 - TargetType convertNumber(SourceType const& number); - - template<> - double convertNumber(double const& number){ - return number; - } + ValueType pow(ValueType const& value, uint_fast64_t exponent); template - ValueType abs(ValueType const& number) { - return carl::abs(number); - } - - template<> - RationalFunction& simplify(RationalFunction& value); - - template<> - RationalFunction&& simplify(RationalFunction&& value); - - template<> - RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { - return carl::pow(value, exponent); - } - - template<> - RationalFunction simplify(RationalFunction value) { - value.simplify(); - return value; - } - - template<> - RationalFunction& simplify(RationalFunction& value) { - value.simplify(); - return value; - } - - template<> - RationalFunction&& simplify(RationalFunction&& value) { - value.simplify(); - return std::move(value); - } - - template<> - double convertNumber(RationalNumber const& number){ - return carl::toDouble(number); - } - - template<> - RationalNumber convertNumber(double const& number){ - return carl::rationalize(number); - } - - template<> - RationalFunction convertNumber(double const& number){ - return RationalFunction(carl::rationalize(number)); - } -// -// template<> -// storm::RationalNumber abs(storm::RationalNumber const& number) { -// return carl::abs(number); -// } - - template - storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { - simplify(matrixEntry.getValue()); - return matrixEntry; - } + ValueType simplify(ValueType value); template - storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { - simplify(matrixEntry.getValue()); - return matrixEntry; - } + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template - storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry) { - simplify(matrixEntry.getValue()); - return std::move(matrixEntry); - } + storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + template + TargetType convertNumber(SourceType const& number); + template + ValueType abs(ValueType const& number); } } diff --git a/src/utility/vector.h b/src/utility/vector.h index e22564f08..e5ea35444 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -592,11 +592,13 @@ namespace storm { if (val2 == 0) { return (storm::utility::abs(val1) <= precision); } - if (storm::utility::abs((val1 - val2)/val2) > precision) { + T relDiff = (val1 - val2)/val2; + if (storm::utility::abs(relDiff) > precision) { return false; } } else { - if (storm::utility::abs(val1 - val2) > precision) return false; + T diff = val1 - val2; + if (storm::utility::abs(diff) > precision) return false; } return true; }