stormpy.pars.developer

Warning

The stormpy developer API is internal and can be subject to change.

Raw pybind11 bindings for storm-pars.

This module is only meant for developers. Use stormpy.pars for the public API.

The naming of functions and classes of the bindings mirrors the corresponding storm::pars C++ functions and classes.

Functions

check_feasibility(...)	Find a well-defined valuation satisfying a bounded probability or reward formula
initialize_region_model_checker(environment, ...)	Create and specify a region model checker
initialize_region_refinement_checker(...)	Create and specify a region refinement checker
parse_region(input_string, considered_variables)	Parse region from string, e.g. 0.3<=p<=0.5,0.1<=q<=0.4.
verify(-> bool verify)	Verify a bounded probability or reward formula for all well-defined valuations in the region

Classes

GraphPreservationStatus(*values)	Guarantee whether the graph structure is preserved within a region
RegionModelChecker	Region model checker via parameter lifting
RegionRefinementChecker	Region refinement checker
RegionResultHypothesis(*values)	Hypothesis for the result of a parameter region
RegionSplitEstimateKind(*values)	Kinds of estimates for splitting regions
SparseDtmcParameterLiftingModelChecker(self)	Region model checker for DTMCs
SparseInstantiationModelChecker	Instantiate and check a parametric model
SparseMdpParameterLiftingModelChecker(self)	Region model checker for MDPs
SparseParametricModelSimplifier	Model simplifier for parametric DTMCs