Regression Testing

PRISM has a regression test suite, which is built into the main PRISM repository, in the prism-tests directory.

You can trigger a full run of the regression test suite by running:

make tests

This is used for GitHub continuous integration, for example to automatically check commits and PRs. If you are submitting a PR, you should typically include a new test (or tests) in prism-tests, as appropriate. There is a specific bugfixes subdirectory for PRs that fix bugs. Here is an example. See below for details of the mechanisms for specifying tests and of the test suite itself.

During development of a feature branch, it's also common to put some tests in a directory prism/tests. These are also triggered by make tests (or can be triggered in isolation with make testslocal). These can then be migrated to the main prism-tests directory when stable.

There are also some JUnit tests in the prism/unit-tests subdirectory, which can be run as follows:

make unittests

Test mode

PRISM has some built-in support for testing. In particular, the command-line version of the tool has a test mode, enabled by using the -test switch. When in test mode, PRISM looks for the expected result of each property that it is checking, embedded in a comment immediately before the property. It then checks that the computed result is correct and reports an error if not.

The specification of an expected result looks like this:

// RESULT: 0.5
P=? [ F "goal" ]

and a run of PRISM in test mode looks like:

prism model.nm some-props.pctl -test

For each correctly checked property, PRISM displays a line of the form:

Testing result: PASS

after the result of model checking. If the result is incorrect, PRISM display an error message

Testing result: FAIL: Wrong result (expected 0.5)

and terminates immediately. If you want to the see testing result for all properties, regardless of correctness, use the switch -testall instead:

prism model.nm some-props.pctl -testall

Result specification

The RESULT notation illustrated above allows a variety of different types of expected results to be specified, depending on the type and result of the property being checked.

Some typical examples, of varying types, are:

// RESULT: 0.5
Pmax=? [ F s=2 ];

// RESULT: 1/2
Pmax=? [ F s=2 ];

// RESULT: true
P<0.6 [ F s=2 ];

// RESULT: 2
ceil(Pmax=? [ F s=2 ]) + 1;

Notice that you can use rationals (e.g. 1/2 above) if you know the exact result. Conversely, if the result is only known to fall within some range, an interval can be given:

// RESULT: [0.43162,0.431214]
Pmax=? [ F s=2 ];

If PRISM generates numerical results to a known level of accuracy, then this is used when checking the result. If not, a default accuracy of 1e-5 (relative error) is used.

If PRISM should generate an error on a particular property, you can specify this as follows:

// RESULT: Error
Pmax=? [ F<=(-1) s=2 ];

You can also specify that one or more specific words should occur in the error message that results when checking the property:

// RESULT: Error:Invalid
Pmax=? [ F<=(-1) s=2 ];

// RESULT: Error:Invalid,bound
Pmax=? [ F<=(-1) s=2 ];

Note that there should be no spaces after "Error:" or between any words that follow it.

If the result of model checking depends on a constant, you can embed this information in the result too. For example:

// RESULT (N=1): 0.5
// RESULT (N=2): 0.75
// RESULT (N=3): 0.875
Pmax=? [ F s=2 ];

or:

// RESULT (K=1,N=1): 0.5
// RESULT (K=1,N=2): 0.75
// RESULT (K=2,N=1): 0.4
// RESULT (K=2,N=2): 0.65
Pmax=? [ F s=2 ];

Or, you can write the expected result as a PRISM expression in terms of the constant:

// RESULT: p/(4-2*p)
P=? [ F s=2 ];

Regression test suite

The regression test suite, as used by make tests is in the prism-tests directory.

Tests are grouped into directories. A test usually comprises a model file (e.g. model.nm) and an accompanying properties file (e.g. model.nm.props) annotated with expected results. Optionally, there may be a file containing some command-line arguments needed to run the test (e.g. model.nm.props.args). Multiple lines in the .args file yield multiple tests.

This structure is designed to allow easy automatic testing using the prism-auto script, found in the etc/scripts directory of PRISM distributions. For example:

prism-auto -m -t model.nm

runs PRISM in test mode on a specific test, and:

prism-auto -m -t .

recursively finds all tests in the current directory and runs PRISM in test mode on all of them. The -m (or --matching) tells prism-auto to look for properties files that have names matching each model, as in the example names above. The -t (or --test) switch enables test mode and also suppresses all output except for the result of testing.

When in test mode, prism-auto will also look for exported files (i.e. anything that is an argument of a switch starting -export...), and check it against a file containing the expected output, which should be present in the current directory. If you want to run a test that does not need a properties file, create a matching file ending in .test, for example model.nm.test or model.nm.somename.test, containing the required command-line arguments (as in a .args file).

You can use other features of prism-auto too, for example, you can run the tests using a different version of PRISM, using -p (or --prog):

prism-auto -m -t -p /my/branch/of/prism .

or you can pass additional argument(s) to PRISM using -x (or --extra), e.g.:

prism-auto -m -t -x -s .

prism-auto -m -t -x "-s -gs" .

You can achieve the same thing by providing a global .args file. For example, create a file called test.args with one line "-s -gs" and then specify this to prism-auto using the -a (or --args) switch:

prism-auto -m -t -a test.args .

If the global .args file contains multiple lines, then prism is executed once for each line.

Use -e (or --echo) to just echo the test commands to the terminal, rather than execute them:

prism-auto -m -t -e .

or use --echo-full for expanded functionality which also prints out additional commands mimicking additional outputs, checks and exports done by prism-auto.

Use switch --test-all to run PRISM with the -testall (rather than -test) switch mentioned above:

prism-auto -m -t --test-all .

Type prism-auto -help to see more available options.