diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 868c47bba..1be905837 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -39,6 +39,11 @@ namespace storm { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); + if (storm::settings::getModule().isBuildFullModelSet()) { + options.buildAllLabels = true; + options.buildAllRewardModels = true; + } + storm::builder::DdPrismModelBuilder builder; return builder.build(model.asPrismProgram(), options); } else { @@ -46,6 +51,11 @@ namespace storm { typename storm::builder::DdJaniModelBuilder::Options options; options = typename storm::builder::DdJaniModelBuilder::Options(formulas); + if (storm::settings::getModule().isBuildFullModelSet()) { + options.buildAllLabels = true; + options.buildAllRewardModels = true; + } + storm::builder::DdJaniModelBuilder builder; return builder.build(model.asJaniModel(), options); } diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 6f1e67252..f5ae8e13a 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/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; + } + } } } diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 149fc8936..b67fc9705 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -1239,7 +1239,7 @@ namespace storm { stateActionDd = transitionMatrix.notZero().existsAbstract(generationInfo.columnMetaVariables).template toAdd(); } 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); } diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 6bc39b83c..7719b08e5 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -113,7 +113,7 @@ namespace storm { // edges and transient assignments that are added to the locations. std::map> 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()) {