| ►Ncarl | |
| CCache | |
| CFactorizedPolynomial | |
| CInterval | |
| CRationalFunction | |
| ►NEigen | |
| CNumTraits< storm::RationalNumber > | |
| ►Nstd | |
| Chash< Eigen::Matrix< ValueType, Eigen::Dynamic, 1 > > | |
| Chash< std::pair< uint_fast64_t, uint_fast64_t > > | |
| Chash< storm::dd::InternalBdd< storm::dd::DdType::CUDD > > | |
| Chash< storm::dd::InternalBdd< storm::dd::DdType::Sylvan > > | |
| Chash< storm::generator::ObservationDenseBeliefState< T > > | |
| Chash< storm::generator::SparseBeliefState< T > > | |
| Chash< storm::storage::BitVector > | |
| Chash< storm::storage::StateActionPair > | |
| Chash< storm::storage::StateActionTarget > | |
| ►Nstorm | LabParser.cpp |
| ►Nadapters | |
| CAddExpressionAdapter | |
| CDereferenceIteratorAdapter | |
| CDereferencer | |
| CEigenAdapter | |
| CGmmxxAdapter | |
| CSmt2ExpressionAdapter | |
| ►Nanalysis | |
| CAssumptionChecker | |
| CAssumptionMaker | |
| CConstraintCollector | Class to collect constraints on parametric Markov chains |
| CConstraintType | |
| CConstraintType< ValueType, typename std::enable_if< std::is_same< storm::RationalFunction, ValueType >::value >::type > | |
| CLocalMonotonicityResult | |
| CMonotonicityChecker | |
| CMonotonicityHelper | |
| CMonotonicityResult | |
| ►COrder | |
| CNode | Nodes of the Reachability Order |
| COrderExtender | |
| CQualitativeAnalysisOnGraphs | |
| CUniqueObservationStates | |
| ►Napi | |
| CMonotonicitySetting | |
| ►Nautomata | |
| CAcceptanceCondition | |
| CAPSet | |
| CDeterministicAutomaton | |
| CHOAConsumerDA | |
| ►CHOAConsumerDAHeader | |
| Cheader_parsing_done | |
| CHOAHeader | |
| CLTL2DeterministicAutomaton | |
| ►Nbuilder | |
| ►CBeliefMdpExplorer | |
| CSuccessorObservationInformation | |
| CBuilderOptions | |
| ►CCombinedEdgesSystemComposer | |
| CActionDd | |
| CActionIdentification | |
| CActionIdentificationHash | |
| CActionInstantiation | |
| CActionInstantiationHash | |
| CAutomatonDd | |
| CEdgeDd | |
| CComposerResult | |
| CCompositionVariableCreator | |
| CCompositionVariables | |
| ►CDdJaniModelBuilder | |
| COptions | |
| ►CDdPrismModelBuilder | |
| CGenerationInformation | |
| COptions | |
| CSystemResult | |
| CEdgeDestinationDd | |
| ►CExplicitModelBuilder | |
| COptions | |
| CExplicitStateLookup | |
| CJaniGSPNBuilder | |
| CLabelOrExpression | |
| CModelComponents | |
| CModuleComposer | |
| CParallelCompositionBuilder | Build a parallel composition of Markov chains |
| CParameterCreator | |
| CParameterCreator< Type, storm::RationalFunction > | |
| CRewardModelBuilder | A structure that is used to keep track of a reward model currently being built |
| CRewardModelInformation | |
| CStateAndChoiceInformationBuilder | This class collects information regarding the states and choices during model building |
| CSystemComposer | |
| CTerminalStates | |
| ►Ncli | |
| CModelProcessingInformation | |
| CPostprocessingIdentity | |
| CSymbolicInput | |
| ►Nconverter | |
| CJaniConversionOptions | |
| CPrismToJaniConverterOptions | |
| ►Ncounterexamples | |
| CCounterexample | |
| CHighLevelCounterexample | |
| CMILPMinimalLabelSetGenerator | This class provides functionality to generate a minimal counterexample to a probabilistic reachability property in terms of used labels |
| CPathCounterexample | |
| ►CSMTMinimalLabelSetGenerator | This class provides functionality to generate a minimal counterexample to a probabilistic reachability property in terms of used labels |
| CCexInput | |
| CGeneratorStats | |
| COptions | |
| ►Ndd | |
| ►Nbisimulation | |
| CInternalRepresentativeComputer | |
| CInternalRepresentativeComputer< storm::dd::DdType::CUDD > | |
| CInternalRepresentativeComputer< storm::dd::DdType::Sylvan > | |
| CInternalRepresentativeComputerBase | |
| CInternalSignatureRefiner | |
| CInternalSignatureRefiner< storm::dd::DdType::CUDD, ValueType > | |
| CInternalSignatureRefiner< storm::dd::DdType::Sylvan, ValueType > | |
| CInternalSignatureRefinerOptions | |
| CInternalSparseQuotientExtractor | |
| CInternalSparseQuotientExtractor< storm::dd::DdType::CUDD, ValueType > | |
| CInternalSparseQuotientExtractor< storm::dd::DdType::Sylvan, ValueType, ExportValueType > | |
| CInternalSparseQuotientExtractorBase | |
| CInternalSylvanSignatureRefinerBase | |
| CNondeterministicModelPartitionRefiner | |
| CPartialQuotientExtractor | |
| CPartition | |
| CPartitionRefiner | |
| CPreservationInformation | |
| CQuotientExtractor | |
| CReuseWrapper | |
| CSignature | |
| CSignatureComputer | |
| CSignatureIterator | |
| CSignatureRefiner | |
| ►CAdd | |
| CMatrixAndLabeling | Converts the ADD to a row-grouped (sparse) matrix |
| CAddIterator | |
| CAddIterator< DdType::CUDD, ValueType > | |
| CAddIterator< DdType::Sylvan, ValueType > | |
| CBdd | |
| CBisimulationDecomposition | |
| CCuddPointerPairHash | |
| CDd | |
| CDdManager | |
| CDdMetaVariable | |
| CFromVectorHelper | |
| CFromVectorHelper< LibraryType, storm::RationalFunction > | |
| CInternalAdd | |
| CInternalAdd< DdType::CUDD, ValueType > | |
| CInternalAdd< DdType::Sylvan, ValueType > | |
| CInternalBdd | |
| CInternalBdd< DdType::CUDD > | |
| CInternalBdd< DdType::Sylvan > | |
| CInternalDdManager | |
| CInternalDdManager< DdType::CUDD > | |
| CInternalDdManager< DdType::Sylvan > | |
| COdd | |
| CSylvanMTBDDPairHash | |
| CSylvanMTBDDPairLess | |
| ►Nderivative | |
| ►CGradientDescentInstantiationSearcher | |
| CVisualizationPoint | A point in the Gradient Descent walk, recorded if recordRun is set to true in the constructor (false by default) |
| CSignedGradientDescentTerminationCondition | |
| CSparseDerivativeInstantiationModelChecker | |
| ►Ndft | |
| ►Nadapters | |
| CSFTBDDPropertyFormulaAdapter | |
| ►Nbuilder | |
| CDFTBuilder | |
| CDFTExplorationHeuristic | General super class for approximation heuristics |
| CDFTExplorationHeuristicBoundDifference | |
| CDFTExplorationHeuristicDepth | |
| CDFTExplorationHeuristicProbability | |
| CExplicitDFTModelBuilder | Build a Markov chain from DFT |
| ►Ngenerator | |
| CDftNextStateGenerator | Next state generator for DFTs |
| ►Nmodelchecker | |
| CAnd | |
| CBetweenValues | |
| CDependencyPair | |
| CDFTASFChecker | |
| ►CDFTModelChecker | Analyser for DFTs |
| CResultOutputVisitor | |
| CDftModularizationChecker | DFT analysis via modularization |
| CFalseCountIsEqualConstant | |
| CIff | |
| CIfThenElse | |
| CImplies | |
| CIsBoolValue | |
| CIsConstantValue | |
| CIsEqual | |
| CIsGreaterConstant | |
| CIsGreaterEqual | |
| CIsGreaterEqualConstant | |
| CIsLess | |
| CIsLessConstant | |
| CIsLessEqual | |
| CIsLessEqualConstant | |
| CIsMaximum | |
| CIsMinimum | |
| CIsNotConstantValue | |
| CIsTrue | |
| CIsUnequal | |
| COr | |
| CPairwiseDifferent | |
| CSFTBDDChecker | Main class for the SFTBDDChecker |
| CSmtConstraint | |
| CSorted | |
| CSpareAndChildPair | |
| CTrueCountIsConstantValue | |
| CTrueCountIsLessConstant | |
| ►Nparser | |
| CDFTGalileoParser | Parser for DFT in the Galileo format |
| CDFTJsonParser | Parser for DFT in custom JSON format |
| ►Nsettings | |
| ►Nmodules | |
| CDftGspnSettings | This class represents the settings for operations concerning the DFT to GSPN transformation |
| CDftIOSettings | This class represents the settings for IO operations concerning DFTs |
| CFaultTreeSettings | This class represents the settings for DFT model checking |
| ►Nsimulator | |
| CBECountImportanceFunction | Importance function based on counting the number of currently failed BEs |
| CDFTTraceSimulator | Simulator for DFTs |
| CImportanceFunction | Abstract class for importance functions |
| ►Nstorage | |
| ►Nelements | |
| CBEConst | BE which is either constant failed or constant failsafe |
| CBEErlang | BE with Erlang failure distribution |
| CBEExponential | BE with exponential failure distribution |
| CBELogNormal | BE with log-normal failure distribution |
| CBEProbability | BE with constant (Bernoulli) failure probability distribution |
| CBESamples | BE where the failure distribution is defined by samples |
| CBEWeibull | BE with Weibull failure distribution |
| CDFTAnd | AND gate |
| CDFTBE | Abstract base class for basic events (BEs) in DFTs |
| CDFTChildren | Abstract base class for a DFT element with children |
| CDFTDependency | Dependency gate with probability p |
| CDFTElement | Abstract base class for DFT elements |
| CDFTGate | Abstract base class for gates |
| CDFTMutex | Mutex restriction (MUTEX) |
| CDFTOr | OR gate |
| CDFTPand | Priority AND (PAND) gate |
| CDFTPor | Priority OR (POR) gate |
| CDFTRestriction | Abstract base class for restrictions |
| CDFTSeq | Sequence enforcer (SEQ) |
| CDFTSpare | SPARE gate |
| CDFTVot | VOT gate with threshold k |
| CBEColourClass | |
| CBijectionCandidates | |
| CBucketPriorityQueue | Priority queue based on buckets |
| CDFT | Represents a Dynamic Fault Tree |
| CDFTColouring | |
| CDFTElementSort | |
| CDftIndependentModule | Represents an independent module/subtree |
| CDFTIsomorphismCheck | Saves isomorphism between subtrees |
| CDftJsonExporter | Exports a DFT into the JSON format |
| CDFTLayoutInfo | |
| CDftModule | Represents a module/subtree in a DFT |
| CDFTState | |
| CDFTStateGenerationInfo | |
| CDFTStateSpaceGenerationQueues | |
| CDftSymmetries | |
| ►CFailableElements | Handling of currently failable elements (BEs) either due to their own failure or because of dependencies |
| Cconst_iterator | Iterator for failable elements |
| CGateGroupToHash | |
| COrderElementsById | |
| COrderElementsByRank | |
| CSylvanBddManager | Simple Manager for Sylvan |
| ►Ntransformations | |
| CDftInstantiator | Instantiator to yield a concrete DFT from a parametric DFT (with parametric failure rates) |
| CDftToGspnTransformator | Transformator for DFT -> GSPN |
| CDftTransformer | Transformer for operations on DFT |
| CSftToBddTransformator | Transformator for DFT -> BDD |
| ►Nutility | |
| CDftModularizer | Find modules (independent subtrees) in DFT |
| CDftValidator | |
| CFailureBoundFinder | |
| CFDEPConflictFinder | |
| CRelevantEvents | |
| CSymmetryFinder | |
| ►Nexceptions | |
| CBaseException | This class represents the base class of all exception classes |
| ►Nexpressions | |
| CArrayAccessExpression | Represents an access to an array |
| CArrayExpression | The base class of all array expressions |
| CArrayType | |
| CBaseExpression | The base class of all expression classes |
| CBaseType | |
| CBinaryBooleanFunctionExpression | |
| CBinaryExpression | The base class of all binary expressions |
| CBinaryNumericalFunctionExpression | |
| CBinaryRelationExpression | |
| CBitVectorType | |
| CBooleanLiteralExpression | |
| CBooleanType | |
| CChangeManagerVisitor | |
| CCheckIfThenElseGuardVisitor | |
| CCompiledExpression | |
| CConstructorArrayExpression | 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 |
| CEquivalenceChecker | |
| CErrorType | |
| CExpression | |
| CExpressionEvaluator | |
| CExpressionEvaluator< double > | |
| CExpressionEvaluatorBase | |
| CExpressionEvaluatorWithVariableToExpressionMap | |
| CExpressionManager | This class is responsible for managing a set of typed variables and all expressions using these variables |
| CExpressionVisitor | |
| CExprtkCompiledExpression | |
| CExprtkExpressionEvaluator | |
| CExprtkExpressionEvaluatorBase | |
| CFullPredicateSplitter | |
| CFunctionCallExpression | Represents an array with a given list of elements |
| CIfThenElseExpression | |
| CIntegerLiteralExpression | |
| CIntegerType | |
| CJaniExpressionSubstitutionVisitor | |
| CJaniExpressionVisitor | |
| CJaniReduceNestingExpressionVisitor | |
| CJaniSyntacticalEqualityCheckVisitor | |
| ►CLinearCoefficientVisitor | |
| CVariableCoefficients | |
| CLinearityCheckVisitor | |
| CPredicateExpression | The base class of all binary expressions |
| CRationalFunctionToExpression | |
| CRationalLiteralExpression | |
| CRationalType | |
| CReduceNestingVisitor | |
| CRestrictSyntaxVisitor | |
| CSimpleValuation | A simple implementation of the valuation interface |
| CSimpleValuationPointerCompare | A helper class that can be used as the comparison functor wrt |
| CSimpleValuationPointerHash | A helper class that can pe used as the hash functor for data structures that need to hash valuations given via pointers |
| CSimpleValuationPointerLess | A helper class that can be used as the comparison functor wrt |
| CSubstitutionVisitor | |
| CSyntacticalEqualityCheckVisitor | |
| CToCppTranslationOptions | |
| CToCppVisitor | |
| CToDiceStringVisitor | |
| CToExprtkStringVisitor | |
| CToRationalNumberVisitor | |
| CTranscendentalNumberLiteralExpression | |
| CTranscendentalNumberType | |
| CType | |
| CUnaryBooleanFunctionExpression | |
| CUnaryExpression | |
| CUnaryNumericalFunctionExpression | |
| CValuation | The base class of all valuations of variables |
| CValueArrayExpression | Represents an array with a given list of elements |
| CVariable | |
| CVariableExpression | |
| CVariableIterator | |
| CVariableSetPredicateSplitter | |
| ►Ngbar | |
| ►Nabstraction | |
| ►Njani | |
| CAutomatonAbstractor | |
| CEdgeAbstractor | |
| CJaniMenuGameAbstractor | |
| ►Nprism | |
| CCommandAbstractor | |
| CModuleAbstractor | |
| CPrismMenuGameAbstractor | |
| CAbstractionInformation | |
| CAbstractionInformationOptions | |
| CBottomStateResult | |
| CExplicitDijkstraQueueElement | |
| CExplicitDijkstraQueueElementLess | |
| CExplicitPivotStateResult | |
| CExplicitQualitativeGameResult | |
| CExplicitQualitativeGameResultMinMax | |
| CExplicitQualitativeResult | |
| CExplicitQualitativeResultMinMax | |
| CExplicitQuantitativeResult | |
| CExplicitQuantitativeResultMinMax | |
| CExpressionTranslator | |
| CGameBddResult | |
| CLocalExpressionInformation | |
| CMenuGame | This class represents a discrete-time stochastic two-player game |
| CMenuGameAbstractor | |
| CMenuGameAbstractorOptions | |
| CMenuGameRefiner | |
| CMenuGameRefinerOptions | |
| CPivotStateCandidatesResult | |
| CQualitativeResult | |
| CQualitativeResultMinMax | |
| CRefinementCommand | |
| CRefinementPredicates | |
| CStateSet | |
| CStateSetAbstractor | |
| CSymbolicMostProbablePathsResult | |
| CSymbolicPivotStateResult | |
| CSymbolicQualitativeGameResult | |
| CSymbolicQualitativeGameResultMinMax | |
| CSymbolicQualitativeMdpResult | |
| CSymbolicQualitativeMdpResultMinMax | |
| CSymbolicQualitativeResult | |
| CSymbolicQualitativeResultMinMax | |
| CSymbolicQuantitativeGameResult | |
| CSymbolicQuantitativeGameResultMinMax | |
| CSymbolicStateSet | |
| CValidBlockAbstractor | |
| CVariableSetHash | |
| ►Napi | |
| CAbstractionRefinementOptions | |
| ►Nmodelchecker | |
| ►Ndetail | |
| CPreviousExplicitResult | |
| CAbstractAbstractionRefinementModelChecker | |
| CBisimulationAbstractionRefinementModelChecker | |
| CExplicitGameExporter | |
| CGameBasedMdpModelChecker | |
| CGameBasedMdpModelCheckerOptions | |
| ►Ngenerator | |
| CActionMask | Action masks are arguments you can give to the state generator that limit which states are generated |
| CActiveCommandData | |
| CArrayVariableReplacementInformation | |
| CBeliefStateManager | This class keeps track of common information of a set of beliefs |
| CBeliefSupportTracker | |
| CBooleanVariableInformation | |
| CChoice | |
| CDistribution | |
| CDistributionEntry | |
| CIntegerVariableInformation | |
| CJaniNextStateGenerator | |
| CLocationVariableInformation | |
| CNextStateGenerator | |
| ►CNondeterministicBeliefTracker | This tracker implements state estimation for POMDPs |
| COptions | |
| CObservationDenseBeliefState | ObservationDenseBeliefState stores beliefs in a dense format (per observation) |
| CObservationLabelInformation | |
| CPrismNextStateGenerator | |
| CSparseBeliefState | SparseBeliefState stores beliefs in a sparse format |
| CStateBehavior | |
| CStateValuationFunctionMask | A particular instance of the action mask that uses a callback function to evaluate whether an action should be expanded |
| CTransientVariableData | |
| CTransientVariableInformation | |
| CTransientVariableValuation | |
| CVariableInformation | |
| ►Ngspn | |
| CGSPN | |
| CGspnBuilder | |
| CGspnJsonExporter | Exports a GSPN into the JSON format for visualizing it |
| CImmediateTransition | |
| CLayoutInfo | |
| CMarking | |
| CPlace | This class provides methods to store and retrieve data for a place in a gspn |
| CTimedTransition | |
| CTransition | This class represents a transition in a gspn |
| CTransitionPartition | |
| ►Nio | |
| CDirectEncodingOptions | |
| ►Njani | |
| ►Ndetail | |
| CArrayEliminatorDataCollector | Gets the data necessary for array elimination |
| ►CArrayExpressionEliminationVisitor | 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) |
| CResultType | |
| CArrayExpressionFinderExpressionVisitor | |
| CArrayExpressionFinderTraverser | |
| CArrayReplacementsCollectorExpressionVisitor | |
| CArrayVariableReplacer | |
| CConstEdges | |
| CEdges | |
| CFunctionCallExpressionFinderExpressionVisitor | |
| CFunctionCallExpressionFinderTraverser | |
| CFunctionEliminationExpressionVisitor | |
| CFunctionEliminatorTraverser | |
| CInformationCollector | |
| CVariableAccessedTraverser | |
| ►Nelimination_actions | |
| CAutomaticAction | |
| CEliminateAction | |
| CEliminateAutomaticallyAction | |
| CFinishAction | |
| CRebuildWithoutUnreachableAction | |
| CUnfoldAction | |
| ►CUnfoldDependencyGraph | |
| CVariableGroup | |
| CVariableInfo | |
| CAction | |
| CArrayEliminator | |
| ►CArrayEliminatorData | |
| CReplacement | |
| CArrayType | |
| CAssignment | |
| CAssignmentLevelFinder | |
| CAssignmentLevelToLevelComparator | |
| CAssignmentPartialOrderByLevelAndLValue | This functor enables ordering the assignments first by the assignment level and then by lValue |
| ►CAssignmentsFinder | |
| CResultType | |
| CAutomaton | |
| CAutomatonComposition | |
| CBasicType | |
| CBoundedType | |
| CClockType | |
| CComposition | |
| CCompositionInformation | |
| CCompositionInformationVisitor | |
| CCompositionJsonExporter | |
| CCompositionSimplificationVisitor | |
| CCompositionVisitor | |
| CConditionalMetaEdge | |
| CConstant | |
| CConstJaniTraverser | |
| CContinuousType | |
| CEdge | |
| CEdgeContainer | |
| CEdgeDestination | |
| CExpressionToJson | |
| CFilterExpression | |
| CFormulaToJaniJson | |
| CFunctionDefinition | |
| CInformationObject | |
| ►CJaniLocalEliminator | |
| CAction | |
| CEliminationScheduler | |
| CSession | |
| ►CJaniLocationExpander | |
| CNewIndices | |
| CReturnType | |
| CJaniScopeChanger | |
| CJaniTraverser | |
| CJaniType | |
| CJsonExporter | |
| CLocation | Jani Location: |
| CLValue | |
| CModel | |
| CModelFeatures | |
| COrderedAssignments | |
| CParallelComposition | |
| CProperty | |
| CPropertyInterval | Property intervals as per Jani Specification |
| CRewardModelInformation | |
| CSynchronizationVector | |
| CSynchronizationVectorLexicographicalLess | |
| CTemplateEdge | |
| CTemplateEdgeContainer | |
| CTemplateEdgeDestination | |
| CVariable | |
| CVariableSet | |
| CVariablesToConstantsTransformer | |
| ►Nlogic | |
| CAtomicExpressionFormula | |
| CAtomicLabelFormula | |
| CBinaryBooleanPathFormula | |
| CBinaryBooleanStateFormula | |
| CBinaryPathFormula | |
| CBinaryStateFormula | |
| CBooleanLiteralFormula | |
| CBound | |
| CBoundedUntilFormula | |
| CCloneVisitor | |
| CConditionalFormula | |
| CCumulativeRewardFormula | |
| CEventuallyFormula | |
| CExpectedTimeToExpectedRewardVisitor | |
| CExpressionSubstitutionVisitor | |
| CExtractMaximalStateFormulasVisitor | |
| CFormula | |
| CFormulaInformation | |
| CFormulaInformationVisitor | |
| CFormulaVisitor | |
| CFragmentChecker | |
| CFragmentSpecification | |
| CGameFormula | |
| CGloballyFormula | |
| CHOAPathFormula | |
| CInheritedInformation | |
| CInstantaneousRewardFormula | |
| CLabelSubstitutionVisitor | |
| CLiftableTransitionRewardsVisitor | |
| CLongRunAverageOperatorFormula | |
| CLongRunAverageRewardFormula | |
| CMultiObjectiveFormula | |
| CNextFormula | |
| COperatorFormula | |
| COperatorInformation | |
| CPathFormula | |
| CPlayerCoalition | |
| CProbabilityOperatorFormula | |
| CQuantileFormula | |
| CRewardAccumulation | |
| CRewardAccumulationEliminationVisitor | |
| CRewardModelNameSubstitutionVisitor | |
| CRewardOperatorFormula | |
| CStateFormula | |
| CTimeBound | |
| CTimeBoundReference | |
| CTimeOperatorFormula | |
| CToExpressionVisitor | |
| CToPrefixStringVisitor | |
| CTotalRewardFormula | |
| CUnaryBooleanPathFormula | |
| CUnaryBooleanStateFormula | |
| CUnaryPathFormula | |
| CUnaryStateFormula | |
| CUntilFormula | |
| ►Nmodelchecker | |
| ►Nexploration_detail | |
| CBounds | |
| CExplorationInformation | |
| CStateGeneration | |
| CStatistics | |
| ►Nhelper | |
| ►Ninternal | |
| CLraViHelper | Helper class that performs iterations of the value iteration method |
| CSparseLTLSchedulerHelper | Helper class for scheduler construction in LTL model checking |
| ►Nlexicographic | |
| ►Nspothelper | |
| Cproduct_state_hash | |
| ClexicographicModelCheckerHelper | |
| ►Nrewardbounded | |
| CCostLimit | |
| ►CCostLimitClosure | |
| CCostLimitsCompare | |
| CDimension | |
| CEpochManager | |
| CEpochModel | |
| CMemoryStateManager | |
| CMultiDimensionalRewardUnfolding | |
| CProductModel | |
| CQuantileHelper | |
| CBaierUpperRewardBoundsComputer | |
| CDsMpiDtmcPriorityLess | |
| CDsMpiDtmcUpperRewardBoundsComputer | |
| CDsMpiMdpPriorityLess | |
| CDsMpiMdpUpperRewardBoundsComputer | |
| CHybridCtmcCslHelper | |
| CHybridDtmcPrctlHelper | |
| CHybridInfiniteHorizonHelper | Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system |
| CHybridMarkovAutomatonCslHelper | |
| CHybridMdpPrctlHelper | |
| CMaybeStateResult | |
| CMDPSparseModelCheckingHelperReturnType | |
| CModelCheckerHelper | Helper class for solving a model checking query |
| CQualitativeStateSetsReachabilityRewards | |
| CQualitativeStateSetsUntilProbabilities | |
| CSingleValueModelCheckerHelper | Helper for model checking queries where we are interested in (optimizing) a single value per state |
| CSolverRequirementsData | |
| CSparseCtmcCslHelper | |
| CSparseDeterministicInfiniteHorizonHelper | Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system |
| CSparseDeterministicStepBoundedHorizonHelper | |
| CSparseDeterministicVisitingTimesHelper | Helper class for computing for each state the expected number of times to visit that state assuming a given initial distribution |
| CSparseDtmcPrctlHelper | |
| CSparseInfiniteHorizonHelper | Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system |
| CSparseLTLHelper | Helper class for LTL model checking |
| CSparseMarkovAutomatonCslHelper | |
| CSparseMdpEndComponentInformation | |
| CSparseMdpHintType | |
| CSparseMdpPrctlHelper | |
| CSparseNondeterministicInfiniteHorizonHelper | Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system |
| CSparseNondeterministicStepBoundedHorizonHelper | |
| CSymbolicDtmcPrctlHelper | |
| CSymbolicMdpPrctlHelper | |
| CUnifPlusHelper | |
| ►Nmultiobjective | |
| ►Npreprocessing | |
| CSparseMultiObjectivePreprocessor | |
| CSparseMultiObjectivePreprocessorResult | |
| ►CSparseMultiObjectiveRewardAnalysis | |
| CReturnType | |
| CDeterministicSchedsAchievabilityChecker | |
| CDeterministicSchedsLpChecker | Represents the LP Encoding for achievability under simple strategies |
| CDeterministicSchedsObjectiveHelper | |
| ►CDeterministicSchedsParetoExplorer | Implements the exploration of the Pareto front |
| CFacet | |
| CPoint | |
| CPointset | |
| CObjective | |
| CPcaaWeightVectorChecker | Helper Class that takes a weight vector and .. |
| CRewardBoundedMdpPcaaWeightVectorChecker | Helper Class that takes preprocessed Pcaa data and a weight vector and .. |
| CSparseCbAchievabilityQuery | |
| CSparseCbQuery | |
| CSparsePcaaAchievabilityQuery | |
| CSparsePcaaParetoQuery | |
| CSparsePcaaQuantitativeQuery | |
| ►CSparsePcaaQuery | |
| CRefinementStep | |
| CStandardMaPcaaWeightVectorChecker | Helper Class that takes preprocessed Pcaa data and a weight vector and .. |
| CStandardMdpPcaaWeightVectorChecker | Helper Class that takes preprocessed Pcaa data and a weight vector and .. |
| ►CStandardPcaaWeightVectorChecker | Helper Class that takes preprocessed Pcaa data and a weight vector and .. |
| CEcQuotient | |
| CLraMecDecomposition | |
| CVisitingTimesHelper | Provides helper functions for computing bounds on the expected visiting times |
| CWeightVectorCheckerFactory | |
| ►Nregion | |
| CSparseDtmcRegionModelChecker | |
| CAbstractModelChecker | |
| CCheckResult | |
| CCheckTask | |
| CExplicitModelCheckerHint | This class contains information that might accelerate the model checking process |
| CExplicitParetoCurveCheckResult | |
| CExplicitQualitativeCheckResult | |
| CExplicitQuantitativeCheckResult | |
| CHybridCtmcCslModelChecker | |
| CHybridDtmcPrctlModelChecker | |
| CHybridMarkovAutomatonCslModelChecker | |
| CHybridMdpPrctlModelChecker | |
| CHybridQuantitativeCheckResult | |
| CLexicographicCheckResult | |
| CModelCheckerHint | This class contains information that might accelerate the model checking process |
| CParetoCurveCheckResult | |
| CQualitativeCheckResult | |
| CQuantitativeCheckResult | |
| CRegionBound | |
| CRegionCheckResult | |
| CRegionModelChecker | |
| CRegionRefinementCheckResult | |
| CSparseCtmcCslModelChecker | |
| CSparseCtmcInstantiationModelChecker | Class to efficiently check a formula on a parametric model with different parameter instantiations |
| CSparseDtmcEliminationModelChecker | |
| CSparseDtmcInstantiationModelChecker | Class to efficiently check a formula on a parametric model with different parameter instantiations |
| CSparseDtmcParameterLiftingModelChecker | |
| CSparseDtmcPrctlModelChecker | |
| CSparseExplorationModelChecker | |
| CSparseInstantiationModelChecker | Class to efficiently check a formula on a parametric model with different parameter instantiations |
| CSparseMarkovAutomatonCslModelChecker | |
| CSparseMdpInstantiationModelChecker | Class to efficiently check a formula on a parametric model with different parameter instantiations |
| CSparseMdpParameterLiftingModelChecker | |
| CSparseMdpPrctlModelChecker | |
| CSparseParameterLiftingModelChecker | 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., |
| CSparsePropositionalModelChecker | |
| CSparseSmgRpatlModelChecker | |
| CSymbolicDtmcPrctlModelChecker | |
| CSymbolicMdpPrctlModelChecker | |
| CSymbolicParetoCurveCheckResult | |
| CSymbolicPropositionalModelChecker | |
| CSymbolicQualitativeCheckResult | |
| CSymbolicQuantitativeCheckResult | |
| CValidatingSparseDtmcParameterLiftingModelChecker | |
| CValidatingSparseMdpParameterLiftingModelChecker | |
| CValidatingSparseParameterLiftingModelChecker | |
| ►Nmodels | |
| ►Nsparse | |
| CChoiceLabeling | This class manages the labeling of the choice space with a number of (atomic) labels |
| CCtmc | This class represents a continuous-time Markov chain |
| CDeterministicModel | The base class of all sparse deterministic models |
| CDtmc | This class represents a discrete-time Markov chain |
| CItemLabeling | A base class managing the labeling of items with a number of (atomic) labels |
| CMarkovAutomaton | This class represents a Markov automaton |
| CMdp | This class represents a (discrete-time) Markov decision process |
| CModel | Base class for all sparse models |
| CNondeterministicModel | The base class of sparse nondeterministic models |
| CPomdp | This class represents a partially observable Markov decision process |
| CSmg | This class represents a stochastic multiplayer game |
| CStandardRewardModel | |
| CStateAnnotation | |
| CStateLabeling | This class manages the labeling of the state space with a number of (atomic) labels |
| CStochasticTwoPlayerGame | This class represents a (discrete-time) stochastic two-player game |
| ►Nsymbolic | |
| CCtmc | This class represents a continuous-time Markov chain |
| CDeterministicModel | Base class for all deterministic symbolic models |
| CDtmc | This class represents a discrete-time Markov chain |
| CMarkovAutomaton | This class represents a discrete-time Markov decision process |
| CMdp | This class represents a discrete-time Markov decision process |
| CModel | Base class for all symbolic models |
| CNondeterministicModel | Base class for all nondeterministic symbolic models |
| CStandardRewardModel | |
| CStochasticTwoPlayerGame | This class represents a discrete-time stochastic two-player game |
| CGetDdType | |
| CGetDdType< ModelRepresentation::DdCudd > | |
| CGetDdType< ModelRepresentation::DdSylvan > | |
| CGetDdType< ModelRepresentation::Sparse > | |
| CGetModelRepresentation | |
| CGetModelRepresentation< storm::dd::DdType::CUDD > | |
| CGetModelRepresentation< storm::dd::DdType::Sylvan > | |
| CModel | |
| CModelBase | |
| ►Npars | |
| CFeasibilitySynthesisTask | |
| CPreprocessResult | |
| CSampleInformation | |
| ►Nparser | Contains all file parsers and helper classes |
| CAtomicPropositionLabelingParser | This class can be used to parse a labeling file |
| CAutoParser | This class automatically chooses the correct parser for the given files and returns the corresponding model |
| CDeterministicModelParser | Loads a deterministic model (Dtmc or Ctmc) from files |
| ►CDeterministicSparseTransitionParser | This class can be used to parse a file containing either transitions or transition rewards of a deterministic model |
| CFirstPassResult | A structure representing the result of the first pass of this parser |
| CDirectEncodingParser | Parser for models in the DRN format with explicit encoding |
| CDirectEncodingParserOptions | |
| CExpressionCreator | |
| CExpressionParser | |
| CFormulaParser | |
| CFormulaParserGrammar | |
| CGlobalProgramInformation | |
| CGspnParser | |
| CImcaMarkovAutomatonParser | |
| CImcaParserGrammar | |
| ►CJaniParser | |
| CScope | |
| CMappedFile | Opens a file and maps it to memory providing a char* containing the file content |
| CMarkovAutomatonParser | Loads a labeled Markov automaton from files |
| ►CMarkovAutomatonSparseTransitionParser | A class providing the functionality to parse the transitions of a Markov automaton |
| CFirstPassResult | A structure representing the result of the first pass of this parser |
| CResult | A structure representing the result of the parser |
| CMonotonicityParser | |
| CNondeterministicModelParser | Loads a nondeterministic model (Mdp or Ctmdp) from files |
| ►CNondeterministicSparseTransitionParser | A class providing the functionality to parse the transitions of a nondeterministic model |
| CFirstPassResult | A structure representing the result of the first pass of this parser |
| CParameterRegionParser | |
| CPrismParser | |
| CPrismParserGrammar | |
| CRationalPolicies | |
| CSparseChoiceLabelingParser | A class providing the functionality to parse a choice labeling |
| CSparseItemLabelingParser | This class can be used to parse a labeling file |
| CSparseStateRewardParser | A class providing the functionality to parse a the state rewards of a model |
| CSpiritErrorHandler | |
| CValueParser | Parser for values according to their ValueType |
| ►Npomdp | |
| ►Nanalysis | |
| ►CFormulaInformation | |
| CStateSet | Characterizes a certain set of states |
| ►Nmodelchecker | |
| ►CBeliefExplorationPomdpModelChecker | Model checker for checking reachability queries on POMDPs using approximations based on exploration of the belief MDP |
| CResult | Struct used to store the results of the model checker |
| CBeliefExplorationPomdpModelCheckerOptions | |
| CPOMDPValueBounds | Structure for storing values on the POMDP used for cut-offs and clipping |
| CPreprocessingPomdpValueBoundsModelChecker | |
| ►Nqualitative | |
| ►Ndetail | |
| CObsActPair | |
| CJaniBeliefSupportMdpGenerator | |
| ►Nstorage | |
| CExtremePOMDPValueBound | Struct to store the extreme bound values needed for the reward correction values when clipping is used |
| CPreprocessingPomdpValueBounds | Struct for storing precomputed values bounding the actual values on the POMDP |
| ►Ntransformer | |
| CKnownProbabilityTransformer | |
| CInternalObservationScheduler | |
| ►CIterativePolicySearch | |
| CStatistics | |
| CMemlessSearchOptions | |
| CObservationTraceUnfolder | Observation-trace unrolling to allow model checking for monitoring |
| COneShotPolicySearch | |
| CWinningRegion | |
| CWinningRegionQueryInterface | |
| ►Nprism | |
| CAssignment | |
| CBooleanVariable | |
| CClockVariable | |
| CCommand | |
| CComposition | |
| CCompositionToJaniVisitor | |
| CCompositionValidityChecker | |
| CCompositionVisitor | |
| CConstant | |
| CFormula | |
| CHidingComposition | |
| CInitialConstruct | |
| CIntegerVariable | |
| CInterleavingParallelComposition | |
| CLabel | |
| CLocatedInformation | |
| CModule | |
| CModuleComposition | |
| CModuleRenaming | |
| CObservationLabel | |
| COverlappingGuardAnalyser | |
| CParallelComposition | |
| CPlayer | |
| CProgram | |
| CRenamingComposition | |
| CRestrictedParallelComposition | |
| CRewardModel | |
| CStateActionReward | |
| CStateReward | |
| CSynchronizingParallelComposition | |
| CSystemCompositionConstruct | |
| CToJaniConverter | |
| CTransitionReward | |
| CUpdate | |
| CVariable | |
| ►Nps | |
| CMilpPermissiveSchedulerComputation | |
| CPermissiveScheduler | |
| CPermissiveSchedulerComputation | |
| CPermissiveSchedulerPenalties | |
| CSmtPermissiveSchedulerComputation | |
| CSubMDPPermissiveScheduler | |
| ►Nsettings | |
| ►Nmodules | |
| CAbstractionSettings | This class represents the settings for the abstraction procedures |
| CBeliefExplorationSettings | This class represents the settings for POMDP model checking |
| CBisimulationSettings | This class represents the bisimulation settings |
| CBuildSettings | |
| CConversionGeneralSettings | |
| CConversionInputSettings | |
| CConversionOutputSettings | |
| CCoreSettings | This class represents the core settings |
| CCounterexampleGeneratorSettings | This class represents the settings for counterexample generation |
| CCuddSettings | This class represents the settings for CUDD |
| CDebugSettings | This class represents the debug settings |
| CDerivativeSettings | This class represents the settings for Gradient Descent |
| CEigenEquationSolverSettings | This class represents the settings for Eigen |
| CEliminationSettings | This class represents the settings for the elimination-based procedures |
| CExplorationSettings | This class represents the exploration settings |
| CFeasibilitySettings | This class represents the settings for parametric model checking |
| CGameSolverSettings | This class represents the game solver settings |
| CGeneralSettings | This class represents the general settings |
| CGlpkSettings | This class represents the settings for glpk |
| CGmmxxEquationSolverSettings | This class represents the settings for gmm++ |
| CGSPNExportSettings | |
| CGSPNSettings | |
| CGurobiSettings | This class represents the settings for Gurobi |
| CHintSettings | This class represents the model transformer settings |
| CIOSettings | This class represents the markov chain settings |
| CJaniExportSettings | |
| CLongRunAverageSolverSettings | This class represents the LRA solver settings |
| CMinMaxEquationSolverSettings | This class represents the min/max solver settings |
| CModelCheckerSettings | This class represents the general settings |
| CModuleSettings | This is the base class of the settings for a particular module |
| CMonotonicitySettings | This class represents the settings for monotonicity checking |
| CMultiObjectiveSettings | This class represents the settings for multi-objective model checking |
| CMultiplierSettings | This class represents the multiplier settings |
| CNativeEquationSolverSettings | This class represents the settings for the native equation solver |
| COviSolverSettings | This class represents the settings for the optimistic value iteration solver |
| CParametricSettings | This class represents the settings for parametric model checking |
| CPartitionSettings | This class represents the settings for parametric model checking |
| CPOMDPSettings | This class represents the settings for POMDP model checking |
| CPrismExportSettings | |
| CQualitativePOMDPAnalysisSettings | This class represents the settings for POMDP model checking |
| CRegionSettings | This class represents the settings for parametric model checking |
| CRegionVerificationSettings | |
| CResourceSettings | This class represents the resource settings |
| CSamplingSettings | |
| CSmt2SmtSolverSettings | This class represents the settings for interaction with SMT-LIBv2 solvers |
| CSylvanSettings | This class represents the settings for Sylvan |
| CTimeBoundedSolverSettings | This class represents the min/max solver settings |
| CToParametricSettings | This class represents the settings for POMDP model checking |
| CTopologicalEquationSolverSettings | This class represents the settings for the native equation solver |
| CTransformationSettings | This class represents the model transformer settings |
| CArgument | This class subclasses the argument base to actually implement the pure virtual functions |
| CArgumentBase | This class serves as the (untemplated) base class of argument classes |
| CArgumentBuilder | This class serves as an API for creating arguments |
| CArgumentValidator | |
| CArgumentValidatorFactory | |
| CFileValidator | |
| CMultipleChoiceValidator | |
| COption | This class represents one command-line option |
| COptionBuilder | This class provides the interface to create an option.. |
| CRangeArgumentValidator | |
| CSettingMemento | This class is used to reset the state of an option that was temporarily set to a different status |
| CSettingsManager | Provides the central API for the registration of command line options and parsing the options from the command line |
| ►Nsimulator | |
| CDiscreteTimePrismProgramSimulator | This class provides a simulator interface on the prism program, and uses the next state generator |
| CDiscreteTimeSparseModelSimulator | This class is a low-level interface to quickly sample from Discrete-Time Models stored explicitly as a SparseModel |
| ►Nsolver | |
| ►Nhelper | |
| CGSVIBackend | |
| CIIBackend | |
| CIIData | |
| CIntervalIterationHelper | Implements interval iteration |
| COptimisticValueIterationHelper | Implements Optimistic value iteration |
| COVIBackend | |
| CRationalSearchHelper | Implements rational search |
| CRSBackend | |
| CSchedulerTrackingBackend | |
| CSchedulerTrackingHelper | Helper class to extract optimal scheduler choices from a MinMax equation system solution |
| ►CSoundValueIterationHelper | Implements sound value iteration |
| CSVIData | |
| CSVIBackend | |
| CValueIterationHelper | |
| CValueIterationOperator | This class represents the Value Iteration Operator (also known as Bellman operator) |
| CVIOperatorBackend | |
| ►Nstateelimination | |
| CConditionalStateEliminator | |
| CDynamicStatePriorityQueue | |
| CEliminatorBase | |
| CEquationSystemEliminator | |
| CMultiValueStateEliminator | |
| CNondeterministicModelStateEliminator | |
| CPrioritizedStateEliminator | |
| CPriorityComparator | |
| CStateEliminator | |
| CStatePriorityQueue | |
| CStaticStatePriorityQueue | |
| CAbstractEquationSolver | |
| CAcyclicLinearEquationSolver | This solver can be used on equation systems that are known to be acyclic |
| CAcyclicMinMaxLinearEquationSolver | This solver can be used on equation systems that are known to be acyclic |
| CEigenLinearEquationSolver | A class that uses the Eigen library to implement the LinearEquationSolver interface |
| CEigenLinearEquationSolverFactory | |
| CEliminationLinearEquationSolver | A class that uses gaussian elimination to implement the LinearEquationSolver interface |
| CEliminationLinearEquationSolverFactory | |
| CGameSolver | A class representing the interface that all game solvers shall implement |
| CGameSolverFactory | |
| CGeneralLinearEquationSolverFactory | |
| CGeneralMinMaxLinearEquationSolverFactory | |
| CGeneralSymbolicLinearEquationSolverFactory | |
| CGeneralSymbolicMinMaxLinearEquationSolverFactory | |
| CGlpkLpSolver | |
| CGmmxxLinearEquationSolver | A class that uses the gmm++ library to implement the LinearEquationSolver interface |
| CGmmxxLinearEquationSolverFactory | |
| CGmmxxMultiplier | |
| CGurobiEnvironment | |
| CGurobiLpSolver | A class that implements the LpSolver interface using Gurobi |
| CIterativeMinMaxLinearEquationSolver | |
| CLinearEquationSolver | An interface that represents an abstract linear equation solver |
| CLinearEquationSolverFactory | |
| CLinearEquationSolverRequirements | |
| CLpMinMaxLinearEquationSolver | Solves a MinMaxLinearEquationSystem using a linear programming solver |
| CLpSolver | An interface that captures the functionality of an LP solver |
| ►CMathsatSmtSolver | |
| COptions | A class that captures options that may be passed to the Mathsat solver |
| CMinMaxLinearEquationSolver | A class representing the interface that all min-max linear equation solvers shall implement |
| CMinMaxLinearEquationSolverFactory | |
| CMinMaxLinearEquationSolverRequirements | |
| CMultiplier | |
| CMultiplierFactory | |
| CNativeLinearEquationSolver | A class that uses storm's native matrix operations to implement the LinearEquationSolver interface |
| CNativeLinearEquationSolverFactory | |
| CNativeMultiplier | |
| CNoTerminationCondition | |
| CRawLpConstraint | |
| ►CSmtlibSmtSolver | This class represents an SMT-LIBv2 conforming solver |
| CSmtlibModelReference | |
| ►CSmtSolver | An interface that captures the functionality of an SMT solver |
| CModelReference | The base class for all model references |
| CSolveGoal | |
| CSolverRequirement | |
| CSoplexLpSolver | |
| CStandardGameSolver | |
| CStandardMinMaxLinearEquationSolver | |
| CSymbolicEliminationLinearEquationSolver | |
| CSymbolicEliminationLinearEquationSolverFactory | |
| CSymbolicEquationSolver | |
| CSymbolicGameSolver | An interface that represents an abstract symbolic game solver |
| CSymbolicGameSolverFactory | |
| CSymbolicLinearEquationSolver | An interface that represents an abstract symbolic linear equation solver |
| CSymbolicLinearEquationSolverFactory | |
| CSymbolicMinMaxLinearEquationSolver | An interface that represents an abstract symbolic linear equation solver |
| CSymbolicMinMaxLinearEquationSolverFactory | |
| CSymbolicNativeLinearEquationSolver | An interface that represents an abstract symbolic linear equation solver |
| CSymbolicNativeLinearEquationSolverFactory | |
| CTerminateIfFilteredExtremumBelowThreshold | |
| CTerminateIfFilteredExtremumExceedsThreshold | |
| CTerminateIfFilteredSumExceedsThreshold | |
| CTerminationCondition | |
| CTopologicalLinearEquationSolver | |
| CTopologicalLinearEquationSolverFactory | |
| CTopologicalMinMaxLinearEquationSolver | |
| CZ3LpSolver | A class that implements the LpSolver interface using Z3 |
| ►CZ3SmtSolver | |
| CZ3ModelReference | |
| ►Nstorage | |
| ►Nbisimulation | |
| CBlock | |
| CDeterministicBlockData | |
| CPartition | |
| ►Ngeometry | |
| CHalfspace | |
| CHyperplaneCollector | This class can be used to collect a set of hyperplanes (without duplicates) |
| CHyperplaneEnumeration | |
| CHyperrectangle | |
| CNativePolytope | |
| CPolytope | |
| CPolytopeTree | Represents a set of points in Euclidean space |
| CQuickHull | |
| CReduceVertexCloud | |
| CSubsetEnumerator | This class can be used to enumerate all k-sized subsets of {0,...,n-1} |
| ►Nsparse | |
| CChoiceOrigins | 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) |
| CJaniChoiceOrigins | This class represents for each choice the origin in the jani specification // TODO complete this |
| CModelComponents | |
| CPrismChoiceOrigins | This class represents for each choice the set of prism commands that induced the choice |
| CStateStorage | |
| ►CStateValuations | |
| CStateValuation | |
| CStateValueIterator | |
| CStateValueIteratorRange | |
| CStateValuationsBuilder | |
| ►CBeliefManager | |
| CBeliefClipping | |
| CTriangulation | |
| ►CBisimulationDecomposition | This class is the superclass of all decompositions of a sparse model into its bisimulation quotient |
| COptions | |
| ►CBitVector | A bit vector that is internally represented as a vector of 64-bit values |
| Cconst_iterator | A class that enables iterating over the indices of the bit vector whose corresponding bits are set to true |
| Cconst_reverse_iterator | A class that enables iterating over the indices of the bit vector whose corresponding bits are set to true |
| ►CBitVectorHashMap | This class represents a hash-map whose keys are bit vectors |
| CBitVectorHashMapIterator | |
| CConsecutiveUint64DynamicPriorityQueue | |
| CDecomposition | This class represents the decomposition of a model into blocks which are of the template type |
| CDeterministicModelBisimulationDecomposition | This class represents the decomposition of a deterministic model into its bisimulation quotient |
| CDeterministicTransition | |
| CDFT | |
| CDistribution | |
| CDistributionWithReward | |
| CDynamicPriorityQueue | |
| CExplicitGameStrategy | |
| CExplicitGameStrategyPair | |
| CFlexibleSparseMatrix | The flexible sparse matrix is used during state elimination |
| CFNV1aBitVectorHash | |
| CIntegerInterval | |
| CMatrixEntry | |
| CMaximalEndComponent | This class represents a maximal end-component of a nondeterministic model |
| CMaximalEndComponentDecomposition | This class represents the decomposition of a nondeterministic model into its maximal end components |
| CMemoryStructure | 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 |
| CMemoryStructureBuilder | |
| CModelFormulasPair | |
| CMurmur3BitVectorHash | |
| CNondeterministicMemoryStructure | |
| CNondeterministicMemoryStructureBuilder | |
| CNondeterministicModelBisimulationDecomposition | This class represents the decomposition of a nondeterministic model into its bisimulation quotient |
| CParameterRegion | |
| CPomdpMemory | |
| CPomdpMemoryBuilder | |
| CQvbsBenchmark | This class provides easy access to a benchmark of the Quantitative Verification Benchmark Set http://qcomp.org/benchmarks/ |
| CSccDecompositionMemoryCache | Holds temporary computation data used during the SCC decomposition algorithm |
| CSccDecompositionResult | Holds the result data of the implemented SCC decomposition algorithm |
| CScheduler | This class defines which action is chosen in a particular state of a non-deterministic model |
| CSchedulerChoice | |
| CSchedulerClass | |
| ►CSparseMatrix | A class that holds a possibly non-square matrix in the compressed row storage format |
| Cconst_rows | This class represents a number of consecutive rows of the matrix |
| Crows | This class represents a number of consecutive rows of the matrix |
| CSparseMatrixBuilder | A class that can be used to build a sparse matrix by adding value by value |
| CSparseModelMemoryProduct | This class builds the product of the given sparse model and the given memory structure |
| CSparseModelNondeterministicMemoryProduct | |
| CStateActionPair | |
| CStateActionTarget | |
| CStateBlock | |
| CStronglyConnectedComponent | This class represents a strongly connected component, i.e., a set of states such that every state can reach every other state |
| CStronglyConnectedComponentDecomposition | This class represents the decomposition of a graph-like structure into its strongly connected components |
| CStronglyConnectedComponentDecompositionOptions | |
| CSymbolicModelDescription | |
| ►Ntransformer | |
| ►Ndetail | |
| CActionIdentifier | |
| CChoiceLabelIdStorage | |
| CAddUncertainty | This class is a convenience transformer to add uncertainty |
| CApplyFiniteSchedulerToPomdp | |
| CBinaryDtmcTransformer | |
| CBinaryPomdpTransformer | |
| CBinaryPomdpTransformerRowGroup | |
| CBinaryPomdpTransformerRowGroupCompare | |
| CChoiceSelector | |
| CContinuousToDiscreteTimeModelTransformer | |
| CDAProduct | |
| CDAProductBuilder | |
| ►CEndComponentEliminator | |
| CEndComponentEliminatorReturnType | |
| CGlobalPomdpMecChoiceEliminator | |
| CGlobalPOMDPSelfLoopEliminator | |
| ►CGoalStateMerger | |
| CReturnType | |
| CLabelInformation | |
| CMakePOMDPCanonic | |
| CMakeStateSetObservationClosed | |
| CMemoryIncorporation | 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 |
| CNonMarkovianChainTransformer | Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov automata |
| ►CParameterLifter | 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 |
| CAbstractValuation | |
| CPomdpMemoryUnfolder | |
| CPomdpTransformationResult | |
| CProduct | |
| CProductBuilder | |
| CRationalFunctionConstructor | |
| CSparseParametricDtmcSimplifier | This class performs different steps to simplify the given (parametric) model |
| CSparseParametricMdpSimplifier | This class performs different steps to simplify the given (parametric) model |
| CSparseParametricModelSimplifier | This class performs different steps to simplify the given (parametric) model |
| CStateWithRow | |
| CSubsystemBuilderOptions | |
| CSubsystemBuilderReturnType | |
| CSymbolicCtmcToSparseCtmcTransformer | |
| CSymbolicDtmcToSparseDtmcTransformer | |
| CSymbolicMaToSparseMaTransformer | |
| CSymbolicMdpToSparseMdpTransformer | |
| CTimeTravelling | |
| ►Nutility | |
| ►Ndetail | |
| CDoubleGreater | |
| CDoubleLess | |
| CElementGreater | |
| CElementGreater< double > | |
| CElementLess | |
| CElementLess< double > | |
| ►Ngraph | |
| CExplicitGameProb01Result | |
| CSymbolicGameProb01Result | |
| ►Nksp | |
| CPath | |
| CShortestPathsGenerator | |
| ►Nnumerical | |
| CFoxGlynnResult | |
| ►Nparametric | |
| CCoefficientType | Acess the type of coefficients from a given function type |
| CVariableType | Access the type of variables from a given function type |
| ►Npfinternal | |
| CFeatures | |
| ►Nresources | |
| CSignalInformation | |
| ►Nsolver | |
| CGlpkLpSolverFactory | |
| CGurobiLpSolverFactory | |
| CLpSolverFactory | |
| CMathsatSmtSolverFactory | |
| CSmtSolverFactory | |
| CSoplexLpSolverFactory | |
| CZ3LpSolverFactory | |
| CZ3SmtSolverFactory | |
| ►Nstring | |
| CSimilarStrings | |
| ►Nvector | |
| CVectorHash | |
| CAutomaticSettings | |
| CBernoulliDistributionGenerator | |
| CConstantsComparator | |
| CConstantsComparator< ValueType, ConstantsComparatorEnablePrecision< ValueType > > | |
| CExponentialDistributionGenerator | |
| CExtremum | Stores and manages an extremal (maximal or minimal) value |
| CFilteredRewardModel | |
| CHash | |
| CModelInstantiator | This class allows efficient instantiation of the given parametric model |
| CProgressMeasurement | A class that provides convenience operations to display run times |
| CRandomProbabilityGenerator | |
| CRandomProbabilityGenerator< double > | |
| CRandomProbabilityGenerator< storm::RationalNumber > | |
| CStopwatch | A class that provides convenience operations to display run times |
| CVectorHelper | |
| CEigenSolverEnvironment | |
| CEnvironment | |
| CGameSolverEnvironment | |
| CGmmxxSolverEnvironment | |
| CInternalEnvironment | |
| CLongRunAverageSolverEnvironment | |
| CMinMaxLpSolverEnvironment | |
| CMinMaxSolverEnvironment | |
| CModelCheckerEnvironment | |
| CMultiObjectiveModelCheckerEnvironment | |
| CMultiplierEnvironment | |
| CNativeSolverEnvironment | |
| CNullRefType | Auxiliary struct used to identify OptionalRefs that do not contain a reference |
| CNumberTraits | |
| CNumberTraits< double > | |
| CNumberTraits< storm::RationalFunction > | |
| COptionalRef | Helper class that optionally holds a reference to an object of type T |
| COviSolverEnvironment | |
| CSolverEnvironment | |
| CStormVersion | |
| CSubEnvironment | |
| CTimeBoundedSolverEnvironment | |
| CTopologicalSolverEnvironment | |
| CAssumptionCheckerTest | |
| CAssumptionMakerTest | |
| ►CBeliefExplorationAPITest | |
| CInput | |
| CBinaryDtmcTransformer | |
| CCudd | |
| CDd | |
| CDdPrismModelBuilderTest | |
| CDefaultDoubleVIEnvironment | |
| CExplicitPrismModelBuilderTest | |
| CFullySymbolicGameSolverTest | |
| CGameBasedDtmcModelCheckerTest | |
| CGameBasedMdpModelCheckerTest | |
| CGraphTestAR | |
| CGraphTestExplicit | |
| CGraphTestSymbolic | |
| CJaniLocalElimination | |
| CKSPTest | |
| CMonotonicityCheckerTest | |
| CMonotonicityHelperTest | |
| COrderExtenderTest | |
| CPrismMenuGame | |
| CQualitativeAnalysis | |
| CSparseDtmcMultiDimensionalRewardUnfoldingTest | |
| CSparseExplorationModelCheckerTest | |
| CSparseMaCbMultiObjectiveModelCheckerTest | |
| CSparseMdpCbMultiObjectiveModelCheckerTest | |
| CSparseMdpMultiDimensionalRewardUnfoldingTest | |
| CSylvan | |
| CSylvanDd | |
| CSymbolicModelBisimulationDecomposition | |
| CTimeTravelling | |
1.9.8