DiscreteTimePrismProgramSimulator

Warning

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

class DiscreteTimePrismProgramSimulator[ValueType](
program: stormpy.io.PrismProgram,
options: stormpy.developer.BuilderOptions,
)

Simulator for Prism programs

Template arguments:

  • ValueType (type)

Available specializations:

  • DiscreteTimePrismProgramSimulator[float]

Construction

Create simulator

The default specialization is DiscreteTimePrismProgramSimulator[float].

Members

DiscreteTimePrismProgramSimulator.get_choices(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → list[stormpy.developer.Choice[float]]

Get the choices of the current state

DiscreteTimePrismProgramSimulator.get_current_state(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → stormpy.datastructures.BitVector

Get the current state

DiscreteTimePrismProgramSimulator.get_current_state_as_valuation(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → stormpy.models.SimpleValuation

Get the current state as valuation

DiscreteTimePrismProgramSimulator.get_current_state_labelling(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → list[str]

Get the labels of the current state

DiscreteTimePrismProgramSimulator.get_current_state_string(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → str

Get string representation of the current state

DiscreteTimePrismProgramSimulator.get_last_rewards(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → list[float]

Get the rewards obtained in the last step

DiscreteTimePrismProgramSimulator.get_observation_as_json(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → stormpy.datastructures.JsonContainer[float]

Get the current observation as JSON

DiscreteTimePrismProgramSimulator.get_reward_names(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → list[str]

Get the names of the rewards

DiscreteTimePrismProgramSimulator.get_state_as_json(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → stormpy.datastructures.JsonContainer[float]

Get the current state as JSON

DiscreteTimePrismProgramSimulator.is_sink_state(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → bool

Whether the current state is a sink state

DiscreteTimePrismProgramSimulator.reset_to_initial(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
) → bool

Reset to the initial state

DiscreteTimePrismProgramSimulator.reset_to_state(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
compressed_state: stormpy.datastructures.BitVector,
) → bool
DiscreteTimePrismProgramSimulator.reset_to_state(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
valuation_state: stormpy.models.SimpleValuation,
) → bool

Reset to the given state

Reset to the given state

DiscreteTimePrismProgramSimulator.set_seed(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
seed: SupportsInt | SupportsIndex,
) → None

Set the seed of the random generator

DiscreteTimePrismProgramSimulator.step(
self: stormpy.developer.DiscreteTimePrismProgramSimulator[ValueType],
action_number: SupportsInt | SupportsIndex,
) → bool

Make a step and randomly select the successor. The index of the choice is given as argument (see get_choices).