diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 0f1fb968c..51ba38c64 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -143,12 +143,6 @@ namespace storm { auto modelCheckingStart = std::chrono::high_resolution_clock::now(); std::vector entryStateQueue; uint_fast64_t maximalDepth = treatScc(dtmc, flexibleMatrix, oneStepProbabilities, newInitialStates, subsystem, submatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, distances); - - if (storm::settings::parametricSettings().isEliminateEntryStatesLastSet()) { - for (auto const& state : entryStateQueue) { - std::cout << "state " << state << " has " << flexibleMatrix.getRow(state).size() << " outgoing transitions and " << flexibleBackwardTransitions.getRow(state).size() << " predecessors. " << std::endl; - } - } // If the entry states were to be eliminated last, we need to do so now. STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); diff --git a/src/settings/modules/ParametricSettings.cpp b/src/settings/modules/ParametricSettings.cpp index fb0b87f57..50e7dfa47 100644 --- a/src/settings/modules/ParametricSettings.cpp +++ b/src/settings/modules/ParametricSettings.cpp @@ -15,7 +15,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, sortTrivialSccOptionName, true, "Sets whether the trivial SCCs are to be eliminated in descending order with respect to their distances from the initial state.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.") - .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(50).setIsOptional(true).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build()); } bool ParametricSettings::isEliminateEntryStatesLastSet() const {