Benchmarking

The prism-auto script

The PRISM distribution includes a script (in etc/scripts) called prism-auto designed to facilitate benchmarking and regression testing. It is used to automatically run a set of PRISM invocations (or any other executable that accepts the same inputs).

Typically, each call to PRISM requires a model file and a properties file containing one or more properties. prism-auto runs in one of two modes. The first (the default) is for benchmarking, which usually runs multiple properties against multiple models. The second is for regression testing and usually checks one or more models, each with an associated properties file - for example, a model model.prism and properties file model.prism.props. The latter is enabled using the switches -m (or --matching), to find matching model/properties files, and -t (or --test), which performs regression testing. See the section Regression Testing for details. Here, we describe the use of prism-auto for benchmarking.

Running prism-auto

Consider a directory containing two PRISM model files, model1.prism and model2.prism, and two properties files, p1.props and p2.props. The basic usage of prism-auto for benchmarking is just:

prism-auto model1.prism

This finds any properties files in the same directory as model1.prism and calls PRISM to check each one against the model. You can also see what would be run with this command using the -e (or --echo) switch:

prism-auto -e model1.prism

which would print:

prism model1.prism ./p1.props
prism model1.prism ./p2.props

In fact, prism-auto can take multiple files or directories as arguments. For directories, it will scan for all models in the directory (by default, recursively). So the following are equivalent here:

prism-auto .

prism-auto model1.prism model2.prism

and would execute:

prism ./model1.prism ./p1.props
prism ./model1.prism ./p2.props
prism ./model2.prism ./p1.props
prism ./model2.prism ./p2.props

Specifying Models, Constants and Arguments

Often, command-line switches will need to be provided to PRISM for it to run. A common example of this is the provision of values for constants in a model or property using the -const switch. The arguments needed for a particular model or property can be provided in an accompanying .args file. For example, if model2.prism.args contains the single line -const N=2, then prism-auto . will run:

prism ./model1.prism ./p1.props
prism ./model1.prism ./p2.props
prism ./model2.prism -const N=2 ./p1.props
prism ./model2.prism -const N=2 ./p2.props

and if p2.props.args additionally contains -const T=10, then the result will be:

prism ./model1.prism ./p1.props
prism ./model1.prism ./p2.props -const T=10
prism ./model2.prism -const N=2 ./p1.props
prism ./model2.prism -const N=2 ./p2.props -const T=10

Each line of the .args file can contain as many switches/arguments as needed. Multiple lines will result in multiple calls to PRISM. For example, if model2.prism.args contains:

-const N=2
-const N=3

then prism-auto model2.prism will run:

prism model2.prism -const N=2 ./p1.props
prism model2.prism -const N=2 ./p2.props
prism model2.prism -const N=3 ./p1.props
prism model2.prism -const N=3 ./p2.props

An alternative approach for specifying a set of models and accompanying switches is to provide a models file, and then run prism-auto on the directory (e.g., prism-auto .). This is done, for example, in the PRISM benchmark suite. Here is an example models file:

model1.prism -const M=5
model2.prism -const N=2
model2.prism -const N=3

Note that the models listed in this file can be a subset of the ones in the directory, and this overrides the default behaviour of using all models.

Lines in .args or models files starting with # are ignored by prism-auto. This can be used either to add comments to the files, or to temporarily disable a model/argument. If you want to read from a file called something other than models, use the switch --models-filename=<file>.

You can also filter the set of models that are used with the filter-models switch. This relies on the provision of model metadata provided in a models.csv file, as is done for example in the PRISM benchmark suite (here is an example). Currently, the fields states and model_type are available, and can be used in a Python-formatted expression, as in these two examples:

prism-auto prism-benchmarks/models/dtmcs --filter-models="states<1000"

prism-auto prism-benchmarks/models --filter-models="states<10000 and model_type=='CTMC'"

If the model metadata is in a file other than models.csv, use --models-info=<file> to specify it.

Benchmarking with prism-auto

Benchmarking typically involves comparing two or more ways of performing the same model checking task. prism-auto, in conjunction with the script prism-log-extract, makes this process easy to automate. Here is a simple example, using the --args (or -a) and --log (or -l) switches:

prism-auto . --args args --log logs

where args is a file containing the lines:

-gs
-jac
-jor -omega 0.9

This runs PRISM on all model/property combinations in the current directory three times, using each of the three sets of command-line switches in the args file. The output of each run is stored in a separate log file in logs (this directory is created if it does not already exist) with the name of each log file being automatically generated using the model, property and switches (e.g., model1.prism.p2.props.jor.omega.0.9.log).

You can achieve the same thing without creating an args file using the --args-list switch:

prism-auto . --args-list '-gs,-jac,-jor -omega 0.9' --log logs

For commands like these, another useful option is --log-subdirs, which organises log files into subdirectories: for the example above, the logs directory would contain subdirectories gs, jac, etc. This works well with the script for extracting data from logs, described next.

Collating Information with prism-log-extract

The prism-log-extract script extracts and collates information from PRISM log files, such as those generated from an execution of prism-auto. Basic usage is just:

prism-log-extract logs

which will search (recursively) through all the files in the logs directory, extract all known pieces of information ("fields") from the files and then display them in a CSV file, one row per file.

The arguments to prism-log-extract can be one or more directories or files. For further control over which files are searched, you can for example use:

prism-log-extract --non-recursive --extension=log logs/test 

which looks in logs/test but does not search recursively, and only considers files matching *.log.

Typically, only a subset of the fields are required. This command just extracts the model filename, its constants and the time for model checking:

prism-log-extract --fields=model_file,model_consts,time_check logs

For a full list of the fields that are available, use prism-log-extract --show-fields. There are also several "meta-fields" available, which expand to multiple fields, e.g., model is both the filename and constants for the model and benchmark is the filenames and constants for both model and property.

prism-log-extract can also group together rows of the CSV file which have common values for some fields, providing easier comparisons. Here is a typical example of prism-auto and prism-log-extract combined:

prism-auto logs --args-list "-pow,-jac,-gs" --log logs --log-subdir
prism-log-extract logs --groupby=log_dir --groupkey=benchmark --fields=time_check > times.csv

The result will be a CSV file, where each row is for a different benchmark (as specified by --groupkey) and where the time_check field is listed for each different log directory name (as specified by --groupby); these are pow, jac, and gs, which are the subdirectories created by prism-auto. So times.csv looks ike:

model_file,model_consts,prop_file,prop_consts,pow:time_check,gs:time_check,jac:time_check
"brp.pm","N=16,MAX=2","p1.pctl","",0.034,0.031,0.032
"brp.pm","N=16,MAX=2","p2.pctl","",0.025,0.027,0.026
"brp.pm","N=16,MAX=2","p4.pctl","",0.006,0.006,0.006
"brp.pm","N=16,MAX=3","p1.pctl","",0.03,0.033,0.03
...

Other prism-auto Options

Here are some other useful options that can be provided to prism-auto (run prism-auto --help for a full list.

--extra: You can provide extra command-line switches to be added to all PRISM invocations using --extra (or -x). Separate multiple switches with spaces:

prism-auto . --extra -ex

--prog: By default, all invocations just call prism. This means prism needs to be in your path. If it is not, or you want to run a different program, use --prog (or -p):

prism-auto . --prog /home/dave/prism-branch/prism/bin/prism

prism-auto . --prog prism-games

--timeout: You can set a timeout delay so that any PRISM invocation taking longer than this is cleanly killed, and the next invocation executed. This is done using the --timeout switch. For example, to timeout after 30 seconds, 90 minutes or 2 hours:

prism-auto . --timeout=30s

prism-auto . --timeout=90m

prism-auto . --timeout=2h

--build: If you want to just build models, and not execute model checking, use the --build (or -b) switch. Here's the command we use to generate logs for the model metadata in each directory of the PRISM benchmark suite:

find dtmcs ctmcs mdps -type d -exec prism-auto -p prism -n -b {} -l {}/logs \;