From 7cd0dfe8b01d4929dd579bb8abe58416ac147c28 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 27 Nov 2014 18:12:32 +0100
Subject: [PATCH 1/3] Fixed an issue regarding the reward model generation.
Former-commit-id: 237acf99f9d4671d0deaf8f940d6dbb3ee731eea
---
src/adapters/ExplicitModelAdapter.h | 4 +++-
src/storage/prism/RewardModel.cpp | 6 +++++-
src/utility/cli.h | 2 +-
3 files changed, 9 insertions(+), 3 deletions(-)
diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index 38758fce7..803f897a1 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -98,7 +98,7 @@ namespace storm {
* @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, storm::prism::RewardModel const& rewardModel = storm::prism::RewardModel(), std::string const& constantDefinitionString = "") {
+ static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, std::string const& rewardModelName = "", 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);
@@ -110,6 +110,7 @@ namespace storm {
// all expressions in the program so we can then evaluate them without having to store the values of the
// constants in the state (i.e., valuation).
preparedProgram = preparedProgram.substituteConstants();
+ storm::prism::RewardModel const& rewardModel = rewardModelName != "" ? preparedProgram.getRewardModel(rewardModelName) : storm::prism::RewardModel();
ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel);
@@ -525,6 +526,7 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
+ std::cout << transitionReward.getStatePredicateExpression() << std::endl;
if (transitionReward.getActionName() == "" && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
}
diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
index 3576dece9..7f9b8107a 100644
--- a/src/storage/prism/RewardModel.cpp
+++ b/src/storage/prism/RewardModel.cpp
@@ -46,7 +46,11 @@ namespace storm {
}
std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
- stream << "rewards \"" << rewardModel.getName() << "\"" << std::endl;
+ stream << "rewards";
+ if (rewardModel.getName() != "") {
+ std::cout << " \"" << rewardModel.getName() << "\"";
+ }
+ std::cout << std::endl;
for (auto const& reward : rewardModel.getStateRewards()) {
stream << reward << std::endl;
}
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 1051d22b6..e0736efbc 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, settings.isSymbolicRewardModelNameSet() ? program.getRewardModel(settings.getSymbolicRewardModelName()) : storm::prism::RewardModel(), constants);
+ result = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, settings.isSymbolicRewardModelNameSet() ? settings.getSymbolicRewardModelName() : "", constants);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
From a7bce9e520f8f44d326a80663d04ece42eeaa5be Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 27 Nov 2014 18:21:51 +0100
Subject: [PATCH 2/3] Removed debug output and fixed the reward issue a bit
more.
Former-commit-id: ecbbeff14ef2b7fadf76ae74afdb8d11b44c80cd
---
src/adapters/ExplicitModelAdapter.h | 3 +--
src/storage/prism/Program.cpp | 5 +++++
src/storage/prism/Program.h | 8 ++++++++
3 files changed, 14 insertions(+), 2 deletions(-)
diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index 803f897a1..33d855af7 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -110,7 +110,7 @@ namespace storm {
// all expressions in the program so we can then evaluate them without having to store the values of the
// constants in the state (i.e., valuation).
preparedProgram = preparedProgram.substituteConstants();
- storm::prism::RewardModel const& rewardModel = rewardModelName != "" ? preparedProgram.getRewardModel(rewardModelName) : storm::prism::RewardModel();
+ storm::prism::RewardModel const& rewardModel = rewardModelName != "" || preparedProgram.hasRewardModel(rewardModelName) ? preparedProgram.getRewardModel(rewardModelName) : storm::prism::RewardModel();
ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel);
@@ -526,7 +526,6 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
- std::cout << transitionReward.getStatePredicateExpression() << std::endl;
if (transitionReward.getActionName() == "" && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
}
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 5392a7949..00a2fca09 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -149,6 +149,11 @@ namespace storm {
return !this->rewardModels.empty();
}
+ bool Program::hasRewardModel(std::string const& name) const {
+ auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
+ return nameIndexPair != this->rewardModelToIndexMap.end();
+ }
+
std::vector<storm::prism::RewardModel> const& Program::getRewardModels() const {
return this->rewardModels;
}
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 56321600d..ad7777f85 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -226,6 +226,14 @@ namespace storm {
*/
bool hasRewardModel() const;
+ /*!
+ * Retrieves whether the program has a reward model with the given name.
+ *
+ * @param name The name of the reward model to look for.
+ * @return True iff the program has a reward model with the given name.
+ */
+ bool hasRewardModel(std::string const& name) const;
+
/*!
* Retrieves the reward models of the program.
*
From 79798e2cb14dba323a3cefa78c17d0258316fed2 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 27 Nov 2014 18:35:09 +0100
Subject: [PATCH 3/3] Fixed the reward-issue even harder.
Former-commit-id: 2ca1c229e1732824aca34f32cad8248cfeade28a
---
src/adapters/ExplicitModelAdapter.h | 17 ++++++++++++++---
src/utility/cli.h | 2 +-
2 files changed, 15 insertions(+), 4 deletions(-)
diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index 33d855af7..f6526ff11 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -98,7 +98,7 @@ namespace storm {
* @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& rewardModelName = "", std::string const& constantDefinitionString = "") {
+ static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, bool rewards = true, std::string const& rewardModelName = "", 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);
@@ -110,8 +110,19 @@ namespace storm {
// all expressions in the program so we can then evaluate them without having to store the values of the
// constants in the state (i.e., valuation).
preparedProgram = preparedProgram.substituteConstants();
- storm::prism::RewardModel const& rewardModel = rewardModelName != "" || preparedProgram.hasRewardModel(rewardModelName) ? preparedProgram.getRewardModel(rewardModelName) : storm::prism::RewardModel();
-
+ storm::prism::RewardModel rewardModel = storm::prism::RewardModel();
+
+ // Select the appropriate reward model.
+ if (rewards) {
+ // If a specific reward model was selected or one with the empty name exists, select it.
+ if (rewardModelName != "" || preparedProgram.hasRewardModel(rewardModelName)) {
+ rewardModel = preparedProgram.getRewardModel(rewardModelName);
+ } else if (preparedProgram.hasRewardModel()) {
+ // Otherwise, we select the first one.
+ rewardModel = preparedProgram.getRewardModel(0);
+ }
+ }
+
ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel);
std::unique_ptr<storm::models::AbstractModel<ValueType>> result;
diff --git a/src/utility/cli.h b/src/utility/cli.h
index e0736efbc..30366caa9 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, settings.isSymbolicRewardModelNameSet() ? settings.getSymbolicRewardModelName() : "", constants);
+ result = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, true, settings.isSymbolicRewardModelNameSet() ? settings.getSymbolicRewardModelName() : "", constants);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}