diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 527bb07e0..85a08ea96 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -32,11 +32,6 @@ namespace storm { storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); - STORM_LOG_DEBUG("clippedStatesOfCoalition" << clippedStatesOfCoalition); - - //clippedStatesOfCoalition.complement(); - //STORM_LOG_DEBUG("clippedStatesOfCoalition" << clippedStatesOfCoalition); - if(!relevantStates.empty()) { // Reduce the matrix to relevant states. storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); @@ -57,11 +52,9 @@ namespace storm { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); } } - // Fill up the result vector with the values of x for the relevant states, with 1s for psi states (0 is default) storm::utility::vector::setVectorValues(result, relevantStates, x); storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); - STORM_LOG_DEBUG(result); return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } @@ -91,7 +84,6 @@ namespace storm { // The psiStates are flipped, then the true U part is calculated, at the end the result is flipped again. storm::storage::BitVector notPsiStates = ~psiStates; statesOfCoalition.complement(); - STORM_LOG_DEBUG(statesOfCoalition); auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); for (auto& element : result.values) { @@ -100,7 +92,6 @@ namespace storm { for (auto& element : result.choiceValues) { element = storm::utility::one() - element; } - STORM_LOG_DEBUG(result.values); return result; } @@ -112,7 +103,6 @@ namespace storm { std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(allStates, psiStates); std::vector choiceValues = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); statesOfCoalition.complement(); - STORM_LOG_DEBUG(statesOfCoalition); if (produceScheduler) { STORM_LOG_WARN("Next formula does not expect that produceScheduler is set to true."); @@ -123,7 +113,6 @@ namespace storm { if (goal.isShieldingTask()) { choiceValues = b; } - STORM_LOG_DEBUG(result); return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(allStates), nullptr, std::move(choiceValues)); } @@ -141,7 +130,6 @@ namespace storm { for (auto& element : result.choiceValues) { element = storm::utility::one() - element; } - STORM_LOG_DEBUG(result.values); return result; } @@ -217,12 +205,10 @@ namespace storm { } storm::utility::vector::setVectorValues(result, relevantStates, x); } - // In bounded-globally formulas we not only to reach a psiState on the path but also want to stay in a set of psiStates in the given step bounds. if(!computeBoundedGlobally){ storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } - STORM_LOG_DEBUG(result); return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 96a2e0c81..4ddadc247 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -127,17 +127,7 @@ namespace storm { } for (uint64_t iter = 0; iter < upperBound; iter++) { if(iter == upperBound - 1) { - STORM_LOG_DEBUG("before multipliing ..."); - STORM_LOG_DEBUG("_x = " << _x); - STORM_LOG_DEBUG("_b = " << _b); - STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); - _multiplier->multiply(env, _x, &_b, constrainedChoiceValues); - STORM_LOG_DEBUG("before multipliing ..."); - STORM_LOG_DEBUG("_x = " << _x); - STORM_LOG_DEBUG("_b = " << _b); - STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); - } performIterationStepUpperBound(env, dir); }