Stormpy.exceptions¶
- exception StormError(message)¶
Base class for exceptions in Storm.
Contents:
Modules:
ActionMaskDouble
AtomicExpressionFormula
AtomicLabelFormula
Bdd_Sylvan
BinaryBooleanOperatorType
BinaryPathFormula
BinaryStateFormula
BisimulationType
BitVector
BooleanBinaryStateFormula
BooleanLiteralFormula
BoundedUntilFormula
BuilderOptions
CheckTask
ChoiceLabeling
ChoiceOrigins
ComparisonType
ConditionalFormula
ConstraintCollector
CumulativeRewardFormula
DdManager_Sylvan
DdMetaVariableType
DdMetaVariable_Sylvan
Dd_Sylvan
DiceStringVisitor
DirectEncodingOptions
DirectEncodingParserOptions
DistributionDouble
EliminationLabelBehavior
EndComponentEliminatorReturnTypeDouble
Environment
EquationSolverType
EventuallyFormula
ExactCheckTask
ExactSparseMatrix
ExactSparseMatrixBuilder
ExactSparseMatrixEntry
ExactSparseMatrixRows
ExplicitExactQuantitativeCheckResult
ExplicitModelBuilder
ExplicitModelCheckerHintDouble
ExplicitParametricModelBuilder
ExplicitParametricQuantitativeCheckResult
ExplicitParetoCurveCheckResultDouble
ExplicitQualitativeCheckResult
ExplicitQuantitativeCheckResult
ExplicitStateLookup
Expression
ExpressionManager
ExpressionParser
ExpressionType
FactorizedPolynomial
FactorizedRationalFunction
FlatSet
Formula
GloballyFormula
HybridExactQuantitativeCheckResult
HybridParametricQuantitativeCheckResult
HybridQuantitativeCheckResult
InstantaneousRewardFormula
ItemLabeling
JaniAssignment
JaniAutomaton
JaniChoiceOrigins
JaniConstant
JaniEdge
JaniEdgeDestination
JaniInformationObject
JaniLocation
JaniLocationExpander
JaniModel
JaniModelType
JaniOrderedAssignments
JaniScopeChanger
JaniTemplateEdge
JaniTemplateEdgeDestination
JaniVariable
JaniVariableSet
LongRunAvarageOperator
LongRunAverageRewardFormula
MaximalEndComponent
MaximalEndComponentDecomposition_double
MaximalEndComponentDecomposition_exact
MaximalEndComponentDecomposition_ratfunc
MinMaxMethod
MinMaxSolverEnvironment
ModelCheckerHint
ModelFormulasPair
ModelType
MultiObjectiveFormula
NativeLinearEquationSolverMethod
NativeSolverEnvironment
OperatorFormula
OperatorType
OptimizationDirection
OverlappingGuardAnalyser
ParametricCheckTask
ParametricSparseMatrix
ParametricSparseMatrixBuilder
ParametricSparseMatrixEntry
ParametricSparseMatrixRows
ParetoCurveCheckResultDouble
PathFormula
Polynomial
PolytopeDouble
PolytopeExact
PrismAssignment
PrismBooleanVariable
PrismChoiceOrigins
PrismCommand
PrismConstant
PrismIntegerVariable
PrismLabel
PrismModelType
PrismModule
PrismProgram
PrismRewardModel
PrismUpdate
PrismVariable
ProbabilityOperator
Property
QuotientFormat
Rational
RationalFunction
RationalRF
RewardOperator
SMTCounterExampleGenerator
SMTCounterExampleGeneratorOptions
SMTCounterExampleGeneratorStats
SMTCounterExampleInput
SchedulerChoiceDouble
SchedulerChoiceExact
SchedulerChoiceParametric
SchedulerDouble
SchedulerExact
SchedulerParametric
SimpleValuation
SolverEnvironment
SparseCtmc
SparseDtmc
SparseExactCtmc
SparseExactDtmc
SparseExactMA
SparseExactMdp
SparseExactModelAction
SparseExactModelActions
SparseExactModelComponents
SparseExactModelState
SparseExactModelStates
SparseExactPomdp
SparseExactRewardModel
SparseMA
SparseMatrix
SparseMatrixBuilder
SparseMatrixEntry
SparseMatrixRows
SparseMdp
SparseModelAction
SparseModelActions
SparseModelComponents
SparseModelState
SparseModelStates
SparseParametricCtmc
SparseParametricDtmc
SparseParametricMA
SparseParametricMdp
SparseParametricModelAction
SparseParametricModelActions
SparseParametricModelState
SparseParametricModelStates
SparseParametricPomdp
SparseParametricRewardModel
SparsePomdp
SparseRewardModel
StateFormula
StateLabeling
StateValuation
StateValuationFunctionActionMaskDouble
StateValuationsBuilder
StormError
SubsystemBuilderOptions
SubsystemBuilderReturnTypeDouble
SubsystemBuilderReturnTypeExact
SubsystemBuilderReturnTypeRatFunc
SymbolicExactQuantitativeCheckResult
SymbolicModelDescription
SymbolicParametricQuantitativeCheckResult
SymbolicQualitativeCheckResult
SymbolicQuantitativeCheckResult
SymbolicSylvanCtmc
SymbolicSylvanDtmc
SymbolicSylvanMA
SymbolicSylvanMdp
SymbolicSylvanParametricCtmc
SymbolicSylvanParametricDtmc
SymbolicSylvanParametricMA
SymbolicSylvanParametricMdp
SymbolicSylvanParametricRewardModel
SymbolicSylvanRewardModel
TimeOperator
UnaryBooleanStateFormula
UnaryPathFormula
UnaryStateFormula
UntilFormula
Variable
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_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()
AtomicExpressionFormula
AtomicLabelFormula
BinaryBooleanOperatorType
BinaryPathFormula
BinaryStateFormula
BooleanBinaryStateFormula
BooleanLiteralFormula
BoundedUntilFormula
ComparisonType
ConditionalFormula
CumulativeRewardFormula
EventuallyFormula
Formula
GloballyFormula
InstantaneousRewardFormula
LongRunAvarageOperator
LongRunAverageRewardFormula
MultiObjectiveFormula
OperatorFormula
PathFormula
ProbabilityOperator
RewardOperator
StateFormula
TimeOperator
UnaryBooleanStateFormula
UnaryPathFormula
UnaryStateFormula
UntilFormula
Bdd_Sylvan
BitVector
ChoiceLabeling
ChoiceOrigins
DdManager_Sylvan
DdMetaVariableType
DdMetaVariable_Sylvan
Dd_Sylvan
DiceStringVisitor
DistributionDouble
ExactSparseMatrix
ExactSparseMatrixBuilder
ExactSparseMatrixEntry
ExactSparseMatrixRows
Expression
ExpressionManager
ExpressionParser
ExpressionType
ItemLabeling
JaniAssignment
JaniAutomaton
JaniChoiceOrigins
JaniConstant
JaniEdge
JaniEdgeDestination
JaniInformationObject
JaniLocation
JaniLocationExpander
JaniModel
JaniOrderedAssignments
JaniScopeChanger
JaniTemplateEdge
JaniTemplateEdgeDestination
JaniVariable
JaniVariableSet
MaximalEndComponent
MaximalEndComponentDecomposition_double
MaximalEndComponentDecomposition_exact
MaximalEndComponentDecomposition_ratfunc
ModelType
OperatorType
OverlappingGuardAnalyser
ParametricSparseMatrix
ParametricSparseMatrixBuilder
ParametricSparseMatrixEntry
ParametricSparseMatrixRows
PolytopeDouble
PolytopeExact
PrismAssignment
PrismBooleanVariable
PrismChoiceOrigins
PrismCommand
PrismConstant
PrismIntegerVariable
PrismLabel
PrismModelType
PrismModule
PrismProgram
PrismRewardModel
PrismUpdate
PrismVariable
SchedulerChoiceDouble
SchedulerChoiceExact
SchedulerChoiceParametric
SchedulerDouble
SchedulerExact
SchedulerParametric
SimpleValuation
SparseCtmc
SparseDtmc
SparseExactCtmc
SparseExactDtmc
SparseExactMA
SparseExactMdp
SparseExactModelAction
SparseExactModelActions
SparseExactModelComponents
SparseExactModelState
SparseExactModelStates
SparseExactPomdp
SparseExactRewardModel
SparseMA
SparseMatrix
SparseMatrixBuilder
SparseMatrixEntry
SparseMatrixRows
SparseMdp
SparseModelAction
SparseModelActions
SparseModelComponents
SparseModelState
SparseModelStates
SparseParametricCtmc
SparseParametricDtmc
SparseParametricMA
SparseParametricMdp
SparseParametricModelAction
SparseParametricModelActions
SparseParametricModelState
SparseParametricModelStates
SparseParametricPomdp
SparseParametricRewardModel
SparsePomdp
SparseRewardModel
StateLabeling
StateValuation
StateValuationsBuilder
SymbolicSylvanCtmc
SymbolicSylvanDtmc
SymbolicSylvanMA
SymbolicSylvanMdp
SymbolicSylvanParametricCtmc
SymbolicSylvanParametricDtmc
SymbolicSylvanParametricMA
SymbolicSylvanParametricMdp
SymbolicSylvanParametricRewardModel
SymbolicSylvanRewardModel
Variable
build_parametric_sparse_matrix()
build_sparse_matrix()
collect_information()
eliminate_reward_accumulations()
get_maximal_end_components()
ApproximationHeuristic
DFTBE_double
DFTBE_ratfunc
DFTDependency_double
DFTDependency_ratfunc
DFTElementType
DFTElement_double
DFTElement_ratfunc
DFTInstantiator
DFTSimulator_double
DFTSimulator_ratfunc
DFTStateInfo
DFTState_double
DFTState_ratfunc
DFTSymmetries
DFT_double
DFT_ratfunc
DftIndependentModule
ExplicitDFTModelBuilder_double
ExplicitDFTModelBuilder_ratfunc
FailableElement
FailableElements
FailableIterator
RandomGenerator
RelevantEvents
SimulationResult
analyze_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()
DtmcParameterLiftingModelChecker
MdpParameterLiftingModelChecker
ModelInstantiator
ModelType
PCtmcExactInstantiationChecker
PCtmcInstantiationChecker
PCtmcInstantiator
PDtmcExactInstantiationChecker
PDtmcInstantiationChecker
PDtmcInstantiator
PMaInstantiator
PMdpExactInstantiationChecker
PMdpInstantiationChecker
PMdpInstantiator
ParameterRegion
PartialPCtmcInstantiator
PartialPDtmcInstantiator
PartialPMaInstantiator
PartialPMdpInstantiator
RegionModelChecker
RegionResult
RegionResultHypothesis
StormError
create_region_checker()
gather_derivatives()
simplify_model()