fixing issue related to vector swapping in (explicit) value iteration and power method

src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp

@@ -322,6 +322,7 @@ namespace storm {
                 
                 // Then compute the state reward vector to use in the computation.
                 storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false);
+                conversionWatch.start();
                 std::vector<ValueType> explicitTotalRewardVector = totalRewardVector.toVector(odd);
                 conversionWatch.stop();
                 STORM_LOG_INFO("Converting symbolic matrix/vector to explicit representation done in " << conversionWatch.getTimeInMilliseconds() << "ms.");

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -288,8 +288,6 @@ namespace storm {
             // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations.
             uint64_t iterations = currentIterations;
             
-            std::vector<ValueType>* originalX = currentX;
-            
             SolverStatus status = SolverStatus::InProgress;
             while (status == SolverStatus::InProgress) {
                 // Compute x' = min/max(A*x + b).
@@ -315,11 +313,6 @@ namespace storm {
                 this->showProgressIterative(iterations);
             }
             
-            // Swap the pointers so that the output is always in currentX.
-            if (originalX == newX) {
-                std::swap(currentX, newX);
-            }
-            
             return ValueIterationResult(iterations - currentIterations, status);
         }
         
@@ -1282,7 +1275,9 @@ namespace storm {
         template<typename ValueType>
         template<typename RationalType, typename ImpreciseType>
         bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, IterativeMinMaxLinearEquationSolver<ImpreciseType> const& impreciseSolver, storm::storage::SparseMatrix<RationalType> const& rationalA, std::vector<RationalType>& rationalX, std::vector<RationalType> const& rationalB, storm::storage::SparseMatrix<ImpreciseType> const& A, std::vector<ImpreciseType>& x, std::vector<ImpreciseType> const& b, std::vector<ImpreciseType>& tmpX) const {
-            
+
+            std::vector<ImpreciseType> const* originalX = &x;
+
             std::vector<ImpreciseType>* currentX = &x;
             std::vector<ImpreciseType>* newX = &tmpX;
 
@@ -1324,6 +1319,11 @@ namespace storm {
                 }
             }
             
+            // Swap the two vectors if the current result is not in the original x.
+            if (currentX != originalX) {
+                std::swap(x, tmpX);
+            }
+            
             if (status == SolverStatus::InProgress && overallIterations == env.solver().minMax().getMaximalNumberOfIterations()) {
                 status = SolverStatus::MaximalIterationsExceeded;
             }

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -307,8 +307,6 @@ namespace storm {
 
             bool useGaussSeidelMultiplication = multiplicationStyle == storm::solver::MultiplicationStyle::GaussSeidel;
             
-            std::vector<ValueType>* originalX = currentX;
-            
             bool converged = false;
             bool terminate = this->terminateNow(*currentX, guarantee);
             uint64_t iterations = currentIterations;
@@ -320,21 +318,16 @@ namespace storm {
                     this->multiplier->multiply(env, *currentX, &b, *newX);
                 }
                 
-                // Now check for termination.
+                // Check for convergence.
                 converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative);
+
+                // Check for termination.
+                std::swap(currentX, newX);
+                ++iterations;
                 terminate = this->terminateNow(*currentX, guarantee);
                 
                 // Potentially show progress.
                 this->showProgressIterative(iterations);
-                
-                // Set up next iteration.
-                std::swap(currentX, newX);
-                ++iterations;
-            }
-            
-            // Swap the pointers so that the output is always in currentX.
-            if (originalX == newX) {
-                std::swap(currentX, newX);
             }
             
             return PowerIterationResult(iterations - currentIterations, converged ? SolverStatus::Converged : (terminate ? SolverStatus::TerminatedEarly : SolverStatus::MaximalIterationsExceeded));
@@ -883,6 +876,8 @@ namespace storm {
             bool relative = env.solver().native().getRelativeTerminationCriterion();
             auto multiplicationStyle = env.solver().native().getPowerMethodMultiplicationStyle();
             
+            std::vector<ImpreciseType> const* originalX = &x;
+            
             std::vector<ImpreciseType>* currentX = &x;
             std::vector<ImpreciseType>* newX = &tmpX;
 
@@ -907,10 +902,10 @@ namespace storm {
                 
                 // Make sure that currentX and rationalX are not aliased.
                 std::vector<RationalType>* temporaryRational = TemporaryHelper<RationalType, ImpreciseType>::getTemporary(rationalX, currentX, newX);
-                
+
                 // Sharpen solution and place it in the temporary rational.
                 bool foundSolution = sharpen(p, rationalA, *currentX, rationalB, *temporaryRational);
-                
+
                 // After sharpen, if a solution was found, it is contained in the free rational.
                 
                 if (foundSolution) {
@@ -923,6 +918,11 @@ namespace storm {
                 }
             }
             
+            // Swap the two vectors if the current result is not in the original x.
+            if (currentX != originalX) {
+                std::swap(x, tmpX);
+            }
+            
             if (status == SolverStatus::InProgress && overallIterations == maxIter) {
                 status = SolverStatus::MaximalIterationsExceeded;
             }

src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

@@ -58,7 +58,7 @@ namespace storm {
             
             storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env, needAdaptPrecision);
             
-            std::cout << "Found " << this->sortedSccDecomposition->size() << "SCCs. Average size is " << static_cast<double>(this->A->getRowGroupCount()) / static_cast<double>(this->sortedSccDecomposition->size()) << "." << std::endl;
+            STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast<double>(this->A->getRowGroupCount()) / static_cast<double>(this->sortedSccDecomposition->size()) << ".");
             if (this->longestSccChainSize) {
                 std::cout << "Longest SCC chain size is " << this->longestSccChainSize.get() << std::endl;
             }