From a0b7eea500e8caac42a60958929b0c45ac889b57 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 23 Jul 2019 17:04:42 +0200
Subject: [PATCH] DetScheds: Print model statistics.

---
 .../DeterministicSchedsParetoExplorer.cpp     | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

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 <class SparseModelType, typename GeometryValueType>
             DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) {
+                if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+                    std::string modelname = "original-model";
+                    std::vector<SparseModelType const*> 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<storm::RationalNumber>();
+                        for (uint64_t state = 0; state < m->getNumberOfStates(); ++state) {
+                            storm::RationalNumber numChoices = storm::utility::convertNumber<storm::RationalNumber, uint64_t>(m->getNumberOfChoices());
+                            numScheds *= storm::utility::max(storm::utility::one<storm::RationalNumber>(), 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) {