ExplicitModelCheckerHint

class ExplicitModelCheckerHint[ValueType]

Information that may accelerate an explicit state model checker

Template arguments:

• ValueType (type)

Available specializations:

• ExplicitModelCheckerHint[float]

Construction

Create empty hint

The default specialization is ExplicitModelCheckerHint[float].

Members

ExplicitModelCheckerHint.set_compute_only_maybe_states(

self: stormpy.ExplicitModelCheckerHint[ValueType],

value: bool,

) → None

Set whether only the maybe states are computed

ExplicitModelCheckerHint.set_maybe_states(

self: stormpy.ExplicitModelCheckerHint[ValueType],

maybe_states: stormpy.datastructures.BitVector,

) → None

Set the maybe states. This is assumed to be correct.

ExplicitModelCheckerHint.set_no_end_components_in_maybe_states(

self: stormpy.ExplicitModelCheckerHint[ValueType],

value: bool,

) → None

Set whether the maybe states contain no end components

ExplicitModelCheckerHint.set_result_hint(

self: stormpy.ExplicitModelCheckerHint[ValueType],

result_hint: collections.abc.Sequence[SupportsFloat | SupportsIndex] | None,

) → None

Set a result hint close to the actual result

ExplicitModelCheckerHint.set_scheduler_hint(

self: stormpy.ExplicitModelCheckerHint[ValueType],

scheduler_hint: stormpy.models.Scheduler[float] | None,

) → None

Set a scheduler that is close to the optimal scheduler