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: 26/02/12 15:08 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) ========potential races======== object id: 57687255 (57687255) field: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskStates org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState thread id: 2 (UC1Simulator-0) instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent(CashDeskApplicationImpl.java:83) WRITE [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent(CashDeskApplicationImpl.java:81) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent(CashDeskApplicationImpl.java:301) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent(CashDeskApplicationImpl.java:89) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent(CashDeskApplicationImpl.java:247) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onCreditCardScannedEvent(CashDeskApplicationImpl.java:239) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent(CashDeskApplicationImpl.java:301) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onCreditCardScannedEvent(CashDeskApplicationImpl.java:239) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:159) WRITE [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:158) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent(CashDeskApplicationImpl.java:307) WRITE [()] ] thread id: 3 (UC1Simulator-1) instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent(CashDeskApplicationImpl.java:83) WRITE [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent(CashDeskApplicationImpl.java:81) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent(CashDeskApplicationImpl.java:89) READ [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:159) WRITE [()] ] instruction: org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:158) READ [()] ] ============================ ======== sumary ======== 1 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent read: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent < 2 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent read: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent < 3 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent read: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent < 4 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent read: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent < 5 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent read: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent < 6 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent read: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent < 7 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent read: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent < 8 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent read: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent < 9 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent read: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent < 10 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent read: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent < 11 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent read: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onCreditCardScannedEvent < 12 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent read: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent < 13 >Potential race for field org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-1] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent read: [UC1Simulator-0] org2.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onCreditCardScannedEvent < ====================================================== results error #1: gov.nasa.jpf.listener.PreciseRaceDetector "race for field org2.objectweb.dsrg.cocome.fractal...." ====================================================== statistics elapsed time: 00:00:01 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: 73MB loaded code: classes=165, methods=1712 ====================================================== search finished: 26/02/12 15:08