partial (parametric) model instantiators

src/storm-pars/utility/ModelInstantiator.cpp

@@ -137,10 +137,7 @@ namespace storm {
             template<typename ParametricSparseModelType, typename ConstantSparseModelType>
             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>(
-                            storm::utility::parametric::evaluate(functionResult.first, valuation));
-                }
+                instantiate_helper(valuation);
                 
                 //Write the instantiated values to the matrices and vectors according to the stored mappings
                 for(auto& entryValuePair : this->matrixMapping){
@@ -170,6 +167,12 @@ namespace storm {
             template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<storm::RationalNumber>>;
             template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
             template class ModelInstantiator<storm::models::sparse::StochasticTwoPlayerGame<storm::RationalFunction>, storm::models::sparse::StochasticTwoPlayerGame<storm::RationalNumber>>;
+
+            // For stormpy:
+            template class ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<storm::RationalFunction>>;
+            template class ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<storm::RationalFunction>>;
+            template class ModelInstantiator<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::models::sparse::Ctmc<storm::RationalFunction>>;
+            template class ModelInstantiator<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>;
 #endif
     } //namespace utility
 } //namespace storm

src/storm-pars/utility/ModelInstantiator.h

@@ -117,7 +117,29 @@ namespace storm {
                     
                     this->instantiatedModel = std::make_shared<ConstantSparseModelType>(std::move(components));
                 }
-                
+
+                template<typename PMT = ParametricSparseModelType>
+                typename std::enable_if<
+                        std::is_same<PMT,ConstantSparseModelType>::value
+                >::type
+                instantiate_helper(storm::utility::parametric::Valuation<ParametricType> const& valuation) {
+                    for(auto& functionResult : this->functions){
+                        functionResult.second=
+                                storm::utility::parametric::substitute(functionResult.first, valuation);
+                    }
+                }
+
+                template<typename PMT = ParametricSparseModelType>
+                typename std::enable_if<
+                        !std::is_same<PMT,ConstantSparseModelType>::value
+                >::type
+                instantiate_helper(storm::utility::parametric::Valuation<ParametricType> const& valuation) {
+                    for(auto& functionResult : this->functions){
+                        functionResult.second=storm::utility::convertNumber<ConstantType>(
+                                storm::utility::parametric::evaluate(functionResult.first, valuation));
+                    }
+                }
+
                 /*!
                  * Creates a matrix that has entries at the same position as the given matrix.
                  * The returned matrix is a stochastic matrix, i.e., the rows sum up to one.

src/storm-pars/utility/parametric.cpp

@@ -21,7 +21,13 @@ namespace storm {
             typename CoefficientType<storm::RationalFunction>::type evaluate<storm::RationalFunction>(storm::RationalFunction const& function, Valuation<storm::RationalFunction> const& valuation){
                 return function.evaluate(valuation);
             }
-            
+
+            template<>
+            typename storm::RationalFunction substitute<storm::RationalFunction>(storm::RationalFunction const& function, Valuation<storm::RationalFunction> const& valuation){
+                return function.substitute(valuation);
+            }
+
+
             template<>
             void gatherOccurringVariables<storm::RationalFunction>(storm::RationalFunction const& function, std::set<typename VariableType<storm::RationalFunction>::type>& variableSet){
                 function.gatherVariables(variableSet);

src/storm-pars/utility/parametric.h

@@ -35,7 +35,13 @@ namespace storm {
              */
             template<typename FunctionType>
             typename CoefficientType<FunctionType>::type evaluate(FunctionType const& function, Valuation<FunctionType> const& valuation);
-            
+
+            /*!
+             * Evaluates the given function wrt. the given valuation
+             */
+            template<typename FunctionType>
+            FunctionType substitute(FunctionType const& function, Valuation<FunctionType> const& valuation);
+
             /*!
              *  Add all variables that occur in the given function to the the given set
              */