Browse Source

Changed default maximal SCC size to 20. Removed some debug output.

Former-commit-id: 302ca216ec
tempestpy_adaptions
dehnert 10 years ago
parent
commit
5571e2111c
  1. 6
      src/modelchecker/reachability/SparseSccModelChecker.cpp
  2. 2
      src/settings/modules/ParametricSettings.cpp

6
src/modelchecker/reachability/SparseSccModelChecker.cpp

@ -143,12 +143,6 @@ namespace storm {
auto modelCheckingStart = std::chrono::high_resolution_clock::now(); auto modelCheckingStart = std::chrono::high_resolution_clock::now();
std::vector<storm::storage::sparse::state_type> entryStateQueue; std::vector<storm::storage::sparse::state_type> entryStateQueue;
uint_fast64_t maximalDepth = treatScc(dtmc, flexibleMatrix, oneStepProbabilities, newInitialStates, subsystem, submatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, distances); 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. // 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."); STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step.");

2
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, 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, 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.") 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 { bool ParametricSettings::isEliminateEntryStatesLastSet() const {

Loading…
Cancel
Save