View - Edit - Print - Search

Running PRISM /

Exporting The Model

If required, once the model has been constructed, it can be exported, either for manual examination or for use in another tool. The following can all be exported:

• the transition matrix (or function);
• the rewards (state/transition) rewards;
• the labels (in the model or properties) and the states that satisfy them
• the definition of (reachable) states, i.e., their variable values
• the definition of observations, i.e., their observable values, for partially observable models

From the command-line version of PRISM, the most convenient and flexible approach is to use the -exportmodel switch. This will, by default, use the extension of the filename(s) to determine the format.

From the GUI, use the "Model | Export" menu to export the data to a file or, for small models, use the "Model | View" menu to print the details directly to the log. For the case of labels, if you want to export labels from the properties file too, use the "Properties | Export labels" option, rather than the "Model | Export" one.

The main formats for model export are:

• plain text files (sometimes referred to as "explicit" or ".tra" files)
• UMB (Unified Markov binary) format, a binary format supported by other probabilistic model checkers
• Dot format, for a graphical view of the model

Plain text (explicit files)

This format exports different parts of the model in different file, with the expected filename extensions being:

• .tra - transition matrix
• .srew, .trew, .rew - rewards: states, transitions or both
• .lab - labels
• .sta - states
• .obs - observations

To export just the transition matrix in this format, use:

To export multiple parts, use, e.g.:

If you omit the file basename of the export files and the basename of the model will be used, so this is equivalent to the above:

You can use the shorthand .all to export everything, and .rew to export both state and transition rewards. For example:

You can always use stdout instead of a filename. For example:

is a quick way to print all details (of a small model) to the terminal.

The labels (.lab) export includes the built-in labels "init" and "deadlock", providing a way to export information about initial states and (fixed) deadlock states.

When there are multiple reward structures, a separate file is created for each one and a (1-indexed) suffix is added to distinguish them. By default, a header in each file (see the "Explicit Model Files" appendix) also shows the name of the reward structure. This can be omitted - see the options below - or via the option "Include headers in model exports" in the GUI.

UMB (Unified Markov binary) format

UMB is a binary format that can incorporate all parts of the model listed above.

By default, everything is included. You can omit some parts with the -exportmodel options rewards, labels, states and obs, e.g.:

For a small model, you can also see a textual version of the UMB format using file extension .umbt (or option text):

You can also configure the compression used: zip=false turns it off, zip=gzip uses gzip and zip=xz uses xz (smaller but slower to read/write).

Other formats and options

If the file extension is not recognised, PRISM defaults to plain text (explicit) format. You can always override this using the @format@ option, e.g.:

You can perform multiple model exports using several instances of -exportmodel, e.g.:

Other file formats are also available:

• Matlab code (extension .m) or format=matlab
• Storm's DRN model format (extension .drn) or format=drn

Other -exportmodel options are:

• actions (=true/false) - whether to actions on choices/transitions
• precision (=<n>) - use <n> significant figures for floating point values (in text)
• headers (=true/false) - whether to include headers when exporting rewards
• rows - export matrices with one row/distribution on each line (plain text)
• proplabels - also export labels from a properties file into a .lab file

For plain text export, although -exportmodel is now usually the best switch to use, other older switches still exist. For example, you can export individual files using -exporttrans <file>, -exportstates <file>, -exportstaterewards <file>, -exporttransrewards <file>, -exportrewards <file> <file>, -exportlabels <file>, and -exportproplabels <file>. And you can use switches -exportmodelprecision <x>, -exportmatlab and -exportrows to specify format options affecting all of them.

Exporting (B)SCCs and end components

It is also possible to export the set of (bottom) strongly connected components (SCCs or BSCCs) for a model. This can only be done from the command-line currently. Use, for example:

For an MDP, you can also export the set of maximal end components (MECs):