[[Concurrency Tool Comparison|Back]]

== 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 ==

{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | alarmClock (4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 0.84s
| 148.30 (0.00)
| 71.02 (62.84)
|-
| JPF Stateless Random Walk
| 10179 (849) 0.08
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 0.33s
| 352.00 (3.00)
| 72.00 (NA)
|- bgcolor="white" |
| colspan=5 align="center" | alarmClock (9)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 0.80s
| 152.12 (0.00)
| 71.05 (61.97)
|-
| JPF Stateless Random Walk
| 10123 (942) 0.09
| align="right"| 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. 

{| align=center | border=1 | -bgcolor=grey
! 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). 
{| align="center" | border=1 
|- bgcolor="lightblue"
! 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%
| align="right"| 0.84s
| 148.30 (0.00)
| 71.02 (62.84)
| align="right" | 841.21
| align="right" | 841.21
| align="right" | 71.02
| align="right" | 62.84
| align="right" | 110.53
| align="right" | 37.77
| align="right" | 0.94
| align="right" | 84.46
| align="right" | 45.76
| align="right" | 0.00
| align="right" | 14474.24
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 164.27
| align="right" | 164.27
|-
|(9)
| 100 (100) 100.00%
| align="right"| 0.80s
| 152.12 (0.00)
| 71.05 (61.97)
| align="right" | 802.61
| align="right" | 802.61
| align="right" | 71.05
| align="right" | 61.97
| align="right" | 111.65
| align="right" | 40.47
| align="right" | 0.86
| align="right" | 89.15
| align="right" | 47.82
| align="right" | 0.00
| align="right" | 13974.40
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 164.66
| align="right" | 164.66
|}