Stormpy.pars¶

class DtmcParameterLiftingModelChecker¶

Region model checker for DTMCs

get_bound_all_states()¶: Get bound

class MdpParameterLiftingModelChecker¶

Region model checker for MPDs

get_bound_all_states()¶: 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()¶: Instantiate model with given parameter values

class PDtmcInstantiationChecker¶

Instantiate pDTMCs to DTMCs and immediately check

check()¶

set_graph_preserving()¶

class PDtmcInstantiator¶

Instantiate PDTMCs to DTMCs

instantiate()¶: Instantiate model with given parameter values

class PMaInstantiator¶

Instantiate PMAs to MAs

instantiate()¶: Instantiate model with given parameter values

class PMdpInstantiationChecker¶

Instantiate PMDP to MDPs and immediately check

check()¶

set_graph_preserving()¶

class PMdpInstantiator¶

Instantiate PMDPs to MDPs

instantiate()¶: Instantiate model with given parameter values

class ParameterRegion¶: Parameter region

class RegionModelChecker¶

Region model checker via paramater lifting

check_region()¶: Check region

get_bound()¶: Get bound

get_split_suggestion()¶: Get estimate

specify()¶: 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()¶: Create region checker

gather_derivatives()¶: 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.