search
Table of Contents
Model Description
A race condition in the model.
Classes: 6
SLOC: 103
Parameters: (gc, wc, envFirst?)
Summary Results Table
| raxextended (2,3) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
|---|---|---|---|---|
| JPF “Randomized DFS” | 100 (100) 1.00 | 2.42s | 9488.65 (0.00) | 285.73 (277.29) |
| JPF Stateless Random Walk | 10127 (1288) 0.13 | NA | NA (NA) | NA (NA) |
| raxextended (4,3) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 48.26s | 615352.88 (0.00) | 829.48 (802.28) |
Java Pathfinder
Stateless Random Walk
| Parameters | Path Error Density |
|---|---|
| 2,3 | 0.128 |
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 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| (2,3) | 100 (100) 100.00% | 2.42s | 9488.65 (0.00) | 285.73 (277.29) | 2416.94 | 2316.94 | 285.73 | 277.29 | 1782.51 | 7706.14 | 0.00 | 9210.36 | 1504.67 | 0.00 | 31459.84 | 6990528.00 | 1305.71 | 196.39 | 196.39 |
| (4,3) | 100 (100) 100.00% | 48.26s | 615352.88 (0.00) | 829.48 (802.28) | 48262.50 | 4461.25 | 829.48 | 802.28 | 64984.05 | 550368.83 | 0.00 | 614549.60 | 64181.20 | 0.00 | 275468.16 | 6990528.00 | 114670.13 | 213.99 | 214.29 |
