Namespaces
namespace	detail
namespace	internal
namespace	validation

Classes
struct	ExportOptions
struct	ImportOptions
struct	AnyValueType
class	GenericVector
struct	ModelIndex
class	StringsBuilder
struct	TypeDeclaration
struct	SizedType
class	UmbModel
	Represents a model in the UMB format. More...
struct	ValuationClassDescription
struct	ValuationDescription
class	Valuations
class	ValueEncoding

Typedefs
template<typename T>
using	VectorType = std::conditional_t<std::is_same_v<T, bool>, storm::storage::BitVector, std::vector<T>>
template<typename T>
using	OptionalVectorType = std::optional<VectorType<T>>
template<typename T>
using	TO1 = std::conditional_t<std::is_same_v<T, AnyValueType>, GenericVector, OptionalVectorType<T>>
template<typename T>
using	SEQ = TO1<T>
using	CSR = OptionalVectorType<uint64_t>

Enumerations
enum class	Type { Bool , Int , IntInterval , Uint , UintInterval , Double , DoubleInterval , Rational , RationalInterval , String }

Functions
template<typename ValueType>
storm::umb::UmbModel	sparseModelToUmb (storm::models::sparse::Model< ValueType > const &model, ExportOptions const &options)
template storm::umb::UmbModel	sparseModelToUmb< double > (storm::models::sparse::Model< double > const &model, ExportOptions const &options)
template storm::umb::UmbModel	sparseModelToUmb< storm::RationalNumber > (storm::models::sparse::Model< storm::RationalNumber > const &model, ExportOptions const &options)
template storm::umb::UmbModel	sparseModelToUmb< storm::Interval > (storm::models::sparse::Model< storm::Interval > const &model, ExportOptions const &options)
template storm::umb::UmbModel	sparseModelToUmb< storm::RationalInterval > (storm::models::sparse::Model< storm::RationalInterval > const &model, ExportOptions const &options)
void	toArchive (storm::umb::UmbModel const &umbModel, std::filesystem::path const &archivePath, ExportOptions const &options)
storm::models::ModelType	deriveModelType (storm::umb::ModelIndex const &index)
	Derives the model type from the given UMB model index.
template<typename ValueType>
bool	deriveValueType (storm::umb::ModelIndex const &index, ImportOptions const &options={})
	Returns true iff the given umb model with the given options should have ValueType as its ValueType.
template<typename ValueType>
std::shared_ptr< storm::models::sparse::Model< ValueType > >	sparseModelFromUmb (storm::umb::UmbModel const &umbModel, ImportOptions const &options={})
	Constructs a sparse model from the given UMB model.
std::shared_ptr< storm::models::ModelBase >	sparseModelFromUmb (storm::umb::UmbModel const &umbModel, ImportOptions const &options={})
	Constructs a sparse model from the given UMB model.
template std::shared_ptr< storm::models::sparse::Model< double > >	sparseModelFromUmb< double > (storm::umb::UmbModel const &umbModel, ImportOptions const &options)
template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > >	sparseModelFromUmb< storm::RationalNumber > (storm::umb::UmbModel const &umbModel, ImportOptions const &options)
template std::shared_ptr< storm::models::sparse::Model< storm::Interval > >	sparseModelFromUmb< storm::Interval > (storm::umb::UmbModel const &umbModel, ImportOptions const &options)
template std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > >	sparseModelFromUmb< storm::RationalInterval > (storm::umb::UmbModel const &umbModel, ImportOptions const &options)
storm::umb::UmbModel	importUmb (std::filesystem::path const &umbLocation, ImportOptions const &options)
auto	stringVectorView (SEQ< char > const &strings, CSR const &stringMapping)
bool	isBooleanType (Type const type)
bool	isDiscreteNumericType (Type const type)
bool	isContinuousNumericType (Type const type)
bool	isNumericType (Type const type)
bool	isIntervalType (Type const type)
bool	isStringType (Type const type)
uint64_t	defaultBitSize (Type const type)
	Returns the default size (in bits) of a type, if available.
std::string	toString (Type const type)
	Returns a string representation of the type.
bool	validate (storm::umb::UmbModel const &umbModel, std::ostream &errors)
	Validates the given UMB model and writes potential errors to the given output stream.
void	validateOrThrow (storm::umb::UmbModel const &umbModel)
	Validates the given UMB model.
template<typename ValueType>
std::shared_ptr< storm::models::sparse::Model< ValueType > >	buildModelFromUmb (std::filesystem::path const &umbLocation, ImportOptions const &options)
std::shared_ptr< storm::models::ModelBase >	buildModelFromUmb (std::filesystem::path const &umbLocation, ImportOptions const &options)
template<typename ValueType>
void	exportModelToUmb (storm::models::sparse::Model< ValueType > const &model, std::filesystem::path const &targetLocation, ExportOptions const &options)
template void	exportModelToUmb (storm::models::sparse::Model< double > const &, std::filesystem::path const &, ExportOptions const &)
template void	exportModelToUmb (storm::models::sparse::Model< storm::RationalNumber > const &, std::filesystem::path const &, ExportOptions const &)
template void	exportModelToUmb (storm::models::sparse::Model< storm::Interval > const &, std::filesystem::path const &, ExportOptions const &)
template void	exportModelToUmb (storm::models::sparse::Model< storm::RationalInterval > const &, std::filesystem::path const &, ExportOptions const &)

Variables
const std::string	DefaultAnnotationAlias = "default"

Typedef Documentation

◆ CSR

using storm::umb::CSR = OptionalVectorType<uint64_t>

Definition at line 31 of file FileTypes.h.

◆ OptionalVectorType

template<typename T>

using storm::umb::OptionalVectorType = std::optional<VectorType<T>>

Definition at line 21 of file FileTypes.h.

◆ SEQ

template<typename T>

using storm::umb::SEQ = TO1<T>

Definition at line 29 of file FileTypes.h.

◆ TO1

template<typename T>

using storm::umb::TO1 = std::conditional_t<std::is_same_v<T, AnyValueType>, GenericVector, OptionalVectorType<T>>

Definition at line 26 of file FileTypes.h.

◆ VectorType

template<typename T>

using storm::umb::VectorType = std::conditional_t<std::is_same_v<T, bool>, storm::storage::BitVector, std::vector<T>>

Definition at line 18 of file FileTypes.h.

Enumeration Type Documentation

◆ Type

enum class storm::umb::Type

strong

Enumerator
Bool
Int
IntInterval
Uint
UintInterval
Double
DoubleInterval
Rational
RationalInterval
String

Definition at line 11 of file Type.h.

Function Documentation

◆ buildModelFromUmb() [1/2]

std::shared_ptr< storm::models::ModelBase > storm::umb::buildModelFromUmb	(	std::filesystem::path const &	umbLocation,
		ImportOptions const &	options )

Definition at line 29 of file Umb.cpp.

◆ buildModelFromUmb() [2/2]

template<typename ValueType>

std::shared_ptr< storm::models::ModelBase > storm::umb::buildModelFromUmb	(	std::filesystem::path const &	umbLocation,
		ImportOptions const &	options )

Definition at line 22 of file Umb.cpp.

◆ defaultBitSize()

uint64_t storm::umb::defaultBitSize ( Type const type )

Returns the default size (in bits) of a type, if available.

Definition at line 59 of file Type.cpp.

◆ deriveModelType()

storm::models::ModelType storm::umb::deriveModelType ( storm::umb::ModelIndex const & index )

Derives the model type from the given UMB model index.

Definition at line 316 of file SparseModelFromUmb.cpp.

◆ deriveValueType()

template<typename ValueType>

bool storm::umb::deriveValueType	(	storm::umb::ModelIndex const &	index,
		ImportOptions const &	options = {} )

Returns true iff the given umb model with the given options should have ValueType as its ValueType.

Currently, this can be either double, storm::RationalNumber, storm::Interval, or storm::RationalInterval.

Note: this does not check whether the model can actually be represented with the derived ValueType (e.g., interval to double is not possible).

Definition at line 347 of file SparseModelFromUmb.cpp.

◆ exportModelToUmb() [1/5]

template void storm::umb::exportModelToUmb	(	storm::models::sparse::Model< double > const &	,
		std::filesystem::path const &	,
		ExportOptions const &	)

◆ exportModelToUmb() [2/5]

template void storm::umb::exportModelToUmb	(	storm::models::sparse::Model< storm::Interval > const &	,
		std::filesystem::path const &	,
		ExportOptions const &	)

◆ exportModelToUmb() [3/5]

template void storm::umb::exportModelToUmb	(	storm::models::sparse::Model< storm::RationalInterval > const &	,
		std::filesystem::path const &	,
		ExportOptions const &	)

◆ exportModelToUmb() [4/5]

template void storm::umb::exportModelToUmb	(	storm::models::sparse::Model< storm::RationalNumber > const &	,
		std::filesystem::path const &	,
		ExportOptions const &	)

◆ exportModelToUmb() [5/5]

template<typename ValueType>

void storm::umb::exportModelToUmb	(	storm::models::sparse::Model< ValueType > const &	model,
		std::filesystem::path const &	targetLocation,
		ExportOptions const &	options )

Definition at line 37 of file Umb.cpp.

◆ importUmb()

storm::umb::UmbModel storm::umb::importUmb	(	std::filesystem::path const &	umbLocation,
		ImportOptions const &	options )

Definition at line 258 of file UmbImport.cpp.

◆ isBooleanType()

bool storm::umb::isBooleanType ( Type const type )

Returns: true if the type is Boolean.

Definition at line 8 of file Type.cpp.

◆ isContinuousNumericType()

bool storm::umb::isContinuousNumericType ( Type const type )

Returns: true if the type is continuous (double, rational, or interval of doubles/rationals)

Definition at line 25 of file Type.cpp.

◆ isDiscreteNumericType()

bool storm::umb::isDiscreteNumericType ( Type const type )

Returns: true if the type is discrete (uint, int, or interval of (u)ints).

Definition at line 12 of file Type.cpp.

◆ isIntervalType()

bool storm::umb::isIntervalType ( Type const type )

Returns: true if the type is an interval type.

Definition at line 42 of file Type.cpp.

◆ isNumericType()

bool storm::umb::isNumericType ( Type const type )

Returns: true if the type is numeric (discrete or continuous).

Definition at line 38 of file Type.cpp.

◆ isStringType()

bool storm::umb::isStringType ( Type const type )

Returns: true if the type is an interval type.

Definition at line 55 of file Type.cpp.

◆ sparseModelFromUmb() [1/2]

std::shared_ptr< storm::models::ModelBase > storm::umb::sparseModelFromUmb	(	storm::umb::UmbModel const &	umbModel,
		ImportOptions const &	options = {} )

Constructs a sparse model from the given UMB model.

Note: deriveValueType can be used to determine the right ValueType for downward casting the returned ModelBase.

Definition at line 385 of file SparseModelFromUmb.cpp.

◆ sparseModelFromUmb() [2/2]

template<typename ValueType>

std::shared_ptr< storm::models::ModelBase > storm::umb::sparseModelFromUmb	(	storm::umb::UmbModel const &	umbModel,
		ImportOptions const &	options = {} )

Constructs a sparse model from the given UMB model.

The derived value type is enforced, which might trigger conversions e.g. from/to rationals. Throws an exception if such a conversion is not possible (e.g. interval to ValueType=double).

Note: deriveValueType can be used to determine the right ValueType for downward casting the returned ModelBase.

Definition at line 381 of file SparseModelFromUmb.cpp.

◆ sparseModelFromUmb< double >()

template std::shared_ptr< storm::models::sparse::Model< double > > storm::umb::sparseModelFromUmb< double >	(	storm::umb::UmbModel const &	umbModel,
		ImportOptions const &	options )

◆ sparseModelFromUmb< storm::Interval >()

template std::shared_ptr< storm::models::sparse::Model< storm::Interval > > storm::umb::sparseModelFromUmb< storm::Interval >	(	storm::umb::UmbModel const &	umbModel,
		ImportOptions const &	options )

◆ sparseModelFromUmb< storm::RationalInterval >()

template std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > > storm::umb::sparseModelFromUmb< storm::RationalInterval >	(	storm::umb::UmbModel const &	umbModel,
		ImportOptions const &	options )

◆ sparseModelFromUmb< storm::RationalNumber >()

template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > storm::umb::sparseModelFromUmb< storm::RationalNumber >	(	storm::umb::UmbModel const &	umbModel,
		ImportOptions const &	options )

◆ sparseModelToUmb()

template<typename ValueType>

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

Definition at line 471 of file SparseModelToUmb.cpp.

◆ sparseModelToUmb< double >()

template storm::umb::UmbModel storm::umb::sparseModelToUmb< double >	(	storm::models::sparse::Model< double > const &	model,
		ExportOptions const &	options )

◆ sparseModelToUmb< storm::Interval >()

template storm::umb::UmbModel storm::umb::sparseModelToUmb< storm::Interval >	(	storm::models::sparse::Model< storm::Interval > const &	model,
		ExportOptions const &	options )

◆ sparseModelToUmb< storm::RationalInterval >()

template storm::umb::UmbModel storm::umb::sparseModelToUmb< storm::RationalInterval >	(	storm::models::sparse::Model< storm::RationalInterval > const &	model,
		ExportOptions const &	options )

◆ sparseModelToUmb< storm::RationalNumber >()

template storm::umb::UmbModel storm::umb::sparseModelToUmb< storm::RationalNumber >	(	storm::models::sparse::Model< storm::RationalNumber > const &	model,
		ExportOptions const &	options )

◆ stringVectorView()

auto storm::umb::stringVectorView	(	SEQ< char > const &	strings,
		CSR const &	stringMapping )

inline

Definition at line 10 of file StringEncoding.h.

◆ toArchive()

void storm::umb::toArchive	(	storm::umb::UmbModel const &	umbModel,
		std::filesystem::path const &	archivePath,
		ExportOptions const &	options )

Definition at line 137 of file UmbExport.cpp.

◆ toString()

std::string storm::umb::toString ( Type const type )

Returns a string representation of the type.

Definition at line 82 of file Type.cpp.

◆ validate()

bool storm::umb::validate	(	storm::umb::UmbModel const &	umbModel,
		std::ostream &	errors )

Validates the given UMB model and writes potential errors to the given output stream.

Returns: true if the UMB model is valid.

Note: This only validates the umbModel against the UMB specification. It does not check whether Storm supports all features used in the model.; The validation checks are incomplete. In particular, this does not apply any checks that would require iterating over dynamic-sized structures.

Definition at line 110 of file Validation.cpp.

◆ validateOrThrow()

void storm::umb::validateOrThrow ( storm::umb::UmbModel const & umbModel )

Validates the given UMB model.

If it is invalid, an exception is thrown.

Note: : This only validates the umbModel against the UMB specification. It does not check whether Storm supports all features used in the model.; The validation checks are incomplete. In particular, this does not apply any checks that would require iterating over dynamic-sized structures.

Definition at line 572 of file Validation.cpp.

Variable Documentation

◆ DefaultAnnotationAlias

const std::string storm::umb::DefaultAnnotationAlias = "default"

Definition at line 28 of file ModelIndex.cpp.

Namespaces

Classes

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

◆ CSR

◆ OptionalVectorType

◆ SEQ

◆ TO1

◆ VectorType

Enumeration Type Documentation

◆ Type

Function Documentation

◆ buildModelFromUmb() [1/2]

◆ buildModelFromUmb() [2/2]

◆ defaultBitSize()

◆ deriveModelType()

◆ deriveValueType()

◆ exportModelToUmb() [1/5]

◆ exportModelToUmb() [2/5]

◆ exportModelToUmb() [3/5]

◆ exportModelToUmb() [4/5]

◆ exportModelToUmb() [5/5]

◆ importUmb()

◆ isBooleanType()

◆ isContinuousNumericType()

◆ isDiscreteNumericType()

◆ isIntervalType()

◆ isNumericType()

◆ isStringType()

◆ sparseModelFromUmb() [1/2]

◆ sparseModelFromUmb() [2/2]

◆ sparseModelFromUmb< double >()

◆ sparseModelFromUmb< storm::Interval >()

◆ sparseModelFromUmb< storm::RationalInterval >()

◆ sparseModelFromUmb< storm::RationalNumber >()

◆ sparseModelToUmb()

◆ sparseModelToUmb< double >()

◆ sparseModelToUmb< storm::Interval >()

◆ sparseModelToUmb< storm::RationalInterval >()

◆ sparseModelToUmb< storm::RationalNumber >()

◆ stringVectorView()

◆ toArchive()

◆ toString()

◆ validate()

◆ validateOrThrow()

Variable Documentation

◆ DefaultAnnotationAlias