RegionModelChecker

Warning

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

class RegionModelChecker

Bases: pybind11_object

Region model checker via parameter lifting

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_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