From 64c37d4da1b6d3e711974b1f2861a568d81365a6 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 24 Mar 2017 10:40:05 +0100
Subject: [PATCH] minor fixes for exact validation in parameter lifting

---
 src/storm/modelchecker/parametric/ParameterLifting.cpp    | 8 ++++++--
 .../parametric/SparseDtmcParameterLifting.cpp             | 2 +-
 .../modelchecker/parametric/SparseMdpParameterLifting.cpp | 2 +-
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp
index d0ea5dc08..4db278bba 100644
--- a/src/storm/modelchecker/parametric/ParameterLifting.cpp
+++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp
@@ -17,6 +17,7 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/ParametricSettings.h"
 
 
 namespace storm {
@@ -24,8 +25,7 @@ namespace storm {
         namespace parametric {
 
             ParameterLiftingSettings::ParameterLiftingSettings() {
-                // todo: get this form settings
-                this->applyExactValidation = false;
+                this->applyExactValidation = storm::settings::getModule<storm::settings::modules::ParametricSettings>().isExactValidationSet();
             }
             
             template <typename SparseModelType, typename ConstantType>
@@ -126,20 +126,24 @@ namespace storm {
                 if (numericResult == RegionCheckResult::AllSat) {
                     if(!exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
                         // Numerical result is wrong; Check whether the region is AllViolated!
+                        STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result...");
                         if(!exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
                             parameterLiftingCheckerStopwatch.stop();
                             return RegionCheckResult::AllViolated;
                         } else {
+                            parameterLiftingCheckerStopwatch.stop();
                             return RegionCheckResult::Unknown;
                         }
                     }
                 } else if (numericResult == RegionCheckResult::AllViolated) {
                     if(exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
                         // Numerical result is wrong; Check whether the region is AllSat!
+                        STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result...");
                         if(exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
                             parameterLiftingCheckerStopwatch.stop();
                             return RegionCheckResult::AllSat;
                         } else {
+                            parameterLiftingCheckerStopwatch.stop();
                             return RegionCheckResult::Unknown;
                         }
                     }
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp
index 2ca6ba507..55b1406a8 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp
@@ -33,7 +33,7 @@ namespace storm {
             template <typename SparseModelType, typename ConstantType>
             void SparseDtmcParameterLifting<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
                 if (this->settings.applyExactValidation) {
-                    STORM_LOG_WARN_COND((std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>::value) , "Exact validation is not necessarry if the original computation is already exact");
+                    STORM_LOG_WARN_COND(!(std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>::value) , "Exact validation is not necessarry if the original computation is already exact");
                     this->exactParameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel());
                 }
                 this->parameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp
index 25d222063..001d0d6e4 100644
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp
@@ -33,7 +33,7 @@ namespace storm {
             template <typename SparseModelType, typename ConstantType>
             void SparseMdpParameterLifting<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
                 if (this->settings.applyExactValidation) {
-                    STORM_LOG_WARN_COND((std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact");
+                    STORM_LOG_WARN_COND(!(std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact");
                     this->exactParameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel());
                 }
                 this->parameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());