From 81356d1dc8c10de54ab1fa75cb8b56edc8f47c6f Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 13 Mar 2020 20:05:54 +0100
Subject: [PATCH] Jani JSONExporter: Increased precision for output.

---
 resources/3rdparty/modernjson/src/json.hpp | 18 +++++++++++++++---
 src/storm/storage/jani/JSONExporter.cpp    | 21 ++-------------------
 src/storm/storage/jani/JSONExporter.h      |  2 +-
 3 files changed, 18 insertions(+), 23 deletions(-)

diff --git a/resources/3rdparty/modernjson/src/json.hpp b/resources/3rdparty/modernjson/src/json.hpp
index 9a18b60d6..98f3b6da8 100755
--- a/resources/3rdparty/modernjson/src/json.hpp
+++ b/resources/3rdparty/modernjson/src/json.hpp
@@ -168,10 +168,22 @@ and fractional parts.
         
         template <>
         void float_to_stream(std::ostream& o, storm::RationalNumber const& number) {
-            auto result = storm::utility::to_string(storm::utility::convertNumber<double>(number));
+            double numberAsDouble = storm::utility::convertNumber<double>(number);
+            std::stringstream ss;
+            ss.precision(std::numeric_limits<double>::digits10);
+            ss << numberAsDouble;
+            auto result = ss.str();
             // Parse the result again to check for accuracy
             auto compare = storm::utility::convertNumber<storm::RationalNumber>(result);
-            STORM_LOG_WARN_COND(compare == number, "Inaccurate JSON export: During export, the number " << number << " will be rounded to " << result << ".");
+            if (compare != number) {
+                // Retry with increased accuracy
+                ss = std::stringstream();
+                ss.precision(std::numeric_limits<double>::max_digits10 + 2);
+                ss << numberAsDouble;
+                result = ss.str();
+                compare = storm::utility::convertNumber<storm::RationalNumber>(result);
+                STORM_LOG_WARN_COND(compare == number, "Inaccurate JSON export: The number " << number << " will be rounded to " << compare << ". Difference is approx. " << (storm::utility::convertNumber<double, storm::RationalNumber>(number - compare)) << ".");
+            }
             o << result;
         }
         
@@ -2256,7 +2268,7 @@ Format](http://rfc7159.net/rfc7159)
             // double->string; to be safe, we read this value from
             // std::numeric_limits<number_float_t>::digits10
             // Note that other libraries need to be able to read this, so we just stick to the standard double precision.
-            ss.precision(std::numeric_limits<double>::max_digits10 + 2);
+            ss.precision(std::numeric_limits<double>::digits10);
 
             if (indent >= 0)
             {
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index bf082b3e0..e312a7e93 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -125,23 +125,6 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType");
         }
         
-        ExportJsonType numberToJson(storm::RationalNumber rn) {
-            ExportJsonType numDecl;
-            numDecl = storm::utility::convertNumber<double>(rn);
-//            if(carl::isOne(carl::getDenom(rn))) {
-//                numDecl = ExportJsonType(carl::toString(carl::getNum(rn)));
-//            } else {
-//                numDecl["op"] = "/";
-//                // TODO set json lib to work with arbitrary precision ints.
-//                assert(carl::toInt<int64_t>(carl::getNum(rn)) == carl::getNum(rn));
-//                assert(carl::toInt<int64_t>(carl::getDenom(rn)) == carl::getDenom(rn));
-//                numDecl["left"] = carl::toInt<int64_t>(carl::getNum(rn));
-//                numDecl["right"] = carl::toInt<int64_t>(carl::getDenom(rn));
-//            }
-            return numDecl;
-        }
-        
-        
         ExportJsonType FormulaToJaniJson::constructPropertyInterval(boost::optional<storm::expressions::Expression> const& lower, boost::optional<bool> const& lowerExclusive, boost::optional<storm::expressions::Expression> const& upper, boost::optional<bool> const& upperExclusive) const {
             STORM_LOG_THROW((lower.is_initialized() || upper.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval needs either a lower or an upper bound, but none was given.");
             STORM_LOG_THROW((lower.is_initialized() || !lowerExclusive.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval defines wether the lower bound is exclusive but no lower bound is given.");
@@ -690,7 +673,7 @@ namespace storm {
             return ExportJsonType(expression.getValue());
         }
         boost::any ExpressionToJson::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) {
-            return ExportJsonType(expression.getValueAsDouble());
+            return ExportJsonType(expression.getValue());
         }
         
         boost::any ExpressionToJson::visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data) {
@@ -994,7 +977,7 @@ namespace storm {
                 destEntry["location"] = locationNames.at(destination.getLocationIndex());
                 bool prob1 = false;
                 if(destination.getProbability().isLiteral()) {
-                    if(destination.getProbability().evaluateAsDouble() == 1) {
+                    if(storm::utility::isOne(destination.getProbability().evaluateAsRational())) {
                         prob1 = true;
                     }
                 }
diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h
index ba2489b03..d8ba87489 100644
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/src/storm/storage/jani/JSONExporter.h
@@ -12,7 +12,7 @@
 namespace storm {
     namespace jani {
 
-        typedef storm::json<double> ExportJsonType;
+        typedef storm::json<storm::RationalNumber> ExportJsonType;
         
         class ExpressionToJson : public storm::expressions::ExpressionVisitor, public storm::expressions::JaniExpressionVisitor {