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

CTMC = <ModelType.CTMC: 1>

DTMC = <ModelType.DTMC: 0>

MA = <ModelType.MA: 3>

MDP = <ModelType.MDP: 2>

POMDP = <ModelType.POMDP: 5>

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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Set[pycarl.core.Variable]) → stormpy.pars.pars.ParameterRegion

Create region from string

class PartialPCtmcInstantiator

Instantiate PCTMCs to CTMCs

instantiate(self: stormpy.pars.pars.PartialPCtmcInstantiator, arg0: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: Dict[pycarl.core.Variable, pycarl.cln.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: pycarl.cln.cln.Rational, precision_absolute: bool = False) → Tuple[pycarl.cln.cln.FactorizedRationalFunction, Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]]

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

Get bound

get_split_suggestion(self: stormpy.pars.pars.RegionModelChecker) → Dict[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>

name()

__str__(*args, **kwargs) Overloaded function.

1. __str__(self: stormpy.pars.pars.RegionResult) -> str

2. __str__(self: handle) -> str

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>

name()

__str__(*args, **kwargs) Overloaded function.

1. __str__(self: stormpy.pars.pars.RegionResultHypothesis) -> str

2. __str__(self: handle) -> str

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: pycarl.core.Variable) → Set[pycarl.cln.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.