search
Table of Contents
Model Description
The model contains a deadlock.
Classes: 4
SLOC: 51
Parameters: (#first, #second, #iter)
Summary Results Table
| clean (1,1,12) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
|---|---|---|---|---|
| JPF “Randomized DFS” | 100 (100) 1.00 | 1.54s | 1742.56 (0.00) | 161.30 (14.97) |
| JPF Stateless Random Walk | 10125 (336) 0.03 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (1) 1.00 | 0.93s | 1800.00 (10.00) | 180.00 (NA) |
| ConTest | 1000 (30) 0.03 | NA | NA (NA) | NA (NA) |
| clean (10,10,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 114 (110) 0.96 | 113.28s | 1326102.90 (0.00) | 221.93 (218.74) |
| JPF Stateless Random Walk | 10129 (2928) 0.29 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (0) 0.00 | NA | NA (NA) | NA (NA) |
| ConTest | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
Chess
- ChessBound=2
- ChessMonitorVolatiles=false
| Clean Params | Tests | Found Error | Time Taken | Steps (Depth) |
|---|---|---|---|---|
| 1,1,12 | 10 | Yes | 0.93 secs | 180 |
| 10,10,1 | >=398,000 | No | 3604.715 secs | 242 |
Java PathFinder
Stateless Random Walk
- 10,000 Trials of Random Walk
- The ratio of the error discovery trials over the total number of trials is the
path error density.
| Clean Params | Path Error Density |
|---|---|
| 1,1,12 | 0.033 |
| 10,10,1 | 0.289 |
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 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| (1,1,12) | 100 (100) 100.00% | 1.54s | 1742.56 (0.00) | 161.30 (14.97) | 1539.79 | 1539.79 | 161.30 | 14.97 | 906.75 | 835.81 | 0.96 | 1726.59 | 889.82 | 0.00 | 17153.92 | 6990528.00 | 0.00 | 138.00 | 149.00 |
| (10,10,1) | 114 (110) 96.49% | 113.28s | 1326102.90 (0.00) | 221.93 (218.74) | 113278.95 | 3154.25 | 221.93 | 218.74 | 281078.65 | 1045024.25 | 0.60 | 1325883.16 | 280858.31 | 0.00 | 452811.64 | 6990528.00 | 163324.80 | 210.00 | 221.00 |
ConTest
- 1000 independent trials
- The ratio of the error discovery trials over the total number of trials is the
path error density.
| Clean Params | Path Error Density |
|---|---|
| 1,1,12 | 0.030 |
| 10,10,1 | ? (not-halt or deadlock) |
CalFuzzer
Not Applicable. The initial dynamic analysis does not find any input target locations.
