From f1eaab56031ce02e23ec9d6380a3e0e6ca3dd9b7 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 27 Jun 2018 15:28:53 +0200
Subject: [PATCH] enabling preservation of total reward formulas in
 ContinuousToDiscreteTimeModelTransformer

---
 .../transformer/ContinuousToDiscreteTimeModelTransformer.cpp   | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
index 20357f400..5a70e0b16 100644
--- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
+++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp
@@ -91,9 +91,10 @@ namespace storm {
             fragment.setUntilFormulasAllowed(true);
             fragment.setRewardOperatorsAllowed(true);
             fragment.setReachabilityRewardFormulasAllowed(true);
+            fragment.setTotalRewardFormulasAllowed(true);
+            fragment.setMultiObjectiveFormulasAllowed(true);
             return formula.isInFragment(fragment);
         }
-        
   
         template <typename ValueType, typename RewardModelType>
         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) {