From 15b61b6d0fb2aef360303f0ba6f93bef27f5ddd0 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 12 Jun 2017 12:09:34 +0200
Subject: [PATCH] Fixed missing return statement for
 continuousToDiscreteTimeModelTransformer

---
 .../ContinuousToDiscreteTimeModelTransformer.cpp      | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
index b27dc9524..0a1c03e4b 100644
--- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
+++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
@@ -10,6 +10,7 @@
 #include "storm/utility/vector.h"
 
 #include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace transformer {
@@ -32,16 +33,18 @@ namespace storm {
                 SparseCtmcToSparseDtmcTransformer<ValueType, RewardModelType> transformer;
                 if (transformer.transformationPreservesProperty(*formula)) {
                     STORM_LOG_INFO("Transforming Ctmc to embedded Dtmc...");
-                    markovModel = transformer.translate(*markovModel->template as<storm::models::sparse::Ctmc<ValueType>>(), timeRewardModelName);
+                    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...");
-                    markovModel = transformer.translate(*markovModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(), timeRewardModelName);
+                    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 markovModel;
+            return nullptr;
         }
         
        template <typename ValueType, typename RewardModelType>
@@ -70,6 +73,8 @@ namespace storm {
                     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.");
             }
         }