From ccc60ef145aaa6a7e2335b52bf2f7ee019b80ae8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 19 Mar 2015 18:34:15 +0100 Subject: [PATCH] Removed a lot of debug output. Former-commit-id: cbe28c66ae4c95ce3684d0603037a56365cdc8b9 --- .../csl/SparseCtmcCslModelChecker.cpp | 46 +------------------ src/utility/numerical.h | 7 --- 2 files changed, 1 insertion(+), 52 deletions(-) diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index cabf7753b..6e432c754 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -50,8 +50,6 @@ namespace storm { upperBound = pathFormula.getUpperBound(); } - std::cout << "initial: " << this->getModel().getInitialStates() << std::endl; - std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound))); return result; @@ -107,7 +105,6 @@ namespace storm { storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } else { if (comparator.isZero(lowerBound)) { - std::cout << "case [0, t]" << std::endl; // In this case, the interval is of the form [0, t]. // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. @@ -121,18 +118,14 @@ namespace storm { // Compute the uniformized matrix. storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), statesWithProbabilityGreater0, psiStates, uniformizationRate, exitRates); -// storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), psiStates, uniformizationRate, exitRates); // Finally compute the transient probabilities. std::vector psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero()); storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one()); -// storm::utility::vector::setVectorValues(psiStateValues, psiStates, storm::utility::one()); std::vector subresult = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * upperBound, psiStateValues, *this->linearEquationSolver); storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult); -// result = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * upperBound, psiStateValues, *this->linearEquationSolver); } else if (comparator.isInfinity(upperBound)) { - std::cout << "case [t, inf]" << std::endl; // In this case, the interval is of the form [t, inf] with t != 0. // Start by computing the (unbounded) reachability probabilities of reaching psi states while @@ -159,7 +152,6 @@ namespace storm { result = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * lowerBound, result, *this->linearEquationSolver); } else { // In this case, the interval is of the form [t, t'] with t != 0 and t' != inf. - std::cout << "case [t, t']" << std::endl; // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. ValueType uniformizationRate = 0; @@ -199,11 +191,6 @@ namespace storm { } } - std::cout << "final result" << std::endl; - for (uint_fast64_t index = 0; index < result.size(); ++index) { - std::cout << "result[" << index << "] = " << result[index] << std::endl; - } - return result; } @@ -249,16 +236,6 @@ namespace storm { element /= std::get<2>(foxGlynnResult); } - std::cout << "fox glynn:" << std::endl; - std::cout << "left: " << std::get<0>(foxGlynnResult) << std::endl; - std::cout << "right: " << std::get<1>(foxGlynnResult) << std::endl; - std::cout << "total: " << std::get<2>(foxGlynnResult) << std::endl; - int i = 0; - for (auto const& weight : std::get<3>(foxGlynnResult)) { - std::cout << "weight[" << i << "]: " << weight << std::endl; - ++i; - } - // Initialize result. std::vector result; uint_fast64_t startingIteration = std::get<0>(foxGlynnResult); @@ -271,41 +248,20 @@ namespace storm { } std::vector multiplicationResult(result.size()); - std::cout << "starting vector:" << std::endl; - for (int i = 0; i < result.size(); ++i) { - std::cout << i << ": " << result[i] << std::endl; - } - // Perform the matrix-vector multiplications (without adding). if (std::get<0>(foxGlynnResult) > 1) { linearEquationSolver.performMatrixVectorMultiplication(uniformizedMatrix, values, nullptr, std::get<0>(foxGlynnResult) - 1, &multiplicationResult); } - std::cout << "vector after initial mult phase:" << std::endl; - for (int i = 0; i < result.size(); ++i) { - std::cout << i << ": " << result[i] << std::endl; - } - // For the indices that fall in between the truncation points, we need to perform the matrix-vector // multiplication, scale and add the result. ValueType weight = 0; - std::function addAndScale = [&weight] (ValueType const& a, ValueType const& b) { std::cout << "computing " << a << " + " << weight << " * " << b << " = " << (a + weight * b) << std::endl; return a + weight * b; }; + std::function addAndScale = [&weight] (ValueType const& a, ValueType const& b) { return a + weight * b; }; for (uint_fast64_t index = startingIteration; index <= std::get<1>(foxGlynnResult); ++index) { linearEquationSolver.performMatrixVectorMultiplication(uniformizedMatrix, values, nullptr, 1, &multiplicationResult); weight = std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)]; - std::cout << "setting weight for index " << index << "(" << (index - std::get<0>(foxGlynnResult)) << ") " << " to " << std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)] << std::endl; storm::utility::vector::applyPointwiseInPlace(result, values, addAndScale); - - std::cout << "values after index: " << index << std::endl; - for (int i = 0; i < values.size(); ++i) { - std::cout << i << ": " << values[i] << std::endl; - } - - std::cout << "result after index: " << index << std::endl; - for (int i = 0; i < result.size(); ++i) { - std::cout << i << ": " << result[i] << std::endl; - } } return result; diff --git a/src/utility/numerical.h b/src/utility/numerical.h index 944dff32d..baf8bd1a2 100644 --- a/src/utility/numerical.h +++ b/src/utility/numerical.h @@ -14,8 +14,6 @@ namespace storm { storm::utility::ConstantsComparator comparator; STORM_LOG_THROW(!comparator.isZero(lambda), storm::exceptions::InvalidArgumentException, "Error in Fox-Glynn algorithm: lambda must not be zero."); - std::cout << "calling Fox-Glynn with " << lambda << ", " << overflow << ", " << underflow << ", " << accuracy << std::endl; - // This code is a modified version of the one in PRISM. According to their implementation, for lambda // smaller than 400, we compute the result using the naive method. if (lambda < 400) { @@ -79,8 +77,6 @@ namespace storm { dkl = 1.0 / (1 - std::exp(-(2.0 / 9.0)*(k * sqrt2 * sqrtLambda + 1.5))); } - std::cout << "k for upper: " << k << std::endl; - // Left hand side of the equation in Corollary 1. rightTruncationPoint = static_cast(std::ceil((m + k * sqrt2 * sqrtLambda + 1.5))); @@ -89,11 +85,8 @@ namespace storm { // Right hand side of the equation in Corollary 2. while ((accuracy / 2.0) < ((bLambda * std::exp(-(k*k / 2.0))) / (k * sqrt2 * sqrtpi))) { - std::cout << "k=" << k << " produces: " << ((bLambda * std::exp(-(k*k / 2.0))) / (k * sqrt2 * sqrtpi)) << std::endl; ++k; } - std::cout << "k=" << k << " produces: " << ((bLambda * std::exp(-(k*k / 2.0))) / (k * sqrt2 * sqrtpi)) << std::endl; - std::cout << "k for lower: " << k << std::endl; // Left hand side of the equation in Corollary 2. leftTruncationPoint = static_cast(std::max(std::trunc(m - k * sqrtLambda - 1.5), storm::utility::zero()));