diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index 1a5bcee4a..4108667d1 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -281,6 +281,25 @@ namespace storm { template DeterministicSchedsParetoExplorer::DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) { + if (storm::settings::getModule().isShowStatisticsSet()) { + std::string modelname = "original-model"; + std::vector models; + models.push_back(&preprocessorResult.originalModel); + models.push_back(model.get()); + for (SparseModelType const* m : models) { + STORM_PRINT_AND_LOG("#STATS " << m->getNumberOfStates() << " states in " << modelname << std::endl); + STORM_PRINT_AND_LOG("#STATS " << m->getNumberOfChoices() << " choices in " << modelname << std::endl); + STORM_PRINT_AND_LOG("#STATS " << m->getNumberOfTransitions() << " transitions in " << modelname << std::endl); + storm::RationalNumber numScheds = storm::utility::one(); + for (uint64_t state = 0; state < m->getNumberOfStates(); ++state) { + storm::RationalNumber numChoices = storm::utility::convertNumber(m->getNumberOfChoices()); + numScheds *= storm::utility::max(storm::utility::one(), numChoices); + } + STORM_PRINT_AND_LOG("#STATS " << numScheds << " memoryless deterministic schedulers in " << modelname << std::endl); + + modelname = "unfolded-model"; + } + } originalModelInitialState = *preprocessorResult.originalModel.getInitialStates().begin(); objectiveHelper.reserve(objectives.size()); for (auto const& obj : objectives) {