The experiments for the enabling analysis of ProB are presented on this web page. The test cases were performed by using the nightly-build command line version of the ProB tool. The benchmarks are produced by running four different checks (see the table below) in order to evaluate the reduction technique. Each experiment has been performed ten times and its respective geometric means (run-times and wall-times) are reported in the results. The results are re-produced every day with the latest nightly-build version of ProB and are saved into an Excel-File that consists of three worksheets: 1. System and Tools Info (contains information about the current ProB version and the system where the tests are performed), 2. Benchmarks (contains the essential results of the performed benchmarks), 3. Benchmarks' Statistics (complementary statistical data such as standard deviation, min, max, etc.). All tests are currently run on an Intel Xeon Server, 8 x 3.00 GHz Intel(R) Xeon(TM) CPU with 8 GB RAM running Ubuntu 12.04.3 LTS.
| Check | Command Line Instruction | Description |
|---|---|---|
| Enabling Analysis | probcli filename -enabling_analysis | Running the enabling analysis for filename, where filename is a B or Event-B machine. |
The B and Event-B machines with which the technique was evaluated can be downloaded from here. The latest nightly build version of ProB can be downloaded from ProB nightly.
The web page is maintained by Ivaylo Dobrikov.