starting JPF on class: gov.nasa.jpf.rtsj.examples.airplane.TestAirplane Java Pathfinder Model Checker v3.1.1 - (C) 1999,2003 RIACS/NASA Ames Research Center search started Running under JPF Simulation starts at time 0:0 [0:0] altitude 5000, runway 126720 ft., speed set at 249 mph [0:0] altitude 5000, runway 126720 ft., request to change flaps from 0 to 5 [5000:0] altitude 4931, runway 124890 ft., flaps changed from 0 to 5 [5000:0] altitude 4931, runway 123060 ft., speed set at 199 mph [35000:0] altitude 4515, runway 114270 ft., request to change flaps from 5 to 15 [45000:0] altitude 4377, runway 111340 ft., flaps changed from 5 to 15 [45000:0] altitude 4377, runway 99620 ft., speed set at 180 mph [45000:0] Pilot passivates, awaiting localizer alive event [230819:0] *** One Shot Timer thread terminates; 11708 instructions executed with cost 117070 in 1963 real milliseconds [287081:0] *** One Shot Timer thread terminates; 7681 instructions executed with cost 76800 in 1212 real milliseconds [313674:0] localizer alive event [313674:0] *** One Shot Timer thread terminates; 3100 instructions executed with cost 30990 in 560 real milliseconds [313674:0] altitude 1800, runway 28691 ft., localizer alive [337113:0] altitude 1800, runway 22503 ft., glide slope captured [337113:0] altitude 1800, runway 22503 ft., gear change requested from up to down [354113:0] altitude 1800, runway 18015 ft., gear change from up to down completed [354113:0] altitude 1800, runway 18015 ft., spoilers armed [354113:0] altitude 1800, runway 18015 ft., request to change flaps from 15 to 25 [364113:0] altitude 1800, runway 15375 ft., flaps changed from 15 to 25 [364113:0] altitude 1800, runway 15375 ft., speed set at 139 mph [394113:0] altitude 1080, runway 9225 ft., request to change flaps from 25 to 40 [409113:0] altitude 720, runway 6150 ft., flaps changed from 25 to 40 [409113:0] altitude 720, runway 6150 ft., speed set at 99 mph [409113:0] Pilot passivates, awaiting on ground event [451236:0] on ground event [451236:0] *** One Shot Timer thread terminates; 1537 instructions executed with cost 15360 in 271 real milliseconds [451236:0] altitude 0, runway 1 ft., on ground [451236:0] altitude 0, runway 1 ft., >>> spoilers deploy automatically <<< [451236:0] altitude 0, runway 1 ft., engines reversed [451236:0] altitude 0, runway 1 ft., brakes applied [451236:0] *** pilot terminates; 35349 instructions executed with cost 353480 in 5788 real milliseconds [451236:0] simulation ends state backtracked; cost now 380240; instruction count now 38024 state advanced; cost now 323410; instruction count now 32341 state backtracked; cost now 323430; instruction count now 32343 state advanced; cost now 323400; instruction count now 32340 state backtracked; cost now 323410; instruction count now 32341 state advanced; cost now 323390; instruction count now 32339 state backtracked; cost now 323400; instruction count now 32340 state advanced; cost now 323380; instruction count now 32338 state backtracked; cost now 323400; instruction count now 32340 state advanced; cost now 323360; instruction count now 32336 state backtracked; cost now 323400; instruction count now 32340 state advanced; cost now 227630; instruction count now 22763 [356435:0] altitude 1800, runway 17402 ft., gear change from up to down completed [356435:0] altitude 1800, runway 17402 ft., spoilers armed [356435:0] altitude 1800, runway 17402 ft., request to change flaps from 15 to 25 [366435:0] altitude 1800, runway 14762 ft., flaps changed from 15 to 25 [366435:0] altitude 1800, runway 14762 ft., speed set at 139 mph [396435:0] altitude 1051, runway 8612 ft., request to change flaps from 25 to 40 [411435:0] altitude 676, runway 5537 ft., flaps changed from 25 to 40 [411435:0] altitude 676, runway 5537 ft., speed set at 99 mph [411435:0] Pilot passivates, awaiting on ground event [449359:0] on ground event [449359:0] *** One Shot Timer thread terminates; 1537 instructions executed with cost 15360 in 210 real milliseconds [449359:0] altitude 0, runway 1 ft., on ground [449359:0] altitude 0, runway 1 ft., >>> spoilers deploy automatically <<< [449359:0] altitude 0, runway 1 ft., engines reversed [449359:0] altitude 0, runway 1 ft., brakes applied [449359:0] *** pilot terminates; 35351 instructions executed with cost 353500 in 8062 real milliseconds [449359:0] simulation ends state backtracked; cost now 380260; instruction count now 38026 state advanced; cost now 323430; instruction count now 32343 state backtracked; cost now 323450; instruction count now 32345 state advanced; cost now 323420; instruction count now 32342 state backtracked; cost now 323430; instruction count now 32343 state advanced; cost now 323410; instruction count now 32341 state backtracked; cost now 323420; instruction count now 32342 state advanced; cost now 323400; instruction count now 32340 state backtracked; cost now 323420; instruction count now 32342 state advanced; cost now 323380; instruction count now 32338 state backtracked; cost now 323420; instruction count now 32342 state advanced; cost now 227650; instruction count now 22765 [376113:0] altitude 1800, runway 12207 ft., gear change from up to down completed [376113:0] altitude 1800, runway 12207 ft., doors not retracted -- arm spoilers manually! [376113:0] altitude 1800, runway 12207 ft., request to change flaps from 15 to 25 [386113:0] altitude 1800, runway 9567 ft., flaps changed from 15 to 25 [386113:0] altitude 1800, runway 9567 ft., speed set at 139 mph [416113:0] altitude 643, runway 3417 ft., request to change flaps from 25 to 40 [431113:0] altitude 65, runway 342 ft., flaps changed from 25 to 40 [431113:0] altitude 65, runway 342 ft., speed set at 99 mph [431113:0] Pilot passivates, awaiting on ground event [433455:0] on ground event [433455:0] *** One Shot Timer thread terminates; 1537 instructions executed with cost 15360 in 211 real milliseconds [433455:0] altitude 0, runway 1 ft., on ground [433455:0] altitude 0, runway 1 ft., >>> deploy spoilers manually! <<< [433455:0] altitude 0, runway 1 ft., engines reversed [433455:0] altitude 0, runway 1 ft., brakes applied [433455:0] *** pilot terminates; 35353 instructions executed with cost 353520 in 10585 real milliseconds [433455:0] simulation ends state backtracked; cost now 380280; instruction count now 38028 state advanced; cost now 323460; instruction count now 32346 state backtracked; cost now 323480; instruction count now 32348 state advanced; cost now 323450; instruction count now 32345 state backtracked; cost now 323460; instruction count now 32346 state advanced; cost now 323440; instruction count now 32344 state backtracked; cost now 323450; instruction count now 32345 state advanced; cost now 323430; instruction count now 32343 state backtracked; cost now 323450; instruction count now 32345 state advanced; cost now 323410; instruction count now 32341 state backtracked; cost now 323450; instruction count now 32345 state advanced; cost now 156730; instruction count now 15673 state backtracked; cost now 156750; instruction count now 15675 state advanced; cost now 156720; instruction count now 15672 state backtracked; cost now 156730; instruction count now 15673 state advanced; cost now 156710; instruction count now 15671 state backtracked; cost now 156720; instruction count now 15672 state advanced; cost now 156700; instruction count now 15670 state backtracked; cost now 156720; instruction count now 15672 state advanced; cost now 156680; instruction count now 15668 state backtracked; cost now 156720; instruction count now 15672 state advanced; cost now 91720; instruction count now 9172 state backtracked; cost now 91740; instruction count now 9174 state advanced; cost now 91710; instruction count now 9171 state backtracked; cost now 91720; instruction count now 9172 state advanced; cost now 91700; instruction count now 9170 state backtracked; cost now 91710; instruction count now 9171 state advanced; cost now 91690; instruction count now 9169 state backtracked; cost now 91710; instruction count now 9171 state advanced; cost now 91670; instruction count now 9167 state backtracked; cost now 91710; instruction count now 9171 state advanced; cost now 36740; instruction count now 3674 state backtracked; cost now 36760; instruction count now 3676 state advanced; cost now 36730; instruction count now 3673 state backtracked; cost now 36740; instruction count now 3674 state advanced; cost now 36720; instruction count now 3672 state backtracked; cost now 36730; instruction count now 3673 state advanced; cost now 36710; instruction count now 3671 state backtracked; cost now 36730; instruction count now 3673 state advanced; cost now 36690; instruction count now 3669 state backtracked; cost now 36730; instruction count now 3673 state advanced; cost now 11110; instruction count now 1111 state backtracked; cost now 11130; instruction count now 1113 state advanced; cost now 11100; instruction count now 1110 state backtracked; cost now 11110; instruction count now 1111 state advanced; cost now 11090; instruction count now 1109 state backtracked; cost now 11100; instruction count now 1110 state advanced; cost now 11080; instruction count now 1108 state backtracked; cost now 11100; instruction count now 1110 state advanced; cost now 11060; instruction count now 1106 state backtracked; cost now 11100; instruction count now 1110 search finished =================================== No Errors Found =================================== +++ Execution ends after 12919 true 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 14324 GCs begun; 14324 ended 72 classes loaded 16117 states processed 16154 backtracks ----------------------------------- States visited : 16,120 Transitions executed : 16,155 Instructions executed: 68,729 Maximum stack depth : 9,046 Intermediate steps : 67 Memory used : 81.27MB Memory used after gc : 5.62MB Storage memory : 0.0B Collected objects : 2,615 Mark and sweep runs : 14,324 Execution time : 12.919s Speed : 1,250tr/s ----------------------------------- ACONST_NULL 261 ICONST_0 2091 LCONST_0 265 BIPUSH 462 SIPUSH 133 LDC 442 LDC_W 128 LDC2_W 47 ILOAD 289 LLOAD 298 FLOAD 15 DLOAD 2 ALOAD 132 ILOAD_0 39 ILOAD_1 993 ILOAD_2 98 ILOAD_3 270 LLOAD_0 68 LLOAD_1 620 LLOAD_2 2 LLOAD_3 918 ALOAD_0 12858 ALOAD_1 3865 ALOAD_2 1225 ALOAD_3 648 DALOAD 3 AALOAD 73 ISTORE 474 LSTORE 534 FSTORE 15 ASTORE 149 ASTORE_0 11 ASTORE_1 89 ASTORE_2 662 ASTORE_3 199 IASTORE 32 DASTORE 3 AASTORE 43 POP 358 DUP 1876 DUP_X1 13 IADD 429 LADD 58 DADD 2 LSUB 146 LSUB 136 DSUB 1 IMUL 92 LMUL 2 FMUL 15 DMUL 3 IDIV 81 LDIV 2 FDIV 15 ISHL 8 LSHR 81 IUSHR 8 IAND 4 LAND 1 IXOR 12 LXOR 1 IINC 152 I2L 27 I2F 15 L2I 68 L2F 30 F2I 15 D2I 3 LCMP 372 IFEQ 150 IFNE 631 IFLT 104 IFGE 271 IFGT 130 IFLE 221 IF_ICMPEQ 13 IF_ICMPNE 40 IF_ICMPLT 125 IF_ICMPGE 81 IF_ICMPGT 46 IF_ICMPLE 116 IF_ACMPNE 38 GOTO 788 IRETURN 1102 LRETURN 1258 DRETURN 4 ARETURN 1872 RETURN 4566 GETSTATIC 1343 PUTSTATIC 48 GETFIELD 5646 PUTFIELD 4320 INVOKEVIRTUAL 5508 INVOKESPECIAL 3805 INVOKESTATIC 721 INVOKEINTERFACE 245 NEW 1204 NEWARRAY 283 ANEWARRAY 22 ARRAYLENGTH 15 CHECKCAST 97 INSTANCEOF 1 MONITORENTER 367 MONITOREXIT 364 IFNULL 128 IFNONNULL 574