made cli output respect filters

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);
             }
         }
         

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;
 

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);
-            }
-            template<typename ValueType>
-            QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const {
-                return static_cast<QuantitativeCheckResult<ValueType> const&>(*this);
-            }
+            QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult();
             
+            template<typename ValueType>
+            QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const;
 
             ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const;