diff --git a/src/storm-pars/utility/ModelInstantiator.cpp b/src/storm-pars/utility/ModelInstantiator.cpp index f59649ab7..719427529 100644 --- a/src/storm-pars/utility/ModelInstantiator.cpp +++ b/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 diff --git a/src/storm-pars/utility/ModelInstantiator.h b/src/storm-pars/utility/ModelInstantiator.h index e96a4dda8..cba624074 100644 --- a/src/storm-pars/utility/ModelInstantiator.h +++ b/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. diff --git a/src/storm-pars/utility/parametric.cpp b/src/storm-pars/utility/parametric.cpp index 3b6934a3e..96c30e78e 100644 --- a/src/storm-pars/utility/parametric.cpp +++ b/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); diff --git a/src/storm-pars/utility/parametric.h b/src/storm-pars/utility/parametric.h index 77a58e7f8..31a81f1a7 100644 --- a/src/storm-pars/utility/parametric.h +++ b/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 */