SparseInstantiationModelChecker

Warning

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

class SparseInstantiationModelChecker[ModelType, ResultType]

Instantiate and check a parametric model

Template arguments:

  • ModelType (value)

  • ResultType (type)

Available specializations:

  • SparseInstantiationModelChecker[stormpy.models.ModelType.DTMC, float]

  • SparseInstantiationModelChecker[stormpy.models.ModelType.MDP, float]

  • SparseInstantiationModelChecker[stormpy.models.ModelType.CTMC, float]

  • SparseInstantiationModelChecker[stormpy.models.ModelType.DTMC, stormpy.numbers.Rational]

  • SparseInstantiationModelChecker[stormpy.models.ModelType.MDP, stormpy.numbers.Rational]

  • SparseInstantiationModelChecker[stormpy.models.ModelType.CTMC, stormpy.numbers.Rational]

Construction

Constructor signatures vary by specialization:

  • SparseInstantiationModelChecker[stormpy.models.ModelType.DTMC, float](environment: stormpy.environments.Environment, model: stormpy.models.SparseDtmc[stormpy.numbers.RationalFunction])

  • SparseInstantiationModelChecker[stormpy.models.ModelType.DTMC, stormpy.numbers.Rational](environment: stormpy.environments.Environment, model: stormpy.models.SparseDtmc[stormpy.numbers.RationalFunction])

  • SparseInstantiationModelChecker[stormpy.models.ModelType.MDP, float](environment: stormpy.environments.Environment, model: stormpy.models.SparseMdp[stormpy.numbers.RationalFunction])

  • SparseInstantiationModelChecker[stormpy.models.ModelType.MDP, stormpy.numbers.Rational](environment: stormpy.environments.Environment, model: stormpy.models.SparseMdp[stormpy.numbers.RationalFunction])

  • SparseInstantiationModelChecker[stormpy.models.ModelType.CTMC, float](environment: stormpy.environments.Environment, model: stormpy.models.SparseCtmc[stormpy.numbers.RationalFunction])

  • SparseInstantiationModelChecker[stormpy.models.ModelType.CTMC, stormpy.numbers.Rational](environment: stormpy.environments.Environment, model: stormpy.models.SparseCtmc[stormpy.numbers.RationalFunction])

Members

SparseInstantiationModelChecker.check(
self: stormpy.pars.developer.SparseInstantiationModelChecker[ModelType, ResultType],
environment: stormpy.environments.Environment,
valuation: collections.abc.Mapping[stormpy.numbers.Variable, stormpy.numbers.RationalFunctionCoefficient],
) → stormpy.results.CheckResult

Check the model instantiated with the given valuation

SparseInstantiationModelChecker.set_instantiations_are_graph_preserving(
self: stormpy.pars.developer.SparseInstantiationModelChecker[ModelType, ResultType],
value: bool,
) → None

Set whether all instantiations preserve the graph structure

SparseInstantiationModelChecker.specify_formula(
self,
check_task: stormpy.developer.CheckTask[stormpy.numbers.RationalFunction],
) → None

Specify the formula to check