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

#include <StateReward.h>

Inheritance diagram for storm::prism::StateReward:
Collaboration diagram for storm::prism::StateReward:

Public Member Functions

 StateReward (storm::expressions::Expression const &statePredicateExpression, storm::expressions::Expression const &rewardValueExpression, std::string const &filename="", uint_fast64_t lineNumber=0)
 Creates a state reward for the states satisfying the given expression with the value given by a second expression.
 
 StateReward ()=default
 
 StateReward (StateReward const &other)=default
 
StateRewardoperator= (StateReward const &other)=default
 
 StateReward (StateReward &&other)=default
 
StateRewardoperator= (StateReward &&other)=default
 
storm::expressions::Expression const & getStatePredicateExpression () const
 Retrieves the state predicate that is associated with this state reward.
 
storm::expressions::Expression const & getRewardValueExpression () const
 Retrieves the reward value associated with this state reward.
 
StateReward substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
 Substitutes all identifiers in the state 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, StateReward const &stateReward)
 

Detailed Description

Definition at line 20 of file StateReward.h.

Constructor & Destructor Documentation

◆ StateReward() [1/4]

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

Creates a state reward for the states satisfying the given expression with the value given by a second expression.

Parameters
statePredicateExpressionThe predicate that states earning this state-based reward need to satisfy.
rewardValueExpressionAn expression specifying the values of the rewards to attach to the states.
filenameThe filename in which the state reward is defined.
lineNumberThe line number in which the state reward is defined.

Definition at line 6 of file StateReward.cpp.

◆ StateReward() [2/4]

storm::prism::StateReward::StateReward ( )
default

◆ StateReward() [3/4]

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

◆ StateReward() [4/4]

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

Member Function Documentation

◆ getRewardValueExpression()

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

Retrieves the reward value associated with this state reward.

Returns
The reward value associated with this state reward.

Definition at line 16 of file StateReward.cpp.

◆ getStatePredicateExpression()

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

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

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

Definition at line 12 of file StateReward.cpp.

◆ operator=() [1/2]

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

◆ operator=() [2/2]

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

◆ substitute()

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

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

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

Definition at line 20 of file StateReward.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<< ( std::ostream &  stream,
StateReward const &  stateReward 
)
friend

Definition at line 25 of file StateReward.cpp.


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