diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 5ab18683b..94df8a2f9 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1752,7 +1752,13 @@ namespace storm { storm::dd::Bdd postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (model.getModelType() == storm::jani::ModelType::DTMC) { - system.transitions = system.transitions / system.transitions.sumAbstract(variables.columnMetaVariables); + storm::dd::Add stateToNumberOfChoices = system.transitions.sumAbstract(variables.columnMetaVariables); + system.transitions = system.transitions / stateToNumberOfChoices; + + // Scale all state-action rewards. + for (auto& entry : system.transientEdgeAssignments) { + entry.second = entry.second / stateToNumberOfChoices; + } } // If we were asked to treat some states as terminal states, we cut away their transitions now.