Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::prism::StateActionReward Class Reference

#include <StateActionReward.h>

Inheritance diagram for storm::prism::StateActionReward:
Collaboration diagram for storm::prism::StateActionReward:

Public Member Functions

 StateActionReward (uint_fast64_t actionIndex, std::string const &actionName, storm::expressions::Expression const &statePredicateExpression, storm::expressions::Expression const &rewardValueExpression, std::string const &filename="", uint_fast64_t lineNumber=0)
 Creates a transition reward for the transitions with the given name emanating from states satisfying the given expression with the value given by another expression.
 
 StateActionReward ()=default
 
 StateActionReward (StateActionReward const &other)=default
 
StateActionRewardoperator= (StateActionReward const &other)=default
 
 StateActionReward (StateActionReward &&other)=default
 
StateActionRewardoperator= (StateActionReward &&other)=default
 
std::string const & getActionName () const
 Retrieves the action name that is associated with this transition reward.
 
uint_fast64_t getActionIndex () const
 Retrieves the action index of the action associated with this transition reward (if any).
 
storm::expressions::Expression const & getStatePredicateExpression () const
 Retrieves the state predicate expression that is associated with this state reward.
 
storm::expressions::Expression const & getRewardValueExpression () const
 Retrieves the reward value expression associated with this state reward.
 
bool isLabeled () const
 Retrieves whether the transition reward has an action label.
 
StateActionReward substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
 Substitutes all identifiers in the transition reward according to the given map.
 
- Public Member Functions inherited from storm::prism::LocatedInformation
 LocatedInformation (std::string const &filename, uint_fast64_t lineNumber)
 Constructs a located information with the given filename and line number.
 
 LocatedInformation ()=default
 
 LocatedInformation (LocatedInformation const &other)=default
 
LocatedInformationoperator= (LocatedInformation const &other)=default
 
 LocatedInformation (LocatedInformation &&other)=default
 
LocatedInformationoperator= (LocatedInformation &&other)=default
 
std::string const & getFilename () const
 Retrieves the name of the file in which the information was found.
 
void setFilename (std::string const &filename)
 Sets the filename of this information.
 
uint_fast64_t getLineNumber () const
 Retrieves the line number in which the information was found.
 
void setLineNumber (uint_fast64_t lineNumber)
 Sets the line number of this information.
 

Friends

std::ostream & operator<< (std::ostream &stream, StateActionReward const &stateActionReward)
 

Detailed Description

Definition at line 20 of file StateActionReward.h.

Constructor & Destructor Documentation

◆ StateActionReward() [1/4]

storm::prism::StateActionReward::StateActionReward ( uint_fast64_t  actionIndex,
std::string const &  actionName,
storm::expressions::Expression const &  statePredicateExpression,
storm::expressions::Expression const &  rewardValueExpression,
std::string const &  filename = "",
uint_fast64_t  lineNumber = 0 
)

Creates a transition reward for the transitions with the given name emanating from states satisfying the given expression with the value given by another expression.

Parameters
actionIndexThe index of the action.
actionNameThe name of the command that obtains this reward.
statePredicateExpressionThe predicate that needs to hold before taking a transition with the previously specified name in order to obtain the reward.
rewardValueExpressionAn expression specifying the values of the rewards to attach to the transitions.
filenameThe filename in which the transition reward is defined.
lineNumberThe line number in which the transition reward is defined.

Definition at line 6 of file StateActionReward.cpp.

◆ StateActionReward() [2/4]

storm::prism::StateActionReward::StateActionReward ( )
default

◆ StateActionReward() [3/4]

storm::prism::StateActionReward::StateActionReward ( StateActionReward const &  other)
default

◆ StateActionReward() [4/4]

storm::prism::StateActionReward::StateActionReward ( StateActionReward &&  other)
default

Member Function Documentation

◆ getActionIndex()

uint_fast64_t storm::prism::StateActionReward::getActionIndex ( ) const

Retrieves the action index of the action associated with this transition reward (if any).

Returns
The action index of the transition reward.

Definition at line 21 of file StateActionReward.cpp.

◆ getActionName()

std::string const & storm::prism::StateActionReward::getActionName ( ) const

Retrieves the action name that is associated with this transition reward.

Returns
The action name that is associated with this transition reward.

Definition at line 17 of file StateActionReward.cpp.

◆ getRewardValueExpression()

storm::expressions::Expression const & storm::prism::StateActionReward::getRewardValueExpression ( ) const

Retrieves the reward value expression associated with this state reward.

Returns
The reward value expression associated with this state reward.

Definition at line 29 of file StateActionReward.cpp.

◆ getStatePredicateExpression()

storm::expressions::Expression const & storm::prism::StateActionReward::getStatePredicateExpression ( ) const

Retrieves the state predicate expression that is associated with this state reward.

Returns
The state predicate expression that is associated with this state reward.

Definition at line 25 of file StateActionReward.cpp.

◆ isLabeled()

bool storm::prism::StateActionReward::isLabeled ( ) const

Retrieves whether the transition reward has an action label.

Returns
True iff the transition reward has an action label.

Definition at line 33 of file StateActionReward.cpp.

◆ operator=() [1/2]

StateActionReward & storm::prism::StateActionReward::operator= ( StateActionReward &&  other)
default

◆ operator=() [2/2]

StateActionReward & storm::prism::StateActionReward::operator= ( StateActionReward const &  other)
default

◆ substitute()

StateActionReward storm::prism::StateActionReward::substitute ( std::map< storm::expressions::Variable, storm::expressions::Expression > const &  substitution) const

Substitutes all identifiers in the transition reward according to the given map.

Parameters
substitutionThe substitution to perform.
Returns
The resulting transition reward.

Definition at line 37 of file StateActionReward.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<< ( std::ostream &  stream,
StateActionReward const &  stateActionReward 
)
friend

Definition at line 42 of file StateActionReward.cpp.


The documentation for this class was generated from the following files: