BuilderOptions

class BuilderOptions(
formulas: collections.abc.Sequence[stormpy.logic.Formula],
model_description: stormpy.io.SymbolicModelDescription = ...,
)
class BuilderOptions(build_all_reward_models: bool = False, build_all_labels: bool = False)

Bases: BuilderOptions

Options for building a model from a symbolic description.

The options can be created preserving the given properties via e.g. BuilderOptions(properties), or they can be created for the full model via BuilderOptions(build_full=True). Single flags can be set afterwards, e.g. options.set_build_all_labels() or options.set_build_state_valuations().

Parameters:

  • properties – (optional) Property or properties (or formulas) whose labels and reward models are preserved.

  • model_description – (optional) Symbolic model description used to resolve the properties.

  • build_full – Whether the full model is built, i.e., all reward models, all labels, state valuations, choice labels and choice origins (in addition to the labels and reward models required by the properties).

Create options preserving the given formulas

Create options without formulas

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

Get the names of the labels to build

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

Whether all labels are built

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

Whether all reward models are built

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

Whether choice labels are built

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

Whether choice origins are built

is_build_observation_valuations_set(self: stormpy.developer.BuilderOptions) → bool

Whether observation valuations are built

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

Whether state valuations are built

set_add_out_of_bounds_state(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Add a state for out-of-bounds valuations

set_add_overlapping_guards_label(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Label states with overlapping guards

set_apply_maximal_progress_assumption(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Apply the maximal progress assumption

set_build_all_labels(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Build all state labels

set_build_all_reward_models(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Build all reward models

set_build_choice_labels(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Build choice labels

set_build_choice_origins(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Build choice origins

set_build_observation_valuations(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Build observation valuations

set_build_state_valuations(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Build state valuations

set_exploration_checks(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Perform extra checks during exploration

set_scale_and_lift_transition_rewards(
self: stormpy.developer.BuilderOptions,
new_value: bool = True,
) → stormpy.developer.BuilderOptions

Scale and lift transition rewards