Executing command: java -jar /Users/vchar/eclipsejava/jpf-core/build/RunJPF.jar +shell.port=4242 /Users/vchar/eclipsejava/JPF/src/examples/TTTConsoleNonOO2P.jpf Running Symbolic PathFinder ... symbolic.dp=choco symbolic.string_dp_timeout_ms=0 symbolic.string_dp=none symbolic.choco_time_bound=30000 symbolic.max_pc_length=2147483647 symbolic.max_pc_msec=0 symbolic.bvlength=32 symbolic.min_int=-2147483648 symbolic.min_long=-9223372036854775808 symbolic.min_short=-32768 symbolic.min_byte=-128 symbolic.min_char=0 symbolic.max_int=2147483647 symbolic.max_long=9223372036854775807 symbolic.max_short=32767 symbolic.max_byte=127 symbolic.max_char=65535 symbolic.min_double=4.9E-324 symbolic.max_double=1.7976931348623157E308 JavaPathfinder core system v8.0 (rev ${version}) - (C) 2005-2014 United States Government. All rights reserved. ====================================================== system under test TTTConsoleNonOO2P.main() ====================================================== search started: 7/10/17 2:23 AM New sym int row min=-2147483648, max=2147483647 New sym int col min=-2147483648, max=2147483647 Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 1 row >= 0 -> true ### PCs: total:1 sat:1 unsat:0 string analysis: SPC # = 0 NPC constraint # = 1 row >= 0 numeric PC: constraint # = 2 row < 3 && row >= 0 -> true ### PCs: total:2 sat:2 unsat:0 string analysis: SPC # = 0 NPC constraint # = 2 row < 3 && row >= 0 numeric PC: constraint # = 3 col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:3 sat:3 unsat:0 string analysis: SPC # = 0 NPC constraint # = 3 col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 4 col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:4 sat:4 unsat:0 string analysis: SPC # = 0 NPC constraint # = 4 col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 5 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:5 sat:5 unsat:0 string analysis: SPC # = 0 NPC constraint # = 5 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:6 sat:6 unsat:0 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:7 sat:7 unsat:0 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:8 sat:8 unsat:0 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:9 sat:9 unsat:0 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:10 sat:10 unsat:0 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:132) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 1 = col && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:11 sat:10 unsat:1 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:130) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 2 = col && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:12 sat:10 unsat:2 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:130) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 col < 0 && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:13 sat:10 unsat:3 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:130) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 col >= 3 && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:14 sat:10 unsat:4 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:130) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 1 = col && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:15 sat:10 unsat:5 numeric PC: constraint # = 7 2 = col && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:16 sat:10 unsat:6 numeric PC: constraint # = 7 col < 0 && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:17 sat:10 unsat:7 numeric PC: constraint # = 7 col >= 3 && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:18 sat:10 unsat:8 numeric PC: constraint # = 7 1 = row && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:19 sat:10 unsat:9 numeric PC: constraint # = 7 2 = row && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:20 sat:10 unsat:10 numeric PC: constraint # = 7 row < 0 && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:21 sat:10 unsat:11 numeric PC: constraint # = 7 row >= 3 && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:22 sat:10 unsat:12 numeric PC: constraint # = 7 1 = row && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:23 sat:10 unsat:13 numeric PC: constraint # = 7 2 = row && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:24 sat:10 unsat:14 numeric PC: constraint # = 7 row < 0 && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:25 sat:10 unsat:15 numeric PC: constraint # = 7 row >= 3 && 0 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:26 sat:10 unsat:16 numeric PC: constraint # = 6 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:27 sat:11 unsat:16 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:28 sat:12 unsat:16 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = col && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:29 sat:12 unsat:17 numeric PC: constraint # = 6 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:30 sat:13 unsat:17 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = col && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:31 sat:13 unsat:18 numeric PC: constraint # = 6 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:32 sat:14 unsat:18 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 7 row = col && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:33 sat:14 unsat:19 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:133) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 row != col && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:34 sat:15 unsat:19 string analysis: SPC # = 0 NPC constraint # = 7 row != col && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:136) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 2 = col && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:35 sat:15 unsat:20 numeric PC: constraint # = 7 col < 0 && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:36 sat:15 unsat:21 numeric PC: constraint # = 7 col >= 3 && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:37 sat:15 unsat:22 numeric PC: constraint # = 7 2 = col && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:38 sat:15 unsat:23 numeric PC: constraint # = 7 col < 0 && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:39 sat:15 unsat:24 numeric PC: constraint # = 7 col >= 3 && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:40 sat:15 unsat:25 numeric PC: constraint # = 7 1 = row && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:41 sat:15 unsat:26 numeric PC: constraint # = 7 2 = row && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:42 sat:15 unsat:27 numeric PC: constraint # = 7 row < 0 && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:43 sat:15 unsat:28 numeric PC: constraint # = 7 row >= 3 && 1 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:44 sat:15 unsat:29 numeric PC: constraint # = 6 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:45 sat:16 unsat:29 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:46 sat:17 unsat:29 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = col && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:47 sat:17 unsat:30 numeric PC: constraint # = 7 1 = col && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:48 sat:17 unsat:31 numeric PC: constraint # = 6 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:49 sat:18 unsat:31 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = col && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:50 sat:18 unsat:32 numeric PC: constraint # = 7 1 = col && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:51 sat:18 unsat:33 numeric PC: constraint # = 6 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:52 sat:19 unsat:33 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 7 row = col && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:53 sat:19 unsat:34 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:133) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 row != col && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:54 sat:20 unsat:34 string analysis: SPC # = 0 NPC constraint # = 7 row != col && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:136) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 col < 0 && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:55 sat:20 unsat:35 numeric PC: constraint # = 7 col >= 3 && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:56 sat:20 unsat:36 numeric PC: constraint # = 7 col < 0 && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:57 sat:20 unsat:37 numeric PC: constraint # = 7 col >= 3 && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:58 sat:20 unsat:38 numeric PC: constraint # = 7 1 = row && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:59 sat:20 unsat:39 numeric PC: constraint # = 7 2 = row && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:60 sat:20 unsat:40 numeric PC: constraint # = 7 row < 0 && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:61 sat:20 unsat:41 numeric PC: constraint # = 7 row >= 3 && 2 = col && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:62 sat:20 unsat:42 numeric PC: constraint # = 6 col < 0 && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:63 sat:20 unsat:43 numeric PC: constraint # = 6 col >= 3 && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:64 sat:21 unsat:43 string analysis: SPC # = 0 NPC constraint # = 6 col >= 3 && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 6 col >= 3 && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true string analysis: SPC # = 0 NPC constraint # = 6 col >= 3 && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 Property Violated: PC is constraint # = 6 col >= 3 && 0 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 Property Violated: result is "java.lang.ArrayIndexOutOfBoundsException..." **************************** ====================================================== error 1 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.ArrayIndexOutOfBoundsException at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) ====================================================== snapshot #1 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) ====================================================== trace #1 ------------------------------------------------------ transition #0 thread: 0 gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"ROOT" ,1/1,isCascaded:false} [3099 insn w/o sources] TTTConsoleNonOO2P.java:23 : public static int[][] board = new int[ROWS][COLS]; // game board in 2D array TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner [5 insn w/o sources] TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner [4 insn w/o sources] TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner TTTConsoleNonOO2P.java:1 : import java.util.Scanner; [1 insn w/o sources] TTTConsoleNonOO2P.java:35 : int row = 0; TTTConsoleNonOO2P.java:37 : int col = 0; TTTConsoleNonOO2P.java:39 : startGame(row, col); ------------------------------------------------------ transition #1 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..0,delta=+1,cur=0] TTTConsoleNonOO2P.java:39 : startGame(row, col); TTTConsoleNonOO2P.java:44 : initGame(); TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:71 : currentState = PLAYING; // ready to play TTTConsoleNonOO2P.java:72 : currentPlayer = CROSS; // cross plays first TTTConsoleNonOO2P.java:73 : } TTTConsoleNonOO2P.java:48 : playerMove(currentPlayer, row, col); // update currentRow and currentCol TTTConsoleNonOO2P.java:78 : boolean validInput = false; // for input validation TTTConsoleNonOO2P.java:80 : if (theSeed == CROSS) { TTTConsoleNonOO2P.java:81 : System.out.print("Player 'X', enter your move (row[1-3] column[1-3]): "); [2 insn w/o sources] TTTConsoleNonOO2P.java:82 : } else { TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #2 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #3 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #4 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #5 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { TTTConsoleNonOO2P.java:88 : currntRow = row; TTTConsoleNonOO2P.java:89 : currentCol = col; TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content ------------------------------------------------------ transition #6 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=0] TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content ------------------------------------------------------ transition #7 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=4] numeric PC: constraint # = 5 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:65 sat:22 unsat:43 string analysis: SPC # = 0 NPC constraint # = 5 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:66 sat:23 unsat:43 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = row && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:67 sat:23 unsat:44 numeric PC: constraint # = 6 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:68 sat:24 unsat:44 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = row && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:69 sat:24 unsat:45 numeric PC: constraint # = 6 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:70 sat:25 unsat:45 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:71 sat:26 unsat:45 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 7 row = col && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:72 sat:26 unsat:46 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:133) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 row != col && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:73 sat:27 unsat:46 string analysis: SPC # = 0 NPC constraint # = 7 row != col && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:136) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 1 = col && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:74 sat:27 unsat:47 numeric PC: constraint # = 7 2 = col && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:75 sat:27 unsat:48 numeric PC: constraint # = 7 col < 0 && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:76 sat:27 unsat:49 numeric PC: constraint # = 7 col >= 3 && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:77 sat:27 unsat:50 numeric PC: constraint # = 7 2 = row && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:78 sat:27 unsat:51 numeric PC: constraint # = 7 row < 0 && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:79 sat:27 unsat:52 numeric PC: constraint # = 7 row >= 3 && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:80 sat:27 unsat:53 numeric PC: constraint # = 7 2 = row && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:81 sat:27 unsat:54 numeric PC: constraint # = 7 row < 0 && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:82 sat:27 unsat:55 numeric PC: constraint # = 7 row >= 3 && 0 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:83 sat:27 unsat:56 numeric PC: constraint # = 6 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:84 sat:28 unsat:56 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = row && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:85 sat:28 unsat:57 numeric PC: constraint # = 6 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:86 sat:29 unsat:57 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = col && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:87 sat:29 unsat:58 numeric PC: constraint # = 6 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:88 sat:30 unsat:58 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 7 row = col && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:89 sat:31 unsat:58 string analysis: SPC # = 0 NPC constraint # = 7 row = col && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 8 (col + row) = 2 && row = col && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:90 sat:32 unsat:58 string analysis: SPC # = 0 NPC constraint # = 8 (col + row) = 2 && row = col && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 | | ----------- | X | ----------- | | Player 'O', enter your move (row[1-3] column[1-3]): ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 8 (col + row) != 2 && row = col && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:91 sat:32 unsat:59 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:126) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 row != col && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:92 sat:32 unsat:60 numeric PC: constraint # = 7 2 = col && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:93 sat:32 unsat:61 numeric PC: constraint # = 7 col < 0 && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:94 sat:32 unsat:62 numeric PC: constraint # = 7 col >= 3 && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:95 sat:32 unsat:63 numeric PC: constraint # = 7 2 = row && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:96 sat:32 unsat:64 numeric PC: constraint # = 7 row < 0 && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:97 sat:32 unsat:65 numeric PC: constraint # = 7 row >= 3 && 1 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:98 sat:32 unsat:66 numeric PC: constraint # = 6 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:99 sat:33 unsat:66 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = row && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:100 sat:33 unsat:67 numeric PC: constraint # = 6 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:101 sat:34 unsat:67 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = col && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:102 sat:34 unsat:68 numeric PC: constraint # = 7 1 = col && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:103 sat:34 unsat:69 numeric PC: constraint # = 6 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:104 sat:35 unsat:69 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 7 row = col && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:105 sat:35 unsat:70 numeric PC: constraint # = 7 row != col && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:106 sat:36 unsat:70 string analysis: SPC # = 0 NPC constraint # = 7 row != col && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 8 (col + row) = 2 && row != col && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:107 sat:36 unsat:71 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:137) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 8 (col + row) != 2 && row != col && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:108 sat:37 unsat:71 string analysis: SPC # = 0 NPC constraint # = 8 (col + row) != 2 && row != col && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 | | ----------- | | X ----------- | | Player 'O', enter your move (row[1-3] column[1-3]): ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 col < 0 && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:109 sat:37 unsat:72 numeric PC: constraint # = 7 col >= 3 && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:110 sat:37 unsat:73 numeric PC: constraint # = 7 2 = row && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:111 sat:37 unsat:74 numeric PC: constraint # = 7 row < 0 && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:112 sat:37 unsat:75 numeric PC: constraint # = 7 row >= 3 && 2 = col && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:113 sat:37 unsat:76 numeric PC: constraint # = 6 col < 0 && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:114 sat:37 unsat:77 numeric PC: constraint # = 6 col >= 3 && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:115 sat:38 unsat:77 string analysis: SPC # = 0 NPC constraint # = 6 col >= 3 && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 6 col >= 3 && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true string analysis: SPC # = 0 NPC constraint # = 6 col >= 3 && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 Property Violated: PC is constraint # = 6 col >= 3 && 1 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 Property Violated: result is "java.lang.ArrayIndexOutOfBoundsException..." **************************** ====================================================== error 2 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.ArrayIndexOutOfBoundsException at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) ====================================================== snapshot #2 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) ====================================================== trace #2 ------------------------------------------------------ transition #0 thread: 0 gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"ROOT" ,1/1,isCascaded:false} [3099 insn w/o sources] TTTConsoleNonOO2P.java:23 : public static int[][] board = new int[ROWS][COLS]; // game board in 2D array TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner [5 insn w/o sources] TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner [4 insn w/o sources] TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner TTTConsoleNonOO2P.java:1 : import java.util.Scanner; [1 insn w/o sources] TTTConsoleNonOO2P.java:35 : int row = 0; TTTConsoleNonOO2P.java:37 : int col = 0; TTTConsoleNonOO2P.java:39 : startGame(row, col); ------------------------------------------------------ transition #1 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..0,delta=+1,cur=0] TTTConsoleNonOO2P.java:39 : startGame(row, col); TTTConsoleNonOO2P.java:44 : initGame(); TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:71 : currentState = PLAYING; // ready to play TTTConsoleNonOO2P.java:72 : currentPlayer = CROSS; // cross plays first TTTConsoleNonOO2P.java:73 : } TTTConsoleNonOO2P.java:48 : playerMove(currentPlayer, row, col); // update currentRow and currentCol TTTConsoleNonOO2P.java:78 : boolean validInput = false; // for input validation TTTConsoleNonOO2P.java:80 : if (theSeed == CROSS) { TTTConsoleNonOO2P.java:81 : System.out.print("Player 'X', enter your move (row[1-3] column[1-3]): "); [2 insn w/o sources] TTTConsoleNonOO2P.java:82 : } else { TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #2 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #3 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #4 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #5 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { TTTConsoleNonOO2P.java:88 : currntRow = row; TTTConsoleNonOO2P.java:89 : currentCol = col; TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content ------------------------------------------------------ transition #6 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=1] TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content ------------------------------------------------------ transition #7 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=4] numeric PC: constraint # = 5 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:116 sat:39 unsat:77 string analysis: SPC # = 0 NPC constraint # = 5 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:117 sat:40 unsat:77 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = row && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:118 sat:40 unsat:78 numeric PC: constraint # = 7 1 = row && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:119 sat:40 unsat:79 numeric PC: constraint # = 6 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:120 sat:41 unsat:79 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = row && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:121 sat:41 unsat:80 numeric PC: constraint # = 7 1 = row && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:122 sat:41 unsat:81 numeric PC: constraint # = 6 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:123 sat:42 unsat:81 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 6 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:124 sat:43 unsat:81 string analysis: SPC # = 0 NPC constraint # = 6 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 7 row = col && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:125 sat:43 unsat:82 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:133) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 row != col && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:126 sat:44 unsat:82 string analysis: SPC # = 0 NPC constraint # = 7 row != col && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:136) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 1 = col && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:127 sat:44 unsat:83 numeric PC: constraint # = 7 2 = col && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:128 sat:44 unsat:84 numeric PC: constraint # = 7 col < 0 && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:129 sat:44 unsat:85 numeric PC: constraint # = 7 col >= 3 && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:130 sat:44 unsat:86 numeric PC: constraint # = 7 row < 0 && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:131 sat:44 unsat:87 numeric PC: constraint # = 7 row >= 3 && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:132 sat:44 unsat:88 numeric PC: constraint # = 7 row < 0 && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:133 sat:44 unsat:89 numeric PC: constraint # = 7 row >= 3 && 0 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:134 sat:44 unsat:90 numeric PC: constraint # = 6 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:135 sat:45 unsat:90 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = row && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:136 sat:45 unsat:91 numeric PC: constraint # = 7 1 = row && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:137 sat:45 unsat:92 numeric PC: constraint # = 6 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:138 sat:46 unsat:92 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = col && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:139 sat:46 unsat:93 numeric PC: constraint # = 6 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:140 sat:47 unsat:93 string analysis: SPC # = 0 NPC constraint # = 6 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 7 row = col && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:141 sat:47 unsat:94 numeric PC: constraint # = 7 row != col && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:142 sat:48 unsat:94 string analysis: SPC # = 0 NPC constraint # = 7 row != col && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 8 (col + row) = 2 && row != col && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:143 sat:48 unsat:95 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:137) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 8 (col + row) != 2 && row != col && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:144 sat:49 unsat:95 string analysis: SPC # = 0 NPC constraint # = 8 (col + row) != 2 && row != col && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 | | ----------- | | ----------- | X | Player 'O', enter your move (row[1-3] column[1-3]): ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 2 = col && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:145 sat:49 unsat:96 numeric PC: constraint # = 7 col < 0 && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:146 sat:49 unsat:97 numeric PC: constraint # = 7 col >= 3 && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:147 sat:49 unsat:98 numeric PC: constraint # = 7 row < 0 && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:148 sat:49 unsat:99 numeric PC: constraint # = 7 row >= 3 && 1 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:149 sat:49 unsat:100 numeric PC: constraint # = 6 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:150 sat:50 unsat:100 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = row && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:151 sat:50 unsat:101 numeric PC: constraint # = 7 1 = row && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:152 sat:50 unsat:102 numeric PC: constraint # = 6 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:153 sat:51 unsat:102 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1] numeric PC: constraint # = 7 0 = col && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:154 sat:51 unsat:103 numeric PC: constraint # = 7 1 = col && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:155 sat:51 unsat:104 numeric PC: constraint # = 6 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:156 sat:52 unsat:104 string analysis: SPC # = 0 NPC constraint # = 6 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 7 row = col && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:157 sat:53 unsat:104 string analysis: SPC # = 0 NPC constraint # = 7 row = col && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 8 (col + row) = 2 && row = col && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:158 sat:53 unsat:105 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:137) at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 8 (col + row) != 2 && row = col && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:159 sat:54 unsat:105 string analysis: SPC # = 0 NPC constraint # = 8 (col + row) != 2 && row = col && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 | | ----------- | | ----------- | | X Player 'O', enter your move (row[1-3] column[1-3]): ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 7 row != col && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:160 sat:54 unsat:106 numeric PC: constraint # = 7 col < 0 && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:161 sat:54 unsat:107 numeric PC: constraint # = 7 col >= 3 && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:162 sat:54 unsat:108 numeric PC: constraint # = 7 row < 0 && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:163 sat:54 unsat:109 numeric PC: constraint # = 7 row >= 3 && 2 = col && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:164 sat:54 unsat:110 numeric PC: constraint # = 6 col < 0 && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:165 sat:54 unsat:111 numeric PC: constraint # = 6 col >= 3 && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:166 sat:55 unsat:111 string analysis: SPC # = 0 NPC constraint # = 6 col >= 3 && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 6 col >= 3 && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 -> true string analysis: SPC # = 0 NPC constraint # = 6 col >= 3 && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 Property Violated: PC is constraint # = 6 col >= 3 && 2 = row && col <= 3 && col >= 0 && row < 3 && row >= 0 Property Violated: result is "java.lang.ArrayIndexOutOfBoundsException..." **************************** ====================================================== error 3 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.ArrayIndexOutOfBoundsException at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) ====================================================== snapshot #3 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) ====================================================== trace #3 ------------------------------------------------------ transition #0 thread: 0 gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"ROOT" ,1/1,isCascaded:false} [3099 insn w/o sources] TTTConsoleNonOO2P.java:23 : public static int[][] board = new int[ROWS][COLS]; // game board in 2D array TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner [5 insn w/o sources] TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner [4 insn w/o sources] TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner TTTConsoleNonOO2P.java:1 : import java.util.Scanner; [1 insn w/o sources] TTTConsoleNonOO2P.java:35 : int row = 0; TTTConsoleNonOO2P.java:37 : int col = 0; TTTConsoleNonOO2P.java:39 : startGame(row, col); ------------------------------------------------------ transition #1 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..0,delta=+1,cur=0] TTTConsoleNonOO2P.java:39 : startGame(row, col); TTTConsoleNonOO2P.java:44 : initGame(); TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) { TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) { TTTConsoleNonOO2P.java:71 : currentState = PLAYING; // ready to play TTTConsoleNonOO2P.java:72 : currentPlayer = CROSS; // cross plays first TTTConsoleNonOO2P.java:73 : } TTTConsoleNonOO2P.java:48 : playerMove(currentPlayer, row, col); // update currentRow and currentCol TTTConsoleNonOO2P.java:78 : boolean validInput = false; // for input validation TTTConsoleNonOO2P.java:80 : if (theSeed == CROSS) { TTTConsoleNonOO2P.java:81 : System.out.print("Player 'X', enter your move (row[1-3] column[1-3]): "); [2 insn w/o sources] TTTConsoleNonOO2P.java:82 : } else { TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #2 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #3 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #4 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { ------------------------------------------------------ transition #5 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0] TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) { TTTConsoleNonOO2P.java:88 : currntRow = row; TTTConsoleNonOO2P.java:89 : currentCol = col; TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content ------------------------------------------------------ transition #6 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=2] TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content ------------------------------------------------------ transition #7 thread: 0 gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=4] numeric PC: constraint # = 5 row < 0 && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:167 sat:55 unsat:112 numeric PC: constraint # = 5 row >= 3 && col <= 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:168 sat:55 unsat:113 numeric PC: constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:169 sat:56 unsat:113 string analysis: SPC # = 0 NPC constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:170 sat:57 unsat:113 string analysis: SPC # = 0 NPC constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:171 sat:58 unsat:113 string analysis: SPC # = 0 NPC constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:172 sat:59 unsat:113 string analysis: SPC # = 0 NPC constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 5 col <= 3 && col > 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:173 sat:59 unsat:114 numeric PC: constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:174 sat:60 unsat:114 string analysis: SPC # = 0 NPC constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:175 sat:61 unsat:114 string analysis: SPC # = 0 NPC constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 numeric PC: constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 -> true ### PCs: total:176 sat:62 unsat:114 string analysis: SPC # = 0 NPC constraint # = 4 col > 3 && col >= 0 && row < 3 && row >= 0 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 5 row >= 3 && col > 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:177 sat:62 unsat:115 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:93) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 5 row < 0 && col > 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:178 sat:62 unsat:116 numeric PC: constraint # = 5 col < 0 && col > 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:179 sat:62 unsat:117 numeric PC: constraint # = 5 row >= 3 && col > 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:180 sat:62 unsat:118 numeric PC: constraint # = 5 row < 0 && col > 3 && col >= 0 && row < 3 && row >= 0 -> false ### PCs: total:181 sat:62 unsat:119 numeric PC: constraint # = 3 col < 0 && row < 3 && row >= 0 -> true ### PCs: total:182 sat:63 unsat:119 string analysis: SPC # = 0 NPC constraint # = 3 col < 0 && row < 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 3 col < 0 && row < 3 && row >= 0 -> true ### PCs: total:183 sat:64 unsat:119 string analysis: SPC # = 0 NPC constraint # = 3 col < 0 && row < 3 && row >= 0 numeric PC: constraint # = 3 col < 0 && row < 3 && row >= 0 -> true ### PCs: total:184 sat:65 unsat:119 string analysis: SPC # = 0 NPC constraint # = 3 col < 0 && row < 3 && row >= 0 numeric PC: constraint # = 4 col >= 0 && col < 0 && row < 3 && row >= 0 -> false ### PCs: total:185 sat:65 unsat:120 numeric PC: constraint # = 3 col < 0 && row < 3 && row >= 0 -> true ### PCs: total:186 sat:66 unsat:120 string analysis: SPC # = 0 NPC constraint # = 3 col < 0 && row < 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 3 col < 0 && row < 3 && row >= 0 -> true ### PCs: total:187 sat:67 unsat:120 string analysis: SPC # = 0 NPC constraint # = 3 col < 0 && row < 3 && row >= 0 numeric PC: constraint # = 3 col < 0 && row < 3 && row >= 0 -> true ### PCs: total:188 sat:68 unsat:120 string analysis: SPC # = 0 NPC constraint # = 3 col < 0 && row < 3 && row >= 0 numeric PC: constraint # = 4 col >= 0 && col < 0 && row < 3 && row >= 0 -> false ### PCs: total:189 sat:68 unsat:121 numeric PC: constraint # = 3 col < 0 && row < 3 && row >= 0 -> true ### PCs: total:190 sat:69 unsat:121 string analysis: SPC # = 0 NPC constraint # = 3 col < 0 && row < 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 3 col < 0 && row < 3 && row >= 0 -> true ### PCs: total:191 sat:70 unsat:121 string analysis: SPC # = 0 NPC constraint # = 3 col < 0 && row < 3 && row >= 0 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 4 row < 0 && col < 0 && row < 3 && row >= 0 -> false ### PCs: total:192 sat:70 unsat:122 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:93) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 4 row >= 3 && col < 0 && row < 3 && row >= 0 -> false ### PCs: total:193 sat:70 unsat:123 numeric PC: constraint # = 4 row < 0 && col < 0 && row < 3 && row >= 0 -> false ### PCs: total:194 sat:70 unsat:124 numeric PC: constraint # = 4 row >= 3 && col < 0 && row < 3 && row >= 0 -> false ### PCs: total:195 sat:70 unsat:125 numeric PC: constraint # = 4 row < 0 && col < 0 && row < 3 && row >= 0 -> false ### PCs: total:196 sat:70 unsat:126 numeric PC: constraint # = 2 row >= 3 && row >= 0 -> true ### PCs: total:197 sat:71 unsat:126 string analysis: SPC # = 0 NPC constraint # = 2 row >= 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 3 && row >= 0 -> true ### PCs: total:198 sat:72 unsat:126 string analysis: SPC # = 0 NPC constraint # = 2 row >= 3 && row >= 0 numeric PC: constraint # = 3 row < 3 && row >= 3 && row >= 0 -> false ### PCs: total:199 sat:72 unsat:127 numeric PC: constraint # = 2 row >= 3 && row >= 0 -> true ### PCs: total:200 sat:73 unsat:127 string analysis: SPC # = 0 NPC constraint # = 2 row >= 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 3 && row >= 0 -> true ### PCs: total:201 sat:74 unsat:127 string analysis: SPC # = 0 NPC constraint # = 2 row >= 3 && row >= 0 numeric PC: constraint # = 3 row < 3 && row >= 3 && row >= 0 -> false ### PCs: total:202 sat:74 unsat:128 numeric PC: constraint # = 2 row >= 3 && row >= 0 -> true ### PCs: total:203 sat:75 unsat:128 string analysis: SPC # = 0 NPC constraint # = 2 row >= 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 3 && row >= 0 -> true ### PCs: total:204 sat:76 unsat:128 string analysis: SPC # = 0 NPC constraint # = 2 row >= 3 && row >= 0 numeric PC: constraint # = 3 row < 3 && row >= 3 && row >= 0 -> false ### PCs: total:205 sat:76 unsat:129 numeric PC: constraint # = 2 row >= 3 && row >= 0 -> true ### PCs: total:206 sat:77 unsat:129 string analysis: SPC # = 0 NPC constraint # = 2 row >= 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 3 && row >= 0 -> true ### PCs: total:207 sat:78 unsat:129 string analysis: SPC # = 0 NPC constraint # = 2 row >= 3 && row >= 0 numeric PC: constraint # = 3 row < 3 && row >= 3 && row >= 0 -> false ### PCs: total:208 sat:78 unsat:130 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 2 row >= 3 && row >= 0 -> true ### PCs: total:209 sat:79 unsat:130 string analysis: SPC # = 0 NPC constraint # = 2 row >= 3 && row >= 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 3 row < 0 && row >= 3 && row >= 0 -> false ### PCs: total:210 sat:79 unsat:131 numeric PC: constraint # = 3 row < 0 && row >= 3 && row >= 0 -> false ### PCs: total:211 sat:79 unsat:132 numeric PC: constraint # = 3 row < 0 && row >= 3 && row >= 0 -> false ### PCs: total:212 sat:79 unsat:133 numeric PC: constraint # = 3 row < 0 && row >= 3 && row >= 0 -> false ### PCs: total:213 sat:79 unsat:134 numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:214 sat:80 unsat:134 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 0 && row < 0 -> false ### PCs: total:215 sat:80 unsat:135 numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:216 sat:81 unsat:135 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 0 && row < 0 -> false ### PCs: total:217 sat:81 unsat:136 numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:218 sat:82 unsat:136 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 0 && row < 0 -> false ### PCs: total:219 sat:82 unsat:137 numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:220 sat:83 unsat:137 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 0 && row < 0 -> false ### PCs: total:221 sat:83 unsat:138 numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:222 sat:84 unsat:138 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 0 && row < 0 -> false ### PCs: total:223 sat:84 unsat:139 numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:224 sat:85 unsat:139 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 0 && row < 0 -> false ### PCs: total:225 sat:85 unsat:140 numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:226 sat:86 unsat:140 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 0 && row < 0 -> false ### PCs: total:227 sat:86 unsat:141 numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:228 sat:87 unsat:141 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 0 && row < 0 -> false ### PCs: total:229 sat:87 unsat:142 numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:230 sat:88 unsat:142 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2 row >= 0 && row < 0 -> false ### PCs: total:231 sat:88 unsat:143 ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) numeric PC: constraint # = 1 row < 0 -> true ### PCs: total:232 sat:89 unsat:143 string analysis: SPC # = 0 NPC constraint # = 1 row < 0 This move at (0,0) is not valid. Try again... Player 'X', enter your move (row[1-3] column[1-3]): ====================================================== search constraint depth limit reached: 12 ====================================================== snapshot thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87) at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48) at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39) ====================================================== Method Summaries Inputs: row,col TTTConsoleNonOO2P.startGame() --> "java.lang.ArrayIndexOutOfBoundsException..." ====================================================== Method Summaries (HTML)

Test Cases Generated by Symbolic JavaPath Finder for TTTConsoleNonOO2P.startGame (Path Coverage)

rowcolRETURN
"java.lang.ArrayIndexOutOfBoundsException..."
====================================================== results error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArrayIndexOutOfBoundsException at TTTCo..." error #2: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArrayIndexOutOfBoundsException at TTTCo..." error #3: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArrayIndexOutOfBoundsException at TTTCo..." ====================================================== statistics elapsed time: 00:00:00 states: new=234,visited=0,backtracked=234,end=0 search: maxDepth=12,constraints=29 choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=75 heap: new=598,released=102,maxLive=369,gcCycles=65 instructions: 6307 max memory: 245MB loaded code: classes=68,methods=1475 ====================================================== search finished: 7/10/17 2:23 AM