|
Storm 1.14.0.1
A Modern Probabilistic Model Checker
|
Namespaces | |
| namespace | pfinternal |
| namespace | resources |
| namespace | solver |
| namespace | parameterlifting |
| namespace | parametric |
| namespace | cstring |
| namespace | permutation |
| namespace | builder |
| namespace | combinatorics |
| namespace | detail |
| namespace | dd |
| namespace | graph |
| namespace | kwek_mehlhorn |
| namespace | numerical |
| namespace | vector |
| namespace | ksp |
| namespace | string |
Classes | |
| class | AutomaticSettings |
| class | ModelInstantiator |
| This class allows efficient instantiation of the given parametric model. More... | |
| class | ConstantsComparator |
| class | Extremum |
| Stores and manages an extremal (maximal or minimal) value. More... | |
| class | FilteredRewardModel |
| class | ProgressMeasurement |
| A class that provides convenience operations to display run times. More... | |
| class | RandomProbabilityGenerator |
| class | RandomProbabilityGenerator< double > |
| class | RandomProbabilityGenerator< storm::RationalNumber > |
| class | BernoulliDistributionGenerator |
| class | ExponentialDistributionGenerator |
| 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 T> | |
| T | byteSwap (T const t) |
| Swaps the byte representation of the given value, (i.e., swaps endianness) Taken from https://en.cppreference.com/w/cpp/numeric/byteswap. | |
| template<typename T, bool ReverseBytes = true> | |
| T | reverseBits (T const t) |
| Swaps the bits in the bit representation of the given value. | |
| 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> | |
| uint64_t | bitsize (ValueType const &number) |
| Returns the minimum number of bits to represent the given 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 ÷nd, 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 | isConstant (storm::RationalInterval 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<> | |
| storm::RationalInterval | convertNumber (double const &number) |
| template<> | |
| storm::RationalInterval | convertNumber (uint64_t const &number) |
| template<> | |
| double | convertNumber (storm::Interval const &number) |
| template<> | |
| double | convertNumber (storm::RationalInterval const &number) |
| template<> | |
| storm::Interval | convertNumber (storm::RationalInterval const &number) |
| template<> | |
| storm::RationalInterval | 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<> | |
| bool | isApproxEqual (storm::RationalInterval const &a, storm::RationalInterval const &b, storm::RationalInterval const &precision, bool relative) |
| template<> | |
| storm::RationalInterval | abs (storm::RationalInterval const &interval) |
| 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 uint64_t | bitsize (storm::storage::sparse::state_type const &number) |
| template int64_t | convertNumber (int64_t const &) |
| 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 bool | isOne (RationalInterval const &value) |
| template bool | isZero (RationalInterval const &value) |
| template bool | isInfinity (RationalInterval const &value) |
| template bool | isAlmostZero (RationalInterval const &value) |
| template bool | isNonNegative (RationalInterval const &value) |
| template bool | isPositive (RationalInterval const &value) |
| template bool | isBetween (RationalInterval const &, RationalInterval const &, RationalInterval const &value, bool) |
| template std::string | to_string (storm::RationalInterval 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 | setStatisticsLogLevel (l3pp::LogLevel level) |
| Set the log level for the statistics channel, independently of the global log level. | |
| void | setProgressLogLevel (l3pp::LogLevel level) |
| Set the log level for the progress channel, independently of the global log level. | |
| void | initializeFileLogging (std::string const &logfileName) |
| Sets up the logging to file. | |
| storm::RationalNumber | findRational (storm::RationalNumber const &lowerBound, bool lowerInclusive, storm::RationalNumber const &upperBound, bool upperInclusive) |
| Finds the "simplest" rational number in the given interval, where "simplest" means having the smallest denominator. | |
| std::ostream & | operator<< (std::ostream &out, Stopwatch const &stopwatch) |
| uint64_t | getNumberOfThreads () |
Variables | |
| constexpr const char * | STATISTICS_LOG_CHANNEL = "storm.statistics" |
| constexpr const char * | PROGRESS_LOG_CHANNEL = "storm.progress" |
| using storm::utility::ElementGreater = typename detail::ElementGreater<ValueType>::type |
Definition at line 71 of file constants.h.
| using storm::utility::ElementLess = typename detail::ElementLess<ValueType>::type |
Definition at line 68 of file constants.h.
| using storm::utility::Maximum = Extremum<storm::OptimizationDirection::Maximize, ValueType> |
Definition at line 127 of file Extremum.h.
| using storm::utility::Minimum = Extremum<storm::OptimizationDirection::Minimize, ValueType> |
Definition at line 129 of file Extremum.h.
|
strong |
| template double storm::utility::abs | ( | double const & | number | ) |
| storm::Interval storm::utility::abs | ( | storm::Interval const & | interval | ) |
Definition at line 1145 of file constants.cpp.
| storm::RationalInterval storm::utility::abs | ( | storm::RationalInterval const & | interval | ) |
Definition at line 1164 of file constants.cpp.
| ValueType storm::utility::abs | ( | ValueType const & | number | ) |
Definition at line 271 of file constants.cpp.
| std::pair< ValueType, ValueType > storm::utility::asFraction | ( | ValueType const & | number | ) |
| template uint64_t storm::utility::bitsize | ( | storm::storage::sparse::state_type const & | number | ) |
| uint64_t storm::utility::bitsize | ( | ValueType const & | number | ) |
Returns the minimum number of bits to represent the given number.
Ignores sign, i.e. number and -number have the same size.
Definition at line 324 of file constants.cpp.
|
inline |
Swaps the byte representation of the given value, (i.e., swaps endianness) Taken from https://en.cppreference.com/w/cpp/numeric/byteswap.
Definition at line 16 of file bitoperations.h.
| 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 258 of file Engine.cpp.
| 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 99 of file Engine.cpp.
| template bool storm::utility::canHandle< double > | ( | storm::utility::Engine const & | , |
| std::vector< storm::jani::Property > const & | , | ||
| storm::storage::SymbolicModelDescription const & | ) |
| template bool storm::utility::canHandle< storm::RationalFunction > | ( | storm::utility::Engine const & | , |
| std::vector< storm::jani::Property > const & | , | ||
| storm::storage::SymbolicModelDescription const & | ) |
| 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 196 of file Engine.cpp.
| template bool storm::utility::canHandle< storm::RationalNumber > | ( | storm::utility::Engine const & | , |
| std::vector< storm::jani::Property > const & | , | ||
| storm::storage::SymbolicModelDescription const & | ) |
| template double storm::utility::ceil | ( | double const & | number | ) |
| ValueType storm::utility::ceil | ( | ValueType const & | number | ) |
Definition at line 281 of file constants.cpp.
| void storm::utility::cleanUp | ( | ) |
Performs some necessary clean-up.
Definition at line 37 of file initialize.cpp.
| storm::RationalInterval storm::utility::convertNumber | ( | double const & | number | ) |
Definition at line 1063 of file constants.cpp.
| storm::Interval storm::utility::convertNumber | ( | double const & | number | ) |
Definition at line 1053 of file constants.cpp.
| RationalFunction storm::utility::convertNumber | ( | double const & | number | ) |
Definition at line 874 of file constants.cpp.
| double storm::utility::convertNumber | ( | double const & | number | ) |
Definition at line 163 of file constants.cpp.
| int_fast64_t storm::utility::convertNumber | ( | double const & | number | ) |
Definition at line 153 of file constants.cpp.
| uint_fast64_t storm::utility::convertNumber | ( | double const & | number | ) |
Definition at line 148 of file constants.cpp.
| template int64_t storm::utility::convertNumber | ( | int64_t const & | ) |
| RationalFunction storm::utility::convertNumber | ( | int_fast64_t const & | number | ) |
Definition at line 879 of file constants.cpp.
| template double storm::utility::convertNumber | ( | long const & | ) |
| storm::storage::sparse::state_type storm::utility::convertNumber | ( | long long const & | number | ) |
Definition at line 173 of file constants.cpp.
| double storm::utility::convertNumber | ( | long long const & | number | ) |
Definition at line 168 of file constants.cpp.
| double storm::utility::convertNumber | ( | RationalFunction const & | func | ) |
Definition at line 920 of file constants.cpp.
| carl::sint storm::utility::convertNumber | ( | RationalFunction const & | func | ) |
Definition at line 915 of file constants.cpp.
| carl::uint storm::utility::convertNumber | ( | RationalFunction const & | func | ) |
Definition at line 910 of file constants.cpp.
| RationalFunction storm::utility::convertNumber | ( | RationalFunction const & | number | ) |
Definition at line 925 of file constants.cpp.
| TargetType storm::utility::convertNumber | ( | SourceType const & | number | ) |
Definition at line 143 of file constants.cpp.
| RationalFunction storm::utility::convertNumber | ( | std::string const & | number | ) |
Definition at line 930 of file constants.cpp.
| double storm::utility::convertNumber | ( | std::string const & | value | ) |
Definition at line 1048 of file constants.cpp.
| storm::RationalInterval storm::utility::convertNumber | ( | storm::Interval const & | number | ) |
Definition at line 1139 of file constants.cpp.
| template Interval storm::utility::convertNumber | ( | storm::Interval const & | number | ) |
Definition at line 1121 of file constants.cpp.
| storm::Interval storm::utility::convertNumber | ( | storm::RationalInterval const & | number | ) |
Definition at line 1133 of file constants.cpp.
| template RationalInterval storm::utility::convertNumber | ( | storm::RationalInterval const & | number | ) |
Definition at line 1127 of file constants.cpp.
| RationalFunction storm::utility::convertNumber | ( | storm::storage::sparse::state_type const & | number | ) |
Definition at line 935 of file constants.cpp.
| storm::RationalInterval storm::utility::convertNumber | ( | uint64_t const & | number | ) |
Definition at line 1068 of file constants.cpp.
| storm::Interval storm::utility::convertNumber | ( | uint64_t const & | number | ) |
Definition at line 1058 of file constants.cpp.
| double storm::utility::convertNumber | ( | uint_fast64_t const & | number | ) |
Definition at line 158 of file constants.cpp.
| template double storm::utility::cos | ( | double const & | number | ) |
| ValueType storm::utility::cos | ( | ValueType const & | number | ) |
Definition at line 302 of file constants.cpp.
| FilteredRewardModel< typename ModelType::RewardModelType > storm::utility::createFilteredRewardModel | ( | ModelType const & | model, |
| CheckTaskType const & | checkTask ) |
Definition at line 99 of file FilteredRewardModel.h.
| FilteredRewardModel< RewardModelType > storm::utility::createFilteredRewardModel | ( | RewardModelType const & | baseRewardModel, |
| bool | isDiscreteTimeModel, | ||
| FormulaType const & | formula ) |
Definition at line 90 of file FilteredRewardModel.h.
| FilteredRewardModel< RewardModelType > storm::utility::createFilteredRewardModel | ( | RewardModelType const & | baseRewardModel, |
| storm::logic::RewardAccumulation const & | acc, | ||
| bool | isDiscreteTimeModel ) |
Definition at line 78 of file FilteredRewardModel.h.
| NumberTraits< RationalType >::IntegerType storm::utility::denominator | ( | RationalType const & | number | ) |
| 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 349 of file constants.cpp.
| 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 64 of file Engine.cpp.
| storm::RationalNumber storm::utility::findRational | ( | storm::RationalNumber const & | lowerBound, |
| bool | lowerInclusive, | ||
| storm::RationalNumber const & | upperBound, | ||
| bool | upperInclusive ) |
Finds the "simplest" rational number in the given interval, where "simplest" means having the smallest denominator.
| lowerBound | The lower bound of the interval |
| lowerInclusive | Whether the lower bound itself is included |
| upperBound | the upper bound of the interval |
| upperInclusive | Whether the upper bound itself is included |
Definition at line 10 of file RationalApproximation.cpp.
| template double storm::utility::floor | ( | double const & | number | ) |
| ValueType storm::utility::floor | ( | ValueType const & | number | ) |
Definition at line 276 of file constants.cpp.
| storm::builder::BuilderType storm::utility::getBuilderType | ( | Engine const & | engine | ) |
Returns the builder type used for the given engine.
Definition at line 78 of file Engine.cpp.
| std::vector< Engine > storm::utility::getEngines | ( | ) |
Returns a list of all available engines (excluding Unknown).
Definition at line 27 of file Engine.cpp.
| l3pp::LogLevel storm::utility::getLogLevel | ( | ) |
Gets the global log level.
Definition at line 55 of file initialize.cpp.
| uint64_t storm::utility::getNumberOfThreads | ( | ) |
Definition at line 55 of file threads.cpp.
| storm::RationalFunction storm::utility::infinity | ( | ) |
Definition at line 811 of file constants.cpp.
| ValueType storm::utility::infinity | ( | ) |
Definition at line 29 of file constants.cpp.
| void storm::utility::initializeFileLogging | ( | std::string const & | logfileName | ) |
Sets up the logging to file.
Definition at line 76 of file initialize.cpp.
| void storm::utility::initializeLogger | ( | ) |
Initializes the logging framework and sets up logging to console.
Definition at line 10 of file initialize.cpp.
| template bool storm::utility::isAlmostOne | ( | double const & | value | ) |
| bool storm::utility::isAlmostOne | ( | storm::RationalFunction const & | a | ) |
Definition at line 969 of file constants.cpp.
| bool storm::utility::isAlmostOne | ( | ValueType const & | a | ) |
Definition at line 101 of file constants.cpp.
| template bool storm::utility::isAlmostZero | ( | double const & | value | ) |
| template bool storm::utility::isAlmostZero | ( | Interval const & | value | ) |
| template bool storm::utility::isAlmostZero | ( | RationalInterval const & | value | ) |
| bool storm::utility::isAlmostZero | ( | storm::RationalFunction const & | a | ) |
Definition at line 964 of file constants.cpp.
| bool storm::utility::isAlmostZero | ( | ValueType const & | a | ) |
Definition at line 96 of file constants.cpp.
| template bool storm::utility::isApproxEqual | ( | double const & | a, |
| double const & | b, | ||
| double const & | precision, | ||
| bool | relative ) |
| template bool storm::utility::isApproxEqual | ( | int const & | a, |
| int const & | b, | ||
| int const & | precision, | ||
| bool | relative ) |
| bool storm::utility::isApproxEqual | ( | storm::Interval const & | a, |
| storm::Interval const & | b, | ||
| storm::Interval const & | precision, | ||
| bool | relative ) |
Definition at line 1150 of file constants.cpp.
| bool storm::utility::isApproxEqual | ( | storm::RationalFunction const & | a, |
| storm::RationalFunction const & | b, | ||
| storm::RationalFunction const & | precision, | ||
| bool | relative ) |
Definition at line 847 of file constants.cpp.
| bool storm::utility::isApproxEqual | ( | storm::RationalInterval const & | a, |
| storm::RationalInterval const & | b, | ||
| storm::RationalInterval const & | precision, | ||
| bool | relative ) |
Definition at line 1157 of file constants.cpp.
| 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 ) |
| bool storm::utility::isApproxEqual | ( | ValueType const & | a, |
| ValueType const & | b, | ||
| ValueType const & | precision, | ||
| bool | relative ) |
Definition at line 57 of file constants.cpp.
| template bool storm::utility::isBetween | ( | double const & | a, |
| double const & | b, | ||
| double const & | c, | ||
| bool | strict ) |
| template bool storm::utility::isBetween | ( | int const & | a, |
| int const & | b, | ||
| int const & | c, | ||
| bool | strict ) |
| template bool storm::utility::isBetween | ( | Interval const & | , |
| Interval const & | , | ||
| Interval const & | value, | ||
| bool | ) |
| template bool storm::utility::isBetween | ( | RationalInterval const & | , |
| RationalInterval const & | , | ||
| RationalInterval const & | value, | ||
| bool | ) |
| bool storm::utility::isBetween | ( | storm::RationalFunction const & | a, |
| storm::RationalFunction const & | b, | ||
| storm::RationalFunction const & | c, | ||
| bool | strict ) |
Definition at line 984 of file constants.cpp.
| 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 ) |
| template bool storm::utility::isBetween | ( | uint32_t const & | a, |
| uint32_t const & | b, | ||
| uint32_t const & | c, | ||
| bool | strict ) |
| 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).
| a | A constant value |
| b | Some value |
| c | A constant value |
| strict | Changes the type of the comparison |
Definition at line 85 of file constants.cpp.
| template bool storm::utility::isConstant | ( | double const & | value | ) |
| template bool storm::utility::isConstant | ( | int const & | value | ) |
| bool storm::utility::isConstant | ( | storm::Interval const & | a | ) |
Definition at line 853 of file constants.cpp.
| bool storm::utility::isConstant | ( | storm::Polynomial const & | a | ) |
Definition at line 842 of file constants.cpp.
| bool storm::utility::isConstant | ( | storm::RationalFunction const & | a | ) |
Definition at line 837 of file constants.cpp.
| bool storm::utility::isConstant | ( | storm::RationalInterval const & | a | ) |
Definition at line 858 of file constants.cpp.
| template bool storm::utility::isConstant | ( | storm::storage::sparse::state_type const & | value | ) |
| template bool storm::utility::isConstant | ( | uint32_t const & | value | ) |
| bool storm::utility::isConstant | ( | ValueType const & | ) |
Definition at line 106 of file constants.cpp.
| template bool storm::utility::isInfinity | ( | double const & | value | ) |
| template bool storm::utility::isInfinity | ( | int const & | value | ) |
| template bool storm::utility::isInfinity | ( | Interval const & | value | ) |
| template bool storm::utility::isInfinity | ( | RationalInterval const & | value | ) |
| bool storm::utility::isInfinity | ( | storm::RationalFunction const & | a | ) |
Definition at line 863 of file constants.cpp.
| template bool storm::utility::isInfinity | ( | storm::storage::sparse::state_type const & | value | ) |
| template bool storm::utility::isInfinity | ( | uint32_t const & | value | ) |
| bool storm::utility::isInfinity | ( | ValueType const & | a | ) |
Definition at line 111 of file constants.cpp.
| template bool storm::utility::isInteger | ( | double const & | number | ) |
| bool storm::utility::isInteger | ( | int const & | ) |
Definition at line 128 of file constants.cpp.
| bool storm::utility::isInteger | ( | storm::RationalFunction const & | func | ) |
Definition at line 869 of file constants.cpp.
| bool storm::utility::isInteger | ( | storm::storage::sparse::state_type const & | ) |
Definition at line 138 of file constants.cpp.
| bool storm::utility::isInteger | ( | uint32_t const & | ) |
Definition at line 133 of file constants.cpp.
| bool storm::utility::isInteger | ( | ValueType const & | number | ) |
Definition at line 121 of file constants.cpp.
| bool storm::utility::isNan | ( | double const & | value | ) |
Definition at line 52 of file constants.cpp.
| template bool storm::utility::isNan | ( | RationalFunction const & | ) |
| bool storm::utility::isNan | ( | ValueType const & | ) |
Definition at line 47 of file constants.cpp.
| template bool storm::utility::isNonNegative | ( | double const & | value | ) |
| template bool storm::utility::isNonNegative | ( | int const & | value | ) |
| template bool storm::utility::isNonNegative | ( | Interval const & | value | ) |
| template bool storm::utility::isNonNegative | ( | RationalInterval const & | value | ) |
| bool storm::utility::isNonNegative | ( | storm::RationalFunction const & | a | ) |
Definition at line 974 of file constants.cpp.
| template bool storm::utility::isNonNegative | ( | storm::storage::sparse::state_type const & | value | ) |
| template bool storm::utility::isNonNegative | ( | uint32_t const & | value | ) |
| bool storm::utility::isNonNegative | ( | ValueType const & | a | ) |
Definition at line 72 of file constants.cpp.
| template bool storm::utility::isOne | ( | double const & | value | ) |
| template bool storm::utility::isOne | ( | int const & | value | ) |
| template bool storm::utility::isOne | ( | Interval const & | value | ) |
| template bool storm::utility::isOne | ( | RationalInterval const & | value | ) |
| bool storm::utility::isOne | ( | storm::Polynomial const & | a | ) |
Definition at line 822 of file constants.cpp.
| bool storm::utility::isOne | ( | storm::RationalFunction const & | a | ) |
Definition at line 817 of file constants.cpp.
| template bool storm::utility::isOne | ( | storm::storage::sparse::state_type const & | value | ) |
| template bool storm::utility::isOne | ( | uint32_t const & | value | ) |
| bool storm::utility::isOne | ( | ValueType const & | a | ) |
Definition at line 37 of file constants.cpp.
| template bool storm::utility::isPositive | ( | double const & | value | ) |
| template bool storm::utility::isPositive | ( | int const & | value | ) |
| template bool storm::utility::isPositive | ( | Interval const & | value | ) |
| template bool storm::utility::isPositive | ( | RationalInterval const & | value | ) |
| bool storm::utility::isPositive | ( | storm::RationalFunction const & | a | ) |
Definition at line 979 of file constants.cpp.
| template bool storm::utility::isPositive | ( | storm::storage::sparse::state_type const & | value | ) |
| template bool storm::utility::isPositive | ( | uint32_t const & | value | ) |
| bool storm::utility::isPositive | ( | ValueType const & | a | ) |
Definition at line 67 of file constants.cpp.
| template bool storm::utility::isZero | ( | double const & | value | ) |
| template bool storm::utility::isZero | ( | int const & | value | ) |
| template bool storm::utility::isZero | ( | Interval const & | value | ) |
| template bool storm::utility::isZero | ( | RationalInterval const & | value | ) |
| bool storm::utility::isZero | ( | storm::Polynomial const & | a | ) |
Definition at line 832 of file constants.cpp.
| bool storm::utility::isZero | ( | storm::RationalFunction const & | a | ) |
Definition at line 827 of file constants.cpp.
| template bool storm::utility::isZero | ( | storm::storage::sparse::state_type const & | value | ) |
| template bool storm::utility::isZero | ( | uint32_t const & | value | ) |
| bool storm::utility::isZero | ( | ValueType const & | a | ) |
Definition at line 42 of file constants.cpp.
| template double storm::utility::log | ( | double const & | number | ) |
| ValueType storm::utility::log | ( | ValueType const & | number | ) |
Definition at line 292 of file constants.cpp.
| template double storm::utility::log10 | ( | double const & | number | ) |
| ValueType storm::utility::log10 | ( | ValueType const & | number | ) |
Definition at line 297 of file constants.cpp.
| template double storm::utility::max | ( | double const & | first, |
| double const & | second ) |
| ValueType storm::utility::max | ( | ValueType const & | first, |
| ValueType const & | second ) |
Definition at line 256 of file constants.cpp.
| ValueType storm::utility::maximum | ( | std::map< K, ValueType > const & | values | ) |
Definition at line 246 of file constants.cpp.
| template double storm::utility::maximum | ( | std::map< uint64_t, double > const & | ) |
| storm::RationalFunction storm::utility::maximum | ( | std::map< uint64_t, storm::RationalFunction > const & | ) |
Definition at line 1017 of file constants.cpp.
| template double storm::utility::maximum | ( | std::vector< double > const & | ) |
| storm::RationalFunction storm::utility::maximum | ( | std::vector< storm::RationalFunction > const & | ) |
Definition at line 1002 of file constants.cpp.
| ValueType storm::utility::maximum | ( | std::vector< ValueType > const & | values | ) |
Definition at line 213 of file constants.cpp.
| template double storm::utility::min | ( | double const & | first, |
| double const & | second ) |
| ValueType storm::utility::min | ( | ValueType const & | first, |
| ValueType const & | second ) |
Definition at line 261 of file constants.cpp.
| ValueType storm::utility::minimum | ( | std::map< K, ValueType > const & | values | ) |
Definition at line 241 of file constants.cpp.
| template double storm::utility::minimum | ( | std::map< uint64_t, double > const & | ) |
| storm::RationalFunction storm::utility::minimum | ( | std::map< uint64_t, storm::RationalFunction > const & | ) |
Definition at line 1012 of file constants.cpp.
| template double storm::utility::minimum | ( | std::vector< double > const & | ) |
| storm::RationalFunction storm::utility::minimum | ( | std::vector< storm::RationalFunction > const & | ) |
Definition at line 997 of file constants.cpp.
| ValueType storm::utility::minimum | ( | std::vector< ValueType > const & | values | ) |
Definition at line 201 of file constants.cpp.
| std::pair< ValueType, ValueType > storm::utility::minmax | ( | std::map< K, ValueType > const & | values | ) |
Definition at line 225 of file constants.cpp.
| template std::pair< double, double > storm::utility::minmax | ( | std::map< uint64_t, double > const & | ) |
| std::pair< storm::RationalFunction, storm::RationalFunction > storm::utility::minmax | ( | std::map< uint64_t, storm::RationalFunction > const & | ) |
Definition at line 1007 of file constants.cpp.
| template std::pair< double, double > storm::utility::minmax | ( | std::vector< double > const & | ) |
| std::pair< storm::RationalFunction, storm::RationalFunction > storm::utility::minmax | ( | std::vector< storm::RationalFunction > const & | ) |
Definition at line 992 of file constants.cpp.
| std::pair< ValueType, ValueType > storm::utility::minmax | ( | std::vector< ValueType > const & | values | ) |
Definition at line 185 of file constants.cpp.
| template double storm::utility::mod | ( | double const & | first, |
| double const & | second ) |
| IntegerType storm::utility::mod | ( | IntegerType const & | first, |
| IntegerType const & | second ) |
Definition at line 344 of file constants.cpp.
| uint64_t storm::utility::numDigits | ( | ValueType const & | number | ) |
Definition at line 312 of file constants.cpp.
| NumberTraits< RationalType >::IntegerType storm::utility::numerator | ( | RationalType const & | number | ) |
| template double storm::utility::one | ( | ) |
| ValueType storm::utility::one | ( | ) |
Definition at line 19 of file constants.cpp.
| 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 59 of file Engine.cpp.
| std::ostream & storm::utility::operator<< | ( | std::ostream & | out, |
| Stopwatch const & | stopwatch ) |
Definition at line 68 of file Stopwatch.cpp.
| template double storm::utility::pow | ( | double const & | value, |
| int_fast64_t | exponent ) |
| RationalFunction storm::utility::pow | ( | RationalFunction const & | value, |
| int_fast64_t | exponent ) |
Definition at line 1022 of file constants.cpp.
| ValueType storm::utility::pow | ( | ValueType const & | value, |
| int_fast64_t | exponent ) |
Definition at line 251 of file constants.cpp.
|
inline |
Swaps the bits in the bit representation of the given value.
| ReverseBytes | If true, the byte representation is also swapped (i.e., endianness is swapped) |
Definition at line 29 of file bitoperations.h.
| template double storm::utility::round | ( | double const & | number | ) |
| ValueType storm::utility::round | ( | ValueType const & | number | ) |
Definition at line 286 of file constants.cpp.
| void storm::utility::setLogLevel | ( | l3pp::LogLevel | level | ) |
Set the global log level.
Definition at line 59 of file initialize.cpp.
| void storm::utility::setOutputDigits | ( | int | digits | ) |
Set number of digits for printing output.
| digits | Number of digits to print. |
Definition at line 28 of file initialize.cpp.
| 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.
| precision | General precision. |
Definition at line 41 of file initialize.cpp.
| void storm::utility::setProgressLogLevel | ( | l3pp::LogLevel | level | ) |
Set the log level for the progress channel, independently of the global log level.
Definition at line 72 of file initialize.cpp.
| void storm::utility::setStatisticsLogLevel | ( | l3pp::LogLevel | level | ) |
Set the log level for the statistics channel, independently of the global log level.
Definition at line 68 of file initialize.cpp.
| void storm::utility::setUp | ( | ) |
Performs some necessary initializations.
Definition at line 32 of file initialize.cpp.
| template double storm::utility::simplify | ( | double | value | ) |
| RationalFunction && storm::utility::simplify | ( | RationalFunction && | value | ) |
Definition at line 958 of file constants.cpp.
| RationalFunction && storm::utility::simplify | ( | RationalFunction && | value | ) |
Definition at line 958 of file constants.cpp.
| RationalFunction & storm::utility::simplify | ( | RationalFunction & | value | ) |
Definition at line 952 of file constants.cpp.
| RationalFunction & storm::utility::simplify | ( | RationalFunction & | value | ) |
Definition at line 952 of file constants.cpp.
| RationalFunction storm::utility::simplify | ( | RationalFunction | value | ) |
Definition at line 946 of file constants.cpp.
| storm::storage::MatrixEntry< IndexType, ValueType > && storm::utility::simplify | ( | storm::storage::MatrixEntry< IndexType, ValueType > && | matrixEntry | ) |
| storm::storage::MatrixEntry< IndexType, ValueType > & storm::utility::simplify | ( | storm::storage::MatrixEntry< IndexType, ValueType > & | matrixEntry | ) |
| ValueType storm::utility::simplify | ( | ValueType | value | ) |
Definition at line 178 of file constants.cpp.
| template double storm::utility::sin | ( | double const & | number | ) |
| ValueType storm::utility::sin | ( | ValueType const & | number | ) |
Definition at line 307 of file constants.cpp.
| template double storm::utility::sqrt | ( | double const & | number | ) |
| ValueType storm::utility::sqrt | ( | ValueType const & | number | ) |
Definition at line 266 of file constants.cpp.
| template std::string storm::utility::to_string | ( | double const & | value | ) |
| std::string storm::utility::to_string | ( | RationalFunction const & | f | ) |
Definition at line 1031 of file constants.cpp.
| template std::string storm::utility::to_string | ( | storm::Interval const & | value | ) |
| template std::string storm::utility::to_string | ( | storm::RationalInterval const & | value | ) |
| std::string storm::utility::to_string | ( | ValueType const & | value | ) |
Definition at line 354 of file constants.cpp.
| std::string storm::utility::toString | ( | Engine const & | engine | ) |
Returns a string representation of the given engine.
Definition at line 35 of file Engine.cpp.
| template NumberTraits< double >::IntegerType storm::utility::trunc | ( | double const & | number | ) |
| NumberTraits< ValueType >::IntegerType storm::utility::trunc | ( | ValueType const & | number | ) |
Definition at line 339 of file constants.cpp.
| template double storm::utility::zero | ( | ) |
| ValueType storm::utility::zero | ( | ) |
Definition at line 24 of file constants.cpp.
|
constexpr |