storm::utility::dd Namespace Reference

Functions
template<storm::dd::DdType Type>
std::pair< storm::dd::Bdd< Type >, uint64_t >	computeReachableStates (storm::dd::Bdd< Type > const &initialStates, storm::dd::Bdd< Type > const &transitions, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables)
template<storm::dd::DdType Type>
storm::dd::Bdd< Type >	computeBackwardsReachableStates (storm::dd::Bdd< Type > const &initialStates, storm::dd::Bdd< Type > const &constraintStates, storm::dd::Bdd< Type > const &transitions, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables)
template<storm::dd::DdType Type>
storm::dd::Bdd< Type >	getRowColumnDiagonal (storm::dd::DdManager< Type > const &ddManager, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs)
template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, uint64_t >	computeReachableStates (storm::dd::Bdd< storm::dd::DdType::CUDD > const &initialStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitions, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables)
template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, uint64_t >	computeReachableStates (storm::dd::Bdd< storm::dd::DdType::Sylvan > const &initialStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitions, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	computeBackwardsReachableStates (storm::dd::Bdd< storm::dd::DdType::CUDD > const &initialStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &constraintStates, storm::dd::Bdd< storm::dd::DdType::CUDD > const &transitions, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	computeBackwardsReachableStates (storm::dd::Bdd< storm::dd::DdType::Sylvan > const &initialStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &constraintStates, storm::dd::Bdd< storm::dd::DdType::Sylvan > const &transitions, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables)
template storm::dd::Bdd< storm::dd::DdType::CUDD >	getRowColumnDiagonal (storm::dd::DdManager< storm::dd::DdType::CUDD > const &ddManager, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs)
template storm::dd::Bdd< storm::dd::DdType::Sylvan >	getRowColumnDiagonal (storm::dd::DdManager< storm::dd::DdType::Sylvan > const &ddManager, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs)
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Add< Type, ValueType >	getRowColumnDiagonal (storm::dd::DdManager< Type > const &ddManager, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs)

Function Documentation

computeBackwardsReachableStates() [1/3]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::dd::computeBackwardsReachableStates	(	storm::dd::Bdd< storm::dd::DdType::CUDD > const &	initialStates,
		storm::dd::Bdd< storm::dd::DdType::CUDD > const &	constraintStates,
		storm::dd::Bdd< storm::dd::DdType::CUDD > const &	transitions,
		std::set< storm::expressions::Variable > const &	rowMetaVariables,
		std::set< storm::expressions::Variable > const &	columnMetaVariables
	)

computeBackwardsReachableStates() [2/3]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::dd::computeBackwardsReachableStates	(	storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	initialStates,
		storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	constraintStates,
		storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	transitions,
		std::set< storm::expressions::Variable > const &	rowMetaVariables,
		std::set< storm::expressions::Variable > const &	columnMetaVariables
	)

computeBackwardsReachableStates() [3/3]

template<storm::dd::DdType Type>

storm::dd::Bdd< Type > storm::utility::dd::computeBackwardsReachableStates	(	storm::dd::Bdd< Type > const &	initialStates,
		storm::dd::Bdd< Type > const &	constraintStates,
		storm::dd::Bdd< Type > const &	transitions,
		std::set< storm::expressions::Variable > const &	rowMetaVariables,
		std::set< storm::expressions::Variable > const &	columnMetaVariables
	)

Definition at line 53 of file dd.cpp.

computeReachableStates() [1/3]

template std::pair< storm::dd::Bdd< storm::dd::DdType::CUDD >, uint64_t > storm::utility::dd::computeReachableStates	(	storm::dd::Bdd< storm::dd::DdType::CUDD > const &	initialStates,
		storm::dd::Bdd< storm::dd::DdType::CUDD > const &	transitions,
		std::set< storm::expressions::Variable > const &	rowMetaVariables,
		std::set< storm::expressions::Variable > const &	columnMetaVariables
	)

computeReachableStates() [2/3]

template std::pair< storm::dd::Bdd< storm::dd::DdType::Sylvan >, uint64_t > storm::utility::dd::computeReachableStates	(	storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	initialStates,
		storm::dd::Bdd< storm::dd::DdType::Sylvan > const &	transitions,
		std::set< storm::expressions::Variable > const &	rowMetaVariables,
		std::set< storm::expressions::Variable > const &	columnMetaVariables
	)

computeReachableStates() [3/3]

template<storm::dd::DdType Type>

std::pair< storm::dd::Bdd< Type >, uint64_t > storm::utility::dd::computeReachableStates	(	storm::dd::Bdd< Type > const &	initialStates,
		storm::dd::Bdd< Type > const &	transitions,
		std::set< storm::expressions::Variable > const &	rowMetaVariables,
		std::set< storm::expressions::Variable > const &	columnMetaVariables
	)

Definition at line 16 of file dd.cpp.

getRowColumnDiagonal() [1/4]

template storm::dd::Bdd< storm::dd::DdType::CUDD > storm::utility::dd::getRowColumnDiagonal	(	storm::dd::DdManager< storm::dd::DdType::CUDD > const &	ddManager,
		std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	rowColumnMetaVariablePairs
	)

getRowColumnDiagonal() [2/4]

template storm::dd::Bdd< storm::dd::DdType::Sylvan > storm::utility::dd::getRowColumnDiagonal	(	storm::dd::DdManager< storm::dd::DdType::Sylvan > const &	ddManager,
		std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	rowColumnMetaVariablePairs
	)

getRowColumnDiagonal() [3/4]

template<storm::dd::DdType Type>

storm::dd::Bdd< Type > storm::utility::dd::getRowColumnDiagonal	(	storm::dd::DdManager< Type > const &	ddManager,
		std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	rowColumnMetaVariablePairs
	)

Definition at line 91 of file dd.cpp.

getRowColumnDiagonal() [4/4]

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

storm::dd::Add< Type, ValueType > storm::utility::dd::getRowColumnDiagonal	(	storm::dd::DdManager< Type > const &	ddManager,
		std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	rowColumnMetaVariablePairs
	)