Made some adaptions to make parametric model checking work in the main executable.

Former-commit-id: 0f56bec3e2

src/adapters/CarlAdapter.h

@@ -1,12 +1,10 @@
-/**
- * @file:   extendedCarl.h
- * @author: Sebastian Junges
- *
- * @since March 18, 2014
- */
+#ifndef STORM_ADAPTERS_CARLADAPTER_H_
+#define STORM_ADAPTERS_CARLADAPTER_H_
 
-#ifndef STORM_ADAPTERS_EXTENDEDCARL_H_
-#define STORM_ADAPTERS_EXTENDEDCARL_H_
+// Include config to know whether CARL is available or not.
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_CARL
 
 #include <cln/cln.h>
 #include <carl/core/MultivariatePolynomial.h>
@@ -15,29 +13,35 @@
 #include <carl/core/Constraint.h>
 #include <carl/core/FactorizedPolynomial.h>
 
-namespace carl
-{
+namespace carl {
+    // Define hash values for all polynomials and rational function.
     template<typename C, typename O, typename P>
-    inline size_t hash_value(carl::MultivariatePolynomial<C,O,P> const& p)
-    {
+    inline size_t hash_value(carl::MultivariatePolynomial<C,O,P> const& p) {
         std::hash<carl::MultivariatePolynomial<C,O,P>> h;
         return h(p);
     }
     
     template<typename Pol>
-    inline size_t hash_value(carl::RationalFunction<Pol> const& f)
-    {
-        std::hash<Pol> h;
-        return h(f.nominator()) ^ h(f.denominator());
+    inline size_t hash_value(carl::FactorizedPolynomial<Pol> const& p) {
+        std::hash<FactorizedPolynomial<Pol>> h;
+        return h(p);
     }
 
     template<typename Pol>
-    inline size_t hash_value(carl::FactorizedPolynomial<Pol> const& p)
-    {
-        std::hash<FactorizedPolynomial<Pol>> h;
-        return h(p);
+    inline size_t hash_value(carl::RationalFunction<Pol> const& f)  {
+        std::hash<Pol> h;
+        return h(f.nominator()) ^ h(f.denominator());
     }
 }
 
+namespace storm {
+	typedef carl::Variable  Variable;
+    typedef carl::MultivariatePolynomial<cln::cl_RA> RawPolynomial;
+    typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
+	typedef carl::CompareRelation CompareRelation;
+	typedef carl::RationalFunction<Polynomial> RationalFunction;
+}
 
 #endif
+
+#endif /* STORM_ADAPTERS_CARLADAPTER_H_ */

src/modelchecker/propositional/SparsePropositionalModelChecker.cpp

@@ -1,7 +1,6 @@
 #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
 
-#include "storm-config.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 
 #include "src/models/Dtmc.h"
 #include "src/models/Mdp.h"
@@ -54,7 +53,7 @@ namespace storm {
         template storm::models::Mdp<double> const& SparsePropositionalModelChecker<double>::getModelAs() const;
         template class SparsePropositionalModelChecker<double>;
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template storm::models::Dtmc<storm::RationalFunction> const& SparsePropositionalModelChecker<storm::RationalFunction>::getModelAs() const;
         template storm::models::Mdp<storm::RationalFunction> const& SparsePropositionalModelChecker<storm::RationalFunction>::getModelAs() const;
         template class SparsePropositionalModelChecker<storm::RationalFunction>;

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -3,9 +3,7 @@
 #include <algorithm>
 #include <chrono>
 
-#ifdef PARAMETRIC_SYSTEMS
-#include "src/storage/parameters.h"
-#endif
+#include "src/adapters/CarlAdapter.h"
 
 #include "src/storage/StronglyConnectedComponentDecomposition.h"
 
@@ -1021,8 +1019,8 @@ namespace storm {
         
         template class SparseDtmcEliminationModelChecker<double>;
         
-#ifdef PARAMETRIC_SYSTEMS
-        template class SparseDtmcEliminationModelChecker<RationalFunction>;
+#ifdef STORM_HAVE_CARL
+        template class SparseDtmcEliminationModelChecker<storm::RationalFunction>;
 #endif
     } // namespace modelchecker
 } // namespace storm

src/modelchecker/results/CheckResult.cpp

@@ -1,7 +1,7 @@
 #include "src/modelchecker/results/CheckResult.h"
 
 #include "storm-config.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
@@ -90,7 +90,7 @@ namespace storm {
         template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template QuantitativeCheckResult<storm::RationalFunction>& CheckResult::asQuantitativeCheckResult();
         template QuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asQuantitativeCheckResult() const;
         template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();

src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -4,10 +4,7 @@
 #include "src/storage/BitVector.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
-
-// Include the configuration to check whether rational functions are available.
-#include "storm-config.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace modelchecker {
@@ -231,7 +228,7 @@ namespace storm {
         
         template class ExplicitQuantitativeCheckResult<double>;
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template class ExplicitQuantitativeCheckResult<storm::RationalFunction>;
 #endif
     }

src/modelchecker/results/QuantitativeCheckResult.cpp

@@ -1,7 +1,7 @@
 #include "src/modelchecker/results/QuantitativeCheckResult.h"
 
 #include "storm-config.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
@@ -15,7 +15,7 @@ namespace storm {
         
         template class QuantitativeCheckResult<double>;
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template class QuantitativeCheckResult<storm::RationalFunction>;
 #endif
     }

src/settings/modules/GeneralSettings.cpp

@@ -41,6 +41,7 @@ namespace storm {
             const std::string GeneralSettings::statisticsOptionShortName = "stats";
             const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
             const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
+            const std::string GeneralSettings::parametricOptionName = "parametric";
 
             GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
@@ -84,6 +85,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to use the parametric engine.").build());
             }
             
             bool GeneralSettings::isHelpSet() const {
@@ -239,6 +241,14 @@ namespace storm {
                 return this->getOption(statisticsOptionName).getHasOptionBeenSet();
             }
             
+            bool GeneralSettings::isBisimulationSet() const {
+                return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
+            }
+            
+            bool GeneralSettings::isParametricSet() const {
+                return this->getOption(parametricOptionName).getHasOptionBeenSet();
+            }
+
             bool GeneralSettings::check() const {
                 // Ensure that the model was given either symbolically or explicitly.
                 STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both.");
@@ -250,10 +260,6 @@ namespace storm {
                 return true;
             }
             
-            bool GeneralSettings::isBisimulationSet() const {
-                return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
-            }
-            
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/settings/modules/GeneralSettings.h

@@ -286,6 +286,13 @@ namespace storm {
                  */
                 bool isBisimulationSet() const;
                 
+                /*!
+                 * Retrieves whether the option enabling parametric model checking is set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isParametricSet() const;
+                
                 bool check() const override;
 
                 // The name of the module.
@@ -325,6 +332,7 @@ namespace storm {
                 static const std::string statisticsOptionShortName;
                 static const std::string bisimulationOptionName;
                 static const std::string bisimulationOptionShortName;
+                static const std::string parametricOptionName;
             };
             
         } // namespace modules

src/storage/DeterministicModelBisimulationDecomposition.cpp

@@ -6,7 +6,7 @@
 #include <iomanip>
 #include <boost/iterator/transform_iterator.hpp>
 
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 
@@ -1488,7 +1488,7 @@ namespace storm {
         
         template class DeterministicModelBisimulationDecomposition<double>;
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template class DeterministicModelBisimulationDecomposition<storm::RationalFunction>;
 #endif
     }

src/storage/SparseMatrix.cpp

@@ -8,7 +8,7 @@
 #endif
 
 #include "src/storage/SparseMatrix.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 
 #include "src/exceptions/InvalidStateException.h"
 #include "src/utility/macros.h"
@@ -986,7 +986,7 @@ namespace storm {
         template class SparseMatrixBuilder<int>;
         template class SparseMatrix<int>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
         template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalFunction> const& entry);
         template class SparseMatrixBuilder<RationalFunction>;

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -1,6 +1,6 @@
 #include "src/storage/StronglyConnectedComponentDecomposition.h"
 #include "src/models/AbstractModel.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace storage {
@@ -211,11 +211,9 @@ namespace storm {
         
         // Explicitly instantiate the SCC decomposition.
         template class StronglyConnectedComponentDecomposition<double>;
-        #ifdef PARAMETRIC_SYSTEMS
-        template class StronglyConnectedComponentDecomposition<Polynomial>;
-        template class StronglyConnectedComponentDecomposition<RationalFunction>;
-        #endif
-        
-        
+#ifdef STORM_HAVE_CARL
+        template class StronglyConnectedComponentDecomposition<storm::Polynomial>;
+        template class StronglyConnectedComponentDecomposition<storm::RationalFunction>;
+#endif
     } // namespace storage
 } // namespace storm

src/storage/expressions/ExpressionEvaluator.h

@@ -3,7 +3,7 @@
 
 #include <unordered_map>
 
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 #include "src/storage/expressions/Variable.h"
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/ExprtkExpressionEvaluator.h"

src/storage/expressions/ExpressionEvaluatorBase.cpp

@@ -1,7 +1,7 @@
 #include "src/storage/expressions/ExpressionEvaluatorBase.h"
 
 #include "src/storage/expressions/ExpressionManager.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace expressions {
@@ -17,7 +17,7 @@ namespace storm {
         
         template class ExpressionEvaluatorBase<double>;
 #ifdef STORM_HAVE_CARL
-        template class ExpressionEvaluatorBase<RationalFunction>;
+        template class ExpressionEvaluatorBase<storm::RationalFunction>;
 #endif
     }
 }

src/storage/expressions/ExprtkExpressionEvaluator.cpp

@@ -1,7 +1,7 @@
 #include "src/storage/expressions/ExprtkExpressionEvaluator.h"
 #include "src/storage/expressions/ExpressionManager.h"
 
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 #include "src/utility/macros.h"
 
 namespace storm {

src/storage/expressions/ToRationalFunctionVisitor.h

@@ -1,7 +1,7 @@
 #ifndef STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_
 #define STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_
 
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/Expressions.h"
 #include "src/storage/expressions/ExpressionVisitor.h"

src/utility/ConstantsComparator.cpp

@@ -79,7 +79,7 @@ namespace storm {
             return true;
         }
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template<>
         RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
             return carl::pow(value, exponent);
@@ -182,7 +182,7 @@ namespace storm {
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template class ConstantsComparator<RationalFunction>;
         template class ConstantsComparator<Polynomial>;
 

src/utility/ConstantsComparator.h

@@ -13,12 +13,7 @@
 #include <cstdint>
 
 #include "src/settings/SettingsManager.h"
-
-#include "storm-config.h"
-
-#ifdef PARAMETRIC_SYSTEMS
-#include "src/storage/parameters.h"
-#endif
+#include "src/adapters/CarlAdapter.h"
 
 namespace storm {
     
@@ -81,7 +76,7 @@ namespace storm {
             double precision;
         };
         
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
         template<>
         RationalFunction& simplify(RationalFunction& value);
         

src/utility/PrismUtility.h

@@ -225,7 +225,7 @@ namespace storm {
                                 constantDefinitions[variable] = program.getManager().rational(doubleValue);
                             }
                         } else {
-                            throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << ".";
+                            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: unknown undefined constant " << constantName << ".");
                         }
                     }
                 }

src/utility/cli.h

@@ -274,58 +274,59 @@ namespace storm {
                 }
                 
                 // Customize model-building.
-                typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+                typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
                 if (formula) {
-                    options = storm::builder::ExplicitPrismModelBuilder<double>::Options(*formula.get());
+                    options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
                 }
                 options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
                 
                 // Then, build the model from the symbolic description.
-                result = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
+                result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
                 return result;
             }
             
             template<typename ValueType>
             std::shared_ptr<storm::models::AbstractModel<ValueType>> preprocessModel(std::shared_ptr<storm::models::AbstractModel<ValueType>> model, boost::optional<std::shared_ptr<storm::logic::Formula>> const& formula) {
                 if (storm::settings::generalSettings().isBisimulationSet()) {
-                    STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs.");
-                    std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->template as<storm::models::Dtmc<double>>();
+                    STORM_LOG_THROW(model->getType() == storm::models::DTMC || model->getType() == storm::models::CTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs.");
+                    std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
                     
                     if (dtmc->hasTransitionRewards()) {
                         dtmc->convertTransitionRewardsToStateRewards();
                     }
                     
                     std::cout << "Performing bisimulation minimization... ";
-                    typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+                    typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options;
                     if (formula) {
-                        options = storm::storage::DeterministicModelBisimulationDecomposition<double>::Options(*model, *formula.get());
+                        options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options(*model, *formula.get());
                     }
                     if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
                         options.weak = true;
                         options.bounded = false;
                     }
                     
-                    storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, options);
+                    storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
                     model = bisimulationDecomposition.getQuotient();
                     std::cout << "done." << std::endl << std::endl;
                 }
                 return model;
             }
             
-            void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+            template<typename ValueType>
+            void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::AbstractModel<ValueType>> model, std::shared_ptr<storm::logic::Formula> formula) {
                 if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
                     STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
                     STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
                     
-                    std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
+                    std::shared_ptr<storm::models::Mdp<ValueType>> mdp = model->template as<storm::models::Mdp<ValueType>>();
 
                     // Determine whether we are required to use the MILP-version or the SAT-version.
                     bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet();
 
                     if (useMILP) {
-                        storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formula);
+                        storm::counterexamples::MILPMinimalLabelSetGenerator<ValueType>::computeCounterexample(program, *mdp, formula);
                     } else {
-                        storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula);
+                        storm::counterexamples::SMTMinimalCommandSetGenerator<ValueType>::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula);
                     }
 
                 } else {
@@ -333,12 +334,119 @@ namespace storm {
                 }
             }
             
+            template<>
+            void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
+            }
+            
+            template<typename ValueType>
+            void verifyModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::AbstractModel<ValueType>> model, std::shared_ptr<storm::logic::Formula> formula) {
+                storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
+                
+                // If we were requested to generate a counterexample, we now do so.
+                if (settings.isCounterexampleSet()) {
+                    STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model.");
+                    generateCounterexample<ValueType>(program.get(), model, formula);
+                } else {
+                    std::cout << std::endl << "Model checking property: " << *formula << " ...";
+                    std::unique_ptr<storm::modelchecker::CheckResult> result;
+                    if (model->getType() == storm::models::DTMC) {
+                        std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
+                        storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);
+                        if (modelchecker.canHandle(*formula.get())) {
+                            result = modelchecker.check(*formula.get());
+                        } else {
+                            storm::modelchecker::SparseDtmcPrctlModelChecker<ValueType> modelchecker2(*dtmc);
+                            if (modelchecker2.canHandle(*formula.get())) {
+                                modelchecker2.check(*formula.get());
+                            }
+                        }
+                    } else if (model->getType() == storm::models::MDP) {
+                        std::shared_ptr<storm::models::Mdp<ValueType>> mdp = model->template as<storm::models::Mdp<ValueType>>();
+                        storm::modelchecker::SparseMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
+                        result = modelchecker.check(*formula.get());
+                    }
+                    
+                    if (result) {
+                        std::cout << " done." << std::endl;
+                        std::cout << "Result (initial states): ";
+                        result->writeToStream(std::cout, model->getInitialStates());
+                        std::cout << std::endl << std::endl;
+                    } else {
+                        std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                    }
+                }
+            }
+            
+            template<>
+            void verifyModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
+                storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
+                
+                STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs.");
+                std::shared_ptr<storm::models::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::Dtmc<storm::RationalFunction>>();
+
+                std::cout << std::endl << "Model checking property: " << *formula << " ...";
+                std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+                storm::modelchecker::SparseDtmcEliminationModelChecker<storm::RationalFunction> modelchecker(*dtmc);
+                if (modelchecker.canHandle(*formula.get())) {
+                    result = modelchecker.check(*formula.get());
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property.");
+                }
+
+                if (result) {
+                    std::cout << " done." << std::endl;
+                    std::cout << "Result (initial states): ";
+                    result->writeToStream(std::cout, model->getInitialStates());
+                    std::cout << std::endl << std::endl;
+                } else {
+                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                }
+            }
+            
+            template<typename ValueType>
+            void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
+                // Now we are ready to actually build the model.
+                STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed.");
+                std::shared_ptr<storm::models::AbstractModel<ValueType>> model = buildSymbolicModel<ValueType>(program.get(), formula);
+                
+                // Preprocess the model if needed.
+                model = preprocessModel<ValueType>(model, formula);
+
+                // Print some information about the model.
+                model->printModelInformationToStream(std::cout);
+
+                // Verify the model, if a formula was given.
+                if (formula) {
+                    verifyModel<ValueType>(program, model, formula.get());
+                }
+            }
+            
+            template<typename ValueType>
+            void buildAndCheckExplicitModel(boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
+                storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
+
+                STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
+                std::shared_ptr<storm::models::AbstractModel<ValueType>> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>());
+                
+                // Preprocess the model if needed.
+                model = preprocessModel<ValueType>(model, formula);
+                
+                // Print some information about the model.
+                model->printModelInformationToStream(std::cout);
+                
+                // Verify the model, if a formula was given.
+                if (formula) {
+                    verifyModel<ValueType>(boost::optional<storm::prism::Program>(), model, formula.get());
+                }
+            }
+            
             void processOptions() {
                 if (storm::settings::debugSettings().isLogfileSet()) {
                     initializeFileLogging();
                 }
                 
-                std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now();
                 storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
                 
                 // If we have to build the model from a symbolic representation, we need to parse the representation first.
@@ -360,82 +468,16 @@ namespace storm {
                     }
                 }
                 
-                // Now we are ready to actually build the model.
-                std::chrono::high_resolution_clock::time_point buildingTimeStart = std::chrono::high_resolution_clock::now();
-                std::shared_ptr<storm::models::AbstractModel<double>> model;
-                if (settings.isExplicitSet()) {
-                    model = buildExplicitModel<double>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>());
-                } else if (settings.isSymbolicSet()) {
-                    STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed.");
-                    model = buildSymbolicModel<double>(program.get(), formula);
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
-                }
-                std::chrono::high_resolution_clock::time_point buildingTimeEnd = std::chrono::high_resolution_clock::now();
-
-                // Now, we can do the preprocessing on the model, if it was requested.
-                std::chrono::high_resolution_clock::time_point preprocessingTimeStart = std::chrono::high_resolution_clock::now();
-                model = preprocessModel(model, formula);
-                std::chrono::high_resolution_clock::time_point preprocessingTimeEnd = std::chrono::high_resolution_clock::now();
-
-                // Print some information about the model.
-                model->printModelInformationToStream(std::cout);
-                
-                std::chrono::high_resolution_clock::time_point checkingTimeStart = std::chrono::high_resolution_clock::now();
-                // If we were requested to generate a counterexample, we now do so.
-                if (settings.isCounterexampleSet()) {
-                    STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");
-                    STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model.");
-                    generateCounterexample(program.get(), model, formula.get());
-                } else if (formula) {
-                    std::cout << std::endl << "Model checking property: " << *formula.get() << " ...";
-                    std::unique_ptr<storm::modelchecker::CheckResult> result;
-                    if (model->getType() == storm::models::DTMC) {
-                        std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->as<storm::models::Dtmc<double>>();
-                        storm::modelchecker::SparseDtmcEliminationModelChecker<double> modelchecker(*dtmc);
-                        if (modelchecker.canHandle(*formula.get())) {
-                            result = modelchecker.check(*formula.get());
+                if (settings.isSymbolicSet()) {
+                    if (settings.isParametricSet()) {
+                        buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
                     } else {
-                            storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker2(*dtmc);
-                            if (modelchecker2.canHandle(*formula.get())) {
-                                modelchecker2.check(*formula.get());
+                        buildAndCheckSymbolicModel<double>(program.get(), formula);
                     }
-                        }
-                    } else if (model->getType() == storm::models::MDP) {
-                        std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
-                        storm::modelchecker::SparseMdpPrctlModelChecker<double> modelchecker(*mdp);
-                        result = modelchecker.check(*formula.get());
-                    }
-                    if (result) {
-                        std::cout << " done." << std::endl;
-                        std::cout << "Result (initial states): ";
-                        result->writeToStream(std::cout, model->getInitialStates());
-                        std::cout << std::endl << std::endl;
+                } else if (settings.isExplicitSet()) {
+                    buildAndCheckExplicitModel<double>(formula);
                 } else {
-                        std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
-                    }
-                }
-                std::chrono::high_resolution_clock::time_point checkingTimeEnd = std::chrono::high_resolution_clock::now();
-                std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now();
-
-                if (storm::settings::generalSettings().isShowStatisticsSet()) {
-                    std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart;
-                    std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime);
-                    std::chrono::high_resolution_clock::duration buildingTime = buildingTimeEnd - buildingTimeStart;
-                    std::chrono::milliseconds buildingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(buildingTime);
-                    std::chrono::high_resolution_clock::duration preprocessingTime = preprocessingTimeEnd - preprocessingTimeStart;
-                    std::chrono::milliseconds preprocessingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(preprocessingTime);
-                    std::chrono::high_resolution_clock::duration checkingTime = checkingTimeEnd - checkingTimeStart;
-                    std::chrono::milliseconds checkingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(checkingTime);
-                    
-                    STORM_PRINT_AND_LOG(std::endl);
-                    STORM_PRINT_AND_LOG("Time breakdown:" << std::endl);
-                    STORM_PRINT_AND_LOG("    * time for building: " << buildingTimeInMilliseconds.count() << "ms" << std::endl);
-                    STORM_PRINT_AND_LOG("    * time for preprocessing: " << preprocessingTimeInMilliseconds.count() << "ms" << std::endl);
-                    STORM_PRINT_AND_LOG("    * time for checking: " << checkingTimeInMilliseconds.count() << "ms" << std::endl);
-                    STORM_PRINT_AND_LOG("------------------------------------------" << std::endl);
-                    STORM_PRINT_AND_LOG("    * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl);
-                    STORM_PRINT_AND_LOG(std::endl);
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
                 }
             }
         }