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 std::shared_ptr> ContinuousToDiscreteTimeModelTransformer::transform(storm::models::sparse::MarkovAutomaton const& ma, boost::optional const& timeRewardModelName) {