API tools faq
paste
cevilio

TTT

cevilio
Oct 6th, 2017
184
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 84.60 KB | None | 0 0
raw download clone embed print report
  1. Executing command: java -jar /Users/vchar/eclipsejava/jpf-core/build/RunJPF.jar +shell.port=4242 /Users/vchar/eclipsejava/JPF/src/examples/TTTConsoleNonOO2P.jpf
  2. Running Symbolic PathFinder ...
  3. symbolic.dp=choco
  4. symbolic.string_dp_timeout_ms=0
  5. symbolic.string_dp=none
  6. symbolic.choco_time_bound=30000
  7. symbolic.max_pc_length=2147483647
  8. symbolic.max_pc_msec=0
  9. symbolic.bvlength=32
  10. symbolic.min_int=-2147483648
  11. symbolic.min_long=-9223372036854775808
  12. symbolic.min_short=-32768
  13. symbolic.min_byte=-128
  14. symbolic.min_char=0
  15. symbolic.max_int=2147483647
  16. symbolic.max_long=9223372036854775807
  17. symbolic.max_short=32767
  18. symbolic.max_byte=127
  19. symbolic.max_char=65535
  20. symbolic.min_double=4.9E-324
  21. symbolic.max_double=1.7976931348623157E308
  22. JavaPathfinder core system v8.0 (rev ${version}) - (C) 2005-2014 United States Government. All rights reserved.
  23.  
  24.  
  25. ====================================================== system under test
  26. TTTConsoleNonOO2P.main()
  27.  
  28. ====================================================== search started: 7/10/17 2:23 AM
  29. New sym int row min=-2147483648, max=2147483647
  30. New sym int col min=-2147483648, max=2147483647
  31. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 1
  32. row >= 0 -> true
  33.  
  34. ### PCs: total:1 sat:1 unsat:0
  35.  
  36. string analysis: SPC # = 0
  37. NPC constraint # = 1
  38. row >= 0
  39. numeric PC: constraint # = 2
  40. row < 3 &&
  41. row >= 0 -> true
  42.  
  43. ### PCs: total:2 sat:2 unsat:0
  44.  
  45. string analysis: SPC # = 0
  46. NPC constraint # = 2
  47. row < 3 &&
  48. row >= 0
  49. numeric PC: constraint # = 3
  50. col >= 0 &&
  51. row < 3 &&
  52. row >= 0 -> true
  53.  
  54. ### PCs: total:3 sat:3 unsat:0
  55.  
  56. string analysis: SPC # = 0
  57. NPC constraint # = 3
  58. col >= 0 &&
  59. row < 3 &&
  60. row >= 0
  61. numeric PC: constraint # = 4
  62. col <= 3 &&
  63. col >= 0 &&
  64. row < 3 &&
  65. row >= 0 -> true
  66.  
  67. ### PCs: total:4 sat:4 unsat:0
  68.  
  69. string analysis: SPC # = 0
  70. NPC constraint # = 4
  71. col <= 3 &&
  72. col >= 0 &&
  73. row < 3 &&
  74. row >= 0
  75. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  76. numeric PC: constraint # = 5
  77. 0 = row &&
  78. col <= 3 &&
  79. col >= 0 &&
  80. row < 3 &&
  81. row >= 0 -> true
  82.  
  83. ### PCs: total:5 sat:5 unsat:0
  84.  
  85. string analysis: SPC # = 0
  86. NPC constraint # = 5
  87. 0 = row &&
  88. col <= 3 &&
  89. col >= 0 &&
  90. row < 3 &&
  91. row >= 0
  92. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  93. numeric PC: constraint # = 6
  94. 0 = col &&
  95. 0 = row &&
  96. col <= 3 &&
  97. col >= 0 &&
  98. row < 3 &&
  99. row >= 0 -> true
  100.  
  101. ### PCs: total:6 sat:6 unsat:0
  102.  
  103. string analysis: SPC # = 0
  104. NPC constraint # = 6
  105. 0 = col &&
  106. 0 = row &&
  107. col <= 3 &&
  108. col >= 0 &&
  109. row < 3 &&
  110. row >= 0
  111. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  112. numeric PC: constraint # = 6
  113. 0 = col &&
  114. 0 = row &&
  115. col <= 3 &&
  116. col >= 0 &&
  117. row < 3 &&
  118. row >= 0 -> true
  119.  
  120. ### PCs: total:7 sat:7 unsat:0
  121.  
  122. string analysis: SPC # = 0
  123. NPC constraint # = 6
  124. 0 = col &&
  125. 0 = row &&
  126. col <= 3 &&
  127. col >= 0 &&
  128. row < 3 &&
  129. row >= 0
  130. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  131. numeric PC: constraint # = 6
  132. 0 = col &&
  133. 0 = row &&
  134. col <= 3 &&
  135. col >= 0 &&
  136. row < 3 &&
  137. row >= 0 -> true
  138.  
  139. ### PCs: total:8 sat:8 unsat:0
  140.  
  141. string analysis: SPC # = 0
  142. NPC constraint # = 6
  143. 0 = col &&
  144. 0 = row &&
  145. col <= 3 &&
  146. col >= 0 &&
  147. row < 3 &&
  148. row >= 0
  149. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  150. numeric PC: constraint # = 6
  151. 0 = col &&
  152. 0 = row &&
  153. col <= 3 &&
  154. col >= 0 &&
  155. row < 3 &&
  156. row >= 0 -> true
  157.  
  158. ### PCs: total:9 sat:9 unsat:0
  159.  
  160. string analysis: SPC # = 0
  161. NPC constraint # = 6
  162. 0 = col &&
  163. 0 = row &&
  164. col <= 3 &&
  165. col >= 0 &&
  166. row < 3 &&
  167. row >= 0
  168. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  169. numeric PC: constraint # = 6
  170. 0 = col &&
  171. 0 = row &&
  172. col <= 3 &&
  173. col >= 0 &&
  174. row < 3 &&
  175. row >= 0 -> true
  176.  
  177. ### PCs: total:10 sat:10 unsat:0
  178.  
  179. string analysis: SPC # = 0
  180. NPC constraint # = 6
  181. 0 = col &&
  182. 0 = row &&
  183. col <= 3 &&
  184. col >= 0 &&
  185. row < 3 &&
  186. row >= 0
  187.  
  188. ====================================================== search constraint
  189. depth limit reached: 12
  190.  
  191. ====================================================== snapshot
  192. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  193. call stack:
  194. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:132)
  195. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  196. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  197. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  198.  
  199. numeric PC: constraint # = 7
  200. 1 = col &&
  201. 0 = col &&
  202. 0 = row &&
  203. col <= 3 &&
  204. col >= 0 &&
  205. row < 3 &&
  206. row >= 0 -> false
  207.  
  208. ### PCs: total:11 sat:10 unsat:1
  209.  
  210.  
  211. ====================================================== search constraint
  212. depth limit reached: 12
  213.  
  214. ====================================================== snapshot
  215. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  216. call stack:
  217. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:130)
  218. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  219. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  220. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  221.  
  222. numeric PC: constraint # = 7
  223. 2 = col &&
  224. 0 = col &&
  225. 0 = row &&
  226. col <= 3 &&
  227. col >= 0 &&
  228. row < 3 &&
  229. row >= 0 -> false
  230.  
  231. ### PCs: total:12 sat:10 unsat:2
  232.  
  233.  
  234. ====================================================== search constraint
  235. depth limit reached: 12
  236.  
  237. ====================================================== snapshot
  238. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  239. call stack:
  240. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:130)
  241. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  242. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  243. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  244.  
  245. numeric PC: constraint # = 7
  246. col < 0 &&
  247. 0 = col &&
  248. 0 = row &&
  249. col <= 3 &&
  250. col >= 0 &&
  251. row < 3 &&
  252. row >= 0 -> false
  253.  
  254. ### PCs: total:13 sat:10 unsat:3
  255.  
  256.  
  257. ====================================================== search constraint
  258. depth limit reached: 12
  259.  
  260. ====================================================== snapshot
  261. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  262. call stack:
  263. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:130)
  264. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  265. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  266. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  267.  
  268. numeric PC: constraint # = 7
  269. col >= 3 &&
  270. 0 = col &&
  271. 0 = row &&
  272. col <= 3 &&
  273. col >= 0 &&
  274. row < 3 &&
  275. row >= 0 -> false
  276.  
  277. ### PCs: total:14 sat:10 unsat:4
  278.  
  279.  
  280. ====================================================== search constraint
  281. depth limit reached: 12
  282.  
  283. ====================================================== snapshot
  284. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  285. call stack:
  286. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:130)
  287. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  288. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  289. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  290.  
  291. numeric PC: constraint # = 7
  292. 1 = col &&
  293. 0 = col &&
  294. 0 = row &&
  295. col <= 3 &&
  296. col >= 0 &&
  297. row < 3 &&
  298. row >= 0 -> false
  299.  
  300. ### PCs: total:15 sat:10 unsat:5
  301.  
  302. numeric PC: constraint # = 7
  303. 2 = col &&
  304. 0 = col &&
  305. 0 = row &&
  306. col <= 3 &&
  307. col >= 0 &&
  308. row < 3 &&
  309. row >= 0 -> false
  310.  
  311. ### PCs: total:16 sat:10 unsat:6
  312.  
  313. numeric PC: constraint # = 7
  314. col < 0 &&
  315. 0 = col &&
  316. 0 = row &&
  317. col <= 3 &&
  318. col >= 0 &&
  319. row < 3 &&
  320. row >= 0 -> false
  321.  
  322. ### PCs: total:17 sat:10 unsat:7
  323.  
  324. numeric PC: constraint # = 7
  325. col >= 3 &&
  326. 0 = col &&
  327. 0 = row &&
  328. col <= 3 &&
  329. col >= 0 &&
  330. row < 3 &&
  331. row >= 0 -> false
  332.  
  333. ### PCs: total:18 sat:10 unsat:8
  334.  
  335. numeric PC: constraint # = 7
  336. 1 = row &&
  337. 0 = col &&
  338. 0 = row &&
  339. col <= 3 &&
  340. col >= 0 &&
  341. row < 3 &&
  342. row >= 0 -> false
  343.  
  344. ### PCs: total:19 sat:10 unsat:9
  345.  
  346. numeric PC: constraint # = 7
  347. 2 = row &&
  348. 0 = col &&
  349. 0 = row &&
  350. col <= 3 &&
  351. col >= 0 &&
  352. row < 3 &&
  353. row >= 0 -> false
  354.  
  355. ### PCs: total:20 sat:10 unsat:10
  356.  
  357. numeric PC: constraint # = 7
  358. row < 0 &&
  359. 0 = col &&
  360. 0 = row &&
  361. col <= 3 &&
  362. col >= 0 &&
  363. row < 3 &&
  364. row >= 0 -> false
  365.  
  366. ### PCs: total:21 sat:10 unsat:11
  367.  
  368. numeric PC: constraint # = 7
  369. row >= 3 &&
  370. 0 = col &&
  371. 0 = row &&
  372. col <= 3 &&
  373. col >= 0 &&
  374. row < 3 &&
  375. row >= 0 -> false
  376.  
  377. ### PCs: total:22 sat:10 unsat:12
  378.  
  379. numeric PC: constraint # = 7
  380. 1 = row &&
  381. 0 = col &&
  382. 0 = row &&
  383. col <= 3 &&
  384. col >= 0 &&
  385. row < 3 &&
  386. row >= 0 -> false
  387.  
  388. ### PCs: total:23 sat:10 unsat:13
  389.  
  390. numeric PC: constraint # = 7
  391. 2 = row &&
  392. 0 = col &&
  393. 0 = row &&
  394. col <= 3 &&
  395. col >= 0 &&
  396. row < 3 &&
  397. row >= 0 -> false
  398.  
  399. ### PCs: total:24 sat:10 unsat:14
  400.  
  401. numeric PC: constraint # = 7
  402. row < 0 &&
  403. 0 = col &&
  404. 0 = row &&
  405. col <= 3 &&
  406. col >= 0 &&
  407. row < 3 &&
  408. row >= 0 -> false
  409.  
  410. ### PCs: total:25 sat:10 unsat:15
  411.  
  412. numeric PC: constraint # = 7
  413. row >= 3 &&
  414. 0 = col &&
  415. 0 = row &&
  416. col <= 3 &&
  417. col >= 0 &&
  418. row < 3 &&
  419. row >= 0 -> false
  420.  
  421. ### PCs: total:26 sat:10 unsat:16
  422.  
  423. numeric PC: constraint # = 6
  424. 1 = col &&
  425. 0 = row &&
  426. col <= 3 &&
  427. col >= 0 &&
  428. row < 3 &&
  429. row >= 0 -> true
  430.  
  431. ### PCs: total:27 sat:11 unsat:16
  432.  
  433. string analysis: SPC # = 0
  434. NPC constraint # = 6
  435. 1 = col &&
  436. 0 = row &&
  437. col <= 3 &&
  438. col >= 0 &&
  439. row < 3 &&
  440. row >= 0
  441. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  442. numeric PC: constraint # = 6
  443. 1 = col &&
  444. 0 = row &&
  445. col <= 3 &&
  446. col >= 0 &&
  447. row < 3 &&
  448. row >= 0 -> true
  449.  
  450. ### PCs: total:28 sat:12 unsat:16
  451.  
  452. string analysis: SPC # = 0
  453. NPC constraint # = 6
  454. 1 = col &&
  455. 0 = row &&
  456. col <= 3 &&
  457. col >= 0 &&
  458. row < 3 &&
  459. row >= 0
  460. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  461. numeric PC: constraint # = 7
  462. 0 = col &&
  463. 1 = col &&
  464. 0 = row &&
  465. col <= 3 &&
  466. col >= 0 &&
  467. row < 3 &&
  468. row >= 0 -> false
  469.  
  470. ### PCs: total:29 sat:12 unsat:17
  471.  
  472. numeric PC: constraint # = 6
  473. 1 = col &&
  474. 0 = row &&
  475. col <= 3 &&
  476. col >= 0 &&
  477. row < 3 &&
  478. row >= 0 -> true
  479.  
  480. ### PCs: total:30 sat:13 unsat:17
  481.  
  482. string analysis: SPC # = 0
  483. NPC constraint # = 6
  484. 1 = col &&
  485. 0 = row &&
  486. col <= 3 &&
  487. col >= 0 &&
  488. row < 3 &&
  489. row >= 0
  490. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  491. numeric PC: constraint # = 7
  492. 0 = col &&
  493. 1 = col &&
  494. 0 = row &&
  495. col <= 3 &&
  496. col >= 0 &&
  497. row < 3 &&
  498. row >= 0 -> false
  499.  
  500. ### PCs: total:31 sat:13 unsat:18
  501.  
  502. numeric PC: constraint # = 6
  503. 1 = col &&
  504. 0 = row &&
  505. col <= 3 &&
  506. col >= 0 &&
  507. row < 3 &&
  508. row >= 0 -> true
  509.  
  510. ### PCs: total:32 sat:14 unsat:18
  511.  
  512. string analysis: SPC # = 0
  513. NPC constraint # = 6
  514. 1 = col &&
  515. 0 = row &&
  516. col <= 3 &&
  517. col >= 0 &&
  518. row < 3 &&
  519. row >= 0
  520. numeric PC: constraint # = 7
  521. row = col &&
  522. 1 = col &&
  523. 0 = row &&
  524. col <= 3 &&
  525. col >= 0 &&
  526. row < 3 &&
  527. row >= 0 -> false
  528.  
  529. ### PCs: total:33 sat:14 unsat:19
  530.  
  531.  
  532. ====================================================== search constraint
  533. depth limit reached: 12
  534.  
  535. ====================================================== snapshot
  536. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  537. call stack:
  538. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:133)
  539. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  540. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  541. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  542.  
  543. numeric PC: constraint # = 7
  544. row != col &&
  545. 1 = col &&
  546. 0 = row &&
  547. col <= 3 &&
  548. col >= 0 &&
  549. row < 3 &&
  550. row >= 0 -> true
  551.  
  552. ### PCs: total:34 sat:15 unsat:19
  553.  
  554. string analysis: SPC # = 0
  555. NPC constraint # = 7
  556. row != col &&
  557. 1 = col &&
  558. 0 = row &&
  559. col <= 3 &&
  560. col >= 0 &&
  561. row < 3 &&
  562. row >= 0
  563.  
  564. ====================================================== search constraint
  565. depth limit reached: 12
  566.  
  567. ====================================================== snapshot
  568. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  569. call stack:
  570. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:136)
  571. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  572. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  573. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  574.  
  575. numeric PC: constraint # = 7
  576. 2 = col &&
  577. 1 = col &&
  578. 0 = row &&
  579. col <= 3 &&
  580. col >= 0 &&
  581. row < 3 &&
  582. row >= 0 -> false
  583.  
  584. ### PCs: total:35 sat:15 unsat:20
  585.  
  586. numeric PC: constraint # = 7
  587. col < 0 &&
  588. 1 = col &&
  589. 0 = row &&
  590. col <= 3 &&
  591. col >= 0 &&
  592. row < 3 &&
  593. row >= 0 -> false
  594.  
  595. ### PCs: total:36 sat:15 unsat:21
  596.  
  597. numeric PC: constraint # = 7
  598. col >= 3 &&
  599. 1 = col &&
  600. 0 = row &&
  601. col <= 3 &&
  602. col >= 0 &&
  603. row < 3 &&
  604. row >= 0 -> false
  605.  
  606. ### PCs: total:37 sat:15 unsat:22
  607.  
  608. numeric PC: constraint # = 7
  609. 2 = col &&
  610. 1 = col &&
  611. 0 = row &&
  612. col <= 3 &&
  613. col >= 0 &&
  614. row < 3 &&
  615. row >= 0 -> false
  616.  
  617. ### PCs: total:38 sat:15 unsat:23
  618.  
  619. numeric PC: constraint # = 7
  620. col < 0 &&
  621. 1 = col &&
  622. 0 = row &&
  623. col <= 3 &&
  624. col >= 0 &&
  625. row < 3 &&
  626. row >= 0 -> false
  627.  
  628. ### PCs: total:39 sat:15 unsat:24
  629.  
  630. numeric PC: constraint # = 7
  631. col >= 3 &&
  632. 1 = col &&
  633. 0 = row &&
  634. col <= 3 &&
  635. col >= 0 &&
  636. row < 3 &&
  637. row >= 0 -> false
  638.  
  639. ### PCs: total:40 sat:15 unsat:25
  640.  
  641. numeric PC: constraint # = 7
  642. 1 = row &&
  643. 1 = col &&
  644. 0 = row &&
  645. col <= 3 &&
  646. col >= 0 &&
  647. row < 3 &&
  648. row >= 0 -> false
  649.  
  650. ### PCs: total:41 sat:15 unsat:26
  651.  
  652. numeric PC: constraint # = 7
  653. 2 = row &&
  654. 1 = col &&
  655. 0 = row &&
  656. col <= 3 &&
  657. col >= 0 &&
  658. row < 3 &&
  659. row >= 0 -> false
  660.  
  661. ### PCs: total:42 sat:15 unsat:27
  662.  
  663. numeric PC: constraint # = 7
  664. row < 0 &&
  665. 1 = col &&
  666. 0 = row &&
  667. col <= 3 &&
  668. col >= 0 &&
  669. row < 3 &&
  670. row >= 0 -> false
  671.  
  672. ### PCs: total:43 sat:15 unsat:28
  673.  
  674. numeric PC: constraint # = 7
  675. row >= 3 &&
  676. 1 = col &&
  677. 0 = row &&
  678. col <= 3 &&
  679. col >= 0 &&
  680. row < 3 &&
  681. row >= 0 -> false
  682.  
  683. ### PCs: total:44 sat:15 unsat:29
  684.  
  685. numeric PC: constraint # = 6
  686. 2 = col &&
  687. 0 = row &&
  688. col <= 3 &&
  689. col >= 0 &&
  690. row < 3 &&
  691. row >= 0 -> true
  692.  
  693. ### PCs: total:45 sat:16 unsat:29
  694.  
  695. string analysis: SPC # = 0
  696. NPC constraint # = 6
  697. 2 = col &&
  698. 0 = row &&
  699. col <= 3 &&
  700. col >= 0 &&
  701. row < 3 &&
  702. row >= 0
  703. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  704. numeric PC: constraint # = 6
  705. 2 = col &&
  706. 0 = row &&
  707. col <= 3 &&
  708. col >= 0 &&
  709. row < 3 &&
  710. row >= 0 -> true
  711.  
  712. ### PCs: total:46 sat:17 unsat:29
  713.  
  714. string analysis: SPC # = 0
  715. NPC constraint # = 6
  716. 2 = col &&
  717. 0 = row &&
  718. col <= 3 &&
  719. col >= 0 &&
  720. row < 3 &&
  721. row >= 0
  722. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  723. numeric PC: constraint # = 7
  724. 0 = col &&
  725. 2 = col &&
  726. 0 = row &&
  727. col <= 3 &&
  728. col >= 0 &&
  729. row < 3 &&
  730. row >= 0 -> false
  731.  
  732. ### PCs: total:47 sat:17 unsat:30
  733.  
  734. numeric PC: constraint # = 7
  735. 1 = col &&
  736. 2 = col &&
  737. 0 = row &&
  738. col <= 3 &&
  739. col >= 0 &&
  740. row < 3 &&
  741. row >= 0 -> false
  742.  
  743. ### PCs: total:48 sat:17 unsat:31
  744.  
  745. numeric PC: constraint # = 6
  746. 2 = col &&
  747. 0 = row &&
  748. col <= 3 &&
  749. col >= 0 &&
  750. row < 3 &&
  751. row >= 0 -> true
  752.  
  753. ### PCs: total:49 sat:18 unsat:31
  754.  
  755. string analysis: SPC # = 0
  756. NPC constraint # = 6
  757. 2 = col &&
  758. 0 = row &&
  759. col <= 3 &&
  760. col >= 0 &&
  761. row < 3 &&
  762. row >= 0
  763. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  764. numeric PC: constraint # = 7
  765. 0 = col &&
  766. 2 = col &&
  767. 0 = row &&
  768. col <= 3 &&
  769. col >= 0 &&
  770. row < 3 &&
  771. row >= 0 -> false
  772.  
  773. ### PCs: total:50 sat:18 unsat:32
  774.  
  775. numeric PC: constraint # = 7
  776. 1 = col &&
  777. 2 = col &&
  778. 0 = row &&
  779. col <= 3 &&
  780. col >= 0 &&
  781. row < 3 &&
  782. row >= 0 -> false
  783.  
  784. ### PCs: total:51 sat:18 unsat:33
  785.  
  786. numeric PC: constraint # = 6
  787. 2 = col &&
  788. 0 = row &&
  789. col <= 3 &&
  790. col >= 0 &&
  791. row < 3 &&
  792. row >= 0 -> true
  793.  
  794. ### PCs: total:52 sat:19 unsat:33
  795.  
  796. string analysis: SPC # = 0
  797. NPC constraint # = 6
  798. 2 = col &&
  799. 0 = row &&
  800. col <= 3 &&
  801. col >= 0 &&
  802. row < 3 &&
  803. row >= 0
  804. numeric PC: constraint # = 7
  805. row = col &&
  806. 2 = col &&
  807. 0 = row &&
  808. col <= 3 &&
  809. col >= 0 &&
  810. row < 3 &&
  811. row >= 0 -> false
  812.  
  813. ### PCs: total:53 sat:19 unsat:34
  814.  
  815.  
  816. ====================================================== search constraint
  817. depth limit reached: 12
  818.  
  819. ====================================================== snapshot
  820. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  821. call stack:
  822. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:133)
  823. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  824. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  825. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  826.  
  827. numeric PC: constraint # = 7
  828. row != col &&
  829. 2 = col &&
  830. 0 = row &&
  831. col <= 3 &&
  832. col >= 0 &&
  833. row < 3 &&
  834. row >= 0 -> true
  835.  
  836. ### PCs: total:54 sat:20 unsat:34
  837.  
  838. string analysis: SPC # = 0
  839. NPC constraint # = 7
  840. row != col &&
  841. 2 = col &&
  842. 0 = row &&
  843. col <= 3 &&
  844. col >= 0 &&
  845. row < 3 &&
  846. row >= 0
  847.  
  848. ====================================================== search constraint
  849. depth limit reached: 12
  850.  
  851. ====================================================== snapshot
  852. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  853. call stack:
  854. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:136)
  855. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  856. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  857. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  858.  
  859. numeric PC: constraint # = 7
  860. col < 0 &&
  861. 2 = col &&
  862. 0 = row &&
  863. col <= 3 &&
  864. col >= 0 &&
  865. row < 3 &&
  866. row >= 0 -> false
  867.  
  868. ### PCs: total:55 sat:20 unsat:35
  869.  
  870. numeric PC: constraint # = 7
  871. col >= 3 &&
  872. 2 = col &&
  873. 0 = row &&
  874. col <= 3 &&
  875. col >= 0 &&
  876. row < 3 &&
  877. row >= 0 -> false
  878.  
  879. ### PCs: total:56 sat:20 unsat:36
  880.  
  881. numeric PC: constraint # = 7
  882. col < 0 &&
  883. 2 = col &&
  884. 0 = row &&
  885. col <= 3 &&
  886. col >= 0 &&
  887. row < 3 &&
  888. row >= 0 -> false
  889.  
  890. ### PCs: total:57 sat:20 unsat:37
  891.  
  892. numeric PC: constraint # = 7
  893. col >= 3 &&
  894. 2 = col &&
  895. 0 = row &&
  896. col <= 3 &&
  897. col >= 0 &&
  898. row < 3 &&
  899. row >= 0 -> false
  900.  
  901. ### PCs: total:58 sat:20 unsat:38
  902.  
  903. numeric PC: constraint # = 7
  904. 1 = row &&
  905. 2 = col &&
  906. 0 = row &&
  907. col <= 3 &&
  908. col >= 0 &&
  909. row < 3 &&
  910. row >= 0 -> false
  911.  
  912. ### PCs: total:59 sat:20 unsat:39
  913.  
  914. numeric PC: constraint # = 7
  915. 2 = row &&
  916. 2 = col &&
  917. 0 = row &&
  918. col <= 3 &&
  919. col >= 0 &&
  920. row < 3 &&
  921. row >= 0 -> false
  922.  
  923. ### PCs: total:60 sat:20 unsat:40
  924.  
  925. numeric PC: constraint # = 7
  926. row < 0 &&
  927. 2 = col &&
  928. 0 = row &&
  929. col <= 3 &&
  930. col >= 0 &&
  931. row < 3 &&
  932. row >= 0 -> false
  933.  
  934. ### PCs: total:61 sat:20 unsat:41
  935.  
  936. numeric PC: constraint # = 7
  937. row >= 3 &&
  938. 2 = col &&
  939. 0 = row &&
  940. col <= 3 &&
  941. col >= 0 &&
  942. row < 3 &&
  943. row >= 0 -> false
  944.  
  945. ### PCs: total:62 sat:20 unsat:42
  946.  
  947. numeric PC: constraint # = 6
  948. col < 0 &&
  949. 0 = row &&
  950. col <= 3 &&
  951. col >= 0 &&
  952. row < 3 &&
  953. row >= 0 -> false
  954.  
  955. ### PCs: total:63 sat:20 unsat:43
  956.  
  957. numeric PC: constraint # = 6
  958. col >= 3 &&
  959. 0 = row &&
  960. col <= 3 &&
  961. col >= 0 &&
  962. row < 3 &&
  963. row >= 0 -> true
  964.  
  965. ### PCs: total:64 sat:21 unsat:43
  966.  
  967. string analysis: SPC # = 0
  968. NPC constraint # = 6
  969. col >= 3 &&
  970. 0 = row &&
  971. col <= 3 &&
  972. col >= 0 &&
  973. row < 3 &&
  974. row >= 0
  975. numeric PC: constraint # = 6
  976. col >= 3 &&
  977. 0 = row &&
  978. col <= 3 &&
  979. col >= 0 &&
  980. row < 3 &&
  981. row >= 0 -> true
  982.  
  983. string analysis: SPC # = 0
  984. NPC constraint # = 6
  985. col >= 3 &&
  986. 0 = row &&
  987. col <= 3 &&
  988. col >= 0 &&
  989. row < 3 &&
  990. row >= 0
  991. Property Violated: PC is constraint # = 6
  992. col >= 3 &&
  993. 0 = row &&
  994. col <= 3 &&
  995. col >= 0 &&
  996. row < 3 &&
  997. row >= 0
  998. Property Violated: result is "java.lang.ArrayIndexOutOfBoundsException..."
  999. ****************************
  1000.  
  1001. ====================================================== error 1
  1002. gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
  1003. java.lang.ArrayIndexOutOfBoundsException
  1004. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90)
  1005. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  1006. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1007.  
  1008.  
  1009. ====================================================== snapshot #1
  1010. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  1011. call stack:
  1012. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90)
  1013. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  1014. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1015.  
  1016.  
  1017. ====================================================== trace #1
  1018. ------------------------------------------------------ transition #0 thread: 0
  1019. gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"ROOT" ,1/1,isCascaded:false}
  1020. [3099 insn w/o sources]
  1021. TTTConsoleNonOO2P.java:23 : public static int[][] board = new int[ROWS][COLS]; // game board in 2D array
  1022. TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner
  1023. [5 insn w/o sources]
  1024. TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner
  1025. [4 insn w/o sources]
  1026. TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner
  1027. TTTConsoleNonOO2P.java:1 : import java.util.Scanner;
  1028. [1 insn w/o sources]
  1029. TTTConsoleNonOO2P.java:35 : int row = 0;
  1030. TTTConsoleNonOO2P.java:37 : int col = 0;
  1031. TTTConsoleNonOO2P.java:39 : startGame(row, col);
  1032. ------------------------------------------------------ transition #1 thread: 0
  1033. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..0,delta=+1,cur=0]
  1034. TTTConsoleNonOO2P.java:39 : startGame(row, col);
  1035. TTTConsoleNonOO2P.java:44 : initGame();
  1036. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  1037. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1038. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1039. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1040. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1041. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1042. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1043. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1044. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  1045. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1046. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1047. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1048. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1049. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1050. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1051. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1052. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  1053. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1054. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1055. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1056. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1057. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1058. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1059. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1060. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  1061. TTTConsoleNonOO2P.java:71 : currentState = PLAYING; // ready to play
  1062. TTTConsoleNonOO2P.java:72 : currentPlayer = CROSS; // cross plays first
  1063. TTTConsoleNonOO2P.java:73 : }
  1064. TTTConsoleNonOO2P.java:48 : playerMove(currentPlayer, row, col); // update currentRow and currentCol
  1065. TTTConsoleNonOO2P.java:78 : boolean validInput = false; // for input validation
  1066. TTTConsoleNonOO2P.java:80 : if (theSeed == CROSS) {
  1067. TTTConsoleNonOO2P.java:81 : System.out.print("Player 'X', enter your move (row[1-3] column[1-3]): ");
  1068. [2 insn w/o sources]
  1069. TTTConsoleNonOO2P.java:82 : } else {
  1070. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1071. ------------------------------------------------------ transition #2 thread: 0
  1072. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  1073. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1074. ------------------------------------------------------ transition #3 thread: 0
  1075. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  1076. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1077. ------------------------------------------------------ transition #4 thread: 0
  1078. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  1079. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1080. ------------------------------------------------------ transition #5 thread: 0
  1081. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  1082. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1083. TTTConsoleNonOO2P.java:88 : currntRow = row;
  1084. TTTConsoleNonOO2P.java:89 : currentCol = col;
  1085. TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content
  1086. ------------------------------------------------------ transition #6 thread: 0
  1087. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=0]
  1088. TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content
  1089. ------------------------------------------------------ transition #7 thread: 0
  1090. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=4]
  1091. numeric PC: constraint # = 5
  1092. 1 = row &&
  1093. col <= 3 &&
  1094. col >= 0 &&
  1095. row < 3 &&
  1096. row >= 0 -> true
  1097.  
  1098. ### PCs: total:65 sat:22 unsat:43
  1099.  
  1100. string analysis: SPC # = 0
  1101. NPC constraint # = 5
  1102. 1 = row &&
  1103. col <= 3 &&
  1104. col >= 0 &&
  1105. row < 3 &&
  1106. row >= 0
  1107. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  1108. numeric PC: constraint # = 6
  1109. 0 = col &&
  1110. 1 = row &&
  1111. col <= 3 &&
  1112. col >= 0 &&
  1113. row < 3 &&
  1114. row >= 0 -> true
  1115.  
  1116. ### PCs: total:66 sat:23 unsat:43
  1117.  
  1118. string analysis: SPC # = 0
  1119. NPC constraint # = 6
  1120. 0 = col &&
  1121. 1 = row &&
  1122. col <= 3 &&
  1123. col >= 0 &&
  1124. row < 3 &&
  1125. row >= 0
  1126. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  1127. numeric PC: constraint # = 7
  1128. 0 = row &&
  1129. 0 = col &&
  1130. 1 = row &&
  1131. col <= 3 &&
  1132. col >= 0 &&
  1133. row < 3 &&
  1134. row >= 0 -> false
  1135.  
  1136. ### PCs: total:67 sat:23 unsat:44
  1137.  
  1138. numeric PC: constraint # = 6
  1139. 0 = col &&
  1140. 1 = row &&
  1141. col <= 3 &&
  1142. col >= 0 &&
  1143. row < 3 &&
  1144. row >= 0 -> true
  1145.  
  1146. ### PCs: total:68 sat:24 unsat:44
  1147.  
  1148. string analysis: SPC # = 0
  1149. NPC constraint # = 6
  1150. 0 = col &&
  1151. 1 = row &&
  1152. col <= 3 &&
  1153. col >= 0 &&
  1154. row < 3 &&
  1155. row >= 0
  1156. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  1157. numeric PC: constraint # = 7
  1158. 0 = row &&
  1159. 0 = col &&
  1160. 1 = row &&
  1161. col <= 3 &&
  1162. col >= 0 &&
  1163. row < 3 &&
  1164. row >= 0 -> false
  1165.  
  1166. ### PCs: total:69 sat:24 unsat:45
  1167.  
  1168. numeric PC: constraint # = 6
  1169. 0 = col &&
  1170. 1 = row &&
  1171. col <= 3 &&
  1172. col >= 0 &&
  1173. row < 3 &&
  1174. row >= 0 -> true
  1175.  
  1176. ### PCs: total:70 sat:25 unsat:45
  1177.  
  1178. string analysis: SPC # = 0
  1179. NPC constraint # = 6
  1180. 0 = col &&
  1181. 1 = row &&
  1182. col <= 3 &&
  1183. col >= 0 &&
  1184. row < 3 &&
  1185. row >= 0
  1186. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  1187. numeric PC: constraint # = 6
  1188. 0 = col &&
  1189. 1 = row &&
  1190. col <= 3 &&
  1191. col >= 0 &&
  1192. row < 3 &&
  1193. row >= 0 -> true
  1194.  
  1195. ### PCs: total:71 sat:26 unsat:45
  1196.  
  1197. string analysis: SPC # = 0
  1198. NPC constraint # = 6
  1199. 0 = col &&
  1200. 1 = row &&
  1201. col <= 3 &&
  1202. col >= 0 &&
  1203. row < 3 &&
  1204. row >= 0
  1205. numeric PC: constraint # = 7
  1206. row = col &&
  1207. 0 = col &&
  1208. 1 = row &&
  1209. col <= 3 &&
  1210. col >= 0 &&
  1211. row < 3 &&
  1212. row >= 0 -> false
  1213.  
  1214. ### PCs: total:72 sat:26 unsat:46
  1215.  
  1216.  
  1217. ====================================================== search constraint
  1218. depth limit reached: 12
  1219.  
  1220. ====================================================== snapshot
  1221. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  1222. call stack:
  1223. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:133)
  1224. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  1225. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  1226. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1227.  
  1228. numeric PC: constraint # = 7
  1229. row != col &&
  1230. 0 = col &&
  1231. 1 = row &&
  1232. col <= 3 &&
  1233. col >= 0 &&
  1234. row < 3 &&
  1235. row >= 0 -> true
  1236.  
  1237. ### PCs: total:73 sat:27 unsat:46
  1238.  
  1239. string analysis: SPC # = 0
  1240. NPC constraint # = 7
  1241. row != col &&
  1242. 0 = col &&
  1243. 1 = row &&
  1244. col <= 3 &&
  1245. col >= 0 &&
  1246. row < 3 &&
  1247. row >= 0
  1248.  
  1249. ====================================================== search constraint
  1250. depth limit reached: 12
  1251.  
  1252. ====================================================== snapshot
  1253. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  1254. call stack:
  1255. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:136)
  1256. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  1257. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  1258. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1259.  
  1260. numeric PC: constraint # = 7
  1261. 1 = col &&
  1262. 0 = col &&
  1263. 1 = row &&
  1264. col <= 3 &&
  1265. col >= 0 &&
  1266. row < 3 &&
  1267. row >= 0 -> false
  1268.  
  1269. ### PCs: total:74 sat:27 unsat:47
  1270.  
  1271. numeric PC: constraint # = 7
  1272. 2 = col &&
  1273. 0 = col &&
  1274. 1 = row &&
  1275. col <= 3 &&
  1276. col >= 0 &&
  1277. row < 3 &&
  1278. row >= 0 -> false
  1279.  
  1280. ### PCs: total:75 sat:27 unsat:48
  1281.  
  1282. numeric PC: constraint # = 7
  1283. col < 0 &&
  1284. 0 = col &&
  1285. 1 = row &&
  1286. col <= 3 &&
  1287. col >= 0 &&
  1288. row < 3 &&
  1289. row >= 0 -> false
  1290.  
  1291. ### PCs: total:76 sat:27 unsat:49
  1292.  
  1293. numeric PC: constraint # = 7
  1294. col >= 3 &&
  1295. 0 = col &&
  1296. 1 = row &&
  1297. col <= 3 &&
  1298. col >= 0 &&
  1299. row < 3 &&
  1300. row >= 0 -> false
  1301.  
  1302. ### PCs: total:77 sat:27 unsat:50
  1303.  
  1304. numeric PC: constraint # = 7
  1305. 2 = row &&
  1306. 0 = col &&
  1307. 1 = row &&
  1308. col <= 3 &&
  1309. col >= 0 &&
  1310. row < 3 &&
  1311. row >= 0 -> false
  1312.  
  1313. ### PCs: total:78 sat:27 unsat:51
  1314.  
  1315. numeric PC: constraint # = 7
  1316. row < 0 &&
  1317. 0 = col &&
  1318. 1 = row &&
  1319. col <= 3 &&
  1320. col >= 0 &&
  1321. row < 3 &&
  1322. row >= 0 -> false
  1323.  
  1324. ### PCs: total:79 sat:27 unsat:52
  1325.  
  1326. numeric PC: constraint # = 7
  1327. row >= 3 &&
  1328. 0 = col &&
  1329. 1 = row &&
  1330. col <= 3 &&
  1331. col >= 0 &&
  1332. row < 3 &&
  1333. row >= 0 -> false
  1334.  
  1335. ### PCs: total:80 sat:27 unsat:53
  1336.  
  1337. numeric PC: constraint # = 7
  1338. 2 = row &&
  1339. 0 = col &&
  1340. 1 = row &&
  1341. col <= 3 &&
  1342. col >= 0 &&
  1343. row < 3 &&
  1344. row >= 0 -> false
  1345.  
  1346. ### PCs: total:81 sat:27 unsat:54
  1347.  
  1348. numeric PC: constraint # = 7
  1349. row < 0 &&
  1350. 0 = col &&
  1351. 1 = row &&
  1352. col <= 3 &&
  1353. col >= 0 &&
  1354. row < 3 &&
  1355. row >= 0 -> false
  1356.  
  1357. ### PCs: total:82 sat:27 unsat:55
  1358.  
  1359. numeric PC: constraint # = 7
  1360. row >= 3 &&
  1361. 0 = col &&
  1362. 1 = row &&
  1363. col <= 3 &&
  1364. col >= 0 &&
  1365. row < 3 &&
  1366. row >= 0 -> false
  1367.  
  1368. ### PCs: total:83 sat:27 unsat:56
  1369.  
  1370. numeric PC: constraint # = 6
  1371. 1 = col &&
  1372. 1 = row &&
  1373. col <= 3 &&
  1374. col >= 0 &&
  1375. row < 3 &&
  1376. row >= 0 -> true
  1377.  
  1378. ### PCs: total:84 sat:28 unsat:56
  1379.  
  1380. string analysis: SPC # = 0
  1381. NPC constraint # = 6
  1382. 1 = col &&
  1383. 1 = row &&
  1384. col <= 3 &&
  1385. col >= 0 &&
  1386. row < 3 &&
  1387. row >= 0
  1388. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  1389. numeric PC: constraint # = 7
  1390. 0 = row &&
  1391. 1 = col &&
  1392. 1 = row &&
  1393. col <= 3 &&
  1394. col >= 0 &&
  1395. row < 3 &&
  1396. row >= 0 -> false
  1397.  
  1398. ### PCs: total:85 sat:28 unsat:57
  1399.  
  1400. numeric PC: constraint # = 6
  1401. 1 = col &&
  1402. 1 = row &&
  1403. col <= 3 &&
  1404. col >= 0 &&
  1405. row < 3 &&
  1406. row >= 0 -> true
  1407.  
  1408. ### PCs: total:86 sat:29 unsat:57
  1409.  
  1410. string analysis: SPC # = 0
  1411. NPC constraint # = 6
  1412. 1 = col &&
  1413. 1 = row &&
  1414. col <= 3 &&
  1415. col >= 0 &&
  1416. row < 3 &&
  1417. row >= 0
  1418. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  1419. numeric PC: constraint # = 7
  1420. 0 = col &&
  1421. 1 = col &&
  1422. 1 = row &&
  1423. col <= 3 &&
  1424. col >= 0 &&
  1425. row < 3 &&
  1426. row >= 0 -> false
  1427.  
  1428. ### PCs: total:87 sat:29 unsat:58
  1429.  
  1430. numeric PC: constraint # = 6
  1431. 1 = col &&
  1432. 1 = row &&
  1433. col <= 3 &&
  1434. col >= 0 &&
  1435. row < 3 &&
  1436. row >= 0 -> true
  1437.  
  1438. ### PCs: total:88 sat:30 unsat:58
  1439.  
  1440. string analysis: SPC # = 0
  1441. NPC constraint # = 6
  1442. 1 = col &&
  1443. 1 = row &&
  1444. col <= 3 &&
  1445. col >= 0 &&
  1446. row < 3 &&
  1447. row >= 0
  1448. numeric PC: constraint # = 7
  1449. row = col &&
  1450. 1 = col &&
  1451. 1 = row &&
  1452. col <= 3 &&
  1453. col >= 0 &&
  1454. row < 3 &&
  1455. row >= 0 -> true
  1456.  
  1457. ### PCs: total:89 sat:31 unsat:58
  1458.  
  1459. string analysis: SPC # = 0
  1460. NPC constraint # = 7
  1461. row = col &&
  1462. 1 = col &&
  1463. 1 = row &&
  1464. col <= 3 &&
  1465. col >= 0 &&
  1466. row < 3 &&
  1467. row >= 0
  1468. numeric PC: constraint # = 8
  1469. (col + row) = 2 &&
  1470. row = col &&
  1471. 1 = col &&
  1472. 1 = row &&
  1473. col <= 3 &&
  1474. col >= 0 &&
  1475. row < 3 &&
  1476. row >= 0 -> true
  1477.  
  1478. ### PCs: total:90 sat:32 unsat:58
  1479.  
  1480. string analysis: SPC # = 0
  1481. NPC constraint # = 8
  1482. (col + row) = 2 &&
  1483. row = col &&
  1484. 1 = col &&
  1485. 1 = row &&
  1486. col <= 3 &&
  1487. col >= 0 &&
  1488. row < 3 &&
  1489. row >= 0
  1490. | |
  1491. -----------
  1492. | X |
  1493. -----------
  1494. | |
  1495.  
  1496. Player 'O', enter your move (row[1-3] column[1-3]):
  1497. ====================================================== search constraint
  1498. depth limit reached: 12
  1499.  
  1500. ====================================================== snapshot
  1501. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  1502. call stack:
  1503. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  1504. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  1505. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1506.  
  1507. numeric PC: constraint # = 8
  1508. (col + row) != 2 &&
  1509. row = col &&
  1510. 1 = col &&
  1511. 1 = row &&
  1512. col <= 3 &&
  1513. col >= 0 &&
  1514. row < 3 &&
  1515. row >= 0 -> false
  1516.  
  1517. ### PCs: total:91 sat:32 unsat:59
  1518.  
  1519.  
  1520. ====================================================== search constraint
  1521. depth limit reached: 12
  1522.  
  1523. ====================================================== snapshot
  1524. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  1525. call stack:
  1526. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:126)
  1527. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  1528. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  1529. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1530.  
  1531. numeric PC: constraint # = 7
  1532. row != col &&
  1533. 1 = col &&
  1534. 1 = row &&
  1535. col <= 3 &&
  1536. col >= 0 &&
  1537. row < 3 &&
  1538. row >= 0 -> false
  1539.  
  1540. ### PCs: total:92 sat:32 unsat:60
  1541.  
  1542. numeric PC: constraint # = 7
  1543. 2 = col &&
  1544. 1 = col &&
  1545. 1 = row &&
  1546. col <= 3 &&
  1547. col >= 0 &&
  1548. row < 3 &&
  1549. row >= 0 -> false
  1550.  
  1551. ### PCs: total:93 sat:32 unsat:61
  1552.  
  1553. numeric PC: constraint # = 7
  1554. col < 0 &&
  1555. 1 = col &&
  1556. 1 = row &&
  1557. col <= 3 &&
  1558. col >= 0 &&
  1559. row < 3 &&
  1560. row >= 0 -> false
  1561.  
  1562. ### PCs: total:94 sat:32 unsat:62
  1563.  
  1564. numeric PC: constraint # = 7
  1565. col >= 3 &&
  1566. 1 = col &&
  1567. 1 = row &&
  1568. col <= 3 &&
  1569. col >= 0 &&
  1570. row < 3 &&
  1571. row >= 0 -> false
  1572.  
  1573. ### PCs: total:95 sat:32 unsat:63
  1574.  
  1575. numeric PC: constraint # = 7
  1576. 2 = row &&
  1577. 1 = col &&
  1578. 1 = row &&
  1579. col <= 3 &&
  1580. col >= 0 &&
  1581. row < 3 &&
  1582. row >= 0 -> false
  1583.  
  1584. ### PCs: total:96 sat:32 unsat:64
  1585.  
  1586. numeric PC: constraint # = 7
  1587. row < 0 &&
  1588. 1 = col &&
  1589. 1 = row &&
  1590. col <= 3 &&
  1591. col >= 0 &&
  1592. row < 3 &&
  1593. row >= 0 -> false
  1594.  
  1595. ### PCs: total:97 sat:32 unsat:65
  1596.  
  1597. numeric PC: constraint # = 7
  1598. row >= 3 &&
  1599. 1 = col &&
  1600. 1 = row &&
  1601. col <= 3 &&
  1602. col >= 0 &&
  1603. row < 3 &&
  1604. row >= 0 -> false
  1605.  
  1606. ### PCs: total:98 sat:32 unsat:66
  1607.  
  1608. numeric PC: constraint # = 6
  1609. 2 = col &&
  1610. 1 = row &&
  1611. col <= 3 &&
  1612. col >= 0 &&
  1613. row < 3 &&
  1614. row >= 0 -> true
  1615.  
  1616. ### PCs: total:99 sat:33 unsat:66
  1617.  
  1618. string analysis: SPC # = 0
  1619. NPC constraint # = 6
  1620. 2 = col &&
  1621. 1 = row &&
  1622. col <= 3 &&
  1623. col >= 0 &&
  1624. row < 3 &&
  1625. row >= 0
  1626. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  1627. numeric PC: constraint # = 7
  1628. 0 = row &&
  1629. 2 = col &&
  1630. 1 = row &&
  1631. col <= 3 &&
  1632. col >= 0 &&
  1633. row < 3 &&
  1634. row >= 0 -> false
  1635.  
  1636. ### PCs: total:100 sat:33 unsat:67
  1637.  
  1638. numeric PC: constraint # = 6
  1639. 2 = col &&
  1640. 1 = row &&
  1641. col <= 3 &&
  1642. col >= 0 &&
  1643. row < 3 &&
  1644. row >= 0 -> true
  1645.  
  1646. ### PCs: total:101 sat:34 unsat:67
  1647.  
  1648. string analysis: SPC # = 0
  1649. NPC constraint # = 6
  1650. 2 = col &&
  1651. 1 = row &&
  1652. col <= 3 &&
  1653. col >= 0 &&
  1654. row < 3 &&
  1655. row >= 0
  1656. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  1657. numeric PC: constraint # = 7
  1658. 0 = col &&
  1659. 2 = col &&
  1660. 1 = row &&
  1661. col <= 3 &&
  1662. col >= 0 &&
  1663. row < 3 &&
  1664. row >= 0 -> false
  1665.  
  1666. ### PCs: total:102 sat:34 unsat:68
  1667.  
  1668. numeric PC: constraint # = 7
  1669. 1 = col &&
  1670. 2 = col &&
  1671. 1 = row &&
  1672. col <= 3 &&
  1673. col >= 0 &&
  1674. row < 3 &&
  1675. row >= 0 -> false
  1676.  
  1677. ### PCs: total:103 sat:34 unsat:69
  1678.  
  1679. numeric PC: constraint # = 6
  1680. 2 = col &&
  1681. 1 = row &&
  1682. col <= 3 &&
  1683. col >= 0 &&
  1684. row < 3 &&
  1685. row >= 0 -> true
  1686.  
  1687. ### PCs: total:104 sat:35 unsat:69
  1688.  
  1689. string analysis: SPC # = 0
  1690. NPC constraint # = 6
  1691. 2 = col &&
  1692. 1 = row &&
  1693. col <= 3 &&
  1694. col >= 0 &&
  1695. row < 3 &&
  1696. row >= 0
  1697. numeric PC: constraint # = 7
  1698. row = col &&
  1699. 2 = col &&
  1700. 1 = row &&
  1701. col <= 3 &&
  1702. col >= 0 &&
  1703. row < 3 &&
  1704. row >= 0 -> false
  1705.  
  1706. ### PCs: total:105 sat:35 unsat:70
  1707.  
  1708. numeric PC: constraint # = 7
  1709. row != col &&
  1710. 2 = col &&
  1711. 1 = row &&
  1712. col <= 3 &&
  1713. col >= 0 &&
  1714. row < 3 &&
  1715. row >= 0 -> true
  1716.  
  1717. ### PCs: total:106 sat:36 unsat:70
  1718.  
  1719. string analysis: SPC # = 0
  1720. NPC constraint # = 7
  1721. row != col &&
  1722. 2 = col &&
  1723. 1 = row &&
  1724. col <= 3 &&
  1725. col >= 0 &&
  1726. row < 3 &&
  1727. row >= 0
  1728. numeric PC: constraint # = 8
  1729. (col + row) = 2 &&
  1730. row != col &&
  1731. 2 = col &&
  1732. 1 = row &&
  1733. col <= 3 &&
  1734. col >= 0 &&
  1735. row < 3 &&
  1736. row >= 0 -> false
  1737.  
  1738. ### PCs: total:107 sat:36 unsat:71
  1739.  
  1740.  
  1741. ====================================================== search constraint
  1742. depth limit reached: 12
  1743.  
  1744. ====================================================== snapshot
  1745. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  1746. call stack:
  1747. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:137)
  1748. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  1749. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  1750. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1751.  
  1752. numeric PC: constraint # = 8
  1753. (col + row) != 2 &&
  1754. row != col &&
  1755. 2 = col &&
  1756. 1 = row &&
  1757. col <= 3 &&
  1758. col >= 0 &&
  1759. row < 3 &&
  1760. row >= 0 -> true
  1761.  
  1762. ### PCs: total:108 sat:37 unsat:71
  1763.  
  1764. string analysis: SPC # = 0
  1765. NPC constraint # = 8
  1766. (col + row) != 2 &&
  1767. row != col &&
  1768. 2 = col &&
  1769. 1 = row &&
  1770. col <= 3 &&
  1771. col >= 0 &&
  1772. row < 3 &&
  1773. row >= 0
  1774. | |
  1775. -----------
  1776. | | X
  1777. -----------
  1778. | |
  1779.  
  1780. Player 'O', enter your move (row[1-3] column[1-3]):
  1781. ====================================================== search constraint
  1782. depth limit reached: 12
  1783.  
  1784. ====================================================== snapshot
  1785. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  1786. call stack:
  1787. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  1788. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  1789. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1790.  
  1791. numeric PC: constraint # = 7
  1792. col < 0 &&
  1793. 2 = col &&
  1794. 1 = row &&
  1795. col <= 3 &&
  1796. col >= 0 &&
  1797. row < 3 &&
  1798. row >= 0 -> false
  1799.  
  1800. ### PCs: total:109 sat:37 unsat:72
  1801.  
  1802. numeric PC: constraint # = 7
  1803. col >= 3 &&
  1804. 2 = col &&
  1805. 1 = row &&
  1806. col <= 3 &&
  1807. col >= 0 &&
  1808. row < 3 &&
  1809. row >= 0 -> false
  1810.  
  1811. ### PCs: total:110 sat:37 unsat:73
  1812.  
  1813. numeric PC: constraint # = 7
  1814. 2 = row &&
  1815. 2 = col &&
  1816. 1 = row &&
  1817. col <= 3 &&
  1818. col >= 0 &&
  1819. row < 3 &&
  1820. row >= 0 -> false
  1821.  
  1822. ### PCs: total:111 sat:37 unsat:74
  1823.  
  1824. numeric PC: constraint # = 7
  1825. row < 0 &&
  1826. 2 = col &&
  1827. 1 = row &&
  1828. col <= 3 &&
  1829. col >= 0 &&
  1830. row < 3 &&
  1831. row >= 0 -> false
  1832.  
  1833. ### PCs: total:112 sat:37 unsat:75
  1834.  
  1835. numeric PC: constraint # = 7
  1836. row >= 3 &&
  1837. 2 = col &&
  1838. 1 = row &&
  1839. col <= 3 &&
  1840. col >= 0 &&
  1841. row < 3 &&
  1842. row >= 0 -> false
  1843.  
  1844. ### PCs: total:113 sat:37 unsat:76
  1845.  
  1846. numeric PC: constraint # = 6
  1847. col < 0 &&
  1848. 1 = row &&
  1849. col <= 3 &&
  1850. col >= 0 &&
  1851. row < 3 &&
  1852. row >= 0 -> false
  1853.  
  1854. ### PCs: total:114 sat:37 unsat:77
  1855.  
  1856. numeric PC: constraint # = 6
  1857. col >= 3 &&
  1858. 1 = row &&
  1859. col <= 3 &&
  1860. col >= 0 &&
  1861. row < 3 &&
  1862. row >= 0 -> true
  1863.  
  1864. ### PCs: total:115 sat:38 unsat:77
  1865.  
  1866. string analysis: SPC # = 0
  1867. NPC constraint # = 6
  1868. col >= 3 &&
  1869. 1 = row &&
  1870. col <= 3 &&
  1871. col >= 0 &&
  1872. row < 3 &&
  1873. row >= 0
  1874. numeric PC: constraint # = 6
  1875. col >= 3 &&
  1876. 1 = row &&
  1877. col <= 3 &&
  1878. col >= 0 &&
  1879. row < 3 &&
  1880. row >= 0 -> true
  1881.  
  1882. string analysis: SPC # = 0
  1883. NPC constraint # = 6
  1884. col >= 3 &&
  1885. 1 = row &&
  1886. col <= 3 &&
  1887. col >= 0 &&
  1888. row < 3 &&
  1889. row >= 0
  1890. Property Violated: PC is constraint # = 6
  1891. col >= 3 &&
  1892. 1 = row &&
  1893. col <= 3 &&
  1894. col >= 0 &&
  1895. row < 3 &&
  1896. row >= 0
  1897. Property Violated: result is "java.lang.ArrayIndexOutOfBoundsException..."
  1898. ****************************
  1899.  
  1900. ====================================================== error 2
  1901. gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
  1902. java.lang.ArrayIndexOutOfBoundsException
  1903. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90)
  1904. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  1905. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1906.  
  1907.  
  1908. ====================================================== snapshot #2
  1909. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  1910. call stack:
  1911. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90)
  1912. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  1913. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  1914.  
  1915.  
  1916. ====================================================== trace #2
  1917. ------------------------------------------------------ transition #0 thread: 0
  1918. gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"ROOT" ,1/1,isCascaded:false}
  1919. [3099 insn w/o sources]
  1920. TTTConsoleNonOO2P.java:23 : public static int[][] board = new int[ROWS][COLS]; // game board in 2D array
  1921. TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner
  1922. [5 insn w/o sources]
  1923. TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner
  1924. [4 insn w/o sources]
  1925. TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner
  1926. TTTConsoleNonOO2P.java:1 : import java.util.Scanner;
  1927. [1 insn w/o sources]
  1928. TTTConsoleNonOO2P.java:35 : int row = 0;
  1929. TTTConsoleNonOO2P.java:37 : int col = 0;
  1930. TTTConsoleNonOO2P.java:39 : startGame(row, col);
  1931. ------------------------------------------------------ transition #1 thread: 0
  1932. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..0,delta=+1,cur=0]
  1933. TTTConsoleNonOO2P.java:39 : startGame(row, col);
  1934. TTTConsoleNonOO2P.java:44 : initGame();
  1935. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  1936. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1937. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1938. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1939. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1940. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1941. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1942. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1943. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  1944. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1945. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1946. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1947. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1948. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1949. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1950. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1951. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  1952. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1953. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1954. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1955. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1956. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1957. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  1958. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  1959. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  1960. TTTConsoleNonOO2P.java:71 : currentState = PLAYING; // ready to play
  1961. TTTConsoleNonOO2P.java:72 : currentPlayer = CROSS; // cross plays first
  1962. TTTConsoleNonOO2P.java:73 : }
  1963. TTTConsoleNonOO2P.java:48 : playerMove(currentPlayer, row, col); // update currentRow and currentCol
  1964. TTTConsoleNonOO2P.java:78 : boolean validInput = false; // for input validation
  1965. TTTConsoleNonOO2P.java:80 : if (theSeed == CROSS) {
  1966. TTTConsoleNonOO2P.java:81 : System.out.print("Player 'X', enter your move (row[1-3] column[1-3]): ");
  1967. [2 insn w/o sources]
  1968. TTTConsoleNonOO2P.java:82 : } else {
  1969. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1970. ------------------------------------------------------ transition #2 thread: 0
  1971. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  1972. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1973. ------------------------------------------------------ transition #3 thread: 0
  1974. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  1975. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1976. ------------------------------------------------------ transition #4 thread: 0
  1977. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  1978. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1979. ------------------------------------------------------ transition #5 thread: 0
  1980. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  1981. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  1982. TTTConsoleNonOO2P.java:88 : currntRow = row;
  1983. TTTConsoleNonOO2P.java:89 : currentCol = col;
  1984. TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content
  1985. ------------------------------------------------------ transition #6 thread: 0
  1986. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=1]
  1987. TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content
  1988. ------------------------------------------------------ transition #7 thread: 0
  1989. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=4]
  1990. numeric PC: constraint # = 5
  1991. 2 = row &&
  1992. col <= 3 &&
  1993. col >= 0 &&
  1994. row < 3 &&
  1995. row >= 0 -> true
  1996.  
  1997. ### PCs: total:116 sat:39 unsat:77
  1998.  
  1999. string analysis: SPC # = 0
  2000. NPC constraint # = 5
  2001. 2 = row &&
  2002. col <= 3 &&
  2003. col >= 0 &&
  2004. row < 3 &&
  2005. row >= 0
  2006. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  2007. numeric PC: constraint # = 6
  2008. 0 = col &&
  2009. 2 = row &&
  2010. col <= 3 &&
  2011. col >= 0 &&
  2012. row < 3 &&
  2013. row >= 0 -> true
  2014.  
  2015. ### PCs: total:117 sat:40 unsat:77
  2016.  
  2017. string analysis: SPC # = 0
  2018. NPC constraint # = 6
  2019. 0 = col &&
  2020. 2 = row &&
  2021. col <= 3 &&
  2022. col >= 0 &&
  2023. row < 3 &&
  2024. row >= 0
  2025. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  2026. numeric PC: constraint # = 7
  2027. 0 = row &&
  2028. 0 = col &&
  2029. 2 = row &&
  2030. col <= 3 &&
  2031. col >= 0 &&
  2032. row < 3 &&
  2033. row >= 0 -> false
  2034.  
  2035. ### PCs: total:118 sat:40 unsat:78
  2036.  
  2037. numeric PC: constraint # = 7
  2038. 1 = row &&
  2039. 0 = col &&
  2040. 2 = row &&
  2041. col <= 3 &&
  2042. col >= 0 &&
  2043. row < 3 &&
  2044. row >= 0 -> false
  2045.  
  2046. ### PCs: total:119 sat:40 unsat:79
  2047.  
  2048. numeric PC: constraint # = 6
  2049. 0 = col &&
  2050. 2 = row &&
  2051. col <= 3 &&
  2052. col >= 0 &&
  2053. row < 3 &&
  2054. row >= 0 -> true
  2055.  
  2056. ### PCs: total:120 sat:41 unsat:79
  2057.  
  2058. string analysis: SPC # = 0
  2059. NPC constraint # = 6
  2060. 0 = col &&
  2061. 2 = row &&
  2062. col <= 3 &&
  2063. col >= 0 &&
  2064. row < 3 &&
  2065. row >= 0
  2066. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  2067. numeric PC: constraint # = 7
  2068. 0 = row &&
  2069. 0 = col &&
  2070. 2 = row &&
  2071. col <= 3 &&
  2072. col >= 0 &&
  2073. row < 3 &&
  2074. row >= 0 -> false
  2075.  
  2076. ### PCs: total:121 sat:41 unsat:80
  2077.  
  2078. numeric PC: constraint # = 7
  2079. 1 = row &&
  2080. 0 = col &&
  2081. 2 = row &&
  2082. col <= 3 &&
  2083. col >= 0 &&
  2084. row < 3 &&
  2085. row >= 0 -> false
  2086.  
  2087. ### PCs: total:122 sat:41 unsat:81
  2088.  
  2089. numeric PC: constraint # = 6
  2090. 0 = col &&
  2091. 2 = row &&
  2092. col <= 3 &&
  2093. col >= 0 &&
  2094. row < 3 &&
  2095. row >= 0 -> true
  2096.  
  2097. ### PCs: total:123 sat:42 unsat:81
  2098.  
  2099. string analysis: SPC # = 0
  2100. NPC constraint # = 6
  2101. 0 = col &&
  2102. 2 = row &&
  2103. col <= 3 &&
  2104. col >= 0 &&
  2105. row < 3 &&
  2106. row >= 0
  2107. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  2108. numeric PC: constraint # = 6
  2109. 0 = col &&
  2110. 2 = row &&
  2111. col <= 3 &&
  2112. col >= 0 &&
  2113. row < 3 &&
  2114. row >= 0 -> true
  2115.  
  2116. ### PCs: total:124 sat:43 unsat:81
  2117.  
  2118. string analysis: SPC # = 0
  2119. NPC constraint # = 6
  2120. 0 = col &&
  2121. 2 = row &&
  2122. col <= 3 &&
  2123. col >= 0 &&
  2124. row < 3 &&
  2125. row >= 0
  2126. numeric PC: constraint # = 7
  2127. row = col &&
  2128. 0 = col &&
  2129. 2 = row &&
  2130. col <= 3 &&
  2131. col >= 0 &&
  2132. row < 3 &&
  2133. row >= 0 -> false
  2134.  
  2135. ### PCs: total:125 sat:43 unsat:82
  2136.  
  2137.  
  2138. ====================================================== search constraint
  2139. depth limit reached: 12
  2140.  
  2141. ====================================================== snapshot
  2142. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  2143. call stack:
  2144. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:133)
  2145. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  2146. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  2147. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  2148.  
  2149. numeric PC: constraint # = 7
  2150. row != col &&
  2151. 0 = col &&
  2152. 2 = row &&
  2153. col <= 3 &&
  2154. col >= 0 &&
  2155. row < 3 &&
  2156. row >= 0 -> true
  2157.  
  2158. ### PCs: total:126 sat:44 unsat:82
  2159.  
  2160. string analysis: SPC # = 0
  2161. NPC constraint # = 7
  2162. row != col &&
  2163. 0 = col &&
  2164. 2 = row &&
  2165. col <= 3 &&
  2166. col >= 0 &&
  2167. row < 3 &&
  2168. row >= 0
  2169.  
  2170. ====================================================== search constraint
  2171. depth limit reached: 12
  2172.  
  2173. ====================================================== snapshot
  2174. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  2175. call stack:
  2176. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:136)
  2177. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  2178. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  2179. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  2180.  
  2181. numeric PC: constraint # = 7
  2182. 1 = col &&
  2183. 0 = col &&
  2184. 2 = row &&
  2185. col <= 3 &&
  2186. col >= 0 &&
  2187. row < 3 &&
  2188. row >= 0 -> false
  2189.  
  2190. ### PCs: total:127 sat:44 unsat:83
  2191.  
  2192. numeric PC: constraint # = 7
  2193. 2 = col &&
  2194. 0 = col &&
  2195. 2 = row &&
  2196. col <= 3 &&
  2197. col >= 0 &&
  2198. row < 3 &&
  2199. row >= 0 -> false
  2200.  
  2201. ### PCs: total:128 sat:44 unsat:84
  2202.  
  2203. numeric PC: constraint # = 7
  2204. col < 0 &&
  2205. 0 = col &&
  2206. 2 = row &&
  2207. col <= 3 &&
  2208. col >= 0 &&
  2209. row < 3 &&
  2210. row >= 0 -> false
  2211.  
  2212. ### PCs: total:129 sat:44 unsat:85
  2213.  
  2214. numeric PC: constraint # = 7
  2215. col >= 3 &&
  2216. 0 = col &&
  2217. 2 = row &&
  2218. col <= 3 &&
  2219. col >= 0 &&
  2220. row < 3 &&
  2221. row >= 0 -> false
  2222.  
  2223. ### PCs: total:130 sat:44 unsat:86
  2224.  
  2225. numeric PC: constraint # = 7
  2226. row < 0 &&
  2227. 0 = col &&
  2228. 2 = row &&
  2229. col <= 3 &&
  2230. col >= 0 &&
  2231. row < 3 &&
  2232. row >= 0 -> false
  2233.  
  2234. ### PCs: total:131 sat:44 unsat:87
  2235.  
  2236. numeric PC: constraint # = 7
  2237. row >= 3 &&
  2238. 0 = col &&
  2239. 2 = row &&
  2240. col <= 3 &&
  2241. col >= 0 &&
  2242. row < 3 &&
  2243. row >= 0 -> false
  2244.  
  2245. ### PCs: total:132 sat:44 unsat:88
  2246.  
  2247. numeric PC: constraint # = 7
  2248. row < 0 &&
  2249. 0 = col &&
  2250. 2 = row &&
  2251. col <= 3 &&
  2252. col >= 0 &&
  2253. row < 3 &&
  2254. row >= 0 -> false
  2255.  
  2256. ### PCs: total:133 sat:44 unsat:89
  2257.  
  2258. numeric PC: constraint # = 7
  2259. row >= 3 &&
  2260. 0 = col &&
  2261. 2 = row &&
  2262. col <= 3 &&
  2263. col >= 0 &&
  2264. row < 3 &&
  2265. row >= 0 -> false
  2266.  
  2267. ### PCs: total:134 sat:44 unsat:90
  2268.  
  2269. numeric PC: constraint # = 6
  2270. 1 = col &&
  2271. 2 = row &&
  2272. col <= 3 &&
  2273. col >= 0 &&
  2274. row < 3 &&
  2275. row >= 0 -> true
  2276.  
  2277. ### PCs: total:135 sat:45 unsat:90
  2278.  
  2279. string analysis: SPC # = 0
  2280. NPC constraint # = 6
  2281. 1 = col &&
  2282. 2 = row &&
  2283. col <= 3 &&
  2284. col >= 0 &&
  2285. row < 3 &&
  2286. row >= 0
  2287. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  2288. numeric PC: constraint # = 7
  2289. 0 = row &&
  2290. 1 = col &&
  2291. 2 = row &&
  2292. col <= 3 &&
  2293. col >= 0 &&
  2294. row < 3 &&
  2295. row >= 0 -> false
  2296.  
  2297. ### PCs: total:136 sat:45 unsat:91
  2298.  
  2299. numeric PC: constraint # = 7
  2300. 1 = row &&
  2301. 1 = col &&
  2302. 2 = row &&
  2303. col <= 3 &&
  2304. col >= 0 &&
  2305. row < 3 &&
  2306. row >= 0 -> false
  2307.  
  2308. ### PCs: total:137 sat:45 unsat:92
  2309.  
  2310. numeric PC: constraint # = 6
  2311. 1 = col &&
  2312. 2 = row &&
  2313. col <= 3 &&
  2314. col >= 0 &&
  2315. row < 3 &&
  2316. row >= 0 -> true
  2317.  
  2318. ### PCs: total:138 sat:46 unsat:92
  2319.  
  2320. string analysis: SPC # = 0
  2321. NPC constraint # = 6
  2322. 1 = col &&
  2323. 2 = row &&
  2324. col <= 3 &&
  2325. col >= 0 &&
  2326. row < 3 &&
  2327. row >= 0
  2328. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  2329. numeric PC: constraint # = 7
  2330. 0 = col &&
  2331. 1 = col &&
  2332. 2 = row &&
  2333. col <= 3 &&
  2334. col >= 0 &&
  2335. row < 3 &&
  2336. row >= 0 -> false
  2337.  
  2338. ### PCs: total:139 sat:46 unsat:93
  2339.  
  2340. numeric PC: constraint # = 6
  2341. 1 = col &&
  2342. 2 = row &&
  2343. col <= 3 &&
  2344. col >= 0 &&
  2345. row < 3 &&
  2346. row >= 0 -> true
  2347.  
  2348. ### PCs: total:140 sat:47 unsat:93
  2349.  
  2350. string analysis: SPC # = 0
  2351. NPC constraint # = 6
  2352. 1 = col &&
  2353. 2 = row &&
  2354. col <= 3 &&
  2355. col >= 0 &&
  2356. row < 3 &&
  2357. row >= 0
  2358. numeric PC: constraint # = 7
  2359. row = col &&
  2360. 1 = col &&
  2361. 2 = row &&
  2362. col <= 3 &&
  2363. col >= 0 &&
  2364. row < 3 &&
  2365. row >= 0 -> false
  2366.  
  2367. ### PCs: total:141 sat:47 unsat:94
  2368.  
  2369. numeric PC: constraint # = 7
  2370. row != col &&
  2371. 1 = col &&
  2372. 2 = row &&
  2373. col <= 3 &&
  2374. col >= 0 &&
  2375. row < 3 &&
  2376. row >= 0 -> true
  2377.  
  2378. ### PCs: total:142 sat:48 unsat:94
  2379.  
  2380. string analysis: SPC # = 0
  2381. NPC constraint # = 7
  2382. row != col &&
  2383. 1 = col &&
  2384. 2 = row &&
  2385. col <= 3 &&
  2386. col >= 0 &&
  2387. row < 3 &&
  2388. row >= 0
  2389. numeric PC: constraint # = 8
  2390. (col + row) = 2 &&
  2391. row != col &&
  2392. 1 = col &&
  2393. 2 = row &&
  2394. col <= 3 &&
  2395. col >= 0 &&
  2396. row < 3 &&
  2397. row >= 0 -> false
  2398.  
  2399. ### PCs: total:143 sat:48 unsat:95
  2400.  
  2401.  
  2402. ====================================================== search constraint
  2403. depth limit reached: 12
  2404.  
  2405. ====================================================== snapshot
  2406. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  2407. call stack:
  2408. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:137)
  2409. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  2410. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  2411. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  2412.  
  2413. numeric PC: constraint # = 8
  2414. (col + row) != 2 &&
  2415. row != col &&
  2416. 1 = col &&
  2417. 2 = row &&
  2418. col <= 3 &&
  2419. col >= 0 &&
  2420. row < 3 &&
  2421. row >= 0 -> true
  2422.  
  2423. ### PCs: total:144 sat:49 unsat:95
  2424.  
  2425. string analysis: SPC # = 0
  2426. NPC constraint # = 8
  2427. (col + row) != 2 &&
  2428. row != col &&
  2429. 1 = col &&
  2430. 2 = row &&
  2431. col <= 3 &&
  2432. col >= 0 &&
  2433. row < 3 &&
  2434. row >= 0
  2435. | |
  2436. -----------
  2437. | |
  2438. -----------
  2439. | X |
  2440.  
  2441. Player 'O', enter your move (row[1-3] column[1-3]):
  2442. ====================================================== search constraint
  2443. depth limit reached: 12
  2444.  
  2445. ====================================================== snapshot
  2446. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  2447. call stack:
  2448. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  2449. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  2450. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  2451.  
  2452. numeric PC: constraint # = 7
  2453. 2 = col &&
  2454. 1 = col &&
  2455. 2 = row &&
  2456. col <= 3 &&
  2457. col >= 0 &&
  2458. row < 3 &&
  2459. row >= 0 -> false
  2460.  
  2461. ### PCs: total:145 sat:49 unsat:96
  2462.  
  2463. numeric PC: constraint # = 7
  2464. col < 0 &&
  2465. 1 = col &&
  2466. 2 = row &&
  2467. col <= 3 &&
  2468. col >= 0 &&
  2469. row < 3 &&
  2470. row >= 0 -> false
  2471.  
  2472. ### PCs: total:146 sat:49 unsat:97
  2473.  
  2474. numeric PC: constraint # = 7
  2475. col >= 3 &&
  2476. 1 = col &&
  2477. 2 = row &&
  2478. col <= 3 &&
  2479. col >= 0 &&
  2480. row < 3 &&
  2481. row >= 0 -> false
  2482.  
  2483. ### PCs: total:147 sat:49 unsat:98
  2484.  
  2485. numeric PC: constraint # = 7
  2486. row < 0 &&
  2487. 1 = col &&
  2488. 2 = row &&
  2489. col <= 3 &&
  2490. col >= 0 &&
  2491. row < 3 &&
  2492. row >= 0 -> false
  2493.  
  2494. ### PCs: total:148 sat:49 unsat:99
  2495.  
  2496. numeric PC: constraint # = 7
  2497. row >= 3 &&
  2498. 1 = col &&
  2499. 2 = row &&
  2500. col <= 3 &&
  2501. col >= 0 &&
  2502. row < 3 &&
  2503. row >= 0 -> false
  2504.  
  2505. ### PCs: total:149 sat:49 unsat:100
  2506.  
  2507. numeric PC: constraint # = 6
  2508. 2 = col &&
  2509. 2 = row &&
  2510. col <= 3 &&
  2511. col >= 0 &&
  2512. row < 3 &&
  2513. row >= 0 -> true
  2514.  
  2515. ### PCs: total:150 sat:50 unsat:100
  2516.  
  2517. string analysis: SPC # = 0
  2518. NPC constraint # = 6
  2519. 2 = col &&
  2520. 2 = row &&
  2521. col <= 3 &&
  2522. col >= 0 &&
  2523. row < 3 &&
  2524. row >= 0
  2525. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  2526. numeric PC: constraint # = 7
  2527. 0 = row &&
  2528. 2 = col &&
  2529. 2 = row &&
  2530. col <= 3 &&
  2531. col >= 0 &&
  2532. row < 3 &&
  2533. row >= 0 -> false
  2534.  
  2535. ### PCs: total:151 sat:50 unsat:101
  2536.  
  2537. numeric PC: constraint # = 7
  2538. 1 = row &&
  2539. 2 = col &&
  2540. 2 = row &&
  2541. col <= 3 &&
  2542. col >= 0 &&
  2543. row < 3 &&
  2544. row >= 0 -> false
  2545.  
  2546. ### PCs: total:152 sat:50 unsat:102
  2547.  
  2548. numeric PC: constraint # = 6
  2549. 2 = col &&
  2550. 2 = row &&
  2551. col <= 3 &&
  2552. col >= 0 &&
  2553. row < 3 &&
  2554. row >= 0 -> true
  2555.  
  2556. ### PCs: total:153 sat:51 unsat:102
  2557.  
  2558. string analysis: SPC # = 0
  2559. NPC constraint # = 6
  2560. 2 = col &&
  2561. 2 = row &&
  2562. col <= 3 &&
  2563. col >= 0 &&
  2564. row < 3 &&
  2565. row >= 0
  2566. # array cg registered: gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=-1]
  2567. numeric PC: constraint # = 7
  2568. 0 = col &&
  2569. 2 = col &&
  2570. 2 = row &&
  2571. col <= 3 &&
  2572. col >= 0 &&
  2573. row < 3 &&
  2574. row >= 0 -> false
  2575.  
  2576. ### PCs: total:154 sat:51 unsat:103
  2577.  
  2578. numeric PC: constraint # = 7
  2579. 1 = col &&
  2580. 2 = col &&
  2581. 2 = row &&
  2582. col <= 3 &&
  2583. col >= 0 &&
  2584. row < 3 &&
  2585. row >= 0 -> false
  2586.  
  2587. ### PCs: total:155 sat:51 unsat:104
  2588.  
  2589. numeric PC: constraint # = 6
  2590. 2 = col &&
  2591. 2 = row &&
  2592. col <= 3 &&
  2593. col >= 0 &&
  2594. row < 3 &&
  2595. row >= 0 -> true
  2596.  
  2597. ### PCs: total:156 sat:52 unsat:104
  2598.  
  2599. string analysis: SPC # = 0
  2600. NPC constraint # = 6
  2601. 2 = col &&
  2602. 2 = row &&
  2603. col <= 3 &&
  2604. col >= 0 &&
  2605. row < 3 &&
  2606. row >= 0
  2607. numeric PC: constraint # = 7
  2608. row = col &&
  2609. 2 = col &&
  2610. 2 = row &&
  2611. col <= 3 &&
  2612. col >= 0 &&
  2613. row < 3 &&
  2614. row >= 0 -> true
  2615.  
  2616. ### PCs: total:157 sat:53 unsat:104
  2617.  
  2618. string analysis: SPC # = 0
  2619. NPC constraint # = 7
  2620. row = col &&
  2621. 2 = col &&
  2622. 2 = row &&
  2623. col <= 3 &&
  2624. col >= 0 &&
  2625. row < 3 &&
  2626. row >= 0
  2627. numeric PC: constraint # = 8
  2628. (col + row) = 2 &&
  2629. row = col &&
  2630. 2 = col &&
  2631. 2 = row &&
  2632. col <= 3 &&
  2633. col >= 0 &&
  2634. row < 3 &&
  2635. row >= 0 -> false
  2636.  
  2637. ### PCs: total:158 sat:53 unsat:105
  2638.  
  2639.  
  2640. ====================================================== search constraint
  2641. depth limit reached: 12
  2642.  
  2643. ====================================================== snapshot
  2644. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  2645. call stack:
  2646. at TTTConsoleNonOO2P.hasWon(TTTConsoleNonOO2P.java:137)
  2647. at TTTConsoleNonOO2P.updateGame(TTTConsoleNonOO2P.java:102)
  2648. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:49)
  2649. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  2650.  
  2651. numeric PC: constraint # = 8
  2652. (col + row) != 2 &&
  2653. row = col &&
  2654. 2 = col &&
  2655. 2 = row &&
  2656. col <= 3 &&
  2657. col >= 0 &&
  2658. row < 3 &&
  2659. row >= 0 -> true
  2660.  
  2661. ### PCs: total:159 sat:54 unsat:105
  2662.  
  2663. string analysis: SPC # = 0
  2664. NPC constraint # = 8
  2665. (col + row) != 2 &&
  2666. row = col &&
  2667. 2 = col &&
  2668. 2 = row &&
  2669. col <= 3 &&
  2670. col >= 0 &&
  2671. row < 3 &&
  2672. row >= 0
  2673. | |
  2674. -----------
  2675. | |
  2676. -----------
  2677. | | X
  2678.  
  2679. Player 'O', enter your move (row[1-3] column[1-3]):
  2680. ====================================================== search constraint
  2681. depth limit reached: 12
  2682.  
  2683. ====================================================== snapshot
  2684. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  2685. call stack:
  2686. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  2687. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  2688. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  2689.  
  2690. numeric PC: constraint # = 7
  2691. row != col &&
  2692. 2 = col &&
  2693. 2 = row &&
  2694. col <= 3 &&
  2695. col >= 0 &&
  2696. row < 3 &&
  2697. row >= 0 -> false
  2698.  
  2699. ### PCs: total:160 sat:54 unsat:106
  2700.  
  2701. numeric PC: constraint # = 7
  2702. col < 0 &&
  2703. 2 = col &&
  2704. 2 = row &&
  2705. col <= 3 &&
  2706. col >= 0 &&
  2707. row < 3 &&
  2708. row >= 0 -> false
  2709.  
  2710. ### PCs: total:161 sat:54 unsat:107
  2711.  
  2712. numeric PC: constraint # = 7
  2713. col >= 3 &&
  2714. 2 = col &&
  2715. 2 = row &&
  2716. col <= 3 &&
  2717. col >= 0 &&
  2718. row < 3 &&
  2719. row >= 0 -> false
  2720.  
  2721. ### PCs: total:162 sat:54 unsat:108
  2722.  
  2723. numeric PC: constraint # = 7
  2724. row < 0 &&
  2725. 2 = col &&
  2726. 2 = row &&
  2727. col <= 3 &&
  2728. col >= 0 &&
  2729. row < 3 &&
  2730. row >= 0 -> false
  2731.  
  2732. ### PCs: total:163 sat:54 unsat:109
  2733.  
  2734. numeric PC: constraint # = 7
  2735. row >= 3 &&
  2736. 2 = col &&
  2737. 2 = row &&
  2738. col <= 3 &&
  2739. col >= 0 &&
  2740. row < 3 &&
  2741. row >= 0 -> false
  2742.  
  2743. ### PCs: total:164 sat:54 unsat:110
  2744.  
  2745. numeric PC: constraint # = 6
  2746. col < 0 &&
  2747. 2 = row &&
  2748. col <= 3 &&
  2749. col >= 0 &&
  2750. row < 3 &&
  2751. row >= 0 -> false
  2752.  
  2753. ### PCs: total:165 sat:54 unsat:111
  2754.  
  2755. numeric PC: constraint # = 6
  2756. col >= 3 &&
  2757. 2 = row &&
  2758. col <= 3 &&
  2759. col >= 0 &&
  2760. row < 3 &&
  2761. row >= 0 -> true
  2762.  
  2763. ### PCs: total:166 sat:55 unsat:111
  2764.  
  2765. string analysis: SPC # = 0
  2766. NPC constraint # = 6
  2767. col >= 3 &&
  2768. 2 = row &&
  2769. col <= 3 &&
  2770. col >= 0 &&
  2771. row < 3 &&
  2772. row >= 0
  2773. numeric PC: constraint # = 6
  2774. col >= 3 &&
  2775. 2 = row &&
  2776. col <= 3 &&
  2777. col >= 0 &&
  2778. row < 3 &&
  2779. row >= 0 -> true
  2780.  
  2781. string analysis: SPC # = 0
  2782. NPC constraint # = 6
  2783. col >= 3 &&
  2784. 2 = row &&
  2785. col <= 3 &&
  2786. col >= 0 &&
  2787. row < 3 &&
  2788. row >= 0
  2789. Property Violated: PC is constraint # = 6
  2790. col >= 3 &&
  2791. 2 = row &&
  2792. col <= 3 &&
  2793. col >= 0 &&
  2794. row < 3 &&
  2795. row >= 0
  2796. Property Violated: result is "java.lang.ArrayIndexOutOfBoundsException..."
  2797. ****************************
  2798.  
  2799. ====================================================== error 3
  2800. gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
  2801. java.lang.ArrayIndexOutOfBoundsException
  2802. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90)
  2803. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  2804. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  2805.  
  2806.  
  2807. ====================================================== snapshot #3
  2808. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  2809. call stack:
  2810. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:90)
  2811. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  2812. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  2813.  
  2814.  
  2815. ====================================================== trace #3
  2816. ------------------------------------------------------ transition #0 thread: 0
  2817. gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"ROOT" ,1/1,isCascaded:false}
  2818. [3099 insn w/o sources]
  2819. TTTConsoleNonOO2P.java:23 : public static int[][] board = new int[ROWS][COLS]; // game board in 2D array
  2820. TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner
  2821. [5 insn w/o sources]
  2822. TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner
  2823. [4 insn w/o sources]
  2824. TTTConsoleNonOO2P.java:30 : public static Scanner in = new Scanner(System.in); // the input Scanner
  2825. TTTConsoleNonOO2P.java:1 : import java.util.Scanner;
  2826. [1 insn w/o sources]
  2827. TTTConsoleNonOO2P.java:35 : int row = 0;
  2828. TTTConsoleNonOO2P.java:37 : int col = 0;
  2829. TTTConsoleNonOO2P.java:39 : startGame(row, col);
  2830. ------------------------------------------------------ transition #1 thread: 0
  2831. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..0,delta=+1,cur=0]
  2832. TTTConsoleNonOO2P.java:39 : startGame(row, col);
  2833. TTTConsoleNonOO2P.java:44 : initGame();
  2834. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  2835. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2836. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  2837. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2838. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  2839. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2840. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  2841. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2842. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  2843. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2844. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  2845. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2846. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  2847. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2848. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  2849. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2850. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  2851. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2852. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  2853. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2854. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  2855. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2856. TTTConsoleNonOO2P.java:68 : board[row][col] = EMPTY; // all cells empty
  2857. TTTConsoleNonOO2P.java:67 : for (int col = 0; col < COLS; ++col) {
  2858. TTTConsoleNonOO2P.java:66 : for (int row = 0; row < ROWS; ++row) {
  2859. TTTConsoleNonOO2P.java:71 : currentState = PLAYING; // ready to play
  2860. TTTConsoleNonOO2P.java:72 : currentPlayer = CROSS; // cross plays first
  2861. TTTConsoleNonOO2P.java:73 : }
  2862. TTTConsoleNonOO2P.java:48 : playerMove(currentPlayer, row, col); // update currentRow and currentCol
  2863. TTTConsoleNonOO2P.java:78 : boolean validInput = false; // for input validation
  2864. TTTConsoleNonOO2P.java:80 : if (theSeed == CROSS) {
  2865. TTTConsoleNonOO2P.java:81 : System.out.print("Player 'X', enter your move (row[1-3] column[1-3]): ");
  2866. [2 insn w/o sources]
  2867. TTTConsoleNonOO2P.java:82 : } else {
  2868. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  2869. ------------------------------------------------------ transition #2 thread: 0
  2870. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  2871. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  2872. ------------------------------------------------------ transition #3 thread: 0
  2873. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  2874. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  2875. ------------------------------------------------------ transition #4 thread: 0
  2876. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  2877. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  2878. ------------------------------------------------------ transition #5 thread: 0
  2879. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..1,delta=+1,cur=0]
  2880. TTTConsoleNonOO2P.java:87 : if (row >= 0 && row < ROWS && col >= 0 && col <= COLS) {
  2881. TTTConsoleNonOO2P.java:88 : currntRow = row;
  2882. TTTConsoleNonOO2P.java:89 : currentCol = col;
  2883. TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content
  2884. ------------------------------------------------------ transition #6 thread: 0
  2885. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=2]
  2886. TTTConsoleNonOO2P.java:90 : board[currntRow][currentCol] = theSeed; // update game-board content
  2887. ------------------------------------------------------ transition #7 thread: 0
  2888. gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[id="?",isCascaded:false,0..4,delta=+1,cur=4]
  2889. numeric PC: constraint # = 5
  2890. row < 0 &&
  2891. col <= 3 &&
  2892. col >= 0 &&
  2893. row < 3 &&
  2894. row >= 0 -> false
  2895.  
  2896. ### PCs: total:167 sat:55 unsat:112
  2897.  
  2898. numeric PC: constraint # = 5
  2899. row >= 3 &&
  2900. col <= 3 &&
  2901. col >= 0 &&
  2902. row < 3 &&
  2903. row >= 0 -> false
  2904.  
  2905. ### PCs: total:168 sat:55 unsat:113
  2906.  
  2907. numeric PC: constraint # = 4
  2908. col > 3 &&
  2909. col >= 0 &&
  2910. row < 3 &&
  2911. row >= 0 -> true
  2912.  
  2913. ### PCs: total:169 sat:56 unsat:113
  2914.  
  2915. string analysis: SPC # = 0
  2916. NPC constraint # = 4
  2917. col > 3 &&
  2918. col >= 0 &&
  2919. row < 3 &&
  2920. row >= 0
  2921. This move at (0,0) is not valid. Try again...
  2922. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 4
  2923. col > 3 &&
  2924. col >= 0 &&
  2925. row < 3 &&
  2926. row >= 0 -> true
  2927.  
  2928. ### PCs: total:170 sat:57 unsat:113
  2929.  
  2930. string analysis: SPC # = 0
  2931. NPC constraint # = 4
  2932. col > 3 &&
  2933. col >= 0 &&
  2934. row < 3 &&
  2935. row >= 0
  2936. numeric PC: constraint # = 4
  2937. col > 3 &&
  2938. col >= 0 &&
  2939. row < 3 &&
  2940. row >= 0 -> true
  2941.  
  2942. ### PCs: total:171 sat:58 unsat:113
  2943.  
  2944. string analysis: SPC # = 0
  2945. NPC constraint # = 4
  2946. col > 3 &&
  2947. col >= 0 &&
  2948. row < 3 &&
  2949. row >= 0
  2950. numeric PC: constraint # = 4
  2951. col > 3 &&
  2952. col >= 0 &&
  2953. row < 3 &&
  2954. row >= 0 -> true
  2955.  
  2956. ### PCs: total:172 sat:59 unsat:113
  2957.  
  2958. string analysis: SPC # = 0
  2959. NPC constraint # = 4
  2960. col > 3 &&
  2961. col >= 0 &&
  2962. row < 3 &&
  2963. row >= 0
  2964. numeric PC: constraint # = 5
  2965. col <= 3 &&
  2966. col > 3 &&
  2967. col >= 0 &&
  2968. row < 3 &&
  2969. row >= 0 -> false
  2970.  
  2971. ### PCs: total:173 sat:59 unsat:114
  2972.  
  2973. numeric PC: constraint # = 4
  2974. col > 3 &&
  2975. col >= 0 &&
  2976. row < 3 &&
  2977. row >= 0 -> true
  2978.  
  2979. ### PCs: total:174 sat:60 unsat:114
  2980.  
  2981. string analysis: SPC # = 0
  2982. NPC constraint # = 4
  2983. col > 3 &&
  2984. col >= 0 &&
  2985. row < 3 &&
  2986. row >= 0
  2987. This move at (0,0) is not valid. Try again...
  2988. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 4
  2989. col > 3 &&
  2990. col >= 0 &&
  2991. row < 3 &&
  2992. row >= 0 -> true
  2993.  
  2994. ### PCs: total:175 sat:61 unsat:114
  2995.  
  2996. string analysis: SPC # = 0
  2997. NPC constraint # = 4
  2998. col > 3 &&
  2999. col >= 0 &&
  3000. row < 3 &&
  3001. row >= 0
  3002. numeric PC: constraint # = 4
  3003. col > 3 &&
  3004. col >= 0 &&
  3005. row < 3 &&
  3006. row >= 0 -> true
  3007.  
  3008. ### PCs: total:176 sat:62 unsat:114
  3009.  
  3010. string analysis: SPC # = 0
  3011. NPC constraint # = 4
  3012. col > 3 &&
  3013. col >= 0 &&
  3014. row < 3 &&
  3015. row >= 0
  3016.  
  3017. ====================================================== search constraint
  3018. depth limit reached: 12
  3019.  
  3020. ====================================================== snapshot
  3021. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  3022. call stack:
  3023. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  3024. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  3025. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  3026.  
  3027. numeric PC: constraint # = 5
  3028. row >= 3 &&
  3029. col > 3 &&
  3030. col >= 0 &&
  3031. row < 3 &&
  3032. row >= 0 -> false
  3033.  
  3034. ### PCs: total:177 sat:62 unsat:115
  3035.  
  3036.  
  3037. ====================================================== search constraint
  3038. depth limit reached: 12
  3039.  
  3040. ====================================================== snapshot
  3041. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  3042. call stack:
  3043. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:93)
  3044. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  3045. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  3046.  
  3047. numeric PC: constraint # = 5
  3048. row < 0 &&
  3049. col > 3 &&
  3050. col >= 0 &&
  3051. row < 3 &&
  3052. row >= 0 -> false
  3053.  
  3054. ### PCs: total:178 sat:62 unsat:116
  3055.  
  3056. numeric PC: constraint # = 5
  3057. col < 0 &&
  3058. col > 3 &&
  3059. col >= 0 &&
  3060. row < 3 &&
  3061. row >= 0 -> false
  3062.  
  3063. ### PCs: total:179 sat:62 unsat:117
  3064.  
  3065. numeric PC: constraint # = 5
  3066. row >= 3 &&
  3067. col > 3 &&
  3068. col >= 0 &&
  3069. row < 3 &&
  3070. row >= 0 -> false
  3071.  
  3072. ### PCs: total:180 sat:62 unsat:118
  3073.  
  3074. numeric PC: constraint # = 5
  3075. row < 0 &&
  3076. col > 3 &&
  3077. col >= 0 &&
  3078. row < 3 &&
  3079. row >= 0 -> false
  3080.  
  3081. ### PCs: total:181 sat:62 unsat:119
  3082.  
  3083. numeric PC: constraint # = 3
  3084. col < 0 &&
  3085. row < 3 &&
  3086. row >= 0 -> true
  3087.  
  3088. ### PCs: total:182 sat:63 unsat:119
  3089.  
  3090. string analysis: SPC # = 0
  3091. NPC constraint # = 3
  3092. col < 0 &&
  3093. row < 3 &&
  3094. row >= 0
  3095. This move at (0,0) is not valid. Try again...
  3096. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 3
  3097. col < 0 &&
  3098. row < 3 &&
  3099. row >= 0 -> true
  3100.  
  3101. ### PCs: total:183 sat:64 unsat:119
  3102.  
  3103. string analysis: SPC # = 0
  3104. NPC constraint # = 3
  3105. col < 0 &&
  3106. row < 3 &&
  3107. row >= 0
  3108. numeric PC: constraint # = 3
  3109. col < 0 &&
  3110. row < 3 &&
  3111. row >= 0 -> true
  3112.  
  3113. ### PCs: total:184 sat:65 unsat:119
  3114.  
  3115. string analysis: SPC # = 0
  3116. NPC constraint # = 3
  3117. col < 0 &&
  3118. row < 3 &&
  3119. row >= 0
  3120. numeric PC: constraint # = 4
  3121. col >= 0 &&
  3122. col < 0 &&
  3123. row < 3 &&
  3124. row >= 0 -> false
  3125.  
  3126. ### PCs: total:185 sat:65 unsat:120
  3127.  
  3128. numeric PC: constraint # = 3
  3129. col < 0 &&
  3130. row < 3 &&
  3131. row >= 0 -> true
  3132.  
  3133. ### PCs: total:186 sat:66 unsat:120
  3134.  
  3135. string analysis: SPC # = 0
  3136. NPC constraint # = 3
  3137. col < 0 &&
  3138. row < 3 &&
  3139. row >= 0
  3140. This move at (0,0) is not valid. Try again...
  3141. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 3
  3142. col < 0 &&
  3143. row < 3 &&
  3144. row >= 0 -> true
  3145.  
  3146. ### PCs: total:187 sat:67 unsat:120
  3147.  
  3148. string analysis: SPC # = 0
  3149. NPC constraint # = 3
  3150. col < 0 &&
  3151. row < 3 &&
  3152. row >= 0
  3153. numeric PC: constraint # = 3
  3154. col < 0 &&
  3155. row < 3 &&
  3156. row >= 0 -> true
  3157.  
  3158. ### PCs: total:188 sat:68 unsat:120
  3159.  
  3160. string analysis: SPC # = 0
  3161. NPC constraint # = 3
  3162. col < 0 &&
  3163. row < 3 &&
  3164. row >= 0
  3165. numeric PC: constraint # = 4
  3166. col >= 0 &&
  3167. col < 0 &&
  3168. row < 3 &&
  3169. row >= 0 -> false
  3170.  
  3171. ### PCs: total:189 sat:68 unsat:121
  3172.  
  3173. numeric PC: constraint # = 3
  3174. col < 0 &&
  3175. row < 3 &&
  3176. row >= 0 -> true
  3177.  
  3178. ### PCs: total:190 sat:69 unsat:121
  3179.  
  3180. string analysis: SPC # = 0
  3181. NPC constraint # = 3
  3182. col < 0 &&
  3183. row < 3 &&
  3184. row >= 0
  3185. This move at (0,0) is not valid. Try again...
  3186. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 3
  3187. col < 0 &&
  3188. row < 3 &&
  3189. row >= 0 -> true
  3190.  
  3191. ### PCs: total:191 sat:70 unsat:121
  3192.  
  3193. string analysis: SPC # = 0
  3194. NPC constraint # = 3
  3195. col < 0 &&
  3196. row < 3 &&
  3197. row >= 0
  3198.  
  3199. ====================================================== search constraint
  3200. depth limit reached: 12
  3201.  
  3202. ====================================================== snapshot
  3203. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  3204. call stack:
  3205. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  3206. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  3207. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  3208.  
  3209. numeric PC: constraint # = 4
  3210. row < 0 &&
  3211. col < 0 &&
  3212. row < 3 &&
  3213. row >= 0 -> false
  3214.  
  3215. ### PCs: total:192 sat:70 unsat:122
  3216.  
  3217.  
  3218. ====================================================== search constraint
  3219. depth limit reached: 12
  3220.  
  3221. ====================================================== snapshot
  3222. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  3223. call stack:
  3224. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:93)
  3225. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  3226. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  3227.  
  3228. numeric PC: constraint # = 4
  3229. row >= 3 &&
  3230. col < 0 &&
  3231. row < 3 &&
  3232. row >= 0 -> false
  3233.  
  3234. ### PCs: total:193 sat:70 unsat:123
  3235.  
  3236. numeric PC: constraint # = 4
  3237. row < 0 &&
  3238. col < 0 &&
  3239. row < 3 &&
  3240. row >= 0 -> false
  3241.  
  3242. ### PCs: total:194 sat:70 unsat:124
  3243.  
  3244. numeric PC: constraint # = 4
  3245. row >= 3 &&
  3246. col < 0 &&
  3247. row < 3 &&
  3248. row >= 0 -> false
  3249.  
  3250. ### PCs: total:195 sat:70 unsat:125
  3251.  
  3252. numeric PC: constraint # = 4
  3253. row < 0 &&
  3254. col < 0 &&
  3255. row < 3 &&
  3256. row >= 0 -> false
  3257.  
  3258. ### PCs: total:196 sat:70 unsat:126
  3259.  
  3260. numeric PC: constraint # = 2
  3261. row >= 3 &&
  3262. row >= 0 -> true
  3263.  
  3264. ### PCs: total:197 sat:71 unsat:126
  3265.  
  3266. string analysis: SPC # = 0
  3267. NPC constraint # = 2
  3268. row >= 3 &&
  3269. row >= 0
  3270. This move at (0,0) is not valid. Try again...
  3271. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3272. row >= 3 &&
  3273. row >= 0 -> true
  3274.  
  3275. ### PCs: total:198 sat:72 unsat:126
  3276.  
  3277. string analysis: SPC # = 0
  3278. NPC constraint # = 2
  3279. row >= 3 &&
  3280. row >= 0
  3281. numeric PC: constraint # = 3
  3282. row < 3 &&
  3283. row >= 3 &&
  3284. row >= 0 -> false
  3285.  
  3286. ### PCs: total:199 sat:72 unsat:127
  3287.  
  3288. numeric PC: constraint # = 2
  3289. row >= 3 &&
  3290. row >= 0 -> true
  3291.  
  3292. ### PCs: total:200 sat:73 unsat:127
  3293.  
  3294. string analysis: SPC # = 0
  3295. NPC constraint # = 2
  3296. row >= 3 &&
  3297. row >= 0
  3298. This move at (0,0) is not valid. Try again...
  3299. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3300. row >= 3 &&
  3301. row >= 0 -> true
  3302.  
  3303. ### PCs: total:201 sat:74 unsat:127
  3304.  
  3305. string analysis: SPC # = 0
  3306. NPC constraint # = 2
  3307. row >= 3 &&
  3308. row >= 0
  3309. numeric PC: constraint # = 3
  3310. row < 3 &&
  3311. row >= 3 &&
  3312. row >= 0 -> false
  3313.  
  3314. ### PCs: total:202 sat:74 unsat:128
  3315.  
  3316. numeric PC: constraint # = 2
  3317. row >= 3 &&
  3318. row >= 0 -> true
  3319.  
  3320. ### PCs: total:203 sat:75 unsat:128
  3321.  
  3322. string analysis: SPC # = 0
  3323. NPC constraint # = 2
  3324. row >= 3 &&
  3325. row >= 0
  3326. This move at (0,0) is not valid. Try again...
  3327. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3328. row >= 3 &&
  3329. row >= 0 -> true
  3330.  
  3331. ### PCs: total:204 sat:76 unsat:128
  3332.  
  3333. string analysis: SPC # = 0
  3334. NPC constraint # = 2
  3335. row >= 3 &&
  3336. row >= 0
  3337. numeric PC: constraint # = 3
  3338. row < 3 &&
  3339. row >= 3 &&
  3340. row >= 0 -> false
  3341.  
  3342. ### PCs: total:205 sat:76 unsat:129
  3343.  
  3344. numeric PC: constraint # = 2
  3345. row >= 3 &&
  3346. row >= 0 -> true
  3347.  
  3348. ### PCs: total:206 sat:77 unsat:129
  3349.  
  3350. string analysis: SPC # = 0
  3351. NPC constraint # = 2
  3352. row >= 3 &&
  3353. row >= 0
  3354. This move at (0,0) is not valid. Try again...
  3355. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3356. row >= 3 &&
  3357. row >= 0 -> true
  3358.  
  3359. ### PCs: total:207 sat:78 unsat:129
  3360.  
  3361. string analysis: SPC # = 0
  3362. NPC constraint # = 2
  3363. row >= 3 &&
  3364. row >= 0
  3365. numeric PC: constraint # = 3
  3366. row < 3 &&
  3367. row >= 3 &&
  3368. row >= 0 -> false
  3369.  
  3370. ### PCs: total:208 sat:78 unsat:130
  3371.  
  3372.  
  3373. ====================================================== search constraint
  3374. depth limit reached: 12
  3375.  
  3376. ====================================================== snapshot
  3377. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  3378. call stack:
  3379. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  3380. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  3381. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  3382.  
  3383. numeric PC: constraint # = 2
  3384. row >= 3 &&
  3385. row >= 0 -> true
  3386.  
  3387. ### PCs: total:209 sat:79 unsat:130
  3388.  
  3389. string analysis: SPC # = 0
  3390. NPC constraint # = 2
  3391. row >= 3 &&
  3392. row >= 0
  3393. This move at (0,0) is not valid. Try again...
  3394. Player 'X', enter your move (row[1-3] column[1-3]):
  3395. ====================================================== search constraint
  3396. depth limit reached: 12
  3397.  
  3398. ====================================================== snapshot
  3399. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  3400. call stack:
  3401. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  3402. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  3403. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  3404.  
  3405. numeric PC: constraint # = 3
  3406. row < 0 &&
  3407. row >= 3 &&
  3408. row >= 0 -> false
  3409.  
  3410. ### PCs: total:210 sat:79 unsat:131
  3411.  
  3412. numeric PC: constraint # = 3
  3413. row < 0 &&
  3414. row >= 3 &&
  3415. row >= 0 -> false
  3416.  
  3417. ### PCs: total:211 sat:79 unsat:132
  3418.  
  3419. numeric PC: constraint # = 3
  3420. row < 0 &&
  3421. row >= 3 &&
  3422. row >= 0 -> false
  3423.  
  3424. ### PCs: total:212 sat:79 unsat:133
  3425.  
  3426. numeric PC: constraint # = 3
  3427. row < 0 &&
  3428. row >= 3 &&
  3429. row >= 0 -> false
  3430.  
  3431. ### PCs: total:213 sat:79 unsat:134
  3432.  
  3433. numeric PC: constraint # = 1
  3434. row < 0 -> true
  3435.  
  3436. ### PCs: total:214 sat:80 unsat:134
  3437.  
  3438. string analysis: SPC # = 0
  3439. NPC constraint # = 1
  3440. row < 0
  3441. This move at (0,0) is not valid. Try again...
  3442. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3443. row >= 0 &&
  3444. row < 0 -> false
  3445.  
  3446. ### PCs: total:215 sat:80 unsat:135
  3447.  
  3448. numeric PC: constraint # = 1
  3449. row < 0 -> true
  3450.  
  3451. ### PCs: total:216 sat:81 unsat:135
  3452.  
  3453. string analysis: SPC # = 0
  3454. NPC constraint # = 1
  3455. row < 0
  3456. This move at (0,0) is not valid. Try again...
  3457. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3458. row >= 0 &&
  3459. row < 0 -> false
  3460.  
  3461. ### PCs: total:217 sat:81 unsat:136
  3462.  
  3463. numeric PC: constraint # = 1
  3464. row < 0 -> true
  3465.  
  3466. ### PCs: total:218 sat:82 unsat:136
  3467.  
  3468. string analysis: SPC # = 0
  3469. NPC constraint # = 1
  3470. row < 0
  3471. This move at (0,0) is not valid. Try again...
  3472. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3473. row >= 0 &&
  3474. row < 0 -> false
  3475.  
  3476. ### PCs: total:219 sat:82 unsat:137
  3477.  
  3478. numeric PC: constraint # = 1
  3479. row < 0 -> true
  3480.  
  3481. ### PCs: total:220 sat:83 unsat:137
  3482.  
  3483. string analysis: SPC # = 0
  3484. NPC constraint # = 1
  3485. row < 0
  3486. This move at (0,0) is not valid. Try again...
  3487. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3488. row >= 0 &&
  3489. row < 0 -> false
  3490.  
  3491. ### PCs: total:221 sat:83 unsat:138
  3492.  
  3493. numeric PC: constraint # = 1
  3494. row < 0 -> true
  3495.  
  3496. ### PCs: total:222 sat:84 unsat:138
  3497.  
  3498. string analysis: SPC # = 0
  3499. NPC constraint # = 1
  3500. row < 0
  3501. This move at (0,0) is not valid. Try again...
  3502. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3503. row >= 0 &&
  3504. row < 0 -> false
  3505.  
  3506. ### PCs: total:223 sat:84 unsat:139
  3507.  
  3508. numeric PC: constraint # = 1
  3509. row < 0 -> true
  3510.  
  3511. ### PCs: total:224 sat:85 unsat:139
  3512.  
  3513. string analysis: SPC # = 0
  3514. NPC constraint # = 1
  3515. row < 0
  3516. This move at (0,0) is not valid. Try again...
  3517. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3518. row >= 0 &&
  3519. row < 0 -> false
  3520.  
  3521. ### PCs: total:225 sat:85 unsat:140
  3522.  
  3523. numeric PC: constraint # = 1
  3524. row < 0 -> true
  3525.  
  3526. ### PCs: total:226 sat:86 unsat:140
  3527.  
  3528. string analysis: SPC # = 0
  3529. NPC constraint # = 1
  3530. row < 0
  3531. This move at (0,0) is not valid. Try again...
  3532. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3533. row >= 0 &&
  3534. row < 0 -> false
  3535.  
  3536. ### PCs: total:227 sat:86 unsat:141
  3537.  
  3538. numeric PC: constraint # = 1
  3539. row < 0 -> true
  3540.  
  3541. ### PCs: total:228 sat:87 unsat:141
  3542.  
  3543. string analysis: SPC # = 0
  3544. NPC constraint # = 1
  3545. row < 0
  3546. This move at (0,0) is not valid. Try again...
  3547. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3548. row >= 0 &&
  3549. row < 0 -> false
  3550.  
  3551. ### PCs: total:229 sat:87 unsat:142
  3552.  
  3553. numeric PC: constraint # = 1
  3554. row < 0 -> true
  3555.  
  3556. ### PCs: total:230 sat:88 unsat:142
  3557.  
  3558. string analysis: SPC # = 0
  3559. NPC constraint # = 1
  3560. row < 0
  3561. This move at (0,0) is not valid. Try again...
  3562. Player 'X', enter your move (row[1-3] column[1-3]): numeric PC: constraint # = 2
  3563. row >= 0 &&
  3564. row < 0 -> false
  3565.  
  3566. ### PCs: total:231 sat:88 unsat:143
  3567.  
  3568.  
  3569. ====================================================== search constraint
  3570. depth limit reached: 12
  3571.  
  3572. ====================================================== snapshot
  3573. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  3574. call stack:
  3575. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  3576. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  3577. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  3578.  
  3579. numeric PC: constraint # = 1
  3580. row < 0 -> true
  3581.  
  3582. ### PCs: total:232 sat:89 unsat:143
  3583.  
  3584. string analysis: SPC # = 0
  3585. NPC constraint # = 1
  3586. row < 0
  3587. This move at (0,0) is not valid. Try again...
  3588. Player 'X', enter your move (row[1-3] column[1-3]):
  3589. ====================================================== search constraint
  3590. depth limit reached: 12
  3591.  
  3592. ====================================================== snapshot
  3593. thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  3594. call stack:
  3595. at TTTConsoleNonOO2P.playerMove(TTTConsoleNonOO2P.java:87)
  3596. at TTTConsoleNonOO2P.startGame(TTTConsoleNonOO2P.java:48)
  3597. at TTTConsoleNonOO2P.main(TTTConsoleNonOO2P.java:39)
  3598.  
  3599.  
  3600. ====================================================== Method Summaries
  3601. Inputs: row,col
  3602.  
  3603. TTTConsoleNonOO2P.startGame() --> "java.lang.ArrayIndexOutOfBoundsException..."
  3604.  
  3605. ====================================================== Method Summaries (HTML)
  3606. <h1>Test Cases Generated by Symbolic JavaPath Finder for TTTConsoleNonOO2P.startGame (Path Coverage) </h1>
  3607. <table border=1>
  3608. <tr><td>row</td><td>col</td><td>RETURN</td></tr>
  3609. <tr><td>"java.lang.ArrayIndexOutOfBoundsException..."</td></tr>
  3610. </table>
  3611.  
  3612. ====================================================== results
  3613. error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArrayIndexOutOfBoundsException at TTTCo..."
  3614. error #2: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArrayIndexOutOfBoundsException at TTTCo..."
  3615. error #3: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArrayIndexOutOfBoundsException at TTTCo..."
  3616.  
  3617. ====================================================== statistics
  3618. elapsed time: 00:00:00
  3619. states: new=234,visited=0,backtracked=234,end=0
  3620. search: maxDepth=12,constraints=29
  3621. choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=75
  3622. heap: new=598,released=102,maxLive=369,gcCycles=65
  3623. instructions: 6307
  3624. max memory: 245MB
  3625. loaded code: classes=68,methods=1475
  3626.  
  3627. ====================================================== search finished: 7/10/17 2:23 AM
Advertisement
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!