Stormpy API ReferenceΒΆ
Work in progress!
Stormpy modules:
- Stormpy.core
ActionMaskDoubleAddIterator_Sylvan_DoubleAdd_Sylvan_DoubleArrayTypeAtomicExpressionFormulaAtomicLabelFormulaBasicTypeBdd_SylvanBinaryBooleanOperatorTypeBinaryPathFormulaBinaryStateFormulaBisimulationTypeBitVectorBooleanBinaryStateFormulaBooleanLiteralFormulaBoundedTypeBoundedUntilFormulaBuilderOptionsCheckTaskChoiceLabelingChoiceOriginsClockTypeComparisonTypeConditionalFormulaConstraintCollectorContinuousTypeCumulativeRewardFormulaDdManager_SylvanDdMetaVariableTypeDdMetaVariable_SylvanDd_SylvanDiceStringVisitorDirectEncodingExporterOptionsDirectEncodingParserOptionsDistributionDistributionExactDistributionIntervalEliminationLabelBehaviorEndComponentEliminatorReturnTypeDoubleEnumEnvironmentEquationSolverTypeEventuallyFormulaExactCheckTaskExactParetoCurveCheckResultExactSparseMatrixExactSparseMatrixBuilderExactSparseMatrixEntryExactSparseMatrixRowsExplicitExactParetoCurveCheckResultExplicitExactQualitativeCheckResultExplicitExactQuantitativeCheckResultExplicitModelBuilderExplicitModelCheckerHintDoubleExplicitParametricModelBuilderExplicitParametricQualitativeCheckResultExplicitParametricQuantitativeCheckResultExplicitParetoCurveCheckResultExplicitQualitativeCheckResultExplicitQuantitativeCheckResultExplicitStateLookupExpressionExpressionManagerExpressionParserExpressionTypeFactorizedPolynomialFactorizedRationalFunctionFlatSetFormulaGameFormulaGloballyFormulaHybridExactQuantitativeCheckResultHybridParametricQuantitativeCheckResultHybridQuantitativeCheckResultInstantaneousRewardFormulaIntervalSparseMatrixIntervalSparseMatrixBuilderIntervalSparseMatrixEntryIntervalSparseMatrixRowsItemLabelingJaniAssignmentJaniAutomatonJaniChoiceOriginsJaniConstantJaniEdgeJaniEdgeDestinationJaniInformationObjectJaniLocationJaniLocationExpanderJaniModelJaniModelTypeJaniOrderedAssignmentsJaniScopeChangerJaniTemplateEdgeJaniTemplateEdgeDestinationJaniTypeJaniVariableJaniVariableSetLongRunAvarageOperatorLongRunAverageRewardFormulaMaximalEndComponentMaximalEndComponentDecomposition_doubleMaximalEndComponentDecomposition_exactMaximalEndComponentDecomposition_intervalMaximalEndComponentDecomposition_ratfuncMemoryStructureMemoryStructureBuilderMemoryStructureBuilderExactMemoryStructureBuilderIntervalMemoryStructureBuilderParametricMemoryStructureProductMemoryStructureProductExactMemoryStructureProductIntervalMemoryStructureProductParametricMinMaxMethodMinMaxSolverEnvironmentModelCheckerHintModelFormulasPairModelTypeMultiObjectiveFormulaNativeLinearEquationSolverMethodNativeSolverEnvironmentOperatorFormulaOperatorTypeOptimizationDirectionOverlappingGuardAnalyserParametricCheckTaskParametricSparseMatrixParametricSparseMatrixBuilderParametricSparseMatrixEntryParametricSparseMatrixRowsParetoCurveCheckResultPathFormulaPolynomialPolytopeDoublePolytopeExactPrismAssignmentPrismBooleanVariablePrismChoiceOriginsPrismCommandPrismConstantPrismIntegerVariablePrismLabelPrismModelTypePrismModulePrismProgramPrismRewardModelPrismUpdatePrismVariableProbabilityOperatorPropertyQuotientFormatRationalRationalFunctionRationalRFRewardOperatorSMTCounterExampleGeneratorSMTCounterExampleGeneratorOptionsSMTCounterExampleGeneratorStatsSMTCounterExampleInputSchedulerSchedulerChoiceSchedulerChoiceExactSchedulerChoiceIntervalSchedulerChoiceParametricSchedulerExactSchedulerIntervalSchedulerParametricSimpleValuationSolverEnvironmentSparseCtmcSparseDtmcSparseExactCtmcSparseExactDtmcSparseExactMASparseExactMdpSparseExactModelActionSparseExactModelActionsSparseExactModelComponentsSparseExactModelStateSparseExactModelStatesSparseExactPomdpSparseExactRewardModelSparseExactSmgSparseIntervalCtmcSparseIntervalDtmcSparseIntervalMASparseIntervalMdpSparseIntervalModelActionSparseIntervalModelActionsSparseIntervalModelComponentsSparseIntervalModelStateSparseIntervalModelStatesSparseIntervalPomdpSparseIntervalRewardModelSparseIntervalSmgSparseMASparseMatrixSparseMatrixBuilderSparseMatrixEntrySparseMatrixRowsSparseMdpSparseModelActionSparseModelActionsSparseModelComponentsSparseModelStateSparseModelStatesSparseParametricCtmcSparseParametricDtmcSparseParametricMASparseParametricMdpSparseParametricModelActionSparseParametricModelActionsSparseParametricModelComponentsSparseParametricModelStateSparseParametricModelStatesSparseParametricPomdpSparseParametricRewardModelSparseParametricSmgSparsePomdpSparseRewardModelSparseSmgStateFormulaStateLabelingStateValuationStateValuationFunctionActionMaskDoubleStateValuationTransformerStateValuationsBuilderSubsystemBuilderOptionsSubsystemBuilderReturnTypeDoubleSubsystemBuilderReturnTypeExactSubsystemBuilderReturnTypeRatFuncSymbolicExactQuantitativeCheckResultSymbolicModelDescriptionSymbolicParametricQuantitativeCheckResultSymbolicQualitativeCheckResultSymbolicQuantitativeCheckResultSymbolicSylvanCtmcSymbolicSylvanDtmcSymbolicSylvanExactCtmcSymbolicSylvanExactDtmcSymbolicSylvanExactMASymbolicSylvanExactMdpSymbolicSylvanExactRewardModelSymbolicSylvanMASymbolicSylvanMdpSymbolicSylvanParametricCtmcSymbolicSylvanParametricDtmcSymbolicSylvanParametricMASymbolicSylvanParametricMdpSymbolicSylvanParametricRewardModelSymbolicSylvanRewardModelTimeOperatorUnaryBooleanStateFormulaUnaryPathFormulaUnaryStateFormulaUncertaintyResolutionModeUntilFormulaValuationVariablebuild_interval_model_from_drn()build_model()build_model_from_drn()build_parametric_model()build_parametric_model_from_drn()build_parametric_sparse_matrix()build_sparse_exact_model()build_sparse_exact_model_with_options()build_sparse_interval_model()build_sparse_interval_model_with_options()build_sparse_matrix()build_sparse_model()build_sparse_model_from_explicit()build_sparse_model_with_options()build_sparse_parametric_model()build_sparse_parametric_model_with_options()build_symbolic_model()build_symbolic_parametric_model()check_interval_dtmc()check_interval_mdp()check_model_dd()check_model_hybrid()check_model_sparse()collect_information()compute_all_until_probabilities()compute_expected_number_of_visits()compute_prob01_states()compute_prob01max_states()compute_prob01min_states()compute_steady_state_distribution()compute_transient_probabilities()construct_submodel()create_filter_initial_states_sparse()create_filter_initial_states_sparseExact()create_filter_initial_states_symbolic()create_filter_initial_states_symbolicExact()create_filter_symbolic()create_filter_symbolicExact()eliminate_ECs()eliminate_non_markovian_chains()eliminate_reward_accumulations()export_jani_to_file()export_to_drn()get_maximal_end_components()get_reachable_states()install_signal_handlers()make_sparse_model_builder()make_sparse_model_builder_exact()make_sparse_model_builder_parametric()model_checking()parse_constants_string()parse_jani_model()parse_jani_model_from_string()parse_prism_program()parse_properties()parse_properties_for_jani_model()parse_properties_for_prism_program()parse_properties_without_context()perform_bisimulation()perform_sparse_bisimulation()perform_symbolic_bisimulation()preprocess_symbolic_input()prob01max_states()prob01min_states()product_model()reset_timeout()set_loglevel_debug()set_loglevel_error()set_loglevel_trace()set_settings()set_state_valuations()set_timeout()topological_sort()transform_to_discrete_time_model()transform_to_sparse_model()
- Stormpy.info
- Stormpy.exceptions
- Stormpy.logic
AtomicExpressionFormulaAtomicLabelFormulaBinaryBooleanOperatorTypeBinaryPathFormulaBinaryStateFormulaBooleanBinaryStateFormulaBooleanLiteralFormulaBoundedUntilFormulaComparisonTypeConditionalFormulaCumulativeRewardFormulaEventuallyFormulaFormulaGameFormulaGloballyFormulaInstantaneousRewardFormulaLongRunAvarageOperatorLongRunAverageRewardFormulaMultiObjectiveFormulaOperatorFormulaPathFormulaProbabilityOperatorRewardOperatorStateFormulaTimeOperatorUnaryBooleanStateFormulaUnaryPathFormulaUnaryStateFormulaUntilFormula
- Stormpy.storage
AddIterator_Sylvan_DoubleAdd_Sylvan_DoubleArrayTypeBasicTypeBdd_SylvanBitVectorBoundedTypeChoiceLabelingChoiceOriginsClockTypeContinuousTypeDdManager_SylvanDdMetaVariableTypeDdMetaVariable_SylvanDd_SylvanDiceStringVisitorDistributionDistributionExactDistributionIntervalExactSparseMatrixExactSparseMatrixBuilderExactSparseMatrixEntryExactSparseMatrixRowsExpressionExpressionManagerExpressionParserExpressionTypeIntervalSparseMatrixIntervalSparseMatrixBuilderIntervalSparseMatrixEntryIntervalSparseMatrixRowsItemLabelingJaniAssignmentJaniAutomatonJaniChoiceOriginsJaniConstantJaniEdgeJaniEdgeDestinationJaniInformationObjectJaniLocationJaniLocationExpanderJaniModelJaniOrderedAssignmentsJaniScopeChangerJaniTemplateEdgeJaniTemplateEdgeDestinationJaniTypeJaniVariableJaniVariableSetMaximalEndComponentMaximalEndComponentDecomposition_doubleMaximalEndComponentDecomposition_exactMaximalEndComponentDecomposition_intervalMaximalEndComponentDecomposition_ratfuncMemoryStructureMemoryStructureBuilderMemoryStructureBuilderExactMemoryStructureBuilderIntervalMemoryStructureBuilderParametricMemoryStructureProductMemoryStructureProductExactMemoryStructureProductIntervalMemoryStructureProductParametricModelTypeOperatorTypeOverlappingGuardAnalyserParametricSparseMatrixParametricSparseMatrixBuilderParametricSparseMatrixEntryParametricSparseMatrixRowsPolytopeDoublePolytopeExactPrismAssignmentPrismBooleanVariablePrismChoiceOriginsPrismCommandPrismConstantPrismIntegerVariablePrismLabelPrismModelTypePrismModulePrismProgramPrismRewardModelPrismUpdatePrismVariableSchedulerSchedulerChoiceSchedulerChoiceExactSchedulerChoiceIntervalSchedulerChoiceParametricSchedulerExactSchedulerIntervalSchedulerParametricSimpleValuationSparseCtmcSparseDtmcSparseExactCtmcSparseExactDtmcSparseExactMASparseExactMdpSparseExactModelActionSparseExactModelActionsSparseExactModelComponentsSparseExactModelStateSparseExactModelStatesSparseExactPomdpSparseExactRewardModelSparseExactSmgSparseIntervalCtmcSparseIntervalDtmcSparseIntervalMASparseIntervalMdpSparseIntervalModelActionSparseIntervalModelActionsSparseIntervalModelComponentsSparseIntervalModelStateSparseIntervalModelStatesSparseIntervalPomdpSparseIntervalRewardModelSparseIntervalSmgSparseMASparseMatrixSparseMatrixBuilderSparseMatrixEntrySparseMatrixRowsSparseMdpSparseModelActionSparseModelActionsSparseModelComponentsSparseModelStateSparseModelStatesSparseParametricCtmcSparseParametricDtmcSparseParametricMASparseParametricMdpSparseParametricModelActionSparseParametricModelActionsSparseParametricModelComponentsSparseParametricModelStateSparseParametricModelStatesSparseParametricPomdpSparseParametricRewardModelSparseParametricSmgSparsePomdpSparseRewardModelSparseSmgStateLabelingStateValuationStateValuationTransformerStateValuationsBuilderSymbolicSylvanCtmcSymbolicSylvanDtmcSymbolicSylvanExactCtmcSymbolicSylvanExactDtmcSymbolicSylvanExactMASymbolicSylvanExactMdpSymbolicSylvanExactRewardModelSymbolicSylvanMASymbolicSylvanMdpSymbolicSylvanParametricCtmcSymbolicSylvanParametricDtmcSymbolicSylvanParametricMASymbolicSylvanParametricMdpSymbolicSylvanParametricRewardModelSymbolicSylvanRewardModelValuationVariablebuild_parametric_sparse_matrix()build_sparse_matrix()collect_information()eliminate_reward_accumulations()export_jani_to_file()get_maximal_end_components()product_model()
- Stormpy.utility
- Stormpy.dft
ApproximationHeuristicDFTBE_doubleDFTBE_ratfuncDFTDependency_doubleDFTDependency_ratfuncDFTElementTypeDFTElement_doubleDFTElement_ratfuncDFTInstantiatorDFTSimulator_doubleDFTSimulator_ratfuncDFTStateInfoDFTState_doubleDFTState_ratfuncDFT_doubleDFT_ratfuncDftIndependentModuleDftSymmetriesExplicitDFTModelBuilder_doubleExplicitDFTModelBuilder_ratfuncFailableElementFailableElementsFailableIteratorRandomGeneratorRelevantEventsSimulationStepResultSimulationTraceResultanalyze_dft()build_model()compute_dependency_conflicts()compute_relevant_events()export_dft_json_file()export_dft_json_string()export_parametric_dft_json_file()export_parametric_dft_json_string()get_parameters()has_potential_modeling_issues()is_well_formed()load_dft_galileo_file()load_dft_json_file()load_dft_json_string()load_parametric_dft_galileo_file()load_parametric_dft_json_file()load_parametric_dft_json_string()modules_json()prepare_for_analysis()transform_dft()
- Stormpy.gspn
- Stormpy.pars
DtmcParameterLiftingModelCheckerMdpParameterLiftingModelCheckerModelInstantiatorModelTypePCtmcExactInstantiationCheckerPCtmcInstantiationCheckerPCtmcInstantiatorPDtmcExactInstantiationCheckerPDtmcInstantiationCheckerPDtmcInstantiatorPMaInstantiatorPMdpExactInstantiationCheckerPMdpInstantiationCheckerPMdpInstantiatorParameterRegionPartialPCtmcInstantiatorPartialPDtmcInstantiatorPartialPMaInstantiatorPartialPMdpInstantiatorRegionModelCheckerRegionRefinementCheckerRegionResultRegionResultHypothesiscreate_region_checker()create_region_refinement_checker()gather_derivatives()simplify_model()
- Stormpy.pomdp
BeliefExplorationModelCheckerDoubleBeliefExplorationModelCheckerOptionsDoubleBeliefExplorationPomdpModelCheckerResultDoubleBeliefMdpExplorerDoubleBeliefSupportTrackerDoubleBeliefSupportTrackerExactBeliefSupportWinningRegionBeliefSupportWinningRegionQueryInterfaceDoubleIterativeQualitativeSearchOptionsIterativeQualitativeSearchSolverDoubleNondeterministicBeliefTrackerDoubleSparseNondeterministicBeliefTrackerDoubleSparseOptionsNondeterministicBeliefTrackerExactSparseNondeterministicBeliefTrackerExactSparseOptionsObservationTraceUnfolderDoubleObservationTraceUnfolderExactObservationTraceUnfolderRfPomdpFscApplicationModePomdpMemoryPomdpMemoryBuilderPomdpMemoryPatternSparseBeliefStateDoubleSparseBeliefStateExactapply_unknown_fsc()create_interactive_mc()create_iterative_qualitative_search_solver_Double()create_nondeterminstic_belief_tracker()create_observation_trace_unfolder()make_canonic()make_simple()prepare_pomdp_for_qualitative_search_Double()unfold_memory()
- Pycarl core
- Pycarl convert
- Pycarl formula
- Pycarl parse