From 6471bfdcea68e60831008fbd1f806358e4a328c8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 4 Jul 2017 11:17:01 +0200
Subject: [PATCH] made cli output respect filters

---
 src/storm/cli/cli.cpp                          |  8 +++++---
 src/storm/modelchecker/results/CheckResult.cpp | 18 ++++++++++++++++++
 src/storm/modelchecker/results/CheckResult.h   | 10 +++-------
 3 files changed, 26 insertions(+), 10 deletions(-)

diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 8fea01e61..10f992d96 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -615,9 +615,11 @@ 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) {
+        void printResult(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): ");
+                std::stringstream ss;
+                ss << "'" << *property.getFilter().getStatesFormula() << "'";
+                STORM_PRINT_AND_LOG("Result (for " << (property.getFilter().getStatesFormula()->isInitialFormula() ? "initial" : ss.str()) << " states): ");
                 printFilteredResult<ValueType>(result, property.getFilter().getFilterType());
                 if (watch) {
                     STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl);
@@ -640,8 +642,8 @@ namespace storm {
                 storm::utility::Stopwatch watch(true);
                 std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula());
                 watch.stop();
-                printInitialStatesResult<ValueType>(result, property, &watch);
                 postprocessingCallback(result);
+                printResult<ValueType>(result, property, &watch);
             }
         }
         
diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp
index bdcf68c8f..9155057d3 100644
--- a/src/storm/modelchecker/results/CheckResult.cpp
+++ b/src/storm/modelchecker/results/CheckResult.cpp
@@ -113,6 +113,15 @@ namespace storm {
             return dynamic_cast<QualitativeCheckResult const&>(*this);
         }
 
+        template<typename ValueType>
+        QuantitativeCheckResult<ValueType>& CheckResult::asQuantitativeCheckResult() {
+            return static_cast<QuantitativeCheckResult<ValueType> &>(*this);
+        }
+        
+        template<typename ValueType>
+        QuantitativeCheckResult<ValueType> const& CheckResult::asQuantitativeCheckResult() const {
+            return static_cast<QuantitativeCheckResult<ValueType> const&>(*this);
+        }
 
         template <storm::dd::DdType Type>
         SymbolicQualitativeCheckResult<Type>& CheckResult::asSymbolicQualitativeCheckResult() {
@@ -155,6 +164,9 @@ namespace storm {
         }
         
         // Explicitly instantiate the template functions.
+        template QuantitativeCheckResult<double>& CheckResult::asQuantitativeCheckResult();
+        template QuantitativeCheckResult<double> const& CheckResult::asQuantitativeCheckResult() const;
+        
         template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
         template ExplicitParetoCurveCheckResult<double>& CheckResult::asExplicitParetoCurveCheckResult();
@@ -184,9 +196,15 @@ namespace storm {
 
 
 #ifdef STORM_HAVE_CARL
+        template QuantitativeCheckResult<storm::RationalNumber>& CheckResult::asQuantitativeCheckResult();
+        template QuantitativeCheckResult<storm::RationalNumber> const& CheckResult::asQuantitativeCheckResult() const;
+        
         template ExplicitQuantitativeCheckResult<storm::RationalNumber>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<storm::RationalNumber> const& CheckResult::asExplicitQuantitativeCheckResult() const;
 
+        template QuantitativeCheckResult<storm::RationalFunction>& CheckResult::asQuantitativeCheckResult();
+        template QuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asQuantitativeCheckResult() const;
+
         template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;
 
diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h
index 2cff249c9..43954a220 100644
--- a/src/storm/modelchecker/results/CheckResult.h
+++ b/src/storm/modelchecker/results/CheckResult.h
@@ -66,14 +66,10 @@ namespace storm {
             QualitativeCheckResult const& asQualitativeCheckResult() const;
 
             template<typename ValueType>
-            QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult() {
-                return static_cast<QuantitativeCheckResult<ValueType> &>(*this);
-            }
+            QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult();
+            
             template<typename ValueType>
-            QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const {
-                return static_cast<QuantitativeCheckResult<ValueType> const&>(*this);
-            }
-
+            QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const;
 
             ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const;