Environments

All verigym environments follow the gymnasium API and inherit from VeriGymEnv. Generative environments wrap simulators, e.g., a gymnasium environment (GenerativeEnv.from_gymnasium) or a PRISM program (GenerativeEnv.from_prism). Explicit environments store the full transition and reward functions (see Model Components), so they can be model checked: an AbstractedExplicitEnv is learned from a simulator (see the model learning guide), and a FrameworkExplicitEnv is loaded from an external tool, e.g., from stormpy or a .umb file (see the import and export guide). Interval environments are the interval MDP (IMDP) counterparts of the explicit environments.

Base class

class verigym.VeriGymEnv

Abstract wrapper around gymnasium.Env for a unified VeriGym interface. Parent to all types of VeriGym environments.

simulate(policy: PolicyClass, n_steps: int = 1, verbose=True, seed=None) → list[list[tuple[NDArray, NDArray, NDArray, NDArray, bool]]]

Simulate the environment for n_steps using the provided policy.

Args:

policy: A function that takes an observation and returns an action. n_steps (int): Number of steps to simulate.

Returns:

A list of trajectories containing a list of tuples (state, action, reward, next_state, terminated) for each step. terminated is True only if next_state is terminal (e.g. the pole fell in CartPole); a trajectory that was cut off by truncation (e.g. a time limit) ends with terminated=False.

classmethod make_vec(num_envs: int = 1, vectorization_mode: str | None = 'sync', vector_kwargs: dict[str, Any] | None = None, wrappers: Sequence[Callable[[Env], Wrapper]] | None = None, wrapper_kwargs: list | None = None, make_callback=None, **kwargs)

Builds vectorized VeriGymEnvs.

Parameters:

• num_envs (int) – How many envs to contain in the vectorized env.

• render_mode (str) – Environment render mode. Currently can only be None.

• vectorization_mode (str) – The vectorization mode. Can be “sync” or “async”

• vector_kwargs (dict) – Further arguments to apply to vectorization.

• wrappers (Sequence) – List of wrappers to be applied to the environments.

• **kwargs – Allows to include environment-specific parameters.

Returns:

env – The vectorized FrameworkExplicitEnvs.

Return type:

gym.SyncVectorEnv(VeriGymEnv) if vectorization_mode==”sync” or gym.AsyncVectorEnv(VeriGymEnv) if vectorization_mode==”async”

Generative environments

class verigym.GenerativeEnv

classmethod from_gymnasium(env: Env)

Creates a GenerativeEnv from a gymnasium.Env instance. All attributes (in the gymnasium.Env’s __dict__ and __slots__) are shallow-copied over to the new instance.

Notes: - The original env is not used after copying, this might cause issues with C-level definitions in some environments. - This method uses dynamic class creation to merge the original gymnasium environment’s class with GenerativeEnv and returns a class called GenerativeEnv_from_gym that should behave like any other GenerativeEnv instantiation. - Be cautious when using gymnasium envs with applied wrappers as their compatibility has not been tested, including vectorized envs. - GenerativeEnv.__init__ is currently not called for the merged instance.

Parameters:

env (gym.Env) – The gymnasium environment to wrap.

Returns:

A merged instance whose behavior follows the gym env class first, while remaining an instance of GenerativeEnv.

Return type:

GenerativeEnv

classmethod vec_from_gymnasium(env, num_envs: int = 1, vectorization_mode: str | None = 'sync', vector_kwargs: dict[str, Any] | None = None, wrappers: Sequence[Callable[[Env], Wrapper]] | None = None, wrapper_kwargs: list | None = None)

Builds vectorized GenerativeEnv from a gym environment.

Parameters:

• env (gym.Env) – The base environment.

• num_envs (int) – How many envs to contain in the vectorized env.

• render_mode (str) – Environment render mode.

• vectorization_mode (str) – The vectorization mode. Can be “sync” or “async”

• vector_kwargs (dict) – Further arguments to apply to vectorization.

• wrappers (Sequence) – List of wrappers to be applied to the environments.

• wrapper_kwargs (list) – Further arguments, per wrapper, to apply to wrappers.

Returns:

env – The vectorized GenerativeEnv.

Return type:

gym.SyncVectorEnv(GenerativeEnv) if vectorization_mode==”sync” or gym.AsyncVectorEnv(GenerativeEnv) if vectorization_mode==”async”

classmethod vec_from_prism(prism_filepath: str, num_envs: int = 1, vectorization_mode: str | None = 'sync', vector_kwargs: dict[str, Any] | None = None, wrappers: Sequence[Callable[[Env], Wrapper]] | None = None, wrapper_kwargs: list | None = None)

Builds a vectorized GenerativeEnv from a prism program file.

Parameters:

• prism_filepath (str) – The path to the prism program.

• num_envs (int) – How many envs to contain in the vectorized env.

• render_mode (str) – Environment render mode. Note: We currently do not support visualization of envs from PRISM.

• vectorization_mode (str) – The vectorization mode. Can be “sync” or “async”

• vector_kwargs (dict) – Further arguments to apply to vectorization.

• wrappers (Sequence) – List of wrappers to be applied to the environments.

• wrapper_kwargs (list) – Further arguments, per wrapper, to apply to wrappers.

Returns:

env – The vectorized GenerativeEnv.

Return type:

gym.SyncVectorEnv(GenerativeEnv) if vectorization_mode==”sync” or gym.AsyncVectorEnv(GenerativeEnv) if vectorization_mode==”async”

class verigym.environments.generativeenv.SymbolicGenerativeEnv(simulator: Simulator, n_actions: int)

Bases: GenerativeEnv

This is an extension to GenerativeEnv meant for simulation environments from symbolic model descriptions (e.g., in PRISM language). It overwrites the step and reset methods to use the stormpy.simulator.

Note that we do not build the underlying MDP here, and hence do not have access to an explicit model representation.

step(action)

Take a step in the environment, using the simulator.

reset(seed: int | None = None, options: dict | None = None)

Reset the simulator. A seed reseeds the simulator.

Explicit environments

class verigym.environments.base_explicitenv.BaseExplicitEnv(nr_states: int, nr_actions: int, initial_state_distr: StateDistribution | NDArray, transition_function: TransitionFunction, reward_function: RewardFunction, nr_rewards: int = 1, observation_space: Space | None = None, render_mode: str | None = None, dummy_terminal_state: int | None = None)

Bases: VeriGymEnv, ABC

Stores the explicit model and sets up the spaces. Shared by all explicit envs, which pass their model in this form (e.g., FrameworkExplicitEnv converts its model with its formatter).

Parameters:

• nr_states (int) – Number of states.

• nr_actions (int) – Number of actions.

• initial_state_distr (StateDistribution | NDArray) – The initial state distribution. An array (with the probability of each state) is converted to a StateDistribution.

• transition_function (TransitionFunction) – The transition function.

• reward_function (RewardFunction) – The reward function.

• nr_rewards (int, default=1) – Number of reward functions/models.

• observation_space (gym.spaces.Space | None, default=None) – The observation space, Discrete(nr_states) by default.

• render_mode (str | None, default=None) – Environment render mode. Currently can only be None.

• dummy_terminal_state (int | None, default=None) – The terminal sink state, e.g., of a learned abstraction.

get_transition_function() → TransitionFunction

Provides access to the transition function. The format is defined by self.formatter.

get_reward_function() → RewardFunction

Provides access to the reward function. The format is defined by self.formatter.

set_state(state) → None

Set the environment to a given state.

get_abstraction_map()

Returns the environment’s abstraction map or None if it does not have any.

encode(state)

Returns the index of a state of the observation space. The identity, unless the env has other states (e.g., factored states).

decode(state_idx)

Returns the state of the observation space with index state_idx. The identity, unless the env has other states (e.g., factored states).

sample_initial_state()

Samples a state from the initial state distribution.

step(action)

Take a step in the environment from the current state.

Parameters:

action (int) – Chosen action from self.action_space. Unavailable actions do not change the state and give no reward.

Returns:

• observation – The new state (a factored state if the env has factored states).

• reward (float) – The sum of the rewards, since gymnasium requires a single reward. info["reward"] has the list of rewards.

• terminated (bool) – Whether the new state is terminal (see _init_terminal_states).

• truncated (bool) – Always False.

• info (dict) – The info of the new state (see _get_info) and of the transition (see _gather_transition_info).

reset(seed: int | None = None, options: dict | None = None)

Reset to an initial state. A seed reseeds the generator that samples transitions and initial states.

class verigym.AbstractedExplicitEnv(nr_states: int, nr_actions: int, initial_state_distr: StateDistribution | NDArray, transition_function: TransitionFunction, reward_function: RewardFunction, nr_rewards: int = 1, abstraction_map=None, original_env: VeriGymEnv = None, render_mode: str | None = None, dummy_terminal_state: int = None)

Bases: BaseExplicitEnv

Stores the explicit model and sets up the spaces. Shared by all explicit envs, which pass their model in this form (e.g., FrameworkExplicitEnv converts its model with its formatter).

Parameters:

• nr_states (int) – Number of states.

• nr_actions (int) – Number of actions.

• initial_state_distr (StateDistribution | NDArray) – The initial state distribution. An array (with the probability of each state) is converted to a StateDistribution.

• transition_function (TransitionFunction) – The transition function.

• reward_function (RewardFunction) – The reward function.

• nr_rewards (int, default=1) – Number of reward functions/models.

• observation_space (gym.spaces.Space | None, default=None) – The observation space, Discrete(nr_states) by default.

• render_mode (str | None, default=None) – Environment render mode. Currently can only be None.

• dummy_terminal_state (int | None, default=None) – The terminal sink state, e.g., of a learned abstraction.

get_abstraction_map()

Returns the environment’s abstraction map or None if it does not have any.

class verigym.FrameworkExplicitEnv(model: Any, formatter: ExplicitFormatter, flat: bool = True, render_mode: str | None = None)

Bases: BaseExplicitEnv

An explicit env of a model of a framework (e.g., a stormpy MDP), converted with the framework’s formatter.

Parameters:

• model (Any) – The model, e.g., a stormpy.storage.SparseMdp.

• formatter (ExplicitFormatter) – The formatter of the model, e.g., a StormpyFormatter. Also provides the action names, labels and valuations of the env.

• flat (bool, default=True) – Whether the env uses flat (integer) states, or factored states from the state valuations.

• render_mode (str | None, default=None) – Environment render mode. Currently can only be None.

decode(state_idx)

Returns the state of the observation space with index state_idx. The identity, unless the env has other states (e.g., factored states).

encode(state_values)

Returns the index of a state of the observation space. The identity, unless the env has other states (e.g., factored states).

classmethod from_stormpy(mdp, flat: bool = True, render_mode: str | None = None)

Builds an env from a stormpy MDP, or an IntervalFrameworkExplicitEnv from a stormpy interval MDP (stormpy.storage.SparseIntervalMdp).

classmethod vec_from_stormpy(mdp, render_mode: str | None = None, num_envs: int = 1, vectorization_mode: str = 'sync', vector_kwargs: dict[str, Any] | None = None, wrappers: Sequence[Callable[[Env], Wrapper]] | None = None, wrapper_kwargs: list | None = None)

Builds vectorized envs of this class from a stormpy MDP (see from_stormpy). Note that only the “sync” vectorization mode works here, since we cannot pickle and serialize stormpy MDPs, which are C++ objects. We could enable “async” by not storing the stormpy MDP.

Parameters:

• mdp (stormpy.storage.SparseMdp) – The underlying MDP.

• num_envs (int) – How many envs to contain in the vectorized env.

• render_mode (str) – Environment render mode. Currently can only be None.

• vectorization_mode (str, default="sync") – The vectorization mode. Here, we can only use “sync”

• vector_kwargs (dict) – Further arguments to apply to vectorization.

• wrappers (Sequence) – List of wrappers to be applied to the environments.

Returns:

env – The vectorized envs, built with cls.from_stormpy.

Return type:

gym.SyncVectorEnv

Interval environments

class verigym.environments.interval_explicitenv.IntervalEnvMixin

Intervals over the transition probabilities and rewards, i.e., an interval MDP (IMDP). Shared by IntervalExplicitEnv (e.g., learned abstractions) and IntervalFrameworkExplicitEnv (e.g., interval MDPs loaded with stormpy).

The env only stores the intervals. Wherever a point estimate is required (e.g., to sample transitions in step, for the action mask and terminal states, or to export the env as a point MDP), it uses the point estimates of the intervals: IntervalTransitionFunction.point_estimate and IntervalRewardFunction.point_estimate. These are the transition_function and reward_function of the env.

get_interval_transition_function() → IntervalTransitionFunction

Provides access to the interval transition function.

get_interval_reward_function() → IntervalRewardFunction

Provides access to the interval reward function.

class verigym.environments.interval_explicitenv.IntervalAbstractedExplicitEnv(nr_states: int, nr_actions: int, initial_state_distr: StateDistribution | NDArray, interval_transition_function: IntervalTransitionFunction, interval_reward_function: IntervalRewardFunction, nr_rewards: int = 1, abstraction_map=None, original_env: VeriGymEnv = None, render_mode: str | None = None, dummy_terminal_state: int = None)

Bases: IntervalEnvMixin, AbstractedExplicitEnv

An AbstractedExplicitEnv with intervals over the transition probabilities and rewards, i.e., an interval MDP (IMDP), e.g., a learned abstraction. See IntervalEnvMixin for how the intervals and their point estimates are used.

class verigym.environments.frameworkexplicitenv.IntervalFrameworkExplicitEnv(model: Any, formatter: ExplicitFormatter, flat: bool = True, render_mode: str | None = None)

Bases: IntervalEnvMixin, FrameworkExplicitEnv

A FrameworkExplicitEnv of an interval MDP (IMDP), e.g., loaded with stormpy: its formatter converts the transition probabilities and rewards to intervals. Apart from that, it is the same as for MDPs (action names, labels, valuations, factored states).

Depends on IntervalEnvMixin for shared functionality between this class and IntervalExplicitEnv. See IntervalEnvMixin for how the intervals and their point estimates are used; step reports the intervals of the transition in its info, as IntervalExplicitEnv does.

An explicit env of a model of a framework (e.g., a stormpy MDP), converted with the framework’s formatter.

Parameters:

• model (Any) – The model, e.g., a stormpy.storage.SparseMdp.

• formatter (ExplicitFormatter) – The formatter of the model, e.g., a StormpyFormatter. Also provides the action names, labels and valuations of the env.

• flat (bool, default=True) – Whether the env uses flat (integer) states, or factored states from the state valuations.

• render_mode (str | None, default=None) – Environment render mode. Currently can only be None.