started with instantiation model checker

src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp

@@ -0,0 +1,34 @@
+#include "SparseDtmcInstantiationModelChecker.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace parametric {
+            
+            template <typename SparseModelType, typename ConstantType>
+            SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel) {
+                //Intentionally left empty
+            }
+    
+            template <typename SparseModelType, typename ConstantType>
+            bool SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::canHandle(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
+                storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> mc(this->parametricModel);
+                return mc.canHandle(checkTask);
+            }
+    
+            template <typename SparseModelType, typename ConstantType>
+            std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
+                auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+                storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> mc(instantiatedModel);
+                
+                // todo check whether the model checker supports hints on the specified property and if this is the case,
+                
+                return mc.check(*this->currentCheckTask);
+            }
+            
+    
+        }
+    }
+}

src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h

@@ -1,37 +1,32 @@
 #pragma once
 
-#include "storm/logic/Formulas.h"
-#include "storm/modelchecker/CheckTask.h"
-#include "storm/modelchecker/results/CheckResult.h"
-#include "storm/utility/parametric.h"
+#include <memory>
+
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h"
+#include "storm/utility/ModelInstantiator.h"
 
 namespace storm {
     namespace modelchecker {
         namespace parametric {
-            template <typename SparseModelType, typename ConstantType>
-            
             
             /*!
-             * Class to efficiently check a formula on a parametric model on different parameter instantiations
+             * Class to efficiently check a formula on a parametric model with different parameter instantiations
              */
-            class SparseInstantiationModelChecker {
+            template <typename SparseModelType, typename ConstantType>
+            class SparseDtmcInstantiationModelChecker : public SparseInstantiationModelChecker<SparseModelType, ConstantType> {
             public:
-                SparseInstantiationModelChecker(SparseModelType const& parametricModel);
+                SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel);
                 
-                virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) = 0;
+                virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
                 
-                virtual void specifyFormula(CheckTask<storm::logic::Formula, ValueType> const& checkTask) = 0;
+                virtual void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
                 
-                virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
+                virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
 
-            private:
-                
-                SparseModelType const& parametricModel;
-                
+            protected:
+                storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Dtmc<ConstantType>> modelInstantiator;
             };
         }
     }
 }
-
-
-#endif //STORM_SPARSEINSTANTIATIONMODELCHECKER_H

src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp

@@ -1,5 +1,26 @@
-//
-// Created by Tim Quatmann on 23/02/2017.
-//
-
 #include "SparseInstantiationModelChecker.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace parametric {
+            
+            template <typename SparseModelType, typename ConstantType>
+            SparseInstantiationModelChecker<SparseModelType, ConstantType>::SparseInstantiationModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) {
+                //Intentionally left empty
+            }
+            
+                
+            template <typename SparseModelType, typename ConstantType>
+            void SparseInstantiationModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+                storm::logic::Formula const& formula = checkTask.getFormula();
+                STORM_LOG_THROW(this->canHandle(checkTask), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
+                
+                currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.getFormula(), checkTask.isOnlyInitialStatesRelevantSet());
+                currentCheckTask->setProduceSchedulers(checkTask.isProduceSchedulersSet());
+            }
+            
+        }
+    }
+}

src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h

@@ -1,16 +1,34 @@
-//
-// Created by Tim Quatmann on 23/02/2017.
-//
-
-#ifndef STORM_SPARSEINSTANTIATIONMODELCHECKER_H
-#define STORM_SPARSEINSTANTIATIONMODELCHECKER_H
-
-
-
-class SparseInstantiationModelChecker {
-
-};
-
-
-
-#endif //STORM_SPARSEINSTANTIATIONMODELCHECKER_H
+#pragma once
+
+#include "storm/logic/Formulas.h"
+#include "storm/modelchecker/CheckTask.h"
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/utility/parametric.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace parametric {
+            
+            /*!
+             * Class to efficiently check a formula on a parametric model with different parameter instantiations
+             */
+            template <typename SparseModelType, typename ConstantType>
+            class SparseInstantiationModelChecker {
+            public:
+                SparseInstantiationModelChecker(SparseModelType const& parametricModel);
+                
+                virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const = 0;
+                
+                void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
+                
+                virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
+
+            protected:
+                
+                SparseModelType const& parametricModel;
+                std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
+
+            };
+        }
+    }
+}

src/storm/utility/ModelInstantiator.cpp

@@ -132,7 +132,7 @@ namespace storm {
             }
             
             template<typename ParametricSparseModelType, typename ConstantSparseModelType>
-            ConstantSparseModelType const& ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::instantiate(std::map<VariableType, CoefficientType>const& valuation){
+            ConstantSparseModelType const& ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType>::instantiate(storm::utility::parametric::Valuation<ParametricType> const& valuation){
                 //Write results into the placeholders
                 for(auto& functionResult : this->functions){
                     functionResult.second=storm::utility::convertNumber<ConstantType>(

src/storm/utility/ModelInstantiator.h

@@ -53,7 +53,7 @@ namespace storm {
                  * @param valuation Maps each occurring variables to the value with which it should be substituted
                  * @return The instantiated model
                  */
-                ConstantSparseModelType const& instantiate(std::map<VariableType, CoefficientType>const& valuation);
+                ConstantSparseModelType const& instantiate(storm::utility::parametric::Valuation<ParametricType> const& valuation);
                 
                 /*!
                  *  Check validity

src/storm/utility/parametric.cpp

@@ -25,7 +25,7 @@ namespace storm {
             
 #ifdef STORM_HAVE_CARL
             template<>
-            typename CoefficientType<storm::RationalFunction>::type evaluate<storm::RationalFunction>(storm::RationalFunction const& function, std::map<typename VariableType<storm::RationalFunction>::type, typename CoefficientType<storm::RationalFunction>::type> const& valuation){
+            typename CoefficientType<storm::RationalFunction>::type evaluate<storm::RationalFunction>(storm::RationalFunction const& function, Valuation<storm::RationalFunction> const& valuation){
                 return function.evaluate(valuation);
             }
             

src/storm/utility/parametric.h

@@ -1,10 +1,3 @@
-//
-//  parametric.h
-//
-//  Created by Tim Quatmann on 08/03/16.
-//
-//
-
 #ifndef STORM_UTILITY_PARAMETRIC_H
 #define STORM_UTILITY_PARAMETRIC_H
 
@@ -21,6 +14,7 @@ namespace storm {
              */
             template<typename FunctionType>
             struct VariableType { typedef void type; };
+            
             /*!
              * Acess the type of coefficients from a given function type
              */
@@ -33,12 +27,14 @@ namespace storm {
             template<>
             struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; };
 #endif
-            
+
+            template<typename FunctionType> using Valuation = std::map<typename VariableType<FunctionType>::type, typename CoefficientType<FunctionType>::type>;
+
             /*!
              * Evaluates the given function wrt. the given valuation
              */
             template<typename FunctionType>
-            typename CoefficientType<FunctionType>::type evaluate(FunctionType const& function, std::map<typename VariableType<FunctionType>::type, typename CoefficientType<FunctionType>::type> const& valuation);
+            typename CoefficientType<FunctionType>::type evaluate(FunctionType const& function, Valuation<FunctionType> const& valuation);
             
             /*!
              * Retrieves the constant part of the given function.