diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index edde6925d..38758fce7 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -95,12 +95,10 @@ namespace storm {
* @param program The program to translate.
* @param constantDefinitionString A string that contains a comma-separated definition of all undefined
* constants in the model.
- * @param rewardModelName The name of reward model to be added to the model. This must be either a reward
- * model of the program or the empty string. In the latter case, the constructed model will contain no
- * rewards.
+ * @param rewardModel The reward model that is to be built.
* @return The explicit model that was given by the probabilistic program.
*/
- static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") {
+ static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, storm::prism::RewardModel const& rewardModel = storm::prism::RewardModel(), std::string const& constantDefinitionString = "") {
// Start by defining the undefined constants in the model.
// First, we need to parse the constant definition string.
std::map<std::string, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
@@ -113,21 +111,21 @@ namespace storm {
// constants in the state (i.e., valuation).
preparedProgram = preparedProgram.substituteConstants();
- ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModelName);
+ ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel);
std::unique_ptr<storm::models::AbstractModel<ValueType>> result;
switch (program.getModelType()) {
case storm::prism::Program::ModelType::DTMC:
- result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
+ result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
case storm::prism::Program::ModelType::CTMC:
- result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
+ result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
case storm::prism::Program::ModelType::MDP:
- result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
+ result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
case storm::prism::Program::ModelType::CTMDP:
- result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
+ result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
default:
LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type.");
@@ -634,11 +632,10 @@ namespace storm {
* Explores the state space of the given program and returns the components of the model as a result.
*
* @param program The program whose state space to explore.
- * @param rewardModelName The name of the reward model that is to be considered. If empty, no reward model
- * is considered.
+ * @param rewardModel The reward model that is to be considered.
* @return A structure containing the components of the resulting model.
*/
- static ModelComponents buildModelComponents(storm::prism::Program const& program, std::string const& rewardModelName) {
+ static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel) {
ModelComponents modelComponents;
VariableInformation variableInformation;
@@ -654,9 +651,6 @@ namespace storm {
// Create the structure for storing the reachable state space.
StateInformation stateInformation;
- // Get the selected reward model or create an empty one if none is selected.
- storm::prism::RewardModel const& rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::prism::RewardModel();
-
// Determine whether we have to combine different choices to one or whether this model can have more than
// one choice per state.
bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC;
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index d04ec0d25..ece0d9a00 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -61,7 +61,8 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("rewardmodel", "The name of the reward model to use.").setDefaultValueString("").setIsOptional(true).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies a PCTL formula that is to be checked on the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, pctlFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
@@ -154,6 +155,14 @@ namespace storm {
return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString();
}
+ bool GeneralSettings::isSymbolicRewardModelNameSet() const {
+ return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getHasBeenSet();
+ }
+
+ std::string GeneralSettings::getSymbolicRewardModelName() const {
+ return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getValueAsString();
+ }
+
bool GeneralSettings::isPctlPropertySet() const {
return this->getOption(pctlOptionName).getHasOptionBeenSet();
}
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index c65ab57a2..22f8fe58f 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -39,7 +39,6 @@ namespace storm {
*/
bool isVersionSet() const;
-
/*!
* Retrieves the name of the module for which to show the help or "all" to indicate that the full help
* needs to be shown.
@@ -127,6 +126,20 @@ namespace storm {
* @return The name of the file that contains the symbolic model specification.
*/
std::string getSymbolicModelFilename() const;
+
+ /*!
+ * Retrieves whether the name of a reward model was passed to the symbolic option.
+ *
+ * @return True iff the name of a reward model was passed to the symbolic option.
+ */
+ bool isSymbolicRewardModelNameSet() const;
+
+ /*!
+ * Retrieves the name of the reward model if one was set using the symbolic option.
+ *
+ * @return The name of the selected reward model.
+ */
+ std::string getSymbolicRewardModelName() const;
/*!
* Retrieves whether the pctl option was set.
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index f053c93e8..5392a7949 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -145,6 +145,10 @@ namespace storm {
return variableNameToModuleIndexPair->second;
}
+ bool Program::hasRewardModel() const {
+ return !this->rewardModels.empty();
+ }
+
std::vector<storm::prism::RewardModel> const& Program::getRewardModels() const {
return this->rewardModels;
}
@@ -159,6 +163,11 @@ namespace storm {
return this->getRewardModels()[nameIndexPair->second];
}
+ RewardModel const& Program::getRewardModel(uint_fast64_t index) const {
+ STORM_LOG_THROW(this->getNumberOfRewardModels() > index, storm::exceptions::OutOfRangeException, "Reward model with index " << index << " does not exist.");
+ return this->rewardModels[index];
+ }
+
std::vector<Label> const& Program::getLabels() const {
return this->labels;
}
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 2a618ff7a..56321600d 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -219,6 +219,13 @@ namespace storm {
*/
uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const;
+ /*!
+ * Retrieves whether the program has reward models.
+ *
+ * @return True iff the program has at least one reward model.
+ */
+ bool hasRewardModel() const;
+
/*!
* Retrieves the reward models of the program.
*
@@ -241,6 +248,14 @@ namespace storm {
*/
RewardModel const& getRewardModel(std::string const& rewardModelName) const;
+ /*!
+ * Retrieves the reward model with the given index.
+ *
+ * @param index The index of the reward model to return.
+ * @return The reward model with the given index.
+ */
+ RewardModel const& getRewardModel(uint_fast64_t index) const;
+
/*!
* Retrieves all labels that are defined by the probabilitic program.
*
diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
index a6c68b34f..3576dece9 100644
--- a/src/storage/prism/RewardModel.cpp
+++ b/src/storage/prism/RewardModel.cpp
@@ -10,6 +10,10 @@ namespace storm {
return this->rewardModelName;
}
+ bool RewardModel::empty() const {
+ return !this->hasStateRewards() && !this->hasTransitionRewards();
+ }
+
bool RewardModel::hasStateRewards() const {
return this->stateRewards.size() > 0;
}
diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h
index 3bb68d1b5..62841ef5e 100644
--- a/src/storage/prism/RewardModel.h
+++ b/src/storage/prism/RewardModel.h
@@ -40,6 +40,13 @@ namespace storm {
*/
std::string const& getName() const;
+ /*!
+ * Checks whether the reward model is empty, i.e. contains no state or transition rewards.
+ *
+ * @return True iff the reward model is empty.
+ */
+ bool empty() const;
+
/*!
* Retrieves whether there are any state rewards.
*
diff --git a/src/utility/cli.h b/src/utility/cli.h
index df8aa248a..a185a56a2 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -258,7 +258,7 @@ namespace storm {
storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
// Then, build the model from the symbolic description.
- result = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, constants);
+ result = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, settings.isSymbolicRewardModelNameSet() ? program.getRewardModel(settings.getSymbolicRewardModelName()) : storm::prism::RewardModel(), constants);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}