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

#include <Label.h>

Inheritance diagram for storm::prism::ObservationLabel:
Collaboration diagram for storm::prism::ObservationLabel:

Public Member Functions

 ObservationLabel (std::string const &name, storm::expressions::Expression const &statePredicateExpression, std::string const &filename="", uint_fast64_t lineNumber=0)
 Creates a label with the given name and state predicate expression.
 
 ObservationLabel ()=default
 
 ObservationLabel (ObservationLabel const &other)=default
 
ObservationLabeloperator= (ObservationLabel const &other)=default
 
 ObservationLabel (ObservationLabel &&other)=default
 
ObservationLabeloperator= (ObservationLabel &&other)=default
 
ObservationLabel substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
 Substitutes all identifiers in the expression of the label according to the given map.
 
ObservationLabel substituteNonStandardPredicates () const
 
- Public Member Functions inherited from storm::prism::Label
 Label (std::string const &name, storm::expressions::Expression const &statePredicateExpression, std::string const &filename="", uint_fast64_t lineNumber=0)
 Creates a label with the given name and state predicate expression.
 
 Label ()=default
 
 Label (Label const &other)=default
 
Labeloperator= (Label const &other)=default
 
 Label (Label &&other)=default
 
Labeloperator= (Label &&other)=default
 
std::string const & getName () const
 Retrieves the name that is associated with this label.
 
storm::expressions::Expression const & getStatePredicateExpression () const
 Retrieves the state predicate expression that is associated with this label.
 
Label substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
 Substitutes all identifiers in the expression of the label according to the given map.
 
Label substituteNonStandardPredicates () const
 
- 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.
 

Detailed Description

Definition at line 74 of file Label.h.

Constructor & Destructor Documentation

◆ ObservationLabel() [1/4]

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

Creates a label with the given name and state predicate expression.

Parameters
nameThe name of the label.
statePredicateExpressionThe predicate that needs to hold before taking a transition with the previously specified name in order to obtain the reward.
filenameThe filename in which the transition reward is defined.
lineNumberThe line number in which the transition reward is defined.

Definition at line 32 of file Label.cpp.

◆ ObservationLabel() [2/4]

storm::prism::ObservationLabel::ObservationLabel ( )
default

◆ ObservationLabel() [3/4]

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

◆ ObservationLabel() [4/4]

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

Member Function Documentation

◆ operator=() [1/2]

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

◆ operator=() [2/2]

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

◆ substitute()

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

Substitutes all identifiers in the expression of the label according to the given map.

Parameters
substitutionThe substitution to perform.
Returns
The resulting label.

Definition at line 38 of file Label.cpp.

◆ substituteNonStandardPredicates()

ObservationLabel storm::prism::ObservationLabel::substituteNonStandardPredicates ( ) const

Definition at line 42 of file Label.cpp.


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