Running PRISM /

Experiments

PRISM supports experiments, which is a way of automating multiple instances of model checking. This is done by leaving one or more constants undefined, e.g.:

This can be done for constants in the model file, the properties file, or both. Before any verification can be performed, values must be provided for any such constants. In the GUI, a dialog appears in which the user is required to enter values. From the command line, the -const switch must be used, e.g.:

To run an experiment, provide a range of values for one or more of the constants. Model checking will be performed for all combinations of the constant values provided. For example:

where N=4:6 means that values of 4,5 and 6 are used for N, and T=60:10:100 means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for T. For convenience, constant specifications can be split across separate instances of the -const switch, if desired.

From the GUI, the same thing can be achieved by selecting a single property, right clicking on it and selecting "New experiment" (or alternatively using the popup menu in the "Experiments" panel). Values or ranges for each undefined constant can then be supplied in the resulting dialog. Details of the new experiment and its progress are shown in the panel. To stop the experiment before it has completed, click the red "Stop" button and it will halt after finishing the current iteration of model checking. Once the experiment has finished, right clicking on the experiment produces a pop-up menu, from which you can view the results of the experiment or export them to a file.

For experiments based on properties which return numerical results, you can also use the GUI to plot graphs of the results. This can be done either before the experiment starts, by selecting the "Create graph" tick-box in the dialog used to create the experiment (in fact this box is ticked by default), or after the experiment's completion, by choosing "Plot results" from the pop-up menu on the experiment. A dialog appears, where you can choose which constant (if there are more than one) to use for the x-axis of the graph, and for which values of any other constants the results should be plotted. The graph will appear in the panel below the list of experiments. Right clicking on a graph and selecting "Graph options" brings up a dialog from which many properties of the graph can be configured. From the pop-up menu of a graph, you can also choose to print the graph (to a printer or Postscript file) or export it in a variety of formats: as an image (PNG or JPEG), as an encapsulated Postscript file (EPS), in an XML-based format (for reloading back into PRISM), or as code which can be used to generate the graph in Matlab.

Approximate computation of quantitive results obtained with the simulator can also be used on experiments. In the GUI, select the "Use Simulation" option when defining the parameters for the experiment. From the command-line, just add the -sim switch as usual.

Exporting results

You can export all the results from an experiment to a file or to the screen. From the command-line, use the -exportresults switch, for example:

to send to output file res.txt, or:

to send the results straight to the screen. From the GUI, right click on the experiment and select "Export results".

The default behaviour is to export a list of results in text form, using tabs to separate items. The above examples produce:

You can change the format in which the results are exported by appending one or more comma-separated options to the end of the -exportresults switch, for example to export in CSV (comma-separated values) format:

You can also add the matrix option, to export the results as one or more 2D matrices, rather than a list. This is particularly useful if you want to create a surface plot from results that vary over two constants.

The matrix option is also available in normal (non-CSV) mode.

Finally, you can export results in the form of comments, used by PRISM's functionality: