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


====================================================== system under test
application: org2/objectweb/dsrg/cocome/fractal/Simulator.java
arguments:   2 

====================================================== search started: 20/03/12 13:48
StoreImpl: Objects initialized
StoreImpl: Objects initialized
Simulator: Starting UC1 simulation for 2 cash desks.
Simulator: All 2 cash desks are running.
Simulator: All 2 cash desks have been closed.
UC1Simulator: Starting simulation ...
UC1Simulator: Starting simulation ...
UC1Simulator: Starting simulation ...

====================================================== error #1
gov.nasa.jpf.listener.PreciseRaceDetector
race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl@202.currState
  UC1Simulator-0 at org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent(CashDeskApplicationImpl.java:247)
"  : getfield
  UC1Simulator-1 at org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:159)
"  : putfield


====================================================== snapshot #1
thread org2.objectweb.dsrg.cocome.fractal.UC1Simulator:{id:2,name:UC1Simulator-0,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:
	at org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent(CashDeskApplicationImpl.java:247)
	at org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskBusImpl.sendPINEnteredEvent(CashDeskBusImpl.java:69)
	at org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CardReaderControllerImpl.simulatedPINEntered(CardReaderControllerImpl.java:79)
	at org2.objectweb.dsrg.cocome.fractal.UC1Simulator.run(Simulator.java:60)

thread org2.objectweb.dsrg.cocome.fractal.UC1Simulator:{id:3,name:UC1Simulator-1,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:
	at org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:159)
	at org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskBusImpl.sendSaleFinishedEvent(CashDeskBusImpl.java:85)
	at org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashBoxControllerImpl.simulatedSaleFinished(CashBoxControllerImpl.java:57)
	at org2.objectweb.dsrg.cocome.fractal.UC1Simulator.run(Simulator.java:55)


====================================================== results
error #1: gov.nasa.jpf.listener.PreciseRaceDetector "race for field org2.objectweb.dsrg.cocome.fractal...."

====================================================== statistics
elapsed time:       00:00:04
states:             new=231, visited=0, backtracked=114, end=57
search:             maxDepth=117, constraints hit=0
choice generators:  thread=174 (signal=0, lock=3, shared ref=107), data=0
heap:               new=8700, released=6496, max live=1110, gc-cycles=231
instructions:       275703
max memory:         58MB
loaded code:        classes=165, methods=1712

====================================================== search finished: 20/03/12 13:48