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

Namespaces
namespace	detail

Classes
class	ValueParser
	Parser for values according to their ValueType. More...
class	GspnParser
class	MonotonicityParser
class	ParameterRegionParser
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
struct	ExplicitModelParserOptions
class	ExpressionCreator
struct	RationalPolicies
class	ExpressionParser
class	FormulaParser
class	FormulaParserGrammar
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	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	PrismParser
class	GlobalProgramInformation
class	PrismParserGrammar
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

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)
	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 STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< double > >	parseDirectEncodingModel< double > (std::filesystem::path const &file, DirectEncodingParserOptions const &options)
template STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > >	parseDirectEncodingModel< storm::RationalNumber > (std::filesystem::path const &file, DirectEncodingParserOptions const &options)
template STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< storm::Interval > >	parseDirectEncodingModel< storm::Interval > (std::filesystem::path const &file, DirectEncodingParserOptions const &options)
template STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > >	parseDirectEncodingModel< storm::RationalInterval > (std::filesystem::path const &file, DirectEncodingParserOptions const &options)
template STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > >	parseDirectEncodingModel< storm::RationalFunction > (std::filesystem::path const &file, DirectEncodingParserOptions const &options)
template<typename ValueType, typename RewardModelType = models::sparse::StandardRewardModel<ValueType>>
STORM_PARSERS_API 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.
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< std::optional< storm::logic::TimeBound > > &lowerBounds, std::vector< std::optional< storm::logic::TimeBound > > &upperBounds, storm::jani::PropertyInterval const &pi)
std::shared_ptr< storm::logic::Formula const >	makeBinaryBooleanFormula (storm::logic::BinaryBooleanOperatorType oper, std::shared_ptr< storm::logic::Formula const > const &left, std::shared_ptr< storm::logic::Formula const > const &right, storm::logic::FormulaContext context)
std::shared_ptr< storm::logic::Formula const >	makeUnaryBooleanFormula (storm::logic::UnaryBooleanOperatorType oper, std::shared_ptr< storm::logic::Formula const > const &sub, storm::logic::FormulaContext context)
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)
template<typename IntervalType>
bool	parseInterval (std::string const &value, IntervalType &result)
template<typename NumberType>
bool	parseNumber (std::string const &value, NumberType &result)
	Parse number from string.
template STORM_PARSERS_API std::size_t	parseNumber< std::size_t > (std::string const &)
template<typename NumberType>
STORM_PARSERS_API NumberType	parseNumber (std::string const &value)
	Parse number from string.
template<typename NumberType>
STORM_PARSERS_API bool	parseNumber (std::string const &value, NumberType &result)
	Parse number from string.
std::vector< std::string >	parseCommaSeperatedValues (std::string const &input)
	Given a string separated by commas, returns the values.

Variables
template class STORM_PARSERS_API	AutoParser< double, double >
template class STORM_PARSERS_API	AutoParser< double, storm::Interval >
template class STORM_PARSERS_API	DeterministicModelParser< double, double >
template class STORM_PARSERS_API	DeterministicModelParser< double, storm::Interval >
template class STORM_PARSERS_API	DeterministicSparseTransitionParser< double >
template class STORM_PARSERS_API	DeterministicSparseTransitionParser< storm::Interval >
template class STORM_PARSERS_API	ImcaMarkovAutomatonParser< double >
template<typename ValueType>
const bool	JaniParser< ValueType >::defaultVariableTransient = false
const std::string	VARIABLE_AUTOMATON_DELIMITER = "_"
template class STORM_PARSERS_API	JaniParser< double >
template class STORM_PARSERS_API	JaniParser< storm::RationalNumber >
template class STORM_PARSERS_API	MarkovAutomatonParser< double, double >
template class STORM_PARSERS_API	MarkovAutomatonParser< double, storm::Interval >
template class STORM_PARSERS_API	MarkovAutomatonSparseTransitionParser< double >
template class STORM_PARSERS_API	NondeterministicModelParser< double, double >
template class STORM_PARSERS_API	NondeterministicModelParser< double, storm::Interval >
template class STORM_PARSERS_API	NondeterministicSparseTransitionParser< double >
template class STORM_PARSERS_API	NondeterministicSparseTransitionParser< storm::Interval >
template class STORM_PARSERS_API	SparseStateRewardParser< double >
template class STORM_PARSERS_API	SparseStateRewardParser< storm::Interval >
template class STORM_PARSERS_API	ValueParser< double >
template class STORM_PARSERS_API	ValueParser< storm::RationalNumber >
template class STORM_PARSERS_API	ValueParser< storm::Interval >
template class STORM_PARSERS_API	ValueParser< storm::RationalInterval >

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 10 of file ConstantDataType.h.

◆ DirectEncodingValueType

enum class storm::parser::DirectEncodingValueType

strong

Enumerator
Default
Double
DoubleInterval
Rational
RationalInterval
Parametric

Definition at line 16 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 1122 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 1098 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 1114 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 1071 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 1106 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 66 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 82 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 59 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 73 of file JaniParser.cpp.

◆ insertLowerUpperTimeBounds()

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

Definition at line 319 of file JaniParser.cpp.

◆ makeBinaryBooleanFormula()

std::shared_ptr< storm::logic::Formula const > storm::parser::makeBinaryBooleanFormula	(	storm::logic::BinaryBooleanOperatorType	oper,
		std::shared_ptr< storm::logic::Formula const > const &	left,
		std::shared_ptr< storm::logic::Formula const > const &	right,
		storm::logic::FormulaContext	context )

Definition at line 333 of file JaniParser.cpp.

◆ makeUnaryBooleanFormula()

std::shared_ptr< storm::logic::Formula const > storm::parser::makeUnaryBooleanFormula	(	storm::logic::UnaryBooleanOperatorType	oper,
		std::shared_ptr< storm::logic::Formula const > const &	sub,
		storm::logic::FormulaContext	context )

Definition at line 343 of file JaniParser.cpp.

◆ operator<<()

STORM_PARSERS_API 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/3]

STORM_PARSERS_API 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 578 of file DirectEncodingParser.cpp.

◆ parseDirectEncodingModel() [2/3]

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 569 of file DirectEncodingParser.cpp.

◆ parseDirectEncodingModel() [3/3]

template<typename ValueType, typename RewardModelType = models::sparse::StandardRewardModel<ValueType>>

STORM_PARSERS_API 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 569 of file DirectEncodingParser.cpp.

◆ parseDirectEncodingModel< double >()

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

◆ parseDirectEncodingModel< storm::Interval >()

template STORM_PARSERS_API 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 STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > storm::parser::parseDirectEncodingModel< storm::RationalFunction >	(	std::filesystem::path const &	file,
		DirectEncodingParserOptions const &	options )

◆ parseDirectEncodingModel< storm::RationalInterval >()

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

◆ parseDirectEncodingModel< storm::RationalNumber >()

template STORM_PARSERS_API 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 62 of file ValueParser.cpp.

◆ parseInterval()

template<typename IntervalType>

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

Definition at line 78 of file ValueParser.cpp.

◆ parseKeyValueString()

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

Definition at line 11 of file KeyValueParser.cpp.

◆ parseNumber() [1/4]

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/4]

template<typename NumberType>

STORM_PARSERS_API 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() [3/4]

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 124 of file ValueParser.cpp.

◆ parseNumber() [4/4]

template<typename NumberType>

STORM_PARSERS_API 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 124 of file ValueParser.cpp.

◆ parseNumber< std::size_t >()

template STORM_PARSERS_API 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 1812 of file JaniParser.cpp.