check_feasibility

Warning

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

check_feasibility(

environment: stormpy.environments.Environment,

model: stormpy.developer.storage._storage._SparseModel_RationalFunction,

formula: stormpy.logic.Formula,

region: stormpy.pars.ParameterRegion,

method: stormpy.pars.FeasibilityMethod = <FeasibilityMethod.PLA: 0>,

region_engine: stormpy.pars.RegionCheckEngine = <RegionCheckEngine.PARAMETER_LIFTING: 0>,

) → stormpy.pars.FeasibilitySynthesisResult

check_feasibility(

environment: stormpy.environments.Environment,

model: stormpy.developer.storage._storage._SparseModel_RationalFunction,

formula: stormpy.logic.Formula,

region_bound: stormpy.numbers.RationalFunctionCoefficient,

method: stormpy.pars.FeasibilityMethod = <FeasibilityMethod.PLA: 0>,

region_engine: stormpy.pars.RegionCheckEngine = <RegionCheckEngine.PARAMETER_LIFTING: 0>,

) → stormpy.pars.FeasibilitySynthesisResult

Find a well-defined valuation satisfying a bounded probability or reward formula

Find a well-defined valuation satisfying a bounded probability or reward formula