search
Table of Contents
Model Description
The model is a simulation of an Alarm Clock. A null pointer exception exists in the model.
Classes: 6
SLOC: 125
Parameters: (selector)
Summary Results Table
| alarmClock (4) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
|---|---|---|---|---|
| JPF “Randomized DFS” | 100 (100) 1.00 | 0.84s | 148.30 (0.00) | 71.02 (62.84) |
| JPF Stateless Random Walk | 10179 (849) 0.08 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (1) 1.00 | 0.33s | 352.00 (3.00) | 72.00 (NA) |
| alarmClock (9) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 0.80s | 152.12 (0.00) | 71.05 (61.97) |
| JPF Stateless Random Walk | 10123 (942) 0.09 | NA | NA (NA) | NA (NA) |
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 |
|---|---|
| 4 | 0.083 |
| 9 | 0.084 |
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 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| (4) | 100 (100) 100.00% | 0.84s | 148.30 (0.00) | 71.02 (62.84) | 841.21 | 841.21 | 71.02 | 62.84 | 110.53 | 37.77 | 0.94 | 84.46 | 45.76 | 0.00 | 14474.24 | 6990528.00 | 0.00 | 164.27 | 164.27 |
| (9) | 100 (100) 100.00% | 0.80s | 152.12 (0.00) | 71.05 (61.97) | 802.61 | 802.61 | 71.05 | 61.97 | 111.65 | 40.47 | 0.86 | 89.15 | 47.82 | 0.00 | 13974.40 | 6990528.00 | 0.00 | 164.66 | 164.66 |
