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(number)); + double numberAsDouble = storm::utility::convertNumber(number); + std::stringstream ss; + ss.precision(std::numeric_limits::digits10); + ss << numberAsDouble; + auto result = ss.str(); // Parse the result again to check for accuracy auto compare = storm::utility::convertNumber(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::max_digits10 + 2); + ss << numberAsDouble; + result = ss.str(); + compare = storm::utility::convertNumber(result); + STORM_LOG_WARN_COND(compare == number, "Inaccurate JSON export: The number " << number << " will be rounded to " << compare << ". Difference is approx. " << (storm::utility::convertNumber(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::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::max_digits10 + 2); + ss.precision(std::numeric_limits::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(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(carl::getNum(rn)) == carl::getNum(rn)); -// assert(carl::toInt(carl::getDenom(rn)) == carl::getDenom(rn)); -// numDecl["left"] = carl::toInt(carl::getNum(rn)); -// numDecl["right"] = carl::toInt(carl::getDenom(rn)); -// } - return numDecl; - } - - ExportJsonType FormulaToJaniJson::constructPropertyInterval(boost::optional const& lower, boost::optional const& lowerExclusive, boost::optional const& upper, boost::optional 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 ExportJsonType; + typedef storm::json ExportJsonType; class ExpressionToJson : public storm::expressions::ExpressionVisitor, public storm::expressions::JaniExpressionVisitor {