Test Suite

Test Suite#

The R2U2 test suite is intended to test c2po.py and r2u2. Each test case in a suite has an MLTL specification, a trace, and an oracle. The test script compiles the MLTL specification using the given c2po.py script, runs the given r2u2 binary over the compiled specification and trace, and compares the output to the oracle.

The tests also include a “hyper tester” that tests R2U2 over all possible traces for variations of a given formula. This test will likely take a long time on a personal machine (>1 hour) to complete.

Usage#

To run the test suite, run the r2u2test.py script as follows:

python r2u2test.py path/to/c2po.py path/to/r2u2bin SUITE1 SUITE2 ...

where path/to/c2po.py is the relative or absolute path to the c2po.py script to use for compiling specifications, path/to/r2u2bin is the relative or absolute path to the r2u2 binary to run, and SUITE1 SUITE2 ... is a non-empty list of suite names to run.

An example command to run the regression test suite from the top-level r2u2/ directory is as follows:

python test/r2u2test.py compiler/c2po.py monitors/c/build/r2u2 regression

assuming that the C version of the r2u2 binary has been built. The test results can be seen in the test/results directory by default.

Use the --copyback option to copy all the files used in the test case to the results directory. This is useful for re-running and debugging specific test cases.

To run the hyper tester, install all the python requirements via pip install -r requirements.txt then run via python3 hyper_test.py

Suites#

The JSON files in the test/suites directory correspond to the available suites. Some available suites are:

  • ft_subset

  • pt_subset

  • regression

  • cav

  • all (runs every suite in test/suites)

Adding New Suites#

To add a new suite, it is easiest to build off of an existing JSON configuration file. The structure of the JSON files is as follows:

{
    "suite": "SUITE_NAME",
    "options": {
        "compiler-option": "COMPILER_OPTION_VALUE"
    },
    "tests": [
        {
            "name": "TEST_NAME",
            "mltl": "MLTL_FILENAME",
            "trace": "TRACE_FILENAME",
            "oracle": "ORACLE_FILENAME",
            "options": {
                "compiler-option": "COMPILER_OPTION_VALUE"
            }
        }
    ],
    "suites": [ "SUITE_1", "SUITE_2", "..." ]
}

where "SUITE_NAME" should be the same as the name of the JSON file (minus the .json extension), "options" is an object corresponding to the CLI options given to the compiler (these options can be overridden for individual tests), "tests" is an array of objects that describe test cases.

The test cases require a "name", an "mltl" filename that exists in in test/mltl, a "trace" filename that exists in test/trace, and an "oracle" filename that exists in test/oracle.

Each "SUITE_N" in the "suites" attribute should be the name of a suite in the suites/ directory, where each named suite will be run.