Intermediate commit.

Former-commit-id: 19002ec2c1

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<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);
@@ -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<storm::models::AbstractModel<ValueType>> 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));
                                         }

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;
             }

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<storm::models::AbstractModel<storm::RationalFunction>> model = storm::adapters::ExplicitModelAdapter<storm::RationalFunction>::translateProgram(program, constants);
+        std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model = storm::adapters::ExplicitModelAdapter<storm::RationalFunction>::translateProgram(program, storm::settings::generalSettings().isSymbolicRewardModelNameSet() ? program.getRewardModel(storm::settings::generalSettings().getSymbolicRewardModelName()) : storm::prism::RewardModel(), constants);
         
         model->printModelInformationToStream(std::cout);
         

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<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.");
                 }