Stormpy Documentation¶
Stormpy is a set of python bindings for the probabilistic model checker Storm. Pycarl is bundled with stormpy. It is a set of python bindings for the computer arithmetic and logic library carl.
Contents:
- Installation
- Getting Started
- Advanced Examples
- Analysis
- Building Models
- Discrete-time Markov chains (DTMCs)
- Markov decision processes (MDPs)
- Continuous-time Markov chains (CTMCs)
- Markov automata (MAs)
- Engines
- Exploring Models
- Working with Simulators
- Reward Models
- Working with Schedulers
- Working with Shortest Paths
- Parametric Models
- Dynamic Fault Trees
- Generalized Stochastic Petri Nets
- Getting Started with Pycarl
- Contributors
Stormpy API Reference¶
Work in progress!
Modules:
- Stormpy.core
ActionMaskDoubleAddIterator_Sylvan_DoubleAdd_Sylvan_DoubleAtomicExpressionFormulaAtomicLabelFormulaBdd_SylvanBinaryBooleanOperatorTypeBinaryPathFormulaBinaryStateFormulaBisimulationTypeBitVectorBooleanBinaryStateFormulaBooleanLiteralFormulaBoundedUntilFormulaBuilderOptionsCheckTaskChoiceLabelingChoiceOriginsComparisonTypeConditionalFormulaConstraintCollectorCumulativeRewardFormulaDdManager_SylvanDdMetaVariableTypeDdMetaVariable_SylvanDd_SylvanDiceStringVisitorDirectEncodingOptionsDirectEncodingParserOptionsDistributionDistributionExactDistributionIntervalEliminationLabelBehaviorEndComponentEliminatorReturnTypeDoubleEnvironmentEquationSolverTypeEventuallyFormulaExactCheckTaskExactSparseMatrixExactSparseMatrixBuilderExactSparseMatrixEntryExactSparseMatrixRowsExplicitExactQuantitativeCheckResultExplicitModelBuilderExplicitModelCheckerHintDoubleExplicitParametricModelBuilderExplicitParametricQuantitativeCheckResultExplicitParetoCurveCheckResultDoubleExplicitQualitativeCheckResultExplicitQuantitativeCheckResultExplicitStateLookupExpressionExpressionManagerExpressionParserExpressionTypeFactorizedPolynomialFactorizedRationalFunctionFlatSetFormulaGameFormulaGloballyFormulaHybridExactQuantitativeCheckResultHybridParametricQuantitativeCheckResultHybridQuantitativeCheckResultInstantaneousRewardFormulaIntervalSparseMatrixIntervalSparseMatrixBuilderIntervalSparseMatrixEntryIntervalSparseMatrixRowsItemLabelingJaniAssignmentJaniAutomatonJaniChoiceOriginsJaniConstantJaniEdgeJaniEdgeDestinationJaniInformationObjectJaniLocationJaniLocationExpanderJaniModelJaniModelTypeJaniOrderedAssignmentsJaniScopeChangerJaniTemplateEdgeJaniTemplateEdgeDestinationJaniVariableJaniVariableSetLongRunAvarageOperatorLongRunAverageRewardFormulaMaximalEndComponentMaximalEndComponentDecomposition_doubleMaximalEndComponentDecomposition_exactMaximalEndComponentDecomposition_intervalMaximalEndComponentDecomposition_ratfuncMinMaxMethodMinMaxSolverEnvironmentModelCheckerHintModelFormulasPairModelTypeMultiObjectiveFormulaNativeLinearEquationSolverMethodNativeSolverEnvironmentOperatorFormulaOperatorTypeOptimizationDirectionOverlappingGuardAnalyserParametricCheckTaskParametricSparseMatrixParametricSparseMatrixBuilderParametricSparseMatrixEntryParametricSparseMatrixRowsParetoCurveCheckResultDoublePathFormulaPolynomialPolytopeDoublePolytopeExactPrismAssignmentPrismBooleanVariablePrismChoiceOriginsPrismCommandPrismConstantPrismIntegerVariablePrismLabelPrismModelTypePrismModulePrismProgramPrismRewardModelPrismUpdatePrismVariableProbabilityOperatorPropertyQuotientFormatRationalRationalFunctionRationalRFRewardOperatorSMTCounterExampleGeneratorSMTCounterExampleGeneratorOptionsSMTCounterExampleGeneratorStatsSMTCounterExampleInputSchedulerSchedulerChoiceSchedulerChoiceExactSchedulerChoiceIntervalSchedulerChoiceParametricSchedulerExactSchedulerIntervalSchedulerParametricSimpleValuationSolverEnvironmentSparseCtmcSparseDtmcSparseExactCtmcSparseExactDtmcSparseExactMASparseExactMdpSparseExactModelActionSparseExactModelActionsSparseExactModelComponentsSparseExactModelStateSparseExactModelStatesSparseExactPomdpSparseExactRewardModelSparseExactSmgSparseIntervalCtmcSparseIntervalDtmcSparseIntervalMASparseIntervalMdpSparseIntervalModelActionSparseIntervalModelActionsSparseIntervalModelComponentsSparseIntervalModelStateSparseIntervalModelStatesSparseIntervalPomdpSparseIntervalRewardModelSparseIntervalSmgSparseMASparseMatrixSparseMatrixBuilderSparseMatrixEntrySparseMatrixRowsSparseMdpSparseModelActionSparseModelActionsSparseModelComponentsSparseModelStateSparseModelStatesSparseParametricCtmcSparseParametricDtmcSparseParametricMASparseParametricMdpSparseParametricModelActionSparseParametricModelActionsSparseParametricModelComponentsSparseParametricModelStateSparseParametricModelStatesSparseParametricPomdpSparseParametricRewardModelSparsePomdpSparseRewardModelSparseSmgStateFormulaStateLabelingStateValuationStateValuationFunctionActionMaskDoubleStateValuationsBuilderStormErrorSubsystemBuilderOptionsSubsystemBuilderReturnTypeDoubleSubsystemBuilderReturnTypeExactSubsystemBuilderReturnTypeRatFuncSymbolicExactQuantitativeCheckResultSymbolicModelDescriptionSymbolicParametricQuantitativeCheckResultSymbolicQualitativeCheckResultSymbolicQuantitativeCheckResultSymbolicSylvanCtmcSymbolicSylvanDtmcSymbolicSylvanMASymbolicSylvanMdpSymbolicSylvanParametricCtmcSymbolicSylvanParametricDtmcSymbolicSylvanParametricMASymbolicSylvanParametricMdpSymbolicSylvanParametricRewardModelSymbolicSylvanRewardModelTimeOperatorUnaryBooleanStateFormulaUnaryPathFormulaUnaryStateFormulaUntilFormulaValuationVariablebuild_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_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_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_symbolic()create_filter_symbolic()deprecated()eliminate_ECs()eliminate_non_markovian_chains()eliminate_reward_accumulations()export_to_drn()get_boolean_value()get_boolean_values_states()get_integer_value()get_integer_values_states()get_maximal_end_components()get_rational_value()get_rational_values_states()get_reachable_states()get_value()get_values_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()reset_timeout()set_loglevel_debug()set_loglevel_error()set_loglevel_trace()set_settings()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_DoubleBdd_SylvanBitVectorChoiceLabelingChoiceOriginsDdManager_SylvanDdMetaVariableTypeDdMetaVariable_SylvanDd_SylvanDiceStringVisitorDistributionDistributionExactDistributionIntervalExactSparseMatrixExactSparseMatrixBuilderExactSparseMatrixEntryExactSparseMatrixRowsExpressionExpressionManagerExpressionParserExpressionTypeIntervalSparseMatrixIntervalSparseMatrixBuilderIntervalSparseMatrixEntryIntervalSparseMatrixRowsItemLabelingJaniAssignmentJaniAutomatonJaniChoiceOriginsJaniConstantJaniEdgeJaniEdgeDestinationJaniInformationObjectJaniLocationJaniLocationExpanderJaniModelJaniOrderedAssignmentsJaniScopeChangerJaniTemplateEdgeJaniTemplateEdgeDestinationJaniVariableJaniVariableSetMaximalEndComponentMaximalEndComponentDecomposition_doubleMaximalEndComponentDecomposition_exactMaximalEndComponentDecomposition_intervalMaximalEndComponentDecomposition_ratfuncModelTypeOperatorTypeOverlappingGuardAnalyserParametricSparseMatrixParametricSparseMatrixBuilderParametricSparseMatrixEntryParametricSparseMatrixRowsPolytopeDoublePolytopeExactPrismAssignmentPrismBooleanVariablePrismChoiceOriginsPrismCommandPrismConstantPrismIntegerVariablePrismLabelPrismModelTypePrismModulePrismProgramPrismRewardModelPrismUpdatePrismVariableSchedulerSchedulerChoiceSchedulerChoiceExactSchedulerChoiceIntervalSchedulerChoiceParametricSchedulerExactSchedulerIntervalSchedulerParametricSimpleValuationSparseCtmcSparseDtmcSparseExactCtmcSparseExactDtmcSparseExactMASparseExactMdpSparseExactModelActionSparseExactModelActionsSparseExactModelComponentsSparseExactModelStateSparseExactModelStatesSparseExactPomdpSparseExactRewardModelSparseExactSmgSparseIntervalCtmcSparseIntervalDtmcSparseIntervalMASparseIntervalMdpSparseIntervalModelActionSparseIntervalModelActionsSparseIntervalModelComponentsSparseIntervalModelStateSparseIntervalModelStatesSparseIntervalPomdpSparseIntervalRewardModelSparseIntervalSmgSparseMASparseMatrixSparseMatrixBuilderSparseMatrixEntrySparseMatrixRowsSparseMdpSparseModelActionSparseModelActionsSparseModelComponentsSparseModelStateSparseModelStatesSparseParametricCtmcSparseParametricDtmcSparseParametricMASparseParametricMdpSparseParametricModelActionSparseParametricModelActionsSparseParametricModelComponentsSparseParametricModelStateSparseParametricModelStatesSparseParametricPomdpSparseParametricRewardModelSparsePomdpSparseRewardModelSparseSmgStateLabelingStateValuationStateValuationsBuilderSymbolicSylvanCtmcSymbolicSylvanDtmcSymbolicSylvanMASymbolicSylvanMdpSymbolicSylvanParametricCtmcSymbolicSylvanParametricDtmcSymbolicSylvanParametricMASymbolicSylvanParametricMdpSymbolicSylvanParametricRewardModelSymbolicSylvanRewardModelValuationVariablebuild_parametric_sparse_matrix()build_sparse_matrix()collect_information()deprecated()eliminate_reward_accumulations()get_boolean_value()get_boolean_values_states()get_integer_value()get_integer_values_states()get_maximal_end_components()get_rational_value()get_rational_values_states()get_value()get_values_states()
- 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
DtmcParameterLiftingModelCheckerMdpParameterLiftingModelCheckerModelInstantiatorModelTypePCtmcExactInstantiationCheckerPCtmcInstantiationCheckerPCtmcInstantiatorPDtmcExactInstantiationCheckerPDtmcInstantiationCheckerPDtmcInstantiatorPMaInstantiatorPMdpExactInstantiationCheckerPMdpInstantiationCheckerPMdpInstantiatorParameterRegionPartialPCtmcInstantiatorPartialPDtmcInstantiatorPartialPMaInstantiatorPartialPMdpInstantiatorRegionModelCheckerRegionResultRegionResultHypothesisStormErrorcreate_region_checker()gather_derivatives()simplify_model()
- Pycarl core
- Pycarl convert
- Pycarl formula
- Pycarl parse