QualitativeCheckResult

class QualitativeCheckResult

Bases: CheckResult

Base class for qualitative model checking results

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

Complement the result

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

Number of states satisfying the property

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

Whether at least one state satisfies the property

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

Restrict the result to the states of the given filter

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

Whether all states satisfy the property

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

Whether a scheduler is present

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

Whether the result is explicit

is_explicit_pareto_curve_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is an explicit Pareto curve

is_explicit_qualitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is explicit qualitative

is_explicit_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is explicit quantitative

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

Whether the result is hybrid

is_hybrid_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is hybrid quantitative

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

Whether the result is a Pareto curve

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

Whether the result is qualitative

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

Whether the result is quantitative

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

Whether the result contains values for all states

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

Whether the result is symbolic

is_symbolic_qualitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is symbolic qualitative

is_symbolic_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is symbolic quantitative