#include <Model.h>

Public Member Functions
	Model ()
	Creates an uninitialized model.

	Model (std::string const &name, ModelType const &modelType, uint64_t version=1, boost::optional< std::shared_ptr< storm::expressions::ExpressionManager > > const &expressionManager=boost::none)
	Creates an empty model with the given type.

	Model (Model const &other)
	Copies the given model.

Model &	operator= (Model const &other)
	Copy-assigns the given model.

	Model (Model &&other)

Model &	operator= (Model &&other)

storm::expressions::ExpressionManager &	getManager () const
	Retrieves the expression manager responsible for the expressions in the model.

uint64_t	getJaniVersion () const
	Retrieves the JANI-version of the model.

ModelType const &	getModelType () const
	Retrieves the type of the model.

void	setModelType (ModelType const &)
	Changes (only) the type declaration of the model.

ModelFeatures const &	getModelFeatures () const
	Retrieves the enabled model features.

ModelFeatures &	getModelFeatures ()
	Retrieves the enabled model features.

std::string const &	getName () const
	Retrieves the name of the model.

void	setName (std::string const &newName)
	Sets the name of the model.

Model	flattenComposition (std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory=std::make_shared< storm::utility::solver::SmtSolverFactory >()) const
	Flatten the composition to obtain an equivalent model that contains exactly one automaton that has the standard composition.

bool	hasAction (std::string const &name) const
	Checks whether the model has an action with the given name.

uint64_t	getActionIndex (std::string const &name) const
	Get the index of the action.

std::unordered_map< std::string, uint64_t > const &	getActionToIndexMap () const
	Retrieves the mapping from action names to their indices.

uint64_t	addAction (Action const &action)
	Adds an action to the model.

Action const &	getAction (uint64_t index) const
	Retrieves the action with the given index.

std::vector< Action > const &	getActions () const
	Retrieves the actions of the model.

std::map< uint64_t, std::string >	getActionIndexToNameMap () const
	Builds a map with action indices mapped to their names.

storm::storage::FlatSet< uint64_t > const &	getNonsilentActionIndices () const
	Retrieves all non-silent action indices of the model.

void	addConstant (Constant const &constant)
	Adds the given constant to the model.

bool	hasConstant (std::string const &name) const
	Retrieves whether the model has a constant with the given name.

void	removeConstant (std::string const &name)
	Removes (without checks) a constant from the model.

std::vector< Constant > const &	getConstants () const
	Retrieves the constants of the model.

std::vector< Constant > &	getConstants ()
	Retrieves the constants of the model.

Constant const &	getConstant (std::string const &name) const
	Retrieves the constant with the given name (if any).

Variable const &	addVariable (Variable const &variable)
	Adds the given variable to this model.

VariableSet &	getGlobalVariables ()
	Retrieves the variables of this automaton.

VariableSet const &	getGlobalVariables () const
	Retrieves the variables of this automaton.

std::set< storm::expressions::Variable >	getAllExpressionVariables (bool includeLocationExpressionVariables=false) const
	Retrieves all expression variables used by this model.

std::set< storm::expressions::Variable >	getAllLocationExpressionVariables () const
	Retrieves all location expression variables used by this model.

bool	hasGlobalVariable (std::string const &name) const
	Retrieves whether this model has a global variable with the given name.

Variable const &	getGlobalVariable (std::string const &name) const
	Retrieves the global variable with the given name if one exists.

bool	hasNonGlobalTransientVariable () const
	Retrieves whether this model has a non-global transient variable.

FunctionDefinition const &	addFunctionDefinition (FunctionDefinition const &functionDefinition)
	Adds the given function definition.

std::unordered_map< std::string, FunctionDefinition > const &	getGlobalFunctionDefinitions () const
	Retrieves all global function definitions.

std::unordered_map< std::string, FunctionDefinition > &	getGlobalFunctionDefinitions ()
	Retrieves all global function definitions.

storm::expressions::ExpressionManager &	getExpressionManager () const
	Retrieves the manager responsible for the expressions in the JANI model.

bool	hasNonTrivialRewardExpression () const
	Returns true iff there is a non-trivial reward model, i.e., a reward model that does not consist of a single, global, numerical, transient variable.

bool	isNonTrivialRewardModelExpression (std::string const &identifier) const
	Returns true iff the given identifier corresponds to a non-trivial reward expression i.e., a reward model that does not consist of a single, global, numerical, transient variable.

bool	addNonTrivialRewardExpression (std::string const &identifier, storm::expressions::Expression const &rewardExpression)
	Adds a reward expression, i.e., a reward model that does not consist of a single, global, numerical, transient variable.

storm::expressions::Expression	getRewardModelExpression (std::string const &identifier) const
	Retrieves the defining reward expression of the reward model with the given identifier.

std::vector< std::pair< std::string, storm::expressions::Expression > >	getAllRewardModelExpressions () const
	Retrieves all available reward model names and expressions of the model.

std::unordered_map< std::string, storm::expressions::Expression > const &	getNonTrivialRewardExpressions () const
	Retrieves all available non-trivial reward model names and expressions of the model.

std::unordered_map< std::string, storm::expressions::Expression > &	getNonTrivialRewardExpressions ()
	Retrieves all available non-trivial reward model names and expressions of the model.

uint64_t	addAutomaton (Automaton const &automaton)
	Adds the given automaton to the automata of this model.

std::vector< Automaton > &	getAutomata ()
	Retrieves the automata of the model.

std::vector< Automaton > const &	getAutomata () const
	Retrieves the automata of the model.

void	replaceAutomaton (uint64_t index, Automaton const &newAutomaton)
	Replaces the automaton at index with a new automaton.

bool	hasAutomaton (std::string const &name) const
	Rerieves whether there exists an automaton with the given name.

Automaton &	getAutomaton (std::string const &name)
	Retrieves the automaton with the given name.

Automaton &	getAutomaton (uint64_t index)
	Retrieves the automaton with the given index.

Automaton const &	getAutomaton (uint64_t index) const
	Retrieves the automaton with the given index.

Automaton const &	getAutomaton (std::string const &name) const
	Retrieves the automaton with the given name.

uint64_t	getAutomatonIndex (std::string const &name) const
	Retrieves the index of the given automaton.

std::size_t	getNumberOfAutomata () const
	Retrieves the number of automata in this model.

std::size_t	getNumberOfEdges () const
	Retrieves the total number of edges in this model.

std::size_t	getTotalNumberOfNonTransientVariables () const
	Number of global and local variables.

InformationObject	getModelInformation () const
	Returns various information of this model.

void	setSystemComposition (std::shared_ptr< Composition > const &composition)
	Sets the system composition expression of the JANI model.

void	setStandardSystemComposition ()
	Sets the system composition to be the fully-synchronizing parallel composition of all automat.

std::shared_ptr< Composition >	getStandardSystemComposition () const
	Gets the system composition as the standard, fully-synchronizing parallel composition.

Composition const &	getSystemComposition () const
	Retrieves the system composition expression.

void	simplifyComposition ()
	Attempts to simplify the composition.

std::set< std::string >	getActionNames (bool includeSilent=true) const
	Retrieves the set of action names.

Model	defineUndefinedConstants (std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions) const
	Defines the undefined constants of the model by the given expressions.

bool	hasUndefinedConstants () const
	Retrieves whether the model still has undefined constants.

std::vector< std::reference_wrapper< Constant const > >	getUndefinedConstants () const
	Retrieves all undefined constants of the model.

Model &	replaceUnassignedVariablesWithConstants ()
	Replaces each variable to which we never assign a value with a constant.

Model &	substituteConstantsInPlace (bool const substituteTranscendentalNumbers)
	Substitutes all constants in all expressions of the model.

Model	substituteConstants () const
	Substitutes all constants in all expressions of the model.

std::map< storm::expressions::Variable, storm::expressions::Expression >	getConstantsSubstitution () const
	Retrieves a mapping from expression variables associated with defined constants of the model to their (the constants') defining expression.

void	substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution, bool const substituteTranscendentalNumbers)
	Substitutes all expression variables in all expressions of the model.

void	substituteFunctions ()
	Substitutes all function calls with the corresponding function definition.

void	substituteFunctions (std::vector< Property > &properties)

Model	substituteConstantsFunctionsTranscendentals () const

bool	containsArrayVariables () const
	Returns true if at least one array variable occurs in the model.

ArrayEliminatorData	eliminateArrays (bool keepNonTrivialArrayAccess=false)
	Eliminates occurring array variables and expressions by replacing array variables by multiple basic variables.

void	eliminateArrays (std::vector< Property > &properties)
	Eliminates occurring array variables and expressions by replacing array variables by multiple basic variables.

ModelFeatures	restrictToFeatures (ModelFeatures const &modelFeatures)
	Attempts to eliminate all features of this model that are not in the given set of features.

ModelFeatures	restrictToFeatures (ModelFeatures const &modelFeatures, std::vector< Property > &properties)
	Attempts to eliminate all features of this model and the given properties that are not in the given set of features.

bool	hasInitialStatesRestriction () const
	Retrieves whether there is an expression restricting the legal initial values of the global variables.

bool	hasNonTrivialInitialStates () const
	Retrieves whether there are non-trivial initial states in the model or any of the contained automata.

void	setInitialStatesRestriction (storm::expressions::Expression const &initialStatesRestriction)
	Sets the expression restricting the legal initial values of the global variables.

storm::expressions::Expression const &	getInitialStatesRestriction () const
	Gets the expression restricting the legal initial values of the global variables.

storm::expressions::Expression	getInitialStatesExpression () const
	Retrieves the expression defining the legal initial values of the variables.

bool	hasTrivialInitialStatesExpression () const
	Retrieves whether the initial states expression is trivial in the sense that no automaton has an initial states restriction and all variables have initial values.

storm::expressions::Expression	getInitialStatesExpression (std::vector< std::reference_wrapper< storm::jani::Automaton const > > const &automata) const
	Retrieves the expression defining the legal initial values of the variables.

bool	isDeterministicModel () const
	Determines whether this model is a deterministic one in the sense that each state only has one choice.

bool	isDiscreteTimeModel () const
	Determines whether this model is a discrete-time model.

std::vector< storm::expressions::Expression >	getAllRangeExpressions (std::vector< std::reference_wrapper< storm::jani::Automaton const > > const &automata={}) const
	Retrieves a list of expressions that characterize the legal values of the variables in this model.

bool	hasStandardComposition () const
	Retrieves whether this model has the standard composition, that is it composes all automata in parallel and synchronizes over all common actions.

bool	hasStandardCompliantComposition () const
	Checks whether the composition has no nesting.

void	finalize ()
	After adding all components to the model, this method has to be called.

void	checkValid () const
	Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.

storm::expressions::Expression	getLabelExpression (Variable const &transientVariable, std::vector< std::reference_wrapper< Automaton const > > const &automata) const
	Creates the expression that characterizes all states in which the provided transient boolean variable is true.

storm::expressions::Expression	getLabelExpression (Variable const &transientVariable) const
	Creates the expression that characterizes all states in which the provided transient boolean variable is true.

bool	undefinedConstantsAreGraphPreserving () const
	Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.

void	liftTransientEdgeDestinationAssignments (int64_t maxLevel=0)
	Lifts the common edge destination assignments of transient variables to edge assignments.

bool	hasTransientEdgeDestinationAssignments () const
	Retrieves whether there is any transient edge destination assignment in the model.

bool	usesAssignmentLevels (bool onlyTransient=false) const
	Retrieves whether the model uses an assignment level other than zero.

bool	isLinear () const
	Checks the model for linearity.

void	makeStandardJaniCompliant ()

void	pushEdgeAssignmentsToDestinations ()

bool	reusesActionsInComposition () const
	Checks whether in the composition, actions are reused: That is, if the model is put in parallel composition and the same action potentially leads to multiple edges from the same state.

Model	restrictEdges (storm::storage::FlatSet< uint_fast64_t > const &automataAndEdgeIndices) const
	Creates a new model that only contains the selected edges.

void	writeDotToStream (std::ostream &outStream=std::cout) const

Static Public Member Functions
static uint64_t	encodeAutomatonAndEdgeIndices (uint64_t automatonIndex, uint64_t edgeIndex)
	Encode and decode a tuple of automaton and edge index in one 64-bit index.

static std::pair< uint64_t, uint64_t >	decodeAutomatonAndEdgeIndices (uint64_t index)

Static Public Attributes
static const std::string	SILENT_ACTION_NAME = ""
	The name of the silent action.

static const uint64_t	SILENT_ACTION_INDEX = 0
	The index of the silent action.

Friends
class	Exporter

Detailed Description

Definition at line 35 of file Model.h.

Constructor & Destructor Documentation

◆ Model() [1/4]

storm::jani::Model::Model ( )

Creates an uninitialized model.

Definition at line 47 of file Model.cpp.

◆ Model() [2/4]

storm::jani::Model::Model	(	std::string const &	name,
		ModelType const &	modelType,
		uint64_t	version = `1`,
		boost::optional< std::shared_ptr< storm::expressions::ExpressionManager > > const &	expressionManager = `boost::none`
	)

Creates an empty model with the given type.

Definition at line 51 of file Model.cpp.

◆ Model() [3/4]

storm::jani::Model::Model ( Model const & other )

Copies the given model.

Definition at line 69 of file Model.cpp.

◆ Model() [4/4]

storm::jani::Model::Model ( Model && other )

default

Member Function Documentation

◆ addAction()

uint64_t storm::jani::Model::addAction ( Action const & action )

Adds an action to the model.

Returns: the index for this action.

Definition at line 617 of file Model.cpp.

◆ addAutomaton()

uint64_t storm::jani::Model::addAutomaton ( Automaton const & automaton )

Adds the given automaton to the automata of this model.

Definition at line 863 of file Model.cpp.

◆ addConstant()

void storm::jani::Model::addConstant ( Constant const & constant )

Adds the given constant to the model.

Definition at line 654 of file Model.cpp.

◆ addFunctionDefinition()

FunctionDefinition const & storm::jani::Model::addFunctionDefinition ( FunctionDefinition const & functionDefinition )

Adds the given function definition.

Definition at line 774 of file Model.cpp.

◆ addNonTrivialRewardExpression()

bool storm::jani::Model::addNonTrivialRewardExpression	(	std::string const &	identifier,
		storm::expressions::Expression const &	rewardExpression
	)

Adds a reward expression, i.e., a reward model that does not consist of a single, global, numerical, transient variable.

Returns: true if a new reward model was added and false if a reward model with this identifier is already present in the model (in which case no reward model is added)

Definition at line 801 of file Model.cpp.

◆ addVariable()

Variable const & storm::jani::Model::addVariable ( Variable const & variable )

Adds the given variable to this model.

Definition at line 717 of file Model.cpp.

◆ checkValid()

void storm::jani::Model::checkValid ( ) const

Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.

Definition at line 1405 of file Model.cpp.

◆ containsArrayVariables()

bool storm::jani::Model::containsArrayVariables ( ) const

Returns true if at least one array variable occurs in the model.

Definition at line 1219 of file Model.cpp.

◆ decodeAutomatonAndEdgeIndices()

std::pair< uint64_t, uint64_t > storm::jani::Model::decodeAutomatonAndEdgeIndices ( uint64_t index )

static

Definition at line 1593 of file Model.cpp.

◆ defineUndefinedConstants()

Model storm::jani::Model::defineUndefinedConstants ( std::map< storm::expressions::Variable, storm::expressions::Expression > const & constantDefinitions ) const

Defines the undefined constants of the model by the given expressions.

The original model is not modified, but instead a new model is created.

Definition at line 1046 of file Model.cpp.

◆ eliminateArrays() [1/2]

ArrayEliminatorData storm::jani::Model::eliminateArrays ( bool keepNonTrivialArrayAccess = false )

Eliminates occurring array variables and expressions by replacing array variables by multiple basic variables.

Parameters

keepNonTrivialArrayAccess if set, array access expressions in LValues and expressions are only replaced, if the index expression is constant.

Returns: data from the elimination. If non-trivial array accesses are kept, pointers to remaining array variables point to this data.

Definition at line 1231 of file Model.cpp.

◆ eliminateArrays() [2/2]

void storm::jani::Model::eliminateArrays ( std::vector< Property > & properties )

Eliminates occurring array variables and expressions by replacing array variables by multiple basic variables.

Parameters

properties also eliminates array expressions in the given properties

Definition at line 1236 of file Model.cpp.

◆ encodeAutomatonAndEdgeIndices()

uint64_t storm::jani::Model::encodeAutomatonAndEdgeIndices	(	uint64_t	automatonIndex,
		uint64_t	edgeIndex
	)

static

Encode and decode a tuple of automaton and edge index in one 64-bit index.

Definition at line 1589 of file Model.cpp.

◆ finalize()

void storm::jani::Model::finalize ( )

After adding all components to the model, this method has to be called.

It recursively calls finalize on all contained elements. All subsequent changes to the model require another call to this method.

Definition at line 1399 of file Model.cpp.

◆ flattenComposition()

Model storm::jani::Model::flattenComposition ( std::shared_ptr< storm::utility::solver::SmtSolverFactory > const & smtSolverFactory = std::make_shared<storm::utility::solver::SmtSolverFactory>() ) const

Flatten the composition to obtain an equivalent model that contains exactly one automaton that has the standard composition.

Parameters

smtSolverFactory A factory that can be used to create new SMT solvers.

Definition at line 442 of file Model.cpp.

◆ getAction()

Action const & storm::jani::Model::getAction ( uint64_t index ) const

Retrieves the action with the given index.

Definition at line 628 of file Model.cpp.

◆ getActionIndex()

uint64_t storm::jani::Model::getActionIndex ( std::string const & name ) const

Get the index of the action.

Parameters

the	name of the model

Returns: the index of the (unique) action with the given name, undefined if no such action is present.

Definition at line 636 of file Model.cpp.

◆ getActionIndexToNameMap()

std::map< uint64_t, std::string > storm::jani::Model::getActionIndexToNameMap ( ) const

Builds a map with action indices mapped to their names.

Definition at line 1036 of file Model.cpp.

◆ getActionNames()

std::set< std::string > storm::jani::Model::getActionNames ( bool includeSilent = true ) const

Retrieves the set of action names.

Definition at line 1026 of file Model.cpp.

◆ getActions()

std::vector< Action > const & storm::jani::Model::getActions ( ) const

Retrieves the actions of the model.

Definition at line 646 of file Model.cpp.

◆ getActionToIndexMap()

std::unordered_map< std::string, uint64_t > const & storm::jani::Model::getActionToIndexMap ( ) const

Retrieves the mapping from action names to their indices.

Definition at line 642 of file Model.cpp.

◆ getAllExpressionVariables()

std::set< storm::expressions::Variable > storm::jani::Model::getAllExpressionVariables ( bool includeLocationExpressionVariables = false ) const

Retrieves all expression variables used by this model.

Note that this does not include the location expression variables by default.

Returns: The set of expression variables used by this model.

Definition at line 729 of file Model.cpp.

◆ getAllLocationExpressionVariables()

std::set< storm::expressions::Variable > storm::jani::Model::getAllLocationExpressionVariables ( ) const

Retrieves all location expression variables used by this model.

Returns: The set of expression variables used by this model.

Definition at line 749 of file Model.cpp.

◆ getAllRangeExpressions()

std::vector< storm::expressions::Expression > storm::jani::Model::getAllRangeExpressions ( std::vector< std::reference_wrapper< storm::jani::Automaton const > > const & automata = {} ) const

Retrieves a list of expressions that characterize the legal values of the variables in this model.

Parameters

automata If provided only range expressions from these automata will be created.

Definition at line 1377 of file Model.cpp.

◆ getAllRewardModelExpressions()

std::vector< std::pair< std::string, storm::expressions::Expression > > storm::jani::Model::getAllRewardModelExpressions ( ) const

Retrieves all available reward model names and expressions of the model.

This includes defined non-trivial reward expressions as well as transient, global, numerical variables

Definition at line 841 of file Model.cpp.

◆ getAutomata() [1/2]

std::vector< Automaton > & storm::jani::Model::getAutomata ( )

Retrieves the automata of the model.

Definition at line 872 of file Model.cpp.

◆ getAutomata() [2/2]

std::vector< Automaton > const & storm::jani::Model::getAutomata ( ) const

Retrieves the automata of the model.

Definition at line 876 of file Model.cpp.

◆ getAutomaton() [1/4]

Automaton & storm::jani::Model::getAutomaton ( std::string const & name )

Retrieves the automaton with the given name.

Definition at line 888 of file Model.cpp.

◆ getAutomaton() [2/4]

Automaton const & storm::jani::Model::getAutomaton ( std::string const & name ) const

Retrieves the automaton with the given name.

Definition at line 902 of file Model.cpp.

◆ getAutomaton() [3/4]

Automaton & storm::jani::Model::getAutomaton ( uint64_t index )

Retrieves the automaton with the given index.

Definition at line 894 of file Model.cpp.

◆ getAutomaton() [4/4]

Automaton const & storm::jani::Model::getAutomaton ( uint64_t index ) const

Retrieves the automaton with the given index.

Definition at line 898 of file Model.cpp.

◆ getAutomatonIndex()

uint64_t storm::jani::Model::getAutomatonIndex ( std::string const & name ) const

Retrieves the index of the given automaton.

Definition at line 908 of file Model.cpp.

◆ getConstant()

Constant const & storm::jani::Model::getConstant ( std::string const & name ) const

Retrieves the constant with the given name (if any).

Note: the reference to the constant is invalidated whenever a new constant is added.

Definition at line 683 of file Model.cpp.

◆ getConstants() [1/2]

std::vector< Constant > & storm::jani::Model::getConstants ( )

Retrieves the constants of the model.

Definition at line 693 of file Model.cpp.

◆ getConstants() [2/2]

std::vector< Constant > const & storm::jani::Model::getConstants ( ) const

Retrieves the constants of the model.

Definition at line 689 of file Model.cpp.

◆ getConstantsSubstitution()

std::map< storm::expressions::Variable, storm::expressions::Expression > storm::jani::Model::getConstantsSubstitution ( ) const

Retrieves a mapping from expression variables associated with defined constants of the model to their (the constants') defining expression.

Definition at line 1159 of file Model.cpp.

◆ getExpressionManager()

storm::expressions::ExpressionManager & storm::jani::Model::getExpressionManager ( ) const

Retrieves the manager responsible for the expressions in the JANI model.

Definition at line 789 of file Model.cpp.

◆ getGlobalFunctionDefinitions() [1/2]

std::unordered_map< std::string, FunctionDefinition > & storm::jani::Model::getGlobalFunctionDefinitions ( )

Retrieves all global function definitions.

Definition at line 785 of file Model.cpp.

◆ getGlobalFunctionDefinitions() [2/2]

std::unordered_map< std::string, FunctionDefinition > const & storm::jani::Model::getGlobalFunctionDefinitions ( ) const

Retrieves all global function definitions.

Definition at line 781 of file Model.cpp.

◆ getGlobalVariable()

Variable const & storm::jani::Model::getGlobalVariable ( std::string const & name ) const

Retrieves the global variable with the given name if one exists.

Definition at line 761 of file Model.cpp.

◆ getGlobalVariables() [1/2]

VariableSet & storm::jani::Model::getGlobalVariables ( )

Retrieves the variables of this automaton.

Definition at line 721 of file Model.cpp.

◆ getGlobalVariables() [2/2]

VariableSet const & storm::jani::Model::getGlobalVariables ( ) const

Retrieves the variables of this automaton.

Definition at line 725 of file Model.cpp.

◆ getInitialStatesExpression() [1/2]

storm::expressions::Expression storm::jani::Model::getInitialStatesExpression ( ) const

Retrieves the expression defining the legal initial values of the variables.

Definition at line 1312 of file Model.cpp.

◆ getInitialStatesExpression() [2/2]

storm::expressions::Expression storm::jani::Model::getInitialStatesExpression ( std::vector< std::reference_wrapper< storm::jani::Automaton const > > const & automata ) const

Retrieves the expression defining the legal initial values of the variables.

Parameters

automata The resulting expression will also characterize the legal initial states for these automata.

Definition at line 1335 of file Model.cpp.

◆ getInitialStatesRestriction()

storm::expressions::Expression const & storm::jani::Model::getInitialStatesRestriction ( ) const

Gets the expression restricting the legal initial values of the global variables.

Definition at line 1288 of file Model.cpp.

◆ getJaniVersion()

uint64_t storm::jani::Model::getJaniVersion ( ) const

Retrieves the JANI-version of the model.

Definition at line 117 of file Model.cpp.

◆ getLabelExpression() [1/2]

storm::expressions::Expression storm::jani::Model::getLabelExpression ( Variable const & transientVariable ) const

Creates the expression that characterizes all states in which the provided transient boolean variable is true.

The provided location variables are used to encode the location of the automata.

Definition at line 1412 of file Model.cpp.

◆ getLabelExpression() [2/2]

storm::expressions::Expression storm::jani::Model::getLabelExpression	(	Variable const &	transientVariable,
		std::vector< std::reference_wrapper< Automaton const > > const &	automata
	)		const

Creates the expression that characterizes all states in which the provided transient boolean variable is true.

The provided location variables are used to encode the location of the automata.

Definition at line 1420 of file Model.cpp.

◆ getManager()

storm::expressions::ExpressionManager & storm::jani::Model::getManager ( ) const

Retrieves the expression manager responsible for the expressions in the model.

Definition at line 113 of file Model.cpp.

◆ getModelFeatures() [1/2]

ModelFeatures & storm::jani::Model::getModelFeatures ( )

Retrieves the enabled model features.

Definition at line 133 of file Model.cpp.

◆ getModelFeatures() [2/2]

ModelFeatures const & storm::jani::Model::getModelFeatures ( ) const

Retrieves the enabled model features.

Definition at line 129 of file Model.cpp.

◆ getModelInformation()

InformationObject storm::jani::Model::getModelInformation ( ) const

Returns various information of this model.

Definition at line 713 of file Model.cpp.

◆ getModelType()

ModelType const & storm::jani::Model::getModelType ( ) const

Retrieves the type of the model.

Definition at line 121 of file Model.cpp.

◆ getName()

std::string const & storm::jani::Model::getName ( ) const

Retrieves the name of the model.

Definition at line 137 of file Model.cpp.

◆ getNonsilentActionIndices()

storm::storage::FlatSet< uint64_t > const & storm::jani::Model::getNonsilentActionIndices ( ) const

Retrieves all non-silent action indices of the model.

Definition at line 650 of file Model.cpp.

◆ getNonTrivialRewardExpressions() [1/2]

std::unordered_map< std::string, storm::expressions::Expression > & storm::jani::Model::getNonTrivialRewardExpressions ( )

Retrieves all available non-trivial reward model names and expressions of the model.

Definition at line 859 of file Model.cpp.

◆ getNonTrivialRewardExpressions() [2/2]

std::unordered_map< std::string, storm::expressions::Expression > const & storm::jani::Model::getNonTrivialRewardExpressions ( ) const

Retrieves all available non-trivial reward model names and expressions of the model.

Definition at line 855 of file Model.cpp.

◆ getNumberOfAutomata()

std::size_t storm::jani::Model::getNumberOfAutomata ( ) const

Retrieves the number of automata in this model.

Definition at line 914 of file Model.cpp.

◆ getNumberOfEdges()

std::size_t storm::jani::Model::getNumberOfEdges ( ) const

Retrieves the total number of edges in this model.

Definition at line 697 of file Model.cpp.

◆ getRewardModelExpression()

storm::expressions::Expression storm::jani::Model::getRewardModelExpression ( std::string const & identifier ) const

Retrieves the defining reward expression of the reward model with the given identifier.

Definition at line 813 of file Model.cpp.

◆ getStandardSystemComposition()

std::shared_ptr< Composition > storm::jani::Model::getStandardSystemComposition ( ) const

Gets the system composition as the standard, fully-synchronizing parallel composition.

Definition at line 918 of file Model.cpp.

◆ getSystemComposition()

Composition const & storm::jani::Model::getSystemComposition ( ) const

Retrieves the system composition expression.

Definition at line 949 of file Model.cpp.

◆ getTotalNumberOfNonTransientVariables()

std::size_t storm::jani::Model::getTotalNumberOfNonTransientVariables ( ) const

Number of global and local variables.

Definition at line 705 of file Model.cpp.

◆ getUndefinedConstants()

std::vector< std::reference_wrapper< Constant const > > storm::jani::Model::getUndefinedConstants ( ) const

Retrieves all undefined constants of the model.

Definition at line 1092 of file Model.cpp.

◆ hasAction()

bool storm::jani::Model::hasAction ( std::string const & name ) const

Checks whether the model has an action with the given name.

Parameters

name	The name to look for.

Definition at line 632 of file Model.cpp.

◆ hasAutomaton()

bool storm::jani::Model::hasAutomaton ( std::string const & name ) const

Rerieves whether there exists an automaton with the given name.

Parameters

name

Returns

Definition at line 880 of file Model.cpp.

◆ hasConstant()

bool storm::jani::Model::hasConstant ( std::string const & name ) const

Retrieves whether the model has a constant with the given name.

Definition at line 663 of file Model.cpp.

◆ hasGlobalVariable()

bool storm::jani::Model::hasGlobalVariable ( std::string const & name ) const

Retrieves whether this model has a global variable with the given name.

Definition at line 757 of file Model.cpp.

◆ hasInitialStatesRestriction()

bool storm::jani::Model::hasInitialStatesRestriction ( ) const

Retrieves whether there is an expression restricting the legal initial values of the global variables.

Definition at line 1284 of file Model.cpp.

◆ hasNonGlobalTransientVariable()

bool storm::jani::Model::hasNonGlobalTransientVariable ( ) const

Retrieves whether this model has a non-global transient variable.

Definition at line 765 of file Model.cpp.

◆ hasNonTrivialInitialStates()

bool storm::jani::Model::hasNonTrivialInitialStates ( ) const

Retrieves whether there are non-trivial initial states in the model or any of the contained automata.

Definition at line 1292 of file Model.cpp.

◆ hasNonTrivialRewardExpression()

bool storm::jani::Model::hasNonTrivialRewardExpression ( ) const

Returns true iff there is a non-trivial reward model, i.e., a reward model that does not consist of a single, global, numerical, transient variable.

Definition at line 793 of file Model.cpp.

◆ hasStandardCompliantComposition()

bool storm::jani::Model::hasStandardCompliantComposition ( ) const

Checks whether the composition has no nesting.

Definition at line 1477 of file Model.cpp.

◆ hasStandardComposition()

bool storm::jani::Model::hasStandardComposition ( ) const

Retrieves whether this model has the standard composition, that is it composes all automata in parallel and synchronizes over all common actions.

Definition at line 1463 of file Model.cpp.

◆ hasTransientEdgeDestinationAssignments()

bool storm::jani::Model::hasTransientEdgeDestinationAssignments ( ) const

Retrieves whether there is any transient edge destination assignment in the model.

Definition at line 1551 of file Model.cpp.

◆ hasTrivialInitialStatesExpression()

bool storm::jani::Model::hasTrivialInitialStatesExpression ( ) const

Retrieves whether the initial states expression is trivial in the sense that no automaton has an initial states restriction and all variables have initial values.

Definition at line 1320 of file Model.cpp.

◆ hasUndefinedConstants()

bool storm::jani::Model::hasUndefinedConstants ( ) const

Retrieves whether the model still has undefined constants.

Definition at line 1083 of file Model.cpp.

◆ isDeterministicModel()

bool storm::jani::Model::isDeterministicModel ( ) const

Determines whether this model is a deterministic one in the sense that each state only has one choice.

Definition at line 1369 of file Model.cpp.

◆ isDiscreteTimeModel()

bool storm::jani::Model::isDiscreteTimeModel ( ) const

Determines whether this model is a discrete-time model.

Definition at line 1373 of file Model.cpp.

◆ isLinear()

bool storm::jani::Model::isLinear ( ) const

Checks the model for linearity.

A model is linear if all expressions appearing in guards and assignments are linear.

Definition at line 1569 of file Model.cpp.

◆ isNonTrivialRewardModelExpression()

bool storm::jani::Model::isNonTrivialRewardModelExpression ( std::string const & identifier ) const

Returns true iff the given identifier corresponds to a non-trivial reward expression i.e., a reward model that does not consist of a single, global, numerical, transient variable.

Definition at line 797 of file Model.cpp.

◆ liftTransientEdgeDestinationAssignments()

void storm::jani::Model::liftTransientEdgeDestinationAssignments ( int64_t maxLevel = 0 )

Lifts the common edge destination assignments of transient variables to edge assignments.

Parameters

maxLevel the maximum level of assignments that are to be lifted.

Definition at line 1545 of file Model.cpp.

◆ makeStandardJaniCompliant()

void storm::jani::Model::makeStandardJaniCompliant ( )

Definition at line 1528 of file Model.cpp.

◆ operator=() [1/2]

Model & storm::jani::Model::operator= ( Model && other )

default

◆ operator=() [2/2]

Model & storm::jani::Model::operator= ( Model const & other )

Copy-assigns the given model.

Definition at line 73 of file Model.cpp.

◆ pushEdgeAssignmentsToDestinations()

void storm::jani::Model::pushEdgeAssignmentsToDestinations ( )

Definition at line 1539 of file Model.cpp.

◆ removeConstant()

void storm::jani::Model::removeConstant ( std::string const & name )

Removes (without checks) a constant from the model.

Definition at line 667 of file Model.cpp.

◆ replaceAutomaton()

void storm::jani::Model::replaceAutomaton	(	uint64_t	index,
		Automaton const &	newAutomaton
	)

Replaces the automaton at index with a new automaton.

Parameters

index
newAutomaton

Definition at line 884 of file Model.cpp.

◆ replaceUnassignedVariablesWithConstants()

Model & storm::jani::Model::replaceUnassignedVariablesWithConstants ( )

Replaces each variable to which we never assign a value with a constant.

Definition at line 1104 of file Model.cpp.

◆ restrictEdges()

Model storm::jani::Model::restrictEdges ( storm::storage::FlatSet< uint_fast64_t > const & automataAndEdgeIndices ) const

Creates a new model that only contains the selected edges.

The edge indices encode the automata and (local) indices of the edges within the automata.

Definition at line 1597 of file Model.cpp.

◆ restrictToFeatures() [1/2]

ModelFeatures storm::jani::Model::restrictToFeatures ( ModelFeatures const & modelFeatures )

Attempts to eliminate all features of this model that are not in the given set of features.

Returns: The model features that could not be eliminated.

Definition at line 1243 of file Model.cpp.

◆ restrictToFeatures() [2/2]

ModelFeatures storm::jani::Model::restrictToFeatures	(	ModelFeatures const &	modelFeatures,
		std::vector< Property > &	properties
	)

Attempts to eliminate all features of this model and the given properties that are not in the given set of features.

Returns: The model features that could not be eliminated.

Definition at line 1248 of file Model.cpp.

◆ reusesActionsInComposition()

bool storm::jani::Model::reusesActionsInComposition ( ) const

Checks whether in the composition, actions are reused: That is, if the model is put in parallel composition and the same action potentially leads to multiple edges from the same state.

Returns

Definition at line 1582 of file Model.cpp.

◆ setInitialStatesRestriction()

void storm::jani::Model::setInitialStatesRestriction ( storm::expressions::Expression const & initialStatesRestriction )

Sets the expression restricting the legal initial values of the global variables.

Definition at line 1280 of file Model.cpp.

◆ setModelType()

void storm::jani::Model::setModelType ( ModelType const & newModelType )

Changes (only) the type declaration of the model.

Notice that this operation should be applied with great care, as it may break several algorithms. The operation is useful to e.g. make a deterministic model into a non-deterministic one.

Definition at line 125 of file Model.cpp.

◆ setName()

void storm::jani::Model::setName ( std::string const & newName )

Sets the name of the model.

Definition at line 141 of file Model.cpp.

◆ setStandardSystemComposition()

void storm::jani::Model::setStandardSystemComposition ( )

Sets the system composition to be the fully-synchronizing parallel composition of all automat.

See also: getStandardSystemComposition

Definition at line 1022 of file Model.cpp.

◆ setSystemComposition()

void storm::jani::Model::setSystemComposition ( std::shared_ptr< Composition > const & composition )

Sets the system composition expression of the JANI model.

Definition at line 1018 of file Model.cpp.

◆ simplifyComposition()

void storm::jani::Model::simplifyComposition ( )

Attempts to simplify the composition.

Right now, this only means that automata that occur multiple times in the composition will be duplicated su that each automata occurs at most once.

Definition at line 985 of file Model.cpp.

◆ substitute()

void storm::jani::Model::substitute	(	std::map< storm::expressions::Variable, storm::expressions::Expression > const &	substitution,
		bool const	substituteTranscendentalNumbers
	)

Substitutes all expression variables in all expressions of the model.

The original model is not modified, but instead a new model is created.

Definition at line 1171 of file Model.cpp.

◆ substituteConstants()

Model storm::jani::Model::substituteConstants ( ) const

Substitutes all constants in all expressions of the model.

The original model is not modified, but instead a new model is created.

Definition at line 1144 of file Model.cpp.

◆ substituteConstantsFunctionsTranscendentals()

Model storm::jani::Model::substituteConstantsFunctionsTranscendentals ( ) const

Tries to replace variables by constants (if possible).
Substitutes all constants in all expressions of the model.
Substitutes transcendental numbers by their actual value
Afterwards, all function calls are substituted with the defining expression. The original model is not modified, but instead a new model is created.

Definition at line 1151 of file Model.cpp.

◆ substituteConstantsInPlace()

Model & storm::jani::Model::substituteConstantsInPlace ( bool const substituteTranscendentalNumbers )

Substitutes all constants in all expressions of the model.

Definition at line 1109 of file Model.cpp.

◆ substituteFunctions() [1/2]

void storm::jani::Model::substituteFunctions ( )

Substitutes all function calls with the corresponding function definition.

Parameters

properties also eliminates function call expressions in the given properties

Definition at line 1210 of file Model.cpp.

◆ substituteFunctions() [2/2]

void storm::jani::Model::substituteFunctions ( std::vector< Property > & properties )

Definition at line 1215 of file Model.cpp.

◆ undefinedConstantsAreGraphPreserving()

bool storm::jani::Model::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 edge destinations as well as on the right-hand sides of transient assignments.

Definition at line 1486 of file Model.cpp.

◆ usesAssignmentLevels()

bool storm::jani::Model::usesAssignmentLevels ( bool onlyTransient = false ) const

Retrieves whether the model uses an assignment level other than zero.

Parameters

onlyTransient if set, only transient assignments are considered

Definition at line 1560 of file Model.cpp.

◆ writeDotToStream()

void storm::jani::Model::writeDotToStream ( std::ostream & outStream = std::cout ) const

Definition at line 1638 of file Model.cpp.

Friends And Related Symbol Documentation

◆ Exporter

friend class Exporter

friend

Definition at line 37 of file Model.h.

Member Data Documentation

◆ SILENT_ACTION_INDEX

const uint64_t storm::jani::Model::SILENT_ACTION_INDEX = 0

static

The index of the silent action.

Definition at line 642 of file Model.h.

◆ SILENT_ACTION_NAME

const std::string storm::jani::Model::SILENT_ACTION_NAME = ""

static

The name of the silent action.

Definition at line 639 of file Model.h.

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

src/storm/storage/jani/Model.h
src/storm/storage/jani/Model.cpp

Public Member Functions

Static Public Member Functions

Static Public Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Model() [1/4]

◆ Model() [2/4]

◆ Model() [3/4]

◆ Model() [4/4]

Member Function Documentation

◆ addAction()

◆ addAutomaton()

◆ addConstant()

◆ addFunctionDefinition()

◆ addNonTrivialRewardExpression()

◆ addVariable()

◆ checkValid()

◆ containsArrayVariables()

◆ decodeAutomatonAndEdgeIndices()

◆ defineUndefinedConstants()

◆ eliminateArrays() [1/2]

◆ eliminateArrays() [2/2]

◆ encodeAutomatonAndEdgeIndices()

◆ finalize()

◆ flattenComposition()

◆ getAction()

◆ getActionIndex()

◆ getActionIndexToNameMap()

◆ getActionNames()

◆ getActions()

◆ getActionToIndexMap()

◆ getAllExpressionVariables()

◆ getAllLocationExpressionVariables()

◆ getAllRangeExpressions()

◆ getAllRewardModelExpressions()

◆ getAutomata() [1/2]

◆ getAutomata() [2/2]

◆ getAutomaton() [1/4]

◆ getAutomaton() [2/4]

◆ getAutomaton() [3/4]

◆ getAutomaton() [4/4]

◆ getAutomatonIndex()

◆ getConstant()

◆ getConstants() [1/2]

◆ getConstants() [2/2]

◆ getConstantsSubstitution()

◆ getExpressionManager()

◆ getGlobalFunctionDefinitions() [1/2]

◆ getGlobalFunctionDefinitions() [2/2]

◆ getGlobalVariable()

◆ getGlobalVariables() [1/2]

◆ getGlobalVariables() [2/2]

◆ getInitialStatesExpression() [1/2]

◆ getInitialStatesExpression() [2/2]

◆ getInitialStatesRestriction()

◆ getJaniVersion()

◆ getLabelExpression() [1/2]

◆ getLabelExpression() [2/2]

◆ getManager()

◆ getModelFeatures() [1/2]

◆ getModelFeatures() [2/2]

◆ getModelInformation()

◆ getModelType()

◆ getName()

◆ getNonsilentActionIndices()

◆ getNonTrivialRewardExpressions() [1/2]

◆ getNonTrivialRewardExpressions() [2/2]

◆ getNumberOfAutomata()

◆ getNumberOfEdges()

◆ getRewardModelExpression()

◆ getStandardSystemComposition()

◆ getSystemComposition()

◆ getTotalNumberOfNonTransientVariables()

◆ getUndefinedConstants()

◆ hasAction()

◆ hasAutomaton()

◆ hasConstant()

◆ hasGlobalVariable()

◆ hasInitialStatesRestriction()