| ►Cstorm::solver::AbstractEquationSolver< ValueType > | |
| Cstorm::solver::MinMaxLinearEquationSolver< ValueType, ValueType > | |
| ►Cstorm::solver::GameSolver< ValueType > | A class representing the interface that all game solvers shall implement |
| Cstorm::solver::StandardGameSolver< ValueType > | |
| ►Cstorm::solver::LinearEquationSolver< ValueType > | An interface that represents an abstract linear equation solver |
| Cstorm::solver::AcyclicLinearEquationSolver< ValueType > | This solver can be used on equation systems that are known to be acyclic |
| Cstorm::solver::EigenLinearEquationSolver< ValueType > | A class that uses the Eigen library to implement the LinearEquationSolver interface |
| Cstorm::solver::EliminationLinearEquationSolver< ValueType > | A class that uses gaussian elimination to implement the LinearEquationSolver interface |
| Cstorm::solver::GmmxxLinearEquationSolver< ValueType > | A class that uses the gmm++ library to implement the LinearEquationSolver interface |
| Cstorm::solver::NativeLinearEquationSolver< ValueType > | A class that uses storm's native matrix operations to implement the LinearEquationSolver interface |
| Cstorm::solver::TopologicalLinearEquationSolver< ValueType > | |
| ►Cstorm::solver::MinMaxLinearEquationSolver< ValueType, SolutionType > | A class representing the interface that all min-max linear equation solvers shall implement |
| Cstorm::solver::StandardMinMaxLinearEquationSolver< ValueType, ValueType > | |
| ►Cstorm::solver::StandardMinMaxLinearEquationSolver< ValueType, SolutionType > | |
| Cstorm::solver::AcyclicMinMaxLinearEquationSolver< ValueType > | This solver can be used on equation systems that are known to be acyclic |
| Cstorm::solver::IterativeMinMaxLinearEquationSolver< ValueType, SolutionType > | |
| Cstorm::solver::LpMinMaxLinearEquationSolver< ValueType > | Solves a MinMaxLinearEquationSystem using a linear programming solver |
| Cstorm::solver::TopologicalMinMaxLinearEquationSolver< ValueType, SolutionType > | |
| Cstorm::gbar::abstraction::AbstractionInformation< DdType > | |
| Cstorm::gbar::abstraction::AbstractionInformationOptions | |
| Cstorm::gbar::api::AbstractionRefinementOptions | |
| ►Cstorm::modelchecker::AbstractModelChecker< ModelType > | |
| ►Cstorm::modelchecker::SparsePropositionalModelChecker< SparseCtmcModelType > | |
| Cstorm::modelchecker::SparseCtmcCslModelChecker< SparseCtmcModelType > | |
| ►Cstorm::modelchecker::SparsePropositionalModelChecker< SparseDtmcModelType > | |
| Cstorm::modelchecker::SparseDtmcEliminationModelChecker< SparseDtmcModelType > | |
| Cstorm::modelchecker::SparseDtmcPrctlModelChecker< SparseDtmcModelType > | |
| ►Cstorm::modelchecker::SparsePropositionalModelChecker< SparseMarkovAutomatonModelType > | |
| Cstorm::modelchecker::SparseMarkovAutomatonCslModelChecker< SparseMarkovAutomatonModelType > | |
| ►Cstorm::modelchecker::SparsePropositionalModelChecker< SparseMdpModelType > | |
| Cstorm::modelchecker::SparseMdpPrctlModelChecker< SparseMdpModelType > | |
| ►Cstorm::modelchecker::SparsePropositionalModelChecker< SparseSmgModelType > | |
| Cstorm::modelchecker::SparseSmgRpatlModelChecker< SparseSmgModelType > | |
| ►Cstorm::gbar::modelchecker::AbstractAbstractionRefinementModelChecker< ModelType > | |
| Cstorm::gbar::modelchecker::BisimulationAbstractionRefinementModelChecker< ModelType > | |
| Cstorm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType > | |
| Cstorm::modelchecker::SparseExplorationModelChecker< ModelType, StateType > | |
| ►Cstorm::modelchecker::SymbolicPropositionalModelChecker< ModelType > | |
| Cstorm::modelchecker::HybridCtmcCslModelChecker< ModelType > | |
| Cstorm::modelchecker::HybridDtmcPrctlModelChecker< ModelType > | |
| Cstorm::modelchecker::HybridMarkovAutomatonCslModelChecker< ModelType > | |
| Cstorm::modelchecker::HybridMdpPrctlModelChecker< ModelType > | |
| Cstorm::modelchecker::SymbolicDtmcPrctlModelChecker< ModelType > | |
| Cstorm::modelchecker::SymbolicMdpPrctlModelChecker< ModelType > | |
| Cstorm::modelchecker::AbstractModelChecker< SparseCtmcModelType > | |
| Cstorm::modelchecker::AbstractModelChecker< SparseDtmcModelType > | |
| Cstorm::modelchecker::AbstractModelChecker< SparseMarkovAutomatonModelType > | |
| Cstorm::modelchecker::AbstractModelChecker< SparseMdpModelType > | |
| ►Cstorm::modelchecker::AbstractModelChecker< SparseModelType > | |
| Cstorm::modelchecker::SparsePropositionalModelChecker< SparseModelType > | |
| Cstorm::modelchecker::AbstractModelChecker< SparseSmgModelType > | |
| Cstorm::transformer::ParameterLifter< ParametricType, ConstantType >::AbstractValuation | |
| Cstorm::automata::AcceptanceCondition | |
| Cstorm::jani::Action | |
| ►Cstorm::jani::JaniLocalEliminator::Action | |
| Cstorm::jani::elimination_actions::AutomaticAction | |
| Cstorm::jani::elimination_actions::EliminateAction | |
| Cstorm::jani::elimination_actions::EliminateAutomaticallyAction | |
| Cstorm::jani::elimination_actions::FinishAction | |
| Cstorm::jani::elimination_actions::RebuildWithoutUnreachableAction | |
| Cstorm::jani::elimination_actions::UnfoldAction | |
| Cstorm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionDd | |
| Cstorm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionIdentification | |
| Cstorm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionIdentificationHash | |
| Cstorm::transformer::detail::ActionIdentifier | |
| Cstorm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionInstantiation | |
| Cstorm::builder::CombinedEdgesSystemComposer< Type, ValueType >::ActionInstantiationHash | |
| ►Cstorm::generator::ActionMask< ValueType, StateType > | Action masks are arguments you can give to the state generator that limit which states are generated |
| Cstorm::generator::StateValuationFunctionMask< ValueType, StateType > | A particular instance of the action mask that uses a callback function to evaluate whether an action should be expanded |
| Cstorm::generator::ActionMask< ValueType, uint32_t > | |
| Cstorm::generator::ActiveCommandData | |
| Cstorm::dd::AddIterator< LibraryType, ValueType > | |
| Cstorm::dd::AddIterator< DdType::CUDD, ValueType > | |
| Cstorm::dd::AddIterator< DdType::Sylvan, ValueType > | |
| Cstorm::transformer::AddUncertainty< ValueType > | This class is a convenience transformer to add uncertainty |
| Cstorm::transformer::ApplyFiniteSchedulerToPomdp< ValueType > | |
| Cstorm::automata::APSet | |
| ►Cstorm::settings::ArgumentBase | This class serves as the (untemplated) base class of argument classes |
| Cstorm::settings::Argument< T > | This class subclasses the argument base to actually implement the pure virtual functions |
| Cstorm::settings::ArgumentBuilder | This class serves as an API for creating arguments |
| ►Cstorm::settings::ArgumentValidator< ValueType > | |
| Cstorm::settings::RangeArgumentValidator< ValueType > | |
| ►Cstorm::settings::ArgumentValidator< std::string > | |
| Cstorm::settings::FileValidator | |
| Cstorm::settings::MultipleChoiceValidator | |
| Cstorm::settings::ArgumentValidatorFactory | |
| Cstorm::jani::ArrayEliminator | |
| Cstorm::jani::ArrayEliminatorData | |
| Cstorm::generator::ArrayVariableReplacementInformation | |
| Cstorm::jani::Assignment | |
| Cstorm::jani::AssignmentLevelToLevelComparator | |
| Cstorm::jani::AssignmentPartialOrderByLevelAndLValue | This functor enables ordering the assignments first by the assignment level and then by lValue |
| Cstorm::analysis::AssumptionChecker< ValueType, ConstantType > | |
| Cstorm::analysis::AssumptionMaker< ValueType, ConstantType > | |
| Cstorm::parser::AtomicPropositionLabelingParser | This class can be used to parse a labeling file |
| Cstorm::utility::AutomaticSettings | |
| Cstorm::jani::Automaton | |
| Cstorm::gbar::abstraction::jani::AutomatonAbstractor< DdType, ValueType > | |
| Cstorm::builder::CombinedEdgesSystemComposer< Type, ValueType >::AutomatonDd | |
| Cstorm::parser::AutoParser< ValueType, RewardValueType > | This class automatically chooses the correct parser for the given files and returns the corresponding model |
| Cstorm::modelchecker::helper::BaierUpperRewardBoundsComputer< ValueType > | |
| ►Cstorm::expressions::BaseType | |
| Cstorm::expressions::ArrayType | |
| Cstorm::expressions::BitVectorType | |
| Cstorm::expressions::BooleanType | |
| Cstorm::expressions::ErrorType | |
| Cstorm::expressions::IntegerType | |
| Cstorm::expressions::RationalType | |
| Cstorm::expressions::TranscendentalNumberType | |
| Cstorm::dft::storage::BEColourClass< ValueType > | |
| Cstorm::storage::BeliefManager< PomdpType, BeliefValueType, StateType >::BeliefClipping | |
| Cstorm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< PomdpModelType, BeliefValueType, BeliefMDPType > | Model checker for checking reachability queries on POMDPs using approximations based on exploration of the belief MDP |
| Cstorm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions< ValueType > | |
| Cstorm::storage::BeliefManager< PomdpType, BeliefValueType, StateType > | |
| Cstorm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType > | |
| Cstorm::generator::BeliefStateManager< ValueType > | This class keeps track of common information of a set of beliefs |
| Cstorm::generator::BeliefSupportTracker< ValueType > | |
| Cstorm::utility::BernoulliDistributionGenerator | |
| Cstorm::dft::storage::BijectionCandidates< ValueType > | |
| Cstorm::transformer::BinaryDtmcTransformer | |
| Cstorm::transformer::BinaryPomdpTransformer< ValueType > | |
| Cstorm::transformer::BinaryPomdpTransformerRowGroup | |
| Cstorm::transformer::BinaryPomdpTransformerRowGroupCompare | |
| Cstorm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType > | |
| Cstorm::storage::BitVector | A bit vector that is internally represented as a vector of 64-bit values |
| Cstorm::storage::BitVectorHashMap< ValueType, Hash > | This class represents a hash-map whose keys are bit vectors |
| Cstorm::storage::BitVectorHashMap< StateType > | |
| Cstorm::storage::BitVectorHashMap< uint32_t > | |
| Cstorm::storage::BitVectorHashMap< ValueType, Hash >::BitVectorHashMapIterator | |
| Cstorm::storage::bisimulation::Block< DataType > | |
| Cstorm::generator::BooleanVariableInformation | |
| Cstorm::gbar::abstraction::BottomStateResult< DdType > | |
| Cstorm::logic::Bound | |
| Cstorm::modelchecker::exploration_detail::Bounds< StateType, ValueType > | |
| Cstorm::dft::storage::BucketPriorityQueue< PriorityType > | Priority queue based on buckets |
| Cstorm::dft::storage::BucketPriorityQueue< storm::dft::builder::DFTExplorationHeuristic > | |
| Cstorm::builder::BuilderOptions | |
| Ccarl::Cache< P > | |
| Cstorm::counterexamples::SMTMinimalLabelSetGenerator< T >::CexInput | |
| ►Cstorm::modelchecker::CheckResult | |
| Cstorm::modelchecker::ParetoCurveCheckResult< double > | |
| Cstorm::modelchecker::QuantitativeCheckResult< double > | |
| Cstorm::modelchecker::LexicographicCheckResult< ValueType > | |
| ►Cstorm::modelchecker::ParetoCurveCheckResult< ValueType > | |
| Cstorm::modelchecker::ExplicitParetoCurveCheckResult< ValueType > | |
| Cstorm::modelchecker::SymbolicParetoCurveCheckResult< Type, ValueType > | |
| ►Cstorm::modelchecker::QualitativeCheckResult | |
| Cstorm::modelchecker::ExplicitQualitativeCheckResult | |
| Cstorm::modelchecker::SymbolicQualitativeCheckResult< Type > | |
| ►Cstorm::modelchecker::QuantitativeCheckResult< ValueType > | |
| Cstorm::modelchecker::ExplicitQuantitativeCheckResult< ValueType > | |
| Cstorm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType > | |
| Cstorm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType > | |
| ►Cstorm::modelchecker::RegionCheckResult< ValueType > | |
| Cstorm::modelchecker::RegionRefinementCheckResult< ValueType > | |
| Cstorm::modelchecker::CheckTask< FormulaType, ValueType > | |
| Cstorm::generator::Choice< ValueType, StateType > | |
| Cstorm::transformer::detail::ChoiceLabelIdStorage | |
| ►Cstorm::storage::sparse::ChoiceOrigins | This class represents the origin of the choices of a model in terms of the input model specification (e.g., the Prism commands that induced the choice) |
| Cstorm::storage::sparse::JaniChoiceOrigins | This class represents for each choice the origin in the jani specification // TODO complete this |
| Cstorm::storage::sparse::PrismChoiceOrigins | This class represents for each choice the set of prism commands that induced the choice |
| Cstorm::transformer::ChoiceSelector< ValueType, RewardModelType > | |
| Cstorm::utility::parametric::CoefficientType< FunctionType > | Acess the type of coefficients from a given function type |
| Cstorm::utility::parametric::CoefficientType< ParametricType > | |
| Cstorm::utility::parametric::CoefficientType< typename SparseModelType::ValueType > | |
| Cstorm::utility::parametric::CoefficientType< ValueType > | |
| Cstorm::gbar::abstraction::prism::CommandAbstractor< DdType, ValueType > | |
| ►Cstorm::expressions::CompiledExpression | |
| Cstorm::expressions::ExprtkCompiledExpression | |
| Cstorm::builder::ComposerResult< Type, ValueType > | |
| ►Cstorm::jani::Composition | |
| Cstorm::jani::AutomatonComposition | |
| Cstorm::jani::ParallelComposition | |
| ►Cstorm::prism::Composition | |
| Cstorm::prism::HidingComposition | |
| Cstorm::prism::ModuleComposition | |
| ►Cstorm::prism::ParallelComposition | |
| Cstorm::prism::InterleavingParallelComposition | |
| Cstorm::prism::RestrictedParallelComposition | |
| Cstorm::prism::SynchronizingParallelComposition | |
| Cstorm::prism::RenamingComposition | |
| Cstorm::jani::CompositionInformation | |
| Cstorm::builder::CompositionVariables< Type, ValueType > | |
| ►Cstorm::jani::CompositionVisitor | |
| Cstorm::builder::CompositionVariableCreator< Type, ValueType > | |
| ►Cstorm::builder::SystemComposer< Type, ValueType > | |
| Cstorm::builder::CombinedEdgesSystemComposer< Type, ValueType > | |
| Cstorm::jani::CompositionInformationVisitor | |
| Cstorm::jani::CompositionJsonExporter | |
| Cstorm::jani::CompositionSimplificationVisitor | |
| ►Cstorm::prism::CompositionVisitor | |
| Cstorm::builder::ModuleComposer< Type, ValueType > | |
| Cstorm::prism::CompositionToJaniVisitor | |
| Cstorm::prism::CompositionValidityChecker | |
| Cstorm::jani::ConditionalMetaEdge | |
| Cstorm::storage::ConsecutiveUint64DynamicPriorityQueue< Compare > | |
| Cstorm::dft::storage::FailableElements::const_iterator | Iterator for failable elements |
| Cstorm::storage::BitVector::const_iterator | A class that enables iterating over the indices of the bit vector whose corresponding bits are set to true |
| Cstorm::storage::BitVector::const_reverse_iterator | A class that enables iterating over the indices of the bit vector whose corresponding bits are set to true |
| Cstorm::storage::SparseMatrix< ValueType >::const_rows | This class represents a number of consecutive rows of the matrix |
| Cstorm::jani::Constant | |
| Cstorm::utility::ConstantsComparator< ValueType, Enable > | |
| Cstorm::utility::ConstantsComparator< typename PomdpModelType::ValueType > | |
| Cstorm::utility::ConstantsComparator< typename PomdpType::ValueType > | |
| Cstorm::utility::ConstantsComparator< ValueType > | |
| Cstorm::utility::ConstantsComparator< ValueType, ConstantsComparatorEnablePrecision< ValueType > > | |
| Cstorm::jani::detail::ConstEdges | |
| ►Cstorm::jani::ConstJaniTraverser | |
| Cstorm::jani::AssignmentLevelFinder | |
| Cstorm::jani::AssignmentsFinder | |
| Cstorm::jani::RewardModelInformation | |
| Cstorm::jani::detail::ArrayExpressionFinderTraverser | |
| Cstorm::jani::detail::FunctionCallExpressionFinderTraverser | |
| Cstorm::jani::detail::InformationCollector | |
| Cstorm::jani::detail::VariableAccessedTraverser | |
| Cstorm::analysis::ConstraintCollector< ValueType > | Class to collect constraints on parametric Markov chains |
| Cstorm::analysis::ConstraintType< ValueType, Enable > | |
| Cstorm::analysis::ConstraintType< ValueType, typename std::enable_if< std::is_same< storm::RationalFunction, ValueType >::value >::type > | |
| Cstorm::transformer::ContinuousToDiscreteTimeModelTransformer< ValueType, RewardModelType > | |
| Cstorm::modelchecker::helper::rewardbounded::CostLimit | |
| Cstorm::modelchecker::helper::rewardbounded::CostLimitClosure | |
| Cstorm::modelchecker::helper::rewardbounded::CostLimitClosure::CostLimitsCompare | |
| ►Cstorm::counterexamples::Counterexample | |
| Cstorm::counterexamples::HighLevelCounterexample | |
| Cstorm::counterexamples::PathCounterexample< ValueType > | |
| CCudd | |
| Cstorm::dd::CuddPointerPairHash | |
| Cstorm::transformer::DAProductBuilder | |
| ►Cstorm::dd::Dd< LibraryType > | |
| Cstorm::dd::Add< Type, ValueType > | |
| Cstorm::dd::Add< DdType, double > | |
| Cstorm::dd::Add< DdType, ValueType > | |
| Cstorm::dd::Add< Type, double > | |
| Cstorm::dd::Bdd< DdType > | |
| Cstorm::dd::Bdd< Type > | |
| Cstorm::dd::Bdd< storm::dd::DdType::CUDD > | |
| Cstorm::dd::Bdd< storm::dd::DdType::Sylvan > | |
| Cstorm::dd::Add< LibraryType, ValueType > | |
| Cstorm::dd::Bdd< LibraryType > | |
| Cstorm::builder::DdJaniModelBuilder< Type, ValueType > | |
| Cstorm::dd::DdMetaVariable< LibraryType > | |
| Cstorm::builder::DdPrismModelBuilder< Type, ValueType > | |
| Cstorm::builder::DdPrismModelBuilder< Type, ValueType > | |
| Cstorm::storage::Decomposition< BlockType > | This class represents the decomposition of a model into blocks which are of the template type |
| Cstorm::storage::Decomposition< LongRunComponentType > | |
| ►Cstorm::storage::Decomposition< MaximalEndComponent > | |
| Cstorm::storage::MaximalEndComponentDecomposition< ValueType > | This class represents the decomposition of a nondeterministic model into its maximal end components |
| ►Cstorm::storage::Decomposition< StateBlock > | |
| ►Cstorm::storage::BisimulationDecomposition< ModelType, bisimulation::DeterministicBlockData > | |
| Cstorm::storage::DeterministicModelBisimulationDecomposition< ModelType > | This class represents the decomposition of a deterministic model into its bisimulation quotient |
| Cstorm::storage::NondeterministicModelBisimulationDecomposition< ModelType > | This class represents the decomposition of a nondeterministic model into its bisimulation quotient |
| Cstorm::storage::BisimulationDecomposition< ModelType, BlockDataType > | This class is the superclass of all decompositions of a sparse model into its bisimulation quotient |
| ►Cstorm::storage::Decomposition< StronglyConnectedComponent > | |
| Cstorm::storage::StronglyConnectedComponentDecomposition< ValueType > | This class represents the decomposition of a graph-like structure into its strongly connected components |
| CDefaultDoubleVIEnvironment | |
| Cstorm::dft::modelchecker::DependencyPair | |
| Cstorm::adapters::DereferenceIteratorAdapter< ContainerType > | |
| Cstorm::adapters::Dereferencer< T > | |
| Cstorm::automata::DeterministicAutomaton | |
| Cstorm::storage::bisimulation::DeterministicBlockData | |
| Cstorm::parser::DeterministicModelParser< ValueType, RewardValueType > | Loads a deterministic model (Dtmc or Ctmc) from files |
| Cstorm::modelchecker::multiobjective::DeterministicSchedsAchievabilityChecker< SparseModelType, GeometryValueType > | |
| Cstorm::modelchecker::multiobjective::DeterministicSchedsLpChecker< ModelType, GeometryValueType > | Represents the LP Encoding for achievability under simple strategies |
| Cstorm::modelchecker::multiobjective::DeterministicSchedsObjectiveHelper< ModelType > | |
| Cstorm::modelchecker::multiobjective::DeterministicSchedsParetoExplorer< SparseModelType, GeometryValueType > | Implements the exploration of the Pareto front |
| Cstorm::parser::DeterministicSparseTransitionParser< ValueType > | This class can be used to parse a file containing either transitions or transition rewards of a deterministic model |
| Cstorm::storage::DeterministicTransition< ProbabilityType > | |
| Cstorm::dft::storage::DFT< ValueType > | Represents a Dynamic Fault Tree |
| Cstorm::storage::DFT< ValueType > | |
| Cstorm::dft::storage::DFT< ParametricType > | |
| Cstorm::dft::modelchecker::DFTASFChecker | |
| Cstorm::dft::builder::DFTBuilder< ValueType > | |
| Cstorm::dft::storage::DFTColouring< ValueType > | |
| ►Cstorm::dft::storage::elements::DFTElement< ValueType > | Abstract base class for DFT elements |
| ►Cstorm::dft::storage::elements::DFTBE< ValueType > | Abstract base class for basic events (BEs) in DFTs |
| Cstorm::dft::storage::elements::BEConst< ValueType > | BE which is either constant failed or constant failsafe |
| Cstorm::dft::storage::elements::BEErlang< ValueType > | BE with Erlang failure distribution |
| Cstorm::dft::storage::elements::BEExponential< ValueType > | BE with exponential failure distribution |
| Cstorm::dft::storage::elements::BELogNormal< ValueType > | BE with log-normal failure distribution |
| Cstorm::dft::storage::elements::BEProbability< ValueType > | BE with constant (Bernoulli) failure probability distribution |
| Cstorm::dft::storage::elements::BESamples< ValueType > | BE where the failure distribution is defined by samples |
| Cstorm::dft::storage::elements::BEWeibull< ValueType > | BE with Weibull failure distribution |
| ►Cstorm::dft::storage::elements::DFTChildren< ValueType > | Abstract base class for a DFT element with children |
| ►Cstorm::dft::storage::elements::DFTGate< ValueType > | Abstract base class for gates |
| Cstorm::dft::storage::elements::DFTAnd< ValueType > | AND gate |
| Cstorm::dft::storage::elements::DFTOr< ValueType > | OR gate |
| Cstorm::dft::storage::elements::DFTPand< ValueType > | Priority AND (PAND) gate |
| Cstorm::dft::storage::elements::DFTPor< ValueType > | Priority OR (POR) gate |
| Cstorm::dft::storage::elements::DFTSpare< ValueType > | SPARE gate |
| Cstorm::dft::storage::elements::DFTVot< ValueType > | VOT gate with threshold k |
| ►Cstorm::dft::storage::elements::DFTRestriction< ValueType > | Abstract base class for restrictions |
| Cstorm::dft::storage::elements::DFTMutex< ValueType > | Mutex restriction (MUTEX) |
| Cstorm::dft::storage::elements::DFTSeq< ValueType > | Sequence enforcer (SEQ) |
| Cstorm::dft::storage::elements::DFTDependency< ValueType > | Dependency gate with probability p |
| Cstorm::dft::storage::DFTElementSort< ValueType > | |
| ►Cstorm::dft::builder::DFTExplorationHeuristic< ValueType > | General super class for approximation heuristics |
| Cstorm::dft::builder::DFTExplorationHeuristicDepth< ValueType > | |
| ►Cstorm::dft::builder::DFTExplorationHeuristicProbability< ValueType > | |
| Cstorm::dft::builder::DFTExplorationHeuristicBoundDifference< ValueType > | |
| Cstorm::dft::parser::DFTGalileoParser< ValueType > | Parser for DFT in the Galileo format |
| Cstorm::dft::transformations::DftInstantiator< ParametricType, ConstantType > | Instantiator to yield a concrete DFT from a parametric DFT (with parametric failure rates) |
| Cstorm::dft::storage::DFTIsomorphismCheck< ValueType > | Saves isomorphism between subtrees |
| Cstorm::dft::storage::DftJsonExporter< ValueType > | Exports a DFT into the JSON format |
| Cstorm::dft::parser::DFTJsonParser< ValueType > | Parser for DFT in custom JSON format |
| Cstorm::dft::storage::DFTLayoutInfo | |
| Cstorm::dft::modelchecker::DFTModelChecker< ValueType > | Analyser for DFTs |
| Cstorm::dft::modelchecker::DftModularizationChecker< ValueType > | DFT analysis via modularization |
| Cstorm::dft::utility::DftModularizer< ValueType > | Find modules (independent subtrees) in DFT |
| ►Cstorm::dft::storage::DftModule | Represents a module/subtree in a DFT |
| Cstorm::dft::storage::DftIndependentModule | Represents an independent module/subtree |
| Cstorm::dft::generator::DftNextStateGenerator< ValueType, StateType > | Next state generator for DFTs |
| Cstorm::dft::generator::DftNextStateGenerator< ValueType, uint32_t > | |
| Cstorm::dft::storage::DFTState< ValueType > | |
| Cstorm::dft::storage::DFTStateGenerationInfo | |
| Cstorm::dft::storage::DFTStateSpaceGenerationQueues< ValueType > | |
| Cstorm::dft::storage::DftSymmetries | |
| Cstorm::dft::transformations::DftToGspnTransformator< ValueType > | Transformator for DFT -> GSPN |
| Cstorm::dft::simulator::DFTTraceSimulator< ValueType > | Simulator for DFTs |
| Cstorm::dft::transformations::DftTransformer< ValueType > | Transformer for operations on DFT |
| Cstorm::dft::utility::DftValidator< ValueType > | |
| Cstorm::modelchecker::helper::rewardbounded::Dimension< ValueType > | |
| Cstorm::io::DirectEncodingOptions | |
| Cstorm::parser::DirectEncodingParser< ValueType, RewardModelType > | Parser for models in the DRN format with explicit encoding |
| Cstorm::parser::DirectEncodingParserOptions | |
| Cstorm::simulator::DiscreteTimePrismProgramSimulator< ValueType > | This class provides a simulator interface on the prism program, and uses the next state generator |
| Cstorm::simulator::DiscreteTimeSparseModelSimulator< ValueType, RewardModelType > | This class is a low-level interface to quickly sample from Discrete-Time Models stored explicitly as a SparseModel |
| Cstorm::generator::Distribution< IndexType, ValueType > | |
| ►Cstorm::storage::Distribution< ValueType, StateType > | |
| Cstorm::storage::DistributionWithReward< ValueType, StateType > | |
| Cstorm::storage::Distribution< ValueType, uint32_t > | |
| Cstorm::storage::Distribution< ValueType, uint_fast64_t > | |
| Cstorm::generator::DistributionEntry< StateType, ValueType > | |
| Cstorm::utility::detail::DoubleGreater | |
| Cstorm::utility::detail::DoubleLess | |
| Cstorm::modelchecker::helper::DsMpiDtmcPriorityLess< ValueType > | |
| ►Cstorm::modelchecker::helper::DsMpiDtmcUpperRewardBoundsComputer< ValueType > | |
| Cstorm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer< ValueType > | |
| Cstorm::modelchecker::helper::DsMpiMdpPriorityLess< ValueType > | |
| Cstorm::storage::DynamicPriorityQueue< T, Container, Compare > | |
| Cstorm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseModelType >::EcQuotient | |
| Cstorm::jani::Edge | |
| Cstorm::gbar::abstraction::jani::EdgeAbstractor< DdType, ValueType > | |
| Cstorm::jani::EdgeContainer | |
| Cstorm::builder::CombinedEdgesSystemComposer< Type, ValueType >::EdgeDd | |
| Cstorm::jani::EdgeDestination | |
| Cstorm::builder::EdgeDestinationDd< Type, ValueType > | |
| Cstorm::jani::detail::Edges | |
| Cstorm::adapters::EigenAdapter | |
| Cstorm::EigenSolverEnvironment | |
| Cstorm::utility::detail::ElementGreater< ValueType > | |
| Cstorm::utility::detail::ElementGreater< double > | |
| Cstorm::utility::detail::ElementLess< ValueType > | |
| Cstorm::utility::detail::ElementLess< double > | |
| Cstorm::jani::JaniLocalEliminator::EliminationScheduler | |
| Cstorm::solver::stateelimination::EliminatorBase< ValueType, Mode > | |
| ►Cstorm::solver::stateelimination::EliminatorBase< ValueType, ScalingMode::Divide > | |
| Cstorm::solver::stateelimination::EquationSystemEliminator< ValueType > | |
| ►Cstorm::solver::stateelimination::EliminatorBase< ValueType, ScalingMode::DivideOneMinus > | |
| ►Cstorm::solver::stateelimination::StateEliminator< ValueType > | |
| Cstorm::solver::stateelimination::ConditionalStateEliminator< ValueType > | |
| Cstorm::solver::stateelimination::NondeterministicModelStateEliminator< ValueType > | |
| ►Cstorm::solver::stateelimination::PrioritizedStateEliminator< ValueType > | |
| Cstorm::solver::stateelimination::MultiValueStateEliminator< ValueType > | |
| ►Cstd::enable_shared_from_this | |
| Cstorm::dd::DdManager< DdType > | |
| Cstorm::dd::DdManager< DdType::CUDD > | |
| Cstorm::dd::DdManager< DdType::Sylvan > | |
| Cstorm::dd::DdManager< storm::dd::DdType::CUDD > | |
| Cstorm::dd::DdManager< storm::dd::DdType::Sylvan > | |
| Cstorm::dd::DdManager< LibraryType > | |
| ►Cstorm::expressions::BaseExpression | The base class of all expression classes |
| ►Cstorm::expressions::ArrayExpression | The base class of all array expressions |
| Cstorm::expressions::ConstructorArrayExpression | Represents an array of the given size, where the i'th entry is determined by the elementExpression, where occurrences of indexVar will be substituted by i |
| Cstorm::expressions::ValueArrayExpression | Represents an array with a given list of elements |
| ►Cstorm::expressions::BinaryExpression | The base class of all binary expressions |
| Cstorm::expressions::ArrayAccessExpression | Represents an access to an array |
| Cstorm::expressions::BinaryBooleanFunctionExpression | |
| Cstorm::expressions::BinaryNumericalFunctionExpression | |
| Cstorm::expressions::BinaryRelationExpression | |
| Cstorm::expressions::BooleanLiteralExpression | |
| Cstorm::expressions::FunctionCallExpression | Represents an array with a given list of elements |
| Cstorm::expressions::IfThenElseExpression | |
| Cstorm::expressions::IntegerLiteralExpression | |
| Cstorm::expressions::PredicateExpression | The base class of all binary expressions |
| Cstorm::expressions::RationalLiteralExpression | |
| Cstorm::expressions::TranscendentalNumberLiteralExpression | |
| ►Cstorm::expressions::UnaryExpression | |
| Cstorm::expressions::UnaryBooleanFunctionExpression | |
| Cstorm::expressions::UnaryNumericalFunctionExpression | |
| Cstorm::expressions::VariableExpression | |
| Cstorm::expressions::ExpressionManager | This class is responsible for managing a set of typed variables and all expressions using these variables |
| ►Cstorm::logic::Formula | |
| Cstorm::logic::ConditionalFormula | |
| ►Cstorm::logic::PathFormula | |
| ►Cstorm::logic::BinaryPathFormula | |
| Cstorm::logic::BinaryBooleanPathFormula | |
| Cstorm::logic::UntilFormula | |
| Cstorm::logic::BoundedUntilFormula | |
| Cstorm::logic::CumulativeRewardFormula | |
| Cstorm::logic::HOAPathFormula | |
| Cstorm::logic::InstantaneousRewardFormula | |
| Cstorm::logic::LongRunAverageRewardFormula | |
| Cstorm::logic::TotalRewardFormula | |
| ►Cstorm::logic::UnaryPathFormula | |
| Cstorm::logic::EventuallyFormula | |
| Cstorm::logic::GloballyFormula | |
| Cstorm::logic::NextFormula | |
| Cstorm::logic::UnaryBooleanPathFormula | |
| ►Cstorm::logic::StateFormula | |
| Cstorm::logic::AtomicExpressionFormula | |
| Cstorm::logic::AtomicLabelFormula | |
| ►Cstorm::logic::BinaryStateFormula | |
| Cstorm::logic::BinaryBooleanStateFormula | |
| Cstorm::logic::BooleanLiteralFormula | |
| Cstorm::logic::MultiObjectiveFormula | |
| Cstorm::logic::QuantileFormula | |
| ►Cstorm::logic::UnaryStateFormula | |
| Cstorm::logic::GameFormula | |
| ►Cstorm::logic::OperatorFormula | |
| Cstorm::logic::LongRunAverageOperatorFormula | |
| Cstorm::logic::ProbabilityOperatorFormula | |
| Cstorm::logic::RewardOperatorFormula | |
| Cstorm::logic::TimeOperatorFormula | |
| Cstorm::logic::UnaryBooleanStateFormula | |
| ►Cstorm::models::ModelBase | |
| ►Cstorm::models::Model< CValueType > | |
| ►Cstorm::models::sparse::Model< CValueType, CRewardModelType > | Base class for all sparse models |
| Cstorm::models::sparse::DeterministicModel< ValueType, StandardRewardModel< ValueType > > | |
| Cstorm::models::sparse::DeterministicModel< FunctionType, StandardRewardModel< FunctionType > > | |
| Cstorm::models::sparse::NondeterministicModel< ValueType, StandardRewardModel< ValueType > > | |
| Cstorm::models::sparse::NondeterministicModel< double, RM > | |
| Cstorm::models::sparse::NondeterministicModel< double, storm::models::sparse::StandardRewardModel< double > > | |
| Cstorm::models::sparse::NondeterministicModel< ValueType, storm::models::sparse::StandardRewardModel< ValueType > > | |
| ►Cstorm::models::sparse::DeterministicModel< ValueType, RewardModelType > | The base class of all sparse deterministic models |
| Cstorm::models::sparse::Dtmc< FunctionType > | |
| Cstorm::models::sparse::Ctmc< ValueType, RewardModelType > | This class represents a continuous-time Markov chain |
| Cstorm::models::sparse::Dtmc< ValueType, RewardModelType > | This class represents a discrete-time Markov chain |
| ►Cstorm::models::sparse::NondeterministicModel< ValueType, RewardModelType > | The base class of sparse nondeterministic models |
| Cstorm::models::sparse::Mdp< ValueType, StandardRewardModel< ValueType > > | |
| Cstorm::models::sparse::Mdp< double, RM > | |
| Cstorm::models::sparse::Mdp< double, storm::models::sparse::StandardRewardModel< double > > | |
| Cstorm::models::sparse::MarkovAutomaton< ValueType, RewardModelType > | This class represents a Markov automaton |
| ►Cstorm::models::sparse::Mdp< ValueType, RewardModelType > | This class represents a (discrete-time) Markov decision process |
| Cstorm::models::sparse::Pomdp< ValueType, RewardModelType > | This class represents a partially observable Markov decision process |
| Cstorm::models::sparse::Smg< ValueType, RewardModelType > | This class represents a stochastic multiplayer game |
| Cstorm::models::sparse::StochasticTwoPlayerGame< ValueType, RewardModelType > | This class represents a (discrete-time) stochastic two-player game |
| Cstorm::models::Model< double > | |
| Cstorm::models::Model< FunctionType > | |
| ►Cstorm::models::Model< ValueType > | |
| Cstorm::models::sparse::Model< ValueType, StandardRewardModel< ValueType > > | |
| Cstorm::models::sparse::Model< FunctionType, StandardRewardModel< FunctionType > > | |
| Cstorm::models::sparse::Model< ValueType > | |
| Cstorm::models::sparse::Model< double, RM > | |
| Cstorm::models::sparse::Model< double, storm::models::sparse::StandardRewardModel< double > > | |
| Cstorm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< ValueType > > | |
| Cstorm::models::symbolic::Model< DdType, ValueType > | |
| ►Cstorm::models::symbolic::Model< Type, ValueType > | |
| ►Cstorm::models::symbolic::NondeterministicModel< Type, ValueType > | |
| ►Cstorm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
| Cstorm::gbar::abstraction::MenuGame< Type, ValueType > | This class represents a discrete-time stochastic two-player game |
| Cstorm::models::symbolic::NondeterministicModel< DdType, ValueType > | |
| Cstorm::models::symbolic::Model< Type, double > | |
| ►Cstorm::models::symbolic::Model< Type, CValueType > | Base class for all symbolic models |
| Cstorm::models::symbolic::DeterministicModel< Type, double > | |
| Cstorm::models::symbolic::NondeterministicModel< Type, double > | |
| ►Cstorm::models::symbolic::DeterministicModel< Type, ValueType > | Base class for all deterministic symbolic models |
| Cstorm::models::symbolic::Ctmc< Type, ValueType > | This class represents a continuous-time Markov chain |
| Cstorm::models::symbolic::Dtmc< Type, ValueType > | This class represents a discrete-time Markov chain |
| ►Cstorm::models::symbolic::NondeterministicModel< Type, ValueType > | Base class for all nondeterministic symbolic models |
| Cstorm::models::symbolic::MarkovAutomaton< Type, ValueType > | This class represents a discrete-time Markov decision process |
| Cstorm::models::symbolic::Mdp< Type, ValueType > | This class represents a discrete-time Markov decision process |
| Cstorm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | This class represents a discrete-time stochastic two-player game |
| Cstorm::transformer::EndComponentEliminator< ValueType > | |
| Cstorm::transformer::EndComponentEliminator< ValueType >::EndComponentEliminatorReturnType | |
| Cstorm::Environment | |
| Cstorm::modelchecker::helper::rewardbounded::EpochManager | |
| Cstorm::modelchecker::helper::rewardbounded::EpochModel< ValueType, SingleObjectiveMode > | |
| Cstorm::expressions::EquivalenceChecker | |
| ►Cstd::exception | |
| Cstorm::automata::HOAConsumerDAHeader::header_parsing_done | |
| Cstorm::exceptions::BaseException | This class represents the base class of all exception classes |
| Cstorm::dft::builder::ExplicitDFTModelBuilder< ValueType, StateType > | Build a Markov chain from DFT |
| Cstorm::gbar::abstraction::ExplicitDijkstraQueueElement< ValueType > | |
| Cstorm::gbar::abstraction::ExplicitDijkstraQueueElementLess< ValueType > | |
| Cstorm::gbar::modelchecker::ExplicitGameExporter< ValueType > | |
| ►Cstorm::utility::graph::ExplicitGameProb01Result | |
| Cstorm::gbar::abstraction::ExplicitQualitativeGameResult | |
| Cstorm::storage::ExplicitGameStrategy | |
| Cstorm::storage::ExplicitGameStrategyPair | |
| Cstorm::builder::ExplicitModelBuilder< ValueType, RewardModelType, StateType > | |
| Cstorm::gbar::abstraction::ExplicitPivotStateResult< ValueType > | |
| Cstorm::gbar::abstraction::ExplicitQuantitativeResult< ValueType > | |
| Cstorm::gbar::abstraction::ExplicitQuantitativeResultMinMax< ValueType > | |
| Cstorm::builder::ExplicitStateLookup< StateType > | |
| Cstorm::modelchecker::exploration_detail::ExplorationInformation< StateType, ValueType > | |
| Cstorm::utility::ExponentialDistributionGenerator | |
| Cstorm::expressions::Expression | |
| Cstorm::parser::ExpressionCreator | |
| Cstorm::expressions::ExpressionEvaluator< V > | |
| Cstorm::expressions::ExpressionEvaluator< ValueType > | |
| ►Cstorm::expressions::ExpressionEvaluatorBase< RationalReturnType > | |
| ►Cstorm::expressions::ExprtkExpressionEvaluatorBase< double > | |
| ►Cstorm::expressions::ExprtkExpressionEvaluator | |
| Cstorm::expressions::ExpressionEvaluator< double > | |
| Cstorm::expressions::ExpressionEvaluatorBase< double > | |
| ►Cstorm::expressions::ExpressionEvaluatorBase< RationalType > | |
| ►Cstorm::expressions::ExprtkExpressionEvaluatorBase< RationalType > | |
| Cstorm::expressions::ExpressionEvaluatorWithVariableToExpressionMap< RationalType > | |
| ►Cstorm::expressions::ExpressionVisitor | |
| Cstorm::adapters::AddExpressionAdapter< Type, ValueType > | |
| Cstorm::expressions::ChangeManagerVisitor | |
| Cstorm::expressions::CheckIfThenElseGuardVisitor | |
| Cstorm::expressions::FullPredicateSplitter | |
| Cstorm::expressions::LinearCoefficientVisitor | |
| Cstorm::expressions::LinearityCheckVisitor | |
| ►Cstorm::expressions::ReduceNestingVisitor | |
| Cstorm::expressions::JaniReduceNestingExpressionVisitor | |
| Cstorm::expressions::RestrictSyntaxVisitor | |
| ►Cstorm::expressions::SubstitutionVisitor< MapType > | |
| Cstorm::expressions::JaniExpressionSubstitutionVisitor< MapType > | |
| ►Cstorm::expressions::SyntacticalEqualityCheckVisitor | |
| Cstorm::expressions::JaniSyntacticalEqualityCheckVisitor | |
| Cstorm::expressions::ToCppVisitor | |
| Cstorm::expressions::ToDiceStringVisitor | |
| Cstorm::expressions::ToExprtkStringVisitor | |
| Cstorm::expressions::ToRationalNumberVisitor< RationalNumberType > | |
| Cstorm::expressions::VariableSetPredicateSplitter | |
| Cstorm::gbar::abstraction::ExpressionTranslator< DdType > | |
| Cstorm::jani::ExpressionToJson | |
| Cstorm::jani::detail::ArrayExpressionEliminationVisitor | Eliminates the array accesses in the given expression, for example ([[1],[2,3]])[i][j] --> i=0 ? [1][j] : [2,3][j] --> i=0 ? 1 : (j=0 ? 2 : 3) |
| Cstorm::jani::detail::ArrayExpressionFinderExpressionVisitor | |
| Cstorm::jani::detail::ArrayReplacementsCollectorExpressionVisitor | |
| Cstorm::jani::detail::FunctionCallExpressionFinderExpressionVisitor | |
| Cstorm::jani::detail::FunctionEliminationExpressionVisitor | |
| Cstorm::pomdp::storage::ExtremePOMDPValueBound< ValueType > | Struct to store the extreme bound values needed for the reward correction values when clipping is used |
| Cstorm::utility::Extremum< Dir, ValueType > | Stores and manages an extremal (maximal or minimal) value |
| Cstorm::utility::Extremum< Dir, ExactValueType > | |
| Cstorm::utility::Extremum< invert(Dir), ValueType > | |
| Cstorm::utility::Extremum< OptimizationDirection::Maximize, ValueType > | |
| Cstorm::modelchecker::multiobjective::DeterministicSchedsParetoExplorer< SparseModelType, GeometryValueType >::Facet | |
| Ccarl::FactorizedPolynomial< P > | |
| Cstorm::dft::storage::FailableElements | Handling of currently failable elements (BEs) either due to their own failure or because of dependencies |
| Cstorm::dft::utility::FailureBoundFinder | |
| Cstorm::dft::utility::FDEPConflictFinder< ValueType > | |
| Cstorm::pars::FeasibilitySynthesisTask | |
| Cstorm::utility::pfinternal::Features | |
| Cstorm::utility::FilteredRewardModel< RewardModelType > | |
| Cstorm::jani::FilterExpression | |
| Cstorm::parser::DeterministicSparseTransitionParser< ValueType >::FirstPassResult | A structure representing the result of the first pass of this parser |
| Cstorm::parser::MarkovAutomatonSparseTransitionParser< ValueType >::FirstPassResult | A structure representing the result of the first pass of this parser |
| Cstorm::parser::NondeterministicSparseTransitionParser< ValueType >::FirstPassResult | A structure representing the result of the first pass of this parser |
| Cstorm::storage::FlexibleSparseMatrix< ValueType > | The flexible sparse matrix is used during state elimination |
| Cstorm::storage::FNV1aBitVectorHash | |
| Cstorm::logic::FormulaInformation | |
| Cstorm::pomdp::analysis::FormulaInformation | |
| Cstorm::parser::FormulaParser | |
| ►Cstorm::logic::FormulaVisitor | |
| Cstorm::jani::FormulaToJaniJson | |
| ►Cstorm::logic::CloneVisitor | |
| Cstorm::logic::ExpectedTimeToExpectedRewardVisitor | |
| Cstorm::logic::ExpressionSubstitutionVisitor | |
| Cstorm::logic::ExtractMaximalStateFormulasVisitor | |
| Cstorm::logic::LabelSubstitutionVisitor | |
| Cstorm::logic::RewardAccumulationEliminationVisitor | |
| Cstorm::logic::RewardModelNameSubstitutionVisitor | |
| Cstorm::logic::FormulaInformationVisitor | |
| Cstorm::logic::FragmentChecker | |
| Cstorm::logic::LiftableTransitionRewardsVisitor | |
| Cstorm::logic::ToExpressionVisitor | |
| Cstorm::logic::ToPrefixStringVisitor | |
| Cstorm::utility::numerical::FoxGlynnResult< ValueType > | |
| Cstorm::logic::FragmentSpecification | |
| Cstorm::dd::FromVectorHelper< LibraryType, ValueType > | |
| Cstorm::dd::FromVectorHelper< LibraryType, storm::RationalFunction > | |
| Cstorm::jani::FunctionDefinition | |
| Cstorm::gbar::modelchecker::GameBasedMdpModelCheckerOptions | |
| Cstorm::gbar::abstraction::GameBddResult< DdType > | |
| Cstorm::GameSolverEnvironment | |
| Cstorm::solver::GameSolverFactory< ValueType > | |
| Cstorm::dft::storage::GateGroupToHash | |
| Cstorm::builder::DdPrismModelBuilder< Type, ValueType >::GenerationInformation< Type, ValueType > | |
| Cstorm::counterexamples::SMTMinimalLabelSetGenerator< T >::GeneratorStats | |
| ►CGenericNumTraits | |
| CEigen::NumTraits< storm::RationalNumber > | |
| Cstorm::models::GetDdType< representation > | |
| Cstorm::models::GetDdType< ModelRepresentation::DdCudd > | |
| Cstorm::models::GetDdType< ModelRepresentation::DdSylvan > | |
| Cstorm::models::GetDdType< ModelRepresentation::Sparse > | |
| Cstorm::models::GetModelRepresentation< ddType > | |
| Cstorm::models::GetModelRepresentation< storm::dd::DdType::CUDD > | |
| Cstorm::models::GetModelRepresentation< storm::dd::DdType::Sylvan > | |
| Cstorm::transformer::GlobalPomdpMecChoiceEliminator< ValueType > | |
| Cstorm::transformer::GlobalPOMDPSelfLoopEliminator< ValueType > | |
| Cstorm::parser::GlobalProgramInformation | |
| Cstorm::adapters::GmmxxAdapter< T > | |
| Cstorm::GmmxxSolverEnvironment | |
| Cstorm::transformer::GoalStateMerger< SparseModelType > | |
| Cstorm::derivative::GradientDescentInstantiationSearcher< FunctionType, ConstantType > | |
| ►Cboost::spirit::qi::grammar | |
| Cstorm::parser::ExpressionParser | |
| Cstorm::parser::FormulaParserGrammar | |
| Cstorm::parser::ImcaParserGrammar< ValueType, StateType > | |
| Cstorm::parser::PrismParserGrammar | |
| Cstorm::gspn::GSPN | |
| Cstorm::gspn::GspnBuilder | |
| Cstorm::gspn::GspnJsonExporter | Exports a GSPN into the JSON format for visualizing it |
| Cstorm::parser::GspnParser | |
| Cstorm::solver::helper::GSVIBackend< ValueType, Dir, Relative > | |
| Cstorm::solver::GurobiEnvironment | |
| Cstorm::storage::geometry::Halfspace< ValueType > | |
| Cstorm::storage::geometry::Halfspace< GeometryValueType > | |
| Cstorm::utility::Hash< T > | |
| Cstd::hash< Eigen::Matrix< ValueType, Eigen::Dynamic, 1 > > | |
| Cstd::hash< std::pair< uint_fast64_t, uint_fast64_t > > | |
| Cstd::hash< storm::dd::InternalBdd< storm::dd::DdType::CUDD > > | |
| Cstd::hash< storm::dd::InternalBdd< storm::dd::DdType::Sylvan > > | |
| Cstd::hash< storm::generator::ObservationDenseBeliefState< T > > | |
| Cstd::hash< storm::generator::SparseBeliefState< T > > | |
| Cstd::hash< storm::storage::BitVector > | |
| Cstd::hash< storm::storage::StateActionPair > | |
| Cstd::hash< storm::storage::StateActionTarget > | |
| ►Ccpphoafparser::HOAConsumer | |
| ►Cstorm::automata::HOAConsumerDAHeader | |
| Cstorm::automata::HOAConsumerDA | |
| Cstorm::automata::HOAHeader | |
| Cstorm::modelchecker::helper::HybridCtmcCslHelper | |
| Cstorm::modelchecker::helper::HybridDtmcPrctlHelper< DdType, ValueType > | |
| Cstorm::modelchecker::helper::HybridMarkovAutomatonCslHelper | |
| Cstorm::modelchecker::helper::HybridMdpPrctlHelper< DdType, ValueType > | |
| Cstorm::storage::geometry::HyperplaneCollector< ValueType > | This class can be used to collect a set of hyperplanes (without duplicates) |
| Cstorm::storage::geometry::HyperplaneEnumeration< ValueType > | |
| Cstorm::storage::geometry::Hyperrectangle< ValueType > | |
| Cstorm::solver::helper::IIBackend< ValueType, Dir > | |
| Cstorm::solver::helper::IIData< ValueType > | |
| Cstorm::parser::ImcaMarkovAutomatonParser< ValueType > | |
| ►Cstorm::dft::simulator::ImportanceFunction< ValueType > | Abstract class for importance functions |
| Cstorm::dft::simulator::BECountImportanceFunction< ValueType > | Importance function based on counting the number of currently failed BEs |
| Cstorm::jani::InformationObject | |
| Cstorm::logic::InheritedInformation | |
| CBeliefExplorationAPITest< TestType >::Input | |
| Cstorm::storage::IntegerInterval | |
| Cstorm::generator::IntegerVariableInformation | |
| Cstorm::dd::InternalAdd< Type, ValueType > | |
| Cstorm::dd::InternalAdd< DdType::CUDD, ValueType > | |
| Cstorm::dd::InternalAdd< DdType::Sylvan, ValueType > | |
| Cstorm::dd::InternalAdd< LibraryType, double > | |
| Cstorm::dd::InternalAdd< LibraryType, ValueType > | |
| Cstorm::dd::InternalBdd< LibraryType > | |
| Cstorm::dd::InternalBdd< DdType::CUDD > | |
| Cstorm::dd::InternalBdd< DdType::Sylvan > | |
| Cstorm::dd::InternalDdManager< LibraryType > | |
| Cstorm::dd::InternalDdManager< DdType > | |
| Cstorm::dd::InternalDdManager< DdType::CUDD > | |
| Cstorm::dd::InternalDdManager< DdType::Sylvan > | |
| Cstorm::dd::InternalDdManager< storm::dd::DdType::Sylvan > | |
| Cstorm::InternalEnvironment | |
| Cstorm::pomdp::InternalObservationScheduler | |
| Cstorm::dd::bisimulation::InternalRepresentativeComputer< DdType > | |
| Cstorm::dd::bisimulation::InternalRepresentativeComputerBase< DdType > | |
| ►Cstorm::dd::bisimulation::InternalRepresentativeComputerBase< storm::dd::DdType::CUDD > | |
| Cstorm::dd::bisimulation::InternalRepresentativeComputer< storm::dd::DdType::CUDD > | |
| ►Cstorm::dd::bisimulation::InternalRepresentativeComputerBase< storm::dd::DdType::Sylvan > | |
| Cstorm::dd::bisimulation::InternalRepresentativeComputer< storm::dd::DdType::Sylvan > | |
| Cstorm::dd::bisimulation::InternalSignatureRefiner< LibraryType, ValueType > | |
| Cstorm::dd::bisimulation::InternalSignatureRefiner< storm::dd::DdType::CUDD, ValueType > | |
| Cstorm::dd::bisimulation::InternalSignatureRefinerOptions | |
| Cstorm::dd::bisimulation::InternalSparseQuotientExtractor< DdType, ValueType, ExportValueType > | |
| Cstorm::dd::bisimulation::InternalSparseQuotientExtractorBase< DdType, ValueType, ExportValueType > | |
| ►Cstorm::dd::bisimulation::InternalSparseQuotientExtractorBase< storm::dd::DdType::CUDD, ValueType > | |
| Cstorm::dd::bisimulation::InternalSparseQuotientExtractor< storm::dd::DdType::CUDD, ValueType > | |
| ►Cstorm::dd::bisimulation::InternalSparseQuotientExtractorBase< storm::dd::DdType::Sylvan, ValueType, ExportValueType > | |
| Cstorm::dd::bisimulation::InternalSparseQuotientExtractor< storm::dd::DdType::Sylvan, ValueType, ExportValueType > | |
| ►Cstorm::dd::bisimulation::InternalSylvanSignatureRefinerBase | |
| Cstorm::dd::bisimulation::InternalSignatureRefiner< storm::dd::DdType::Sylvan, ValueType > | |
| Ccarl::Interval< Number > | |
| Cstorm::solver::helper::IntervalIterationHelper< ValueType, TrivialRowGrouping > | Implements interval iteration |
| ►Cstorm::models::sparse::ItemLabeling | A base class managing the labeling of items with a number of (atomic) labels |
| Cstorm::models::sparse::ChoiceLabeling | This class manages the labeling of the choice space with a number of (atomic) labels |
| Cstorm::models::sparse::StateLabeling | This class manages the labeling of the state space with a number of (atomic) labels |
| Cstorm::pomdp::IterativePolicySearch< ValueType > | |
| Cstorm::pomdp::qualitative::JaniBeliefSupportMdpGenerator< ValueType > | |
| Cstorm::converter::JaniConversionOptions | |
| ►Cstorm::expressions::JaniExpressionVisitor | |
| Cstorm::expressions::JaniExpressionSubstitutionVisitor< MapType > | |
| Cstorm::expressions::JaniReduceNestingExpressionVisitor | |
| Cstorm::expressions::JaniSyntacticalEqualityCheckVisitor | |
| Cstorm::jani::ExpressionToJson | |
| Cstorm::jani::detail::ArrayExpressionEliminationVisitor | Eliminates the array accesses in the given expression, for example ([[1],[2,3]])[i][j] --> i=0 ? [1][j] : [2,3][j] --> i=0 ? 1 : (j=0 ? 2 : 3) |
| Cstorm::jani::detail::ArrayExpressionFinderExpressionVisitor | |
| Cstorm::jani::detail::ArrayReplacementsCollectorExpressionVisitor | |
| Cstorm::jani::detail::FunctionCallExpressionFinderExpressionVisitor | |
| Cstorm::jani::detail::FunctionEliminationExpressionVisitor | |
| Cstorm::builder::JaniGSPNBuilder | |
| Cstorm::jani::JaniLocalEliminator | |
| Cstorm::jani::JaniLocationExpander | |
| Cstorm::parser::JaniParser< ValueType > | |
| Cstorm::jani::JaniScopeChanger | |
| ►Cstorm::jani::JaniTraverser | |
| Cstorm::jani::detail::ArrayEliminatorDataCollector | Gets the data necessary for array elimination |
| Cstorm::jani::detail::ArrayVariableReplacer | |
| Cstorm::jani::detail::FunctionEliminatorTraverser | |
| ►Cstorm::jani::JaniType | |
| Cstorm::jani::ArrayType | |
| Cstorm::jani::BasicType | |
| Cstorm::jani::BoundedType | |
| Cstorm::jani::ClockType | |
| Cstorm::jani::ContinuousType | |
| Cstorm::jani::JsonExporter | |
| Cstorm::pomdp::transformer::KnownProbabilityTransformer< ValueType > | |
| Cstorm::transformer::LabelInformation | |
| Cstorm::builder::LabelOrExpression | |
| Cstorm::gspn::LayoutInfo | |
| ►Cstorm::solver::LinearEquationSolverFactory< ValueType > | |
| Cstorm::solver::EigenLinearEquationSolverFactory< ValueType > | |
| Cstorm::solver::EliminationLinearEquationSolverFactory< ValueType > | |
| Cstorm::solver::GeneralLinearEquationSolverFactory< ValueType > | |
| Cstorm::solver::GmmxxLinearEquationSolverFactory< ValueType > | |
| Cstorm::solver::NativeLinearEquationSolverFactory< ValueType > | |
| Cstorm::solver::TopologicalLinearEquationSolverFactory< ValueType > | |
| Cstorm::solver::LinearEquationSolverRequirements | |
| Cstorm::gbar::abstraction::LocalExpressionInformation< DdType > | |
| Cstorm::analysis::LocalMonotonicityResult< VariableType > | |
| ►Cstorm::prism::LocatedInformation | |
| Cstorm::prism::Assignment | |
| Cstorm::prism::Command | |
| Cstorm::prism::Constant | |
| Cstorm::prism::Formula | |
| Cstorm::prism::InitialConstruct | |
| ►Cstorm::prism::Label | |
| Cstorm::prism::ObservationLabel | |
| Cstorm::prism::Module | |
| Cstorm::prism::ModuleRenaming | |
| Cstorm::prism::Player | |
| Cstorm::prism::Program | |
| Cstorm::prism::RewardModel | |
| Cstorm::prism::StateActionReward | |
| Cstorm::prism::StateReward | |
| Cstorm::prism::SystemCompositionConstruct | |
| Cstorm::prism::TransitionReward | |
| Cstorm::prism::Update | |
| ►Cstorm::prism::Variable | |
| Cstorm::prism::BooleanVariable | |
| Cstorm::prism::ClockVariable | |
| Cstorm::prism::IntegerVariable | |
| Cstorm::jani::Location | Jani Location: |
| Cstorm::generator::LocationVariableInformation | |
| Cstorm::LongRunAverageSolverEnvironment | |
| ►Cstorm::solver::LpSolver< ValueType, RawMode > | An interface that captures the functionality of an LP solver |
| Cstorm::solver::GlpkLpSolver | |
| Cstorm::solver::GurobiLpSolver< ValueType, RawMode > | A class that implements the LpSolver interface using Gurobi |
| Cstorm::solver::SoplexLpSolver< ValueType, RawMode > | |
| Cstorm::solver::Z3LpSolver< ValueType, RawMode > | A class that implements the LpSolver interface using Z3 |
| Cstorm::solver::LpSolver< double > | |
| Cstorm::solver::LpSolver< ValueType, false > | |
| ►Cstorm::utility::solver::LpSolverFactory< ValueType > | |
| Cstorm::utility::solver::GlpkLpSolverFactory< ValueType > | |
| Cstorm::utility::solver::GurobiLpSolverFactory< ValueType > | |
| Cstorm::utility::solver::SoplexLpSolverFactory< ValueType > | |
| Cstorm::utility::solver::Z3LpSolverFactory< ValueType > | |
| Cstorm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseModelType >::LraMecDecomposition | |
| Cstorm::modelchecker::helper::internal::LraViHelper< ValueType, ComponentType, TransitionsType > | Helper class that performs iterations of the value iteration method |
| Cstorm::automata::LTL2DeterministicAutomaton | |
| Cstorm::jani::LValue | |
| Cstorm::transformer::MakePOMDPCanonic< ValueType > | |
| Cstorm::transformer::MakeStateSetObservationClosed< ValueType > | |
| Cstorm::parser::MappedFile | Opens a file and maps it to memory providing a char* containing the file content |
| Cstorm::gspn::Marking | |
| Cstorm::parser::MarkovAutomatonParser< ValueType, RewardValueType > | Loads a labeled Markov automaton from files |
| Cstorm::parser::MarkovAutomatonSparseTransitionParser< ValueType > | A class providing the functionality to parse the transitions of a Markov automaton |
| Cstorm::dd::Add< LibraryType, ValueType >::MatrixAndLabeling | Converts the ADD to a row-grouped (sparse) matrix |
| Cstorm::storage::MatrixEntry< IndexType, ValueType > | |
| Cstorm::storage::MaximalEndComponent | This class represents a maximal end-component of a nondeterministic model |
| Cstorm::modelchecker::helper::MaybeStateResult< ValueType > | |
| Cstorm::modelchecker::helper::MDPSparseModelCheckingHelperReturnType< ValueType > | |
| Cstorm::pomdp::MemlessSearchOptions | |
| Cstorm::transformer::MemoryIncorporation< SparseModelType > | Incorporates Memory into the state space of the given model, that is the resulting model is the crossproduct of of the given model plus some type of memory structure |
| Cstorm::modelchecker::helper::rewardbounded::MemoryStateManager | |
| Cstorm::storage::MemoryStructure | This class represents a (deterministic) memory structure that can be used to encode certain events (such as reaching a set of goal states) into the state space of the model |
| Cstorm::storage::MemoryStructureBuilder< ValueType, RewardModelType > | |
| ►Cstorm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType > | |
| Cstorm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType > | |
| Cstorm::gbar::abstraction::prism::PrismMenuGameAbstractor< DdType, ValueType > | |
| Cstorm::gbar::abstraction::MenuGameAbstractorOptions | |
| Cstorm::gbar::abstraction::MenuGameRefiner< Type, ValueType > | |
| Cstorm::gbar::abstraction::MenuGameRefinerOptions | |
| Cstorm::counterexamples::MILPMinimalLabelSetGenerator< T > | This class provides functionality to generate a minimal counterexample to a probabilistic reachability property in terms of used labels |
| ►Cstorm::solver::MinMaxLinearEquationSolverFactory< ValueType, SolutionType > | |
| Cstorm::solver::GeneralMinMaxLinearEquationSolverFactory< ValueType, SolutionType > | |
| Cstorm::solver::MinMaxLinearEquationSolverFactory< ValueType, ValueType > | |
| Cstorm::solver::MinMaxLinearEquationSolverRequirements | |
| Cstorm::MinMaxLpSolverEnvironment | |
| Cstorm::MinMaxSolverEnvironment | |
| Cstorm::jani::Model | |
| Cstorm::ModelCheckerEnvironment | |
| Cstorm::modelchecker::helper::ModelCheckerHelper< VT, ModelRepresentation > | Helper class for solving a model checking query |
| ►Cstorm::modelchecker::helper::ModelCheckerHelper< ValueType, ModelRepresentation > | |
| ►Cstorm::modelchecker::helper::SingleValueModelCheckerHelper< ValueType, storm::models::GetModelRepresentation< DdType >::representation > | |
| Cstorm::modelchecker::helper::HybridInfiniteHorizonHelper< ValueType, DdType, Nondeterministic > | Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system |
| ►Cstorm::modelchecker::helper::SingleValueModelCheckerHelper< ValueType, storm::models::ModelRepresentation::Sparse > | |
| ►Cstorm::modelchecker::helper::SparseInfiniteHorizonHelper< ValueType, false > | |
| Cstorm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper< ValueType > | Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system |
| ►Cstorm::modelchecker::helper::SparseInfiniteHorizonHelper< ValueType, true > | |
| Cstorm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper< ValueType > | Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system |
| Cstorm::modelchecker::helper::SparseDeterministicVisitingTimesHelper< ValueType > | Helper class for computing for each state the expected number of times to visit that state assuming a given initial distribution |
| Cstorm::modelchecker::helper::SparseInfiniteHorizonHelper< ValueType, Nondeterministic > | Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system |
| Cstorm::modelchecker::helper::SparseLTLHelper< ValueType, Nondeterministic > | Helper class for LTL model checking |
| Cstorm::modelchecker::helper::lexicographic::lexicographicModelCheckerHelper< SparseModelType, ValueType, Nondeterministic > | |
| Cstorm::modelchecker::helper::SingleValueModelCheckerHelper< ValueType, ModelRepresentation > | Helper for model checking queries where we are interested in (optimizing) a single value per state |
| ►Cstorm::modelchecker::ModelCheckerHint | This class contains information that might accelerate the model checking process |
| Cstorm::modelchecker::ExplicitModelCheckerHint< ValueType > | This class contains information that might accelerate the model checking process |
| Cstorm::builder::ModelComponents< Type, ValueType > | |
| Cstorm::storage::sparse::ModelComponents< ValueType, RewardModelType > | |
| Cstorm::jani::ModelFeatures | |
| Cstorm::storage::ModelFormulasPair | |
| Cstorm::utility::ModelInstantiator< ParametricSparseModelType, ConstantSparseModelType > | This class allows efficient instantiation of the given parametric model |
| Cstorm::utility::ModelInstantiator< SparseModelType, storm::models::sparse::Ctmc< ConstantType > > | |
| Cstorm::utility::ModelInstantiator< SparseModelType, storm::models::sparse::Dtmc< ConstantType > > | |
| Cstorm::utility::ModelInstantiator< SparseModelType, storm::models::sparse::Mdp< ConstantType > > | |
| Cstorm::cli::ModelProcessingInformation | |
| ►Cstorm::solver::SmtSolver::ModelReference | The base class for all model references |
| Cstorm::solver::SmtlibSmtSolver::SmtlibModelReference | |
| Cstorm::solver::Z3SmtSolver::Z3ModelReference | |
| Cstorm::gbar::abstraction::prism::ModuleAbstractor< DdType, ValueType > | |
| ►Cstorm::settings::modules::ModuleSettings | This is the base class of the settings for a particular module |
| Cstorm::dft::settings::modules::DftGspnSettings | This class represents the settings for operations concerning the DFT to GSPN transformation |
| Cstorm::dft::settings::modules::DftIOSettings | This class represents the settings for IO operations concerning DFTs |
| Cstorm::dft::settings::modules::FaultTreeSettings | This class represents the settings for DFT model checking |
| Cstorm::settings::modules::AbstractionSettings | This class represents the settings for the abstraction procedures |
| Cstorm::settings::modules::BeliefExplorationSettings | This class represents the settings for POMDP model checking |
| Cstorm::settings::modules::BisimulationSettings | This class represents the bisimulation settings |
| Cstorm::settings::modules::BuildSettings | |
| Cstorm::settings::modules::ConversionGeneralSettings | |
| Cstorm::settings::modules::ConversionInputSettings | |
| Cstorm::settings::modules::ConversionOutputSettings | |
| Cstorm::settings::modules::CoreSettings | This class represents the core settings |
| Cstorm::settings::modules::CounterexampleGeneratorSettings | This class represents the settings for counterexample generation |
| Cstorm::settings::modules::CuddSettings | This class represents the settings for CUDD |
| Cstorm::settings::modules::DebugSettings | This class represents the debug settings |
| Cstorm::settings::modules::DerivativeSettings | This class represents the settings for Gradient Descent |
| Cstorm::settings::modules::EigenEquationSolverSettings | This class represents the settings for Eigen |
| Cstorm::settings::modules::EliminationSettings | This class represents the settings for the elimination-based procedures |
| Cstorm::settings::modules::ExplorationSettings | This class represents the exploration settings |
| Cstorm::settings::modules::FeasibilitySettings | This class represents the settings for parametric model checking |
| Cstorm::settings::modules::GSPNExportSettings | |
| Cstorm::settings::modules::GSPNSettings | |
| Cstorm::settings::modules::GameSolverSettings | This class represents the game solver settings |
| Cstorm::settings::modules::GeneralSettings | This class represents the general settings |
| Cstorm::settings::modules::GlpkSettings | This class represents the settings for glpk |
| Cstorm::settings::modules::GmmxxEquationSolverSettings | This class represents the settings for gmm++ |
| Cstorm::settings::modules::GurobiSettings | This class represents the settings for Gurobi |
| Cstorm::settings::modules::HintSettings | This class represents the model transformer settings |
| Cstorm::settings::modules::IOSettings | This class represents the markov chain settings |
| Cstorm::settings::modules::JaniExportSettings | |
| Cstorm::settings::modules::LongRunAverageSolverSettings | This class represents the LRA solver settings |
| Cstorm::settings::modules::MinMaxEquationSolverSettings | This class represents the min/max solver settings |
| Cstorm::settings::modules::ModelCheckerSettings | This class represents the general settings |
| Cstorm::settings::modules::MonotonicitySettings | This class represents the settings for monotonicity checking |
| Cstorm::settings::modules::MultiObjectiveSettings | This class represents the settings for multi-objective model checking |
| Cstorm::settings::modules::MultiplierSettings | This class represents the multiplier settings |
| Cstorm::settings::modules::NativeEquationSolverSettings | This class represents the settings for the native equation solver |
| Cstorm::settings::modules::OviSolverSettings | This class represents the settings for the optimistic value iteration solver |
| Cstorm::settings::modules::POMDPSettings | This class represents the settings for POMDP model checking |
| Cstorm::settings::modules::ParametricSettings | This class represents the settings for parametric model checking |
| Cstorm::settings::modules::PartitionSettings | This class represents the settings for parametric model checking |
| Cstorm::settings::modules::PrismExportSettings | |
| Cstorm::settings::modules::QualitativePOMDPAnalysisSettings | This class represents the settings for POMDP model checking |
| Cstorm::settings::modules::RegionSettings | This class represents the settings for parametric model checking |
| Cstorm::settings::modules::RegionVerificationSettings | |
| Cstorm::settings::modules::ResourceSettings | This class represents the resource settings |
| Cstorm::settings::modules::SamplingSettings | |
| Cstorm::settings::modules::Smt2SmtSolverSettings | This class represents the settings for interaction with SMT-LIBv2 solvers |
| Cstorm::settings::modules::SylvanSettings | This class represents the settings for Sylvan |
| Cstorm::settings::modules::TimeBoundedSolverSettings | This class represents the min/max solver settings |
| Cstorm::settings::modules::ToParametricSettings | This class represents the settings for POMDP model checking |
| Cstorm::settings::modules::TopologicalEquationSolverSettings | This class represents the settings for the native equation solver |
| Cstorm::settings::modules::TransformationSettings | This class represents the model transformer settings |
| Cstorm::analysis::MonotonicityChecker< ValueType > | |
| Cstorm::analysis::MonotonicityHelper< ValueType, ConstantType > | |
| Cstorm::parser::MonotonicityParser< VariableType > | |
| Cstorm::analysis::MonotonicityResult< VariableType > | |
| Cstorm::api::MonotonicitySetting | |
| Cstorm::modelchecker::helper::rewardbounded::MultiDimensionalRewardUnfolding< ValueType, SingleObjectiveMode > | |
| Cstorm::modelchecker::helper::rewardbounded::MultiDimensionalRewardUnfolding< ValueType, false > | |
| Cstorm::MultiObjectiveModelCheckerEnvironment | |
| ►Cstorm::solver::Multiplier< ValueType > | |
| Cstorm::solver::GmmxxMultiplier< ValueType > | |
| Cstorm::solver::NativeMultiplier< ValueType > | |
| Cstorm::MultiplierEnvironment | |
| Cstorm::solver::MultiplierFactory< ValueType > | |
| Cstorm::storage::Murmur3BitVectorHash< StateType > | |
| Cstorm::storage::Murmur3BitVectorHash< uint32_t > | |
| Cstorm::storage::Murmur3BitVectorHash< ValueType > | |
| Cstorm::NativeSolverEnvironment | |
| Cstorm::jani::JaniLocationExpander::NewIndices | |
| ►Cstorm::generator::NextStateGenerator< ValueType, StateType > | |
| Cstorm::generator::PrismNextStateGenerator< ValueType, StateType > | |
| Cstorm::generator::JaniNextStateGenerator< ValueType, StateType > | |
| Cstorm::generator::PrismNextStateGenerator< ValueType, StateType > | |
| Cstorm::generator::NextStateGenerator< ValueType, uint32_t > | |
| Cstorm::analysis::Order::Node | Nodes of the Reachability Order |
| Cstorm::generator::NondeterministicBeliefTracker< ValueType, BeliefState > | This tracker implements state estimation for POMDPs |
| Cstorm::storage::NondeterministicMemoryStructure | |
| Cstorm::storage::NondeterministicMemoryStructureBuilder | |
| Cstorm::parser::NondeterministicModelParser< ValueType, RewardValueType > | Loads a nondeterministic model (Mdp or Ctmdp) from files |
| Cstorm::parser::NondeterministicSparseTransitionParser< ValueType > | A class providing the functionality to parse the transitions of a nondeterministic model |
| Cstorm::transformer::NonMarkovianChainTransformer< ValueType, RewardModelType > | Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov automata |
| Cstorm::NullRefType | Auxiliary struct used to identify OptionalRefs that do not contain a reference |
| Cstorm::NumberTraits< ValueType > | |
| Cstorm::NumberTraits< double > | |
| Cstorm::NumberTraits< storm::RationalFunction > | |
| Cstorm::modelchecker::multiobjective::Objective< ValueType > | |
| Cstorm::pomdp::qualitative::detail::ObsActPair | |
| Cstorm::generator::ObservationDenseBeliefState< ValueType > | ObservationDenseBeliefState stores beliefs in a dense format (per observation) |
| Cstorm::generator::ObservationLabelInformation | |
| Cstorm::pomdp::ObservationTraceUnfolder< ValueType > | Observation-trace unrolling to allow model checking for monitoring |
| Cstorm::dd::Odd | |
| Cstorm::pomdp::OneShotPolicySearch< ValueType > | |
| Cstorm::logic::OperatorInformation | |
| Cstorm::solver::helper::OptimisticValueIterationHelper< ValueType, TrivialRowGrouping > | Implements Optimistic value iteration |
| Cstorm::settings::Option | This class represents one command-line option |
| Cstorm::OptionalRef< T > | Helper class that optionally holds a reference to an object of type T |
| Cstorm::OptionalRef< std::vector< ValueType > const > | |
| Cstorm::OptionalRef< storm::storage::BitVector const > | |
| Cstorm::OptionalRef< storm::storage::SparseMatrix< ValueType > const > | |
| Cstorm::OptionalRef< storm::storage::StronglyConnectedComponentDecomposition< ValueType > const > | |
| Cstorm::settings::OptionBuilder | This class provides the interface to create an option.. |
| Cstorm::builder::DdJaniModelBuilder< Type, ValueType >::Options | |
| Cstorm::builder::DdPrismModelBuilder< Type, ValueType >::Options | |
| Cstorm::builder::ExplicitModelBuilder< ValueType, RewardModelType, StateType >::Options | |
| Cstorm::counterexamples::SMTMinimalLabelSetGenerator< T >::Options | |
| Cstorm::generator::NondeterministicBeliefTracker< ValueType, BeliefState >::Options | |
| Cstorm::solver::MathsatSmtSolver::Options | A class that captures options that may be passed to the Mathsat solver |
| Cstorm::storage::BisimulationDecomposition< ModelType, BlockDataType >::Options | |
| Cstorm::analysis::Order | |
| Cstorm::jani::OrderedAssignments | |
| Cstorm::dft::storage::OrderElementsById< ValueType > | |
| Cstorm::dft::storage::OrderElementsByRank< ValueType > | |
| Cstorm::analysis::OrderExtender< ValueType, ConstantType > | |
| Cstorm::prism::OverlappingGuardAnalyser | |
| Cstorm::solver::helper::OVIBackend< ValueType, Dir, Relative > | |
| Cstorm::OviSolverEnvironment | |
| Cstorm::builder::ParallelCompositionBuilder< ValueType > | Build a parallel composition of Markov chains |
| Cstorm::builder::ParameterCreator< Type, ValueType > | |
| Cstorm::builder::ParameterCreator< Type, storm::RationalFunction > | |
| Cstorm::transformer::ParameterLifter< ParametricType, ConstantType > | This class lifts parameter choices to nondeterminism: For each row in the given matrix that considerd #par parameters, the resulting matrix will have one row group consisting of 2^#par rows |
| Cstorm::storage::ParameterRegion< ParametricType > | |
| Cstorm::storage::ParameterRegion< typename SparseModelType::ValueType > | |
| Cstorm::storage::ParameterRegion< ValueType > | |
| Cstorm::parser::ParameterRegionParser< ParametricType > | |
| Cstorm::dd::bisimulation::PartialQuotientExtractor< DdType, ValueType, ExportValueType > | |
| Cstorm::dd::bisimulation::Partition< DdType, ValueType > | |
| Cstorm::storage::bisimulation::Partition< DataType > | |
| Cstorm::storage::bisimulation::Partition< bisimulation::DeterministicBlockData > | |
| Cstorm::storage::bisimulation::Partition< BlockDataType > | |
| ►Cstorm::dd::bisimulation::PartitionRefiner< DdType, ValueType > | |
| Cstorm::dd::bisimulation::NondeterministicModelPartitionRefiner< DdType, ValueType > | |
| Cstorm::utility::ksp::Path< T > | |
| ►Cstorm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType > | Helper Class that takes a weight vector and .. |
| ►Cstorm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseMaModelType > | |
| Cstorm::modelchecker::multiobjective::StandardMaPcaaWeightVectorChecker< SparseMaModelType > | Helper Class that takes preprocessed Pcaa data and a weight vector and .. |
| ►Cstorm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseMdpModelType > | |
| Cstorm::modelchecker::multiobjective::StandardMdpPcaaWeightVectorChecker< SparseMdpModelType > | Helper Class that takes preprocessed Pcaa data and a weight vector and .. |
| Cstorm::modelchecker::multiobjective::PcaaWeightVectorChecker< SparseMaModelType > | |
| ►Cstorm::modelchecker::multiobjective::PcaaWeightVectorChecker< SparseMdpModelType > | |
| Cstorm::modelchecker::multiobjective::RewardBoundedMdpPcaaWeightVectorChecker< SparseMdpModelType > | Helper Class that takes preprocessed Pcaa data and a weight vector and .. |
| ►Cstorm::modelchecker::multiobjective::PcaaWeightVectorChecker< SparseModelType > | |
| Cstorm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseModelType > | Helper Class that takes preprocessed Pcaa data and a weight vector and .. |
| ►Cstorm::ps::PermissiveScheduler | |
| Cstorm::ps::SubMDPPermissiveScheduler< RM > | |
| ►Cstorm::ps::PermissiveSchedulerComputation< RM > | |
| Cstorm::ps::MilpPermissiveSchedulerComputation< RM > | |
| Cstorm::ps::SmtPermissiveSchedulerComputation< RM > | |
| Cstorm::ps::PermissiveSchedulerPenalties | |
| Cstorm::gbar::abstraction::PivotStateCandidatesResult< Type > | |
| Cstorm::gspn::Place | This class provides methods to store and retrieve data for a place in a gspn |
| Cstorm::logic::PlayerCoalition | |
| Cstorm::modelchecker::multiobjective::DeterministicSchedsParetoExplorer< SparseModelType, GeometryValueType >::Point | |
| Cstorm::modelchecker::multiobjective::DeterministicSchedsParetoExplorer< SparseModelType, GeometryValueType >::Pointset | |
| ►Cstorm::storage::geometry::Polytope< ValueType > | |
| Cstorm::storage::geometry::NativePolytope< ValueType > | |
| Cstorm::storage::geometry::PolytopeTree< ValueType > | Represents a set of points in Euclidean space |
| Cstorm::storage::PomdpMemory | |
| Cstorm::storage::PomdpMemoryBuilder | |
| Cstorm::transformer::PomdpMemoryUnfolder< ValueType > | |
| Cstorm::transformer::PomdpTransformationResult< ValueType > | |
| Cstorm::pomdp::modelchecker::POMDPValueBounds< ValueType > | Structure for storing values on the POMDP used for cut-offs and clipping |
| Cstorm::cli::PostprocessingIdentity | |
| Cstorm::pomdp::storage::PreprocessingPomdpValueBounds< ValueType > | Struct for storing precomputed values bounding the actual values on the POMDP |
| Cstorm::pomdp::modelchecker::PreprocessingPomdpValueBoundsModelChecker< ValueType > | |
| Cstorm::pars::PreprocessResult | |
| Cstorm::dd::bisimulation::PreservationInformation< DdType, ValueType > | |
| Cstorm::gbar::modelchecker::detail::PreviousExplicitResult< ValueType > | |
| Cstorm::solver::stateelimination::PriorityComparator | |
| Cstorm::parser::PrismParser | |
| Cstorm::converter::PrismToJaniConverterOptions | |
| ►Cstorm::transformer::Product< Model > | |
| Cstorm::transformer::DAProduct< Model > | |
| Cstorm::modelchecker::helper::lexicographic::spothelper::product_state_hash | |
| Cstorm::transformer::ProductBuilder< Model > | |
| Cstorm::modelchecker::helper::rewardbounded::ProductModel< ValueType > | |
| Cstorm::utility::ProgressMeasurement | A class that provides convenience operations to display run times |
| Cstorm::jani::Property | |
| Cstorm::jani::PropertyInterval | Property intervals as per Jani Specification |
| Cstorm::analysis::QualitativeAnalysisOnGraphs< ValueType > | |
| ►Cstorm::gbar::abstraction::QualitativeResult | |
| ►Cstorm::gbar::abstraction::ExplicitQualitativeResult | |
| Cstorm::gbar::abstraction::ExplicitQualitativeGameResult | |
| ►Cstorm::gbar::abstraction::SymbolicQualitativeResult< Type > | |
| Cstorm::gbar::abstraction::SymbolicQualitativeGameResult< Type > | |
| Cstorm::gbar::abstraction::SymbolicQualitativeMdpResult< Type > | |
| ►Cstorm::gbar::abstraction::QualitativeResultMinMax | |
| ►Cstorm::gbar::abstraction::ExplicitQualitativeResultMinMax | |
| Cstorm::gbar::abstraction::ExplicitQualitativeGameResultMinMax | |
| ►Cstorm::gbar::abstraction::SymbolicQualitativeResultMinMax< Type > | |
| Cstorm::gbar::abstraction::SymbolicQualitativeGameResultMinMax< Type > | |
| Cstorm::gbar::abstraction::SymbolicQualitativeMdpResultMinMax< Type > | |
| Cstorm::modelchecker::helper::QualitativeStateSetsReachabilityRewards | |
| Cstorm::modelchecker::helper::QualitativeStateSetsUntilProbabilities | |
| Cstorm::modelchecker::helper::rewardbounded::QuantileHelper< ModelType > | |
| Cstorm::storage::geometry::QuickHull< ValueType > | |
| Cstorm::dd::bisimulation::QuotientExtractor< DdType, ValueType, ExportValueType > | |
| Cstorm::storage::QvbsBenchmark | This class provides easy access to a benchmark of the Quantitative Verification Benchmark Set http://qcomp.org/benchmarks/ |
| Cstorm::utility::RandomProbabilityGenerator< ValueType > | |
| Cstorm::utility::RandomProbabilityGenerator< double > | |
| Cstorm::utility::RandomProbabilityGenerator< storm::RationalNumber > | |
| Ccarl::RationalFunction< P, as > | |
| Cstorm::transformer::RationalFunctionConstructor | |
| Cstorm::expressions::RationalFunctionToExpression< ValueType > | |
| Cstorm::solver::helper::RationalSearchHelper< TargetValueType, ExactValueType, ImpreciseValueType, TrivialRowGrouping > | Implements rational search |
| Cstorm::solver::RawLpConstraint< ValueType > | |
| Cstorm::storage::geometry::ReduceVertexCloud< ValueType > | |
| Cstorm::gbar::abstraction::RefinementCommand | |
| Cstorm::gbar::abstraction::RefinementPredicates | |
| Cstorm::modelchecker::multiobjective::SparsePcaaQuery< SparseModelType, GeometryValueType >::RefinementStep | |
| Cstorm::modelchecker::RegionBound< SparseModelType, ConstantType > | |
| Cstorm::modelchecker::RegionModelChecker< ParametricType > | |
| ►Cstorm::modelchecker::RegionModelChecker< SparseModelType::ValueType > | |
| Cstorm::modelchecker::SparseParameterLiftingModelChecker< SparseModelType, ImpreciseType > | |
| Cstorm::modelchecker::SparseParameterLiftingModelChecker< SparseModelType, PreciseType > | |
| ►Cstorm::modelchecker::SparseParameterLiftingModelChecker< SparseModelType, ConstantType > | Class to approximatively check a formula on a parametric model for all parameter valuations within a region It is assumed that all considered valuations are graph-preserving and well defined, i.e., |
| Cstorm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ImpreciseType > | |
| Cstorm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, PreciseType > | |
| Cstorm::modelchecker::SparseMdpParameterLiftingModelChecker< SparseModelType, ImpreciseType > | |
| Cstorm::modelchecker::SparseMdpParameterLiftingModelChecker< SparseModelType, PreciseType > | |
| Cstorm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType > | |
| Cstorm::modelchecker::SparseMdpParameterLiftingModelChecker< SparseModelType, ConstantType > | |
| ►Cstorm::modelchecker::ValidatingSparseParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType > | |
| Cstorm::modelchecker::ValidatingSparseDtmcParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType > | |
| Cstorm::modelchecker::ValidatingSparseMdpParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType > | |
| Cstorm::dft::utility::RelevantEvents | |
| Cstorm::jani::ArrayEliminatorData::Replacement | |
| Cstorm::parser::MarkovAutomatonSparseTransitionParser< ValueType >::Result | A structure representing the result of the parser |
| Cstorm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< PomdpModelType, BeliefValueType, BeliefMDPType >::Result | Struct used to store the results of the model checker |
| Cstorm::jani::AssignmentsFinder::ResultType | |
| Cstorm::jani::detail::ArrayExpressionEliminationVisitor::ResultType | |
| Cstorm::jani::JaniLocationExpander::ReturnType | |
| Cstorm::modelchecker::multiobjective::preprocessing::SparseMultiObjectiveRewardAnalysis< SparseModelType >::ReturnType | |
| Cstorm::transformer::GoalStateMerger< SparseModelType >::ReturnType | |
| Cstorm::dd::bisimulation::ReuseWrapper | |
| Cstorm::logic::RewardAccumulation | |
| Cstorm::builder::RewardModelBuilder< ValueType > | A structure that is used to keep track of a reward model currently being built |
| Cstorm::builder::RewardModelInformation | |
| Cstorm::storage::SparseMatrix< ValueType >::rows | This class represents a number of consecutive rows of the matrix |
| Cstorm::solver::helper::RSBackend< ValueType, ExactValueType, Dir > | |
| Cstorm::pars::SampleInformation< ValueType > | |
| Cstorm::storage::SccDecompositionMemoryCache | Holds temporary computation data used during the SCC decomposition algorithm |
| Cstorm::storage::SccDecompositionResult | Holds the result data of the implemented SCC decomposition algorithm |
| Cstorm::storage::Scheduler< ValueType > | This class defines which action is chosen in a particular state of a non-deterministic model |
| Cstorm::storage::SchedulerChoice< ValueType > | |
| Cstorm::storage::SchedulerClass | |
| Cstorm::solver::helper::SchedulerTrackingBackend< ValueType, Dir > | |
| Cstorm::solver::helper::SchedulerTrackingHelper< ValueType, SolutionType > | Helper class to extract optimal scheduler choices from a MinMax equation system solution |
| Cstorm::parser::JaniParser< ValueType >::Scope | |
| Cstorm::jani::JaniLocalEliminator::Session | |
| Cstorm::settings::SettingMemento | This class is used to reset the state of an option that was temporarily set to a different status |
| Cstorm::settings::SettingsManager | Provides the central API for the registration of command line options and parsing the options from the command line |
| Cstorm::dft::modelchecker::SFTBDDChecker | Main class for the SFTBDDChecker |
| Cstorm::dft::adapters::SFTBDDPropertyFormulaAdapter | |
| Cstorm::dft::transformations::SftToBddTransformator< ValueType > | Transformator for DFT -> BDD |
| Cstorm::utility::ksp::ShortestPathsGenerator< T > | |
| Cstorm::utility::resources::SignalInformation | |
| Cstorm::dd::bisimulation::Signature< DdType, ValueType > | |
| Cstorm::dd::bisimulation::SignatureComputer< DdType, ValueType > | |
| Cstorm::dd::bisimulation::SignatureIterator< DdType, ValueType > | |
| Cstorm::dd::bisimulation::SignatureRefiner< DdType, ValueType > | |
| Cstorm::utility::string::SimilarStrings | |
| Cstorm::expressions::SimpleValuationPointerCompare | A helper class that can be used as the comparison functor wrt |
| Cstorm::expressions::SimpleValuationPointerHash | A helper class that can pe used as the hash functor for data structures that need to hash valuations given via pointers |
| Cstorm::expressions::SimpleValuationPointerLess | A helper class that can be used as the comparison functor wrt |
| Cstorm::adapters::Smt2ExpressionAdapter | |
| ►Cstorm::dft::modelchecker::SmtConstraint | |
| Cstorm::dft::modelchecker::And | |
| Cstorm::dft::modelchecker::BetweenValues | |
| Cstorm::dft::modelchecker::FalseCountIsEqualConstant | |
| Cstorm::dft::modelchecker::IfThenElse | |
| Cstorm::dft::modelchecker::Iff | |
| Cstorm::dft::modelchecker::Implies | |
| Cstorm::dft::modelchecker::IsBoolValue | |
| Cstorm::dft::modelchecker::IsConstantValue | |
| Cstorm::dft::modelchecker::IsEqual | |
| Cstorm::dft::modelchecker::IsGreaterConstant | |
| Cstorm::dft::modelchecker::IsGreaterEqual | |
| Cstorm::dft::modelchecker::IsGreaterEqualConstant | |
| Cstorm::dft::modelchecker::IsLess | |
| Cstorm::dft::modelchecker::IsLessConstant | |
| Cstorm::dft::modelchecker::IsLessEqual | |
| Cstorm::dft::modelchecker::IsLessEqualConstant | |
| Cstorm::dft::modelchecker::IsMaximum | |
| Cstorm::dft::modelchecker::IsMinimum | |
| Cstorm::dft::modelchecker::IsNotConstantValue | |
| Cstorm::dft::modelchecker::IsTrue | |
| Cstorm::dft::modelchecker::IsUnequal | |
| Cstorm::dft::modelchecker::Or | |
| Cstorm::dft::modelchecker::PairwiseDifferent | |
| Cstorm::dft::modelchecker::Sorted | |
| Cstorm::dft::modelchecker::TrueCountIsConstantValue | |
| Cstorm::dft::modelchecker::TrueCountIsLessConstant | |
| Cstorm::counterexamples::SMTMinimalLabelSetGenerator< T > | This class provides functionality to generate a minimal counterexample to a probabilistic reachability property in terms of used labels |
| ►Cstorm::solver::SmtSolver | An interface that captures the functionality of an SMT solver |
| Cstorm::solver::MathsatSmtSolver | |
| Cstorm::solver::SmtlibSmtSolver | This class represents an SMT-LIBv2 conforming solver |
| Cstorm::solver::Z3SmtSolver | |
| ►Cstorm::utility::solver::SmtSolverFactory | |
| Cstorm::utility::solver::MathsatSmtSolverFactory | |
| Cstorm::utility::solver::Z3SmtSolverFactory | |
| Cstorm::solver::SolveGoal< ValueType, SolutionType > | |
| Cstorm::SolverEnvironment | |
| Cstorm::solver::SolverRequirement | |
| Cstorm::modelchecker::helper::SolverRequirementsData< ValueType > | |
| Cstorm::solver::helper::SoundValueIterationHelper< ValueType, TrivialRowGrouping > | Implements sound value iteration |
| Cstorm::dft::modelchecker::SpareAndChildPair | |
| Cstorm::generator::SparseBeliefState< ValueType > | SparseBeliefState stores beliefs in a sparse format |
| ►Cstorm::modelchecker::multiobjective::SparseCbQuery< SparseModelType > | |
| Cstorm::modelchecker::multiobjective::SparseCbAchievabilityQuery< SparseModelType > | |
| Cstorm::parser::SparseChoiceLabelingParser | A class providing the functionality to parse a choice labeling |
| Cstorm::modelchecker::helper::SparseCtmcCslHelper | |
| Cstorm::derivative::SparseDerivativeInstantiationModelChecker< FunctionType, ConstantType > | |
| Cstorm::modelchecker::helper::SparseDeterministicStepBoundedHorizonHelper< ValueType > | |
| Cstorm::modelchecker::helper::SparseDtmcPrctlHelper< ValueType, RewardModelType > | |
| Cstorm::modelchecker::region::SparseDtmcRegionModelChecker< ParametricModelType, ConstantType > | |
| ►Cstorm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > | Class to efficiently check a formula on a parametric model with different parameter instantiations |
| Cstorm::modelchecker::SparseCtmcInstantiationModelChecker< SparseModelType, ConstantType > | Class to efficiently check a formula on a parametric model with different parameter instantiations |
| Cstorm::modelchecker::SparseDtmcInstantiationModelChecker< SparseModelType, ConstantType > | Class to efficiently check a formula on a parametric model with different parameter instantiations |
| Cstorm::modelchecker::SparseMdpInstantiationModelChecker< SparseModelType, ConstantType > | Class to efficiently check a formula on a parametric model with different parameter instantiations |
| Cstorm::parser::SparseItemLabelingParser | This class can be used to parse a labeling file |
| Cstorm::modelchecker::helper::internal::SparseLTLSchedulerHelper< ValueType, Nondeterministic > | Helper class for scheduler construction in LTL model checking |
| Cstorm::modelchecker::helper::SparseMarkovAutomatonCslHelper | |
| Cstorm::storage::SparseMatrix< ValueType > | A class that holds a possibly non-square matrix in the compressed row storage format |
| Cstorm::storage::SparseMatrix< carl::RationalFunction > | |
| Cstorm::storage::SparseMatrix< ConstantType > | |
| Cstorm::storage::SparseMatrix< FunctionType > | |
| Cstorm::storage::SparseMatrix< storm::storage::sparse::state_type > | |
| Cstorm::storage::SparseMatrixBuilder< ValueType > | A class that can be used to build a sparse matrix by adding value by value |
| Cstorm::modelchecker::helper::SparseMdpEndComponentInformation< ValueType > | |
| Cstorm::modelchecker::helper::SparseMdpHintType< ValueType > | |
| Cstorm::modelchecker::helper::SparseMdpPrctlHelper< ValueType, SolutionType > | |
| Cstorm::storage::SparseModelMemoryProduct< ValueType, RewardModelType > | This class builds the product of the given sparse model and the given memory structure |
| Cstorm::storage::SparseModelNondeterministicMemoryProduct< SparseModelType > | |
| Cstorm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor< SparseModelType > | |
| Cstorm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessorResult< SparseModelType > | |
| Cstorm::modelchecker::multiobjective::preprocessing::SparseMultiObjectiveRewardAnalysis< SparseModelType > | |
| Cstorm::modelchecker::helper::SparseNondeterministicStepBoundedHorizonHelper< ValueType > | |
| ►Cstorm::transformer::SparseParametricModelSimplifier< SparseModelType > | This class performs different steps to simplify the given (parametric) model |
| Cstorm::transformer::SparseParametricDtmcSimplifier< SparseModelType > | This class performs different steps to simplify the given (parametric) model |
| Cstorm::transformer::SparseParametricMdpSimplifier< SparseModelType > | This class performs different steps to simplify the given (parametric) model |
| ►Cstorm::modelchecker::multiobjective::SparsePcaaQuery< SparseModelType, GeometryValueType > | |
| Cstorm::modelchecker::multiobjective::SparsePcaaAchievabilityQuery< SparseModelType, GeometryValueType > | |
| Cstorm::modelchecker::multiobjective::SparsePcaaParetoQuery< SparseModelType, GeometryValueType > | |
| Cstorm::modelchecker::multiobjective::SparsePcaaQuantitativeQuery< SparseModelType, GeometryValueType > | |
| Cstorm::parser::SparseStateRewardParser< ValueType > | A class providing the functionality to parse a the state rewards of a model |
| Cstorm::parser::SpiritErrorHandler | |
| Cstorm::models::sparse::StandardRewardModel< CValueType > | |
| Cstorm::models::symbolic::StandardRewardModel< Type, ValueType > | |
| Cstorm::storage::StateActionPair | |
| Cstorm::storage::StateActionTarget | |
| Cstorm::builder::StateAndChoiceInformationBuilder | This class collects information regarding the states and choices during model building |
| ►Cstorm::models::sparse::StateAnnotation | |
| Cstorm::storage::sparse::StateValuations | |
| Cstorm::generator::StateBehavior< ValueType, StateType > | |
| ►Cstorm::storage::StateBlock | |
| Cstorm::storage::StronglyConnectedComponent | This class represents a strongly connected component, i.e., a set of states such that every state can reach every other state |
| Cstorm::modelchecker::exploration_detail::StateGeneration< StateType, ValueType > | |
| ►Cstorm::solver::stateelimination::StatePriorityQueue | |
| Cstorm::solver::stateelimination::DynamicStatePriorityQueue< ValueType > | |
| Cstorm::solver::stateelimination::StaticStatePriorityQueue | |
| ►Cstorm::gbar::abstraction::StateSet | |
| Cstorm::gbar::abstraction::SymbolicStateSet< Type > | |
| Cstorm::pomdp::analysis::FormulaInformation::StateSet | Characterizes a certain set of states |
| Cstorm::gbar::abstraction::StateSetAbstractor< DdType, ValueType > | |
| Cstorm::storage::sparse::StateStorage< StateType > | |
| Cstorm::storage::sparse::StateStorage< uint32_t > | |
| Cstorm::storage::sparse::StateValuations::StateValuation | |
| Cstorm::storage::sparse::StateValuationsBuilder | |
| Cstorm::storage::sparse::StateValuations::StateValueIterator | |
| Cstorm::storage::sparse::StateValuations::StateValueIteratorRange | |
| Cstorm::transformer::StateWithRow | |
| ►Cboost::static_visitor | |
| Cstorm::dft::modelchecker::DFTModelChecker< ValueType >::ResultOutputVisitor | |
| Cstorm::modelchecker::exploration_detail::Statistics< StateType, ValueType > | |
| Cstorm::pomdp::IterativePolicySearch< ValueType >::Statistics | |
| Cstorm::utility::Stopwatch | A class that provides convenience operations to display run times |
| Cstorm::StormVersion | |
| ►Cboost::spirit::qi::strict_real_policies | |
| Cstorm::parser::RationalPolicies< NumberType > | |
| Cstorm::storage::StronglyConnectedComponentDecompositionOptions | |
| Cstorm::SubEnvironment< EnvironmentType > | |
| Cstorm::SubEnvironment< storm::EigenSolverEnvironment > | |
| Cstorm::SubEnvironment< storm::GameSolverEnvironment > | |
| Cstorm::SubEnvironment< storm::GmmxxSolverEnvironment > | |
| Cstorm::SubEnvironment< storm::InternalEnvironment > | |
| Cstorm::SubEnvironment< storm::LongRunAverageSolverEnvironment > | |
| Cstorm::SubEnvironment< storm::MinMaxLpSolverEnvironment > | |
| Cstorm::SubEnvironment< storm::MinMaxSolverEnvironment > | |
| Cstorm::SubEnvironment< storm::ModelCheckerEnvironment > | |
| Cstorm::SubEnvironment< storm::MultiObjectiveModelCheckerEnvironment > | |
| Cstorm::SubEnvironment< storm::MultiplierEnvironment > | |
| Cstorm::SubEnvironment< storm::NativeSolverEnvironment > | |
| Cstorm::SubEnvironment< storm::OviSolverEnvironment > | |
| Cstorm::SubEnvironment< storm::SolverEnvironment > | |
| Cstorm::SubEnvironment< storm::TimeBoundedSolverEnvironment > | |
| Cstorm::SubEnvironment< storm::TopologicalSolverEnvironment > | |
| Cstorm::storage::geometry::SubsetEnumerator< DataType > | This class can be used to enumerate all k-sized subsets of {0,...,n-1} |
| Cstorm::transformer::SubsystemBuilderOptions | |
| Cstorm::transformer::SubsystemBuilderReturnType< ValueType, RewardModelType > | |
| Cstorm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::SuccessorObservationInformation | |
| Cstorm::solver::helper::SVIBackend< ValueType, Dir, Stage, TrivialRowGrouping > | |
| Cstorm::solver::helper::SoundValueIterationHelper< ValueType, TrivialRowGrouping >::SVIData | |
| CSylvan | |
| Cstorm::dft::storage::SylvanBddManager | Simple Manager for Sylvan |
| Cstorm::dd::SylvanMTBDDPairHash | |
| Cstorm::dd::SylvanMTBDDPairLess | |
| Cstorm::transformer::SymbolicCtmcToSparseCtmcTransformer< Type, ValueType > | |
| Cstorm::modelchecker::helper::SymbolicDtmcPrctlHelper< DdType, ValueType > | |
| Cstorm::transformer::SymbolicDtmcToSparseDtmcTransformer< Type, ValueType > | |
| ►Cstorm::solver::SymbolicEquationSolver< DdType, ValueType > | |
| Cstorm::solver::SymbolicLinearEquationSolver< DdType, double > | |
| ►Cstorm::solver::SymbolicLinearEquationSolver< DdType, ValueType > | An interface that represents an abstract symbolic linear equation solver |
| Cstorm::solver::SymbolicEliminationLinearEquationSolver< DdType, ValueType > | |
| Cstorm::solver::SymbolicNativeLinearEquationSolver< DdType, ValueType > | An interface that represents an abstract symbolic linear equation solver |
| Cstorm::solver::SymbolicEquationSolver< DdType, double > | |
| ►Cstorm::solver::SymbolicEquationSolver< DdType, ValueType > | |
| Cstorm::solver::SymbolicMinMaxLinearEquationSolver< DdType, ValueType > | An interface that represents an abstract symbolic linear equation solver |
| ►Cstorm::utility::graph::SymbolicGameProb01Result< Type > | |
| Cstorm::gbar::abstraction::SymbolicQualitativeGameResult< Type > | |
| Cstorm::solver::SymbolicGameSolver< Type, ValueType > | An interface that represents an abstract symbolic game solver |
| Cstorm::solver::SymbolicGameSolverFactory< Type, ValueType > | |
| Cstorm::cli::SymbolicInput | |
| ►Cstorm::solver::SymbolicLinearEquationSolverFactory< DdType, ValueType > | |
| Cstorm::solver::GeneralSymbolicLinearEquationSolverFactory< DdType, ValueType > | |
| Cstorm::solver::SymbolicEliminationLinearEquationSolverFactory< DdType, ValueType > | |
| Cstorm::solver::SymbolicNativeLinearEquationSolverFactory< DdType, ValueType > | |
| Cstorm::transformer::SymbolicMaToSparseMaTransformer< Type, ValueType > | |
| Cstorm::modelchecker::helper::SymbolicMdpPrctlHelper< DdType, ValueType > | |
| Cstorm::transformer::SymbolicMdpToSparseMdpTransformer< Type, ValueType > | |
| ►Cstorm::solver::SymbolicMinMaxLinearEquationSolverFactory< DdType, ValueType > | |
| Cstorm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory< DdType, ValueType > | |
| Cstorm::storage::SymbolicModelDescription | |
| Cstorm::gbar::abstraction::SymbolicMostProbablePathsResult< Type, ValueType > | |
| Cstorm::gbar::abstraction::SymbolicPivotStateResult< Type, ValueType > | |
| Cstorm::gbar::abstraction::SymbolicQuantitativeGameResult< Type, ValueType > | |
| Cstorm::gbar::abstraction::SymbolicQuantitativeGameResultMinMax< Type, ValueType > | |
| Cstorm::dft::utility::SymmetryFinder< ValueType > | |
| Cstorm::jani::SynchronizationVector | |
| Cstorm::jani::SynchronizationVectorLexicographicalLess | |
| Cstorm::builder::DdPrismModelBuilder< Type, ValueType >::SystemResult< Type, ValueType > | |
| Cstorm::jani::TemplateEdge | |
| Cstorm::jani::TemplateEdgeDestination | |
| Cstorm::builder::TerminalStates | |
| ►Cstorm::solver::TerminationCondition< ValueType > | |
| Cstorm::derivative::SignedGradientDescentTerminationCondition< ValueType > | |
| Cstorm::solver::NoTerminationCondition< ValueType > | |
| ►Cstorm::solver::TerminateIfFilteredSumExceedsThreshold< ValueType > | |
| Cstorm::solver::TerminateIfFilteredExtremumBelowThreshold< ValueType > | |
| Cstorm::solver::TerminateIfFilteredExtremumExceedsThreshold< ValueType > | |
| ►Ctesting::Test | |
| CAssumptionCheckerTest | |
| CAssumptionMakerTest | |
| CBeliefExplorationAPITest< TestType > | |
| CBinaryDtmcTransformer | |
| CDd< TestType > | |
| CDdPrismModelBuilderTest< TestType > | |
| CExplicitPrismModelBuilderTest | |
| CFullySymbolicGameSolverTest< TestType > | |
| CGameBasedDtmcModelCheckerTest< TestType > | |
| CGameBasedMdpModelCheckerTest< TestType > | |
| CGraphTestAR< TestType > | |
| CGraphTestExplicit | |
| CGraphTestSymbolic< TestType > | |
| CJaniLocalElimination | |
| CKSPTest | |
| CMonotonicityCheckerTest | |
| CMonotonicityHelperTest | |
| COrderExtenderTest | |
| CPrismMenuGame< TestType > | |
| CQualitativeAnalysis | |
| CSparseDtmcMultiDimensionalRewardUnfoldingTest | |
| CSparseExplorationModelCheckerTest | |
| CSparseMaCbMultiObjectiveModelCheckerTest | |
| CSparseMdpCbMultiObjectiveModelCheckerTest | |
| CSparseMdpMultiDimensionalRewardUnfoldingTest | |
| CSylvanDd< TestType > | |
| CSymbolicModelBisimulationDecomposition< TestType > | |
| CTimeTravelling | |
| Cstorm::logic::TimeBound | |
| Cstorm::TimeBoundedSolverEnvironment | |
| Cstorm::logic::TimeBoundReference | |
| Cstorm::transformer::TimeTravelling | |
| Cstorm::expressions::ToCppTranslationOptions | |
| Cstorm::prism::ToJaniConverter | |
| Cstorm::TopologicalSolverEnvironment | |
| Cstorm::generator::TransientVariableData< VariableType > | |
| Cstorm::generator::TransientVariableInformation< ValueType > | |
| Cstorm::generator::TransientVariableValuation< ValueType > | |
| ►Cstorm::gspn::Transition | This class represents a transition in a gspn |
| Cstorm::gspn::ImmediateTransition< WeightType > | |
| Cstorm::gspn::TimedTransition< RateType > | |
| Cstorm::gspn::TransitionPartition | |
| Cstorm::storage::BeliefManager< PomdpType, BeliefValueType, StateType >::Triangulation | |
| Cstorm::expressions::Type | |
| Cstorm::jani::elimination_actions::UnfoldDependencyGraph | |
| Cstorm::modelchecker::helper::UnifPlusHelper< ValueType > | |
| Cstorm::analysis::UniqueObservationStates< ValueType > | |
| ►Cstd::unordered_set | |
| Cstorm::jani::TemplateEdgeContainer | |
| Cstorm::gbar::abstraction::ValidBlockAbstractor< DdType > | |
| ►Cstorm::expressions::Valuation | The base class of all valuations of variables |
| Cstorm::expressions::SimpleValuation | A simple implementation of the valuation interface |
| Cstorm::solver::helper::ValueIterationHelper< ValueType, TrivialRowGrouping, SolutionType > | |
| Cstorm::solver::helper::ValueIterationOperator< ValueType, TrivialRowGrouping, SolutionType > | This class represents the Value Iteration Operator (also known as Bellman operator) |
| Cstorm::parser::ValueParser< ValueType > | Parser for values according to their ValueType |
| Cstorm::expressions::Variable | |
| Cstorm::jani::Variable | |
| Cstorm::expressions::LinearCoefficientVisitor::VariableCoefficients | |
| Cstorm::jani::elimination_actions::UnfoldDependencyGraph::VariableGroup | |
| Cstorm::jani::elimination_actions::UnfoldDependencyGraph::VariableInfo | |
| Cstorm::generator::VariableInformation | |
| Cstorm::expressions::VariableIterator | |
| Cstorm::jani::VariableSet | |
| Cstorm::gbar::abstraction::VariableSetHash | |
| Cstorm::jani::VariablesToConstantsTransformer | |
| Cstorm::utility::parametric::VariableType< FunctionType > | Access the type of variables from a given function type |
| Cstorm::utility::vector::VectorHash< ValueType > | |
| Cstorm::utility::VectorHelper< ValueType > | |
| Cstorm::solver::helper::VIOperatorBackend< ValueType, Dir, Relative > | |
| Cstorm::modelchecker::multiobjective::VisitingTimesHelper< ValueType > | Provides helper functions for computing bounds on the expected visiting times |
| Cstorm::derivative::GradientDescentInstantiationSearcher< FunctionType, ConstantType >::VisualizationPoint | A point in the Gradient Descent walk, recorded if recordRun is set to true in the constructor (false by default) |
| Cstorm::modelchecker::multiobjective::WeightVectorCheckerFactory< ModelType > | |
| Cstorm::pomdp::WinningRegion | |
| Cstorm::pomdp::WinningRegionQueryInterface< ValueType > | |
1.9.8