started to implement a validation that checks whether parameter lifting is sound

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 */

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