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