JavaPathfinder v6.0 (rev 652+) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
application: Airline/Main.java
arguments:   20 5 

====================================================== search started: 1/20/12 7:43 AM

====================================================== error #1
gov.nasa.jpf.listener.PreciseRaceDetector
race for field Airline.Bug.Num_Of_Seats_Sold
  Thread-1 at Airline.Bug.run(Bug.java:64)
"  : putstatic
  Thread-2 at Airline.Bug.run(Bug.java:64)
"  : getstatic


====================================================== snapshot #1
thread java.lang.Thread:{id:1,name:Thread-1,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:
	at Airline.Bug.run(Bug.java:65)

thread java.lang.Thread:{id:2,name:Thread-2,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:
	at Airline.Bug.run(Bug.java:64)

thread java.lang.Thread:{id:3,name:Thread-3,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:4,name:Thread-4,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:5,name:Thread-5,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:6,name:Thread-6,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:7,name:Thread-7,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:8,name:Thread-8,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:9,name:Thread-9,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:10,name:Thread-10,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:11,name:Thread-11,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:12,name:Thread-12,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:13,name:Thread-13,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:14,name:Thread-14,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:15,name:Thread-15,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:16,name:Thread-16,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:17,name:Thread-17,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:18,name:Thread-18,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread java.lang.Thread:{id:19,name:Thread-19,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:


====================================================== results
error #1: gov.nasa.jpf.listener.PreciseRaceDetector "race for field Airline.Bug.Num_Of_Seats_Sold   Thr..."

====================================================== statistics
elapsed time:       00:17:01
states:             new=524314, visited=4456450, backtracked=4980738, end=19
search:             maxDepth=40, constraints hit=0
choice generators:  thread=524313 (signal=0, lock=2, shared ref=4), data=0
heap:               new=477, released=1625, max live=430, gc-cycles=4980760
instructions:       60005981
max memory:         160MB
loaded code:        classes=81, methods=1323

====================================================== search finished: 1/20/12 7:41 AM