[[Concurrency Tool Comparison]]

== Model Description ==

A simple scheduler that contains an assertion violation. 

Classes: 24

SLOC: 838

Parameters: (abs?) 

== Summary Results Table ==

{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | deosA ()
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 2.87s
| 1184.21 (0.00)
| 39.98 (27.78)
|-
| JPF Stateless Random Walk
| 10129 (1925) 0.19
| align="right"| 1.95s
| 9.03 (NA)
| 0.00 (NA)
|}

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

{| align=center | border=1 | -bgcolor=grey
! Parameters !! Path Error Density
|- 
| a || 0.190
|}

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

|-
|(a)
| 100 (100) 100.00%
| align="right"| 2.87s
| 1184.21 (0.00)
| 39.98 (27.78)
| align="right" | 2874.56
| align="right" | 2874.56
| align="right" | 39.98
| align="right" | 27.78
| align="right" | 747.11
| align="right" | 437.10
| align="right" | 0.55
| align="right" | 1155.43
| align="right" | 718.78
| align="right" | 0.00
| align="right" | 38716.16
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 295.17
| align="right" | 295.25
|}