From 8a77e3238d83d3082823ea0ac39046d3c288af3c Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 11 Sep 2020 17:03:26 +0200 Subject: [PATCH 1/2] Implemented isAlmostZero and isAlmostOne also for non-double value types. --- src/storm/utility/constants.cpp | 26 ++++++++++++++++++++++---- src/storm/utility/constants.h | 6 ++++-- 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 1b2bdff97..9172807ad 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -55,12 +55,14 @@ namespace storm { return std::isnan(value); } - bool isAlmostZero(double const& a) { - return a < 1e-12 && a > -1e-12; + template + bool isAlmostZero(ValueType const& a) { + return a < convertNumber(1e-12) && a > -convertNumber(1e-12); } - bool isAlmostOne(double const& a) { - return a < (1.0 + 1e-12) && a > (1.0 - 1e-12); + template + bool isAlmostOne(ValueType const& a) { + return a < convertNumber(1.0 + 1e-12) && a > convertNumber(1.0 - 1e-12); } template @@ -818,6 +820,16 @@ namespace storm { return std::move(value); } + template<> + bool isAlmostZero(storm::RationalFunction const& a) { + return a.isConstant() && isAlmostZero(convertNumber(a)); + } + + template<> + bool isAlmostOne(storm::RationalFunction const& a) { + return a.isConstant() && isAlmostOne(convertNumber(a)); + } + template<> std::pair minmax(std::vector const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum/maximum for rational functions is not defined."); @@ -885,6 +897,8 @@ namespace storm { template double infinity(); template bool isOne(double const& value); template bool isZero(double const& value); + template bool isAlmostZero(double const& value); + template bool isAlmostOne(double const& value); template bool isConstant(double const& value); template bool isInfinity(double const& value); template bool isInteger(double const& number); @@ -982,6 +996,8 @@ namespace storm { template bool isConstant(storm::ClnRationalNumber const& value); template bool isInfinity(storm::ClnRationalNumber const& value); template bool isNan(storm::ClnRationalNumber const& value); + template bool isAlmostZero(storm::ClnRationalNumber const& value); + template bool isAlmostOne(storm::ClnRationalNumber const& value); template storm::NumberTraits::IntegerType convertNumber(storm::NumberTraits::IntegerType const& number); template storm::ClnRationalNumber convertNumber(storm::ClnRationalNumber const& number); template storm::ClnRationalNumber simplify(storm::ClnRationalNumber value); @@ -1008,6 +1024,8 @@ namespace storm { template bool isConstant(storm::GmpRationalNumber const& value); template bool isInfinity(storm::GmpRationalNumber const& value); template bool isNan(storm::GmpRationalNumber const& value); + template bool isAlmostZero(storm::GmpRationalNumber const& value); + template bool isAlmostOne(storm::GmpRationalNumber const& value); template storm::NumberTraits::IntegerType convertNumber(storm::NumberTraits::IntegerType const& number); template storm::GmpRationalNumber convertNumber(storm::GmpRationalNumber const& number); template storm::GmpRationalNumber simplify(storm::GmpRationalNumber value); diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h index ddd125edb..787ead089 100644 --- a/src/storm/utility/constants.h +++ b/src/storm/utility/constants.h @@ -88,9 +88,11 @@ namespace storm { template bool isNan(ValueType const& a); - bool isAlmostZero(double const& a); + template + bool isAlmostZero(ValueType const& a); - bool isAlmostOne(double const& a); + template + bool isAlmostOne(ValueType const& a); template bool isConstant(ValueType const& a); From 94311e7d305f5f15f6df6212ed5793b5042a1ea7 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 11 Sep 2020 17:05:04 +0200 Subject: [PATCH 2/2] Topological solvers: Added a warning for numerical issues triggered in cases where in non-exact mode a selfloop probability is very close to 1 but not equal to 1 --- src/storm/solver/TopologicalLinearEquationSolver.cpp | 11 ++++++----- .../solver/TopologicalMinMaxLinearEquationSolver.cpp | 1 + 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp index 76e4ce3ea..5ae744203 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp @@ -144,11 +144,12 @@ namespace storm { } if (hasDiagonalEntry) { - if (storm::utility::isZero(denominator)) { - STORM_LOG_THROW(storm::utility::isZero(xi), storm::exceptions::InvalidOperationException, "The equation system has no solution."); - } else { - xi /= denominator; - } + STORM_LOG_WARN_COND_DEBUG(storm::NumberTraits::IsExact || !storm::utility::isAlmostZero(denominator) || storm::utility::isZero(denominator), "State " << sccState << " has a selfloop with probability '1-(" << denominator << ")'. This could be an indication for numerical issues."); + if (storm::utility::isZero(denominator)) { + STORM_LOG_THROW(storm::utility::isZero(xi), storm::exceptions::InvalidOperationException, "The equation system has no solution."); + } else { + xi /= denominator; + } } return true; } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 7c366e436..6cf09bd45 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -155,6 +155,7 @@ namespace storm { } } if (hasDiagonalEntry) { + STORM_LOG_WARN_COND_DEBUG(storm::NumberTraits::IsExact || !storm::utility::isAlmostZero(denominator) || storm::utility::isZero(denominator), "State " << sccState << " has a selfloop with probability '1-(" << denominator << ")'. This could be an indication for numerical issues."); if (storm::utility::isZero(denominator)) { // In this case we have a selfloop on this state. This can never an optimal choice: // When minimizing, we are looking for the largest fixpoint (which will never be attained by this action)