search
Table of Contents
Summary Results Table
| replicated (5,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
|---|---|---|---|---|
| JPF “Randomized DFS” | 100 (97) 0.97 | 203.71s | 716039.24 (0.00) | 383.79 (360.53) |
| replicated (8,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (97) 0.97 | 4.77s | 1800.77 (0.00) | 1799.77 (1799.77) |
| JPF Stateless Random Walk | 10159 (9632) 0.95 | 5.39s | 134.49 (NA) | 0.00 (NA) |
Java Pathfinder
Stateless Random Walk
| Parameters | Path Error Density |
|---|---|
| 8,2 | 0.948 |
Stateful Randomized Depth-first search
- 100 randomized depth-first search trial, where each trial is time-bounded at
one hour. A total of 100 computation hours dedicated in discovering the error.
- 2 MB of RAM allocated on each machine
- The Error Discovering Trials is the number of trials that discovered an error
among the initially launched trials (100).
| Parameters | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) | abs time (ms) | rel. time (ms) | search depth | errorDepth | new states | revisited states | end states | backtracks | processed states | restored states | total memory (kB) | max total memory | free memory (kB) | heap objects | max heap objects |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| (5,2) | 100 (97) 97.00% | 203.71s | 716039.24 (0.00) | 383.79 (360.53) | 203712.19 | 3288.24 | 383.79 | 360.53 | 167602.51 | 548436.73 | 0.22 | 715677.71 | 167240.76 | 0.00 | 347472.49 | 6990528.00 | 109416.73 | 726.43 | 735.43 |
| (8,2) | 100 (97) 97.00% | 4.77s | 1800.77 (0.00) | 1799.77 (1799.77) | 4772.70 | 4772.70 | 1799.77 | 1799.77 | 1800.77 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 58443.22 | 6990528.00 | 0.00 | 764.00 | 805.82 |
CHESS
| Parameters | Time | Transitions | paths | Max Depth |
|---|---|---|---|---|
| 5, 2, 0, 10, 05 | 620 | 103 | 1 | 103 |
| 8, 2, 0, 10, 001 | 620 | 157 | 1 | 157 |
