[[Concurrency Tool Comparison]]

== Model Description == 

A race condition in the model. 

Classes: 6

SLOC: 103

Parameters: (gc, wc, envFirst?)

== Summary Results Table ==

{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | raxextended (2,3)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 2.42s
| 9488.65 (0.00)
| 285.73 (277.29)
|-
| JPF Stateless Random Walk
| 10127 (1288) 0.13
| align="right"| NA
| NA (NA)
| NA (NA)
|- bgcolor="white" |
| colspan=5 align="center" | raxextended (4,3)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 48.26s
| 615352.88 (0.00)
| 829.48 (802.28)
|}

==Java Pathfinder==
===Stateless Random Walk===

{| align=center | border=1 | -bgcolor=grey
! 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). 
{| 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

|-
|(2,3)
| 100 (100) 100.00%
| align="right"| 2.42s
| 9488.65 (0.00)
| 285.73 (277.29)
| align="right" | 2416.94
| align="right" | 2316.94
| align="right" | 285.73
| align="right" | 277.29
| align="right" | 1782.51
| align="right" | 7706.14
| align="right" | 0.00
| align="right" | 9210.36
| align="right" | 1504.67
| align="right" | 0.00
| align="right" | 31459.84
| align="right" | 6990528.00
| align="right" | 1305.71
| align="right" | 196.39
| align="right" | 196.39
|-
|(4,3)
| 100 (100) 100.00%
| align="right"| 48.26s
| 615352.88 (0.00)
| 829.48 (802.28)
| align="right" | 48262.50
| align="right" | 4461.25
| align="right" | 829.48
| align="right" | 802.28
| align="right" | 64984.05
| align="right" | 550368.83
| align="right" | 0.00
| align="right" | 614549.60
| align="right" | 64181.20
| align="right" | 0.00
| align="right" | 275468.16
| align="right" | 6990528.00
| align="right" | 114670.13
| align="right" | 213.99
| align="right" | 214.29
|}