added model transformations to the api

src/storm/api/storm.h

@@ -4,6 +4,7 @@
 #include "storm/api/properties.h"
 #include "storm/api/builder.h"
 #include "storm/api/bisimulation.h"
+#include "storm/api/transformation.h"
 #include "storm/api/verification.h"
 #include "storm/api/counterexamples.h"
 #include "storm/api/export.h"

src/storm/api/transformation.h

@@ -0,0 +1,80 @@
+#pragma once
+
+#include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h"
+#include "storm/transformer/SymbolicToSparseTransformer.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidOperationException.h"
+#include "storm/exceptions/NotSupportedException.h"
+
+namespace storm {
+    namespace api {
+        
+        /*!
+         * Transforms the given continuous model to a discrete time model.
+         * If such a transformation does not preserve one of the given formulas, an error is issued.
+         */
+        template <typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+            
+            storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> transformer;
+            
+            for (auto const& formula : formulas) {
+                STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << ".");
+            }
+            
+            if (model->isOfType(storm::models::ModelType::Ctmc)) {
+                return transformer.transform(*model->template as<storm::models::sparse::Ctmc<ValueType>>());
+            } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                return transformer.transform(*model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported");
+            }
+            return nullptr;
+        }
+
+        /*!
+         * Transforms the given continuous model to a discrete time model IN PLACE.
+         * This means that the input continuous time model is replaced by the new discrete time model.
+         * If such a transformation does not preserve one of the given formulas, an error is issued.
+         */
+        template <typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model<ValueType>&& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+            
+            storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> transformer;
+            
+            for (auto const& formula : formulas) {
+                STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << ".");
+            }
+            
+            if (model.isOfType(storm::models::ModelType::Ctmc)) {
+                transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>()));
+            } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                transformer.transform(std::move(*model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>()));
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported.");
+            }
+            return nullptr;
+            
+        }
+        
+        /*!
+         * Transforms the given symbolic model to a sparse model.
+         */
+        template<storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel) {
+            switch (symbolicModel->getType()) {
+                case storm::models::ModelType::Dtmc:
+                    return storm::transformer::SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>().translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
+                case storm::models::ModelType::Mdp:
+                    return storm::transformer::SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Mdp<Type, ValueType>>());
+                case storm::models::ModelType::Ctmc:
+                    return storm::transformer::SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of symbolic " << symbolicModel->getType() << " to sparse model is not supported.");
+            }
+            return nullptr;
+        }
+        
+    }
+}

src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp

@@ -14,72 +14,10 @@
 
 namespace storm {
     namespace transformer {
-        
-        template <typename ValueType, typename RewardModelType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteModel(std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> markovModel, std::shared_ptr<storm::logic::Formula const>& formula) {
-            boost::optional<std::string> timeRewardModelName;
-            if (formula->isTimeOperatorFormula()) {
-                auto const& timeOpFormula = formula->asTimeOperatorFormula();
-                if (timeOpFormula.getSubformula().isReachabilityTimeFormula()) {
-                    auto reachabilityRewardFormula = std::make_shared<storm::logic::EventuallyFormula>(storm::logic::CloneVisitor().clone(timeOpFormula.getSubformula().asReachabilityTimeFormula().getSubformula()), storm::logic::FormulaContext::Reward);
-                    timeRewardModelName = "time";
-                    // make sure that the reward model name is not already in use
-                    while (markovModel->hasRewardModel(*timeRewardModelName)) *timeRewardModelName += "_";
-                    formula = std::make_shared<storm::logic::RewardOperatorFormula const>(reachabilityRewardFormula, timeRewardModelName, timeOpFormula.getOperatorInformation());
-                }
-            }
-        
-            if (markovModel->isOfType(storm::models::ModelType::Ctmc)) {
-                SparseCtmcToSparseDtmcTransformer<ValueType, RewardModelType> transformer;
-                if (transformer.transformationPreservesProperty(*formula)) {
-                    STORM_LOG_INFO("Transforming Ctmc to embedded Dtmc...");
-                    return transformer.translate(*markovModel->template as<storm::models::sparse::Ctmc<ValueType>>(), timeRewardModelName);
-                }
-            } else if (markovModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                SparseMaToSparseMdpTransformer<ValueType, RewardModelType> transformer;
-                if (transformer.transformationPreservesProperty(*formula)) {
-                    STORM_LOG_INFO("Transforming Markov automaton to embedded Mdp...");
-                    return transformer.translate(*markovModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(), timeRewardModelName);
-                }
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Model type " << markovModel->getType() << " not expected.");
-            }
-            return nullptr;
-        }
-        
-       template <typename ValueType, typename RewardModelType>
-        void transformContinuousToDiscreteModelInPlace(std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>& markovModel, std::shared_ptr<storm::logic::Formula const>& formula) {
-            boost::optional<std::string> timeRewardModelName;
-            if (formula->isTimeOperatorFormula()) {
-                auto const& timeOpFormula = formula->asTimeOperatorFormula();
-                if (timeOpFormula.getSubformula().isReachabilityTimeFormula()) {
-                    auto reachabilityRewardFormula = std::make_shared<storm::logic::EventuallyFormula>(storm::logic::CloneVisitor().clone(timeOpFormula.getSubformula().asReachabilityTimeFormula().getSubformula()), storm::logic::FormulaContext::Reward);
-                    timeRewardModelName = "time";
-                    // make sure that the reward model name is not already in use
-                    while (markovModel->hasRewardModel(*timeRewardModelName)) *timeRewardModelName += "_";
-                    formula = std::make_shared<storm::logic::RewardOperatorFormula const>(reachabilityRewardFormula, timeRewardModelName, timeOpFormula.getOperatorInformation());
-                }
-            }
-        
-            if (markovModel->isOfType(storm::models::ModelType::Ctmc)) {
-                SparseCtmcToSparseDtmcTransformer<ValueType, RewardModelType> transformer;
-                if (transformer.transformationPreservesProperty(*formula)) {
-                    STORM_LOG_INFO("Transforming Ctmc to embedded Dtmc...");
-                    markovModel = transformer.translate(std::move(*markovModel->template as<storm::models::sparse::Ctmc<ValueType>>()), timeRewardModelName);
-                }
-            } else if (markovModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                SparseMaToSparseMdpTransformer<ValueType, RewardModelType> transformer;
-                if (transformer.transformationPreservesProperty(*formula)) {
-                    STORM_LOG_INFO("Transforming Markov automaton to embedded Mdp...");
-                    markovModel = transformer.translate(std::move(*markovModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()), timeRewardModelName);
-                }
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Model type " << markovModel->getType() << " not expected.");
-            }
-        }
+
         
        template <typename ValueType, typename RewardModelType>
-        std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> SparseCtmcToSparseDtmcTransformer<ValueType, RewardModelType>::translate(storm::models::sparse::Ctmc<ValueType, RewardModelType> const& ctmc, boost::optional<std::string> const& timeRewardModelName) {
+        std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::transform(storm::models::sparse::Ctmc<ValueType, RewardModelType> const& ctmc, boost::optional<std::string> const& timeRewardModelName) {
             // Init the dtmc components
             storm::storage::sparse::ModelComponents<ValueType, RewardModelType> dtmcComponents(ctmc.getTransitionMatrix(), ctmc.getStateLabeling(), ctmc.getRewardModels());
             dtmcComponents.choiceLabeling = ctmc.getOptionalChoiceLabeling();
@@ -113,7 +51,7 @@ namespace storm {
         }
        
         template <typename ValueType, typename RewardModelType>
-        std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> SparseCtmcToSparseDtmcTransformer<ValueType, RewardModelType>::translate(storm::models::sparse::Ctmc<ValueType, RewardModelType>&& ctmc, boost::optional<std::string> const& timeRewardModelName) {
+        std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::transform(storm::models::sparse::Ctmc<ValueType, RewardModelType>&& ctmc, boost::optional<std::string> const& timeRewardModelName) {
             // Init the dtmc components
             storm::storage::sparse::ModelComponents<ValueType, RewardModelType> dtmcComponents(std::move(ctmc.getTransitionMatrix()), std::move(ctmc.getStateLabeling()), std::move(ctmc.getRewardModels()));
             dtmcComponents.choiceLabeling = std::move(ctmc.getOptionalChoiceLabeling());
@@ -144,7 +82,7 @@ namespace storm {
         }
        
         template <typename ValueType, typename RewardModelType>
-        bool SparseCtmcToSparseDtmcTransformer<ValueType, RewardModelType>::transformationPreservesProperty(storm::logic::Formula const& formula) {
+        bool ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::preservesFormula(storm::logic::Formula const& formula) {
             storm::logic::FragmentSpecification fragment = storm::logic::propositional();
             fragment.setProbabilityOperatorsAllowed(true);
             fragment.setGloballyFormulasAllowed(true);
@@ -158,7 +96,7 @@ namespace storm {
         
   
         template <typename ValueType, typename RewardModelType>
-        std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> SparseMaToSparseMdpTransformer<ValueType, RewardModelType>::translate(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> const& ma, boost::optional<std::string> const& timeRewardModelName) {
+        std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::transform(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> const& ma, boost::optional<std::string> const& timeRewardModelName) {
             STORM_LOG_THROW(ma.isClosed(), storm::exceptions::InvalidArgumentException, "Transformation of MA to its underlying MDP is only possible for closed MAs");
 
             // Init the mdp components
@@ -195,7 +133,7 @@ namespace storm {
         }
 
         template <typename ValueType, typename RewardModelType>
-        std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> SparseMaToSparseMdpTransformer<ValueType, RewardModelType>::translate(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>&& ma, boost::optional<std::string> const& timeRewardModelName) {
+        std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::transform(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>&& ma, boost::optional<std::string> const& timeRewardModelName) {
             STORM_LOG_THROW(ma.isClosed(), storm::exceptions::InvalidArgumentException, "Transformation of MA to its underlying MDP is only possible for closed MAs");
             std::vector<ValueType>& exitRates = ma.getExitRates();
 
@@ -231,31 +169,8 @@ namespace storm {
             return std::make_shared<storm::models::sparse::Mdp<ValueType, RewardModelType>>(std::move(mdpComponents));
         }
         
-        template <typename ValueType, typename RewardModelType>
-        bool SparseMaToSparseMdpTransformer<ValueType, RewardModelType>::transformationPreservesProperty(storm::logic::Formula const& formula) {
-            storm::logic::FragmentSpecification fragment = storm::logic::propositional();
-            fragment.setProbabilityOperatorsAllowed(true);
-            fragment.setGloballyFormulasAllowed(true);
-            fragment.setReachabilityProbabilityFormulasAllowed(true);
-            fragment.setNextFormulasAllowed(true);
-            fragment.setUntilFormulasAllowed(true);
-            fragment.setRewardOperatorsAllowed(true);
-            fragment.setReachabilityRewardFormulasAllowed(true);
-            
-            return formula.isInFragment(fragment);
-        }
-    
-        template std::shared_ptr<storm::models::sparse::Model<double>> transformContinuousToDiscreteModel(std::shared_ptr<storm::models::sparse::Model<double>> markovModel, std::shared_ptr<storm::logic::Formula const>& formula);
-        template std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> transformContinuousToDiscreteModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> markovModel, std::shared_ptr<storm::logic::Formula const>& formula);
-        template std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> transformContinuousToDiscreteModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> markovModel, std::shared_ptr<storm::logic::Formula const>& formula);
-        template void transformContinuousToDiscreteModelInPlace<double>(std::shared_ptr<storm::models::sparse::Model<double>>& markovModel, std::shared_ptr<storm::logic::Formula const>& formula);
-        template void transformContinuousToDiscreteModelInPlace<storm::RationalNumber>(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>>& markovModel, std::shared_ptr<storm::logic::Formula const>& formula);
-        template void transformContinuousToDiscreteModelInPlace<storm::RationalFunction>(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>>& markovModel, std::shared_ptr<storm::logic::Formula const>& formula);
-        template class SparseCtmcToSparseDtmcTransformer<double>;
-        template class SparseCtmcToSparseDtmcTransformer<storm::RationalNumber>;
-        template class SparseCtmcToSparseDtmcTransformer<storm::RationalFunction>;
-        template class SparseMaToSparseMdpTransformer<double>;
-        template class SparseMaToSparseMdpTransformer<storm::RationalNumber>;
-        template class SparseMaToSparseMdpTransformer<storm::RationalFunction>;
+        template class ContinuousToDiscreteTimeModelTransformer<double>;
+        template class ContinuousToDiscreteTimeModelTransformer<storm::RationalNumber>;
+        template class ContinuousToDiscreteTimeModelTransformer<storm::RationalFunction>;
     }
 }

src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h

@@ -12,41 +12,22 @@
 namespace storm {
     namespace transformer {
 
-        
-        // Transforms the given continuous model to a discrete time model.
-        // If such a transformation does not preserve the given formula, the transformation does not take place and the original model is returned
-        // Moreover, the given formula might be changed (e.g. TimeOperatorFormulas become RewardOperatorFormulas).
-        template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteModel(std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> markovModel, std::shared_ptr<storm::logic::Formula const>& formula);
-        
-        // Transforms the given continuous model to a discrete time model IN PLACE (i.e., the continuous model will be invalidated).
-        // If such a transformation does not preserve the given formula, the transformation does not take place.
-        // Moreover, the given formula might be changed (e.g. TimeOperatorFormulas become RewardOperatorFormulas).
         template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
-        void transformContinuousToDiscreteModelInPlace(std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>& markovModel, std::shared_ptr<storm::logic::Formula const>& formula);
+        class ContinuousToDiscreteTimeModelTransformer {
+
+            // If this method returns true, the given formula is preserced by the transformation
+            static bool preservesFormula(storm::logic::Formula const& formula);
         
-        template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
-        class SparseCtmcToSparseDtmcTransformer {
-        public:
             // Transforms the given CTMC to its underlying (aka embedded) DTMC.
             // A reward model for time is added if a corresponding reward model name is given
-            static std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> translate(storm::models::sparse::Ctmc<ValueType, RewardModelType> const& ctmc, boost::optional<std::string> const& timeRewardModelName = boost::none);
-            static std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> translate(storm::models::sparse::Ctmc<ValueType, RewardModelType>&& ctmc, boost::optional<std::string> const& timeRewardModelName = boost::none);
+            static std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> transform(storm::models::sparse::Ctmc<ValueType, RewardModelType> const& ctmc, boost::optional<std::string> const& timeRewardModelName = boost::none);
+            static std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> transform(storm::models::sparse::Ctmc<ValueType, RewardModelType>&& ctmc, boost::optional<std::string> const& timeRewardModelName = boost::none);
             
-            // If this method returns true, the given formula is preserced by the transformation
-            static bool transformationPreservesProperty(storm::logic::Formula const& formula);
-        };
-        
-        template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
-        class SparseMaToSparseMdpTransformer {
-        public:
             // Transforms the given MA to its underlying (aka embedded) MDP.
             // A reward model for time is added if a corresponding reward model name is given
-            static std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> translate(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> const& ma, boost::optional<std::string> const& timeRewardModelName = boost::none);
-            static std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> translate(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>&& ma, boost::optional<std::string> const& timeRewardModelName = boost::none);
+            static std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> transform(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> const& ma, boost::optional<std::string> const& timeRewardModelName = boost::none);
+            static std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> transform(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>&& ma, boost::optional<std::string> const& timeRewardModelName = boost::none);
             
-            // If this method returns true, the given formula is preserved by the transformation
-            static bool transformationPreservesProperty(storm::logic::Formula const& formula);
         };
     }
 }

src/storm/transformer/SymbolicToSparseTransformer.cpp

@@ -11,22 +11,6 @@
 namespace storm {
     namespace transformer {
 
-        template<storm::dd::DdType Type, typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel) {
-            switch (symbolicModel->getType()) {
-                case storm::models::ModelType::Dtmc:
-                    return SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>().translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
-                case storm::models::ModelType::Mdp:
-                    return SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Mdp<Type, ValueType>>());
-                case storm::models::ModelType::Ctmc:
-                    return SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
-                default:
-                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Transformation of symbolic " << symbolicModel->getType() << " to sparse model is not implemented.");
-            }
-            return nullptr;
-        }
-        
-
         template<storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc) {
             this->odd = symbolicDtmc.getReachableStates().createOdd();
@@ -121,11 +105,6 @@ namespace storm {
             return std::make_shared<storm::models::sparse::Ctmc<ValueType>>(transitionMatrix, labelling, rewardModels);
         }
 
-        template std::shared_ptr<storm::models::sparse::Model<double>> transformSymbolicToSparseModel<storm::dd::DdType::CUDD, double>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> const& symbolicModel);
-        template std::shared_ptr<storm::models::sparse::Model<double>> transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, double>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>> const& symbolicModel);
-        template std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalNumber>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalNumber>> const& symbolicModel);
-        template std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalFunction>(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>> const& symbolicModel);
-        
         template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::CUDD, double>;
         template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, double>;
         template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, storm::RationalNumber>;

src/storm/transformer/SymbolicToSparseTransformer.h

@@ -12,9 +12,6 @@
 namespace storm {
     namespace transformer {
 
-        template<storm::dd::DdType Type, typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel);
-        
         template<storm::dd::DdType Type, typename ValueType>
         class SymbolicDtmcToSparseDtmcTransformer {
         public: