Stormpy.exceptions¶
- exception StormError(message)¶
Base class for exceptions in Storm.
Contents:
Modules:
ActionMaskDoubleAtomicExpressionFormulaAtomicLabelFormulaBdd_SylvanBinaryBooleanOperatorTypeBinaryPathFormulaBinaryStateFormulaBisimulationTypeBitVectorBooleanBinaryStateFormulaBooleanLiteralFormulaBoundedUntilFormulaBuilderOptionsCheckTaskChoiceLabelingChoiceOriginsComparisonTypeConditionalFormulaConstraintCollectorCumulativeRewardFormulaDdManager_SylvanDdMetaVariableTypeDdMetaVariable_SylvanDd_SylvanDiceStringVisitorDirectEncodingOptionsDirectEncodingParserOptionsDistributionDoubleEliminationLabelBehaviorEndComponentEliminatorReturnTypeDoubleEnvironmentEquationSolverTypeEventuallyFormulaExactCheckTaskExactSparseMatrixExactSparseMatrixBuilderExactSparseMatrixEntryExactSparseMatrixRowsExplicitExactQuantitativeCheckResultExplicitModelBuilderExplicitModelCheckerHintDoubleExplicitParametricModelBuilderExplicitParametricQuantitativeCheckResultExplicitParetoCurveCheckResultDoubleExplicitQualitativeCheckResultExplicitQuantitativeCheckResultExplicitStateLookupExpressionExpressionManagerExpressionParserExpressionTypeFactorizedPolynomialFactorizedRationalFunctionFlatSetFormulaGloballyFormulaHybridExactQuantitativeCheckResultHybridParametricQuantitativeCheckResultHybridQuantitativeCheckResultInstantaneousRewardFormulaItemLabelingJaniAssignmentJaniAutomatonJaniChoiceOriginsJaniConstantJaniEdgeJaniEdgeDestinationJaniInformationObjectJaniLocationJaniLocationExpanderJaniModelJaniModelTypeJaniOrderedAssignmentsJaniScopeChangerJaniTemplateEdgeJaniTemplateEdgeDestinationJaniVariableJaniVariableSetLongRunAvarageOperatorLongRunAverageRewardFormulaMaximalEndComponentMaximalEndComponentDecomposition_doubleMaximalEndComponentDecomposition_exactMaximalEndComponentDecomposition_ratfuncMinMaxMethodMinMaxSolverEnvironmentModelCheckerHintModelFormulasPairModelTypeMultiObjectiveFormulaNativeLinearEquationSolverMethodNativeSolverEnvironmentOperatorFormulaOperatorTypeOptimizationDirectionOverlappingGuardAnalyserParametricCheckTaskParametricSparseMatrixParametricSparseMatrixBuilderParametricSparseMatrixEntryParametricSparseMatrixRowsParetoCurveCheckResultDoublePathFormulaPolynomialPolytopeDoublePolytopeExactPrismAssignmentPrismBooleanVariablePrismChoiceOriginsPrismCommandPrismConstantPrismIntegerVariablePrismLabelPrismModelTypePrismModulePrismProgramPrismRewardModelPrismUpdatePrismVariableProbabilityOperatorPropertyQuotientFormatRationalRationalFunctionRationalRFRewardOperatorSMTCounterExampleGeneratorSMTCounterExampleGeneratorOptionsSMTCounterExampleGeneratorStatsSMTCounterExampleInputSchedulerChoiceDoubleSchedulerChoiceExactSchedulerChoiceParametricSchedulerDoubleSchedulerExactSchedulerParametricSimpleValuationSolverEnvironmentSparseCtmcSparseDtmcSparseExactCtmcSparseExactDtmcSparseExactMASparseExactMdpSparseExactModelActionSparseExactModelActionsSparseExactModelComponentsSparseExactModelStateSparseExactModelStatesSparseExactPomdpSparseExactRewardModelSparseMASparseMatrixSparseMatrixBuilderSparseMatrixEntrySparseMatrixRowsSparseMdpSparseModelActionSparseModelActionsSparseModelComponentsSparseModelStateSparseModelStatesSparseParametricCtmcSparseParametricDtmcSparseParametricMASparseParametricMdpSparseParametricModelActionSparseParametricModelActionsSparseParametricModelStateSparseParametricModelStatesSparseParametricPomdpSparseParametricRewardModelSparsePomdpSparseRewardModelStateFormulaStateLabelingStateValuationStateValuationFunctionActionMaskDoubleStateValuationsBuilderStormErrorSubsystemBuilderOptionsSubsystemBuilderReturnTypeDoubleSubsystemBuilderReturnTypeExactSubsystemBuilderReturnTypeRatFuncSymbolicExactQuantitativeCheckResultSymbolicModelDescriptionSymbolicParametricQuantitativeCheckResultSymbolicQualitativeCheckResultSymbolicQuantitativeCheckResultSymbolicSylvanCtmcSymbolicSylvanDtmcSymbolicSylvanMASymbolicSylvanMdpSymbolicSylvanParametricCtmcSymbolicSylvanParametricDtmcSymbolicSylvanParametricMASymbolicSylvanParametricMdpSymbolicSylvanParametricRewardModelSymbolicSylvanRewardModelTimeOperatorUnaryBooleanStateFormulaUnaryPathFormulaUnaryStateFormulaUntilFormulaVariablebuild_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_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_transient_probabilities()construct_submodel()create_filter_initial_states_sparse()create_filter_initial_states_symbolic()create_filter_symbolic()eliminate_ECs()eliminate_non_markovian_chains()eliminate_reward_accumulations()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()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()AtomicExpressionFormulaAtomicLabelFormulaBinaryBooleanOperatorTypeBinaryPathFormulaBinaryStateFormulaBooleanBinaryStateFormulaBooleanLiteralFormulaBoundedUntilFormulaComparisonTypeConditionalFormulaCumulativeRewardFormulaEventuallyFormulaFormulaGloballyFormulaInstantaneousRewardFormulaLongRunAvarageOperatorLongRunAverageRewardFormulaMultiObjectiveFormulaOperatorFormulaPathFormulaProbabilityOperatorRewardOperatorStateFormulaTimeOperatorUnaryBooleanStateFormulaUnaryPathFormulaUnaryStateFormulaUntilFormulaBdd_SylvanBitVectorChoiceLabelingChoiceOriginsDdManager_SylvanDdMetaVariableTypeDdMetaVariable_SylvanDd_SylvanDiceStringVisitorDistributionDoubleExactSparseMatrixExactSparseMatrixBuilderExactSparseMatrixEntryExactSparseMatrixRowsExpressionExpressionManagerExpressionParserExpressionTypeItemLabelingJaniAssignmentJaniAutomatonJaniChoiceOriginsJaniConstantJaniEdgeJaniEdgeDestinationJaniInformationObjectJaniLocationJaniLocationExpanderJaniModelJaniOrderedAssignmentsJaniScopeChangerJaniTemplateEdgeJaniTemplateEdgeDestinationJaniVariableJaniVariableSetMaximalEndComponentMaximalEndComponentDecomposition_doubleMaximalEndComponentDecomposition_exactMaximalEndComponentDecomposition_ratfuncModelTypeOperatorTypeOverlappingGuardAnalyserParametricSparseMatrixParametricSparseMatrixBuilderParametricSparseMatrixEntryParametricSparseMatrixRowsPolytopeDoublePolytopeExactPrismAssignmentPrismBooleanVariablePrismChoiceOriginsPrismCommandPrismConstantPrismIntegerVariablePrismLabelPrismModelTypePrismModulePrismProgramPrismRewardModelPrismUpdatePrismVariableSchedulerChoiceDoubleSchedulerChoiceExactSchedulerChoiceParametricSchedulerDoubleSchedulerExactSchedulerParametricSimpleValuationSparseCtmcSparseDtmcSparseExactCtmcSparseExactDtmcSparseExactMASparseExactMdpSparseExactModelActionSparseExactModelActionsSparseExactModelComponentsSparseExactModelStateSparseExactModelStatesSparseExactPomdpSparseExactRewardModelSparseMASparseMatrixSparseMatrixBuilderSparseMatrixEntrySparseMatrixRowsSparseMdpSparseModelActionSparseModelActionsSparseModelComponentsSparseModelStateSparseModelStatesSparseParametricCtmcSparseParametricDtmcSparseParametricMASparseParametricMdpSparseParametricModelActionSparseParametricModelActionsSparseParametricModelStateSparseParametricModelStatesSparseParametricPomdpSparseParametricRewardModelSparsePomdpSparseRewardModelStateLabelingStateValuationStateValuationsBuilderSymbolicSylvanCtmcSymbolicSylvanDtmcSymbolicSylvanMASymbolicSylvanMdpSymbolicSylvanParametricCtmcSymbolicSylvanParametricDtmcSymbolicSylvanParametricMASymbolicSylvanParametricMdpSymbolicSylvanParametricRewardModelSymbolicSylvanRewardModelVariablebuild_parametric_sparse_matrix()build_sparse_matrix()collect_information()eliminate_reward_accumulations()get_maximal_end_components()ApproximationHeuristicDFTBE_doubleDFTBE_ratfuncDFTDependency_doubleDFTDependency_ratfuncDFTElementTypeDFTElement_doubleDFTElement_ratfuncDFTInstantiatorDFTSimulator_doubleDFTSimulator_ratfuncDFTStateInfoDFTState_doubleDFTState_ratfuncDFTSymmetriesDFT_doubleDFT_ratfuncDftIndependentModuleExplicitDFTModelBuilder_doubleExplicitDFTModelBuilder_ratfuncFailableElementFailableElementsFailableIteratorRandomGeneratorRelevantEventsSimulationResultanalyze_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()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()DtmcParameterLiftingModelCheckerMdpParameterLiftingModelCheckerModelInstantiatorModelTypePCtmcExactInstantiationCheckerPCtmcInstantiationCheckerPCtmcInstantiatorPDtmcExactInstantiationCheckerPDtmcInstantiationCheckerPDtmcInstantiatorPMaInstantiatorPMdpExactInstantiationCheckerPMdpInstantiationCheckerPMdpInstantiatorParameterRegionPartialPCtmcInstantiatorPartialPDtmcInstantiatorPartialPMaInstantiatorPartialPMdpInstantiatorRegionModelCheckerRegionResultRegionResultHypothesisStormErrorcreate_region_checker()gather_derivatives()simplify_model()