[[Concurrency Tool Comparison]]

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

{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,16,8)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 9995 (6) 0.00
| align="right"| 1.31s
| 325.50 (0.00)
| 324.50 (324.50)
|-
| JPF Stateless Random Walk
| 10125 (6) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,2,2)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 150 (150) 1.00
| align="right"| 1.58s
| 2276.49 (0.00)
| 53.93 (40.53)
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,4,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 150 (150) 1.00
| align="right"| 54.71s
| 838403.57 (0.00)
| 108.29 (81.40)
|-
| JPF Stateless Random Walk
| 10116 (289) 0.03
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 18.83s
| 628824.00 (3743.00)
| 168.00 (NA)
|-
| ConTest
| 1000 (11) 0.01
| align="right"| NA
| NA (NA)
| NA (NA)
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,5,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 206.89s
| 3057202.80 (0.00)
| 126.45 (100.04)
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,6,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (97) 0.97
| align="right"| 283.17s
| 3883492.16 (0.00)
| 143.87 (117.64)
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,7,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (96) 0.96
| align="right"| 334.26s
| 4566700.58 (0.00)
| 160.06 (133.93)
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,8,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 5000 (4770) 0.95
| align="right"| 301.58s
| 3755044.80 (0.00)
| 179.06 (151.94)
|-
| JPF Stateless Random Walk
| 10124 (850) 0.08
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 42.65s
| 1531872.00 (5319.00)
| 288.00 (NA)
|-
| ConTest
| 100 (11) 0.11
| align="right"| NA
| NA (NA)
| NA (NA)
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,8,5)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 5025 (2866) 0.57
| align="right"| 1179.77s
| 14552031.67 (0.00)
| 184.68 (150.43)
|-
| JPF Stateless Random Walk
| 10124 (301) 0.03
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 12.86s
| 459936.00 (1597.00)
| 288.00 (NA)
|-
| ConTest
| 100 (1) 0.01
| align="right"| NA
| NA (NA)
| NA (NA)
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,8,6)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 4987 (429) 0.09
| align="right"| 1329.92s
| 16186995.16 (0.00)
| 180.35 (146.60)
|-
| JPF Stateless Random Walk
| 10123 (83) 0.01
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 12.86s
| 459936.00 (1597.00)
| 288.00 (NA)
|-
| ConTest
| 100 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|- bgcolor="white" |
| colspan=5 align="center" | piper (2,8,7)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 5186 (91) 0.02
| align="right"| 1487.44s
| 18341935.22 (0.00)
| 176.79 (143.89)
|-
| JPF Stateless Random Walk
| 10130 (17) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 12.86s
| 459936.00 (1597.00)
| 288.00 (NA)
|-
| ConTest
| 100 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|}
==Chess==

* ChessBound=2
* ChessMonitorVolatiles=false 

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

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

{| 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,7,4)
| 100 (96) 96.00%
| align="right"| 334.26s
| 4566700.58 (0.00)
| 160.06 (133.93)
| align="right" | 334260.55
| align="right" | 4928.19
| align="right" | 160.06
| align="right" | 133.93
| align="right" | 871245.98
| align="right" | 3695454.60
| align="right" | 0.89
| align="right" | 4566565.66
| align="right" | 871110.17
| align="right" | 0.00
| align="right" | 1105157.33
| align="right" | 6990528.00
| align="right" | 420132.95
| align="right" | 219.00
| align="right" | 230.00
|-
|(2,16,8)
| 9995 (6) 0.06%
| align="right"| 1.31s
| 325.50 (0.00)
| 324.50 (324.50)
| align="right" | 1306.17
| align="right" | 1306.17
| align="right" | 324.50
| align="right" | 324.50
| align="right" | 325.50
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 15488.00
| align="right" | 932096.00
| align="right" | 0.00
| align="right" | 327.00
| align="right" | 338.00
|-
|(2,8,4)
| 5000 (4770) 95.40%
| align="right"| 301.58s
| 3755044.80 (0.00)
| 179.06 (151.94)
| align="right" | 301575.26
| align="right" | 4681.66
| align="right" | 179.06
| align="right" | 151.94
| align="right" | 742889.64
| align="right" | 3012155.16
| align="right" | 0.92
| align="right" | 3754891.86
| align="right" | 742735.78
| align="right" | 0.00
| align="right" | 334799.17
| align="right" | 932096.00
| align="right" | 158633.07
| align="right" | 231.00
| align="right" | 242.00
|-
|(2,8,5)
| 5025 (2866) 57.03%
| align="right"| 1179.77s
| 14552031.67 (0.00)
| 184.68 (150.43)
| align="right" | 1179766.68
| align="right" | 4888.26
| align="right" | 184.68
| align="right" | 150.43
| align="right" | 3061014.77
| align="right" | 11491016.91
| align="right" | 0.96
| align="right" | 14551880.24
| align="right" | 3060862.38
| align="right" | 0.00
| align="right" | 413719.60
| align="right" | 932096.00
| align="right" | 185184.04
| align="right" | 231.00
| align="right" | 242.00
|-
|(2,8,6)
| 4987 (429) 8.60%
| align="right"| 1329.92s
| 16186995.16 (0.00)
| 180.35 (146.60)
| align="right" | 1329924.23
| align="right" | 4499.45
| align="right" | 180.35
| align="right" | 146.60
| align="right" | 3208115.95
| align="right" | 12978879.21
| align="right" | 0.92
| align="right" | 16186847.55
| align="right" | 3207967.42
| align="right" | 0.00
| align="right" | 403275.04
| align="right" | 932096.00
| align="right" | 183196.31
| align="right" | 231.00
| align="right" | 242.00
|-
|(2,8,7)
| 5186 (91) 1.75%
| align="right"| 1487.44s
| 18341935.22 (0.00)
| 176.79 (143.89)
| align="right" | 1487437.86
| align="right" | 3733.93
| align="right" | 176.79
| align="right" | 143.89
| align="right" | 3564384.73
| align="right" | 14777550.49
| align="right" | 0.85
| align="right" | 18341790.33
| align="right" | 3564238.99
| align="right" | 0.00
| align="right" | 384064.00
| align="right" | 932096.00
| align="right" | 161049.68
| align="right" | 231.00
| align="right" | 242.00
|-
|(2,2,2)
| 150 (150) 100.00%
| align="right"| 1.58s
| 2276.49 (0.00)
| 53.93 (40.53)
| align="right" | 1583.92
| align="right" | 1583.92
| align="right" | 53.93
| align="right" | 40.53
| align="right" | 995.87
| align="right" | 1280.63
| align="right" | 0.87
| align="right" | 2234.96
| align="right" | 953.46
| align="right" | 0.00
| align="right" | 18155.52
| align="right" | 932096.00
| align="right" | 0.00
| align="right" | 159.00
| align="right" | 170.00
|-
|(2,4,4)
| 150 (150) 100.00%
| align="right"| 54.71s
| 838403.57 (0.00)
| 108.29 (81.40)
| align="right" | 54711.95
| align="right" | 4838.51
| align="right" | 108.29
| align="right" | 81.40
| align="right" | 214919.68
| align="right" | 623483.89
| align="right" | 0.98
| align="right" | 838321.17
| align="right" | 214836.30
| align="right" | 0.00
| align="right" | 258444.80
| align="right" | 932096.00
| align="right" | 105054.13
| align="right" | 183.00
| align="right" | 194.00
|-
|(2,5,4)
| 100 (100) 100.00%
| align="right"| 206.89s
| 3057202.80 (0.00)
| 126.45 (100.04)
| align="right" | 206888.94
| align="right" | 4791.95
| align="right" | 126.45
| align="right" | 100.04
| align="right" | 657551.49
| align="right" | 2399651.31
| align="right" | 0.96
| align="right" | 3057101.76
| align="right" | 657449.49
| align="right" | 0.00
| align="right" | 874992.64
| align="right" | 6990528.00
| align="right" | 310137.28
| align="right" | 195.00
| align="right" | 206.00
|-
|(2,6,4)
| 100 (97) 97.00%
| align="right"| 283.17s
| 3883492.16 (0.00)
| 143.87 (117.64)
| align="right" | 283174.82
| align="right" | 4753.69
| align="right" | 143.87
| align="right" | 117.64
| align="right" | 794850.54
| align="right" | 3088641.63
| align="right" | 0.93
| align="right" | 3883373.53
| align="right" | 794730.97
| align="right" | 0.00
| align="right" | 1154472.25
| align="right" | 6990528.00
| align="right" | 469754.15
| align="right" | 207.00
| align="right" | 218.00
|}


==ConTest==

* 100 independent trials

* The ratio of the error discovery trials over the total number of trials is the 
path error density. 

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