From 5571e2111c20e3ddbd9d30c12f648592dfb653d9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 7 Oct 2014 16:35:04 +0200 Subject: [PATCH] Changed default maximal SCC size to 20. Removed some debug output. Former-commit-id: 302ca216ec3955c20bcfedaaa46e5af9f77f6af0 --- src/modelchecker/reachability/SparseSccModelChecker.cpp | 6 ------ src/settings/modules/ParametricSettings.cpp | 2 +- 2 files changed, 1 insertion(+), 7 deletions(-) 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 {