Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm Namespace Reference

LabParser.cpp. More...

Namespaces

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

Classes

class  EigenSolverEnvironment
 
class  Environment
 
class  GameSolverEnvironment
 
class  GmmxxSolverEnvironment
 
struct  InternalEnvironment
 
class  LongRunAverageSolverEnvironment
 
class  MinMaxLpSolverEnvironment
 
class  MinMaxSolverEnvironment
 
class  ModelCheckerEnvironment
 
class  MultiObjectiveModelCheckerEnvironment
 
class  MultiplierEnvironment
 
class  NativeSolverEnvironment
 
struct  NullRefType
 Auxiliary struct used to identify OptionalRefs that do not contain a reference. More...
 
struct  NumberTraits
 
struct  NumberTraits< double >
 
struct  NumberTraits< storm::RationalFunction >
 
class  OptionalRef
 Helper class that optionally holds a reference to an object of type T. More...
 
class  OviSolverEnvironment
 
class  SolverEnvironment
 
struct  StormVersion
 
class  SubEnvironment
 
class  TimeBoundedSolverEnvironment
 
class  TopologicalSolverEnvironment
 

Typedefs

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::FactorizedPolynomial< RawPolynomialPolynomial
 
typedef carl::RationalFunction< Polynomial, true > RationalFunction
 
typedef carl::Interval< double > Interval
 
using OptimizationDirection = solver::OptimizationDirection
 

Enumerations

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)
 
template<class T >
 OptionalRef (T &) -> OptionalRef< T >
 deduction guides
 

Variables

constexpr NullRefType NullRef {0}
 

Detailed Description

LabParser.cpp.

Created on: 21.11.2012 Author: Gereon Kremer

Typedef Documentation

◆ CompareRelation

typedef carl::Relation storm::CompareRelation

Definition at line 45 of file RationalFunctionAdapter_Private.h.

◆ Interval

Definition at line 33 of file RationalNumberForward.h.

◆ json

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

Definition at line 10 of file JsonForward.h.

◆ OptimizationDirection

◆ Polynomial

◆ RationalFunction

◆ RationalFunctionVariable

typedef carl::Variable storm::RationalFunctionVariable

Definition at line 35 of file RationalFunctionForward.h.

◆ RawPolynomial

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

Definition at line 47 of file RationalFunctionForward.h.

◆ RawPolynomialCache

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

Definition at line 44 of file RationalFunctionAdapter_Private.h.

Enumeration Type Documentation

◆ SteadyStateDistributionAlgorithm

Enumerator
Automatic 
EquationSystem 
ExpectedVisitingTimes 
Classic 

Definition at line 4 of file SteadyStateDistributionAlgorithm.h.

Function Documentation

◆ 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
jThe JSON object
compactindicates 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
jjson 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.

◆ 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

◆ NullRef

constexpr NullRefType storm::NullRef {0}
inlineconstexpr

Definition at line 31 of file OptionalRef.h.