Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the examples
directory of the distribution.
The model will then be displayed in the editor in the "Model" tab of the GUI window. The file is parsed upon loading. If there are no errors, information about the modules, variables, and other components of the model is displayed in the panel to the left and a green tick will be visible. If there are errors in the file, a red cross will appear instead and the errors will be highlighted in the model editor. To view details of the error, position the mouse pointer over the source of the error (or over the red cross). Alternatively, select menu option "Model | Parse Model" and the error message will be displayed in a message box. Model descriptions can, of course, also be typed from scratch into the GUI's editor.
In order to perform model checking, PRISM will (in most cases) need to construct the corresponding probabilistic model, i.e. convert the PRISM model description to, for example, an MDP, DTMC or CTMC. During this process, PRISM computes the set of states in the model which are reachable from the initial states and the transition matrix which represents the model.
Model construction is done automatically when you perform model checking. However, you may always want to explicitly ask PRISM to build the model in order to test for errors or to see how large the model is. From the GUI, you can do this by by selecting "Model | Build Model". If there are no errors during model construction, the number of states and transitions in the model will be displayed in the bottom left corner of the window.
From the command-line, simply type:
where model.nm
is the name of the file containing the model description.
For some types of models, notably PTAs, models are not constructed in this way (because the models are infinite-state). In these cases, analysis of the model is not performed until model checking is performed.
The presence of deadlock states in the model,
i.e. states which are reachable but from which there are no outgoing transitions, constitutes an error. From the GUI, you are offered the opportunity to automatically add self-loops to these states to resolve the situation.
The same can be achieved from the command-line by using the -fixdl
switch.
Otherwise, the deadlock states are displayed (in the GUI, they appear in the "Log" tab of the main window). Note that if you choose to fix the deadlocks by adding self-loops, you can determine in which states this occurred by model checking the property "deadlock"
. Another useful technique in this situation is to generate a random path in the simulator in the hope of reaching a deadlock state. This will give you useful information about how the state can be reached.