SymbolicQuantitativeCheckResult

class SymbolicQuantitativeCheckResult[DdType, ValueType]

Symbolic quantitative model checking result

Template arguments:

• DdType (value)

• ValueType (type)

Available specializations:

• SymbolicQuantitativeCheckResult[stormpy.models.DdType.Sylvan, float]

• SymbolicQuantitativeCheckResult[stormpy.models.DdType.Sylvan, stormpy.numbers.Rational]

• SymbolicQuantitativeCheckResult[stormpy.models.DdType.Sylvan, stormpy.numbers.RationalFunction]

Members

SymbolicQuantitativeCheckResult.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.

SymbolicQuantitativeCheckResult.average(

self: stormpy.results.QuantitativeCheckResult[ValueType],

) → ValueType

Get average of the values

SymbolicQuantitativeCheckResult.clone(

self: stormpy.results.SymbolicQuantitativeCheckResult[DdType, ValueType],

) → stormpy.results.SymbolicQuantitativeCheckResult[DdType, ValueType]

Clone the result

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

Restrict the result to the states of the given filter

SymbolicQuantitativeCheckResult.get_max(

self: stormpy.results.QuantitativeCheckResult[ValueType],

) → ValueType

Get maximal value

SymbolicQuantitativeCheckResult.get_min(

self: stormpy.results.QuantitativeCheckResult[ValueType],

) → ValueType

Get minimal value

SymbolicQuantitativeCheckResult.get_value_vector()

For SymbolicQuantitativeCheckResult[stormpy.models.DdType.Sylvan, float]:

get_value_vector(self: stormpy.results.SymbolicQuantitativeCheckResult[DdType, ValueType]) -> stormpy.developer.storage.Add[DdType, ValueType]

Get ADD representing the values

For SymbolicQuantitativeCheckResult[stormpy.models.DdType.Sylvan, stormpy.numbers.Rational], SymbolicQuantitativeCheckResult[stormpy.models.DdType.Sylvan, stormpy.numbers.RationalFunction]:

get_value_vector(self: stormpy.results.SymbolicQuantitativeCheckResult[DdType, ValueType])

Get ADD representing the values

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

Whether a scheduler is present

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

Whether the result is explicit

SymbolicQuantitativeCheckResult.is_explicit_pareto_curve_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is an explicit Pareto curve

SymbolicQuantitativeCheckResult.is_explicit_qualitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is explicit qualitative

SymbolicQuantitativeCheckResult.is_explicit_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is explicit quantitative

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

Whether the result is hybrid

SymbolicQuantitativeCheckResult.is_hybrid_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is hybrid quantitative

SymbolicQuantitativeCheckResult.is_pareto_curve_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is a Pareto curve

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

Whether the result is qualitative

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

Whether the result is quantitative

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

Whether the result contains values for all states

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

Whether the result is symbolic

SymbolicQuantitativeCheckResult.is_symbolic_qualitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is symbolic qualitative

SymbolicQuantitativeCheckResult.is_symbolic_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is symbolic quantitative

SymbolicQuantitativeCheckResult.sum(

self: stormpy.results.QuantitativeCheckResult[ValueType],

) → ValueType

Get sum of the values