Concepts
concept	HasFileNames
concept	FileNameMap
concept	IsOptionalWithFileNames

Typedefs
template<typename ValueType>
using	AccumulationMode = typename storm::storage::SparseMatrixBuilder<ValueType>::AccumulationMode

Functions
template<typename ValueType, typename TargetValueType>
void	transitionMatrixToUmb (storm::storage::SparseMatrix< ValueType > const &matrix, storm::umb::UmbModel &umb, bool const normalize)
void	stateLabelingToUmb (storm::models::sparse::StateLabeling const &labeling, storm::umb::UmbModel &umb)
uint64_t	choiceOriginsToUmb (storm::storage::sparse::ChoiceOrigins const &choiceOrigins, storm::umb::UmbModel &umb)
uint64_t	choiceLabelingToUmb (storm::models::sparse::ChoiceLabeling const &labeling, storm::umb::UmbModel &umb)
template<typename TargetValueType>
void	setGenericVector (storm::umb::GenericVector &target, std::ranges::input_range auto &&values)
template<typename ValueType, typename TargetValueType>
void	rewardToUmb (std::string const &rewardModelName, storm::models::sparse::StandardRewardModel< ValueType > const &rewardModel, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::umb::UmbModel &umb)
template<typename ValueType, typename TargetValueType>
void	playerIndicesToUmb (storm::models::sparse::Smg< ValueType > const &smg, auto &playerNames, auto &stateToPlayerIndices)
template<typename ValueType>
storm::umb::Type	getExportType (ExportOptions const &options)
template<typename ValueType>
void	setIndexInformation (storm::models::sparse::Model< ValueType > const &model, storm::umb::ModelIndex &index, ExportOptions const &options)
template<typename ValueType, typename TargetValueType>
void	sparseModelToUmb (storm::models::sparse::Model< ValueType > const &model, UmbModel &umbModel, ExportOptions const &options)
void	createDirectory (storm::io::ArchiveWriter &archiveWriter, std::filesystem::path const &subdirectory)
template<typename VectorType> requires (!std::is_same_v<std::remove_cvref_t<VectorType>, storm::umb::GenericVector>)
void	writeVector (VectorType const &vector, storm::io::ArchiveWriter &archiveWriter, std::filesystem::path const &filepath)
	Write a vector to archive.
void	writeVector (GenericVector const &vector, storm::io::ArchiveWriter &target, std::filesystem::path const &filepath)
template<typename VectorType>
void	writeVector (std::optional< VectorType > const &vector, storm::io::ArchiveWriter &target, std::filesystem::path const &filepath)
void	writeIndexFile (storm::umb::ModelIndex const &index, storm::io::ArchiveWriter &archiveWriter, std::filesystem::path const &filepath)
template<typename UmbStructure> requires HasFileNames<UmbStructure>
void	exportFiles (UmbStructure const &umbStructure, storm::io::ArchiveWriter &target, std::filesystem::path const &context)
void	exportFiles (FileNameMap auto const &umbStructure, storm::io::ArchiveWriter &target, std::filesystem::path const &context)
auto	csrRange (auto &&csr, uint64_t i)
template<typename ValueType>
storm::storage::SparseMatrix< ValueType >	createBranchMatrix (storm::umb::UmbModel const &umbModel, std::ranges::input_range auto &&branchValues, AccumulationMode< ValueType > accumulationMode)
	Creates a matrix with one row per choice and one column per state, where the entry at (choice, target) is given by the values of the branches.
template<typename ValueType>
storm::storage::SparseMatrix< ValueType >	createBranchMatrix (storm::umb::UmbModel const &umbModel, storm::umb::GenericVector const &branchValues, storm::umb::SizedType const &sourceType, AccumulationMode< ValueType > accumulationMode)
template<typename ValueType>
storm::storage::SparseMatrix< ValueType >	createBranchMatrix (storm::umb::UmbModel const &umbModel, ValueType const &defaultValue, AccumulationMode< ValueType > accumulationMode)
storm::storage::BitVector	createBitVector (storm::umb::VectorType< bool > const &umbBitVector, uint64_t size)
storm::storage::BitVector	createBitVector (storm::umb::OptionalVectorType< bool > const &umbBitVector, uint64_t size)
storm::models::sparse::StateLabeling	constructStateLabeling (storm::umb::UmbModel const &umbModel)
storm::models::sparse::ChoiceLabeling	constructChoiceLabeling (storm::umb::UmbModel const &umbModel)
template<typename ValueType>
auto	constructRewardModels (storm::umb::UmbModel const &umbModel)
template<typename ValueType>
storm::storage::SparseMatrix< ValueType >	constructTransitionMatrix (storm::umb::UmbModel const &umbModel)
template<typename ValueType>
std::shared_ptr< storm::models::sparse::Model< ValueType > >	constructSparseModel (storm::umb::UmbModel const &umbModel, ImportOptions const &options)
void	warnNonStandardFiles (UmbModel const &umb, std::filesystem::path const &location)

Typedef Documentation

◆ AccumulationMode

template<typename ValueType>

using storm::umb::detail::AccumulationMode = typename storm::storage::SparseMatrixBuilder<ValueType>::AccumulationMode

Definition at line 37 of file SparseModelFromUmb.cpp.

Function Documentation

◆ choiceLabelingToUmb()

uint64_t storm::umb::detail::choiceLabelingToUmb	(	storm::models::sparse::ChoiceLabeling const &	labeling,
		storm::umb::UmbModel &	umb )

Definition at line 92 of file SparseModelToUmb.cpp.

◆ choiceOriginsToUmb()

uint64_t storm::umb::detail::choiceOriginsToUmb	(	storm::storage::sparse::ChoiceOrigins const &	choiceOrigins,
		storm::umb::UmbModel &	umb )

Definition at line 68 of file SparseModelToUmb.cpp.

◆ constructChoiceLabeling()

storm::models::sparse::ChoiceLabeling storm::umb::detail::constructChoiceLabeling ( storm::umb::UmbModel const & umbModel )

Definition at line 133 of file SparseModelFromUmb.cpp.

◆ constructRewardModels()

template<typename ValueType>

auto storm::umb::detail::constructRewardModels ( storm::umb::UmbModel const & umbModel )

Definition at line 177 of file SparseModelFromUmb.cpp.

◆ constructSparseModel()

template<typename ValueType>

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::umb::detail::constructSparseModel	(	storm::umb::UmbModel const &	umbModel,
		ImportOptions const &	options )

Definition at line 274 of file SparseModelFromUmb.cpp.

◆ constructStateLabeling()

storm::models::sparse::StateLabeling storm::umb::detail::constructStateLabeling ( storm::umb::UmbModel const & umbModel )

Definition at line 98 of file SparseModelFromUmb.cpp.

◆ constructTransitionMatrix()

template<typename ValueType>

storm::storage::SparseMatrix< ValueType > storm::umb::detail::constructTransitionMatrix ( storm::umb::UmbModel const & umbModel )

Definition at line 223 of file SparseModelFromUmb.cpp.

◆ createBitVector() [1/2]

storm::storage::BitVector storm::umb::detail::createBitVector	(	storm::umb::OptionalVectorType< bool > const &	umbBitVector,
		uint64_t	size )

Definition at line 93 of file SparseModelFromUmb.cpp.

◆ createBitVector() [2/2]

storm::storage::BitVector storm::umb::detail::createBitVector	(	storm::umb::VectorType< bool > const &	umbBitVector,
		uint64_t	size )

Definition at line 85 of file SparseModelFromUmb.cpp.

◆ createBranchMatrix() [1/3]

template<typename ValueType>

storm::storage::SparseMatrix< ValueType > storm::umb::detail::createBranchMatrix	(	storm::umb::UmbModel const &	umbModel,
		std::ranges::input_range auto &&	branchValues,
		AccumulationMode< ValueType >	accumulationMode )

Creates a matrix with one row per choice and one column per state, where the entry at (choice, target) is given by the values of the branches.

UMB allows multiple branches with the same source choice and target state, but Storm's SparseMatrix has at most one entry per row and column. The given accumulation mode specifies how the values of such branches are merged into a single entry.

Definition at line 45 of file SparseModelFromUmb.cpp.

◆ createBranchMatrix() [2/3]

template<typename ValueType>

storm::storage::SparseMatrix< ValueType > storm::umb::detail::createBranchMatrix	(	storm::umb::UmbModel const &	umbModel,
		storm::umb::GenericVector const &	branchValues,
		storm::umb::SizedType const &	sourceType,
		AccumulationMode< ValueType >	accumulationMode )

Definition at line 71 of file SparseModelFromUmb.cpp.

◆ createBranchMatrix() [3/3]

template<typename ValueType>

storm::storage::SparseMatrix< ValueType > storm::umb::detail::createBranchMatrix	(	storm::umb::UmbModel const &	umbModel,
		ValueType const &	defaultValue,
		AccumulationMode< ValueType >	accumulationMode )

Definition at line 78 of file SparseModelFromUmb.cpp.

◆ createDirectory()

void storm::umb::detail::createDirectory	(	storm::io::ArchiveWriter &	archiveWriter,
		std::filesystem::path const &	subdirectory )

Definition at line 19 of file UmbExport.cpp.

◆ csrRange()

auto storm::umb::detail::csrRange	(	auto &&	csr,
		uint64_t	i )

Definition at line 26 of file SparseModelFromUmb.cpp.

◆ exportFiles() [1/2]

void storm::umb::detail::exportFiles	(	FileNameMap auto const &	umbStructure,
		storm::io::ArchiveWriter &	target,
		std::filesystem::path const &	context )

Definition at line 75 of file UmbExport.cpp.

◆ exportFiles() [2/2]

template<typename UmbStructure>
requires HasFileNames<UmbStructure>

void storm::umb::detail::exportFiles	(	UmbStructure const &	umbStructure,
		storm::io::ArchiveWriter &	target,
		std::filesystem::path const &	context )

Definition at line 86 of file UmbExport.cpp.

◆ getExportType()

template<typename ValueType>

storm::umb::Type storm::umb::detail::getExportType ( ExportOptions const & options )

Definition at line 255 of file SparseModelToUmb.cpp.

◆ playerIndicesToUmb()

template<typename ValueType, typename TargetValueType>

void storm::umb::detail::playerIndicesToUmb	(	storm::models::sparse::Smg< ValueType > const &	smg,
		auto &	playerNames,
		auto &	stateToPlayerIndices )

Definition at line 215 of file SparseModelToUmb.cpp.

◆ rewardToUmb()

template<typename ValueType, typename TargetValueType>

void storm::umb::detail::rewardToUmb	(	std::string const &	rewardModelName,
		storm::models::sparse::StandardRewardModel< ValueType > const &	rewardModel,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::umb::UmbModel &	umb )

Definition at line 174 of file SparseModelToUmb.cpp.

◆ setGenericVector()

template<typename TargetValueType>

void storm::umb::detail::setGenericVector	(	storm::umb::GenericVector &	target,
		std::ranges::input_range auto &&	values )

Definition at line 164 of file SparseModelToUmb.cpp.

◆ setIndexInformation()

template<typename ValueType>

void storm::umb::detail::setIndexInformation	(	storm::models::sparse::Model< ValueType > const &	model,
		storm::umb::ModelIndex &	index,
		ExportOptions const &	options )

Definition at line 283 of file SparseModelToUmb.cpp.

◆ sparseModelToUmb()

template<typename ValueType, typename TargetValueType>

void storm::umb::detail::sparseModelToUmb	(	storm::models::sparse::Model< ValueType > const &	model,
		UmbModel &	umbModel,
		ExportOptions const &	options )

Definition at line 417 of file SparseModelToUmb.cpp.

◆ stateLabelingToUmb()

void storm::umb::detail::stateLabelingToUmb	(	storm::models::sparse::StateLabeling const &	labeling,
		storm::umb::UmbModel &	umb )

Definition at line 53 of file SparseModelToUmb.cpp.

◆ transitionMatrixToUmb()

template<typename ValueType, typename TargetValueType>

void storm::umb::detail::transitionMatrixToUmb	(	storm::storage::SparseMatrix< ValueType > const &	matrix,
		storm::umb::UmbModel &	umb,
		bool const	normalize )

Definition at line 28 of file SparseModelToUmb.cpp.

◆ warnNonStandardFiles()

void storm::umb::detail::warnNonStandardFiles	(	UmbModel const &	umb,
		std::filesystem::path const &	location )

Definition at line 13 of file Umb.cpp.

◆ writeIndexFile()

void storm::umb::detail::writeIndexFile	(	storm::umb::ModelIndex const &	index,
		storm::io::ArchiveWriter &	archiveWriter,
		std::filesystem::path const &	filepath )

Definition at line 57 of file UmbExport.cpp.

◆ writeVector() [1/3]

void storm::umb::detail::writeVector	(	GenericVector const &	vector,
		storm::io::ArchiveWriter &	target,
		std::filesystem::path const &	filepath )

Definition at line 33 of file UmbExport.cpp.

◆ writeVector() [2/3]

template<typename VectorType>

void storm::umb::detail::writeVector	(	std::optional< VectorType > const &	vector,
		storm::io::ArchiveWriter &	target,
		std::filesystem::path const &	filepath )

Definition at line 51 of file UmbExport.cpp.

◆ writeVector() [3/3]

template<typename VectorType>
requires (!std::is_same_v<std::remove_cvref_t<VectorType>, storm::umb::GenericVector>)

void storm::umb::detail::writeVector	(	VectorType const &	vector,
		storm::io::ArchiveWriter &	archiveWriter,
		std::filesystem::path const &	filepath )

Write a vector to archive.

The file path must have the extension .bin.

Definition at line 29 of file UmbExport.cpp.

Concepts

Typedefs

Functions

Typedef Documentation

◆ AccumulationMode

Function Documentation

◆ choiceLabelingToUmb()

◆ choiceOriginsToUmb()

◆ constructChoiceLabeling()

◆ constructRewardModels()

◆ constructSparseModel()

◆ constructStateLabeling()

◆ constructTransitionMatrix()

◆ createBitVector() [1/2]

◆ createBitVector() [2/2]

◆ createBranchMatrix() [1/3]

◆ createBranchMatrix() [2/3]

◆ createBranchMatrix() [3/3]

◆ createDirectory()

◆ csrRange()

◆ exportFiles() [1/2]

◆ exportFiles() [2/2]

◆ getExportType()

◆ playerIndicesToUmb()

◆ rewardToUmb()

◆ setGenericVector()

◆ setIndexInformation()

◆ sparseModelToUmb()

◆ stateLabelingToUmb()

◆ transitionMatrixToUmb()

◆ warnNonStandardFiles()

◆ writeIndexFile()

◆ writeVector() [1/3]

◆ writeVector() [2/3]

◆ writeVector() [3/3]