Namespaces
namespace	builder

namespace	cli

namespace	combinatorics

namespace	cstring

namespace	dd

namespace	detail

namespace	graph

namespace	jani

namespace	ksp

namespace	kwek_mehlhorn

namespace	math

namespace	matrix

namespace	numerical

namespace	parameterlifting

namespace	parametric

namespace	permutation

namespace	pfinternal

namespace	prism

namespace	resources

namespace	solver

namespace	stateelimination

namespace	string

namespace	vector

Classes
class	AutomaticSettings

class	BernoulliDistributionGenerator

class	ConstantsComparator

class	ExponentialDistributionGenerator

class	Extremum
	Stores and manages an extremal (maximal or minimal) value. More...

class	FilteredRewardModel

class	Hash

class	ModelInstantiator
	This class allows efficient instantiation of the given parametric model. More...

class	ProgressMeasurement
	A class that provides convenience operations to display run times. More...

class	RandomProbabilityGenerator

class	RandomProbabilityGenerator< double >

class	RandomProbabilityGenerator< storm::RationalNumber >

class	Stopwatch
	A class that provides convenience operations to display run times. More...

Typedefs
template<typename ValueType >
using	ElementLess = typename detail::ElementLess< ValueType >::type

template<typename ValueType >
using	ElementGreater = typename detail::ElementGreater< ValueType >::type

template<typename ValueType >
using	Maximum = Extremum< storm::OptimizationDirection::Maximize, ValueType >

template<typename ValueType >
using	Minimum = Extremum< storm::OptimizationDirection::Minimize, ValueType >

Enumerations
enum class	Engine { Sparse , Hybrid , Dd , DdSparse , Exploration , AbstractionRefinement , Automatic , Unknown }
	An enumeration of all engines. More...

Functions
template<typename ValueType >
ValueType	one ()

template<typename ValueType >
ValueType	zero ()

template<typename ValueType >
ValueType	infinity ()

template<typename ValueType >
bool	isOne (ValueType const &a)

template<typename ValueType >
bool	isZero (ValueType const &a)

template<typename ValueType >
bool	isNan (ValueType const &)

template<>
bool	isNan (double const &value)

template<typename ValueType >
bool	isApproxEqual (ValueType const &a, ValueType const &b, ValueType const &precision, bool relative)

template<typename ValueType >
bool	isPositive (ValueType const &a)

template<typename ValueType >
bool	isNonNegative (ValueType const &a)

template<typename ValueType >
bool	isBetween (ValueType const &a, ValueType const &b, ValueType const &c, bool strict)
	Compare whether a <= b <= c or a < b < c, based on the strictness parameter.

template<typename ValueType >
bool	isAlmostZero (ValueType const &a)

template<typename ValueType >
bool	isAlmostOne (ValueType const &a)

template<typename ValueType >
bool	isConstant (ValueType const &)

template<typename ValueType >
bool	isInfinity (ValueType const &a)

template<typename ValueType >
bool	isInteger (ValueType const &number)

template<>
bool	isInteger (int const &)

template<>
bool	isInteger (uint32_t const &)

template<>
bool	isInteger (storm::storage::sparse::state_type const &)

template<typename TargetType , typename SourceType >
TargetType	convertNumber (SourceType const &number)

template<>
uint_fast64_t	convertNumber (double const &number)

template<>
int_fast64_t	convertNumber (double const &number)

template<>
double	convertNumber (uint_fast64_t const &number)

template<>
double	convertNumber (double const &number)

template<>
double	convertNumber (long long const &number)

template<>
storm::storage::sparse::state_type	convertNumber (long long const &number)

template<typename ValueType >
ValueType	simplify (ValueType value)

template<typename ValueType >
std::pair< ValueType, ValueType >	minmax (std::vector< ValueType > const &values)

template<typename ValueType >
ValueType	minimum (std::vector< ValueType > const &values)

template<typename ValueType >
ValueType	maximum (std::vector< ValueType > const &values)

template<typename K , typename ValueType >
std::pair< ValueType, ValueType >	minmax (std::map< K, ValueType > const &values)

template<typename K , typename ValueType >
ValueType	minimum (std::map< K, ValueType > const &values)

template<typename K , typename ValueType >
ValueType	maximum (std::map< K, ValueType > const &values)

template<typename ValueType >
ValueType	pow (ValueType const &value, int_fast64_t exponent)

template<typename ValueType >
ValueType	max (ValueType const &first, ValueType const &second)

template<typename ValueType >
ValueType	min (ValueType const &first, ValueType const &second)

template<typename ValueType >
ValueType	sqrt (ValueType const &number)

template<typename ValueType >
ValueType	abs (ValueType const &number)

template<typename ValueType >
ValueType	floor (ValueType const &number)

template<typename ValueType >
ValueType	ceil (ValueType const &number)

template<typename ValueType >
ValueType	round (ValueType const &number)

template<typename ValueType >
ValueType	log (ValueType const &number)

template<typename ValueType >
ValueType	log10 (ValueType const &number)

template<typename ValueType >
ValueType	cos (ValueType const &number)

template<typename ValueType >
ValueType	sin (ValueType const &number)

template<typename ValueType >
uint64_t	numDigits (ValueType const &number)

template<typename ValueType >
NumberTraits< ValueType >::IntegerType	trunc (ValueType const &number)

template<typename IntegerType >
IntegerType	mod (IntegerType const &first, IntegerType const &second)

template<typename IntegerType >
std::pair< IntegerType, IntegerType >	divide (IntegerType const &dividend, IntegerType const &divisor)
	(Integer-)Divides the dividend by the divisor and returns the result plus the remainder.

template<typename ValueType >
std::string	to_string (ValueType const &value)

template<>
storm::RationalFunction	infinity ()

template<>
bool	isOne (storm::RationalFunction const &a)

template<>
bool	isOne (storm::Polynomial const &a)

template<>
bool	isZero (storm::RationalFunction const &a)

template<>
bool	isZero (storm::Polynomial const &a)

template<>
bool	isConstant (storm::RationalFunction const &a)

template<>
bool	isConstant (storm::Polynomial const &a)

template<>
bool	isApproxEqual (storm::RationalFunction const &a, storm::RationalFunction const &b, storm::RationalFunction const &precision, bool relative)

template<>
bool	isConstant (storm::Interval const &a)

template<>
bool	isInfinity (storm::RationalFunction const &a)

template<>
bool	isInteger (storm::RationalFunction const &func)

template<>
RationalFunction	convertNumber (double const &number)

template<>
RationalFunction	convertNumber (int_fast64_t const &number)

template<>
carl::uint	convertNumber (RationalFunction const &func)

template<>
carl::sint	convertNumber (RationalFunction const &func)

template<>
double	convertNumber (RationalFunction const &func)

template<>
RationalFunction	convertNumber (RationalFunction const &number)

template<>
RationalFunction	convertNumber (std::string const &number)

template<>
RationalFunction	convertNumber (storm::storage::sparse::state_type const &number)

template<>
RationalFunction &	simplify (RationalFunction &value)

template<>
RationalFunction &&	simplify (RationalFunction &&value)

template<>
RationalFunction	simplify (RationalFunction value)

template<>
RationalFunction &	simplify (RationalFunction &value)

template<>
RationalFunction &&	simplify (RationalFunction &&value)

template<>
bool	isAlmostZero (storm::RationalFunction const &a)

template<>
bool	isAlmostOne (storm::RationalFunction const &a)

template<>
bool	isNonNegative (storm::RationalFunction const &a)

template<>
bool	isPositive (storm::RationalFunction const &a)

template<>
bool	isBetween (storm::RationalFunction const &a, storm::RationalFunction const &b, storm::RationalFunction const &c, bool strict)

template<>
std::pair< storm::RationalFunction, storm::RationalFunction >	minmax (std::vector< storm::RationalFunction > const &)

template<>
storm::RationalFunction	minimum (std::vector< storm::RationalFunction > const &)

template<>
storm::RationalFunction	maximum (std::vector< storm::RationalFunction > const &)

template<>
std::pair< storm::RationalFunction, storm::RationalFunction >	minmax (std::map< uint64_t, storm::RationalFunction > const &)

template<>
storm::RationalFunction	minimum (std::map< uint64_t, storm::RationalFunction > const &)

template<>
storm::RationalFunction	maximum (std::map< uint64_t, storm::RationalFunction > const &)

template<>
RationalFunction	pow (RationalFunction const &value, int_fast64_t exponent)

template<>
std::string	to_string (RationalFunction const &f)

template<>
double	convertNumber (std::string const &value)

template<>
storm::Interval	convertNumber (double const &number)

template<>
storm::Interval	convertNumber (uint64_t const &number)

template<>
double	convertNumber (storm::Interval const &number)

template<>
storm::Interval	abs (storm::Interval const &interval)

template<>
bool	isApproxEqual (storm::Interval const &a, storm::Interval const &b, storm::Interval const &precision, bool relative)

template double	one ()

template double	zero ()

template bool	isOne (double const &value)

template bool	isZero (double const &value)

template bool	isNonNegative (double const &value)

template bool	isPositive (double const &value)

template bool	isAlmostZero (double const &value)

template bool	isAlmostOne (double const &value)

template bool	isConstant (double const &value)

template bool	isInfinity (double const &value)

template bool	isInteger (double const &number)

template bool	isBetween (double const &a, double const &b, double const &c, bool strict)

template bool	isApproxEqual (double const &a, double const &b, double const &precision, bool relative)

template double	simplify (double value)

template std::pair< double, double >	minmax (std::vector< double > const &)

template double	minimum (std::vector< double > const &)

template double	maximum (std::vector< double > const &)

template std::pair< double, double >	minmax (std::map< uint64_t, double > const &)

template double	minimum (std::map< uint64_t, double > const &)

template double	maximum (std::map< uint64_t, double > const &)

template double	pow (double const &value, int_fast64_t exponent)

template double	max (double const &first, double const &second)

template double	min (double const &first, double const &second)

template double	sqrt (double const &number)

template double	abs (double const &number)

template double	floor (double const &number)

template double	ceil (double const &number)

template double	round (double const &number)

template double	log (double const &number)

template double	log10 (double const &number)

template double	cos (double const &number)

template double	sin (double const &number)

template NumberTraits< double >::IntegerType	trunc (double const &number)

template double	mod (double const &first, double const &second)

template std::string	to_string (double const &value)

template bool	isOne (int const &value)

template bool	isZero (int const &value)

template bool	isConstant (int const &value)

template bool	isInfinity (int const &value)

template bool	isNonNegative (int const &value)

template bool	isPositive (int const &value)

template bool	isApproxEqual (int const &a, int const &b, int const &precision, bool relative)

template bool	isBetween (int const &a, int const &b, int const &c, bool strict)

template bool	isOne (uint32_t const &value)

template bool	isZero (uint32_t const &value)

template bool	isConstant (uint32_t const &value)

template bool	isNonNegative (uint32_t const &value)

template bool	isPositive (uint32_t const &value)

template bool	isInfinity (uint32_t const &value)

template bool	isBetween (uint32_t const &a, uint32_t const &b, uint32_t const &c, bool strict)

template bool	isApproxEqual (storm::storage::sparse::state_type const &a, storm::storage::sparse::state_type const &b, storm::storage::sparse::state_type const &precision, bool relative)

template bool	isOne (storm::storage::sparse::state_type const &value)

template bool	isZero (storm::storage::sparse::state_type const &value)

template bool	isConstant (storm::storage::sparse::state_type const &value)

template bool	isPositive (storm::storage::sparse::state_type const &value)

template bool	isNonNegative (storm::storage::sparse::state_type const &value)

template bool	isInfinity (storm::storage::sparse::state_type const &value)

template bool	isBetween (storm::storage::sparse::state_type const &a, storm::storage::sparse::state_type const &b, storm::storage::sparse::state_type const &c, bool strict)

template unsigned long	convertNumber (long const &)

template bool	isNan (RationalFunction const &)

template bool	isOne (Interval const &value)

template bool	isZero (Interval const &value)

template bool	isInfinity (Interval const &value)

template bool	isAlmostZero (Interval const &value)

template bool	isNonNegative (Interval const &value)

template bool	isPositive (Interval const &value)

template bool	isBetween (Interval const &, Interval const &, Interval const &value, bool)

template std::string	to_string (storm::Interval const &value)

template<typename ValueType >
std::pair< ValueType, ValueType >	asFraction (ValueType const &number)

template<typename IndexType , typename ValueType >
storm::storage::MatrixEntry< IndexType, ValueType > &	simplify (storm::storage::MatrixEntry< IndexType, ValueType > &matrixEntry)

template<typename IndexType , typename ValueType >
storm::storage::MatrixEntry< IndexType, ValueType > &&	simplify (storm::storage::MatrixEntry< IndexType, ValueType > &&matrixEntry)

template<typename RationalType >
NumberTraits< RationalType >::IntegerType	numerator (RationalType const &number)

template<typename RationalType >
NumberTraits< RationalType >::IntegerType	denominator (RationalType const &number)

std::vector< Engine >	getEngines ()
	Returns a list of all available engines (excluding Unknown)

std::string	toString (Engine const &engine)
	Returns a string representation of the given engine.

std::ostream &	operator<< (std::ostream &os, Engine const &engine)
	Writes the string representation of the given engine to the given stream.

Engine	engineFromString (std::string const &engineStr)
	Parses the string representation of an engine and returns the corresponding engine.

storm::builder::BuilderType	getBuilderType (storm::utility::Engine const &engine)
	Returns the builder type used for the given engine.

template<typename ValueType >
bool	canHandle (storm::utility::Engine const &engine, storm::storage::SymbolicModelDescription::ModelType const &modelType, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask)

template<>
bool	canHandle< storm::RationalFunction > (storm::utility::Engine const &engine, storm::storage::SymbolicModelDescription::ModelType const &modelType, storm::modelchecker::CheckTask< storm::logic::Formula, storm::RationalFunction > const &checkTask)

template<typename ValueType >
bool	canHandle (storm::utility::Engine const &engine, std::vector< storm::jani::Property > const &properties, storm::storage::SymbolicModelDescription const &modelDescription)
	Returns false if the given model description and one of the given properties can certainly not be handled by the given engine.

template bool	canHandle< double > (storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)

template bool	canHandle< storm::RationalNumber > (storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)

template bool	canHandle< storm::RationalFunction > (storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)

template<typename RewardModelType >
FilteredRewardModel< RewardModelType >	createFilteredRewardModel (RewardModelType const &baseRewardModel, storm::logic::RewardAccumulation const &acc, bool isDiscreteTimeModel)

template<typename RewardModelType , typename FormulaType >
FilteredRewardModel< RewardModelType >	createFilteredRewardModel (RewardModelType const &baseRewardModel, bool isDiscreteTimeModel, FormulaType const &formula)

template<typename ModelType , typename CheckTaskType >
FilteredRewardModel< typename ModelType::RewardModelType >	createFilteredRewardModel (ModelType const &model, CheckTaskType const &checkTask)

void	initializeLogger ()
	Initializes the logging framework and sets up logging to console.

void	setOutputDigits (int digits)
	Set number of digits for printing output.

void	setUp ()
	Performs some necessary initializations.

void	cleanUp ()
	Performs some necessary clean-up.

void	setOutputDigitsFromGeneralPrecision (double precision)
	Set number of digits for printing output from given precision requirement.

l3pp::LogLevel	getLogLevel ()
	Gets the global log level.

void	setLogLevel (l3pp::LogLevel level)
	Set the global log level.

void	initializeFileLogging (std::string const &logfileName)
	Sets up the logging to file.

std::ostream &	operator<< (std::ostream &out, Stopwatch const &stopwatch)

uint64_t	getNumberOfThreads ()

Typedef Documentation

◆ ElementGreater

template<typename ValueType >

using storm::utility::ElementGreater = typedef typename detail::ElementGreater<ValueType>::type

Definition at line 71 of file constants.h.

◆ ElementLess

template<typename ValueType >

using storm::utility::ElementLess = typedef typename detail::ElementLess<ValueType>::type

Definition at line 68 of file constants.h.

◆ Maximum

template<typename ValueType >

using storm::utility::Maximum = typedef Extremum<storm::OptimizationDirection::Maximize, ValueType>

Definition at line 127 of file Extremum.h.

◆ Minimum

template<typename ValueType >

using storm::utility::Minimum = typedef Extremum<storm::OptimizationDirection::Minimize, ValueType>

Definition at line 129 of file Extremum.h.

Enumeration Type Documentation

◆ Engine

enum class storm::utility::Engine

strong

An enumeration of all engines.

Enumerator
Sparse
Hybrid
Dd
DdSparse
Exploration
AbstractionRefinement
Automatic
Unknown

Definition at line 31 of file Engine.h.

Function Documentation

◆ abs() [1/3]

template double storm::utility::abs ( double const & number )

◆ abs() [2/3]

template<>

storm::Interval storm::utility::abs ( storm::Interval const & interval )

Definition at line 1044 of file constants.cpp.

◆ abs() [3/3]

template<typename ValueType >

ValueType storm::utility::abs ( ValueType const & number )

Definition at line 262 of file constants.cpp.

◆ asFraction()

template<typename ValueType >

std::pair< ValueType, ValueType > storm::utility::asFraction ( ValueType const & number )

◆ canHandle() [1/2]

template<typename ValueType >

bool storm::utility::canHandle	(	storm::utility::Engine const &	engine,
		std::vector< storm::jani::Property > const &	properties,
		storm::storage::SymbolicModelDescription const &	modelDescription
	)

Returns false if the given model description and one of the given properties can certainly not be handled by the given engine.

Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true, the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need to actually build the model in order to decide whether it is supported.

Definition at line 260 of file Engine.cpp.

◆ canHandle() [2/2]

template<typename ValueType >

bool storm::utility::canHandle	(	storm::utility::Engine const &	engine,
		storm::storage::SymbolicModelDescription::ModelType const &	modelType,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	checkTask
	)

Definition at line 101 of file Engine.cpp.

◆ canHandle< double >()

template bool storm::utility::canHandle< double >	(	storm::utility::Engine const &	,
		std::vector< storm::jani::Property > const &	,
		storm::storage::SymbolicModelDescription const &
	)

◆ canHandle< storm::RationalFunction >() [1/2]

template bool storm::utility::canHandle< storm::RationalFunction >	(	storm::utility::Engine const &	,
		std::vector< storm::jani::Property > const &	,
		storm::storage::SymbolicModelDescription const &
	)

◆ canHandle< storm::RationalFunction >() [2/2]

template<>

bool storm::utility::canHandle< storm::RationalFunction >	(	storm::utility::Engine const &	engine,
		storm::storage::SymbolicModelDescription::ModelType const &	modelType,
		storm::modelchecker::CheckTask< storm::logic::Formula, storm::RationalFunction > const &	checkTask
	)

Definition at line 198 of file Engine.cpp.

◆ canHandle< storm::RationalNumber >()

template bool storm::utility::canHandle< storm::RationalNumber >	(	storm::utility::Engine const &	,
		std::vector< storm::jani::Property > const &	,
		storm::storage::SymbolicModelDescription const &
	)

◆ ceil() [1/2]

template double storm::utility::ceil ( double const & number )

◆ ceil() [2/2]

template<typename ValueType >

ValueType storm::utility::ceil ( ValueType const & number )

Definition at line 272 of file constants.cpp.

◆ cleanUp()

void storm::utility::cleanUp ( )

Performs some necessary clean-up.

Definition at line 37 of file initialize.cpp.

◆ convertNumber() [1/20]

template<>

uint_fast64_t storm::utility::convertNumber ( double const & number )

Definition at line 139 of file constants.cpp.

◆ convertNumber() [2/20]

template<>

int_fast64_t storm::utility::convertNumber ( double const & number )

Definition at line 144 of file constants.cpp.

◆ convertNumber() [3/20]

template<>

double storm::utility::convertNumber ( double const & number )

Definition at line 154 of file constants.cpp.

◆ convertNumber() [4/20]

template<>

RationalFunction storm::utility::convertNumber ( double const & number )

Definition at line 823 of file constants.cpp.

◆ convertNumber() [5/20]

template<>

storm::Interval storm::utility::convertNumber ( double const & number )

Definition at line 1002 of file constants.cpp.

◆ convertNumber() [6/20]

template<>

RationalFunction storm::utility::convertNumber ( int_fast64_t const & number )

Definition at line 828 of file constants.cpp.

◆ convertNumber() [7/20]

template double storm::utility::convertNumber ( long const & )

◆ convertNumber() [8/20]

template<>

double storm::utility::convertNumber ( long long const & number )

Definition at line 159 of file constants.cpp.

◆ convertNumber() [9/20]

template<>

storm::storage::sparse::state_type storm::utility::convertNumber ( long long const & number )

Definition at line 164 of file constants.cpp.

◆ convertNumber() [10/20]

template<>

carl::uint storm::utility::convertNumber ( RationalFunction const & func )

Definition at line 859 of file constants.cpp.

◆ convertNumber() [11/20]

template<>

carl::sint storm::utility::convertNumber ( RationalFunction const & func )

Definition at line 864 of file constants.cpp.

◆ convertNumber() [12/20]

template<>

double storm::utility::convertNumber ( RationalFunction const & func )

Definition at line 869 of file constants.cpp.

◆ convertNumber() [13/20]

template<>

RationalFunction storm::utility::convertNumber ( RationalFunction const & number )

Definition at line 874 of file constants.cpp.

◆ convertNumber() [14/20]

template<typename TargetType , typename SourceType >

TargetType storm::utility::convertNumber ( SourceType const & number )

Definition at line 134 of file constants.cpp.

◆ convertNumber() [15/20]

template<>

RationalFunction storm::utility::convertNumber ( std::string const & number )

Definition at line 879 of file constants.cpp.

◆ convertNumber() [16/20]

template<>

double storm::utility::convertNumber ( std::string const & value )

Definition at line 997 of file constants.cpp.

◆ convertNumber() [17/20]

template<>

double storm::utility::convertNumber ( storm::Interval const & number )

Definition at line 1038 of file constants.cpp.

◆ convertNumber() [18/20]

template<>

RationalFunction storm::utility::convertNumber ( storm::storage::sparse::state_type const & number )

Definition at line 884 of file constants.cpp.

◆ convertNumber() [19/20]

template<>

storm::Interval storm::utility::convertNumber ( uint64_t const & number )

Definition at line 1007 of file constants.cpp.

◆ convertNumber() [20/20]

template<>

double storm::utility::convertNumber ( uint_fast64_t const & number )

Definition at line 149 of file constants.cpp.

◆ cos() [1/2]

template double storm::utility::cos ( double const & number )

◆ cos() [2/2]

template<typename ValueType >

ValueType storm::utility::cos ( ValueType const & number )

Definition at line 293 of file constants.cpp.

◆ createFilteredRewardModel() [1/3]

template<typename ModelType , typename CheckTaskType >

FilteredRewardModel< typename ModelType::RewardModelType > storm::utility::createFilteredRewardModel	(	ModelType const &	model,
		CheckTaskType const &	checkTask
	)

Definition at line 96 of file FilteredRewardModel.h.

◆ createFilteredRewardModel() [2/3]

template<typename RewardModelType , typename FormulaType >

FilteredRewardModel< RewardModelType > storm::utility::createFilteredRewardModel	(	RewardModelType const &	baseRewardModel,
		bool	isDiscreteTimeModel,
		FormulaType const &	formula
	)

Definition at line 87 of file FilteredRewardModel.h.

◆ createFilteredRewardModel() [3/3]

template<typename RewardModelType >

FilteredRewardModel< RewardModelType > storm::utility::createFilteredRewardModel	(	RewardModelType const &	baseRewardModel,
		storm::logic::RewardAccumulation const &	acc,
		bool	isDiscreteTimeModel
	)

Definition at line 75 of file FilteredRewardModel.h.

◆ denominator()

template<typename RationalType >

NumberTraits< RationalType >::IntegerType storm::utility::denominator ( RationalType const & number )

◆ divide()

template<typename IntegerType >

std::pair< IntegerType, IntegerType > storm::utility::divide	(	IntegerType const &	dividend,
		IntegerType const &	divisor
	)

(Integer-)Divides the dividend by the divisor and returns the result plus the remainder.

Definition at line 325 of file constants.cpp.

◆ engineFromString()

Engine storm::utility::engineFromString ( std::string const & engineStr )

Parses the string representation of an engine and returns the corresponding engine.

If the engine is not found, we print an error and return Engine::Unknown.

Definition at line 66 of file Engine.cpp.

◆ floor() [1/2]

template double storm::utility::floor ( double const & number )

◆ floor() [2/2]

template<typename ValueType >

ValueType storm::utility::floor ( ValueType const & number )

Definition at line 267 of file constants.cpp.

◆ getBuilderType()

storm::builder::BuilderType storm::utility::getBuilderType ( Engine const & engine )

Returns the builder type used for the given engine.

Definition at line 80 of file Engine.cpp.

◆ getEngines()

std::vector< Engine > storm::utility::getEngines ( )

Returns a list of all available engines (excluding Unknown)

Definition at line 29 of file Engine.cpp.

◆ getLogLevel()

l3pp::LogLevel storm::utility::getLogLevel ( )

Gets the global log level.

Definition at line 55 of file initialize.cpp.

◆ getNumberOfThreads()

uint64_t storm::utility::getNumberOfThreads ( )

Definition at line 53 of file threads.cpp.

◆ infinity() [1/2]

template<typename ValueType >

ValueType storm::utility::infinity ( )

Definition at line 28 of file constants.cpp.

◆ infinity() [2/2]

template<>

storm::RationalFunction storm::utility::infinity ( )

Definition at line 765 of file constants.cpp.

◆ initializeFileLogging()

void storm::utility::initializeFileLogging ( std::string const & logfileName )

Sets up the logging to file.

Definition at line 68 of file initialize.cpp.

◆ initializeLogger()

void storm::utility::initializeLogger ( )

Initializes the logging framework and sets up logging to console.

Definition at line 10 of file initialize.cpp.

◆ isAlmostOne() [1/3]

template bool storm::utility::isAlmostOne ( double const & value )

◆ isAlmostOne() [2/3]

template<>

bool storm::utility::isAlmostOne ( storm::RationalFunction const & a )

Definition at line 918 of file constants.cpp.

◆ isAlmostOne() [3/3]

template<typename ValueType >

bool storm::utility::isAlmostOne ( ValueType const & a )

Definition at line 97 of file constants.cpp.

◆ isAlmostZero() [1/4]

template bool storm::utility::isAlmostZero ( double const & value )

◆ isAlmostZero() [2/4]

template bool storm::utility::isAlmostZero ( Interval const & value )

◆ isAlmostZero() [3/4]

template<>

bool storm::utility::isAlmostZero ( storm::RationalFunction const & a )

Definition at line 913 of file constants.cpp.

◆ isAlmostZero() [4/4]

template<typename ValueType >

bool storm::utility::isAlmostZero ( ValueType const & a )

Definition at line 92 of file constants.cpp.

◆ isApproxEqual() [1/6]

template bool storm::utility::isApproxEqual	(	double const &	a,
		double const &	b,
		double const &	precision,
		bool	relative
	)

◆ isApproxEqual() [2/6]

template bool storm::utility::isApproxEqual	(	int const &	a,
		int const &	b,
		int const &	precision,
		bool	relative
	)

◆ isApproxEqual() [3/6]

template<>

bool storm::utility::isApproxEqual	(	storm::Interval const &	a,
		storm::Interval const &	b,
		storm::Interval const &	precision,
		bool	relative
	)

Definition at line 1049 of file constants.cpp.

◆ isApproxEqual() [4/6]

template<>

bool storm::utility::isApproxEqual	(	storm::RationalFunction const &	a,
		storm::RationalFunction const &	b,
		storm::RationalFunction const &	precision,
		bool	relative
	)

Definition at line 801 of file constants.cpp.

◆ isApproxEqual() [5/6]

template bool storm::utility::isApproxEqual	(	storm::storage::sparse::state_type const &	a,
		storm::storage::sparse::state_type const &	b,
		storm::storage::sparse::state_type const &	precision,
		bool	relative
	)

◆ isApproxEqual() [6/6]

template<typename ValueType >

bool storm::utility::isApproxEqual	(	ValueType const &	a,
		ValueType const &	b,
		ValueType const &	precision,
		bool	relative
	)

Definition at line 53 of file constants.cpp.

◆ isBetween() [1/7]

template bool storm::utility::isBetween	(	double const &	a,
		double const &	b,
		double const &	c,
		bool	strict
	)

◆ isBetween() [2/7]

template bool storm::utility::isBetween	(	int const &	a,
		int const &	b,
		int const &	c,
		bool	strict
	)

◆ isBetween() [3/7]

template bool storm::utility::isBetween	(	Interval const &	,
		Interval const &	,
		Interval const &	value,
		bool
	)

◆ isBetween() [4/7]

template<>

bool storm::utility::isBetween	(	storm::RationalFunction const &	a,
		storm::RationalFunction const &	b,
		storm::RationalFunction const &	c,
		bool	strict
	)

Definition at line 933 of file constants.cpp.

◆ isBetween() [5/7]

template bool storm::utility::isBetween	(	storm::storage::sparse::state_type const &	a,
		storm::storage::sparse::state_type const &	b,
		storm::storage::sparse::state_type const &	c,
		bool	strict
	)

◆ isBetween() [6/7]

template bool storm::utility::isBetween	(	uint32_t const &	a,
		uint32_t const &	b,
		uint32_t const &	c,
		bool	strict
	)

◆ isBetween() [7/7]

template<typename ValueType >

bool storm::utility::isBetween	(	ValueType const &	a,
		ValueType const &	b,
		ValueType const &	c,
		bool	strict
	)

Compare whether a <= b <= c or a < b < c, based on the strictness parameter.

Check whether a <= b <= c holds (if not strict, the default) or a < b < c (if strict).

Parameters

a	A constant value
b	Some value
c	A constant value
strict	Changes the type of the comparison

Returns: true if b is between a and c.

Definition at line 81 of file constants.cpp.

◆ isConstant() [1/8]

template bool storm::utility::isConstant ( double const & value )

◆ isConstant() [2/8]

template bool storm::utility::isConstant ( int const & value )

◆ isConstant() [3/8]

template<>

bool storm::utility::isConstant ( storm::Interval const & a )

Definition at line 807 of file constants.cpp.

◆ isConstant() [4/8]

template<>

bool storm::utility::isConstant ( storm::Polynomial const & a )

Definition at line 796 of file constants.cpp.

◆ isConstant() [5/8]

template<>

bool storm::utility::isConstant ( storm::RationalFunction const & a )

Definition at line 791 of file constants.cpp.

◆ isConstant() [6/8]

template bool storm::utility::isConstant ( storm::storage::sparse::state_type const & value )

◆ isConstant() [7/8]

template bool storm::utility::isConstant ( uint32_t const & value )

◆ isConstant() [8/8]

template<typename ValueType >

bool storm::utility::isConstant ( ValueType const & )

Definition at line 102 of file constants.cpp.

◆ isInfinity() [1/7]

template bool storm::utility::isInfinity ( double const & value )

◆ isInfinity() [2/7]

template bool storm::utility::isInfinity ( int const & value )

◆ isInfinity() [3/7]

template bool storm::utility::isInfinity ( Interval const & value )

◆ isInfinity() [4/7]

template<>

bool storm::utility::isInfinity ( storm::RationalFunction const & a )

Definition at line 812 of file constants.cpp.

◆ isInfinity() [5/7]

template bool storm::utility::isInfinity ( storm::storage::sparse::state_type const & value )

◆ isInfinity() [6/7]

template bool storm::utility::isInfinity ( uint32_t const & value )

◆ isInfinity() [7/7]

template<typename ValueType >

bool storm::utility::isInfinity ( ValueType const & a )

Definition at line 107 of file constants.cpp.

◆ isInteger() [1/6]

template bool storm::utility::isInteger ( double const & number )

◆ isInteger() [2/6]

template<>

bool storm::utility::isInteger ( int const & )

Definition at line 119 of file constants.cpp.

◆ isInteger() [3/6]

template<>

bool storm::utility::isInteger ( storm::RationalFunction const & func )

Definition at line 818 of file constants.cpp.

◆ isInteger() [4/6]

template<>

bool storm::utility::isInteger ( storm::storage::sparse::state_type const & )

Definition at line 129 of file constants.cpp.

◆ isInteger() [5/6]

template<>

bool storm::utility::isInteger ( uint32_t const & )

Definition at line 124 of file constants.cpp.

◆ isInteger() [6/6]

template<typename ValueType >

bool storm::utility::isInteger ( ValueType const & number )

Definition at line 112 of file constants.cpp.

◆ isNan() [1/3]

template<>

bool storm::utility::isNan ( double const & value )

Definition at line 48 of file constants.cpp.

◆ isNan() [2/3]

template bool storm::utility::isNan ( RationalFunction const & )

◆ isNan() [3/3]

template<typename ValueType >

bool storm::utility::isNan ( ValueType const & )

Definition at line 43 of file constants.cpp.

◆ isNonNegative() [1/7]

template bool storm::utility::isNonNegative ( double const & value )

◆ isNonNegative() [2/7]

template bool storm::utility::isNonNegative ( int const & value )

◆ isNonNegative() [3/7]

template bool storm::utility::isNonNegative ( Interval const & value )

◆ isNonNegative() [4/7]

template<>

bool storm::utility::isNonNegative ( storm::RationalFunction const & a )

Definition at line 923 of file constants.cpp.

◆ isNonNegative() [5/7]

template bool storm::utility::isNonNegative ( storm::storage::sparse::state_type const & value )

◆ isNonNegative() [6/7]

template bool storm::utility::isNonNegative ( uint32_t const & value )

◆ isNonNegative() [7/7]

template<typename ValueType >

bool storm::utility::isNonNegative ( ValueType const & a )

Definition at line 68 of file constants.cpp.

◆ isOne() [1/8]

template bool storm::utility::isOne ( double const & value )

◆ isOne() [2/8]

template bool storm::utility::isOne ( int const & value )

◆ isOne() [3/8]

template bool storm::utility::isOne ( Interval const & value )

◆ isOne() [4/8]

template<>

bool storm::utility::isOne ( storm::Polynomial const & a )

Definition at line 776 of file constants.cpp.

◆ isOne() [5/8]

template<>

bool storm::utility::isOne ( storm::RationalFunction const & a )

Definition at line 771 of file constants.cpp.

◆ isOne() [6/8]

template bool storm::utility::isOne ( storm::storage::sparse::state_type const & value )

◆ isOne() [7/8]

template bool storm::utility::isOne ( uint32_t const & value )

◆ isOne() [8/8]

template<typename ValueType >

bool storm::utility::isOne ( ValueType const & a )

Definition at line 33 of file constants.cpp.

◆ isPositive() [1/7]

template bool storm::utility::isPositive ( double const & value )

◆ isPositive() [2/7]

template bool storm::utility::isPositive ( int const & value )

◆ isPositive() [3/7]

template bool storm::utility::isPositive ( Interval const & value )

◆ isPositive() [4/7]

template<>

bool storm::utility::isPositive ( storm::RationalFunction const & a )

Definition at line 928 of file constants.cpp.

◆ isPositive() [5/7]

template bool storm::utility::isPositive ( storm::storage::sparse::state_type const & value )

◆ isPositive() [6/7]

template bool storm::utility::isPositive ( uint32_t const & value )

◆ isPositive() [7/7]

template<typename ValueType >

bool storm::utility::isPositive ( ValueType const & a )

Definition at line 63 of file constants.cpp.

◆ isZero() [1/8]

template bool storm::utility::isZero ( double const & value )

◆ isZero() [2/8]

template bool storm::utility::isZero ( int const & value )

◆ isZero() [3/8]

template bool storm::utility::isZero ( Interval const & value )

◆ isZero() [4/8]

template<>

bool storm::utility::isZero ( storm::Polynomial const & a )

Definition at line 786 of file constants.cpp.

◆ isZero() [5/8]

template<>

bool storm::utility::isZero ( storm::RationalFunction const & a )

Definition at line 781 of file constants.cpp.

◆ isZero() [6/8]

template bool storm::utility::isZero ( storm::storage::sparse::state_type const & value )

◆ isZero() [7/8]

template bool storm::utility::isZero ( uint32_t const & value )

◆ isZero() [8/8]

template<typename ValueType >

bool storm::utility::isZero ( ValueType const & a )

Definition at line 38 of file constants.cpp.

◆ log() [1/2]

template double storm::utility::log ( double const & number )

◆ log() [2/2]

template<typename ValueType >

ValueType storm::utility::log ( ValueType const & number )

Definition at line 283 of file constants.cpp.

◆ log10() [1/2]

template double storm::utility::log10 ( double const & number )

◆ log10() [2/2]

template<typename ValueType >

ValueType storm::utility::log10 ( ValueType const & number )

Definition at line 288 of file constants.cpp.

◆ max() [1/2]

template double storm::utility::max	(	double const &	first,
		double const &	second
	)

◆ max() [2/2]

template<typename ValueType >

ValueType storm::utility::max	(	ValueType const &	first,
		ValueType const &	second
	)

Definition at line 247 of file constants.cpp.

◆ maximum() [1/6]

template<typename K , typename ValueType >

ValueType storm::utility::maximum ( std::map< K, ValueType > const & values )

Definition at line 237 of file constants.cpp.

◆ maximum() [2/6]

template double storm::utility::maximum ( std::map< uint64_t, double > const & )

◆ maximum() [3/6]

template<>

storm::RationalFunction storm::utility::maximum ( std::map< uint64_t, storm::RationalFunction > const & )

Definition at line 966 of file constants.cpp.

◆ maximum() [4/6]

template double storm::utility::maximum ( std::vector< double > const & )

◆ maximum() [5/6]

template<>

storm::RationalFunction storm::utility::maximum ( std::vector< storm::RationalFunction > const & )

Definition at line 951 of file constants.cpp.

◆ maximum() [6/6]

template<typename ValueType >

ValueType storm::utility::maximum ( std::vector< ValueType > const & values )

Definition at line 204 of file constants.cpp.

◆ min() [1/2]

template double storm::utility::min	(	double const &	first,
		double const &	second
	)

◆ min() [2/2]

template<typename ValueType >

ValueType storm::utility::min	(	ValueType const &	first,
		ValueType const &	second
	)

Definition at line 252 of file constants.cpp.

◆ minimum() [1/6]

template<typename K , typename ValueType >

ValueType storm::utility::minimum ( std::map< K, ValueType > const & values )

Definition at line 232 of file constants.cpp.

◆ minimum() [2/6]

template double storm::utility::minimum ( std::map< uint64_t, double > const & )

◆ minimum() [3/6]

template<>

storm::RationalFunction storm::utility::minimum ( std::map< uint64_t, storm::RationalFunction > const & )

Definition at line 961 of file constants.cpp.

◆ minimum() [4/6]

template double storm::utility::minimum ( std::vector< double > const & )

◆ minimum() [5/6]

template<>

storm::RationalFunction storm::utility::minimum ( std::vector< storm::RationalFunction > const & )

Definition at line 946 of file constants.cpp.

◆ minimum() [6/6]

template<typename ValueType >

ValueType storm::utility::minimum ( std::vector< ValueType > const & values )

Definition at line 192 of file constants.cpp.

◆ minmax() [1/6]

template<typename K , typename ValueType >

std::pair< ValueType, ValueType > storm::utility::minmax ( std::map< K, ValueType > const & values )

Definition at line 216 of file constants.cpp.

◆ minmax() [2/6]

template std::pair< double, double > storm::utility::minmax ( std::map< uint64_t, double > const & )

◆ minmax() [3/6]

template<>

std::pair< storm::RationalFunction, storm::RationalFunction > storm::utility::minmax ( std::map< uint64_t, storm::RationalFunction > const & )

Definition at line 956 of file constants.cpp.

◆ minmax() [4/6]

template std::pair< double, double > storm::utility::minmax ( std::vector< double > const & )

◆ minmax() [5/6]

template<>

std::pair< storm::RationalFunction, storm::RationalFunction > storm::utility::minmax ( std::vector< storm::RationalFunction > const & )

Definition at line 941 of file constants.cpp.

◆ minmax() [6/6]

template<typename ValueType >

std::pair< ValueType, ValueType > storm::utility::minmax ( std::vector< ValueType > const & values )

Definition at line 176 of file constants.cpp.

◆ mod() [1/2]

template double storm::utility::mod	(	double const &	first,
		double const &	second
	)

◆ mod() [2/2]

template<typename IntegerType >

IntegerType storm::utility::mod	(	IntegerType const &	first,
		IntegerType const &	second
	)

Definition at line 320 of file constants.cpp.

◆ numDigits()

template<typename ValueType >

uint64_t storm::utility::numDigits ( ValueType const & number )

Definition at line 303 of file constants.cpp.

◆ numerator()

template<typename RationalType >

NumberTraits< RationalType >::IntegerType storm::utility::numerator ( RationalType const & number )

◆ one() [1/2]

template<typename ValueType >

ValueType storm::utility::one ( )

Definition at line 18 of file constants.cpp.

◆ one() [2/2]

template double storm::utility::one ( )

◆ operator<<() [1/2]

std::ostream & storm::utility::operator<<	(	std::ostream &	os,
		Engine const &	engine
	)

Writes the string representation of the given engine to the given stream.

Definition at line 61 of file Engine.cpp.

◆ operator<<() [2/2]

std::ostream & storm::utility::operator<<	(	std::ostream &	out,
		Stopwatch const &	stopwatch
	)

Definition at line 68 of file Stopwatch.cpp.

◆ pow() [1/3]

template double storm::utility::pow	(	double const &	value,
		int_fast64_t	exponent
	)

◆ pow() [2/3]

template<>

RationalFunction storm::utility::pow	(	RationalFunction const &	value,
		int_fast64_t	exponent
	)

Definition at line 971 of file constants.cpp.

◆ pow() [3/3]

template<typename ValueType >

ValueType storm::utility::pow	(	ValueType const &	value,
		int_fast64_t	exponent
	)

Definition at line 242 of file constants.cpp.

◆ round() [1/2]

template double storm::utility::round ( double const & number )

◆ round() [2/2]

template<typename ValueType >

ValueType storm::utility::round ( ValueType const & number )

Definition at line 277 of file constants.cpp.

◆ setLogLevel()

void storm::utility::setLogLevel ( l3pp::LogLevel level )

Set the global log level.

Definition at line 59 of file initialize.cpp.

◆ setOutputDigits()

void storm::utility::setOutputDigits ( int digits )

Set number of digits for printing output.

Parameters

digits Number of digits to print.

Definition at line 28 of file initialize.cpp.

◆ setOutputDigitsFromGeneralPrecision()

void storm::utility::setOutputDigitsFromGeneralPrecision ( double precision )

Set number of digits for printing output from given precision requirement.

For a precision of 1e-n we output at least n digits.

Parameters

precision General precision.

Definition at line 41 of file initialize.cpp.

◆ setUp()

void storm::utility::setUp ( )

Performs some necessary initializations.

Definition at line 32 of file initialize.cpp.

◆ simplify() [1/9]

template double storm::utility::simplify ( double value )

◆ simplify() [2/9]

template<>

RationalFunction && storm::utility::simplify ( RationalFunction && value )

Definition at line 907 of file constants.cpp.

◆ simplify() [3/9]

template<>

RationalFunction && storm::utility::simplify ( RationalFunction && value )

Definition at line 907 of file constants.cpp.

◆ simplify() [4/9]

template<>

RationalFunction & storm::utility::simplify ( RationalFunction & value )

Definition at line 901 of file constants.cpp.

◆ simplify() [5/9]

template<>

RationalFunction & storm::utility::simplify ( RationalFunction & value )

Definition at line 901 of file constants.cpp.

◆ simplify() [6/9]

template<>

RationalFunction storm::utility::simplify ( RationalFunction value )

Definition at line 895 of file constants.cpp.

◆ simplify() [7/9]

template<typename IndexType , typename ValueType >

storm::storage::MatrixEntry< IndexType, ValueType > && storm::utility::simplify ( storm::storage::MatrixEntry< IndexType, ValueType > && matrixEntry )

◆ simplify() [8/9]

template<typename IndexType , typename ValueType >

storm::storage::MatrixEntry< IndexType, ValueType > & storm::utility::simplify ( storm::storage::MatrixEntry< IndexType, ValueType > & matrixEntry )

◆ simplify() [9/9]

template<typename ValueType >

ValueType storm::utility::simplify ( ValueType value )

Definition at line 169 of file constants.cpp.

◆ sin() [1/2]

template double storm::utility::sin ( double const & number )

◆ sin() [2/2]

template<typename ValueType >

ValueType storm::utility::sin ( ValueType const & number )

Definition at line 298 of file constants.cpp.

◆ sqrt() [1/2]

template double storm::utility::sqrt ( double const & number )

◆ sqrt() [2/2]

template<typename ValueType >

ValueType storm::utility::sqrt ( ValueType const & number )

Definition at line 257 of file constants.cpp.

◆ to_string() [1/4]

template std::string storm::utility::to_string ( double const & value )

◆ to_string() [2/4]

template<>

std::string storm::utility::to_string ( RationalFunction const & f )

Definition at line 980 of file constants.cpp.

◆ to_string() [3/4]

template std::string storm::utility::to_string ( storm::Interval const & value )

◆ to_string() [4/4]

template<typename ValueType >

std::string storm::utility::to_string ( ValueType const & value )

Definition at line 330 of file constants.cpp.

◆ toString()

std::string storm::utility::toString ( Engine const & engine )

Returns a string representation of the given engine.

Definition at line 37 of file Engine.cpp.

◆ trunc() [1/2]

template NumberTraits< double >::IntegerType storm::utility::trunc ( double const & number )

◆ trunc() [2/2]

template<typename ValueType >

NumberTraits< ValueType >::IntegerType storm::utility::trunc ( ValueType const & number )

Definition at line 315 of file constants.cpp.

◆ zero() [1/2]

template<typename ValueType >

ValueType storm::utility::zero ( )

Definition at line 23 of file constants.cpp.

◆ zero() [2/2]

template double storm::utility::zero ( )

Namespaces

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ ElementGreater

◆ ElementLess

◆ Maximum

◆ Minimum

Enumeration Type Documentation

◆ Engine

Function Documentation

◆ abs() [1/3]

◆ abs() [2/3]

◆ abs() [3/3]

◆ asFraction()

◆ canHandle() [1/2]

◆ canHandle() [2/2]

◆ canHandle< double >()

◆ canHandle< storm::RationalFunction >() [1/2]

◆ canHandle< storm::RationalFunction >() [2/2]

◆ canHandle< storm::RationalNumber >()

◆ ceil() [1/2]

◆ ceil() [2/2]

◆ cleanUp()

◆ convertNumber() [1/20]

◆ convertNumber() [2/20]

◆ convertNumber() [3/20]

◆ convertNumber() [4/20]

◆ convertNumber() [5/20]

◆ convertNumber() [6/20]

◆ convertNumber() [7/20]

◆ convertNumber() [8/20]

◆ convertNumber() [9/20]

◆ convertNumber() [10/20]

◆ convertNumber() [11/20]

◆ convertNumber() [12/20]

◆ convertNumber() [13/20]

◆ convertNumber() [14/20]

◆ convertNumber() [15/20]

◆ convertNumber() [16/20]

◆ convertNumber() [17/20]

◆ convertNumber() [18/20]

◆ convertNumber() [19/20]

◆ convertNumber() [20/20]

◆ cos() [1/2]

◆ cos() [2/2]

◆ createFilteredRewardModel() [1/3]

◆ createFilteredRewardModel() [2/3]

◆ createFilteredRewardModel() [3/3]

◆ denominator()

◆ divide()

◆ engineFromString()

◆ floor() [1/2]

◆ floor() [2/2]

◆ getBuilderType()

◆ getEngines()

◆ getLogLevel()

◆ getNumberOfThreads()

◆ infinity() [1/2]

◆ infinity() [2/2]

◆ initializeFileLogging()

◆ initializeLogger()

◆ isAlmostOne() [1/3]

◆ isAlmostOne() [2/3]

◆ isAlmostOne() [3/3]

◆ isAlmostZero() [1/4]

◆ isAlmostZero() [2/4]

◆ isAlmostZero() [3/4]

◆ isAlmostZero() [4/4]

◆ isApproxEqual() [1/6]

◆ isApproxEqual() [2/6]

◆ isApproxEqual() [3/6]

◆ isApproxEqual() [4/6]

◆ isApproxEqual() [5/6]

◆ isApproxEqual() [6/6]

◆ isBetween() [1/7]

◆ isBetween() [2/7]

◆ isBetween() [3/7]