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. Two formats for explicit model import are currently supported:

• plain text files (sometimes referred to as "explicit" or ".tra" files)
• UMB (Unified Markov binary) format, a binary format supported by other probabilistic model checkers

Presently, this functionality is only supported in the command-line version of the tool, usually using the -importmodel switch. In a similar fashion to -exportmodel switch, the type of import is usually determined from the file extension.

For UMB, all model info is contained in a single file. An example of import is:

For the plain text files (.tra etc.), various options are possible. To just import the core part of the model (the transition function) use:

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

Using the same formats as for model export, other parts of the model can also be imported:

• .lab - labels
• .srew, .trew - rewards: states, transitions
• .sta - states
• .obs - observations

Here is an example of also importing labels and states:

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

Note also that, 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.

Use the extension .all to import from any matching files with appropriate extensions:

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

Efficiency

Please note, for PRISM's symbolic model construction/engines, which are often used by default, this explicit method of constructing models in PRISM is typically less efficient than using the PRISM language. This is because the underlying data structures used to represent the model function better when there is high-level structure and regularity to exploit. You may want to switch to the "explicit" engine:

The situation can also be alleviated to a certain extent for the symbolic implementations by importing the .sta file, since the composition of the states reintroduces some regularity (although is still typically inefficient to construct).

Other options

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.