added reward model (name) to check settings

Former-commit-id: b830574c07

src/modelchecker/CheckSettings.cpp

@@ -8,12 +8,12 @@ namespace storm {
     namespace modelchecker {
 
         template<typename ValueType>
-        CheckSettings<ValueType>::CheckSettings() : CheckSettings(boost::none, false, boost::none, false, false) {
+        CheckSettings<ValueType>::CheckSettings() : CheckSettings(boost::none, boost::none, false, boost::none, false, false) {
             // Intentionally left empty.
         }
         
         template<typename ValueType>
-        CheckSettings<ValueType>::CheckSettings(boost::optional<storm::OptimizationDirection> const& optimizationDirection, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies) : optimizationDirection(optimizationDirection), onlyInitialStatesRelevant(onlyInitialStatesRelevant), initialStatesBound(initialStatesBound), qualitative(qualitative), produceStrategies(produceStrategies) {
+        CheckSettings<ValueType>::CheckSettings(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies) : optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), initialStatesBound(initialStatesBound), qualitative(qualitative), produceStrategies(produceStrategies) {
             // Intentionally left empty.
         }
         
@@ -30,6 +30,7 @@ namespace storm {
         template<typename ValueType>
         CheckSettings<ValueType> CheckSettings<ValueType>::fromFormula(storm::logic::Formula const& formula, bool toplevel) {
             boost::optional<storm::OptimizationDirection> optimizationDirection;
+            boost::optional<std::string> rewardModel;
             boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> initialStatesBound;
             bool qualitative = false;
             bool onlyInitialStatesRelevant = !toplevel;
@@ -51,6 +52,8 @@ namespace storm {
                 }
             } else if (formula.isRewardOperatorFormula()) {
                 storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
+                rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
+
                 if (rewardOperatorFormula.hasOptimalityType()) {
                     optimizationDirection = rewardOperatorFormula.getOptimalityType();
                 }
@@ -64,7 +67,7 @@ namespace storm {
                     }
                 }
             }
-            return CheckSettings<ValueType>(optimizationDirection, onlyInitialStatesRelevant, initialStatesBound, qualitative, produceStrategies);
+            return CheckSettings<ValueType>(optimizationDirection, rewardModel, onlyInitialStatesRelevant, initialStatesBound, qualitative, produceStrategies);
         }
         
         template<typename ValueType>
@@ -77,6 +80,16 @@ namespace storm {
             return optimizationDirection.get();
         }
         
+        template<typename ValueType>
+        bool CheckSettings<ValueType>::isRewardModelSet() const {
+            return static_cast<bool>(rewardModel);
+        }
+        
+        template<typename ValueType>
+        std::string const& CheckSettings<ValueType>::getRewardModel() const {
+            return rewardModel.get();
+        }
+        
         template<typename ValueType>
         bool CheckSettings<ValueType>::isOnlyInitialStatesRelevantSet() const {
             return onlyInitialStatesRelevant;

src/modelchecker/CheckSettings.h

@@ -48,6 +48,16 @@ namespace storm {
              */
             storm::OptimizationDirection const& getOptimizationDirection() const;
             
+            /*!
+             * Retrieves whether a reward model was set.
+             */
+            bool isRewardModelSet() const;
+            
+            /*!
+             * Retrieves the reward model over which to perform the checking (if set).
+             */
+            std::string const& getRewardModel() const;
+            
             /*!
              * Retrieves whether only the initial states are relevant in the computation.
              */
@@ -79,6 +89,7 @@ namespace storm {
              * Creates a settings object with the given options.
              *
              * @param optimizationDirection If set, the probabilities will be minimized/maximized.
+             * @param rewardModelName If given, the checking has to be done wrt. to this reward model.
              * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values
              * for the initial states.
              * @param initialStatesBound The bound with which the initial states will be compared. This may only be set
@@ -88,7 +99,7 @@ namespace storm {
              * @param produceStrategies If supported by the model checker and the model formalism, strategies to achieve
              * a value will be produced if this flag is set.
              */
-            CheckSettings(boost::optional<storm::OptimizationDirection> const& optimizationDirection, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies);
+            CheckSettings(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies);
             
             /*!
              * Creates a settings object for the given formula.
@@ -101,6 +112,9 @@ namespace storm {
             // If set, the probabilities will be minimized/maximized.
             boost::optional<storm::OptimizationDirection> optimizationDirection;
 
+            // If set, the reward property has to be interpreted over this model.
+            boost::optional<std::string> rewardModel;
+            
             // If set to true, the model checker may decide to only compute the values for the initial states.
             bool onlyInitialStatesRelevant;