From 8b97895e24471398c83d04fe1dc2e41126580c30 Mon Sep 17 00:00:00 2001
From: Jan Erik Karuc <jan.karuc@rwth-aachen.de>
Date: Thu, 27 Feb 2020 17:57:07 +0100
Subject: [PATCH] OVI: More debug output & cross case assert

---
 src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index e81830610..c40df46ae 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -426,6 +426,7 @@ namespace storm {
             uint64_t up_occur = 0;
             uint64_t cross_occur = 0;
             uint64_t down_occur = 0;
+            uint64_t no_case_occur = 0;
             //DEBUG END
 
             if (!this->multiplierA) {
@@ -539,6 +540,7 @@ namespace storm {
                             break;
                         } else if (valuesCrossed) {
                             ++cross_occur;
+                            STORM_LOG_ASSERT(false, "Cross case occurred.");
                             iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues);
                             break;
                         } else if (newUpperBoundAlwaysLowerEqual) {
@@ -568,6 +570,9 @@ namespace storm {
                                 status = SolverStatus::Converged;
                             }
                         }
+                        else {
+                            ++no_case_occur;
+                        }
                         
                         ValueType scaledIterationCount = storm::utility::convertNumber<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor());
                         if (scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) {
@@ -591,7 +596,7 @@ namespace storm {
             }
 
             // DEBUG
-            std::cout << "Up mov: " << up_occur << ", Cross: " << cross_occur << ", Down mov: " << down_occur;
+            std::cout << "Up mov: " << up_occur << ", Cross: " << cross_occur << ", Down mov: " << down_occur << ", None: " << no_case_occur << std::endl;
             // DEBUG END
 
             reportStatus(status, overallIterations);