Fixed a minor issue.

Former-commit-id: 7df7a0b38f

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -128,8 +128,13 @@ namespace storm {
             storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates;
             
             // If the initial state is known to have 0 reward or an infinite reward value, we can directly return the result.
-            STORM_LOG_THROW(model.getInitialStates().isDisjointFrom(infinityStates), storm::exceptions::IllegalArgumentException, "Initial state has infinite reward.");
-            if (!model.getInitialStates().isDisjointFrom(psiStates)) {
+            if (infinityStates.get(initialState)) {
+                STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step.");
+                // This is a work around, because not all (e.g. storm::RationalFunction) data types can represent an
+                // infinity value.
+                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<double>(initialState, storm::utility::infinity<double>()));
+            }
+            if (psiStates.get(initialState)) {
                 STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step.");
                 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initialState, storm::utility::zero<ValueType>()));
             }
@@ -538,17 +543,9 @@ namespace storm {
             // Now, we return the value for the only initial state.
             STORM_LOG_DEBUG("Simplifying and returning result.");
             if (stateRewards) {
-//                if (storm::settings::parametricSettings().isSimplifySet()) {
-//                    return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
-//                } else {
-                    return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
-//                }
+                return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
             } else {
-//                if (storm::settings::parametricSettings().isSimplifySet()) {
-//                    return storm::utility::simplify(oneStepProbabilities[*initialStates.begin()]);
-//                } else {
-                    return oneStepProbabilities[*initialStates.begin()];
-//                }
+                return oneStepProbabilities[*initialStates.begin()];
             }
         }
         

src/storage/expressions/ToRationalFunctionVisitor.cpp

@@ -48,6 +48,9 @@ namespace storm {
                 default:
                     STORM_LOG_ASSERT(false, "Illegal operator type.");
             }
+            
+            // Return a dummy. This point must, however, never be reached.
+            return boost::any();
         }
         
         template<typename RationalFunctionType>
@@ -89,9 +92,7 @@ namespace storm {
         
         template<typename RationalFunctionType>
         boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(DoubleLiteralExpression const& expression) {
-            std::stringstream str;
-            str << std::fixed << std::setprecision(3) << expression.getValue();
-            return RationalFunctionType(carl::rationalize<cln::cl_RA>(str.str()));
+            return RationalFunctionType(carl::rationalize<cln::cl_RA>(expression.getValue()));
         }
 
         template class ToRationalFunctionVisitor<storm::RationalFunction>;

src/utility/ConstantsComparator.cpp

@@ -21,6 +21,14 @@ namespace storm {
             return std::numeric_limits<ValueType>::infinity();
         }
         
+#ifdef STORM_HAVE_CARL
+        template<>
+        storm::RationalFunction infinity() {
+            // FIXME: this does not work.
+            return storm::RationalFunction(carl::rationalize<cln::cl_RA>(std::numeric_limits<double>::infinity()));
+        }
+#endif
+        
         template<typename ValueType>
         ValueType pow(ValueType const& value, uint_fast64_t exponent) {
             return std::pow(value, exponent);
@@ -188,6 +196,7 @@ namespace storm {
 
         template RationalFunction one();
         template RationalFunction zero();
+        template storm::RationalFunction infinity();
         
         template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
         

src/utility/ConstantsComparator.h

@@ -33,6 +33,11 @@ namespace storm {
         template<typename ValueType>
         ValueType infinity();
         
+#ifdef STORM_HAVE_CARL
+        template<>
+        storm::RationalFunction infinity();
+#endif
+        
         template<typename ValueType>
         ValueType pow(ValueType const& value, uint_fast64_t exponent);
         

src/utility/cli.h

@@ -86,8 +86,6 @@ namespace storm {
 				auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL;
                 logger.setLogLevel(loglevel);
 				consoleLogAppender->setThreshold(loglevel);
-                
-                
             }
             
             /*!