SymbolicQualitativeCheckResult

class SymbolicQualitativeCheckResult[DdType](

reachable_states: stormpy.developer.storage.Bdd[stormpy.models.DdType.Sylvan],

truth_values: stormpy.developer.storage.Bdd[stormpy.models.DdType.Sylvan],

)

Symbolic qualitative model checking result

Template arguments:

• DdType (value)

Available specializations:

• SymbolicQualitativeCheckResult[stormpy.models.DdType.Sylvan]

Construction

Create result

The default specialization is SymbolicQualitativeCheckResult[stormpy.models.DdType.Sylvan].

Members

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

Complement the result

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

Number of states satisfying the property

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

Whether at least one state satisfies the property

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

Restrict the result to the states of the given filter

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

Whether all states satisfy the property

SymbolicQualitativeCheckResult.get_truth_values_vector(

self: stormpy.results.SymbolicQualitativeCheckResult[DdType],

) → stormpy.developer.storage.Bdd[stormpy.models.DdType.Sylvan]

Get BDD representing the truth values

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

Whether a scheduler is present

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

Whether the result is explicit

SymbolicQualitativeCheckResult.is_explicit_pareto_curve_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is an explicit Pareto curve

SymbolicQualitativeCheckResult.is_explicit_qualitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is explicit qualitative

SymbolicQualitativeCheckResult.is_explicit_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is explicit quantitative

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

Whether the result is hybrid

SymbolicQualitativeCheckResult.is_hybrid_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is hybrid quantitative

SymbolicQualitativeCheckResult.is_pareto_curve_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is a Pareto curve

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

Whether the result is qualitative

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

Whether the result is quantitative

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

Whether the result contains values for all states

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

Whether the result is symbolic

SymbolicQualitativeCheckResult.is_symbolic_qualitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is symbolic qualitative

SymbolicQualitativeCheckResult.is_symbolic_quantitative_check_result(

self: stormpy.results.CheckResult,

) → bool

Whether the result is symbolic quantitative