View - Edit - Print - Search

Running PRISM /

Explicit Model Import

It is also possible to construct models in PRISM through direct specification of their transition matrix. The format in which this information is input to the tool is exactly the same as is currently output (see the section "Exporting The Model" and the appendix "Explicit Model Files"). Presently, this functionality is only supported in the command-line version of the tool, usually using the -importmodel switch, e.g.:

PRISM tries to determine the model type from the format of the input files, but if this does not work, the model type can be overwritten using the -dtmc, -ctmc and -mdp switches. For example:

Please note that this method of constructing models in PRISM is typically less efficient than using the PRISM language. This is because PRISM is (primarily) a symbolic model checker and the underlying data structures used to represent the model function better when there is high-level structure and regularity to exploit. This situation can be alleviated to a certain extent by importing not just a transition matrix, but also a definition of each state of the model in terms of a set of variables. The format of this information is again identical to PRISM's current output format, using the -exportstates switch. The following example shows how PRISM could be used to build, export and then re-import a model (not a good strategy in general):

If state information is not imported, a single zero-indexed variable x is assumed.

You can also import information about labels (by default, from a file with extension .lab), e.g.:

where the labels file (poll2.lab above) is in the format generated by the -exportlabels export option of PRISM.

In particular, since details about the initial state(s) of a model are not preserved in the .tra file, but are included in the labels file, this should also be used to designate a particular initial state for a model. Otherwise, state 0 is assumed to be the initial state or, if state information is imported, the state in which all variables take their minimum value is used.

Lastly, state and transition rewards can also be imported, assuming extensions .srew and .trew.

Use the extension .all to import from all of these files:

In this case, you can omit the -importmodel switch and just specify the .all-ended filename, e.g.:

In a similar style to PRISM's -exportmodel switch, while -importmodel is usually the most convenient, you can also specify each part separately, e.g.:

There are also -importstaterewards and -impottransrewards switches. You can import multiple reward structures using multiple instances of the these switches. If present in the rewards files (see the appendix "Explicit Model Files"), the names of the reward structures are read too.