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
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:
or, as explained below, use the more convenient switch:
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.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
Possible file extensions are:
.sta (reachable states),
.tra (transition matrix),
.srew (state rewards),
.trew (transition rewards),
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
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 is not exported when using
-exportmodel switch can also be used to export the transition matrix
in Dot format which allows easy graphical visualisation of the model:
-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.
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),
.rewt (for state/transition rewards files)
.lab (for labels).
Alternatively, it is possible to export this information as Matlab code
.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:
or, as described earlier, pass options to the
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:
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:
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:
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):