A simple scheduler that contains an assertion violation.

Classes: 24

SLOC: 838

Parameters: (abs?)

deosA () | ||||

Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
---|---|---|---|---|

JPF “Randomized DFS” | 100 (100) 1.00 | 2.87s | 1184.21 (0.00) | 39.98 (27.78) |

JPF Stateless Random Walk | 10129 (1925) 0.19 | 1.95s | 9.03 (NA) | 0.00 (NA) |

Parameters | Path Error Density |
---|---|

a | 0.190 |

- 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 |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

(a) | 100 (100) 100.00% | 2.87s | 1184.21 (0.00) | 39.98 (27.78) | 2874.56 | 2874.56 | 39.98 | 27.78 | 747.11 | 437.10 | 0.55 | 1155.43 | 718.78 | 0.00 | 38716.16 | 6990528.00 | 0.00 | 295.17 | 295.25 |