search
Table of Contents
Model Description
A simple scheduler that contains an assertion violation.
Classes: 24
SLOC: 838
Parameters: (abs?)
Summary Results Table
| 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) |
Java Pathfinder
Stateless Random Walk
| Parameters | Path Error Density |
|---|---|
| a | 0.190 |
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 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| (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 |
