It is also now 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).
Presently, this functionality is only supported in the command-line version of the tool, using the -importtrans switch.
At the moment, PRISM makes no attempt to discern the model type from the input file.
By default it assumes that the model is an MDP.
If this is not the case, 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 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):
Lastly, since information about the initial state of a model is not preserved in the files output from -exportstates and -exporttrans,
you can also use the -importinit switch to specify an initial state of the imported model.
The format is a comma-separated list of variable assignments, e.g. -importinit s=1,a=0,s1=1,s2=1.
Variables for which no value is provided are assumed to take their minimum value in the initial state.
Imported models for which no states information was provided by default have a single zero-indexed variable x,
so in this case you might use for example the switch -importinit x=100 to override the default initial state of x=0.
