JavaPathfinder v6.0 (rev 652+) - (C) RIACS/NASA Ames Research Center ====================================================== system under test application: org/objectweb/dsrg/cocome/fractal/Simulator.java arguments: 2 ====================================================== search started: 26/02/12 15:02 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 ... ========potential races======== object id: 15134258 (15134258) field: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskStates org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState thread id: 2 (UC1Simulator-0) instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onCreditCardScannedEvent(CashDeskApplicationImpl.java:262) WRITE [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:166) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent(CashDeskApplicationImpl.java:84) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent(CashDeskApplicationImpl.java:270) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent(CashDeskApplicationImpl.java:286) WRITE [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent(CashDeskApplicationImpl.java:87) WRITE [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent(CashDeskApplicationImpl.java:94) READ [()] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onCreditCardScannedEvent(CashDeskApplicationImpl.java:259) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent(CashDeskApplicationImpl.java:340) WRITE [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent(CashDeskApplicationImpl.java:331) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:170) WRITE [(461)] ] thread id: 3 (UC1Simulator-1) instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onCreditCardScannedEvent(CashDeskApplicationImpl.java:262) WRITE [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:166) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent(CashDeskApplicationImpl.java:84) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent(CashDeskApplicationImpl.java:270) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent(CashDeskApplicationImpl.java:286) WRITE [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent(CashDeskApplicationImpl.java:87) WRITE [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent(CashDeskApplicationImpl.java:94) READ [()] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onCreditCardScannedEvent(CashDeskApplicationImpl.java:259) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent(CashDeskApplicationImpl.java:340) WRITE [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent(CashDeskApplicationImpl.java:331) READ [(461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent(CashDeskApplicationImpl.java:170) WRITE [(461)] ] ============================ monitor id 461 java.lang.Object object id: 178864613 (178864613) field: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.PaymentMode org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.Sale.paymentmode thread id: 2 (UC1Simulator-0) instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.Sale.(Sale.java:15) WRITE [(367, 461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.Sale.getPaymentmode(Sale.java:24) READ [(367, 461)] ] thread id: 3 (UC1Simulator-1) instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.Sale.getPaymentmode(Sale.java:24) READ [(367, 461)] ] ============================ monitor id 367 java.util.ArrayList monitor id 461 java.lang.Object object id: 200689253 (200689253) field: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.PaymentMode org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.Sale.paymentmode thread id: 2 (UC1Simulator-0) instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.Sale.getPaymentmode(Sale.java:24) READ [(367, 461)] ] thread id: 3 (UC1Simulator-1) instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.Sale.(Sale.java:15) WRITE [(367, 461)] ] instruction: org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.Sale.getPaymentmode(Sale.java:24) READ [(367, 461)] ] ============================ monitor id 367 java.util.ArrayList monitor id 461 java.lang.Object ======== sumary ======== 1 >Potential race for field org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onCreditCardScannedEvent read: [UC1Simulator-1] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent < 2 >Potential race for field org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPINEnteredEvent read: [UC1Simulator-1] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent < 3 >Potential race for field org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleStartedEvent read: [UC1Simulator-1] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent < 4 >Potential race for field org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onPaymentModeEvent read: [UC1Simulator-1] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent < 5 >Potential race for field org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.currState write: [UC1Simulator-0] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onSaleFinishedEvent read: [UC1Simulator-1] org.objectweb.dsrg.cocome.fractal.tradingsystem.cashdeskline.cashdesk.CashDeskApplicationImpl.onProductBarcodeScannedEvent < ====================================================== results no errors detected ====================================================== statistics elapsed time: 00:00:05 states: new=2171, visited=1350, backtracked=3410, end=84 search: maxDepth=136, constraints hit=0 choice generators: thread=2088 (signal=0, lock=53, shared ref=1436), data=0 heap: new=31323, released=30859, max live=1115, gc-cycles=3521 instructions: 3101148 max memory: 159MB loaded code: classes=167, methods=1921 ====================================================== search finished: 26/02/12 15:02