fixed a bug in dd-based reward model building

src/storm/api/builder.h

@@ -39,6 +39,11 @@ namespace storm {
                 typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options options;
                 options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options(formulas);
                 
+                if (storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()) {
+                    options.buildAllLabels = true;
+                    options.buildAllRewardModels = true;
+                }
+                
                 storm::builder::DdPrismModelBuilder<LibraryType, ValueType> builder;
                 return builder.build(model.asPrismProgram(), options);
             } else {
@@ -46,6 +51,11 @@ namespace storm {
                 typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options options;
                 options = typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options(formulas);
                 
+                if (storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()) {
+                    options.buildAllLabels = true;
+                    options.buildAllRewardModels = true;
+                }
+                
                 storm::builder::DdJaniModelBuilder<LibraryType, ValueType> builder;
                 return builder.build(model.asJaniModel(), options);
             }

src/storm/builder/DdJaniModelBuilder.cpp

@@ -1854,6 +1854,7 @@ namespace storm {
                 }
             } else {
                 auto const& globalVariables = model.getGlobalVariables();
+                
                 for (auto const& rewardModelName : options.getRewardModelNames()) {
                     if (globalVariables.hasVariable(rewardModelName)) {
                         result.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
@@ -1866,7 +1867,12 @@ namespace storm {
                 // If no reward model was yet added, but there was one that was given in the options, we try to build the
                 // standard reward model.
                 if (result.empty() && !options.getRewardModelNames().empty()) {
-                    result.push_back(globalVariables.getTransientVariables().front().getExpressionVariable());
+                    for (auto const& variable : globalVariables.getTransientVariables()) {
+                        if (variable.isRealVariable() || variable.isUnboundedIntegerVariable()) {
+                            result.push_back(variable.getExpressionVariable());
+                            break;
+                        }
+                    }
                 }
             }
             

src/storm/builder/DdPrismModelBuilder.cpp

@@ -1239,7 +1239,7 @@ namespace storm {
                             stateActionDd = transitionMatrix.notZero().existsAbstract(generationInfo.columnMetaVariables).template toAdd<ValueType>();
                         }
                         stateActionRewardDd *= stateActionDd.get();
-                    } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
+                    } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
                         // For CTMCs, we need to multiply the entries with the exit rate of the corresponding action.
                         stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables);
                     }

src/storm/storage/prism/ToJaniConverter.cpp

@@ -113,7 +113,7 @@ namespace storm {
             // edges and transient assignments that are added to the locations.
             std::map<uint_fast64_t, std::vector<storm::jani::Assignment>> transientEdgeAssignments;
             for (auto const& rewardModel : program.getRewardModels()) {
-                auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName());
+                auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default_reward_model" : rewardModel.getName());
                 storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true));
                 
                 if (rewardModel.hasStateRewards()) {