StateReward.h

Go to the documentation of this file.

#ifndef STORM_STORAGE_PRISM_STATEREWARD_H_
#define STORM_STORAGE_PRISM_STATEREWARD_H_
 
#include <map>
 
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/prism/LocatedInformation.h"
 
namespace storm {
namespace storage {
namespace expressions {
class Variable;
}
}  // namespace storage
}  // namespace storm
 
namespace storm {
namespace prism {
class StateReward : public LocatedInformation {
   public:
    StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression,
                std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
    // Create default implementations of constructors/assignment.
    StateReward() = default;
    StateReward(StateReward const& other) = default;
    StateReward& operator=(StateReward const& other) = default;
    StateReward(StateReward&& other) = default;
    StateReward& operator=(StateReward&& other) = default;

    storm::expressions::Expression const& getStatePredicateExpression() const;

    storm::expressions::Expression const& getRewardValueExpression() const;

    StateReward substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
 
    friend std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward);
 
   private:
    // The predicate that characterizes the states that obtain this reward.
    storm::expressions::Expression statePredicateExpression;
 
    // The expression that specifies the value of the reward obtained.
    storm::expressions::Expression rewardValueExpression;
};
 
}  // namespace prism
}  // namespace storm
 
#endif /* STORM_STORAGE_PRISM_STATEREWARD_H_ */