Classes
class	BeliefMdpExplorer

class	BuilderOptions

class	CombinedEdgesSystemComposer

struct	ComposerResult

class	CompositionVariableCreator

struct	CompositionVariables

class	DdJaniModelBuilder

class	DdPrismModelBuilder

struct	EdgeDestinationDd

class	ExplicitModelBuilder

class	ExplicitStateLookup

class	JaniGSPNBuilder

class	LabelOrExpression

struct	ModelComponents

class	ModuleComposer

class	ParallelCompositionBuilder
	Build a parallel composition of Markov chains. More...

class	ParameterCreator

class	ParameterCreator< Type, storm::RationalFunction >

class	RewardModelBuilder
	A structure that is used to keep track of a reward model currently being built. More...

class	RewardModelInformation

class	StateAndChoiceInformationBuilder
	This class collects information regarding the states and choices during model building. More...

class	SystemComposer

struct	TerminalStates

Enumerations
enum class	ExplorationHeuristic { BreadthFirst , LowerBoundPrio , UpperBoundPrio , GapPrio , ProbabilityPrio }

enum class	BuilderType { Explicit , Dd }

enum class	ExplorationOrder { Dfs , Bfs }

Functions
std::string	getUniqueVarName (storm::expressions::ExpressionManager const &manager, std::string name)

storm::jani::ModelFeatures	getSupportedJaniFeatures (BuilderType const &builderType)

template<typename ValueType >
bool	canHandle (BuilderType const &builderType, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional< std::vector< storm::jani::Property > > const &properties)

template bool	canHandle< double > (BuilderType const &builderType, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional< std::vector< storm::jani::Property > > const &properties)

template bool	canHandle< storm::RationalNumber > (BuilderType const &builderType, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional< std::vector< storm::jani::Property > > const &properties)

template bool	canHandle< storm::RationalFunction > (BuilderType const &builderType, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional< std::vector< storm::jani::Property > > const &properties)

template<storm::dd::DdType Type, typename ValueType >
EdgeDestinationDd< Type, ValueType >	buildEdgeDestinationDd (storm::jani::Automaton const &automaton, storm::jani::EdgeDestination const &destination, storm::dd::Bdd< Type > const &guard, CompositionVariables< Type, ValueType > const &variables)

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Add< Type, ValueType >	encodeAction (boost::optional< uint64_t > const &actionIndex, boost::optional< bool > const &markovian, CompositionVariables< Type, ValueType > const &variables)

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Add< Type, ValueType >	encodeIndex (uint64_t index, uint64_t localNondeterminismVariableOffset, uint64_t numberOfLocalNondeterminismVariables, CompositionVariables< Type, ValueType > const &variables)

template<storm::dd::DdType Type, typename ValueType >
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > >	createModel (storm::jani::ModelType const &modelType, CompositionVariables< Type, ValueType > const &variables, ModelComponents< Type, ValueType > const &modelComponents)

template<storm::dd::DdType Type, typename ValueType >
void	postprocessVariables (storm::jani::ModelType const &modelType, ComposerResult< Type, ValueType > &system, CompositionVariables< Type, ValueType > &variables)

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	postprocessSystem (storm::jani::Model const &model, ComposerResult< Type, ValueType > &system, CompositionVariables< Type, ValueType > const &variables, typename DdJaniModelBuilder< Type, ValueType >::Options const &options, std::map< std::string, storm::expressions::Expression > const &labelsToExpressionMap)

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	computeInitialStates (storm::jani::Model const &model, CompositionVariables< Type, ValueType > const &variables)

template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	fixDeadlocks (storm::jani::ModelType const &modelType, storm::dd::Add< Type, ValueType > &transitionMatrix, storm::dd::Bdd< Type > const &transitionMatrixBdd, storm::dd::Bdd< Type > const &reachableStates, CompositionVariables< Type, ValueType > const &variables)

template<storm::dd::DdType Type, typename ValueType >
std::vector< storm::expressions::Variable >	selectRewardVariables (storm::jani::Model const &model, typename DdJaniModelBuilder< Type, ValueType >::Options const &options)

template<storm::dd::DdType Type, typename ValueType >
std::unordered_map< std::string, storm::models::symbolic::StandardRewardModel< Type, ValueType > >	buildRewardModels (storm::dd::Add< Type, ValueType > const &reachableStates, storm::dd::Add< Type, ValueType > const &transitionMatrix, storm::jani::ModelType const &modelType, CompositionVariables< Type, ValueType > const &variables, ComposerResult< Type, ValueType > const &system, std::vector< storm::expressions::Variable > const &rewardVariables)

template<storm::dd::DdType Type, typename ValueType >
std::map< std::string, storm::expressions::Expression >	buildLabelExpressions (storm::jani::Model const &model, CompositionVariables< Type, ValueType > const &variables, typename DdJaniModelBuilder< Type, ValueType >::Options const &options)

template<storm::dd::DdType Type, typename ValueType >
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > >	buildInternal (storm::jani::Model const &model, typename DdJaniModelBuilder< Type, ValueType >::Options const &options, std::shared_ptr< storm::dd::DdManager< Type > > const &manager)

template<storm::dd::DdType Type, typename ValueType >
void	checkRewards (storm::dd::Add< Type, ValueType > const &rewards, std::string const &rewardType)

template<storm::dd::DdType Type>
void	checkRewards (storm::dd::Add< Type, storm::RationalFunction > const &rewards, std::string const &rewardType)

std::ostream &	operator<< (std::ostream &out, ExplorationOrder const &order)

void	getTerminalStatesFromFormula (storm::logic::Formula const &formula, std::function< void(storm::expressions::Expression const &, bool)> const &terminalExpressionCallback, std::function< void(std::string const &, bool)> const &terminalLabelCallback)
	Traverses the formula.

TerminalStates	getTerminalStatesFromFormula (storm::logic::Formula const &formula)
	Traverses the formula.

Enumeration Type Documentation

◆ BuilderType

enum class storm::builder::BuilderType

strong

Enumerator
Explicit
Dd

Definition at line 16 of file BuilderType.h.

◆ ExplorationHeuristic

enum class storm::builder::ExplorationHeuristic

strong

Enumerator
BreadthFirst
LowerBoundPrio
UpperBoundPrio
GapPrio
ProbabilityPrio

Definition at line 24 of file BeliefMdpExplorer.h.

◆ ExplorationOrder

enum class storm::builder::ExplorationOrder

strong

Enumerator
Dfs
Bfs

Definition at line 10 of file ExplorationOrder.h.

Function Documentation

◆ buildEdgeDestinationDd()

template<storm::dd::DdType Type, typename ValueType >

EdgeDestinationDd< Type, ValueType > storm::builder::buildEdgeDestinationDd	(	storm::jani::Automaton const &	automaton,
		storm::jani::EdgeDestination const &	destination,
		storm::dd::Bdd< Type > const &	guard,
		CompositionVariables< Type, ValueType > const &	variables
	)

Definition at line 580 of file DdJaniModelBuilder.cpp.

◆ buildInternal()

template<storm::dd::DdType Type, typename ValueType >

std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > storm::builder::buildInternal	(	storm::jani::Model const &	model,
		typename DdJaniModelBuilder< Type, ValueType >::Options const &	options,
		std::shared_ptr< storm::dd::DdManager< Type > > const &	manager
	)

Definition at line 2339 of file DdJaniModelBuilder.cpp.

◆ buildLabelExpressions()

template<storm::dd::DdType Type, typename ValueType >

std::map< std::string, storm::expressions::Expression > storm::builder::buildLabelExpressions	(	storm::jani::Model const &	model,
		CompositionVariables< Type, ValueType > const &	variables,
		typename DdJaniModelBuilder< Type, ValueType >::Options const &	options
	)

Definition at line 2316 of file DdJaniModelBuilder.cpp.

◆ buildRewardModels()

template<storm::dd::DdType Type, typename ValueType >

std::unordered_map< std::string, storm::models::symbolic::StandardRewardModel< Type, ValueType > > storm::builder::buildRewardModels	(	storm::dd::Add< Type, ValueType > const &	reachableStates,
		storm::dd::Add< Type, ValueType > const &	transitionMatrix,
		storm::jani::ModelType const &	modelType,
		CompositionVariables< Type, ValueType > const &	variables,
		ComposerResult< Type, ValueType > const &	system,
		std::vector< storm::expressions::Variable > const &	rewardVariables
	)

Definition at line 2279 of file DdJaniModelBuilder.cpp.

◆ canHandle()

template<typename ValueType >

bool storm::builder::canHandle	(	BuilderType const &	builderType,
		storm::storage::SymbolicModelDescription const &	modelDescription,
		boost::optional< std::vector< storm::jani::Property > > const &	properties
	)

Definition at line 31 of file BuilderType.cpp.

◆ canHandle< double >()

template bool storm::builder::canHandle< double >	(	BuilderType const &	builderType,
		storm::storage::SymbolicModelDescription const &	modelDescription,
		boost::optional< std::vector< storm::jani::Property > > const &	properties
	)

◆ canHandle< storm::RationalFunction >()

template bool storm::builder::canHandle< storm::RationalFunction >	(	BuilderType const &	builderType,
		storm::storage::SymbolicModelDescription const &	modelDescription,
		boost::optional< std::vector< storm::jani::Property > > const &	properties
	)

◆ canHandle< storm::RationalNumber >()

template bool storm::builder::canHandle< storm::RationalNumber >	(	BuilderType const &	builderType,
		storm::storage::SymbolicModelDescription const &	modelDescription,
		boost::optional< std::vector< storm::jani::Property > > const &	properties
	)

◆ checkRewards() [1/2]

template<storm::dd::DdType Type>

void storm::builder::checkRewards	(	storm::dd::Add< Type, storm::RationalFunction > const &	rewards,
		std::string const &	rewardType
	)

Definition at line 1292 of file DdPrismModelBuilder.cpp.

◆ checkRewards() [2/2]

template<storm::dd::DdType Type, typename ValueType >

void storm::builder::checkRewards	(	storm::dd::Add< Type, ValueType > const &	rewards,
		std::string const &	rewardType
	)

Definition at line 1286 of file DdPrismModelBuilder.cpp.

◆ computeInitialStates()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Bdd< Type > storm::builder::computeInitialStates	(	storm::jani::Model const &	model,
		CompositionVariables< Type, ValueType > const &	variables
	)

Definition at line 2183 of file DdJaniModelBuilder.cpp.

◆ createModel()

template<storm::dd::DdType Type, typename ValueType >

std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > storm::builder::createModel	(	storm::jani::ModelType const &	modelType,
		CompositionVariables< Type, ValueType > const &	variables,
		ModelComponents< Type, ValueType > const &	modelComponents
	)

Definition at line 2089 of file DdJaniModelBuilder.cpp.

◆ encodeAction()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Add< Type, ValueType > storm::builder::encodeAction	(	boost::optional< uint64_t > const &	actionIndex,
		boost::optional< bool > const &	markovian,
		CompositionVariables< Type, ValueType > const &	variables
	)

Definition at line 642 of file DdJaniModelBuilder.cpp.

◆ encodeIndex()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Add< Type, ValueType > storm::builder::encodeIndex	(	uint64_t	index,
		uint64_t	localNondeterminismVariableOffset,
		uint64_t	numberOfLocalNondeterminismVariables,
		CompositionVariables< Type, ValueType > const &	variables
	)

Definition at line 666 of file DdJaniModelBuilder.cpp.

◆ fixDeadlocks()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Bdd< Type > storm::builder::fixDeadlocks	(	storm::jani::ModelType const &	modelType,
		storm::dd::Add< Type, ValueType > &	transitionMatrix,
		storm::dd::Bdd< Type > const &	transitionMatrixBdd,
		storm::dd::Bdd< Type > const &	reachableStates,
		CompositionVariables< Type, ValueType > const &	variables
	)

Definition at line 2203 of file DdJaniModelBuilder.cpp.

◆ getSupportedJaniFeatures()

storm::jani::ModelFeatures storm::builder::getSupportedJaniFeatures ( BuilderType const & builderType )

Definition at line 17 of file BuilderType.cpp.

◆ getTerminalStatesFromFormula() [1/2]

TerminalStates storm::builder::getTerminalStatesFromFormula ( storm::logic::Formula const & formula )

Traverses the formula.

If an expression (or label) is found such that checking the formula does not require further exploration from a state satisfying (or violating) the expression (or label), it is inserted into the returned struct.

Definition at line 95 of file TerminalStatesGetter.cpp.

◆ getTerminalStatesFromFormula() [2/2]

void storm::builder::getTerminalStatesFromFormula	(	storm::logic::Formula const &	formula,
		std::function< void(storm::expressions::Expression const &, bool)> const &	terminalExpressionCallback,
		std::function< void(std::string const &, bool)> const &	terminalLabelCallback
	)

Traverses the formula.

If an expression (or label) is found such that checking the formula does not require further exploration from a state satisfying (or violating) the expression (or label), the corresponding callback function is called.

Parameters

formula	The formula to analyzed
terminalExpressionCallback	called on terminal expressions. The corresponding flag indicates whether exploration can stop from states satisfying (true) or violating (false) the expression
terminalLabelCallback	called on terminal labels. The corresponding flag indicates whether exploration can stop from states having (true) or not having (false) the label

Definition at line 9 of file TerminalStatesGetter.cpp.

◆ getUniqueVarName()

std::string storm::builder::getUniqueVarName	(	storm::expressions::ExpressionManager const &	manager,
		std::string	name
	)

Definition at line 278 of file JaniGSPNBuilder.cpp.

◆ operator<<()

std::ostream & storm::builder::operator<<	(	std::ostream &	out,
		ExplorationOrder const &	order
	)

Definition at line 6 of file ExplorationOrder.cpp.

◆ postprocessSystem()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Bdd< Type > storm::builder::postprocessSystem	(	storm::jani::Model const &	model,
		ComposerResult< Type, ValueType > &	system,
		CompositionVariables< Type, ValueType > const &	variables,
		typename DdJaniModelBuilder< Type, ValueType >::Options const &	options,
		std::map< std::string, storm::expressions::Expression > const &	labelsToExpressionMap
	)

Definition at line 2146 of file DdJaniModelBuilder.cpp.

◆ postprocessVariables()

template<storm::dd::DdType Type, typename ValueType >

void storm::builder::postprocessVariables	(	storm::jani::ModelType const &	modelType,
		ComposerResult< Type, ValueType > &	system,
		CompositionVariables< Type, ValueType > &	variables
	)

Definition at line 2125 of file DdJaniModelBuilder.cpp.

◆ selectRewardVariables()

template<storm::dd::DdType Type, typename ValueType >

std::vector< storm::expressions::Variable > storm::builder::selectRewardVariables	(	storm::jani::Model const &	model,
		typename DdJaniModelBuilder< Type, ValueType >::Options const &	options
	)

Definition at line 2255 of file DdJaniModelBuilder.cpp.

Classes

Enumerations

Functions

Enumeration Type Documentation

◆ BuilderType

◆ ExplorationHeuristic

◆ ExplorationOrder

Function Documentation

◆ buildEdgeDestinationDd()

◆ buildInternal()

◆ buildLabelExpressions()

◆ buildRewardModels()

◆ canHandle()

◆ canHandle< double >()

◆ canHandle< storm::RationalFunction >()

◆ canHandle< storm::RationalNumber >()

◆ checkRewards() [1/2]

◆ checkRewards() [2/2]

◆ computeInitialStates()

◆ createModel()

◆ encodeAction()

◆ encodeIndex()

◆ fixDeadlocks()

◆ getSupportedJaniFeatures()

◆ getTerminalStatesFromFormula() [1/2]

◆ getTerminalStatesFromFormula() [2/2]

◆ getUniqueVarName()

◆ operator<<()

◆ postprocessSystem()

◆ postprocessVariables()

◆ selectRewardVariables()