CheckTask

Warning

The stormpy developer API is internal and can be subject to change.

class CheckTask[ValueType](

formula: stormpy.logic.Formula,

only_initial_states_relevant: bool = False,

uncertainty_resolution_mode: stormpy.UncertaintyResolutionMode = <UncertaintyResolutionMode.UNSET: 4>,

)

Task for model checking

Template arguments:

• ValueType (type)

Available specializations:

• CheckTask[float]

• CheckTask[stormpy.numbers.Rational]

• CheckTask[stormpy.numbers.RationalFunction]

Construction

Create check task

The default specialization is CheckTask[float].

Members

CheckTask.is_only_initial_states_relevant_set(self: stormpy.developer.CheckTask[ValueType]) → bool

Whether only initial states are relevant

CheckTask.is_produce_schedulers_set(self: stormpy.developer.CheckTask[ValueType]) → bool

Whether schedulers are produced

CheckTask.set_hint(

self: stormpy.developer.CheckTask[ValueType],

hint: stormpy.ModelCheckerHint,

) → None

Set a hint that may speed up the solver

CheckTask.set_produce_schedulers(

self: stormpy.developer.CheckTask[ValueType],

produce_schedulers: bool = True,

) → None

Set whether schedulers are produced (if possible)

CheckTask.set_uncertainty_resolution_mode(

self: stormpy.developer.CheckTask[ValueType],

uncertainty_resolution_mode: stormpy.UncertaintyResolutionMode,

) → None

Set how uncertainty is resolved