The experiments for the partial guard evaluation's optimization 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 technique. Each experiment has been performed ten times and its respective geometric means (states, transitions and times) are reported in the results. The results will be re-produced every day with the latest nightly-build version of ProB. 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 |
|---|---|---|
| BF/DF | probcli filename -mc 160000 | Consistency checking using mixed breadth-first and depth-first search. |
| BF/DF+PGE | probcli filename -mc 160000 -p pge disabled | Consistency checking with partial guard evaluation (PGE) using mixed breadth-first and depth-first search. |
| BF | probcli filename -mc 160000 -bf | Consistency checking using breadth-first search. |
| BF+PGE | probcli filename -mc 160000 -bf -p pge disabled | Consistency checking with partial guard evaluation (PGE) using breadth-first search. |
| DF | probcli filename -mc 160000 -df | Consistency checking using depth-first search. |
| DF+PGE | probcli filename -mc 160000 -df -p pge disabled | Consistency checking with partial guard evaluation (PGE) using depth-first search. |
The B and Event-B machines with which the optimisation technique has been tested 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.