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(self: stormpy.storage._storage.ModelType, value: SupportsInt)

Type of the model

Members:

DTMC

MDP

POMDP

CTMC

MA

SMG

CTMC = <ModelType.CTMC: 1>

DTMC = <ModelType.DTMC: 0>

MA = <ModelType.MA: 3>

MDP = <ModelType.MDP: 2>

POMDP = <ModelType.POMDP: 5>

SMG = <ModelType.SMG: 6>

property name

property value

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>, initialResult: stormpy.pars._pars.RegionResult = <RegionResult.UNKNOWN: 0>, sampleVertices: bool = False) → stormpy.pars._pars.RegionResult

Check region

compute_extremum(self: stormpy.pars._pars.RegionModelChecker, 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.FactorizedRationalFunction, dict[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]]

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

Get bound

get_split_suggestion(self: stormpy.pars._pars.RegionModelChecker) → dict[stormpy.pycarl._pycarl_core.Variable, float]

Get estimate

specify(self: stormpy.pars._pars.RegionModelChecker, environment: stormpy._core.Environment, model: stormpy.storage._storage._SparseParametricModel, formula: stormpy.logic._logic.Formula, generate_splitting_estimate: bool = False, allow_model_simplification: bool = True) → None

specify arguments

class RegionResult(self: stormpy.pars._pars.RegionResult, value: SupportsInt)

Types of region check results

Members:

EXISTSSAT

EXISTSVIOLATED

EXISTSBOTH

CENTERSAT

CENTERVIOLATED

ALLSAT

ALLVIOLATED

UNKNOWN

ALLSAT = <RegionResult.ALLSAT: 6>

ALLVIOLATED = <RegionResult.ALLVIOLATED: 7>

CENTERSAT = <RegionResult.CENTERSAT: 3>

CENTERVIOLATED = <RegionResult.CENTERVIOLATED: 4>

EXISTSBOTH = <RegionResult.EXISTSBOTH: 5>

EXISTSSAT = <RegionResult.EXISTSSAT: 1>

EXISTSVIOLATED = <RegionResult.EXISTSVIOLATED: 2>

UNKNOWN = <RegionResult.UNKNOWN: 0>

property name

property value

class RegionResultHypothesis(self: stormpy.pars._pars.RegionResultHypothesis, value: SupportsInt)

Hypothesis for the result of a parameter region

Members:

UNKNOWN

ALLSAT

ALLVIOLATED

ALLSAT = <RegionResultHypothesis.ALLSAT: 1>

ALLVIOLATED = <RegionResultHypothesis.ALLVIOLATED: 2>

UNKNOWN = <RegionResultHypothesis.UNKNOWN: 0>

property name

property value

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

Create region 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.