From 88ee0bbf67ed5cc2262afd56adc8739948a74f3e Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 26 Feb 2019 15:11:25 +0100
Subject: [PATCH] RewardUnfolding: If statistics are enabled, Log when an
 acyclic epoch model is found.

---
 .../rewardbounded/MultiDimensionalRewardUnfolding.cpp     | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
index 4d7d1deb4..3b1f36791 100644
--- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
+++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
@@ -7,6 +7,8 @@
 #include "storm/utility/macros.h"
 #include "storm/logic/Formulas.h"
 
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
 #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
@@ -377,6 +379,11 @@ namespace storm {
                     if (!currentEpoch || !epochManager.compareEpochClass(epoch, currentEpoch.get())) {
                         setCurrentEpochClass(epoch);
                         epochModel.epochMatrixChanged = true;
+                        if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+                            if (storm::utility::graph::hasCycle(epochModel.epochMatrix)) {
+                                std::cout << "Epoch model for epoch " << epochManager.toString(epoch) <<  " is cyclic." << std::endl;
+                            }
+                        }
                     } else {
                         epochModel.epochMatrixChanged = false;
                     }
@@ -690,7 +697,6 @@ namespace storm {
                 
                 template<typename ValueType, bool SingleObjectiveMode>
                 ValueType MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getRequiredEpochModelPrecision(Epoch const& startEpoch, ValueType const& precision) {
-                    // if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
                     uint64_t sumOfDimensions = 0;
                     for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
                         sumOfDimensions += epochManager.getDimensionOfEpoch(startEpoch, dim) + 1;