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:
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, the most convenient and flexible approach is to use the -exportmodel switch, for example:
The default export format is "explicit" plain text files (whose format is detailed in the "Explicit Model Files" appendix). The -exportmodel switch will auto-detect what is to be exported from the file extension provided. In the example above, .tra indicates the transition matrix/function, i.e., the model itself.
Other possible file extensions are:
.sta (reachable states),
.srew (state rewards),
.trew (transition rewards),
and .lab (labels).
You can also perform multiple exports simultaneously using the -exportmodel switch with multiple extensions, 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 (model in this case) is used. For example:
exports the transition matrix and states list to model.tra and model.sta.
You can use the shorthand .all to export everything, and .rew to export both state and transition rewards. For example:
creates multiple files of the form out.* or model.*, respectively.
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.
Other file formats are also available. For a graphical view of the transition matrix, export in the Dot format:
Or, you can export as Matlab code
(a .m file):
Export to Storm's DRN model format (extension .drn) is also supported.
If you don't want to rely on the format being detected by the file extension, you can use the format option, e.g.:
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.
Other options can be specified with the -exportmodel switch and there can be multiple instances of the switch, each with their own options.
Options are:
*format(=explicit/matlab/dot/drn) - model export format *matlab- same as format=matlab *rows- export matrices with one row/distribution on each line *proplabels- export labels from a properties file into the same file, too *actions(=true/false) - show actions on choices/transitions *headers(=true/false) - include headers when exporting rewards *precision(=n) - export probabilities/rewards withnsignificant decimal places
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):
Although -exportmodel is now usually the best switch for model exports, other older switches still exist. For example, these can be use to export particular parts of the model:
-exporttrans <file>
-exportstates <file>
-exportstaterewards <file>
-exporttransrewards <file>
-exportrewards <file> <file>
-exportlabels <file>
-exportproplabels <file>
And these switches specify the format for exports:
-exportmatlab
-exportrows
-exportmodelprecision <x>
Site hosted at the Department of Computer Science, University of Oxford