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 set of reachable states;
• the transition matrix;
• the state rewards vector(s);
• the transition rewards matrix (or matrices).
• labels (in the model or properties) and the states that satisfy them

Note that the last of these also provides a way to export information about initial states and deadlock states (via the built-in labels "init" and "deadlock").

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.

From the command-line version of PRISM, use the following switches:

• -exportstates <file>
• -exporttrans <file>
• -exportstaterewards <file>
• -exporttransrewards <file>
• -exportlabels <file>

or, as explained below, use the more convenient switch:

• -exportmodel <files[:options]>

Replace <file> with stdout in any of the above to print the information to the terminal.

The export command-line switches can be used in combination. For example:

exports both the state space and transition matrix. You can export both state and transition rewards using the -exportrewards switch. The following are equivalent:

When there are multiple reward structures, a separate file is created for each one and a (1-indexed) suffix is added to distinguish them.

You can also easily perform multiple exports simultaneously using the -exportmodel switch, which specifies multiple files using a list of extensions. The file extensions then dictate what is exported. For example:

exports the transition matrix and states list to out.tra and out.sta, respectively. If you omit the file basename (out in this case), then the basename of the model file (poll2 in this case) is used. For example:

exports the transition matrix and states list to poll2.tra and poll2.sta.

Possible file extensions are: .sta (reachable states), .tra (transition matrix), .srew (state rewards), .trew (transition rewards), .lab (labels). You can use the shorthand .all to export everything, and .rew to export both state and transition rewards. For example:

create multiple files of the form out.* or poll2.*, respectively.

As mentioned above, 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.

Finally, the -exportmodel switch can be passed various options. The general form is -exportmodel files:options where options is a comma-separated list of options taken from the following list:

• mrmc - export data in MRMC format
• matlab - export data in Matlab format
• rows - export matrices with one row/distribution on each line
• ordered - output states indices in ascending order [default]
• unordered - don't output states indices in ascending order

An example is:

The meaning of these options is described below.

File formats

By default, model data is exported (or displayed) in plain text format. The precise details of the formats used can be found in the "Explicit Model Files" appendix. As mentioned above, by convention, we use file extensions .sta (for states files), .tra (for transitions files), .rews and .rewt (for state/transition rewards files) and .lab (for labels).

Alternatively, it is possible to export this information as Matlab code (a .m file) or in a format suitable for import into the MRMC tool. Select the appropriate menu item when using the GUI, or add the command-line switches:

• -exportmatlab
• -exportmrmc

or, as described earlier, pass options to the -exportmodel switch.

There is no specific MRMC format for labels, so these are exported as plain text in this case.

There is some additional export functionality available only from the command-line.

Firstly, when outputting matrices for DTMCs or CTMCs, it is possible to request that PRISM does not sort the rows of the matrix, as is normally the case. This is achieved with the switch:

• -exportunordered

The reason for this is that in this case PRISM does not need to construct an explicit version of the model in memory and the process can thus be performed with reduced memory consumption.

Secondly, there is a switch:

• -exportrows

which provides an alternative output format for transition matrices where the elements of each row of the matrix (i.e. the transitions from a state/choice) are grouped on the same line. This can be particularly helpful for viewing the matrix for MDPs. The file format is shown here.

Graphical model export

The transition matrix of the model can also be exported in Dot format, which allows easy graphical visualisation of the graph structure of the model. You can optionally request that state descriptions are added to each state of graph; if not, states are labelled with integer indices that can be cross-referenced with the list of reachable states.

Use the menu entries under "Model | Export | Transition matrix" from the GUI or command-line switches:

• -exporttransdot <file>
• -exporttransdotstates <file>

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):