Namespaces
namespace	utility
namespace	jani
namespace	cli
namespace	storage
namespace	conv
namespace	api
namespace	prism
namespace	converter
namespace	settings
namespace	counterexamples
namespace	dft
namespace	parser
	Contains all file parsers and helper classes.
namespace	gbar
namespace	expressions
namespace	dd
namespace	models
namespace	modelchecker
namespace	builder
namespace	gspn
namespace	pars
namespace	logic
namespace	analysis
namespace	derivative
namespace	transformer
namespace	ps
namespace	pomdp
namespace	generator
namespace	adapters
namespace	detail
namespace	automata
namespace	solver
namespace	exceptions
namespace	io
namespace	simulator
namespace	umb
	Import and export of umb files.
namespace	bisimulation
namespace	optionalref_detail
	Helper to prevent OptionalRef's to rvalue types.
namespace	test

Classes
struct	StormVersion
struct	JsonSerialization
	Helper struct to enable json serialization. More...
class	SerializedEnum
class	CuddDdManagerEnvironment
struct	DdEnvironmentSelector
struct	DdEnvironmentSelector< storm::dd::DdType::CUDD >
struct	DdEnvironmentSelector< storm::dd::DdType::Sylvan >
class	DdEnvironment
class	SylvanDdManagerEnvironment
struct	InternalEnvironment
class	Environment
class	ExplorationEnvironment
class	ConditionalModelCheckerEnvironment
class	ModelCheckerEnvironment
class	MultiObjectiveModelCheckerEnvironment
class	EigenSolverEnvironment
class	EliminationSolverEnvironment
class	GameSolverEnvironment
class	GlpkSolverEnvironment
class	GmmxxSolverEnvironment
class	GurobiSolverEnvironment
class	LongRunAverageSolverEnvironment
class	MinMaxLpSolverEnvironment
class	MinMaxSolverEnvironment
class	MultiplierEnvironment
class	NativeSolverEnvironment
class	OviSolverEnvironment
class	SolverEnvironment
class	TimeBoundedSolverEnvironment
class	TopologicalSolverEnvironment
class	SubEnvironment
struct	NumberTraits
struct	NumberTraits< storm::utility::ExtendedNumber< ValueType > >
	An extended number is exactly as exact as what it extends, and it is the type that does have infinity – that is the whole point of it. More...
struct	NumberTraits< double >
struct	NumberTraits< storm::Interval >
struct	NumberTraits< storm::RationalInterval >
struct	NumberTraits< storm::RationalFunction >
struct	NullRefType
	Auxiliary struct used to identify OptionalRefs that do not contain a reference. More...
class	OptionalRef
	Helper class that optionally holds a reference to an object of type T. More...

Typedefs
using	BoundType = carl::BoundType
	Type describing the interval bounds.
typedef carl::Interval< double >	Interval
	Interval type.
typedef carl::Interval< storm::RationalNumber >	RationalInterval
template<typename ValueType>
using	IntervalBaseType = typename detail::IntervalMetaProgrammingHelper<ValueType>::BaseType
	Helper to access the type in which interval boundaries are stored.
template<typename ValueType>
using	json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, ValueType>
typedef carl::Cache< carl::PolynomialFactorizationPair< RawPolynomial > >	RawPolynomialCache
typedef carl::Relation	CompareRelation
typedef carl::Variable	RationalFunctionVariable
typedef carl::MultivariatePolynomial< RationalFunctionCoefficient >	RawPolynomial
typedef carl::UnivariatePolynomial< RationalFunctionCoefficient >	RawUnivariatePolynomial
typedef carl::FactorizedPolynomial< RawPolynomial >	Polynomial
typedef carl::RationalFunction< Polynomial, true >	RationalFunction
using	OptimizationDirection = solver::OptimizationDirection
using	UncertaintyResolutionModeSetting = solver::UncertaintyResolutionModeSetting
using	UncertaintyResolutionMode = solver::UncertaintyResolutionMode
using	ExtendedRationalNumber = storm::utility::ExtendedValueType<RationalNumber>
	The rational number type extended with the two infinities.
using	ExtendedRationalFunction = storm::utility::ExtendedValueType<RationalFunction>
	The rational function type extended with the two infinities.

Enumerations
enum class	ConditionalAlgorithmSetting { Default , Restart , Bisection , BisectionAdvanced , BisectionPolicyTracking , BisectionAdvancedPolicyTracking , PolicyIteration }
enum class	SteadyStateDistributionAlgorithm { Automatic , EquationSystem , ExpectedVisitingTimes , Classic }

Functions
template<typename ValueType>
bool	isJsonNumberExportAccurate (storm::json< ValueType > const &j)
template<typename ValueType, typename CallBack>
void	json_for_each_number_float (storm::json< ValueType > const &j, CallBack const &f)
template<typename ValueType>
void	warnIfJsonExportNotAccurate (storm::json< ValueType > const &j)
template<typename ValueType>
std::string	dumpJson (storm::json< ValueType > const &j, bool compact=false)
	Dumps the given json object, producing a String.
template std::string	dumpJson (storm::json< double > const &j, bool compact=false)
template std::string	dumpJson (storm::json< storm::RationalNumber > const &j, bool compact=false)
RationalFunctionVariable	createRFVariable (std::string const &name)
RationalFunctionVariable	findRFVariable (std::string const &name)
	Retrieves the (already existing) rational-function variable with the given name.
void	clearRFVariablePool ()
	Clears the global pool of rational-function variables.
template SylvanDdManagerEnvironment &	DdEnvironment::get< storm::dd::DdType::Sylvan > ()
template CuddDdManagerEnvironment &	DdEnvironment::get< storm::dd::DdType::CUDD > ()
std::ostream &	operator<< (std::ostream &stream, ConditionalAlgorithmSetting const &algorithm)
ConditionalAlgorithmSetting	conditionalAlgorithmSettingFromString (std::string const &algorithm)
template<class T>
	OptionalRef (T &) -> OptionalRef< T >
	deduction guides

Variables
template<typename ValueType>
constexpr bool	IsIntervalType = detail::IntervalMetaProgrammingHelper<ValueType>::isInterval
	Helper to check if a type is an interval.
constexpr NullRefType	NullRef {0}

Typedef Documentation

◆ BoundType

using storm::BoundType = carl::BoundType

Type describing the interval bounds.

Definition at line 27 of file IntervalAdapter.h.

◆ CompareRelation

typedef carl::Relation storm::CompareRelation

Definition at line 56 of file RationalFunctionAdapter.h.

◆ ExtendedRationalFunction

using storm::ExtendedRationalFunction = storm::utility::ExtendedValueType<RationalFunction>

The rational function type extended with the two infinities.

Like a rational number, a rational function has no infinity of its own, so this is what a result of that value type is held in.

Definition at line 708 of file ExtendedNumber.h.

◆ ExtendedRationalNumber

using storm::ExtendedRationalNumber = storm::utility::ExtendedValueType<RationalNumber>

The rational number type extended with the two infinities.

A rational number has no infinity of its own, so this is what a result of that value type is held in. It has a name because it is written often.

Definition at line 702 of file ExtendedNumber.h.

◆ Interval

typedef carl::Interval<double> storm::Interval

Interval type.

Definition at line 15 of file IntervalForward.h.

◆ IntervalBaseType

template<typename ValueType>

using storm::IntervalBaseType = typename detail::IntervalMetaProgrammingHelper<ValueType>::BaseType

Helper to access the type in which interval boundaries are stored.

Yields the type identity if the given type is not an interval

Definition at line 47 of file IntervalForward.h.

◆ json

template<typename ValueType>

using storm::json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, ValueType>

Definition at line 11 of file JsonForward.h.

◆ OptimizationDirection

using storm::OptimizationDirection = solver::OptimizationDirection

Definition at line 29 of file OptimizationDirection.h.

◆ Polynomial

typedef carl::FactorizedPolynomial<RawPolynomial> storm::Polynomial

Definition at line 46 of file RationalFunctionForward.h.

◆ RationalFunction

typedef carl::RationalFunction<Polynomial, true> storm::RationalFunction

Definition at line 47 of file RationalFunctionForward.h.

◆ RationalFunctionVariable

typedef carl::Variable storm::RationalFunctionVariable

Definition at line 26 of file RationalFunctionForward.h.

◆ RationalInterval

typedef carl::Interval<storm::RationalNumber> storm::RationalInterval

Definition at line 16 of file IntervalForward.h.

◆ RawPolynomial

typedef carl::MultivariatePolynomial<RationalFunctionCoefficient> storm::RawPolynomial

Definition at line 44 of file RationalFunctionForward.h.

◆ RawPolynomialCache

typedef carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial> > storm::RawPolynomialCache

Definition at line 55 of file RationalFunctionAdapter.h.

◆ RawUnivariatePolynomial

typedef carl::UnivariatePolynomial<RationalFunctionCoefficient> storm::RawUnivariatePolynomial

Definition at line 45 of file RationalFunctionForward.h.

◆ UncertaintyResolutionMode

using storm::UncertaintyResolutionMode = solver::UncertaintyResolutionMode

Definition at line 24 of file UncertaintyResolutionMode.h.

◆ UncertaintyResolutionModeSetting

using storm::UncertaintyResolutionModeSetting = solver::UncertaintyResolutionModeSetting

Definition at line 23 of file UncertaintyResolutionMode.h.

Enumeration Type Documentation

◆ ConditionalAlgorithmSetting

enum class storm::ConditionalAlgorithmSetting

strong

Enumerator
Default
Restart
Bisection
BisectionAdvanced
BisectionPolicyTracking
BisectionAdvancedPolicyTracking
PolicyIteration

Definition at line 8 of file ConditionalAlgorithmSetting.h.

◆ SteadyStateDistributionAlgorithm

enum class storm::SteadyStateDistributionAlgorithm

strong

Enumerator
Automatic
EquationSystem
ExpectedVisitingTimes
Classic

Definition at line 4 of file SteadyStateDistributionAlgorithm.h.

Function Documentation

◆ clearRFVariablePool()

void storm::clearRFVariablePool ( )

Clears the global pool of rational-function variables.

This is mainly used to reset the global state in-between tests.

Definition at line 12 of file RationalFunctionAdapter.cpp.

◆ conditionalAlgorithmSettingFromString()

ConditionalAlgorithmSetting storm::conditionalAlgorithmSettingFromString ( std::string const & algorithm )

Definition at line 25 of file ConditionalAlgorithmSetting.cpp.

◆ createRFVariable()

RationalFunctionVariable storm::createRFVariable ( std::string const & name )

Definition at line 4 of file RationalFunctionAdapter.cpp.

◆ DdEnvironment::get< storm::dd::DdType::CUDD >()

template CuddDdManagerEnvironment & storm::DdEnvironment::get< storm::dd::DdType::CUDD > ( )

◆ DdEnvironment::get< storm::dd::DdType::Sylvan >()

template SylvanDdManagerEnvironment & storm::DdEnvironment::get< storm::dd::DdType::Sylvan > ( )

◆ dumpJson() [1/3]

template std::string storm::dumpJson	(	storm::json< double > const &	j,
		bool	compact = false )

◆ dumpJson() [2/3]

template std::string storm::dumpJson	(	storm::json< storm::RationalNumber > const &	j,
		bool	compact = false )

◆ dumpJson() [3/3]

template<typename ValueType>

std::string storm::dumpJson	(	storm::json< ValueType > const &	j,
		bool	compact = false )

Dumps the given json object, producing a String.

If the ValueType is exact, a warning is printed if one or more number values can not be exported (dumped) with full accuracy (e.g. there is no float for 1/3)

Parameters

j	The JSON object
compact	indicates whether the export should be done in compact mode (no unnecessary whitespace)

Definition at line 60 of file JsonAdapter.cpp.

◆ findRFVariable()

RationalFunctionVariable storm::findRFVariable ( std::string const & name )

Retrieves the (already existing) rational-function variable with the given name.

Parameters

name	Variable name.

Returns: Variable with the given name or an invalid variable, if no such variable exists.

Definition at line 8 of file RationalFunctionAdapter.cpp.

◆ isJsonNumberExportAccurate()

template<typename ValueType>

bool storm::isJsonNumberExportAccurate ( storm::json< ValueType > const & j )

Precondition: j.is_number_float() must be true

Parameters

j	json object, must be of float type

Returns: true iff

Definition at line 12 of file JsonAdapter.cpp.

◆ json_for_each_number_float()

template<typename ValueType, typename CallBack>

void storm::json_for_each_number_float	(	storm::json< ValueType > const &	j,
		CallBack const &	f )

Definition at line 32 of file JsonAdapter.cpp.

◆ operator<<()

std::ostream & storm::operator<<	(	std::ostream &	stream,
		ConditionalAlgorithmSetting const &	algorithm )

Definition at line 4 of file ConditionalAlgorithmSetting.cpp.

◆ OptionalRef()

template<class T>

storm::OptionalRef ( T & ) ->OptionalRef< T >

deduction guides

◆ warnIfJsonExportNotAccurate()

template<typename ValueType>

void storm::warnIfJsonExportNotAccurate ( storm::json< ValueType > const & j )

Definition at line 43 of file JsonAdapter.cpp.

Variable Documentation

◆ IsIntervalType

template<typename ValueType>

bool storm::IsIntervalType = detail::IntervalMetaProgrammingHelper<ValueType>::isInterval

constexpr

Helper to check if a type is an interval.

Definition at line 40 of file IntervalForward.h.

◆ NullRef

NullRefType storm::NullRef {0}

inlineconstexpr

Definition at line 31 of file OptionalRef.h.

Namespaces

Classes

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

◆ BoundType

◆ CompareRelation

◆ ExtendedRationalFunction

◆ ExtendedRationalNumber

◆ Interval

◆ IntervalBaseType

◆ json

◆ OptimizationDirection

◆ Polynomial

◆ RationalFunction

◆ RationalFunctionVariable

◆ RationalInterval

◆ RawPolynomial

◆ RawPolynomialCache

◆ RawUnivariatePolynomial

◆ UncertaintyResolutionMode

◆ UncertaintyResolutionModeSetting

Enumeration Type Documentation

◆ ConditionalAlgorithmSetting

◆ SteadyStateDistributionAlgorithm

Function Documentation

◆ clearRFVariablePool()

◆ conditionalAlgorithmSettingFromString()

◆ createRFVariable()

◆ DdEnvironment::get< storm::dd::DdType::CUDD >()

◆ DdEnvironment::get< storm::dd::DdType::Sylvan >()

◆ dumpJson() [1/3]

◆ dumpJson() [2/3]

◆ dumpJson() [3/3]

◆ findRFVariable()

◆ isJsonNumberExportAccurate()

◆ json_for_each_number_float()

◆ operator<<()

◆ OptionalRef()

◆ warnIfJsonExportNotAccurate()

Variable Documentation

◆ IsIntervalType

◆ NullRef