starting JPF on class: gov.nasa.jpf.rtsj.examples.bridge.OneWayBridge Java Pathfinder Model Checker v3.1.1 - (C) 1999,2003 RIACS/NASA Ames Research Center search started Running under JPF [0:0] Starting one way bridge example with randomize == false [0:0] Car arrivals (priority 1) started [0:0] Bridge Reporter (priority 0) started [0:0] Periodic Timer thread (priority 0) started Simulation starts at time 0:0 [0:0] Car 0 (priority 1) started [0:0] Car arrivals (priority 1) starts hold for 11:0 [0:0] bridge is empty [0:0] Bridge Reporter (priority 0) starts hold for 10:0 [0:0] Periodic Timer thread (priority 0) starts hold for 5:0 [0:0] Car 0 (priority 1) starts hold for 1:0 [1:0] Car 0 (priority 1) completes hold for 1:0 [1:0] Car 0 (priority 1) starts seize of Bridge [1:0] Car 0 (priority 1) gets Bridge [1:0] Car 0 (priority 1) starts hold for 10:0 [5:0] Periodic Timer thread (priority 0) completes hold for 5:0 [5:0] Periodic Timer fires [5:0] Periodic Timer thread (priority 0) starts hold for 5:0 [10:0] Bridge Reporter (priority 0) completes hold for 10:0 [10:0] Car 0 holds bridge [10:0] Bridge Reporter (priority 0) starts hold for 10:0 [10:0] Periodic Timer thread (priority 0) completes hold for 5:0 [10:0] Periodic Timer fires [10:0] Periodic Timer thread (priority 0) starts hold for 5:0 [11:0] Car arrivals (priority 1) completes hold for 11:0 [11:0] Car 1 (priority 2) started [11:0] Car arrivals (priority 1) starts hold for 10:0 [11:0] Car 0 (priority 1) completes hold for 10:0 [11:0] Car 0 (priority 1) releases Bridge [11:0] no one waiting for Bridge [11:0] *** Car 0 terminates; 17283 instructions executed with cost 172830 in 1893 real milliseconds [11:0] Car 1 (priority 2) starts hold for 2:0 [13:0] Car 1 (priority 2) completes hold for 2:0 [13:0] Car 1 (priority 2) starts seize of Bridge [13:0] Car 1 (priority 2) gets Bridge [13:0] Car 1 (priority 2) starts hold for 10:0 [15:0] Periodic Timer thread (priority 0) completes hold for 5:0 [15:0] Periodic Timer fires [15:0] Periodic Timer thread (priority 0) starts hold for 5:0 [20:0] Bridge Reporter (priority 0) completes hold for 10:0 [20:0] Car 1 holds bridge [20:0] Bridge Reporter (priority 0) starts hold for 10:0 [20:0] Periodic Timer thread (priority 0) completes hold for 5:0 [20:0] Periodic Timer fires [20:0] Periodic Timer thread (priority 0) starts hold for 5:0 [21:0] Car arrivals (priority 1) completes hold for 10:0 [21:0] Car 2 (priority 3) started [21:0] Car arrivals (priority 1) starts hold for 9:0 [21:0] Car 2 (priority 3) starts hold for 3:0 [23:0] Car 1 (priority 2) completes hold for 10:0 [23:0] Car 1 (priority 2) releases Bridge [23:0] no one waiting for Bridge [23:0] *** Car 1 terminates; 18802 instructions executed with cost 188020 in 2754 real milliseconds [24:0] Car 2 (priority 3) completes hold for 3:0 [24:0] Car 2 (priority 3) starts seize of Bridge [24:0] Car 2 (priority 3) gets Bridge [24:0] Car 2 (priority 3) starts hold for 10:0 [25:0] Periodic Timer thread (priority 0) completes hold for 5:0 [25:0] Periodic Timer fires [25:0] *** Periodic Timer thread terminates; 43049 instructions executed with cost 430490 in 5478 real milliseconds [30:0] Bridge Reporter (priority 0) completes hold for 10:0 [30:0] Car 2 holds bridge [30:0] Bridge Reporter (priority 0) starts hold for 10:0 [30:0] Car arrivals (priority 1) completes hold for 9:0 [30:0] Car 3 (priority 4) started [30:0] Car arrivals (priority 1) starts hold for 8:0 [30:0] Car 3 (priority 4) starts hold for 4:0 [34:0] Car 2 (priority 3) completes hold for 10:0 [34:0] Car 2 (priority 3) releases Bridge [34:0] no one waiting for Bridge [34:0] *** Car 2 terminates; 17174 instructions executed with cost 171740 in 2494 real milliseconds [34:0] Car 3 (priority 4) completes hold for 4:0 [34:0] Car 3 (priority 4) starts seize of Bridge [34:0] Car 3 (priority 4) gets Bridge [34:0] Car 3 (priority 4) starts hold for 10:0 [38:0] Car arrivals (priority 1) completes hold for 8:0 [38:0] Car 4 (priority 5) started [38:0] Car arrivals (priority 1) starts hold for 7:0 [38:0] Car 4 (priority 5) starts hold for 5:0 [40:0] Bridge Reporter (priority 0) completes hold for 10:0 [40:0] Car 3 holds bridge [40:0] Bridge Reporter (priority 0) starts hold for 10:0 [43:0] Car 4 (priority 5) completes hold for 5:0 [43:0] Car 4 (priority 5) starts seize of Bridge [43:0] >>> Car 3 (priority 4) priority raised to 5 [44:0] Car 3 (priority 5) completes hold for 10:0 [44:0] Car 3 (priority 5) releases Bridge [44:0] <<< Car 3 (priority 5) has priority reduced to 4 [44:0] Bridge given to Car 4 (priority 5) [44:0] *** Car 3 terminates; 18395 instructions executed with cost 183950 in 2384 real milliseconds [44:0] Car 4 (priority 5) starts hold for 10:0 [45:0] Car arrivals (priority 1) completes hold for 7:0 [45:0] *** Car arrivals terminates; 75476 instructions executed with cost 754760 in 9874 real milliseconds [50:0] Bridge Reporter (priority 0) completes hold for 10:0 [50:0] Car 4 holds bridge [50:0] Bridge Reporter (priority 0) starts hold for 10:0 [54:0] Car 4 (priority 5) completes hold for 10:0 [54:0] Car 4 (priority 5) releases Bridge [54:0] no one waiting for Bridge [54:0] *** Car 4 terminates; 15176 instructions executed with cost 151760 in 1973 real milliseconds [60:0] Bridge Reporter (priority 0) completes hold for 10:0 [60:0] *** Bridge Reporter terminates; 77727 instructions executed with cost 777270 in 10014 real milliseconds Bridge Reporter with cost 10000:0 has run time 10014:0 [60:0] Bridge Reporter overrun handler fires [60:0] simulation ends state backtracked; cost now 889760; instruction count now 88976 state advanced; cost now 687870; instruction count now 68787 state backtracked; cost now 687890; instruction count now 68789 state advanced; cost now 687860; instruction count now 68786 state backtracked; cost now 687870; instruction count now 68787 state advanced; cost now 687850; instruction count now 68785 state backtracked; cost now 687860; instruction count now 68786 state advanced; cost now 687840; instruction count now 68784 state backtracked; cost now 687860; instruction count now 68786 state advanced; cost now 687820; instruction count now 68782 state backtracked; cost now 687860; instruction count now 68786 state advanced; cost now 587390; instruction count now 58739 state backtracked; cost now 587410; instruction count now 58741 state advanced; cost now 587380; instruction count now 58738 state backtracked; cost now 587390; instruction count now 58739 state advanced; cost now 587370; instruction count now 58737 state backtracked; cost now 587380; instruction count now 58738 state advanced; cost now 587360; instruction count now 58736 state backtracked; cost now 587380; instruction count now 58738 state advanced; cost now 587340; instruction count now 58734 state backtracked; cost now 587380; instruction count now 58738 state advanced; cost now 443490; instruction count now 44349 state backtracked; cost now 443510; instruction count now 44351 state advanced; cost now 443480; instruction count now 44348 state backtracked; cost now 443490; instruction count now 44349 state advanced; cost now 443470; instruction count now 44347 state backtracked; cost now 443480; instruction count now 44348 state advanced; cost now 443460; instruction count now 44346 state backtracked; cost now 443480; instruction count now 44348 state advanced; cost now 443440; instruction count now 44344 state backtracked; cost now 443480; instruction count now 44348 state advanced; cost now 264060; instruction count now 26406 state backtracked; cost now 264080; instruction count now 26408 state advanced; cost now 264050; instruction count now 26405 state backtracked; cost now 264060; instruction count now 26406 state advanced; cost now 264040; instruction count now 26404 state backtracked; cost now 264050; instruction count now 26405 state advanced; cost now 264030; instruction count now 26403 state backtracked; cost now 264050; instruction count now 26405 state advanced; cost now 264010; instruction count now 26401 state backtracked; cost now 264050; instruction count now 26405 state advanced; cost now 73360; instruction count now 7336 state backtracked; cost now 73380; instruction count now 7338 state advanced; cost now 73350; instruction count now 7335 state backtracked; cost now 73360; instruction count now 7336 state advanced; cost now 73340; instruction count now 7334 state backtracked; cost now 73350; instruction count now 7335 state advanced; cost now 73330; instruction count now 7333 state backtracked; cost now 73350; instruction count now 7335 state advanced; cost now 73310; instruction count now 7331 state backtracked; cost now 73350; instruction count now 7335 state advanced; cost now 53650; instruction count now 5365 state backtracked; cost now 53670; instruction count now 5367 state advanced; cost now 53640; instruction count now 5364 state backtracked; cost now 53650; instruction count now 5365 state advanced; cost now 53630; instruction count now 5363 state backtracked; cost now 53640; instruction count now 5364 state advanced; cost now 53620; instruction count now 5362 state backtracked; cost now 53640; instruction count now 5364 state advanced; cost now 53600; instruction count now 5360 state backtracked; cost now 53640; instruction count now 5364 state advanced; cost now 30950; instruction count now 3095 state backtracked; cost now 30970; instruction count now 3097 state advanced; cost now 30940; instruction count now 3094 state backtracked; cost now 30950; instruction count now 3095 state advanced; cost now 30930; instruction count now 3093 state backtracked; cost now 30940; instruction count now 3094 state advanced; cost now 30920; instruction count now 3092 state backtracked; cost now 30940; instruction count now 3094 state advanced; cost now 30900; instruction count now 3090 state backtracked; cost now 30940; instruction count now 3094 state advanced; cost now 13870; instruction count now 1387 state backtracked; cost now 13890; instruction count now 1389 state advanced; cost now 13860; instruction count now 1386 state backtracked; cost now 13870; instruction count now 1387 state advanced; cost now 13850; instruction count now 1385 state backtracked; cost now 13860; instruction count now 1386 state advanced; cost now 13840; instruction count now 1384 state backtracked; cost now 13860; instruction count now 1386 state advanced; cost now 13820; instruction count now 1382 state backtracked; cost now 13860; instruction count now 1386 search finished =================================== No Errors Found =================================== +++ Execution ends after 13940 milliseconds +++ *** Final path statistics *** 83 instructions executed with total cost 830 66 objects created; 0 released 66 objects in existence 2 threads started; 1 terminated 12608 GCs begun; 12608 ended 73 classes loaded 14292 states processed 14332 backtracks ----------------------------------- States visited : 14,293 Transitions executed : 14,333 Instructions executed: 89,176 Maximum stack depth : 14,245 Intermediate steps : 70 Memory used : 150.09MB Memory used after gc : 15.9MB Storage memory : 0.0B Collected objects : 3,680 Mark and sweep runs : 12,608 Execution time : 13.930s Speed : 1,028tr/s ----------------------------------- ACONST_NULL 266 ICONST_0 3251 LCONST_0 180 BIPUSH 773 SIPUSH 11 LDC 548 LDC_W 194 LDC2_W 41 ILOAD 560 LLOAD 164 ALOAD 204 ILOAD_0 51 ILOAD_1 2635 ILOAD_2 359 ILOAD_3 685 LLOAD_0 159 LLOAD_1 329 LLOAD_3 667 ALOAD_0 16168 ALOAD_1 5190 ALOAD_2 1871 ALOAD_3 490 AALOAD 119 CALOAD 23 ISTORE 740 LSTORE 295 ASTORE 173 ASTORE_0 9 ASTORE_1 155 ASTORE_2 1350 ASTORE_3 218 IASTORE 32 AASTORE 53 POP 476 DUP 2265 DUP_X1 23 IADD 585 LADD 52 LSUB 76 LSUB 9 IMUL 24 ISHL 28 LSHR 257 IUSHR 28 IAND 14 LAND 1 IXOR 42 LXOR 1 IINC 624 I2L 11 L2I 1 LCMP 431 IFEQ 136 IFNE 680 IFLT 350 IFGE 331 IFGT 98 IFLE 358 IF_ICMPEQ 19 IF_ICMPNE 50 IF_ICMPLT 601 IF_ICMPGE 281 IF_ICMPGT 297 IF_ICMPLE 284 IF_ACMPEQ 11 IF_ACMPNE 151 GOTO 1257 IRETURN 1811 LRETURN 766 ARETURN 3216 RETURN 4937 GETSTATIC 1189 PUTSTATIC 45 GETFIELD 7391 PUTFIELD 4978 INVOKEVIRTUAL 6890 INVOKESPECIAL 4235 INVOKESTATIC 1118 INVOKEINTERFACE 678 NEW 1376 NEWARRAY 458 ANEWARRAY 16 ARRAYLENGTH 34 CHECKCAST 274 INSTANCEOF 1 MONITORENTER 551 MONITOREXIT 543 IFNULL 104 IFNONNULL 750