diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index ba3d5b7fa..5ae6a6a99 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -100,7 +100,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> translateProgram(storm::prism::Program program, storm::prism::RewardModel const& rewardModel = storm::prism::RewardModel(), std::string const& constantDefinitionString = "") { + static std::unique_ptr> 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 constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); @@ -116,6 +116,8 @@ 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); std::unique_ptr> result; @@ -527,6 +529,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] += eval.evaluate(transitionReward.getRewardValueExpression(),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/stormParametric.cpp b/src/stormParametric.cpp index 2907be328..143120667 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -143,7 +143,7 @@ int main(const int argc, const char** argv) { std::string const& programFile = storm::settings::generalSettings().getSymbolicModelFilename(); std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString(); storm::prism::Program program = storm::parser::PrismParser::parse(programFile); - std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program, constants); + std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program, storm::settings::generalSettings().isSymbolicRewardModelNameSet() ? program.getRewardModel(storm::settings::generalSettings().getSymbolicRewardModelName()) : storm::prism::RewardModel(), constants); model->printModelInformationToStream(std::cout); diff --git a/src/utility/cli.h b/src/utility/cli.h index f4589450c..ebe93b672 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -262,7 +262,7 @@ namespace storm { storm::prism::Program program = storm::parser::PrismParser::parse(programFile); // Then, build the model from the symbolic description. - result = storm::adapters::ExplicitModelAdapter::translateProgram(program, settings.isSymbolicRewardModelNameSet() ? program.getRewardModel(settings.getSymbolicRewardModelName()) : storm::prism::RewardModel(), constants); + result = storm::adapters::ExplicitModelAdapter::translateProgram(program, settings.isSymbolicRewardModelNameSet() ? settings.getSymbolicRewardModelName() : "", constants); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); }