diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 053d1a4c3..ac237abb1 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -43,16 +43,16 @@ namespace storm { std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); } - STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique."); + STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); for (auto const& state : states) { eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions); } - STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states."); + STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl); } else if (storm::settings::parametricSettings().getEliminationMethod() == storm::settings::modules::ParametricSettings::EliminationMethod::Hybrid) { // When using the hybrid technique, we recursively treat the SCCs up to some size. storm::utility::ConstantsComparator comparator; std::vector entryStateQueue; - STORM_PRINT_AND_LOG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique."); + STORM_PRINT_AND_LOG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, comparator, statePriorities); // If the entry states were to be eliminated last, we need to do so now. @@ -62,7 +62,7 @@ namespace storm { eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions); } } - STORM_PRINT_AND_LOG("Eliminated " << subsystem.size() << " states."); + STORM_PRINT_AND_LOG("Eliminated " << subsystem.size() << " states." << std::endl); } // Finally eliminate initial state. @@ -147,7 +147,6 @@ namespace storm { // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). maybeStates &= reachableStates; - STORM_PRINT_AND_LOG("Found " << maybeStates.getNumberOfSetBits() << " maybe states." << std::endl); // Create a vector for the probabilities to go to a state with probability 1 in one step. std::vector oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);