Storm
A Modern Probabilistic Model Checker
|
#include <Program.h>
Public Types | |
enum class | ModelType { UNDEFINED , DTMC , CTMC , MDP , CTMDP , MA , POMDP , PTA , SMG } |
An enum for the different model types. More... | |
enum class | ValidityCheckLevel : unsigned { VALIDINPUT = 0 , READYFORPROCESSING = 1 } |
Public Member Functions | |
Program (std::shared_ptr< storm::expressions::ExpressionManager > manager, ModelType modelType, std::vector< Constant > const &constants, std::vector< BooleanVariable > const &globalBooleanVariables, std::vector< IntegerVariable > const &globalIntegerVariables, std::vector< Formula > const &formulas, std::vector< Player > const &players, std::vector< Module > const &modules, std::map< std::string, uint_fast64_t > const &actionToIndexMap, std::vector< RewardModel > const &rewardModels, std::vector< Label > const &labels, std::vector< ObservationLabel > const &observationLabels, boost::optional< InitialConstruct > const &initialConstruct, boost::optional< SystemCompositionConstruct > const &compositionConstruct, bool prismCompatibility, std::string const &filename="", uint_fast64_t lineNumber=0, bool finalModel=true) | |
Creates a program with the given model type, undefined constants, global variables, modules, reward models, labels and initial states. | |
Program ()=default | |
Program (Program const &other)=default | |
Program & | operator= (Program const &other)=default |
Program (Program &&other)=default | |
Program & | operator= (Program &&other)=default |
ModelType | getModelType () const |
Retrieves the model type of the model. | |
bool | isDiscreteTimeModel () const |
Retrieves whether the model is a discrete-time model, i.e. | |
bool | isDeterministicModel () const |
Retrieves whether the model is one without nondeterministic choices, i.e. | |
bool | isPartiallyObservable () const |
Retrieves whether the model has restricted observability. | |
bool | hasUnboundedVariables () const |
bool | hasUndefinedConstants () const |
Retrieves whether there are undefined constants of any type in the program. | |
bool | undefinedConstantsAreGraphPreserving () const |
Checks that undefined constants (parameters) of the model preserve the graph of the underlying model. | |
std::vector< std::reference_wrapper< Constant const > > | getUndefinedConstants () const |
Retrieves the undefined constants in the program. | |
std::string | getUndefinedConstantsAsString () const |
Retrieves the undefined constants in the program as a comma-separated string. | |
bool | hasConstant (std::string const &constantName) const |
Retrieves whether the given constant exists in the program. | |
Constant const & | getConstant (std::string const &constantName) const |
Retrieves the constant with the given name if it exists. | |
std::map< storm::expressions::Variable, storm::expressions::Expression > | getConstantsSubstitution () const |
Retrieves a mapping of all defined constants to their defining expressions. | |
std::map< storm::expressions::Variable, storm::expressions::Expression > | getFormulasSubstitution () const |
Retrieves a mapping of all formula variables to their defining expressions. | |
std::map< storm::expressions::Variable, storm::expressions::Expression > | getConstantsFormulasSubstitution (bool getConstantsSubstitution=true, bool getFormulasSubstitution=true) const |
Retrieves a mapping of all defined constants and formula variables to their defining expressions. | |
std::map< storm::expressions::Variable, storm::expressions::Expression > | getSubstitutionForRenamedModule (Module const &renamedModule, std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const |
Applies the renaming of a renamed module to the given substitution. | |
std::map< std::string, std::string > | getFinalRenamingOfModule (Module const &renamedModule) const |
Gets the renaming of a module after flattening all renamings. | |
std::vector< Constant > const & | getConstants () const |
Retrieves all constants defined in the program. | |
std::size_t | getNumberOfConstants () const |
Retrieves the number of all constants defined in the program. | |
std::vector< Constant > | usedConstants () const |
Retrieves the constants that are actually used in the program. | |
size_t | getNumberOfCommands () const |
The total number of commands in the prism file. | |
bool | globalBooleanVariableExists (std::string const &variableName) const |
Retrieves whether a global Boolean variable with the given name exists. | |
bool | globalIntegerVariableExists (std::string const &variableName) const |
Retrieves whether a global Integer variable with the given name exists. | |
std::vector< BooleanVariable > const & | getGlobalBooleanVariables () const |
Retrieves the global boolean variables of the program. | |
BooleanVariable const & | getGlobalBooleanVariable (std::string const &variableName) const |
Retrieves a the global boolean variable with the given name. | |
std::vector< IntegerVariable > const & | getGlobalIntegerVariables () const |
Retrieves the global integer variables of the program. | |
IntegerVariable const & | getGlobalIntegerVariable (std::string const &variableName) const |
Retrieves a the global integer variable with the given name. | |
std::set< storm::expressions::Variable > | getAllExpressionVariables (bool includeConstants=true) const |
Retrieves all expression variables used by this program. | |
std::vector< storm::expressions::Expression > | getAllRangeExpressions () const |
Retrieves a list of expressions that characterize the legal ranges of all variables. | |
std::size_t | getNumberOfGlobalBooleanVariables () const |
Retrieves the number of global boolean variables of the program. | |
std::size_t | getNumberOfGlobalIntegerVariables () const |
Retrieves the number of global integer variables of the program. | |
std::vector< Formula > const & | getFormulas () const |
Retrieves the formulas defined in the program. | |
std::size_t | getNumberOfFormulas () const |
Retrieves the number of formulas in the program. | |
std::size_t | getNumberOfModules () const |
Retrieves the number of modules in the program. | |
Module const & | getModule (uint_fast64_t index) const |
Retrieves the module with the given index. | |
bool | hasModule (std::string const &moduleName) const |
Retrieves whether the program has a module with the given name. | |
Module const & | getModule (std::string const &moduleName) const |
Retrieves the module with the given name. | |
std::vector< Module > const & | getModules () const |
Retrieves all modules of the program. | |
std::vector< Player > const & | getPlayers () const |
Retrieves the players of the program. | |
std::size_t | getNumberOfPlayers () const |
Retrieves the number of players in the program. | |
storm::storage::PlayerIndex const & | getIndexOfPlayer (std::string const &playerName) const |
Retrieves the index of the player in the program. | |
std::map< std::string, storm::storage::PlayerIndex > const & | getPlayerNameToIndexMapping () const |
std::vector< storm::storage::PlayerIndex > | buildModuleIndexToPlayerIndexMap () const |
Retrieves a vector whose i'th entry corresponds to the player controlling module i. | |
std::map< uint_fast64_t, storm::storage::PlayerIndex > | buildActionIndexToPlayerIndexMap () const |
Retrieves a vector whose i'th entry corresponds to the player controlling action with index i. | |
std::map< std::string, uint_fast64_t > const & | getActionNameToIndexMapping () const |
Retrieves the mapping of action names to their indices. | |
void | updateInitialStatesExpression (expressions::Expression const &newExpression) |
Sets a new initial states expression. | |
bool | hasInitialConstruct () const |
Retrieves whether the program specifies an initial construct. | |
storm::expressions::Expression | getInitialStatesExpression () const |
Retrieves an expression characterizing the initial states. | |
bool | specifiesSystemComposition () const |
Retrieves whether the program specifies a system composition in terms of process algebra operations over the modules. | |
SystemCompositionConstruct const & | getSystemCompositionConstruct () const |
If the program specifies a system composition construct, this method retrieves it. | |
boost::optional< SystemCompositionConstruct > | getOptionalSystemCompositionConstruct () const |
Retrieves the system composition construct (if any) and none otherwise. | |
std::shared_ptr< Composition > | getDefaultSystemComposition () const |
Retrieves the default system composition for this program. | |
std::set< std::string > const & | getActions () const |
Retrieves the set of actions present in the program. | |
std::set< uint_fast64_t > const & | getSynchronizingActionIndices () const |
Retrieves the set of synchronizing action indices present in the program. | |
std::string const & | getActionName (uint_fast64_t actionIndex) const |
Retrieves the action name of the given action index. | |
uint_fast64_t | getActionIndex (std::string const &actionName) const |
Retrieves the index of the action with the given name. | |
bool | hasAction (std::string const &actionName) const |
Retrieves whether the program has an action with the given name. | |
bool | hasAction (uint_fast64_t const &actionIndex) const |
Retrieves whether the program has an action with the given index. | |
std::set< uint_fast64_t > const & | getModuleIndicesByAction (std::string const &action) const |
Retrieves the indices of all modules within this program that contain commands that are labelled with the given action. | |
std::set< uint_fast64_t > const & | getModuleIndicesByActionIndex (uint_fast64_t actionIndex) const |
Retrieves the indices of all modules within this program that contain commands that are labelled with the given action index. | |
uint_fast64_t | getModuleIndexByVariable (std::string const &variableName) const |
Retrieves the index of the module in which the given variable name was declared. | |
std::pair< uint_fast64_t, uint_fast64_t > | getModuleCommandIndexByGlobalCommandIndex (uint_fast64_t globalCommandIndex) const |
Retrieves the index of the module and the (local) index of the command with the given global command index. | |
uint64_t | getNumberOfUnlabeledCommands () const |
bool | hasRewardModel () const |
Retrieves whether the program has reward models. | |
bool | hasRewardModel (std::string const &name) const |
Retrieves whether the program has a reward model with the given name. | |
std::vector< RewardModel > const & | getRewardModels () const |
Retrieves the reward models of the program. | |
std::size_t | getNumberOfRewardModels () const |
Retrieves the number of reward models in the program. | |
RewardModel const & | getRewardModel (std::string const &rewardModelName) const |
Retrieves the reward model with the given name. | |
RewardModel const & | getRewardModel (uint_fast64_t index) const |
Retrieves the reward model with the given index. | |
bool | hasLabel (std::string const &labelName) const |
Checks whether the program has a label with the given name. | |
std::vector< Label > const & | getLabels () const |
Retrieves all labels that are defined by the probabilitic program. | |
std::vector< storm::expressions::Expression > | getAllGuards (bool negated=false) const |
Retrieves all guards appearing in the program. | |
storm::expressions::Expression const & | getLabelExpression (std::string const &label) const |
Retrieves the expression associated with the given label, if it exists. | |
std::map< std::string, storm::expressions::Expression > | getLabelToExpressionMapping () const |
Retrieves a mapping from all labels in the program to their defining expressions. | |
std::size_t | getNumberOfLabels () const |
Retrieves the number of labels in the program. | |
void | addLabel (std::string const &name, storm::expressions::Expression const &statePredicateExpression) |
Adds a label with the given name and defining expression to the program. | |
void | removeLabel (std::string const &name) |
Removes the label with the given name from the program. | |
void | filterLabels (std::set< std::string > const &labelSet) |
Removes all labels that are not contained in the given set from the program. | |
void | removeRewardModels () |
std::vector< ObservationLabel > const & | getObservationLabels () const |
Retrieves all observation labels that are defined by this program. | |
std::size_t | getNumberOfObservationLabels () const |
Retrieves the number of observation labels in the program. | |
Program | restrictCommands (storm::storage::FlatSet< uint_fast64_t > const &indexSet) const |
Creates a new program that drops all commands whose indices are not in the given set. | |
Program | defineUndefinedConstants (std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions) const |
Defines the undefined constants according to the given map and returns the resulting program. | |
Program | substituteConstants () const |
Substitutes all constants appearing in the expressions of the program by their defining expressions. | |
Program | substituteFormulas () const |
Substitutes all formulas appearing in the expressions of the program by their defining expressions. | |
Program | substituteNonStandardPredicates () const |
Substitutes all nonstandard predicates in expressions of the program by their defining expressions. | |
Program | substituteConstantsFormulas (bool substituteConstants=true, bool substituteFormulas=true) const |
Substitutes all constants and/or formulas appearing in the expressions of the program by their defining expressions. | |
Program | replaceVariableInitializationByInitExpression () const |
Replace the initialization in variables by an init-expression. | |
Program | replaceConstantByVariable (Constant const &c, expressions::Expression const &lowerBound, expressions::Expression const &upperBound, bool observable=true) const |
Substitutes the given constant by a fresh global variable that is bound between lowerBound and upperBound. | |
Program | simplify () |
Entry point for static analysis for simplify. | |
void | checkValidity (Program::ValidityCheckLevel lvl=Program::ValidityCheckLevel::READYFORPROCESSING) const |
Checks the validity of the program. | |
Program | flattenModules (std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory=std::shared_ptr< storm::utility::solver::SmtSolverFactory >(new storm::utility::solver::SmtSolverFactory())) const |
Creates an equivalent program that contains exactly one module. | |
Program | labelUnlabelledCommands (std::map< uint64_t, std::string > const &nameSuggestions={}) const |
Give commands that do not have an action name an action, which can be helpful for debugging and understanding traces. | |
storm::expressions::ExpressionManager & | getManager () const |
Retrieves the manager responsible for the expressions of this program. | |
std::unordered_map< uint_fast64_t, std::string > | buildCommandIndexToActionNameMap () const |
std::unordered_map< uint_fast64_t, uint_fast64_t > | buildCommandIndexToActionIndex () const |
std::unordered_map< uint_fast64_t, std::string > | buildActionIndexToActionNameMap () const |
storm::jani::Model | toJani (bool allVariablesGlobal=true, std::string suffix="") const |
Converts the PRISM model into an equivalent JANI model. | |
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > | toJani (std::vector< storm::jani::Property > const &properties, bool allVariablesGlobal=true, std::string suffix="") const |
Converts the PRISM model into an equivalent JANI model and if labels or reward models had to be renamed in the process, the renamings are applied to the given properties. | |
storm::storage::BitVector const & | getPossiblySynchronizingCommands () const |
Compute the (labelled) commands in the program that may be synchronizing. | |
![]() | |
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, Program const &program) |
storm::prism::Program::Program | ( | std::shared_ptr< storm::expressions::ExpressionManager > | manager, |
ModelType | modelType, | ||
std::vector< Constant > const & | constants, | ||
std::vector< BooleanVariable > const & | globalBooleanVariables, | ||
std::vector< IntegerVariable > const & | globalIntegerVariables, | ||
std::vector< Formula > const & | formulas, | ||
std::vector< Player > const & | players, | ||
std::vector< Module > const & | modules, | ||
std::map< std::string, uint_fast64_t > const & | actionToIndexMap, | ||
std::vector< RewardModel > const & | rewardModels, | ||
std::vector< Label > const & | labels, | ||
std::vector< ObservationLabel > const & | observationLabels, | ||
boost::optional< InitialConstruct > const & | initialConstruct, | ||
boost::optional< SystemCompositionConstruct > const & | compositionConstruct, | ||
bool | prismCompatibility, | ||
std::string const & | filename = "" , |
||
uint_fast64_t | lineNumber = 0 , |
||
bool | finalModel = true |
||
) |
Creates a program with the given model type, undefined constants, global variables, modules, reward models, labels and initial states.
manager | The manager responsible for the variables and expressions of the program. |
modelType | The type of the program. |
constants | The constants of the program. |
globalBooleanVariables | The global boolean variables of the program. |
globalIntegerVariables | The global integer variables of the program. |
formulas | The formulas defined in the program. |
modules | The modules of the program. |
actionToIndexMap | A mapping of action names to their indices. |
rewardModels | The reward models of the program. |
labels | The labels defined for this program. |
initialConstruct | The initial construct of the program. If none, then an initial construct is built using the initial values of the variables. |
compositionConstruct | If not none, specifies how the modules are composed for the full system. If none, the regular parallel composition is assumed. |
filename | The filename in which the program is defined. |
lineNumber | The line number in which the program is defined. |
finalModel | If set to true, the program is checked for input-validity, as well as some post-processing. |
Definition at line 158 of file Program.cpp.
|
default |
|
default |
void storm::prism::Program::addLabel | ( | std::string const & | name, |
storm::expressions::Expression const & | statePredicateExpression | ||
) |
Adds a label with the given name and defining expression to the program.
name | The name of the label. This name must not yet exist as a label name in the program. |
statePredicateExpression | The predicate that is described by the label. |
Definition at line 866 of file Program.cpp.
std::unordered_map< uint_fast64_t, std::string > storm::prism::Program::buildActionIndexToActionNameMap | ( | ) | const |
Definition at line 2245 of file Program.cpp.
std::map< uint64_t, storm::storage::PlayerIndex > storm::prism::Program::buildActionIndexToPlayerIndexMap | ( | ) | const |
Retrieves a vector whose i'th entry corresponds to the player controlling action with index i.
Actions that are not controlled by any player (in particular the silent action) will get assigned INVALID_PLAYER_INDEX.
Definition at line 590 of file Program.cpp.
std::unordered_map< uint_fast64_t, uint_fast64_t > storm::prism::Program::buildCommandIndexToActionIndex | ( | ) | const |
Definition at line 2253 of file Program.cpp.
std::unordered_map< uint_fast64_t, std::string > storm::prism::Program::buildCommandIndexToActionNameMap | ( | ) | const |
Definition at line 2235 of file Program.cpp.
std::vector< storm::storage::PlayerIndex > storm::prism::Program::buildModuleIndexToPlayerIndexMap | ( | ) | const |
Retrieves a vector whose i'th entry corresponds to the player controlling module i.
Modules that are not controlled by any player will get assigned INVALID_PLAYER_INDEX
Definition at line 578 of file Program.cpp.
void storm::prism::Program::checkValidity | ( | Program::ValidityCheckLevel | lvl = Program::ValidityCheckLevel::READYFORPROCESSING | ) | const |
Checks the validity of the program.
If the program is not valid, an exception is thrown with a message that indicates the source of the problem.
Definition at line 1226 of file Program.cpp.
Program storm::prism::Program::defineUndefinedConstants | ( | std::map< storm::expressions::Variable, storm::expressions::Expression > const & | constantDefinitions | ) | const |
Defines the undefined constants according to the given map and returns the resulting program.
constantDefinitions | A mapping from undefined constant to the expressions they are supposed to be replaced with. |
Definition at line 984 of file Program.cpp.
Removes all labels that are not contained in the given set from the program.
Note: no check is performed as to whether or not the given label names actually exist.
labelSet | The label set that is to be kept. |
Definition at line 884 of file Program.cpp.
Program storm::prism::Program::flattenModules | ( | std::shared_ptr< storm::utility::solver::SmtSolverFactory > const & | smtSolverFactory = std::shared_ptr<storm::utility::solver::SmtSolverFactory>(new storm::utility::solver::SmtSolverFactory()) | ) | const |
Creates an equivalent program that contains exactly one module.
smtSolverFactory | an SMT solver factory to use. If none is given, the default one is used. |
Definition at line 1951 of file Program.cpp.
uint_fast64_t storm::prism::Program::getActionIndex | ( | std::string const & | actionName | ) | const |
Retrieves the index of the action with the given name.
actionName | The name of the action. |
Definition at line 748 of file Program.cpp.
std::string const & storm::prism::Program::getActionName | ( | uint_fast64_t | actionIndex | ) | const |
Retrieves the action name of the given action index.
actionIndex | The index of the action whose name to retrieve. |
Definition at line 742 of file Program.cpp.
std::map< std::string, uint_fast64_t > const & storm::prism::Program::getActionNameToIndexMapping | ( | ) | const |
Retrieves the mapping of action names to their indices.
Definition at line 633 of file Program.cpp.
std::set< std::string > const & storm::prism::Program::getActions | ( | ) | const |
Retrieves the set of actions present in the program.
Definition at line 734 of file Program.cpp.
std::set< storm::expressions::Variable > storm::prism::Program::getAllExpressionVariables | ( | bool | includeConstants = true | ) | const |
Retrieves all expression variables used by this program.
includeConstants | Whether to include constants in the set of expression variables. |
Definition at line 490 of file Program.cpp.
std::vector< storm::expressions::Expression > storm::prism::Program::getAllGuards | ( | bool | negated = false | ) | const |
Retrieves all guards appearing in the program.
negated | A flag indicating whether the guards should be negated. |
Definition at line 837 of file Program.cpp.
std::vector< storm::expressions::Expression > storm::prism::Program::getAllRangeExpressions | ( | ) | const |
Retrieves a list of expressions that characterize the legal ranges of all variables.
Definition at line 512 of file Program.cpp.
Retrieves the constant with the given name if it exists.
constantName | The name of the constant to retrieve. |
Definition at line 397 of file Program.cpp.
Retrieves all constants defined in the program.
Definition at line 402 of file Program.cpp.
std::map< storm::expressions::Variable, storm::expressions::Expression > storm::prism::Program::getConstantsFormulasSubstitution | ( | bool | getConstantsSubstitution = true , |
bool | getFormulasSubstitution = true |
||
) | const |
Retrieves a mapping of all defined constants and formula variables to their defining expressions.
Definition at line 414 of file Program.cpp.
std::map< storm::expressions::Variable, storm::expressions::Expression > storm::prism::Program::getConstantsSubstitution | ( | ) | const |
Retrieves a mapping of all defined constants to their defining expressions.
Definition at line 406 of file Program.cpp.
std::shared_ptr< Composition > storm::prism::Program::getDefaultSystemComposition | ( | ) | const |
Retrieves the default system composition for this program.
Definition at line 722 of file Program.cpp.
std::map< std::string, std::string > storm::prism::Program::getFinalRenamingOfModule | ( | Module const & | renamedModule | ) | const |
Gets the renaming of a module after flattening all renamings.
Note that the base of a renamed module might again be a renamed module.
Definition at line 450 of file Program.cpp.
Retrieves the formulas defined in the program.
Definition at line 558 of file Program.cpp.
std::map< storm::expressions::Variable, storm::expressions::Expression > storm::prism::Program::getFormulasSubstitution | ( | ) | const |
Retrieves a mapping of all formula variables to their defining expressions.
Definition at line 410 of file Program.cpp.
BooleanVariable const & storm::prism::Program::getGlobalBooleanVariable | ( | std::string const & | variableName | ) | const |
Retrieves a the global boolean variable with the given name.
variableName | The name of the global boolean variable to retrieve. |
Definition at line 536 of file Program.cpp.
std::vector< BooleanVariable > const & storm::prism::Program::getGlobalBooleanVariables | ( | ) | const |
Retrieves the global boolean variables of the program.
Definition at line 482 of file Program.cpp.
IntegerVariable const & storm::prism::Program::getGlobalIntegerVariable | ( | std::string const & | variableName | ) | const |
Retrieves a the global integer variable with the given name.
variableName | The name of the global integer variable to retrieve. |
Definition at line 543 of file Program.cpp.
std::vector< IntegerVariable > const & storm::prism::Program::getGlobalIntegerVariables | ( | ) | const |
Retrieves the global integer variables of the program.
Definition at line 486 of file Program.cpp.
storm::storage::PlayerIndex const & storm::prism::Program::getIndexOfPlayer | ( | std::string const & | playerName | ) | const |
Retrieves the index of the player in the program.
Definition at line 570 of file Program.cpp.
storm::expressions::Expression storm::prism::Program::getInitialStatesExpression | ( | ) | const |
Retrieves an expression characterizing the initial states.
Definition at line 662 of file Program.cpp.
storm::expressions::Expression const & storm::prism::Program::getLabelExpression | ( | std::string const & | label | ) | const |
Retrieves the expression associated with the given label, if it exists.
labelName | The name of the label to retrieve. |
Definition at line 847 of file Program.cpp.
Retrieves all labels that are defined by the probabilitic program.
Definition at line 833 of file Program.cpp.
std::map< std::string, storm::expressions::Expression > storm::prism::Program::getLabelToExpressionMapping | ( | ) | const |
Retrieves a mapping from all labels in the program to their defining expressions.
Definition at line 854 of file Program.cpp.
storm::expressions::ExpressionManager & storm::prism::Program::getManager | ( | ) | const |
Retrieves the manager responsible for the expressions of this program.
Definition at line 2359 of file Program.cpp.
Program::ModelType storm::prism::Program::getModelType | ( | ) | const |
Retrieves the model type of the model.
Definition at line 247 of file Program.cpp.
Module const & storm::prism::Program::getModule | ( | std::string const & | moduleName | ) | const |
Retrieves the module with the given name.
moduleName | The name of the module to retrieve. |
Definition at line 623 of file Program.cpp.
storm::prism::Module const & storm::prism::Program::getModule | ( | uint_fast64_t | index | ) | const |
Retrieves the module with the given index.
index | The index of the module to retrieve. |
Definition at line 615 of file Program.cpp.
std::pair< uint_fast64_t, uint_fast64_t > storm::prism::Program::getModuleCommandIndexByGlobalCommandIndex | ( | uint_fast64_t | globalCommandIndex | ) | const |
Retrieves the index of the module and the (local) index of the command with the given global command index.
An exception is thrown if the command index is invalid.
getModule(x).getCommand(y).getGlobalIndex() == globalCommandIndex
globalCommandIndex | the global command index specifying the command that is to be found |
Definition at line 782 of file Program.cpp.
uint_fast64_t storm::prism::Program::getModuleIndexByVariable | ( | std::string const & | variableName | ) | const |
Retrieves the index of the module in which the given variable name was declared.
variableName | The name of the variable to search. |
Definition at line 775 of file Program.cpp.
std::set< uint_fast64_t > const & storm::prism::Program::getModuleIndicesByAction | ( | std::string const & | action | ) | const |
Retrieves the indices of all modules within this program that contain commands that are labelled with the given action.
action | The name of the action the modules are supposed to possess. |
Definition at line 762 of file Program.cpp.
std::set< uint_fast64_t > const & storm::prism::Program::getModuleIndicesByActionIndex | ( | uint_fast64_t | actionIndex | ) | const |
Retrieves the indices of all modules within this program that contain commands that are labelled with the given action index.
actionIndex | The index of the action the modules are supposed to possess. |
Definition at line 768 of file Program.cpp.
std::vector< storm::prism::Module > const & storm::prism::Program::getModules | ( | ) | const |
Retrieves all modules of the program.
Definition at line 629 of file Program.cpp.
size_t storm::prism::Program::getNumberOfCommands | ( | ) | const |
The total number of commands in the prism file.
Definition at line 263 of file Program.cpp.
std::size_t storm::prism::Program::getNumberOfConstants | ( | ) | const |
Retrieves the number of all constants defined in the program.
Definition at line 478 of file Program.cpp.
std::size_t storm::prism::Program::getNumberOfFormulas | ( | ) | const |
Retrieves the number of formulas in the program.
Definition at line 607 of file Program.cpp.
std::size_t storm::prism::Program::getNumberOfGlobalBooleanVariables | ( | ) | const |
Retrieves the number of global boolean variables of the program.
Definition at line 550 of file Program.cpp.
std::size_t storm::prism::Program::getNumberOfGlobalIntegerVariables | ( | ) | const |
Retrieves the number of global integer variables of the program.
Definition at line 554 of file Program.cpp.
std::size_t storm::prism::Program::getNumberOfLabels | ( | ) | const |
Retrieves the number of labels in the program.
Definition at line 862 of file Program.cpp.
std::size_t storm::prism::Program::getNumberOfModules | ( | ) | const |
Retrieves the number of modules in the program.
Definition at line 611 of file Program.cpp.
std::size_t storm::prism::Program::getNumberOfObservationLabels | ( | ) | const |
Retrieves the number of observation labels in the program.
Definition at line 904 of file Program.cpp.
std::size_t storm::prism::Program::getNumberOfPlayers | ( | ) | const |
Retrieves the number of players in the program.
Definition at line 566 of file Program.cpp.
std::size_t storm::prism::Program::getNumberOfRewardModels | ( | ) | const |
Retrieves the number of reward models in the program.
Definition at line 812 of file Program.cpp.
uint64_t storm::prism::Program::getNumberOfUnlabeledCommands | ( | ) | const |
Definition at line 637 of file Program.cpp.
std::vector< ObservationLabel > const & storm::prism::Program::getObservationLabels | ( | ) | const |
Retrieves all observation labels that are defined by this program.
Definition at line 900 of file Program.cpp.
boost::optional< SystemCompositionConstruct > storm::prism::Program::getOptionalSystemCompositionConstruct | ( | ) | const |
Retrieves the system composition construct (if any) and none otherwise.
Definition at line 718 of file Program.cpp.
std::map< std::string, storm::storage::PlayerIndex > const & storm::prism::Program::getPlayerNameToIndexMapping | ( | ) | const |
Definition at line 574 of file Program.cpp.
Retrieves the players of the program.
Definition at line 562 of file Program.cpp.
storm::storage::BitVector const & storm::prism::Program::getPossiblySynchronizingCommands | ( | ) | const |
Compute the (labelled) commands in the program that may be synchronizing.
Definition at line 908 of file Program.cpp.
storm::prism::RewardModel const & storm::prism::Program::getRewardModel | ( | std::string const & | rewardModelName | ) | const |
Retrieves the reward model with the given name.
rewardModelName | The name of the reward model to return. |
Definition at line 816 of file Program.cpp.
RewardModel const & storm::prism::Program::getRewardModel | ( | uint_fast64_t | index | ) | const |
Retrieves the reward model with the given index.
index | The index of the reward model to return. |
Definition at line 823 of file Program.cpp.
std::vector< storm::prism::RewardModel > const & storm::prism::Program::getRewardModels | ( | ) | const |
Retrieves the reward models of the program.
Definition at line 808 of file Program.cpp.
std::map< storm::expressions::Variable, storm::expressions::Expression > storm::prism::Program::getSubstitutionForRenamedModule | ( | Module const & | renamedModule, |
std::map< storm::expressions::Variable, storm::expressions::Expression > const & | substitution | ||
) | const |
Applies the renaming of a renamed module to the given substitution.
Definition at line 432 of file Program.cpp.
std::set< uint_fast64_t > const & storm::prism::Program::getSynchronizingActionIndices | ( | ) | const |
Retrieves the set of synchronizing action indices present in the program.
Definition at line 738 of file Program.cpp.
SystemCompositionConstruct const & storm::prism::Program::getSystemCompositionConstruct | ( | ) | const |
If the program specifies a system composition construct, this method retrieves it.
Definition at line 714 of file Program.cpp.
std::vector< std::reference_wrapper< storm::prism::Constant const > > storm::prism::Program::getUndefinedConstants | ( | ) | const |
Retrieves the undefined constants in the program.
Definition at line 368 of file Program.cpp.
std::string storm::prism::Program::getUndefinedConstantsAsString | ( | ) | const |
Retrieves the undefined constants in the program as a comma-separated string.
Definition at line 378 of file Program.cpp.
Retrieves whether a global Boolean variable with the given name exists.
variableName | The name of the variable |
Definition at line 528 of file Program.cpp.
Retrieves whether a global Integer variable with the given name exists.
variableName | The name of the variable |
Definition at line 532 of file Program.cpp.
Retrieves whether the program has an action with the given name.
Definition at line 754 of file Program.cpp.
bool storm::prism::Program::hasAction | ( | uint_fast64_t const & | actionIndex | ) | const |
Retrieves whether the program has an action with the given index.
Definition at line 758 of file Program.cpp.
Retrieves whether the given constant exists in the program.
constantName | The name of the constant to search. |
Definition at line 393 of file Program.cpp.
bool storm::prism::Program::hasInitialConstruct | ( | ) | const |
Retrieves whether the program specifies an initial construct.
Definition at line 645 of file Program.cpp.
Checks whether the program has a label with the given name.
labelName | The label of the program. |
Definition at line 828 of file Program.cpp.
Retrieves whether the program has a module with the given name.
Definition at line 619 of file Program.cpp.
bool storm::prism::Program::hasRewardModel | ( | ) | const |
Retrieves whether the program has reward models.
Definition at line 799 of file Program.cpp.
Retrieves whether the program has a reward model with the given name.
name | The name of the reward model to look for. |
Definition at line 803 of file Program.cpp.
bool storm::prism::Program::hasUnboundedVariables | ( | ) | const |
Definition at line 271 of file Program.cpp.
bool storm::prism::Program::hasUndefinedConstants | ( | ) | const |
Retrieves whether there are undefined constants of any type in the program.
Definition at line 285 of file Program.cpp.
bool storm::prism::Program::isDeterministicModel | ( | ) | const |
Retrieves whether the model is one without nondeterministic choices, i.e.
a DTMC or a CTMC.
Definition at line 255 of file Program.cpp.
bool storm::prism::Program::isDiscreteTimeModel | ( | ) | const |
Retrieves whether the model is a discrete-time model, i.e.
a DTMC or an MDP.
Definition at line 251 of file Program.cpp.
bool storm::prism::Program::isPartiallyObservable | ( | ) | const |
Retrieves whether the model has restricted observability.
Definition at line 259 of file Program.cpp.
Program storm::prism::Program::labelUnlabelledCommands | ( | std::map< uint64_t, std::string > const & | nameSuggestions = {} | ) | const |
Give commands that do not have an action name an action, which can be helpful for debugging and understanding traces.
nameSuggestions | Optional suggestions that map command indices to names |
Definition at line 1152 of file Program.cpp.
|
default |
|
default |
Removes the label with the given name from the program.
name | The name of a label that exists within the program. |
Definition at line 873 of file Program.cpp.
void storm::prism::Program::removeRewardModels | ( | ) |
Definition at line 879 of file Program.cpp.
Program storm::prism::Program::replaceConstantByVariable | ( | Constant const & | c, |
expressions::Expression const & | lowerBound, | ||
expressions::Expression const & | upperBound, | ||
bool | observable = true |
||
) | const |
Substitutes the given constant by a fresh global variable that is bound between lowerBound and upperBound.
The provided lowerBound and upperBound are not considered if the constant is Boolean. If the constant is defined by an expression, that expression is used as initial value for the created variable.
Definition at line 1205 of file Program.cpp.
Program storm::prism::Program::replaceVariableInitializationByInitExpression | ( | ) | const |
Replace the initialization in variables by an init-expression.
This should not change the semantics of the program and can be a preprocessing step.
Definition at line 1184 of file Program.cpp.
Program storm::prism::Program::restrictCommands | ( | storm::storage::FlatSet< uint_fast64_t > const & | indexSet | ) | const |
Creates a new program that drops all commands whose indices are not in the given set.
indexSet | The set of indices for which to keep the commands. |
Definition at line 912 of file Program.cpp.
Program storm::prism::Program::simplify | ( | ) |
Entry point for static analysis for simplify.
As we use the same expression manager, we recommend to not use the original program any further.
Definition at line 1803 of file Program.cpp.
bool storm::prism::Program::specifiesSystemComposition | ( | ) | const |
Retrieves whether the program specifies a system composition in terms of process algebra operations over the modules.
Definition at line 710 of file Program.cpp.
Program storm::prism::Program::substituteConstants | ( | ) | const |
Substitutes all constants appearing in the expressions of the program by their defining expressions.
For this to work, all constants need to be defined prior to calling this.
Definition at line 1026 of file Program.cpp.
Program storm::prism::Program::substituteConstantsFormulas | ( | bool | substituteConstants = true , |
bool | substituteFormulas = true |
||
) | const |
Substitutes all constants and/or formulas appearing in the expressions of the program by their defining expressions.
For this to work, all constants need to be defined prior to calling this.
Definition at line 1078 of file Program.cpp.
Program storm::prism::Program::substituteFormulas | ( | ) | const |
Substitutes all formulas appearing in the expressions of the program by their defining expressions.
The resulting program still contains the function definition, but does not apply them.
Definition at line 1030 of file Program.cpp.
Program storm::prism::Program::substituteNonStandardPredicates | ( | ) | const |
Substitutes all nonstandard predicates in expressions of the program by their defining expressions.
Definition at line 1034 of file Program.cpp.
storm::jani::Model storm::prism::Program::toJani | ( | bool | allVariablesGlobal = true , |
std::string | suffix = "" |
||
) | const |
Converts the PRISM model into an equivalent JANI model.
Definition at line 2321 of file Program.cpp.
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > storm::prism::Program::toJani | ( | std::vector< storm::jani::Property > const & | properties, |
bool | allVariablesGlobal = true , |
||
std::string | suffix = "" |
||
) | const |
Converts the PRISM model into an equivalent JANI model and if labels or reward models had to be renamed in the process, the renamings are applied to the given properties.
Definition at line 2329 of file Program.cpp.
bool storm::prism::Program::undefinedConstantsAreGraphPreserving | ( | ) | const |
Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.
That is, undefined constants may only appear in the probability expressions of updates as well as in the values in reward models.
Definition at line 294 of file Program.cpp.
void storm::prism::Program::updateInitialStatesExpression | ( | expressions::Expression const & | newExpression | ) |
Sets a new initial states expression.
May only be called if the program already has an initial states expression.
Definition at line 657 of file Program.cpp.
std::vector< Constant > storm::prism::Program::usedConstants | ( | ) | const |
Retrieves the constants that are actually used in the program.
Definition at line 2165 of file Program.cpp.
Definition at line 2405 of file Program.cpp.