From 76c99b55af1882aada2c4b26373dc27ff29d0b0a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 13 Jan 2017 18:04:16 +0100
Subject: [PATCH] return more precise result in dd equation solver

---
 .../modelchecker/results/HybridQuantitativeCheckResult.cpp | 3 +++
 .../results/SymbolicQuantitativeCheckResult.cpp            | 3 +++
 src/storm/solver/SymbolicLinearEquationSolver.cpp          | 7 ++-----
 3 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp
index a712f1125..0d9e86fc5 100644
--- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp
+++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp
@@ -115,6 +115,9 @@ namespace storm {
                             }
                             out << valuationValuePair.second;
                         }
+                        if (symbolicStates.getNonZeroCount() != this->symbolicValues.getNonZeroCount()) {
+                            out << ", 0";
+                        }
                     }
                 }
                 if (!this->explicitStates.isZero()) {
diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
index 6bd18f1b8..9dce5fe56 100644
--- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
+++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
@@ -75,6 +75,9 @@ namespace storm {
                         }
                         out << valuationValuePair.second;
                     }
+                    if (states.getNonZeroCount() != this->values.getNonZeroCount()) {
+                        out << ", 0";
+                    }
                 }
                 out << "}";
             } else {
diff --git a/src/storm/solver/SymbolicLinearEquationSolver.cpp b/src/storm/solver/SymbolicLinearEquationSolver.cpp
index 90db5d037..5bcaea1bc 100644
--- a/src/storm/solver/SymbolicLinearEquationSolver.cpp
+++ b/src/storm/solver/SymbolicLinearEquationSolver.cpp
@@ -54,11 +54,8 @@ namespace storm {
                 
                 // Now check if the process already converged within our precision.
                 converged = xCopy.equalModuloPrecision(tmp, precision, relative);
-                
-                // If the method did not converge yet, we prepare the x vector for the next iteration.
-                if (!converged) {
-                    xCopy = tmp;
-                }
+
+                xCopy = tmp;
                 
                 // Increase iteration count so we can abort if convergence is too slow.
                 ++iterationCount;