Contains all file parsers and helper classes. More...

Namespaces
namespace	detail

Classes
class	AtomicPropositionLabelingParser
	This class can be used to parse a labeling file. More...

class	AutoParser
	This class automatically chooses the correct parser for the given files and returns the corresponding model. More...

class	DeterministicModelParser
	Loads a deterministic model (Dtmc or Ctmc) from files. More...

class	DeterministicSparseTransitionParser
	This class can be used to parse a file containing either transitions or transition rewards of a deterministic model. More...

struct	DirectEncodingParserOptions

class	ExpressionCreator

class	ExpressionParser

class	FormulaParser

class	FormulaParserGrammar

class	GlobalProgramInformation

class	GspnParser

class	ImcaMarkovAutomatonParser

class	ImcaParserGrammar

class	JaniParser

class	MappedFile
	Opens a file and maps it to memory providing a char* containing the file content. More...

class	MarkovAutomatonParser
	Loads a labeled Markov automaton from files. More...

class	MarkovAutomatonSparseTransitionParser
	A class providing the functionality to parse the transitions of a Markov automaton. More...

class	MonotonicityParser

class	NondeterministicModelParser
	Loads a nondeterministic model (Mdp or Ctmdp) from files. More...

class	NondeterministicSparseTransitionParser
	A class providing the functionality to parse the transitions of a nondeterministic model. More...

class	ParameterRegionParser

class	PrismParser

class	PrismParserGrammar

struct	RationalPolicies

class	SparseChoiceLabelingParser
	A class providing the functionality to parse a choice labeling. More...

class	SparseItemLabelingParser
	This class can be used to parse a labeling file. More...

class	SparseStateRewardParser
	A class providing the functionality to parse a the state rewards of a model. More...

struct	SpiritErrorHandler

class	ValueParser
	Parser for values according to their ValueType. More...

Enumerations
enum class	ConstantDataType { Bool , Integer , Rational }

enum class	DirectEncodingValueType { Default , Double , DoubleInterval , Rational , RationalInterval , Parametric }

Functions
std::ostream &	operator<< (std::ostream &out, ConstantDataType const &constantDataType)

template<typename ValueType , typename RewardModelType >
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > >	parseDirectEncodingModel (std::filesystem::path const &file, DirectEncodingParserOptions const &options=DirectEncodingParserOptions())
	Parses the given file in DRN format.

std::shared_ptr< storm::models::ModelBase >	parseDirectEncodingModel (std::filesystem::path const &file, DirectEncodingValueType valueType, DirectEncodingParserOptions const &options=DirectEncodingParserOptions())
	Parses the given file in DRN format.

template std::shared_ptr< storm::models::sparse::Model< double > >	parseDirectEncodingModel< double > (std::filesystem::path const &file, DirectEncodingParserOptions const &options)

template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > >	parseDirectEncodingModel< storm::RationalNumber > (std::filesystem::path const &file, DirectEncodingParserOptions const &options)

template std::shared_ptr< storm::models::sparse::Model< storm::Interval > >	parseDirectEncodingModel< storm::Interval > (std::filesystem::path const &file, DirectEncodingParserOptions const &options)

template std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > >	parseDirectEncodingModel< storm::RationalFunction > (std::filesystem::path const &file, DirectEncodingParserOptions const &options)

template<typename ValueType >
std::string	getString (typename JaniParser< ValueType >::Json const &structure, std::string const &errorInfo)

template<typename ValueType >
bool	getBoolean (typename JaniParser< ValueType >::Json const &structure, std::string const &errorInfo)

template<typename ValueType >
uint64_t	getUnsignedInt (typename JaniParser< ValueType >::Json const &structure, std::string const &errorInfo)

template<typename ValueType >
int64_t	getSignedInt (typename JaniParser< ValueType >::Json const &structure, std::string const &errorInfo)

void	insertLowerUpperTimeBounds (std::vector< boost::optional< storm::logic::TimeBound > > &lowerBounds, std::vector< boost::optional< storm::logic::TimeBound > > &upperBounds, storm::jani::PropertyInterval const &pi)

void	ensureNumberOfArguments (uint64_t expected, uint64_t actual, std::string const &opstring, std::string const &errorInfo)
	Helper for parse expression.

void	ensureBooleanType (storm::expressions::Expression const &expr, std::string const &opstring, unsigned argNr, std::string const &errorInfo)
	Helper for parse expression.

void	ensureNumericalType (storm::expressions::Expression const &expr, std::string const &opstring, unsigned argNr, std::string const &errorInfo)
	Helper for parse expression.

void	ensureIntegerType (storm::expressions::Expression const &expr, std::string const &opstring, unsigned argNr, std::string const &errorInfo)
	Helper for parse expression.

void	ensureArrayType (storm::expressions::Expression const &expr, std::string const &opstring, unsigned argNr, std::string const &errorInfo)
	Helper for parse expression.

template<typename ValueType >
std::vector< storm::jani::SynchronizationVector >	parseSyncVectors (typename JaniParser< ValueType >::Json const &syncVectorStructure)

std::unordered_map< std::string, std::string >	parseKeyValueString (std::string const &keyValueString)

template<typename T >
T	readValue (char const *buf)

template<>
double	readValue< double > (char const *buf)

template<typename NumberType >
NumberType	parseNumber (std::string const &value)
	Parse number from string.

bool	parseDouble (std::string const &value, double &result)

bool	parseInterval (std::string const &value, storm::Interval &result)

template<typename NumberType >
bool	parseNumber (std::string const &value, NumberType &result)
	Parse number from string.

template std::size_t	parseNumber< std::size_t > (std::string const &)

std::vector< std::string >	parseCommaSeperatedValues (std::string const &input)
	Given a string separated by commas, returns the values.

Variables
const std::string	VARIABLE_AUTOMATON_DELIMITER = "_"

Detailed Description

Contains all file parsers and helper classes.

This namespace contains everything needed to load data files (like atomic propositions, transition systems, formulas, etc.) including methods for efficient file access (see MappedFile).

Enumeration Type Documentation

◆ ConstantDataType

enum class storm::parser::ConstantDataType

strong

Enumerator
Bool
Integer
Rational

Definition at line 8 of file ConstantDataType.h.

◆ DirectEncodingValueType

enum class storm::parser::DirectEncodingValueType

strong

Enumerator
Default
Double
DoubleInterval
Rational
RationalInterval
Parametric

Definition at line 15 of file DirectEncodingParser.h.

Function Documentation

◆ ensureArrayType()

void storm::parser::ensureArrayType	(	storm::expressions::Expression const &	expr,
		std::string const &	opstring,
		unsigned	argNr,
		std::string const &	errorInfo
	)

Helper for parse expression.

Definition at line 1078 of file JaniParser.cpp.

◆ ensureBooleanType()

void storm::parser::ensureBooleanType	(	storm::expressions::Expression const &	expr,
		std::string const &	opstring,
		unsigned	argNr,
		std::string const &	errorInfo
	)

Helper for parse expression.

Definition at line 1054 of file JaniParser.cpp.

◆ ensureIntegerType()

void storm::parser::ensureIntegerType	(	storm::expressions::Expression const &	expr,
		std::string const &	opstring,
		unsigned	argNr,
		std::string const &	errorInfo
	)

Helper for parse expression.

Definition at line 1070 of file JaniParser.cpp.

◆ ensureNumberOfArguments()

void storm::parser::ensureNumberOfArguments	(	uint64_t	expected,
		uint64_t	actual,
		std::string const &	opstring,
		std::string const &	errorInfo
	)

Helper for parse expression.

Definition at line 1027 of file JaniParser.cpp.

◆ ensureNumericalType()

void storm::parser::ensureNumericalType	(	storm::expressions::Expression const &	expr,
		std::string const &	opstring,
		unsigned	argNr,
		std::string const &	errorInfo
	)

Helper for parse expression.

Definition at line 1062 of file JaniParser.cpp.

◆ getBoolean()

template<typename ValueType >

bool storm::parser::getBoolean	(	typename JaniParser< ValueType >::Json const &	structure,
		std::string const &	errorInfo
	)

Definition at line 63 of file JaniParser.cpp.

◆ getSignedInt()

template<typename ValueType >

int64_t storm::parser::getSignedInt	(	typename JaniParser< ValueType >::Json const &	structure,
		std::string const &	errorInfo
	)

Definition at line 79 of file JaniParser.cpp.

◆ getString()

template<typename ValueType >

std::string storm::parser::getString	(	typename JaniParser< ValueType >::Json const &	structure,
		std::string const &	errorInfo
	)

Definition at line 56 of file JaniParser.cpp.

◆ getUnsignedInt()

template<typename ValueType >

uint64_t storm::parser::getUnsignedInt	(	typename JaniParser< ValueType >::Json const &	structure,
		std::string const &	errorInfo
	)

Definition at line 70 of file JaniParser.cpp.

◆ insertLowerUpperTimeBounds()

void storm::parser::insertLowerUpperTimeBounds	(	std::vector< boost::optional< storm::logic::TimeBound > > &	lowerBounds,
		std::vector< boost::optional< storm::logic::TimeBound > > &	upperBounds,
		storm::jani::PropertyInterval const &	pi
	)

Definition at line 316 of file JaniParser.cpp.

◆ operator<<()

std::ostream & storm::parser::operator<<	(	std::ostream &	out,
		ConstantDataType const &	constantDataType
	)

Definition at line 5 of file ConstantDataType.cpp.

◆ parseCommaSeperatedValues()

std::vector< std::string > storm::parser::parseCommaSeperatedValues ( std::string const & input )

Given a string separated by commas, returns the values.

Definition at line 11 of file CSVParser.cpp.

◆ parseDirectEncodingModel() [1/2]

template<typename ValueType , typename RewardModelType >

std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > storm::parser::parseDirectEncodingModel	(	std::filesystem::path const &	file,
		DirectEncodingParserOptions const &	options = `DirectEncodingParserOptions()`
	)

Parses the given file in DRN format.

The value type is derived from the given template parameter.

Exceptions

WrongFormatException	if the specified value type is incompatible with the file content (e.g. parametric into double)
WrongFormatException	if the valueType parameter is `Default` and the DRN file does not have a `@value_type` section
WrongFormatException	if the provided file is an interval model but the ValueType is not an interval.

Parameters

file	path to DRN file
valueType	Value type used for output model.
options	Parsing options.

Definition at line 560 of file DirectEncodingParser.cpp.

◆ parseDirectEncodingModel() [2/2]

std::shared_ptr< storm::models::ModelBase > storm::parser::parseDirectEncodingModel	(	std::filesystem::path const &	file,
		DirectEncodingValueType	valueType,
		DirectEncodingParserOptions const &	options = `DirectEncodingParserOptions()`
	)

Parses the given file in DRN format.

The value type can be specified via the valueType parameter. If it is set to Default, the value type of the returned model is derived by the @value_type section in the file.

Exceptions

WrongFormatException	if the specified value type is incompatible with the file content (e.g. parametric into double)
WrongFormatException	if the valueType parameter is `Default` and the DRN file does not have a `@value_type` section

Note: if the provided file is an interval model, the value type is potentially promoted to the corresponding interval variant (double -> storm::Interval)

Parameters

file	path to DRN file
valueType	Value type used for output model.
options	Parsing options.

Definition at line 569 of file DirectEncodingParser.cpp.

◆ parseDirectEncodingModel< double >()

template std::shared_ptr< storm::models::sparse::Model< double > > storm::parser::parseDirectEncodingModel< double >	(	std::filesystem::path const &	file,
		DirectEncodingParserOptions const &	options
	)

◆ parseDirectEncodingModel< storm::Interval >()

template std::shared_ptr< storm::models::sparse::Model< storm::Interval > > storm::parser::parseDirectEncodingModel< storm::Interval >	(	std::filesystem::path const &	file,
		DirectEncodingParserOptions const &	options
	)

◆ parseDirectEncodingModel< storm::RationalFunction >()

template std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > storm::parser::parseDirectEncodingModel< storm::RationalFunction >	(	std::filesystem::path const &	file,
		DirectEncodingParserOptions const &	options
	)

◆ parseDirectEncodingModel< storm::RationalNumber >()

template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > storm::parser::parseDirectEncodingModel< storm::RationalNumber >	(	std::filesystem::path const &	file,
		DirectEncodingParserOptions const &	options
	)

◆ parseDouble()

bool storm::parser::parseDouble	(	std::string const &	value,
		double &	result
	)

Definition at line 63 of file ValueParser.cpp.

◆ parseInterval()

bool storm::parser::parseInterval	(	std::string const &	value,
		storm::Interval &	result
	)

Definition at line 77 of file ValueParser.cpp.

◆ parseKeyValueString()

std::unordered_map< std::string, std::string > storm::parser::parseKeyValueString ( std::string const & keyValueString )

Definition at line 11 of file KeyValueParser.cpp.

◆ parseNumber() [1/2]

template<typename NumberType >

NumberType storm::parser::parseNumber ( std::string const & value )

Parse number from string.

Parameters

value String containing the value.

Exceptions

WrongFormatException if parsing is not successful

Returns: NumberType.

Definition at line 55 of file ValueParser.cpp.

◆ parseNumber() [2/2]

template<typename NumberType >

bool storm::parser::parseNumber	(	std::string const &	value,
		NumberType &	result
	)

Parse number from string.

Parameters

value	String containing the value.
result	if parsing is successful, the parsed number is stored here

Returns: whether parsing is successful.

Definition at line 123 of file ValueParser.cpp.

◆ parseNumber< std::size_t >()

template std::size_t storm::parser::parseNumber< std::size_t > ( std::string const & )

◆ parseSyncVectors()

template<typename ValueType >

std::vector< storm::jani::SynchronizationVector > storm::parser::parseSyncVectors ( typename JaniParser< ValueType >::Json const & syncVectorStructure )

Definition at line 1763 of file JaniParser.cpp.

◆ readValue()

template<typename T >

T storm::parser::readValue ( char const * buf )

◆ readValue< double >()

template<>

double storm::parser::readValue< double > ( char const * buf )

inline

Definition at line 12 of file ReadValues.h.

Variable Documentation

◆ VARIABLE_AUTOMATON_DELIMITER

const std::string storm::parser::VARIABLE_AUTOMATON_DELIMITER = "_"

Definition at line 49 of file JaniParser.cpp.

Namespaces

Classes

Enumerations

Functions

Variables

Detailed Description

Enumeration Type Documentation

◆ ConstantDataType

◆ DirectEncodingValueType

Function Documentation

◆ ensureArrayType()

◆ ensureBooleanType()

◆ ensureIntegerType()

◆ ensureNumberOfArguments()

◆ ensureNumericalType()

◆ getBoolean()

◆ getSignedInt()

◆ getString()

◆ getUnsignedInt()

◆ insertLowerUpperTimeBounds()

◆ operator<<()

◆ parseCommaSeperatedValues()

◆ parseDirectEncodingModel() [1/2]

◆ parseDirectEncodingModel() [2/2]

◆ parseDirectEncodingModel< double >()

◆ parseDirectEncodingModel< storm::Interval >()

◆ parseDirectEncodingModel< storm::RationalFunction >()

◆ parseDirectEncodingModel< storm::RationalNumber >()

◆ parseDouble()

◆ parseInterval()

◆ parseKeyValueString()

◆ parseNumber() [1/2]

◆ parseNumber() [2/2]

◆ parseNumber< std::size_t >()

◆ parseSyncVectors()

◆ readValue()

◆ readValue< double >()

Variable Documentation

◆ VARIABLE_AUTOMATON_DELIMITER