From 57490a7947144157775786d66637b741a18a4ec5 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 27 Jun 2017 18:11:18 +0200
Subject: [PATCH] fixed continuous to discrete time transformation

---
 src/storm/api/transformation.h                   |  4 ++--
 .../ContinuousToDiscreteTimeModelTransformer.cpp | 16 ++++++++++++----
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h
index 9f25e37fa..204e283db 100644
--- a/src/storm/api/transformation.h
+++ b/src/storm/api/transformation.h
@@ -48,9 +48,9 @@ namespace storm {
             }
             
             if (model.isOfType(storm::models::ModelType::Ctmc)) {
-                transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>()));
+                return 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>>()));
+                return 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.");
             }
diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
index d083e17c1..20357f400 100644
--- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
+++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
@@ -112,8 +112,12 @@ namespace storm {
             for (auto& rewardModel : mdpComponents.rewardModels) {
                 if (rewardModel.second.hasStateRewards()) {
                     auto& stateRewards = rewardModel.second.getStateRewardVector();
-                    for (auto state : ma.getMarkovianStates()) {
-                        stateRewards[state] /= exitRates[state];
+                    for (uint_fast64_t state = 0; state < stateRewards.size(); ++state) {
+                        if (ma.getMarkovianStates().get(state)) {
+                            stateRewards[state] /= exitRates[state];
+                        } else {
+                            stateRewards[state] = storm::utility::zero<ValueType>();
+                        }
                     }
                 }
             }
@@ -149,8 +153,12 @@ namespace storm {
             for (auto& rewardModel : mdpComponents.rewardModels) {
                 if (rewardModel.second.hasStateRewards()) {
                     auto& stateRewards = rewardModel.second.getStateRewardVector();
-                    for (auto state : ma.getMarkovianStates()) {
-                        stateRewards[state] /= exitRates[state];
+                    for (uint_fast64_t state = 0; state < stateRewards.size(); ++state) {
+                        if (ma.getMarkovianStates().get(state)) {
+                            stateRewards[state] /= exitRates[state];
+                        } else {
+                            stateRewards[state] = storm::utility::zero<ValueType>();
+                        }
                     }
                 }
             }