Namespaces
namespace	utility
namespace	jani
namespace	cli
namespace	conv
namespace	api
namespace	prism
namespace	converter
namespace	settings
namespace	counterexamples
namespace	dft
namespace	storage
namespace	gbar
namespace	expressions
namespace	dd
namespace	models
namespace	modelchecker
namespace	builder
namespace	parser
	Contains all file parsers and helper classes.
namespace	gspn
namespace	pars
namespace	derivative
namespace	analysis
namespace	transformer
namespace	logic
namespace	ps
namespace	pomdp
namespace	generator
namespace	adapters
namespace	detail
namespace	automata
namespace	exceptions
namespace	io
namespace	solver
namespace	simulator
namespace	umb
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
struct	InternalEnvironment
class	Environment
class	ConditionalModelCheckerEnvironment
class	ModelCheckerEnvironment
class	MultiObjectiveModelCheckerEnvironment
class	EigenSolverEnvironment
class	GameSolverEnvironment
class	GmmxxSolverEnvironment
class	LongRunAverageSolverEnvironment
class	MinMaxLpSolverEnvironment
class	MinMaxSolverEnvironment
class	MultiplierEnvironment
class	NativeSolverEnvironment
class	OviSolverEnvironment
class	SolverEnvironment
class	TimeBoundedSolverEnvironment
class	TopologicalSolverEnvironment
class	SubEnvironment
struct	NumberTraits
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
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

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

◆ CompareRelation

typedef carl::Relation storm::CompareRelation

Definition at line 44 of file RationalFunctionAdapter.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 10 of file JsonForward.h.

◆ OptimizationDirection

using storm::OptimizationDirection = solver::OptimizationDirection

Definition at line 30 of file OptimizationDirection.h.

◆ Polynomial

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

Definition at line 40 of file RationalFunctionForward.h.

◆ RationalFunction

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

Definition at line 41 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 38 of file RationalFunctionForward.h.

◆ RawPolynomialCache

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

Definition at line 43 of file RationalFunctionAdapter.h.

◆ RawUnivariatePolynomial

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

Definition at line 39 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

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

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

◆ 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

◆ CompareRelation

◆ Interval

◆ IntervalBaseType

◆ json

◆ OptimizationDirection

◆ Polynomial

◆ RationalFunction

◆ RationalFunctionVariable

◆ RationalInterval

◆ RawPolynomial

◆ RawPolynomialCache

◆ RawUnivariatePolynomial

◆ UncertaintyResolutionMode

◆ UncertaintyResolutionModeSetting

Enumeration Type Documentation

◆ ConditionalAlgorithmSetting

◆ SteadyStateDistributionAlgorithm

Function Documentation

◆ conditionalAlgorithmSettingFromString()

◆ createRFVariable()

◆ dumpJson() [1/3]

◆ dumpJson() [2/3]

◆ dumpJson() [3/3]

◆ isJsonNumberExportAccurate()

◆ json_for_each_number_float()

◆ operator<<()

◆ OptionalRef()

◆ warnIfJsonExportNotAccurate()

Variable Documentation

◆ IsIntervalType

◆ NullRef