Storm
A Modern Probabilistic Model Checker
|
#include <Label.h>
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 | |
ObservationLabel & | operator= (ObservationLabel const &other)=default |
ObservationLabel (ObservationLabel &&other)=default | |
ObservationLabel & | operator= (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 |
![]() | |
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 | |
Label & | operator= (Label const &other)=default |
Label (Label &&other)=default | |
Label & | operator= (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 |
![]() | |
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 | |
LocatedInformation & | operator= (LocatedInformation const &other)=default |
LocatedInformation (LocatedInformation &&other)=default | |
LocatedInformation & | operator= (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. | |
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.
name | The name of the label. |
statePredicateExpression | The predicate that needs to hold before taking a transition with the previously specified name in order to obtain the reward. |
filename | The filename in which the transition reward is defined. |
lineNumber | The line number in which the transition reward is defined. |
|
default |
|
default |
|
default |
|
default |
|
default |
ObservationLabel storm::prism::ObservationLabel::substitute | ( | std::map< storm::expressions::Variable, storm::expressions::Expression > const & | substitution | ) | const |
ObservationLabel storm::prism::ObservationLabel::substituteNonStandardPredicates | ( | ) | const |