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
-
property
-
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.