From 9ba2f90483a313a2885a483ff3cdaaa09d4ff035 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 4 Apr 2017 18:52:23 +0200
Subject: [PATCH] started to implement a validation that checks whether
 parameter lifting is sound

---
 src/storm/utility/parameterlifting.h | 38 ++++++++++++++++++++++++++++
 src/storm/utility/storm.h            |  3 +++
 2 files changed, 41 insertions(+)
 create mode 100644 src/storm/utility/parameterlifting.h

diff --git a/src/storm/utility/parameterlifting.h b/src/storm/utility/parameterlifting.h
new file mode 100644
index 000000000..f2cf58972
--- /dev/null
+++ b/src/storm/utility/parameterlifting.h
@@ -0,0 +1,38 @@
+#ifndef STORM_UTILITY_PARAMETERLIFTING_H
+#define STORM_UTILITY_PARAMETERLIFTING_H
+
+#include "storm/models/sparse/Model.h"
+#include "storm/utility/parametric.h"
+#include "storm/utility/macros.h"
+#include "storm/logic/Formula.h"
+#include "storm/logic/FragmentSpecification.h"
+
+
+namespace storm {
+    namespace utility {
+        namespace parameterlifting {
+            
+            /*!
+             * Checks whether the parameter lifting approach is sound on the given model with respect to the provided property
+             *
+             * This method is taylored to an efficient but incomplete check, i.e., if false is returned,
+             * parameter lifting might still be applicable. Checking this, however, would be more involved.
+             *
+             * @param model
+             * @param formula
+             * @return true iff it was successfully validated that parameter lifting is sound on the provided model.
+             */
+            template<typename ValueType>
+            static bool validateParameterLiftingSound(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula) {
+                switch (model.getType()) {
+                    default:
+                        return false;
+                }
+            }
+            
+        }
+    }
+}
+
+
+#endif /* STORM_UTILITY_PARAMETERLIFTING_H */
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index a97aa5f06..f9830ff98 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -70,6 +70,7 @@
 #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
 #include "storm/modelchecker/parametric/SparseDtmcParameterLifting.h"
 #include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
+#include "storm/utility/parameterlifting.h"
 
 #include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
 #include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h"
@@ -325,6 +326,8 @@ namespace storm {
         storm::utility::Stopwatch parameterLiftingStopWatch(true);
         std::shared_ptr<storm::logic::Formula const> consideredFormula = formula;
         
+        STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*markovModel, *formula), "Could not validate whether parameter lifting is sound on the input model and the formula " << *formula);
+        
         if (markovModel->isOfType(storm::models::ModelType::Ctmc) || markovModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
             STORM_PRINT_AND_LOG("Transforming continuous model to discrete model...");
             storm::transformer::transformContinuousToDiscreteModelInPlace(markovModel, consideredFormula);