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, 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.
A header in each file (see the "Explicit Model Files" appendix) also shows the name of the reward structure.
These headers can be omitted using the switch -noexportheaders (or via the option "Include headers in model exports" in the GUI).
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:
creates 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.
Although it is not exported when using .all, the -exportmodel switch can also be used to export the transition matrix
in Dot format which allows easy graphical visualisation of the model:
When exporting model details in this way, the precision of numerical values (e.g., for probabilities or rewards) can be configured.
From the command line, use the switch -exportmodelprecision <x> to show values to <x> significant digits.
The same setting is available for exports from the GUI via option "Precision of model export".
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
proplabels - also export labels from the properties file
An example is:
By default, when labels are exported, this only includes the labels from the model.
The proplabels option listed above
(which applies to both -exportmodel and -exportlabels)
indicates that labels from any properties file are exported too.
To export just those labels, use switch -exportproplabels <file>.
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),
.srew and .trew (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.
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>
As mentioned above, for the latter, the following is equivalent (and easier to remember):
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):
Site hosted at the Department of Computer Science, University of Oxford