diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 67c1bb805..ea5a1491c 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -739,7 +739,6 @@ namespace storm { static std::vector buildStateRewards(std::vector const& rewards, StateInformation const& stateInformation, expressions::ExpressionEvaluation& eval) { std::vector result(stateInformation.reachableStates.size()); for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { - std::cout << index << ": " << *stateInformation.reachableStates[index] << std::endl; result[index] = ValueType(0); for (auto const& reward : rewards) { // Add this reward to the state if the state is included in the state reward. diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index d239b8b3e..915cfec50 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -161,13 +161,6 @@ namespace storm { // Project the state reward vector to all maybe-states. boost::optional> stateRewards(maybeStates.getNumberOfSetBits()); storm::utility::vector::selectVectorValues(stateRewards.get(), maybeStates, dtmc.getStateRewardVector()); - for (uint_fast64_t i = 0; i < dtmc.getStateRewardVector().size(); ++i) { - std::cout << i << ": " << dtmc.getStateRewardVector()[i] << ", "; - } - std::cout << std::endl; - std::cout << maybeStates << std::endl; - std::cout << psiStates << std::endl; - std::cout << infinityStates << std::endl; // Determine the set of initial states of the sub-DTMC. storm::storage::BitVector newInitialStates = dtmc.getInitialStates() % maybeStates; @@ -516,7 +509,11 @@ namespace storm { } else { // If we are computing rewards, we basically scale the state reward of the state to eliminate and // add the result to the state reward of the predecessor. - stateRewards.get()[predecessor] += storm::utility::simplify(multiplyElement->getValue() * storm::utility::pow(loopProbability, 2) * stateRewards.get()[state]); + if (hasSelfLoop) { + stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * storm::utility::pow(loopProbability, 2) * stateRewards.get()[state]); + } else { + stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * stateRewards.get()[state]); + } } } diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index b09aa4e93..79c18a684 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -640,9 +640,6 @@ namespace storm { // (b) the new labeling, // (c) the new reward structures. - std::cout << model.getTransitionMatrix() << std::endl; - std::cout << model.getLabeledStates("end") << std::endl;; - // Prepare a matrix builder for (a). storm::storage::SparseMatrixBuilder builder(this->size(), this->size()); @@ -742,13 +739,6 @@ namespace storm { // If the model has state rewards, we simply copy the state reward of the representative state, because // all states in a block are guaranteed to have the same state reward. if (keepRewards && model.hasStateRewards()) { - std::cout << "is block absorbing? " << oldBlock.isAbsorbing() << std::endl; - std::cout << "setting reward for block " << blockIndex << " to " << model.getStateRewardVector()[representativeState] << std::endl; - std::cout << "block: " << std::endl; - for (auto element : this->blocks[blockIndex]) { - std::cout << element << ", "; - } - std::cout << std::endl; stateRewards.get()[blockIndex] = model.getStateRewardVector()[representativeState]; } } @@ -761,8 +751,6 @@ namespace storm { // Finally construct the quotient model. this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling), std::move(stateRewards))); - - std::cout << quotient->getTransitionMatrix() << std::endl; } template @@ -1237,8 +1225,6 @@ namespace storm { this->initializeSilentProbabilities(model, partition); } - partition.print(); - return partition; }