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

#include <Program.h>

Inheritance diagram for storm::prism::Program:
Collaboration diagram for storm::prism::Program:

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
 
Programoperator= (Program const &other)=default
 
 Program (Program &&other)=default
 
Programoperator= (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 constgetConstant (std::string const &constantName) const
 Retrieves the constant with the given name if it exists.
 
std::map< storm::expressions::Variable, storm::expressions::ExpressiongetConstantsSubstitution () const
 Retrieves a mapping of all defined constants to their defining expressions.
 
std::map< storm::expressions::Variable, storm::expressions::ExpressiongetFormulasSubstitution () const
 Retrieves a mapping of all formula variables to their defining expressions.
 
std::map< storm::expressions::Variable, storm::expressions::ExpressiongetConstantsFormulasSubstitution (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::ExpressiongetSubstitutionForRenamedModule (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 > constgetConstants () 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< ConstantusedConstants () 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 > constgetGlobalBooleanVariables () const
 Retrieves the global boolean variables of the program.
 
BooleanVariable constgetGlobalBooleanVariable (std::string const &variableName) const
 Retrieves a the global boolean variable with the given name.
 
std::vector< IntegerVariable > constgetGlobalIntegerVariables () const
 Retrieves the global integer variables of the program.
 
IntegerVariable constgetGlobalIntegerVariable (std::string const &variableName) const
 Retrieves a the global integer variable with the given name.
 
std::set< storm::expressions::VariablegetAllExpressionVariables (bool includeConstants=true) const
 Retrieves all expression variables used by this program.
 
std::vector< storm::expressions::ExpressiongetAllRangeExpressions () 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 > constgetFormulas () 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 > constgetModules () const
 Retrieves all modules of the program.
 
std::vector< Player > constgetPlayers () const
 Retrieves the players of the program.
 
std::size_t getNumberOfPlayers () const
 Retrieves the number of players in the program.
 
storm::storage::PlayerIndex constgetIndexOfPlayer (std::string const &playerName) const
 Retrieves the index of the player in the program.
 
std::map< std::string, storm::storage::PlayerIndex > constgetPlayerNameToIndexMapping () const
 
std::vector< storm::storage::PlayerIndexbuildModuleIndexToPlayerIndexMap () const
 Retrieves a vector whose i'th entry corresponds to the player controlling module i.
 
std::map< uint_fast64_t, storm::storage::PlayerIndexbuildActionIndexToPlayerIndexMap () const
 Retrieves a vector whose i'th entry corresponds to the player controlling action with index i.
 
std::map< std::string, uint_fast64_t > constgetActionNameToIndexMapping () 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 constgetSystemCompositionConstruct () const
 If the program specifies a system composition construct, this method retrieves it.
 
boost::optional< SystemCompositionConstructgetOptionalSystemCompositionConstruct () const
 Retrieves the system composition construct (if any) and none otherwise.
 
std::shared_ptr< CompositiongetDefaultSystemComposition () const
 Retrieves the default system composition for this program.
 
std::set< std::string > constgetActions () const
 Retrieves the set of actions present in the program.
 
std::set< uint_fast64_t > constgetSynchronizingActionIndices () const
 Retrieves the set of synchronizing action indices present in the program.
 
std::string constgetActionName (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 > constgetModuleIndicesByAction (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 > constgetModuleIndicesByActionIndex (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_tgetModuleCommandIndexByGlobalCommandIndex (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 > constgetRewardModels () const
 Retrieves the reward models of the program.
 
std::size_t getNumberOfRewardModels () const
 Retrieves the number of reward models in the program.
 
RewardModel constgetRewardModel (std::string const &rewardModelName) const
 Retrieves the reward model with the given name.
 
RewardModel constgetRewardModel (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 > constgetLabels () const
 Retrieves all labels that are defined by the probabilitic program.
 
std::vector< storm::expressions::ExpressiongetAllGuards (bool negated=false) const
 Retrieves all guards appearing in the program.
 
storm::expressions::Expression constgetLabelExpression (std::string const &label) const
 Retrieves the expression associated with the given label, if it exists.
 
std::map< std::string, storm::expressions::ExpressiongetLabelToExpressionMapping () 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 > constgetObservationLabels () 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::ExpressionManagergetManager () 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_tbuildCommandIndexToActionIndex () 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 constgetPossiblySynchronizingCommands () const
 Compute the (labelled) commands in the program that may be synchronizing.
 
- 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, Program const &program)
 

Detailed Description

Definition at line 32 of file Program.h.

Member Enumeration Documentation

◆ ModelType

An enum for the different model types.

Enumerator
UNDEFINED 
DTMC 
CTMC 
MDP 
CTMDP 
MA 
POMDP 
PTA 
SMG 

Definition at line 37 of file Program.h.

◆ ValidityCheckLevel

Enumerator
VALIDINPUT 
READYFORPROCESSING 

Definition at line 39 of file Program.h.

Constructor & Destructor Documentation

◆ Program() [1/4]

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.

Parameters
managerThe manager responsible for the variables and expressions of the program.
modelTypeThe type of the program.
constantsThe constants of the program.
globalBooleanVariablesThe global boolean variables of the program.
globalIntegerVariablesThe global integer variables of the program.
formulasThe formulas defined in the program.
modulesThe modules of the program.
actionToIndexMapA mapping of action names to their indices.
rewardModelsThe reward models of the program.
labelsThe labels defined for this program.
initialConstructThe initial construct of the program. If none, then an initial construct is built using the initial values of the variables.
compositionConstructIf not none, specifies how the modules are composed for the full system. If none, the regular parallel composition is assumed.
filenameThe filename in which the program is defined.
lineNumberThe line number in which the program is defined.
finalModelIf set to true, the program is checked for input-validity, as well as some post-processing.

Definition at line 158 of file Program.cpp.

◆ Program() [2/4]

storm::prism::Program::Program ( )
default

◆ Program() [3/4]

storm::prism::Program::Program ( Program const other)
default

◆ Program() [4/4]

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

Member Function Documentation

◆ addLabel()

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.

Parameters
nameThe name of the label. This name must not yet exist as a label name in the program.
statePredicateExpressionThe predicate that is described by the label.

Definition at line 866 of file Program.cpp.

◆ buildActionIndexToActionNameMap()

std::unordered_map< uint_fast64_t, std::string > storm::prism::Program::buildActionIndexToActionNameMap ( ) const

Definition at line 2245 of file Program.cpp.

◆ buildActionIndexToPlayerIndexMap()

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.

◆ buildCommandIndexToActionIndex()

std::unordered_map< uint_fast64_t, uint_fast64_t > storm::prism::Program::buildCommandIndexToActionIndex ( ) const

Definition at line 2253 of file Program.cpp.

◆ buildCommandIndexToActionNameMap()

std::unordered_map< uint_fast64_t, std::string > storm::prism::Program::buildCommandIndexToActionNameMap ( ) const

Definition at line 2235 of file Program.cpp.

◆ buildModuleIndexToPlayerIndexMap()

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.

◆ checkValidity()

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.

◆ defineUndefinedConstants()

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.

Parameters
constantDefinitionsA mapping from undefined constant to the expressions they are supposed to be replaced with.
Returns
The program after all undefined constants in the given map have been replaced with their definitions.

Definition at line 984 of file Program.cpp.

◆ filterLabels()

void storm::prism::Program::filterLabels ( std::set< std::string > const labelSet)

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.

Parameters
labelSetThe label set that is to be kept.

Definition at line 884 of file Program.cpp.

◆ flattenModules()

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.

Parameters
smtSolverFactoryan SMT solver factory to use. If none is given, the default one is used.
Returns
The resulting program.

Definition at line 1951 of file Program.cpp.

◆ getActionIndex()

uint_fast64_t storm::prism::Program::getActionIndex ( std::string const actionName) const

Retrieves the index of the action with the given name.

Parameters
actionNameThe name of the action.
Returns
The index of the action.

Definition at line 748 of file Program.cpp.

◆ getActionName()

std::string const & storm::prism::Program::getActionName ( uint_fast64_t  actionIndex) const

Retrieves the action name of the given action index.

Parameters
actionIndexThe index of the action whose name to retrieve.
Returns
The name of the action.

Definition at line 742 of file Program.cpp.

◆ getActionNameToIndexMapping()

std::map< std::string, uint_fast64_t > const & storm::prism::Program::getActionNameToIndexMapping ( ) const

Retrieves the mapping of action names to their indices.

Returns
The mapping of action names to their indices.

Definition at line 633 of file Program.cpp.

◆ getActions()

std::set< std::string > const & storm::prism::Program::getActions ( ) const

Retrieves the set of actions present in the program.

Returns
The set of actions present in the program.

Definition at line 734 of file Program.cpp.

◆ getAllExpressionVariables()

std::set< storm::expressions::Variable > storm::prism::Program::getAllExpressionVariables ( bool  includeConstants = true) const

Retrieves all expression variables used by this program.

Parameters
includeConstantsWhether to include constants in the set of expression variables.
Returns
The set of expression variables used by this program.

Definition at line 490 of file Program.cpp.

◆ getAllGuards()

std::vector< storm::expressions::Expression > storm::prism::Program::getAllGuards ( bool  negated = false) const

Retrieves all guards appearing in the program.

Parameters
negatedA flag indicating whether the guards should be negated.
Returns
All guards appearing in the program.

Definition at line 837 of file Program.cpp.

◆ getAllRangeExpressions()

std::vector< storm::expressions::Expression > storm::prism::Program::getAllRangeExpressions ( ) const

Retrieves a list of expressions that characterize the legal ranges of all variables.

Returns
A list of expressions that characterize the legal ranges of all variables.

Definition at line 512 of file Program.cpp.

◆ getConstant()

Constant const & storm::prism::Program::getConstant ( std::string const constantName) const

Retrieves the constant with the given name if it exists.

Parameters
constantNameThe name of the constant to retrieve.
Returns
The constant with the given name if it exists.

Definition at line 397 of file Program.cpp.

◆ getConstants()

std::vector< Constant > const & storm::prism::Program::getConstants ( ) const

Retrieves all constants defined in the program.

Returns
The constants defined in the program.

Definition at line 402 of file Program.cpp.

◆ getConstantsFormulasSubstitution()

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.

Returns
A mapping from constants and formulas to their expressions.

Definition at line 414 of file Program.cpp.

◆ getConstantsSubstitution()

std::map< storm::expressions::Variable, storm::expressions::Expression > storm::prism::Program::getConstantsSubstitution ( ) const

Retrieves a mapping of all defined constants to their defining expressions.

Returns
A mapping from constants to their 'values'.

Definition at line 406 of file Program.cpp.

◆ getDefaultSystemComposition()

std::shared_ptr< Composition > storm::prism::Program::getDefaultSystemComposition ( ) const

Retrieves the default system composition for this program.

Returns
The default system composition.

Definition at line 722 of file Program.cpp.

◆ getFinalRenamingOfModule()

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.

◆ getFormulas()

std::vector< Formula > const & storm::prism::Program::getFormulas ( ) const

Retrieves the formulas defined in the program.

Returns
The formulas defined in the program.

Definition at line 558 of file Program.cpp.

◆ getFormulasSubstitution()

std::map< storm::expressions::Variable, storm::expressions::Expression > storm::prism::Program::getFormulasSubstitution ( ) const

Retrieves a mapping of all formula variables to their defining expressions.

Returns
A mapping from constants to their 'values'.

Definition at line 410 of file Program.cpp.

◆ getGlobalBooleanVariable()

BooleanVariable const & storm::prism::Program::getGlobalBooleanVariable ( std::string const variableName) const

Retrieves a the global boolean variable with the given name.

Parameters
variableNameThe name of the global boolean variable to retrieve.
Returns
The global boolean variable with the given name.

Definition at line 536 of file Program.cpp.

◆ getGlobalBooleanVariables()

std::vector< BooleanVariable > const & storm::prism::Program::getGlobalBooleanVariables ( ) const

Retrieves the global boolean variables of the program.

Returns
The global boolean variables of the program.

Definition at line 482 of file Program.cpp.

◆ getGlobalIntegerVariable()

IntegerVariable const & storm::prism::Program::getGlobalIntegerVariable ( std::string const variableName) const

Retrieves a the global integer variable with the given name.

Parameters
variableNameThe name of the global integer variable to retrieve.
Returns
The global integer variable with the given name.

Definition at line 543 of file Program.cpp.

◆ getGlobalIntegerVariables()

std::vector< IntegerVariable > const & storm::prism::Program::getGlobalIntegerVariables ( ) const

Retrieves the global integer variables of the program.

Returns
The global integer variables of the program.

Definition at line 486 of file Program.cpp.

◆ getIndexOfPlayer()

storm::storage::PlayerIndex const & storm::prism::Program::getIndexOfPlayer ( std::string const playerName) const

Retrieves the index of the player in the program.

Returns
The index of the player in the program.

Definition at line 570 of file Program.cpp.

◆ getInitialStatesExpression()

storm::expressions::Expression storm::prism::Program::getInitialStatesExpression ( ) const

Retrieves an expression characterizing the initial states.

Returns
an expression characterizing the initial states.

Definition at line 662 of file Program.cpp.

◆ getLabelExpression()

storm::expressions::Expression const & storm::prism::Program::getLabelExpression ( std::string const label) const

Retrieves the expression associated with the given label, if it exists.

Parameters
labelNameThe name of the label to retrieve.

Definition at line 847 of file Program.cpp.

◆ getLabels()

std::vector< Label > const & storm::prism::Program::getLabels ( ) const

Retrieves all labels that are defined by the probabilitic program.

Returns
A set of labels that are defined in the program.

Definition at line 833 of file Program.cpp.

◆ getLabelToExpressionMapping()

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.

Returns
A mapping from label names to their expressions.

Definition at line 854 of file Program.cpp.

◆ getManager()

storm::expressions::ExpressionManager & storm::prism::Program::getManager ( ) const

Retrieves the manager responsible for the expressions of this program.

Returns
The manager responsible for the expressions of this program.

Definition at line 2359 of file Program.cpp.

◆ getModelType()

Program::ModelType storm::prism::Program::getModelType ( ) const

Retrieves the model type of the model.

Returns
The type of the model.

Definition at line 247 of file Program.cpp.

◆ getModule() [1/2]

Module const & storm::prism::Program::getModule ( std::string const &  moduleName) const

Retrieves the module with the given name.

Parameters
moduleNameThe name of the module to retrieve.
Returns
The module with the given name.

Definition at line 623 of file Program.cpp.

◆ getModule() [2/2]

storm::prism::Module const & storm::prism::Program::getModule ( uint_fast64_t  index) const

Retrieves the module with the given index.

Parameters
indexThe index of the module to retrieve.
Returns
The module with the given index.

Definition at line 615 of file Program.cpp.

◆ getModuleCommandIndexByGlobalCommandIndex()

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.

Note
if (x,y) is the result of this method, we have getModule(x).getCommand(y).getGlobalIndex() == globalCommandIndex
Parameters
globalCommandIndexthe global command index specifying the command that is to be found
Returns
the index of the module and the (local) index of the found command

Definition at line 782 of file Program.cpp.

◆ getModuleIndexByVariable()

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.

Parameters
variableNameThe name of the variable to search.
Returns
The index of the module in which the given variable name was declared.

Definition at line 775 of file Program.cpp.

◆ getModuleIndicesByAction()

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.

Parameters
actionThe name of the action the modules are supposed to possess.
Returns
A set of indices of all matching modules.

Definition at line 762 of file Program.cpp.

◆ getModuleIndicesByActionIndex()

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.

Parameters
actionIndexThe index of the action the modules are supposed to possess.
Returns
A set of indices of all matching modules.

Definition at line 768 of file Program.cpp.

◆ getModules()

std::vector< storm::prism::Module > const & storm::prism::Program::getModules ( ) const

Retrieves all modules of the program.

Returns
All modules of the program.

Definition at line 629 of file Program.cpp.

◆ getNumberOfCommands()

size_t storm::prism::Program::getNumberOfCommands ( ) const

The total number of commands in the prism file.

Definition at line 263 of file Program.cpp.

◆ getNumberOfConstants()

std::size_t storm::prism::Program::getNumberOfConstants ( ) const

Retrieves the number of all constants defined in the program.

Returns
The number of constants defined in the program.

Definition at line 478 of file Program.cpp.

◆ getNumberOfFormulas()

std::size_t storm::prism::Program::getNumberOfFormulas ( ) const

Retrieves the number of formulas in the program.

Returns
The number of formulas in the program.

Definition at line 607 of file Program.cpp.

◆ getNumberOfGlobalBooleanVariables()

std::size_t storm::prism::Program::getNumberOfGlobalBooleanVariables ( ) const

Retrieves the number of global boolean variables of the program.

Returns
The number of global boolean variables of the program.

Definition at line 550 of file Program.cpp.

◆ getNumberOfGlobalIntegerVariables()

std::size_t storm::prism::Program::getNumberOfGlobalIntegerVariables ( ) const

Retrieves the number of global integer variables of the program.

Returns
The number of global integer variables of the program.

Definition at line 554 of file Program.cpp.

◆ getNumberOfLabels()

std::size_t storm::prism::Program::getNumberOfLabels ( ) const

Retrieves the number of labels in the program.

Returns
The number of labels in the program.

Definition at line 862 of file Program.cpp.

◆ getNumberOfModules()

std::size_t storm::prism::Program::getNumberOfModules ( ) const

Retrieves the number of modules in the program.

Returns
The number of modules in the program.

Definition at line 611 of file Program.cpp.

◆ getNumberOfObservationLabels()

std::size_t storm::prism::Program::getNumberOfObservationLabels ( ) const

Retrieves the number of observation labels in the program.

Returns
The number of labels in the program.

Definition at line 904 of file Program.cpp.

◆ getNumberOfPlayers()

std::size_t storm::prism::Program::getNumberOfPlayers ( ) const

Retrieves the number of players in the program.

Returns
The number of players in the program.

Definition at line 566 of file Program.cpp.

◆ getNumberOfRewardModels()

std::size_t storm::prism::Program::getNumberOfRewardModels ( ) const

Retrieves the number of reward models in the program.

Returns
The number of reward models in the program.

Definition at line 812 of file Program.cpp.

◆ getNumberOfUnlabeledCommands()

uint64_t storm::prism::Program::getNumberOfUnlabeledCommands ( ) const

Definition at line 637 of file Program.cpp.

◆ getObservationLabels()

std::vector< ObservationLabel > const & storm::prism::Program::getObservationLabels ( ) const

Retrieves all observation labels that are defined by this program.

Returns
A set of observation labels

Definition at line 900 of file Program.cpp.

◆ getOptionalSystemCompositionConstruct()

boost::optional< SystemCompositionConstruct > storm::prism::Program::getOptionalSystemCompositionConstruct ( ) const

Retrieves the system composition construct (if any) and none otherwise.

Returns
The system composition construct specified by the program or none.

Definition at line 718 of file Program.cpp.

◆ getPlayerNameToIndexMapping()

std::map< std::string, storm::storage::PlayerIndex > const & storm::prism::Program::getPlayerNameToIndexMapping ( ) const
Returns
Retrieves the mapping of player names to their indices.

Definition at line 574 of file Program.cpp.

◆ getPlayers()

std::vector< Player > const & storm::prism::Program::getPlayers ( ) const

Retrieves the players of the program.

Returns
The players of the program.

Definition at line 562 of file Program.cpp.

◆ getPossiblySynchronizingCommands()

storm::storage::BitVector const & storm::prism::Program::getPossiblySynchronizingCommands ( ) const

Compute the (labelled) commands in the program that may be synchronizing.

Returns
A bitvector representing the set of commands by global command index

Definition at line 908 of file Program.cpp.

◆ getRewardModel() [1/2]

storm::prism::RewardModel const & storm::prism::Program::getRewardModel ( std::string const rewardModelName) const

Retrieves the reward model with the given name.

Parameters
rewardModelNameThe name of the reward model to return.
Returns
The reward model with the given name.

Definition at line 816 of file Program.cpp.

◆ getRewardModel() [2/2]

RewardModel const & storm::prism::Program::getRewardModel ( uint_fast64_t  index) const

Retrieves the reward model with the given index.

Parameters
indexThe index of the reward model to return.
Returns
The reward model with the given index.

Definition at line 823 of file Program.cpp.

◆ getRewardModels()

std::vector< storm::prism::RewardModel > const & storm::prism::Program::getRewardModels ( ) const

Retrieves the reward models of the program.

Returns
The reward models of the program.

Definition at line 808 of file Program.cpp.

◆ getSubstitutionForRenamedModule()

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.

◆ getSynchronizingActionIndices()

std::set< uint_fast64_t > const & storm::prism::Program::getSynchronizingActionIndices ( ) const

Retrieves the set of synchronizing action indices present in the program.

Returns
The set of synchronizing action indices present in the program.

Definition at line 738 of file Program.cpp.

◆ getSystemCompositionConstruct()

SystemCompositionConstruct const & storm::prism::Program::getSystemCompositionConstruct ( ) const

If the program specifies a system composition construct, this method retrieves it.

Returns
The system composition construct as specified by the program.

Definition at line 714 of file Program.cpp.

◆ getUndefinedConstants()

std::vector< std::reference_wrapper< storm::prism::Constant const > > storm::prism::Program::getUndefinedConstants ( ) const

Retrieves the undefined constants in the program.

Returns
The undefined constants in the program.

Definition at line 368 of file Program.cpp.

◆ getUndefinedConstantsAsString()

std::string storm::prism::Program::getUndefinedConstantsAsString ( ) const

Retrieves the undefined constants in the program as a comma-separated string.

Returns
A string with the undefined constants in the program, separated by a comma

Definition at line 378 of file Program.cpp.

◆ globalBooleanVariableExists()

bool storm::prism::Program::globalBooleanVariableExists ( std::string const variableName) const

Retrieves whether a global Boolean variable with the given name exists.

Parameters
variableNameThe name of the variable
Returns
true iff a global variable of type Boolean with the given name exists.

Definition at line 528 of file Program.cpp.

◆ globalIntegerVariableExists()

bool storm::prism::Program::globalIntegerVariableExists ( std::string const variableName) const

Retrieves whether a global Integer variable with the given name exists.

Parameters
variableNameThe name of the variable
Returns
true iff a global variable of type Integer with the given name exists.

Definition at line 532 of file Program.cpp.

◆ hasAction() [1/2]

bool storm::prism::Program::hasAction ( std::string const actionName) const

Retrieves whether the program has an action with the given name.

Returns
True iff the program has an action with the given name.

Definition at line 754 of file Program.cpp.

◆ hasAction() [2/2]

bool storm::prism::Program::hasAction ( uint_fast64_t const actionIndex) const

Retrieves whether the program has an action with the given index.

Returns
True iff the program has an action with the given index.

Definition at line 758 of file Program.cpp.

◆ hasConstant()

bool storm::prism::Program::hasConstant ( std::string const constantName) const

Retrieves whether the given constant exists in the program.

Parameters
constantNameThe name of the constant to search.
Returns
True iff the constant exists in the program.

Definition at line 393 of file Program.cpp.

◆ hasInitialConstruct()

bool storm::prism::Program::hasInitialConstruct ( ) const

Retrieves whether the program specifies an initial construct.

Definition at line 645 of file Program.cpp.

◆ hasLabel()

bool storm::prism::Program::hasLabel ( std::string const labelName) const

Checks whether the program has a label with the given name.

Parameters
labelNameThe label of the program.
Returns
True iff the label of the program.

Definition at line 828 of file Program.cpp.

◆ hasModule()

bool storm::prism::Program::hasModule ( std::string const moduleName) const

Retrieves whether the program has a module with the given name.

Returns
True iff a module with the given name exists.

Definition at line 619 of file Program.cpp.

◆ hasRewardModel() [1/2]

bool storm::prism::Program::hasRewardModel ( ) const

Retrieves whether the program has reward models.

Returns
True iff the program has at least one reward model.

Definition at line 799 of file Program.cpp.

◆ hasRewardModel() [2/2]

bool storm::prism::Program::hasRewardModel ( std::string const name) const

Retrieves whether the program has a reward model with the given name.

Parameters
nameThe name of the reward model to look for.
Returns
True iff the program has a reward model with the given name.

Definition at line 803 of file Program.cpp.

◆ hasUnboundedVariables()

bool storm::prism::Program::hasUnboundedVariables ( ) const
Returns
True iff the program contains at least one variable with infinite domain

Definition at line 271 of file Program.cpp.

◆ hasUndefinedConstants()

bool storm::prism::Program::hasUndefinedConstants ( ) const

Retrieves whether there are undefined constants of any type in the program.

Returns
True iff there are undefined constants of any type in the program.

Definition at line 285 of file Program.cpp.

◆ isDeterministicModel()

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.

◆ isDiscreteTimeModel()

bool storm::prism::Program::isDiscreteTimeModel ( ) const

Retrieves whether the model is a discrete-time model, i.e.

a DTMC or an MDP.

Returns
True iff the model is a discrete-time model.

Definition at line 251 of file Program.cpp.

◆ isPartiallyObservable()

bool storm::prism::Program::isPartiallyObservable ( ) const

Retrieves whether the model has restricted observability.

Definition at line 259 of file Program.cpp.

◆ labelUnlabelledCommands()

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.

Parameters
nameSuggestionsOptional suggestions that map command indices to names
Returns

Definition at line 1152 of file Program.cpp.

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ removeLabel()

void storm::prism::Program::removeLabel ( std::string const name)

Removes the label with the given name from the program.

Parameters
nameThe name of a label that exists within the program.

Definition at line 873 of file Program.cpp.

◆ removeRewardModels()

void storm::prism::Program::removeRewardModels ( )

Definition at line 879 of file Program.cpp.

◆ replaceConstantByVariable()

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.

Note
If the given constant appears at positions where a variable would be invalid (e.g. variable bounds or the definition of another constant), the resulting program is malformed.
Returns

Definition at line 1205 of file Program.cpp.

◆ replaceVariableInitializationByInitExpression()

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.

Returns

Definition at line 1184 of file Program.cpp.

◆ restrictCommands()

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.

Parameters
indexSetThe set of indices for which to keep the commands.

Definition at line 912 of file Program.cpp.

◆ simplify()

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.

Returns
A simplified, equivalent program.

Definition at line 1803 of file Program.cpp.

◆ specifiesSystemComposition()

bool storm::prism::Program::specifiesSystemComposition ( ) const

Retrieves whether the program specifies a system composition in terms of process algebra operations over the modules.

Returns
True iff the program specifies a system composition.

Definition at line 710 of file Program.cpp.

◆ substituteConstants()

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.

Returns
The resulting program that only contains expressions over variables of the program (and maybe formulas).

Definition at line 1026 of file Program.cpp.

◆ substituteConstantsFormulas()

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.

Returns
The resulting program that only contains expressions over variables of the program.

Definition at line 1078 of file Program.cpp.

◆ substituteFormulas()

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.

Returns
The resulting program that only contains expressions over variables of the program (and maybe constants).

Definition at line 1030 of file Program.cpp.

◆ substituteNonStandardPredicates()

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.

◆ toJani() [1/2]

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.

◆ toJani() [2/2]

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.

Returns
The jani model of this and either the new set of properties or an empty vector if no renamings were necessary

Definition at line 2329 of file Program.cpp.

◆ undefinedConstantsAreGraphPreserving()

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.

Returns
True iff the undefined constants are graph-preserving.

Definition at line 294 of file Program.cpp.

◆ updateInitialStatesExpression()

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.

◆ usedConstants()

std::vector< Constant > storm::prism::Program::usedConstants ( ) const

Retrieves the constants that are actually used in the program.

Returns

Definition at line 2165 of file Program.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<< ( std::ostream &  stream,
Program const program 
)
friend

Definition at line 2405 of file Program.cpp.


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