ExplicitQuantitativeCheckResult

class ExplicitQuantitativeCheckResult[ValueType]

Explicit quantitative model checking result

Template arguments:

  • ValueType (type)

Available specializations:

  • ExplicitQuantitativeCheckResult[float]

  • ExplicitQuantitativeCheckResult[stormpy.numbers.Rational]

  • ExplicitQuantitativeCheckResult[stormpy.numbers.RationalFunction]

Construction

Create result from values

The default specialization is ExplicitQuantitativeCheckResult[float].

Constructor signatures vary by specialization:

  • ExplicitQuantitativeCheckResult[float](values: collections.abc.Sequence[typing.SupportsFloat | typing.SupportsIndex])

  • ExplicitQuantitativeCheckResult[stormpy.numbers.Rational](values: collections.abc.Sequence[stormpy.numbers.Rational])

  • ExplicitQuantitativeCheckResult[stormpy.numbers.RationalFunction](values: collections.abc.Sequence[stormpy.numbers.RationalFunction])

Members

ExplicitQuantitativeCheckResult.aggregate(
self: stormpy.results.QuantitativeCheckResult[ValueType],
filter: stormpy.results.FilterType,
) → stormpy.results.AggregatedValue[ValueType]

Aggregate the values together with the known bounds. Supported filters: MIN, MAX, SUM and AVG.

ExplicitQuantitativeCheckResult.average(
self: stormpy.results.QuantitativeCheckResult[ValueType],
) → ValueType

Get average of the values

ExplicitQuantitativeCheckResult.clear_bounds(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → None

Remove all bounds

ExplicitQuantitativeCheckResult.filter(self: stormpy.results.CheckResult, filter) → None

Restrict the result to the states of the given filter

ExplicitQuantitativeCheckResult.get_finite_value_vector(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → list[ValueType]

Get values for all states as plain values (fails for infinite values which the value type cannot represent)

ExplicitQuantitativeCheckResult.get_lower_bound(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
state: SupportsInt | SupportsIndex,
) → ValueType | None

Get sound lower bound for given state (None if not known)

ExplicitQuantitativeCheckResult.get_lower_bound_vector(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → list[ValueType]

Get sound lower bounds, indexed like get_value_vector()

ExplicitQuantitativeCheckResult.get_max(
self: stormpy.results.QuantitativeCheckResult[ValueType],
) → ValueType

Get maximal value

ExplicitQuantitativeCheckResult.get_min(
self: stormpy.results.QuantitativeCheckResult[ValueType],
) → ValueType

Get minimal value

ExplicitQuantitativeCheckResult.get_scheduler(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → stormpy.models.Scheduler[ValueType]

Get scheduler

ExplicitQuantitativeCheckResult.get_solution_bounds(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → stormpy.results.SolutionBounds[ValueType]

Get sound lower and upper bounds, indexed like get_value_vector()

ExplicitQuantitativeCheckResult.get_states(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → stormpy.datastructures.BitVector

Get BitVector of the states for which the result has values

ExplicitQuantitativeCheckResult.get_upper_bound(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
state: SupportsInt | SupportsIndex,
) → ValueType | None

Get sound upper bound for given state (None if not known)

ExplicitQuantitativeCheckResult.get_upper_bound_vector(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → list[ValueType]

Get sound upper bounds, indexed like get_value_vector()

ExplicitQuantitativeCheckResult.get_value(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
state: SupportsInt | SupportsIndex,
) → ValueType

Get value for given state (without bounds)

ExplicitQuantitativeCheckResult.get_value_vector(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → list[ValueType]

Get values (possibly infinite) of the states for which the result has values

ExplicitQuantitativeCheckResult.has_lower_bounds(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → bool

Whether sound lower bounds on the values are known

ExplicitQuantitativeCheckResult.has_scheduler(self: stormpy.results.CheckResult) → bool

Whether a scheduler is present

ExplicitQuantitativeCheckResult.has_upper_bounds(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → bool

Whether sound upper bounds on the values are known

ExplicitQuantitativeCheckResult.has_value_for_state(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
state: SupportsInt | SupportsIndex,
) → bool

Check whether the result has a value for the given state

ExplicitQuantitativeCheckResult.is_explicit(self: stormpy.results.CheckResult) → bool

Whether the result is explicit

ExplicitQuantitativeCheckResult.is_explicit_pareto_curve_check_result(
self: stormpy.results.CheckResult,
) → bool

Whether the result is an explicit Pareto curve

ExplicitQuantitativeCheckResult.is_explicit_qualitative_check_result(
self: stormpy.results.CheckResult,
) → bool

Whether the result is explicit qualitative

ExplicitQuantitativeCheckResult.is_explicit_quantitative_check_result(
self: stormpy.results.CheckResult,
) → bool

Whether the result is explicit quantitative

ExplicitQuantitativeCheckResult.is_hybrid(self: stormpy.results.CheckResult) → bool

Whether the result is hybrid

ExplicitQuantitativeCheckResult.is_hybrid_quantitative_check_result(
self: stormpy.results.CheckResult,
) → bool

Whether the result is hybrid quantitative

ExplicitQuantitativeCheckResult.is_pareto_curve_check_result(
self: stormpy.results.CheckResult,
) → bool

Whether the result is a Pareto curve

ExplicitQuantitativeCheckResult.is_qualitative(self: stormpy.results.CheckResult) → bool

Whether the result is qualitative

ExplicitQuantitativeCheckResult.is_quantitative(self: stormpy.results.CheckResult) → bool

Whether the result is quantitative

ExplicitQuantitativeCheckResult.is_result_for_all_states(self: stormpy.results.CheckResult) → bool

Whether the result contains values for all states

ExplicitQuantitativeCheckResult.is_symbolic(self: stormpy.results.CheckResult) → bool

Whether the result is symbolic

ExplicitQuantitativeCheckResult.is_symbolic_qualitative_check_result(
self: stormpy.results.CheckResult,
) → bool

Whether the result is symbolic qualitative

ExplicitQuantitativeCheckResult.is_symbolic_quantitative_check_result(
self: stormpy.results.CheckResult,
) → bool

Whether the result is symbolic quantitative

ExplicitQuantitativeCheckResult.set_lower_bounds()

For ExplicitQuantitativeCheckResult[float]:

set_lower_bounds(self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType], lower_bounds: collections.abc.Sequence[typing.SupportsFloat | typing.SupportsIndex]) -> None

Set sound lower bounds, indexed like get_value_vector()

For ExplicitQuantitativeCheckResult[stormpy.numbers.Rational], ExplicitQuantitativeCheckResult[stormpy.numbers.RationalFunction]:

set_lower_bounds(self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType], lower_bounds: collections.abc.Sequence[ValueType]) -> None

Set sound lower bounds, indexed like get_value_vector()

ExplicitQuantitativeCheckResult.set_upper_bounds()

For ExplicitQuantitativeCheckResult[float]:

set_upper_bounds(self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType], upper_bounds: collections.abc.Sequence[typing.SupportsFloat | typing.SupportsIndex]) -> None

Set sound upper bounds, indexed like get_value_vector()

For ExplicitQuantitativeCheckResult[stormpy.numbers.Rational], ExplicitQuantitativeCheckResult[stormpy.numbers.RationalFunction]:

set_upper_bounds(self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType], upper_bounds: collections.abc.Sequence[ValueType]) -> None

Set sound upper bounds, indexed like get_value_vector()

ExplicitQuantitativeCheckResult.set_values_exact(
self: stormpy.results.ExplicitQuantitativeCheckResult[ValueType],
) → None

State that the values are exact, i.e., use them as lower and upper bounds

ExplicitQuantitativeCheckResult.sum(
self: stormpy.results.QuantitativeCheckResult[ValueType],
) → ValueType

Get sum of the values