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]) → stormpy.pars.pars.ParameterRegion¶: Create region from string

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.