SparseMdpParameterLiftingModelChecker¶

Warning

The stormpy developer API is internal and can be subject to change.

Region model checker for MDPs

analyze_region( self: stormpy.pars.developer._pars.RegionModelChecker, environment: stormpy.environments.Environment, region: stormpy.pars.ParameterRegion, hypothesis: stormpy.pars.developer._pars.RegionResultHypothesis = <RegionResultHypothesis.UNKNOWN: 0>, sample_vertices_of_region: bool = False, ) → stormpy.pars.RegionResult¶: Analyze region

get_bound( self: stormpy.pars.developer._pars.SparseMdpParameterLiftingModelChecker, environment: stormpy.environments.Environment, region: stormpy.pars.ParameterRegion, dir_for_parameters: stormpy.logic.OptimizationDirection, ) → stormpy.developer._core._ExplicitQuantitativeCheckResult_Double¶: Get bounds for all states

get_bound_at_init_state( self: stormpy.pars.developer._pars.RegionModelChecker, environment: stormpy.environments.Environment, region: stormpy.pars.ParameterRegion, dir_for_parameters: stormpy.logic.OptimizationDirection, ) → stormpy.numbers.RationalFunctionCoefficient¶: Get bound at the initial state

obtain_region_split_estimates( self: stormpy.pars.developer._pars.RegionModelChecker, relevant_parameters: collections.abc.Set[stormpy.numbers.Variable], ) → list[stormpy.numbers.RationalFunctionCoefficient]¶: Get region split estimates

specify( self: stormpy.pars.developer._pars.RegionModelChecker, environment: stormpy.environments.Environment, model: stormpy.developer.storage._storage._SparseModel_RationalFunction, check_task: stormpy.developer._core._CheckTask_RationalFunction, generate_region_split_estimates: stormpy.pars.developer._pars.RegionSplitEstimateKind | None = None, allow_model_simplifications: bool = True, graph_preservation_status: stormpy.pars.developer._pars.GraphPreservationStatus = <GraphPreservationStatus.GRAPH_PRESERVING: 2>, ) → None¶: Specify model and check task