If required, once the model has been constructed it can be exported, either for manual examination or for use in another tool. In the GUI, the "Model | Export" menu provides options to export various components of the model:
In all cases, it is possible to export this information either in plain text format or as Matlab code. Additionally, matrices and vectors can be exported in a format suitable for import into the MRMC tool and the transition matrix of the model can be exported in Dot format which allows easy graphical visualisation of the graph structure of the model. For the latter, 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 set of reachable states. The GUI also provides options in the "Model | View" menu, which allow exports (in textual format) directly to the log. This is convenient for quick examination of small models.
All of this export functionality is available from the command-line version of PRISM, using the following switches:
-exportstates <file>
-exporttrans <file>
-exportstaterewards <file>
-exporttransrewards <file>
-exporttransdot <file>
-exporttransdotstates <file>
In each case, using stdout
instead of a file name causes the information to be displayed directly to the screen.
To change the export format from the default (plain text) to Matlab or MRMC, use the -exportmatlab
and -exportmrmc
switches.
The export command-line switches can be used in combination. For example:
exports both the state space and transition matrix in Matlab format.
Finally, there is some additional export functionality available only from the command-line.
Firstly, in the case where both a model file and properties file have been specified,
it is possible to export the set of states satisfied by each label in the properties file, including the built-in labels "init"
and "deadlock"
.
This is done with the -exportlabels
switch and the information
can be output either in plain text format (default) or for use with Matlab or MRMC (see switches above).
Secondly, 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 -exportunordered
switch.
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.
Finally, the -exportrows
switch provides an alternative output format for transition matrices where the elements of each row of the matric are grouped on the same line. This can be particularly helpful for viewing the matrix for MDPs. By way of example:
becomes: