BuilderOptions

Warning

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

class BuilderOptions(formulas: collections.abc.Sequence[stormpy.logic.Formula], model_description: stormpy.io.SymbolicModelDescription = <stormpy.io.SymbolicModelDescription object at 0x70e03b76a730>)

class BuilderOptions(build_all_reward_models: bool = False, build_all_labels: bool = False)

Bases: pybind11_object

Options for building process

Create options preserving the given formulas

Create options without formulas

get_label_names(self: stormpy.developer._core.BuilderOptions) → set[str]

Get the names of the labels to build

is_build_all_labels_set(self: stormpy.developer._core.BuilderOptions) → bool

Whether all labels are built

is_build_all_reward_models_set(self: stormpy.developer._core.BuilderOptions) → bool

Whether all reward models are built

is_build_choice_labels_set(self: stormpy.developer._core.BuilderOptions) → bool

Whether choice labels are built

is_build_choice_origins_set(self: stormpy.developer._core.BuilderOptions) → bool

Whether choice origins are built

is_build_observation_valuations_set(

self: stormpy.developer._core.BuilderOptions,

) → bool

Whether observation valuations are built

is_build_state_valuations_set(self: stormpy.developer._core.BuilderOptions) → bool

Whether state valuations are built

set_add_out_of_bounds_state(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Add a state for out-of-bounds valuations

set_add_overlapping_guards_label(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Label states with overlapping guards

set_apply_maximal_progress_assumption(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Apply the maximal progress assumption

set_build_all_labels(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Build all state labels

set_build_all_reward_models(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Build all reward models

set_build_choice_labels(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Build choice labels

set_build_choice_origins(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Build choice origins

set_build_observation_valuations(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Build observation valuations

set_build_state_valuations(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Build state valuations

set_exploration_checks(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Perform extra checks during exploration

set_scale_and_lift_transition_rewards(

self: stormpy.developer._core.BuilderOptions,

new_value: bool = True,

) → stormpy.developer._core.BuilderOptions

Scale and lift transition rewards