Classes
struct	DirectEncodingOptions

Enumerations
enum class	ModelExportFormat { Dot , Drdd , Drn , Json }

Functions
template<storm::dd::DdType Type, typename ValueType >
void	explicitExportSymbolicModel (std::string const &filename, std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > symbolicModel)
	Exports a sparse model into the explicit drdd format.

template void	explicitExportSymbolicModel< storm::dd::DdType::CUDD, double > (std::string const &, std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > > sparseModel)

template void	explicitExportSymbolicModel< storm::dd::DdType::Sylvan, double > (std::string const &, std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > > sparseModel)

template void	explicitExportSymbolicModel< storm::dd::DdType::Sylvan, storm::RationalNumber > (std::string const &, std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > > sparseModel)

template void	explicitExportSymbolicModel< storm::dd::DdType::Sylvan, storm::RationalFunction > (std::string const &, std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > > sparseModel)

template<typename ValueType >
void	explicitExportSparseModel (std::ostream &os, std::shared_ptr< storm::models::sparse::Model< ValueType > > sparseModel, std::vector< std::string > const &parameters, DirectEncodingOptions const &options=DirectEncodingOptions())
	Exports a sparse model into the explicit DRN format.

template<typename ValueType >
std::vector< std::string >	getParameters (std::shared_ptr< storm::models::sparse::Model< ValueType > > sparseModel)
	Accumulate parameters in the model.

template<>
std::vector< std::string >	getParameters (std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > sparseModel)

template<typename ValueType >
std::unordered_map< ValueType, std::string >	generatePlaceholders (std::shared_ptr< storm::models::sparse::Model< ValueType > > sparseModel, std::vector< ValueType > exitRates)
	Generate placeholders for rational functions in the model.

void	createPlaceholder (std::unordered_map< storm::RationalFunction, std::string > &placeholders, storm::RationalFunction const &value, size_t &i)
	Helper function to create a possible placeholder.

template<>
std::unordered_map< storm::RationalFunction, std::string >	generatePlaceholders (std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > sparseModel, std::vector< storm::RationalFunction > exitRates)

template<typename ValueType >
void	writeValue (std::ostream &os, ValueType value, std::unordered_map< ValueType, std::string > const &placeholders)
	Write value to stream while using the placeholders.

template void	explicitExportSparseModel< double > (std::ostream &os, std::shared_ptr< storm::models::sparse::Model< double > > sparseModel, std::vector< std::string > const &parameters, DirectEncodingOptions const &options)

template void	explicitExportSparseModel< storm::RationalNumber > (std::ostream &os, std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > sparseModel, std::vector< std::string > const &parameters, DirectEncodingOptions const &options)

template void	explicitExportSparseModel< storm::RationalFunction > (std::ostream &os, std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > sparseModel, std::vector< std::string > const &parameters, DirectEncodingOptions const &options)

template void	explicitExportSparseModel< storm::Interval > (std::ostream &os, std::shared_ptr< storm::models::sparse::Model< storm::Interval > > sparseModel, std::vector< std::string > const &parameters, DirectEncodingOptions const &options)

template<typename DataType , typename Header1Type = DataType, typename Header2Type = DataType>
void	exportDataToCSVFile (std::string filepath, std::vector< std::vector< DataType > > const &data, boost::optional< std::vector< Header1Type > > const &header1=boost::none, boost::optional< std::vector< Header2Type > > const &header2=boost::none)

template<typename Container >
void	outputFixedWidth (std::ostream &stream, Container const &output, size_t maxWidth=30)
	Output list of strings with linebreaks according to fixed width.

void	openFile (std::string const &filepath, std::ofstream &filestream, bool append=false, bool silent=false)
	Open the given file for writing.

void	openFile (std::string const &filepath, std::ifstream &filestream)
	Open the given file for reading.

void	closeFile (std::ofstream &stream)
	Close the given file after writing.

void	closeFile (std::ifstream &stream)
	Close the given file after reading.

bool	fileExistsAndIsReadable (std::string const &filename)
	Tests whether the given file exists and is readable.

template<class CharT , class Traits , class Allocator >
std::basic_istream< CharT, Traits > &	getline (std::basic_istream< CharT, Traits > &input, std::basic_string< CharT, Traits, Allocator > &str)
	Overloaded getline function which handles different types of newline ( and \r).

ModelExportFormat	getModelExportFormatFromString (std::string const &input)

std::string	toString (ModelExportFormat const &input)

ModelExportFormat	getModelExportFormatFromFileExtension (std::string const &filename)

Enumeration Type Documentation

◆ ModelExportFormat

enum class storm::io::ModelExportFormat

strong

Enumerator
Dot
Drdd
Drn
Json

Definition at line 8 of file ModelExportFormat.h.

Function Documentation

◆ closeFile() [1/2]

void storm::io::closeFile ( std::ifstream & stream )

inline

Close the given file after reading.

Parameters

stream Contains the file handler to close.

Definition at line 56 of file file.h.

◆ closeFile() [2/2]

void storm::io::closeFile ( std::ofstream & stream )

inline

Close the given file after writing.

Parameters

stream Contains the file handler to close.

Definition at line 47 of file file.h.

◆ createPlaceholder()

void storm::io::createPlaceholder	(	std::unordered_map< storm::RationalFunction, std::string > &	placeholders,
		storm::RationalFunction const &	value,
		size_t &	i
	)

Helper function to create a possible placeholder.

A new placeholder is inserted if the rational function is not constant and the function does not exist yet.

Parameters

placeholders	Existing placeholders.
value	Value.
i	Counter to enumerate placeholders.

Definition at line 212 of file DirectEncodingExporter.cpp.

◆ explicitExportSparseModel()

template<typename ValueType >

void storm::io::explicitExportSparseModel	(	std::ostream &	os,
		std::shared_ptr< storm::models::sparse::Model< ValueType > >	sparseModel,
		std::vector< std::string > const &	parameters,
		DirectEncodingOptions const &	options = `DirectEncodingOptions()`
	)

Exports a sparse model into the explicit DRN format.

Parameters

os	Stream to export to
sparseModel	Model to export
parameters	List of parameters

Definition at line 19 of file DirectEncodingExporter.cpp.

◆ explicitExportSparseModel< double >()

template void storm::io::explicitExportSparseModel< double >	(	std::ostream &	os,
		std::shared_ptr< storm::models::sparse::Model< double > >	sparseModel,
		std::vector< std::string > const &	parameters,
		DirectEncodingOptions const &	options
	)

◆ explicitExportSparseModel< storm::Interval >()

template void storm::io::explicitExportSparseModel< storm::Interval >	(	std::ostream &	os,
		std::shared_ptr< storm::models::sparse::Model< storm::Interval > >	sparseModel,
		std::vector< std::string > const &	parameters,
		DirectEncodingOptions const &	options
	)

◆ explicitExportSparseModel< storm::RationalFunction >()

template void storm::io::explicitExportSparseModel< storm::RationalFunction >	(	std::ostream &	os,
		std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > >	sparseModel,
		std::vector< std::string > const &	parameters,
		DirectEncodingOptions const &	options
	)

◆ explicitExportSparseModel< storm::RationalNumber >()

template void storm::io::explicitExportSparseModel< storm::RationalNumber >	(	std::ostream &	os,
		std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > >	sparseModel,
		std::vector< std::string > const &	parameters,
		DirectEncodingOptions const &	options
	)

◆ explicitExportSymbolicModel()

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

void storm::io::explicitExportSymbolicModel	(	std::string const &	filename,
		std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > >	symbolicModel
	)

Exports a sparse model into the explicit drdd format.

Parameters

filename	File path
symbolicModel	Model to export

Definition at line 10 of file DDEncodingExporter.cpp.

◆ explicitExportSymbolicModel< storm::dd::DdType::CUDD, double >()

template void storm::io::explicitExportSymbolicModel< storm::dd::DdType::CUDD, double >	(	std::string const &	,
		std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::CUDD, double > >	sparseModel
	)

◆ explicitExportSymbolicModel< storm::dd::DdType::Sylvan, double >()

template void storm::io::explicitExportSymbolicModel< storm::dd::DdType::Sylvan, double >	(	std::string const &	,
		std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::Sylvan, double > >	sparseModel
	)

◆ explicitExportSymbolicModel< storm::dd::DdType::Sylvan, storm::RationalFunction >()

template void storm::io::explicitExportSymbolicModel< storm::dd::DdType::Sylvan, storm::RationalFunction >	(	std::string const &	,
		std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > >	sparseModel
	)

◆ explicitExportSymbolicModel< storm::dd::DdType::Sylvan, storm::RationalNumber >()

template void storm::io::explicitExportSymbolicModel< storm::dd::DdType::Sylvan, storm::RationalNumber >	(	std::string const &	,
		std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalNumber > >	sparseModel
	)

◆ exportDataToCSVFile()

template<typename DataType , typename Header1Type = DataType, typename Header2Type = DataType>

void storm::io::exportDataToCSVFile	(	std::string	filepath,
		std::vector< std::vector< DataType > > const &	data,
		boost::optional< std::vector< Header1Type > > const &	header1 = `boost::none`,
		boost::optional< std::vector< Header2Type > > const &	header2 = `boost::none`
	)

inline

Definition at line 13 of file export.h.

◆ fileExistsAndIsReadable()

bool storm::io::fileExistsAndIsReadable ( std::string const & filename )

inline

Tests whether the given file exists and is readable.

Parameters

filename Path and name of the file to be tested.

Returns: True iff the file exists and is readable.

Definition at line 66 of file file.h.

◆ generatePlaceholders() [1/2]

template<>

std::unordered_map< storm::RationalFunction, std::string > storm::io::generatePlaceholders	(	std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > >	sparseModel,
		std::vector< storm::RationalFunction >	exitRates
	)

Definition at line 223 of file DirectEncodingExporter.cpp.

◆ generatePlaceholders() [2/2]

template<typename ValueType >

std::unordered_map< ValueType, std::string > storm::io::generatePlaceholders	(	std::shared_ptr< storm::models::sparse::Model< ValueType > >	sparseModel,
		std::vector< ValueType >	exitRates
	)

Generate placeholders for rational functions in the model.

Parameters

sparseModel	Model.
exitRates	Exit rates.

Returns: Mapping of the form:rational function -> placeholder name.

Definition at line 200 of file DirectEncodingExporter.cpp.

◆ getline()

template<class CharT , class Traits , class Allocator >

std::basic_istream< CharT, Traits > & storm::io::getline	(	std::basic_istream< CharT, Traits > &	input,
		std::basic_string< CharT, Traits, Allocator > &	str
	)

inline

Overloaded getline function which handles different types of newline (
and \r).

Parameters

input	Input stream.
str	Output string.

Returns: Remaining stream.

Definition at line 80 of file file.h.

◆ getModelExportFormatFromFileExtension()

ModelExportFormat storm::io::getModelExportFormatFromFileExtension ( std::string const & filename )

Returns: The ModelExportFormat whose string representation matches the extension of the given file

Exceptions

InvalidArgumentException if there is no file extension or if it doesn't match any known format.

Definition at line 36 of file ModelExportFormat.cpp.

◆ getModelExportFormatFromString()

ModelExportFormat storm::io::getModelExportFormatFromString ( std::string const & input )

Returns: The ModelExportFormat whose string representation matches the given input

Exceptions

InvalidArgumentException if the input doesn't match any known format

Definition at line 9 of file ModelExportFormat.cpp.

◆ getParameters() [1/2]

template<>

std::vector< std::string > storm::io::getParameters ( std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > sparseModel )

Definition at line 186 of file DirectEncodingExporter.cpp.

◆ getParameters() [2/2]

template<typename ValueType >

std::vector< std::string > storm::io::getParameters ( std::shared_ptr< storm::models::sparse::Model< ValueType > > sparseModel )

Accumulate parameters in the model.

Parameters

sparseModel Model.

Returns: List of parameters in the model.

Definition at line 181 of file DirectEncodingExporter.cpp.

◆ openFile() [1/2]

void storm::io::openFile	(	std::string const &	filepath,
		std::ifstream &	filestream
	)

inline

Open the given file for reading.

Parameters

filepath	Path and name of the file to be tested.
filestream	Contains the file handler afterwards.

Definition at line 37 of file file.h.

◆ openFile() [2/2]

void storm::io::openFile	(	std::string const &	filepath,
		std::ofstream &	filestream,
		bool	append = `false`,
		bool	silent = `false`
	)

inline

Open the given file for writing.

Parameters

filepath	Path and name of the file to be written to.
filestream	Contains the file handler afterwards.
append	If true, the new content is appended instead of clearing the existing content.

Definition at line 18 of file file.h.

◆ outputFixedWidth()

template<typename Container >

void storm::io::outputFixedWidth	(	std::ostream &	stream,
		Container const &	output,
		size_t	maxWidth = `30`
	)

inline

Output list of strings with linebreaks according to fixed width.

Strings are printed with comma separator. If the length of the current line is greater than maxWidth, a linebreak is inserted.

Parameters

stream	Output stream.
output	List of strings to output.
maxWidth	Maximal width after which a linebreak is inserted. Value 0 represents no linebreaks.

Definition at line 60 of file export.h.

◆ toString()

std::string storm::io::toString ( ModelExportFormat const & input )

Returns: The string representation of the given input

Definition at line 22 of file ModelExportFormat.cpp.

◆ writeValue()

template<typename ValueType >

void storm::io::writeValue	(	std::ostream &	os,
		ValueType	value,
		std::unordered_map< ValueType, std::string > const &	placeholders
	)

Write value to stream while using the placeholders.

Parameters

os	Output stream.
value	Value.
placeholders	Placeholders.

Definition at line 256 of file DirectEncodingExporter.cpp.

Classes

Enumerations

Functions

Enumeration Type Documentation

◆ ModelExportFormat

Function Documentation

◆ closeFile() [1/2]

◆ closeFile() [2/2]

◆ createPlaceholder()

◆ explicitExportSparseModel()

◆ explicitExportSparseModel< double >()

◆ explicitExportSparseModel< storm::Interval >()

◆ explicitExportSparseModel< storm::RationalFunction >()

◆ explicitExportSparseModel< storm::RationalNumber >()

◆ explicitExportSymbolicModel()

◆ explicitExportSymbolicModel< storm::dd::DdType::CUDD, double >()

◆ explicitExportSymbolicModel< storm::dd::DdType::Sylvan, double >()

◆ explicitExportSymbolicModel< storm::dd::DdType::Sylvan, storm::RationalFunction >()

◆ explicitExportSymbolicModel< storm::dd::DdType::Sylvan, storm::RationalNumber >()

◆ exportDataToCSVFile()

◆ fileExistsAndIsReadable()

◆ generatePlaceholders() [1/2]

◆ generatePlaceholders() [2/2]

◆ getline()

◆ getModelExportFormatFromFileExtension()

◆ getModelExportFormatFromString()

◆ getParameters() [1/2]

◆ getParameters() [2/2]

◆ openFile() [1/2]

◆ openFile() [2/2]

◆ outputFixedWidth()

◆ toString()

◆ writeValue()