From f2294fadb0f211ff93b4cf33808cfcb52990370e Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 27 Jun 2017 16:08:02 +0200
Subject: [PATCH] fixed compiling storm-pars cli and improved output a little

---
 src/storm-pars-cli/storm-pars.cpp                   |  4 ++--
 ...ValidatingSparseParameterLiftingModelChecker.cpp |  2 +-
 .../modelchecker/results/RegionCheckResult.cpp      | 13 +++++++++----
 3 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 6fb83ad26..eba86792d 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -137,7 +137,7 @@ namespace storm {
         template<typename ValueType>
         void printInitialStatesResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) {
             if (result) {
-                STORM_PRINT_AND_LOG("Result (initial states): ");
+                STORM_PRINT_AND_LOG("Result (initial states): " << std::endl);
                 
                 auto const* regionCheckResult = dynamic_cast<storm::modelchecker::RegionCheckResult<ValueType> const*>(result.get());
                 if (regionCheckResult != nullptr) {
@@ -184,7 +184,7 @@ namespace storm {
             verifyProperties<ValueType>(input.properties,
                                         [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
                                             std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
-                                            result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(simplificationResult.first->getInitialStates()));
+                                            result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
                                             return result;
                                         },
                                         [&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
index 447bcd27e..d3dabab63 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
@@ -18,7 +18,7 @@ namespace storm {
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
         ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::~ValidatingSparseParameterLiftingModelChecker() {
             if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
-                STORM_PRINT_AND_LOG("Validating Parameter Lifting Model Checker detected " << numOfWrongRegions << " regions where the imprecise method was wrong.");
+                STORM_PRINT_AND_LOG("Validating Parameter Lifting Model Checker detected " << numOfWrongRegions << " regions where the imprecise method was wrong." << std::endl);
             }
         }
         
diff --git a/src/storm-pars/modelchecker/results/RegionCheckResult.cpp b/src/storm-pars/modelchecker/results/RegionCheckResult.cpp
index b561a67ab..2759034e9 100644
--- a/src/storm-pars/modelchecker/results/RegionCheckResult.cpp
+++ b/src/storm-pars/modelchecker/results/RegionCheckResult.cpp
@@ -59,16 +59,19 @@ namespace storm {
             for (auto const& res : this->regionResults) {
                 out << res.first.toString() << ": \t" << res.second << std::endl;
             }
+            return out;
         }
         
         template<typename ValueType>
         std::ostream& RegionCheckResult<ValueType>::writeCondensedToStream(std::ostream& out) const {
+            double satPercent = storm::utility::convertNumber<double>(satFraction) * 100.0;
+            double unsatPercent = storm::utility::convertNumber<double>(unsatFraction) * 100.0;
             auto oneHundred = storm::utility::convertNumber<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>(100.0);
             auto one = storm::utility::convertNumber<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>(1.0);
-            out << "Fraction of satisfied area:   " << (satFraction * oneHundred) << std::endl;
-            out << "Fraction of unsatisfied area: " << (unsatFraction * oneHundred) << std::endl;
-            out << "Unknown fraction:             " << ((one - satFraction - unsatFraction) * oneHundred) << std::endl;
-            out << "Total Number of regions:      " << regionResults.size() << std::endl;
+            out << "  Fraction of satisfied area: " << satPercent << "%" << std::endl;
+            out << "Fraction of unsatisfied area: " << unsatPercent << "%" << std::endl;
+            out << "            Unknown fraction: " << (100.0 - satPercent - unsatPercent) << "%" << std::endl;
+            out << "     Total number of regions: " << regionResults.size() << std::endl;
             std::map<storm::modelchecker::RegionResult, uint_fast64_t> counters;
             for (auto const& res : this->regionResults) {
                 ++counters[res.second];
@@ -76,11 +79,13 @@ namespace storm {
             for (auto const& counter : counters) {
                 out << std::setw(28) << counter.first << ": " << counter.second << std::endl;
             }
+            return out;
         }
 
         template<typename ValueType>
         std::ostream& RegionCheckResult<ValueType>::writeIllustrationToStream(std::ostream& out) const {
             STORM_LOG_WARN("Writing illustration of region check result to a stream is not implemented.");
+            return out;
         }
   
         template<typename ValueType>