search
Table of Contents
Model Description
The model deadlocks because a wait() is enclosed within an if statement instead of a while statement.
Classes: 2
SLOC: 71
Parameters: (#seatRequests, #passengers, capacity)
Summary Results Table
| piper (2,16,8) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
|---|---|---|---|---|
| JPF “Randomized DFS” | 9995 (6) 0.00 | 1.31s | 325.50 (0.00) | 324.50 (324.50) |
| JPF Stateless Random Walk | 10125 (6) 0.00 | NA | NA (NA) | NA (NA) |
| piper (2,2,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 150 (150) 1.00 | 1.58s | 2276.49 (0.00) | 53.93 (40.53) |
| piper (2,4,4) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 150 (150) 1.00 | 54.71s | 838403.57 (0.00) | 108.29 (81.40) |
| JPF Stateless Random Walk | 10116 (289) 0.03 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (1) 1.00 | 18.83s | 628824.00 (3743.00) | 168.00 (NA) |
| ConTest | 1000 (11) 0.01 | NA | NA (NA) | NA (NA) |
| piper (2,5,4) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 206.89s | 3057202.80 (0.00) | 126.45 (100.04) |
| piper (2,6,4) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (97) 0.97 | 283.17s | 3883492.16 (0.00) | 143.87 (117.64) |
| piper (2,7,4) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (96) 0.96 | 334.26s | 4566700.58 (0.00) | 160.06 (133.93) |
| piper (2,8,4) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 5000 (4770) 0.95 | 301.58s | 3755044.80 (0.00) | 179.06 (151.94) |
| JPF Stateless Random Walk | 10124 (850) 0.08 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (1) 1.00 | 42.65s | 1531872.00 (5319.00) | 288.00 (NA) |
| ConTest | 100 (11) 0.11 | NA | NA (NA) | NA (NA) |
| piper (2,8,5) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 5025 (2866) 0.57 | 1179.77s | 14552031.67 (0.00) | 184.68 (150.43) |
| JPF Stateless Random Walk | 10124 (301) 0.03 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (1) 1.00 | 12.86s | 459936.00 (1597.00) | 288.00 (NA) |
| ConTest | 100 (1) 0.01 | NA | NA (NA) | NA (NA) |
| piper (2,8,6) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 4987 (429) 0.09 | 1329.92s | 16186995.16 (0.00) | 180.35 (146.60) |
| JPF Stateless Random Walk | 10123 (83) 0.01 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (1) 1.00 | 12.86s | 459936.00 (1597.00) | 288.00 (NA) |
| ConTest | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
| piper (2,8,7) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 5186 (91) 0.02 | 1487.44s | 18341935.22 (0.00) | 176.79 (143.89) |
| JPF Stateless Random Walk | 10130 (17) 0.00 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (1) 1.00 | 12.86s | 459936.00 (1597.00) | 288.00 (NA) |
| ConTest | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
Chess
- ChessBound=2
- ChessMonitorVolatiles=false
| AccountSubtype Params | Tests | Found Error | Time Taken | Steps (Depth) |
|---|---|---|---|---|
| 2,4,4 | 3,743 | Yes | 18.829 secs | 168 |
| 2,8,4 | 5,319 | Yes | 42.651 secs | 288 |
| 2,8,5 | 1,597 | Yes | 12.855 secs | 288 |
| 2,8,6 | 1,597 | Yes | 8.268 secs | 288 |
| 2,8,7 | 1,597 | Yes | 8.221 secs | 288 |
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.
| Parameters | Path Error Density |
|---|---|
| 2,4,4 | 0.029 |
| 2,8,4 | 0.083 |
| 2,8,5 | 0.030 |
| 2,8,6 | 0.008 |
| 2,8,7 | 0.002 |
| 2,16,7 | 0.0006 |
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,7,4) | 100 (96) 96.00% | 334.26s | 4566700.58 (0.00) | 160.06 (133.93) | 334260.55 | 4928.19 | 160.06 | 133.93 | 871245.98 | 3695454.60 | 0.89 | 4566565.66 | 871110.17 | 0.00 | 1105157.33 | 6990528.00 | 420132.95 | 219.00 | 230.00 |
| (2,16,8) | 9995 (6) 0.06% | 1.31s | 325.50 (0.00) | 324.50 (324.50) | 1306.17 | 1306.17 | 324.50 | 324.50 | 325.50 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 15488.00 | 932096.00 | 0.00 | 327.00 | 338.00 |
| (2,8,4) | 5000 (4770) 95.40% | 301.58s | 3755044.80 (0.00) | 179.06 (151.94) | 301575.26 | 4681.66 | 179.06 | 151.94 | 742889.64 | 3012155.16 | 0.92 | 3754891.86 | 742735.78 | 0.00 | 334799.17 | 932096.00 | 158633.07 | 231.00 | 242.00 |
| (2,8,5) | 5025 (2866) 57.03% | 1179.77s | 14552031.67 (0.00) | 184.68 (150.43) | 1179766.68 | 4888.26 | 184.68 | 150.43 | 3061014.77 | 11491016.91 | 0.96 | 14551880.24 | 3060862.38 | 0.00 | 413719.60 | 932096.00 | 185184.04 | 231.00 | 242.00 |
| (2,8,6) | 4987 (429) 8.60% | 1329.92s | 16186995.16 (0.00) | 180.35 (146.60) | 1329924.23 | 4499.45 | 180.35 | 146.60 | 3208115.95 | 12978879.21 | 0.92 | 16186847.55 | 3207967.42 | 0.00 | 403275.04 | 932096.00 | 183196.31 | 231.00 | 242.00 |
| (2,8,7) | 5186 (91) 1.75% | 1487.44s | 18341935.22 (0.00) | 176.79 (143.89) | 1487437.86 | 3733.93 | 176.79 | 143.89 | 3564384.73 | 14777550.49 | 0.85 | 18341790.33 | 3564238.99 | 0.00 | 384064.00 | 932096.00 | 161049.68 | 231.00 | 242.00 |
| (2,2,2) | 150 (150) 100.00% | 1.58s | 2276.49 (0.00) | 53.93 (40.53) | 1583.92 | 1583.92 | 53.93 | 40.53 | 995.87 | 1280.63 | 0.87 | 2234.96 | 953.46 | 0.00 | 18155.52 | 932096.00 | 0.00 | 159.00 | 170.00 |
| (2,4,4) | 150 (150) 100.00% | 54.71s | 838403.57 (0.00) | 108.29 (81.40) | 54711.95 | 4838.51 | 108.29 | 81.40 | 214919.68 | 623483.89 | 0.98 | 838321.17 | 214836.30 | 0.00 | 258444.80 | 932096.00 | 105054.13 | 183.00 | 194.00 |
| (2,5,4) | 100 (100) 100.00% | 206.89s | 3057202.80 (0.00) | 126.45 (100.04) | 206888.94 | 4791.95 | 126.45 | 100.04 | 657551.49 | 2399651.31 | 0.96 | 3057101.76 | 657449.49 | 0.00 | 874992.64 | 6990528.00 | 310137.28 | 195.00 | 206.00 |
| (2,6,4) | 100 (97) 97.00% | 283.17s | 3883492.16 (0.00) | 143.87 (117.64) | 283174.82 | 4753.69 | 143.87 | 117.64 | 794850.54 | 3088641.63 | 0.93 | 3883373.53 | 794730.97 | 0.00 | 1154472.25 | 6990528.00 | 469754.15 | 207.00 | 218.00 |
ConTest
- 100 independent trials
- The ratio of the error discovery trials over the total number of trials is the
path error density.
| TwoStage Params | Path Error Density |
|---|---|
| 2,4,4 | 0.011 (1000 trials) |
| 2,8,4 | 0.11 |
| 2,8,5 | 0.01 |
| 2,8,6 | 0.000 |
| 2,8,7 | 0.000 |
CalFuzzer
Not Applicable. The initial dynamic analysis does not finish within a time bound of 1 hour.
