#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

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.

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

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)

Detailed Description

Definition at line 32 of file Program.h.

Member Enumeration Documentation

◆ ModelType

enum class storm::prism::Program::ModelType

strong

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

enum class storm::prism::Program::ValidityCheckLevel : unsigned

strong

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

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.

◆ 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

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.

◆ 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

constantDefinitions A 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

labelSet The 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

smtSolverFactory an 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

actionName The 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

actionIndex The 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

includeConstants Whether 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

negated A 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

constantName The 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

variableName The 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

variableName The 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

labelName The 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

moduleName The 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

index The 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

globalCommandIndex the 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

variableName The 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

action The 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

actionIndex The 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

rewardModelName The 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

index The 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

variableName The 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

variableName The 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

constantName The 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

labelName The 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

name	The 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

nameSuggestions Optional suggestions that map command indices to names

Returns

Definition at line 1152 of file Program.cpp.

◆ operator=() [1/2]

Program & storm::prism::Program::operator= ( Program && other )

default

◆ operator=() [2/2]

Program & storm::prism::Program::operator= ( Program const & other )

default

◆ removeLabel()

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

Removes the label with the given name from the program.

Parameters

name	The 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

indexSet The 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:

src/storm/storage/prism/Program.h
src/storm/storage/prism/Program.cpp

Public Types

Public Member Functions

Friends

Detailed Description

Member Enumeration Documentation

◆ ModelType

◆ ValidityCheckLevel

Constructor & Destructor Documentation

◆ Program() [1/4]

◆ Program() [2/4]

◆ Program() [3/4]

◆ Program() [4/4]

Member Function Documentation

◆ addLabel()

◆ buildActionIndexToActionNameMap()

◆ buildActionIndexToPlayerIndexMap()

◆ buildCommandIndexToActionIndex()

◆ buildCommandIndexToActionNameMap()

◆ buildModuleIndexToPlayerIndexMap()

◆ checkValidity()

◆ defineUndefinedConstants()

◆ filterLabels()

◆ flattenModules()

◆ getActionIndex()

◆ getActionName()

◆ getActionNameToIndexMapping()

◆ getActions()

◆ getAllExpressionVariables()

◆ getAllGuards()

◆ getAllRangeExpressions()

◆ getConstant()

◆ getConstants()

◆ getConstantsFormulasSubstitution()

◆ getConstantsSubstitution()

◆ getDefaultSystemComposition()

◆ getFinalRenamingOfModule()

◆ getFormulas()

◆ getFormulasSubstitution()

◆ getGlobalBooleanVariable()

◆ getGlobalBooleanVariables()

◆ getGlobalIntegerVariable()

◆ getGlobalIntegerVariables()

◆ getIndexOfPlayer()

◆ getInitialStatesExpression()

◆ getLabelExpression()

◆ getLabels()

◆ getLabelToExpressionMapping()

◆ getManager()

◆ getModelType()

◆ getModule() [1/2]

◆ getModule() [2/2]

◆ getModuleCommandIndexByGlobalCommandIndex()

◆ getModuleIndexByVariable()

◆ getModuleIndicesByAction()

◆ getModuleIndicesByActionIndex()

◆ getModules()

◆ getNumberOfCommands()

◆ getNumberOfConstants()

◆ getNumberOfFormulas()

◆ getNumberOfGlobalBooleanVariables()

◆ getNumberOfGlobalIntegerVariables()

◆ getNumberOfLabels()

◆ getNumberOfModules()

◆ getNumberOfObservationLabels()

◆ getNumberOfPlayers()

◆ getNumberOfRewardModels()

◆ getNumberOfUnlabeledCommands()

◆ getObservationLabels()

◆ getOptionalSystemCompositionConstruct()

◆ getPlayerNameToIndexMapping()

◆ getPlayers()

◆ getPossiblySynchronizingCommands()

◆ getRewardModel() [1/2]

◆ getRewardModel() [2/2]

◆ getRewardModels()

◆ getSubstitutionForRenamedModule()

◆ getSynchronizingActionIndices()

◆ getSystemCompositionConstruct()

◆ getUndefinedConstants()

◆ getUndefinedConstantsAsString()