Stormpy.pars¶

class 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¶

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.

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

class ModelType¶

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¶

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¶

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¶

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¶

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¶

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¶

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¶

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¶

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¶

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¶

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¶

Parameter region

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¶

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¶

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¶

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¶

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¶

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¶

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¶

exception StormError(message)¶: Base class for exceptions in Storm.

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.