Import and Export

Functions for writing explicit environments to the model formats of external tools, and for loading models from such formats. .umb and .drn files can be read by model checkers such as Storm and PRISM, while the stormpy exports return stormpy models in memory. gymnasium environments and PRISM programs are loaded with GenerativeEnv (see Environments), and policies computed by other tools with the classes in Policies. For a walkthrough, see the import and export guide.

Export

verigym.io.exporter.export_to_umb(env: BaseExplicitEnv, out_file: str | None = None, intervals: bool | None = None, overapproximate=True) → None[source]

Exports an explicit env to the Unified Markov Binary (UMB) format and writes directly to a .umb file.

Parameters:

  • env (BaseExplicitEnv) – The explicit environment.

  • out_file (str) – Path to the output file. By default, writes to cwd/mdp.umb.

  • intervals (bool | None, default=None) – Whether to export an interval MDP (IMDP) instead of an MDP. By default, exports an IMDP if and only if env is an interval env (IntervalEnvMixin, e.g., IntervalExplicitEnv). The IMDP of an interval env has its transition and reward intervals, the IMDP of any other env has point intervals [p, p].

  • overapproximate (bool, default=True) – Whether to over- or underapproximate state labels if the ExplicitEnv is abstracted.

Notes

  • The model is built with export_to_stormpy_mdp or export_to_stormpy_imdp, see the notes of build_stormpy_mdp on choices, choice labels and deadlocks.

  • UMB only stores the actions that are available in some state, and the set of initial states. Loading the file (e.g., with load_from_umb) assumes a uniform distribution over the initial states, so a warning is raised if the initial distribution of env is not uniform.

verigym.io.exporter.export_to_drn(env: BaseExplicitEnv, out_file: str | None = None) → None[source]

Exports an explicit env to an explicit model and writes directly to a .drn file.

Parameters:

  • env (BaseExplicitEnv) – The explicit environment.

  • out_file (str) – Path to the output file. By default, writes to cwd/mdp.drn.

verigym.io.exporter.export_to_stormpy_mdp(env: BaseExplicitEnv, overapproximate=True) → SparseMdp[source]

Exports an ExplicitEnv to a stormpy.storage.SparseMdp. See the notes of build_stormpy_mdp on choices, choice labels and deadlocks.

Parameters:

  • env (ExplicitEnv) – The explicit environment.

  • overapproximate (bool, default=True) – Whether to over- or underapproximate state labels if the ExplicitEnv is abstracted.

Returns:

stormpy_mdp – The mdp.

Return type:

stormpy.storage.SparseMdp

verigym.io.exporter.export_to_stormpy_imdp(env: BaseExplicitEnv, overapproximate=True, use_reward_uncertainty=False) → SparseIntervalMdp[source]

Exports an ExplicitEnv to a stormpy.storage.SparseIntervalMdp. Apart from the intervals, it is the same as export_to_stormpy_mdp; see the notes of build_stormpy_mdp on choices, choice labels and deadlocks.

Parameters:

  • env (ExplicitEnv) – The explicit environment.

  • overapproximate (bool, default=True) – Whether to over- or underapproximate state labels if the ExplicitEnv is abstracted

  • use_reward_uncertainty (bool, default = False) – If True and env is an interval env (IntervalEnvMixin), it builds the IMDP using the interval_reward_function If False, builds an IMDP with a standard reward function using reward_function.

Returns:

stormpy_mdp – The mdp.

Return type:

stormpy.storage.SparseIntervalMdp

Import

verigym.io.importer.load_from_umb(in_file: str, flat: bool = True) → FrameworkExplicitEnv[source]

Loads an explicit env from a Unified Markov Binary (UMB) file, using stormpy.

Parameters:

  • in_file (str) – Path to the .umb file.

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

Returns:

env – A FrameworkExplicitEnv with the choice labels of the file as action labels; for interval MDPs, an IntervalFrameworkExplicitEnv with the transition and reward intervals of the file.

Return type:

FrameworkExplicitEnv | IntervalFrameworkExplicitEnv

Notes

UMB only stores the set of initial states, so the env starts uniformly in one of them.

verigym.io.importer.load_from_drn(in_file: str, flat: bool = True) → FrameworkExplicitEnv[source]

Loads an explicit env from a DRN file, using stormpy.

Parameters:

  • in_file (str) – Path to the .drn file.

  • flat (bool, default=True) – Whether the env uses flat (integer) states, or factored states from the state valuations. DRN files do not store state valuations, so only flat states are available.

Returns:

env – The env, with the choice labels of the file as action labels.

Return type:

FrameworkExplicitEnv

Notes

DRN only stores the set of initial states, so the env starts uniformly in one of them. Interval MDPs are not supported, since stormpy cannot read the interval values of DRN files; use UMB instead.