Stormpy.pars¶

class DtmcParameterLiftingModelChecker(self: stormpy.pars._pars.DtmcParameterLiftingModelChecker)¶

Region model checker for DTMCs

get_bound_all_states(self: stormpy.pars._pars.DtmcParameterLiftingModelChecker, environment: stormpy._core.Environment, region: stormpy.pars._pars.ParameterRegion, maximise: bool = True) → stormpy._core.ExplicitQuantitativeCheckResult¶: Get bound

class MdpParameterLiftingModelChecker(self: stormpy.pars._pars.MdpParameterLiftingModelChecker)¶

Region model checker for MPDs

get_bound_all_states(self: stormpy.pars._pars.MdpParameterLiftingModelChecker, environment: stormpy._core.Environment, region: stormpy.pars._pars.ParameterRegion, maximise: bool = True) → stormpy._core.ExplicitQuantitativeCheckResult¶: Get bound

class ModelInstantiator(model)¶

Class for instantiating models.

Constructor. :param model: Model.

instantiate(valuation)¶: Instantiate model with given valuation. :param valuation: Valuation from parameter to value. :return: Instantiated model.

class ModelType(*values)¶

Type of the model

CTMC = 1¶

DTMC = 0¶

MA = 3¶

MDP = 2¶

POMDP = 5¶

SMG = 6¶

class PCtmcExactInstantiationChecker(self: stormpy.pars._pars.PCtmcExactInstantiationChecker, parametric model: stormpy.storage._storage.SparseParametricCtmc)¶

Instantiate pCTMCs to exact CTMCs and immediately check

check(self: stormpy.pars._pars.PCtmcExactInstantiationChecker, env: stormpy._core.Environment, instantiation: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy._core._CheckResult¶

set_graph_preserving(self: stormpy.pars._pars.PCtmcExactInstantiationChecker, value: bool) → None¶

class PCtmcInstantiationChecker(self: stormpy.pars._pars.PCtmcInstantiationChecker, parametric model: stormpy.storage._storage.SparseParametricCtmc)¶

Instantiate pCTMCs to CTMCs and immediately check

check(self: stormpy.pars._pars.PCtmcInstantiationChecker, env: stormpy._core.Environment, instantiation: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy._core._CheckResult¶

set_graph_preserving(self: stormpy.pars._pars.PCtmcInstantiationChecker, value: bool) → None¶

class PCtmcInstantiator(self: stormpy.pars._pars.PCtmcInstantiator, parametric model: stormpy.storage._storage.SparseParametricCtmc)¶

Instantiate PCTMCs to CTMCs

instantiate(self: stormpy.pars._pars.PCtmcInstantiator, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.storage._storage.SparseCtmc¶: Instantiate model with given parameter values

class PDtmcExactInstantiationChecker(self: stormpy.pars._pars.PDtmcExactInstantiationChecker, parametric model: stormpy.storage._storage.SparseParametricDtmc)¶

Instantiate pDTMCs to exact DTMCs and immediately check

check(self: stormpy.pars._pars.PDtmcExactInstantiationChecker, env: stormpy._core.Environment, instantiation: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy._core._CheckResult¶

set_graph_preserving(self: stormpy.pars._pars.PDtmcExactInstantiationChecker, value: bool) → None¶

class PDtmcInstantiationChecker(self: stormpy.pars._pars.PDtmcInstantiationChecker, parametric model: stormpy.storage._storage.SparseParametricDtmc)¶

Instantiate pDTMCs to DTMCs and immediately check

check(self: stormpy.pars._pars.PDtmcInstantiationChecker, env: stormpy._core.Environment, instantiation: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy._core._CheckResult¶

set_graph_preserving(self: stormpy.pars._pars.PDtmcInstantiationChecker, value: bool) → None¶

class PDtmcInstantiator(self: stormpy.pars._pars.PDtmcInstantiator, parametric model: stormpy.storage._storage.SparseParametricDtmc)¶

Instantiate PDTMCs to DTMCs

instantiate(self: stormpy.pars._pars.PDtmcInstantiator, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.storage._storage.SparseDtmc¶: Instantiate model with given parameter values

class PMaInstantiator(self: stormpy.pars._pars.PMaInstantiator, parametric model: stormpy.storage._storage.SparseParametricMA)¶

Instantiate PMAs to MAs

instantiate(self: stormpy.pars._pars.PMaInstantiator, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.storage._storage.SparseMA¶: Instantiate model with given parameter values

class PMdpExactInstantiationChecker(self: stormpy.pars._pars.PMdpExactInstantiationChecker, parametric model: stormpy.storage._storage.SparseParametricMdp)¶

Instantiate PMDP to exact MDPs and immediately check

check(self: stormpy.pars._pars.PMdpExactInstantiationChecker, env: stormpy._core.Environment, instantiation: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy._core._CheckResult¶

set_graph_preserving(self: stormpy.pars._pars.PMdpExactInstantiationChecker, value: bool) → None¶

class PMdpInstantiationChecker(self: stormpy.pars._pars.PMdpInstantiationChecker, parametric model: stormpy.storage._storage.SparseParametricMdp)¶

Instantiate PMDP to MDPs and immediately check

check(self: stormpy.pars._pars.PMdpInstantiationChecker, env: stormpy._core.Environment, instantiation: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy._core._CheckResult¶

set_graph_preserving(self: stormpy.pars._pars.PMdpInstantiationChecker, value: bool) → None¶

class PMdpInstantiator(self: stormpy.pars._pars.PMdpInstantiator, parametric model: stormpy.storage._storage.SparseParametricMdp)¶

Instantiate PMDPs to MDPs

instantiate(self: stormpy.pars._pars.PMdpInstantiator, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.storage._storage.SparseMdp¶: Instantiate model with given parameter values

class ParameterRegion(self: stormpy.pars._pars.ParameterRegion, valuation: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, tuple[stormpy.pycarl.cln.Rational, stormpy.pycarl.cln.Rational]])¶

Parameter region

Create region from valuation of var -> (lower_bound, upper_bound)

property area¶: Get area

static create_from_string(region_string: str, variables: collections.abc.Set[stormpy.pycarl._pycarl_core.Variable]) → stormpy.pars._pars.ParameterRegion¶: Create region from string

class PartialPCtmcInstantiator(self: stormpy.pars._pars.PartialPCtmcInstantiator, parametric model: stormpy.storage._storage.SparseParametricCtmc)¶

Instantiate PCTMCs to CTMCs

instantiate(self: stormpy.pars._pars.PartialPCtmcInstantiator, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.storage._storage.SparseParametricCtmc¶: Instantiate model with given parameter values

class PartialPDtmcInstantiator(self: stormpy.pars._pars.PartialPDtmcInstantiator, parametric model: stormpy.storage._storage.SparseParametricDtmc)¶

Instantiate PDTMCs to DTMCs

instantiate(self: stormpy.pars._pars.PartialPDtmcInstantiator, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.storage._storage.SparseParametricDtmc¶: Instantiate model with given parameter values

class PartialPMaInstantiator(self: stormpy.pars._pars.PartialPMaInstantiator, parametric model: stormpy.storage._storage.SparseParametricMA)¶

Instantiate PMAs to MAs

instantiate(self: stormpy.pars._pars.PartialPMaInstantiator, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.storage._storage.SparseParametricMA¶: Instantiate model with given parameter values

class PartialPMdpInstantiator(self: stormpy.pars._pars.PartialPMdpInstantiator, parametric model: stormpy.storage._storage.SparseParametricMdp)¶

Instantiate PMDPs to MDPs

instantiate(self: stormpy.pars._pars.PartialPMdpInstantiator, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.storage._storage.SparseParametricMdp¶: Instantiate model with given parameter values

class RegionModelChecker¶

Region model checker via paramater lifting

check_region(self: stormpy.pars._pars.RegionModelChecker, environment: stormpy._core.Environment, region: stormpy.pars._pars.ParameterRegion, hypothesis: stormpy.pars._pars.RegionResultHypothesis = <RegionResultHypothesis.UNKNOWN: 0>, sampleVertices: bool = False) → stormpy.pars._pars.RegionResult¶: Check region

get_bound(self: stormpy.pars._pars.RegionModelChecker, environment: stormpy._core.Environment, region: stormpy.pars._pars.ParameterRegion, maximise: bool = True) → stormpy.pycarl.cln.Rational¶: Get bound

get_split_suggestion(self: stormpy.pars._pars.RegionModelChecker, relevant_parameters: collections.abc.Set[stormpy.pycarl._pycarl_core.Variable]) → list[stormpy.pycarl.cln.Rational]¶: Get region split estimates

specify(self: stormpy.pars._pars.RegionModelChecker, environment: stormpy._core.Environment, model: stormpy.storage._storage._SparseParametricModel, formula: stormpy.logic._logic.Formula, splitting_estimate: storm::modelchecker::RegionSplitEstimateKind | None = None, allow_model_simplification: bool = True, graph_preserving: bool = True) → None¶: specify arguments

class RegionRefinementChecker¶

Region refinement checker

compute_extremum(self: stormpy.pars._pars.RegionRefinementChecker, environment: stormpy._core.Environment, region: stormpy.pars._pars.ParameterRegion, extremum_direction: stormpy._core.OptimizationDirection, precision: stormpy.pycarl.cln.Rational, precision_absolute: bool = False) → tuple[stormpy.pycarl.cln.Rational, dict[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]]¶: Compute extremum value and point with precision

specify(self: stormpy.pars._pars.RegionRefinementChecker, environment: stormpy._core.Environment, model: stormpy.storage._storage._SparseParametricModel, formula: stormpy.logic._logic.Formula, allow_model_simplification: bool = True, graph_preserving: bool = True) → None¶: specify arguments

class RegionResult(*values)¶

Types of region check results

ALLSAT = 8¶

ALLVIOLATED = 9¶

CENTERSAT = 4¶

CENTERVIOLATED = 5¶

EXISTSBOTH = 7¶

EXISTSSAT = 1¶

EXISTSVIOLATED = 2¶

UNKNOWN = 0¶

friendly_name(self: stormpy.pars._pars.RegionResult) → str¶

class RegionResultHypothesis(*values)¶

Hypothesis for the result of a parameter region

ALLSAT = 1¶

ALLVIOLATED = 2¶

UNKNOWN = 0¶

friendly_name(self: stormpy.pars._pars.RegionResultHypothesis) → str¶

create_region_checker(environment: stormpy._core.Environment, model: stormpy.storage._storage._SparseParametricModel, formula: stormpy.logic._logic.Formula, allow_model_simplification: bool = True, graph_preserving: bool = True, preconditions_validated_manually: bool = False) → stormpy.pars._pars.RegionModelChecker¶: Create region checker

create_region_refinement_checker(environment: stormpy._core.Environment, model: stormpy.storage._storage._SparseParametricModel, formula: stormpy.logic._logic.Formula, allow_model_simplification: bool = True, graph_preserving: bool = True, preconditions_validated_manually: bool = False) → stormpy.pars._pars.RegionRefinementChecker¶: Create region refinement checker

gather_derivatives(model: stormpy.storage._storage._SparseParametricModel, var: stormpy.pycarl._pycarl_core.Variable) → set[stormpy.pycarl.cln.FactorizedPolynomial]¶: Gather all derivatives of transition probabilities

simplify_model(model, formula)¶: Simplify parametric model preserving the given formula by eliminating states with constant outgoing probabilities. :param model: Model. :param formula: Formula. :return: Tuple of simplified model and simplified formula.