www.prismmodelchecker.org

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, using the -importtrans switch (and more convenient -importmodel; see below). PRISM makes some attempt to discern 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:

prism -importtrans poll2.tra -ctmc

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):

prism poll2.sm -exporttrans poll2.tra -exportstates poll2.sta
prism -importtrans poll2.tra -importstates poll2.sta -ctmc

You can also import label information using the switch -importlabels, e.g.:

prism -importtrans poll2.tra -importstates poll2.sta -importlabels poll2.lab -ctmc

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 files output from -exportstates and -exporttrans, but are included in the labels file, -importlabels should also be used to designate a particular initial state for a model. If not, the default is to assume a single initial state, in which all variables take their minimum value (if -importstates is not used, the model has a a single zero-indexed variable x, and the initial state is x=0).

Lastly, state (but currently not transition) rewards can also be imported, using the -importstaterewards switch, e.g.:

prism -importtrans poll2.tra -importstates poll2.sta -importlabels poll2.lab -importstaterewards poll2.srew -ctmc

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

In a similar style to PRISM's -exportmodel switch, you can import several several files for a model using a single -importmodel switch. For example, this is equivalent to the command given above:

prism -importmodel poll2.tra,sta,lab,srew -ctmc

The contents of each file is determined by its extension: Possible file extensions are: .sta (reachable states), .tra (transition matrix), .lab (labels), .srew (state rewards).

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

prism -importmodel poll2.all -ctmc

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

prism poll2.all -ctmc

PRISM Manual

Running PRISM

[ View all ]