TransitionReward.h

Go to the documentation of this file.

#pragma once
 
#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 TransitionReward : public LocatedInformation {
   public:
    TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& sourceStatePredicateExpression,
                     storm::expressions::Expression const& targetStatePredicateExpression, storm::expressions::Expression const& rewardValueExpression,
                     std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
    // Create default implementations of constructors/assignment.
    TransitionReward() = default;
    TransitionReward(TransitionReward const& other) = default;
    TransitionReward& operator=(TransitionReward const& other) = default;
    TransitionReward(TransitionReward&& other) = default;
    TransitionReward& operator=(TransitionReward&& other) = default;

    std::string const& getActionName() const;

    uint_fast64_t getActionIndex() const;

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

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

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

    bool isLabeled() const;

    TransitionReward substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
 
    friend std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward);
 
   private:
    // The index of the action name.
    uint_fast64_t actionIndex;
 
    // The name of the command this transition-based reward is attached to.
    std::string actionName;
 
    // A flag that stores whether the transition reward has an action label.
    bool labeled;
 
    // A predicate that needs to be satisfied in the source state of transitions that can earn the reward.
    storm::expressions::Expression sourceStatePredicateExpression;
 
    // A predicate that needs to be satisfied in the target state of transitions that can earn the reward.
    storm::expressions::Expression targetStatePredicateExpression;
 
    // The expression specifying the value of the reward obtained along the transitions.
    storm::expressions::Expression rewardValueExpression;
};
 
}  // namespace prism
}  // namespace storm