Abort when getting infinity in approximation

Former-commit-id: 8bfda3656a

src/modelchecker/dft/DFTModelChecker.cpp

@@ -187,6 +187,7 @@ namespace storm {
 
                     ++iteration;
                     STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
+                    STORM_LOG_THROW(!storm::utility::isInfinity<ValueType>(approxResult.first) && !storm::utility::isInfinity<ValueType>(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity.");
                 } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError));
 
                 STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : "."));

src/utility/constants.cpp

@@ -40,6 +40,10 @@ namespace storm {
             return true;
         }
 
+        template<typename ValueType>
+        bool isInfinity(ValueType const& a) {
+            return a == infinity<ValueType>();
+        }
 
 #ifdef STORM_HAVE_CARL
         template<>
@@ -78,6 +82,12 @@ namespace storm {
             return storm::RationalFunction(-1.0);
         }
 
+        template<>
+        bool isInfinity(storm::RationalFunction const& a) {
+            // FIXME: this should be treated more properly.
+            return a == infinity<storm::RationalFunction>();
+        }
+
         template<>
         bool isOne(storm::RationalNumber const& a) {
             return carl::isOne(a);
@@ -166,6 +176,7 @@ namespace storm {
         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();
@@ -182,6 +193,7 @@ namespace storm {
         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();
@@ -198,6 +210,7 @@ namespace storm {
         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 int one();
         template int zero();
@@ -214,6 +227,7 @@ namespace storm {
         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 uint32_t one();
         template uint32_t zero();
@@ -235,6 +249,7 @@ namespace storm {
         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();
@@ -251,6 +266,7 @@ namespace storm {
         template bool isOne(RationalNumber const& value);
         template bool isZero(RationalNumber const& value);
         template bool isConstant(RationalNumber const& value);
+        template bool isInfinity(RationalNumber const& value);
 
         template RationalNumber one();
         template RationalNumber zero();
@@ -261,6 +277,7 @@ namespace storm {
         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();

src/utility/constants.h

@@ -39,6 +39,9 @@ namespace storm {
         template<typename ValueType>
         bool isConstant(ValueType const& a);
 
+        template<typename ValueType>
+        bool isInfinity(ValueType const& a);
+
         template<typename ValueType>
         ValueType pow(ValueType const& value, uint_fast64_t exponent);