From d0b54fe6b50005a1f8bff211136810a7014680a0 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 11 Mar 2020 12:04:43 +0100
Subject: [PATCH] Set number of printed digits in output

---
 src/storm-cli-utilities/cli.cpp             |  2 ++
 src/storm/models/sparse/MarkovAutomaton.cpp |  2 +-
 src/storm/utility/file.h                    |  2 +-
 src/storm/utility/initialize.cpp            | 21 ++++++++++++++++++++-
 src/storm/utility/initialize.h              | 13 +++++++++++++
 5 files changed, 37 insertions(+), 3 deletions(-)

diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp
index 64a2fcd72..869fc2942 100644
--- a/src/storm-cli-utilities/cli.cpp
+++ b/src/storm-cli-utilities/cli.cpp
@@ -238,6 +238,8 @@ namespace storm {
             setResourceLimits();
             setLogLevel();
             setFileLogging();
+            // Set output precision
+            storm::utility::setOutputDigitsFromGeneralPrecision(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
         }
 
         
diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp
index bea9278c5..39a33d7a6 100644
--- a/src/storm/models/sparse/MarkovAutomaton.cpp
+++ b/src/storm/models/sparse/MarkovAutomaton.cpp
@@ -225,7 +225,7 @@ namespace storm {
                     }
                     return std::make_shared<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(components));
                 }
-                STORM_LOG_TRACE("MA matrix:" << std::endl << this->getTransitionMatrix());
+                //STORM_LOG_TRACE("MA matrix:" << std::endl << this->getTransitionMatrix());
                 STORM_LOG_TRACE("Markovian states: " << getMarkovianStates());
 
                 // Eliminate all probabilistic states by state elimination
diff --git a/src/storm/utility/file.h b/src/storm/utility/file.h
index f4a1cbc96..5d55a2271 100644
--- a/src/storm/utility/file.h
+++ b/src/storm/utility/file.h
@@ -22,7 +22,7 @@ namespace storm {
                 filestream.open(filepath);
             }
             STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
-            filestream.precision(10);
+            filestream.precision(std::cout.precision());
             if (!silent) {
                 STORM_PRINT_AND_LOG("Write to file " << filepath << "." << std::endl);
             }
diff --git a/src/storm/utility/initialize.cpp b/src/storm/utility/initialize.cpp
index ffd92d693..f548aa51b 100644
--- a/src/storm/utility/initialize.cpp
+++ b/src/storm/utility/initialize.cpp
@@ -5,6 +5,7 @@
 
 #include <iostream>
 #include <fstream>
+#include <math.h>
 
 namespace storm {
     namespace utility {
@@ -27,12 +28,30 @@ namespace storm {
 
         void setUp() {
             initializeLogger();
-            std::cout.precision(10);
+            setOutputDigits(10);
         }
 
         void cleanUp() {
             // Intentionally left empty.
         }
+
+        void setOutputDigits(int digits) {
+            std::cout.precision(digits);
+        }
+
+        void setOutputDigitsFromGeneralPrecision(float precision) {
+            if (precision >= 1 || precision < 0) {
+                setOutputDigits(10);
+            } else {
+                int digits = ceil(-log10(precision)) + 4;
+                // Ensure at least 10 digits for now
+                if (digits < 10) {
+                    setOutputDigits(10);
+                } else {
+                    setOutputDigits(digits);
+                }
+            }
+        }
         
         l3pp::LogLevel getLogLevel() {
             return l3pp::Logger::getRootLogger()->getLevel();
diff --git a/src/storm/utility/initialize.h b/src/storm/utility/initialize.h
index 9d7c026a2..6b3be3be9 100644
--- a/src/storm/utility/initialize.h
+++ b/src/storm/utility/initialize.h
@@ -19,6 +19,19 @@ namespace storm {
          */
         void cleanUp();
 
+        /*!
+         * Set number of digits for printing output.
+         * @param digits Number of digits to print.
+         */
+        void setOutputDigits(int digits);
+
+        /*!
+         * Set number of digits for printing output from given precision requirement.
+         * For a precision of 1e-n we output at least n digits.
+         * @param precision General precision.
+         */
+        void setOutputDigitsFromGeneralPrecision(float precision);
+
         /*!
          * Gets the global log level
          */