ExplicitQualitativeCheckResult

class ExplicitQualitativeCheckResult[ValueType](truth_values: stormpy.datastructures.BitVector)

Explicit qualitative model checking result

Template arguments:

• ValueType (type)

Available specializations:

• ExplicitQualitativeCheckResult[float]

• ExplicitQualitativeCheckResult[stormpy.numbers.Rational]

• ExplicitQualitativeCheckResult[stormpy.numbers.RationalFunction]

Construction

Create result from truth values

The default specialization is ExplicitQualitativeCheckResult[float].

Members

ExplicitQualitativeCheckResult.complement(self: stormpy.results.QualitativeCheckResult) → None

Complement the result

ExplicitQualitativeCheckResult.count(self: stormpy.results.QualitativeCheckResult) → int

Number of states satisfying the property

ExplicitQualitativeCheckResult.exists_true(self: stormpy.results.QualitativeCheckResult) → bool

Whether at least one state satisfies the property

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

Restrict the result to the states of the given filter

ExplicitQualitativeCheckResult.forall_true(self: stormpy.results.QualitativeCheckResult) → bool

Whether all states satisfy the property

ExplicitQualitativeCheckResult.get_scheduler(

self: stormpy.results.ExplicitQualitativeCheckResult[ValueType],

) → stormpy.models.Scheduler[ValueType]

Get scheduler

ExplicitQualitativeCheckResult.get_states(

self: stormpy.results.ExplicitQualitativeCheckResult[ValueType],

) → stormpy.datastructures.BitVector

Get BitVector of the states for which the result has values

ExplicitQualitativeCheckResult.get_truth_values_vector(

self: stormpy.results.ExplicitQualitativeCheckResult[ValueType],

) → stormpy.datastructures.BitVector

Get BitVector representing the truth values

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

Whether a scheduler is present

ExplicitQualitativeCheckResult.has_value_for_state(

self: stormpy.results.ExplicitQualitativeCheckResult[ValueType],

state: SupportsInt | SupportsIndex,

) → bool

Check whether the result has a value for the given state

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

Whether the result is explicit

ExplicitQualitativeCheckResult.is_explicit_pareto_curve_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is an explicit Pareto curve

ExplicitQualitativeCheckResult.is_explicit_qualitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is explicit qualitative

ExplicitQualitativeCheckResult.is_explicit_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is explicit quantitative

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

Whether the result is hybrid

ExplicitQualitativeCheckResult.is_hybrid_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is hybrid quantitative

ExplicitQualitativeCheckResult.is_pareto_curve_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is a Pareto curve

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

Whether the result is qualitative

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

Whether the result is quantitative

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

Whether the result contains values for all states

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

Whether the result is symbolic

ExplicitQualitativeCheckResult.is_symbolic_qualitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is symbolic qualitative

ExplicitQualitativeCheckResult.is_symbolic_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is symbolic quantitative