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

CTMC = ModelType.CTMC

DTMC = ModelType.DTMC

MA = ModelType.MA

MDP = ModelType.MDP

POMDP = ModelType.POMDP

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._PDtmcExactInstantiationCheckerBase, 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._PDtmcInstantiationCheckerBase, 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._PMdpExactInstantiationCheckerBase, 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._PMdpInstantiationCheckerBase, 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

create_from_string(region_string: str, variables: Set[pycarl.core.Variable], splitting_threshold: Optional[int] = None) → 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, initialResult: stormpy.pars.pars.RegionResult = RegionResult.UNKNOWN, 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) → 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

ALLSAT = RegionResult.ALLSAT

ALLVIOLATED = RegionResult.ALLVIOLATED

CENTERSAT = RegionResult.CENTERSAT

CENTERVIOLATED = RegionResult.CENTERVIOLATED

EXISTSBOTH = RegionResult.EXISTSBOTH

EXISTSSAT = RegionResult.EXISTSSAT

EXISTSVIOLATED = RegionResult.EXISTSVIOLATED

UNKNOWN = RegionResult.UNKNOWN

class RegionResultHypothesis

Hypothesis for the result of a parameter region

ALLSAT = RegionResultHypothesis.ALLSAT

ALLVIOLATED = RegionResultHypothesis.ALLVIOLATED

UNKNOWN = RegionResultHypothesis.UNKNOWN

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) → 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.