stormpy.pars

Parameter synthesis and model instantiation for sparse parametric models.

Create parameter regions, verify properties throughout a region, compute extremal values, or search for satisfying parameter valuations. Instantiate models with concrete parameter values using ModelInstantiator. Lower-level tools are in stormpy.pars.developer.

Functions

check_feasibility(model, property, *[, ...])	Search for a well-defined parameter valuation satisfying a bounded probability or reward property.
compute_extremal_value(model, property, *, ...)	Compute an extremal probability or expected reward over a parameter region.
create_region(bounds)	Create a parameter region from bounds for each parameter.
gather_derivatives(model, parameter)	Gather the nonconstant numerators of transition-probability derivatives with respect to a parameter
parse_region(region_string, parameters)	Parse a parameter region from a string.
verify(model, property, *[, region, ...])	Verify a bounded probability or reward property for all well-defined valuations in a region.

Classes

ConstraintCollector(self, model)	Collector for constraints on parametric Markov chains
FeasibilityMethod(*values)	Methods for feasibility synthesis
FeasibilityResult	A satisfying parameter valuation and its value at the initial state
FeasibilitySynthesisResult	Feasibility decision: EXISTS_SAT, ALL_VIOLATED, or UNKNOWN, with an optional witness
ModelInstantiator	Instantiate a parametric model
ParameterRegion(self, lower_boundaries, ...)	Parameter region given by lower and upper bounds for each parameter
RegionCheckEngine(*values)	Region checking engines, controlling the arithmetic and supported regions.
RegionResult(*values)	Types of region check results