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

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...

class	DirectEncodingParser
	Parser for models in the DRN format with explicit encoding. 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 }

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

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 seperated 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.

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 1036 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 1012 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 1028 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 985 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 1020 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 seperated by commas, returns the values.

Definition at line 11 of file CSVParser.cpp.

◆ parseDouble()

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

Definition at line 61 of file ValueParser.cpp.

◆ parseInterval()

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

Definition at line 75 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 53 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 121 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 1721 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 )

Definition at line 13 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.

Classes

Enumerations

Functions

Variables

Detailed Description

Enumeration Type Documentation

◆ ConstantDataType

Function Documentation

◆ ensureArrayType()

◆ ensureBooleanType()

◆ ensureIntegerType()

◆ ensureNumberOfArguments()

◆ ensureNumericalType()

◆ getBoolean()

◆ getSignedInt()

◆ getString()

◆ getUnsignedInt()

◆ insertLowerUpperTimeBounds()

◆ operator<<()

◆ parseCommaSeperatedValues()

◆ parseDouble()

◆ parseInterval()

◆ parseKeyValueString()

◆ parseNumber() [1/2]

◆ parseNumber() [2/2]

◆ parseNumber< std::size_t >()

◆ parseSyncVectors()

◆ readValue()

◆ readValue< double >()

Variable Documentation

◆ VARIABLE_AUTOMATON_DELIMITER