Storm
A Modern Probabilistic Model Checker
|
#include <Command.h>
Public Member Functions | |
Command (uint_fast64_t globalIndex, bool markovian, uint_fast64_t actionIndex, std::string const &actionName, storm::expressions::Expression const &guardExpression, std::vector< storm::prism::Update > const &updates, std::string const &filename="", uint_fast64_t lineNumber=0) | |
Creates a command with the given action name, guard and updates. | |
Command ()=default | |
Command (Command const &other)=default | |
Command & | operator= (Command const &other)=default |
Command (Command &&other)=default | |
Command & | operator= (Command &&other)=default |
std::string const & | getActionName () const |
Retrieves the action name of this command. | |
uint_fast64_t | getActionIndex () const |
Retrieves the action index of this command. | |
bool | isMarkovian () const |
Retrieves whether the command is a Markovian command, i.e. | |
void | setMarkovian (bool value) |
Sets whether this command is a Markovian command, i.e. | |
storm::expressions::Expression const & | getGuardExpression () const |
Retrieves a reference to the guard of the command. | |
std::size_t | getNumberOfUpdates () const |
Retrieves the number of updates associated with this command. | |
storm::prism::Update const & | getUpdate (uint_fast64_t index) const |
Retrieves a reference to the update with the given index. | |
std::vector< storm::prism::Update > const & | getUpdates () const |
Retrieves a vector of all updates associated with this command. | |
std::vector< storm::prism::Update > & | getUpdates () |
Retrieves a vector of all updates associated with this command. | |
uint_fast64_t | getGlobalIndex () const |
Retrieves the global index of the command, that is, a unique index over all modules. | |
Command | substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const |
Substitutes all identifiers in the command according to the given map. | |
Command | substituteNonStandardPredicates () const |
bool | isLabeled () const |
Retrieves whether the command possesses a synchronization label. | |
bool | containsVariablesOnlyInUpdateProbabilities (std::set< storm::expressions::Variable > const &undefinedConstantVariables) const |
Checks whether the given set of variables only appears in the update probabilities of the command. | |
Command | simplify () const |
Simplifies this command. | |
![]() | |
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. | |
Friends | |
std::ostream & | operator<< (std::ostream &stream, Command const &command) |
storm::prism::Command::Command | ( | uint_fast64_t | globalIndex, |
bool | markovian, | ||
uint_fast64_t | actionIndex, | ||
std::string const & | actionName, | ||
storm::expressions::Expression const & | guardExpression, | ||
std::vector< storm::prism::Update > const & | updates, | ||
std::string const & | filename = "" , |
||
uint_fast64_t | lineNumber = 0 |
||
) |
Creates a command with the given action name, guard and updates.
globalIndex | The global index of the command. |
markovian | A flag indicating whether the command's update probabilities are to be interpreted as rates in a continuous-time model. |
actionIndex | The index of the action of the command. |
actionName | The action name of the command. |
guardExpression | the expression that defines the guard of the command. |
updates | A list of updates that is associated with this command. |
filename | The filename in which the command is defined. |
lineNumber | The line number in which the command is defined. |
Definition at line 5 of file Command.cpp.
|
default |
|
default |
|
default |
bool storm::prism::Command::containsVariablesOnlyInUpdateProbabilities | ( | std::set< storm::expressions::Variable > const & | undefinedConstantVariables | ) | const |
Checks whether the given set of variables only appears in the update probabilities of the command.
undefinedConstantVariables | The set of variables that may only appear in the update probabilities of the command. |
Definition at line 86 of file Command.cpp.
uint_fast64_t storm::prism::Command::getActionIndex | ( | ) | const |
Retrieves the action index of this command.
Definition at line 19 of file Command.cpp.
std::string const & storm::prism::Command::getActionName | ( | ) | const |
Retrieves the action name of this command.
Definition at line 31 of file Command.cpp.
uint_fast64_t storm::prism::Command::getGlobalIndex | ( | ) | const |
Retrieves the global index of the command, that is, a unique index over all modules.
Definition at line 56 of file Command.cpp.
storm::expressions::Expression const & storm::prism::Command::getGuardExpression | ( | ) | const |
Retrieves a reference to the guard of the command.
Definition at line 35 of file Command.cpp.
std::size_t storm::prism::Command::getNumberOfUpdates | ( | ) | const |
Retrieves the number of updates associated with this command.
Definition at line 39 of file Command.cpp.
storm::prism::Update const & storm::prism::Command::getUpdate | ( | uint_fast64_t | index | ) | const |
Retrieves a reference to the update with the given index.
Definition at line 43 of file Command.cpp.
std::vector< storm::prism::Update > & storm::prism::Command::getUpdates | ( | ) |
Retrieves a vector of all updates associated with this command.
Definition at line 52 of file Command.cpp.
std::vector< storm::prism::Update > const & storm::prism::Command::getUpdates | ( | ) | const |
Retrieves a vector of all updates associated with this command.
Definition at line 48 of file Command.cpp.
bool storm::prism::Command::isLabeled | ( | ) | const |
Retrieves whether the command possesses a synchronization label.
Definition at line 82 of file Command.cpp.
bool storm::prism::Command::isMarkovian | ( | ) | const |
Retrieves whether the command is a Markovian command, i.e.
it's update likelihoods are to be interpreted as rates in a continuous-time model.
Definition at line 23 of file Command.cpp.
void storm::prism::Command::setMarkovian | ( | bool | value | ) |
Sets whether this command is a Markovian command, i.e.
it's update likelihoods are to be interpreted as rates in a continuous-time model.
value | The command is flagged as Markovian iff this flag is set. |
Definition at line 27 of file Command.cpp.
Command storm::prism::Command::simplify | ( | ) | const |
Simplifies this command.
Definition at line 106 of file Command.cpp.
Command storm::prism::Command::substitute | ( | std::map< storm::expressions::Variable, storm::expressions::Expression > const & | substitution | ) | const |
Substitutes all identifiers in the command according to the given map.
substitution | The substitution to perform. |
Definition at line 60 of file Command.cpp.
Command storm::prism::Command::substituteNonStandardPredicates | ( | ) | const |
Definition at line 71 of file Command.cpp.
|
friend |
Definition at line 122 of file Command.cpp.