From e3a506ecc6b8d09b9843b6f06224a624983062ef Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 16 Oct 2017 18:36:59 +0200
Subject: [PATCH] Property information output

---
 ...arseMdpRewardBoundedPcaaWeightVectorChecker.cpp | 14 +++++++++-----
 .../prctl/helper/SparseMdpPrctlHelper.cpp          | 11 ++++++-----
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
index 078f87d32..e019a0f88 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
@@ -50,13 +50,17 @@ namespace storm {
                 auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
                 EpochCheckingData cachedData;
                 ValueType precision = storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+                uint64_t epochCount = 0;
+                for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
+                    epochCount += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
+                }
                 if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
-                    uint64_t denom = 0;
-                    for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
-                        denom += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
-                    }
-                    precision = precision / storm::utility::convertNumber<ValueType>(denom);
+                    precision = precision / storm::utility::convertNumber<ValueType>(epochCount);
                 }
+                if (numChecks == 1) {
+                    STORM_PRINT_AND_LOG("Objective/Dimension/Epoch count is: " << 1 << "/" << rewardUnfolding.getEpochManager().getDimensionCount() << "/" <<  epochCount << "."  << std::endl);
+                }
+
 
                 for (auto const& epoch : epochOrder) {
                     computeEpochSolution(epoch, weightVector, cachedData, precision);
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index d924565c0..53d81fbcd 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -91,13 +91,14 @@ namespace storm {
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
 
                 ValueType precision = storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+                uint64_t epochCount = 0;
+                for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
+                    epochCount += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
+                }
                 if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
-                    uint64_t denom = 0;
-                    for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
-                        denom += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
-                    }
-                    precision = precision / storm::utility::convertNumber<ValueType>(denom);
+                    precision = precision / storm::utility::convertNumber<ValueType>(epochCount);
                 }
+                STORM_PRINT_AND_LOG("Objective/Dimension/Epoch count is: " << 1 << "/" << rewardUnfolding.getEpochManager().getDimensionCount() << "/" <<  epochCount << "."  << std::endl);
 
                 for (auto const& epoch : epochOrder) {
                     swBuild.start();