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)
<h1>Test Cases Generated by Symbolic JavaPath Finder for TTTConsoleNonOO2P.startGame (Path Coverage) </h1>
<table border=1>
<tr><td>row</td><td>col</td><td>RETURN</td></tr>
<tr><td>"java.lang.ArrayIndexOutOfBoundsException..."</td></tr>
</table>
====================================================== 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
Comments