From 24e89ecce6cd5b3003a47ef7e762b157f62d7530 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 13 Sep 2016 11:48:18 +0200
Subject: [PATCH] properly scaling state-action rewards for DTMCs in JANI model
 now

Former-commit-id: a70c5c3c6e458243396887dc0073a071f2e9ed40 [formerly 8d2a346735a5d0a7a4e5679dad54205d4cea9bfa]
Former-commit-id: cad11b1b3f60945b7c636ed298d273460d63ed61
---
 src/builder/DdJaniModelBuilder.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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<Type> postprocessSystem(storm::jani::Model const& model, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::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<Type, ValueType> 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.