У кого-нибудь есть код для головоломки «Четыре рыцаря», написанный на smv (nusmv или nuxmv)? Я описываю проблему с сеткой, но когда я пытался написать ограничения/ходы, я получил ошибки, такие как:
строка 35: определено рекурсивно: S1
в определении next(S3) в строке 43
в определении next(S1) в строке 35
Я понимаю эту проблему, но не знаю, как я могу реализовать эту проблему и избежать этого рекурсивно.
Спасибо!
ну наконец-то у меня получилось самостоятельно (применил выигрышную стратегию для черных, для ситуаций, в которых он должен был выиграть):
MODULE main
VAR
vec : {v1234, v1236, v1246, v1237, v1247, v1267, v1238, v1248, v1268, v1278, v1239, v1249, v1269, v1279, v1289, v1324, v1326, v1346, v1327, v1347, v1367, v1328, v1348, v1368, v1378, v1329, v1349, v1369, v1379, v1389, v2314, v2316, v2346, v2317, v2347, v2367, v2318, v2348, v2368, v2378, v2319, v2349, v2369, v2379, v2389, v1423, v1426, v1436, v1427, v1437, v1467, v1428, v1438, v1468, v1478, v1429, v1439, v1469, v1479, v1489, v2413, v2416, v2436, v2417, v2437, v2467, v2418, v2438, v2468, v2478, v2419, v2439, v2469, v2479, v2489, v3412, v3416, v3426, v3417, v3427, v3467, v3418, v3428, v3468, v3478, v3419, v3429, v3469, v3479, v3489, v1623, v1624, v1634, v1627, v1637, v1647, v1628, v1638, v1648, v1678, v1629, v1639, v1649, v1679, v1689, v2613, v2614, v2634, v2617, v2637, v2647, v2618, v2638, v2648, v2678, v2619, v2639, v2649, v2679, v2689, v3612, v3614, v3624, v3617, v3627, v3647, v3618, v3628, v3648, v3678, v3619, v3629, v3649, v3679, v3689, v4612, v4613, v4623, v4617, v4627, v4637, v4618, v4628, v4638, v4678, v4619, v4629, v4639, v4679, v4689, v1723, v1724, v1734, v1726, v1736, v1746, v1728, v1738, v1748, v1768, v1729, v1739, v1749, v1769, v1789, v2713, v2714, v2734, v2716, v2736, v2746, v2718, v2738, v2748, v2768, v2719, v2739, v2749, v2769, v2789, v3712, v3714, v3724, v3716, v3726, v3746, v3718, v3728, v3748, v3768, v3719, v3729, v3749, v3769, v3789, v4712, v4713, v4723, v4716, v4726, v4736, v4718, v4728, v4738, v4768, v4719, v4729, v4739, v4769, v4789, v6712, v6713, v6723, v6714, v6724, v6734, v6718, v6728, v6738, v6748, v6719, v6729, v6739, v6749, v6789, v1823, v1824, v1834, v1826, v1836, v1846, v1827, v1837, v1847, v1867, v1829, v1839, v1849, v1869, v1879, v2813, v2814, v2834, v2816, v2836, v2846, v2817, v2837, v2847, v2867, v2819, v2839, v2849, v2869, v2879, v3812, v3814, v3824, v3816, v3826, v3846, v3817, v3827, v3847, v3867, v3819, v3829, v3849, v3869, v3879, v4812, v4813, v4823, v4816, v4826, v4836, v4817, v4827, v4837, v4867, v4819, v4829, v4839, v4869, v4879, v6812, v6813, v6823, v6814, v6824, v6834, v6817, v6827, v6837, v6847, v6819, v6829, v6839, v6849, v6879, v7812, v7813, v7823, v7814, v7824, v7834, v7816, v7826, v7836, v7846, v7819, v7829, v7839, v7849, v7869, v1923, v1924, v1934, v1926, v1936, v1946, v1927, v1937, v1947, v1967, v1928, v1938, v1948, v1968, v1978, v2913, v2914, v2934, v2916, v2936, v2946, v2917, v2937, v2947, v2967, v2918, v2938, v2948, v2968, v2978, v3912, v3914, v3924, v3916, v3926, v3946, v3917, v3927, v3947, v3967, v3918, v3928, v3948, v3968, v3978, v4912, v4913, v4923, v4916, v4926, v4936, v4917, v4927, v4937, v4967, v4918, v4928, v4938, v4968, v4978, v6912, v6913, v6923, v6914, v6924, v6934, v6917, v6927, v6937, v6947, v6918, v6928, v6938, v6948, v6978, v7912, v7913, v7923, v7914, v7924, v7934, v7916, v7926, v7936, v7946, v7918, v7928, v7938, v7948, v7968, v8912, v8913, v8923, v8914, v8924, v8934, v8916, v8926, v8936, v8946, v8917, v8927, v8937, v8947, v8967, 0, 5};
player : {W, B};
-- 0 = BLACK WIN, 5 = WHITE WIN
ASSIGN
init(player) := B;
next(player) := case
player = W : B;
player = B : W;
esac;
init(vec) := {v1248, v1239, v1327, v1347, v1367, v1329, v1349, v1369, v2317, v2368, v1426, v1479, v2416, v2436, v2467, v2418, v2438, v2478, v3426, v3417, v3428, v3468, v3419, v3479, v1624, v1637, v1628, v1648, v1639, v1679, v2614, v2634, v2618, v2638, v2649, v2689, v3624, v3679, v4627, v4618, v4638, v4629, v1723, v1734, v1738, v1729, v1749, v1789, v2713, v2746, v2748, v2768, v2719, v2739, v3716, v3718, v3729, v3749, v4713, v4768, v6713, v6724, v6728, v6748, v6719, v6739, v1824, v1826, v1846, v1837, v1839, v1879, v2834, v2816, v2867, v2849, v3824, v3826, v3846, v3817, v3819, v3879, v4812, v4816, v4827, v4867, v4829, v4869, v6823, v6834, v6827, v6847, v6829, v6849, v7824, v7839, v1934, v1927, v1967, v1938, v2913, v2946, v2917, v2937, v2948, v2968, v3912, v3916, v3927, v3967, v3918, v3978, v4913, v4926, v4917, v4937, v4928, v4968, v6913, v6948, v7914, v7934, v7916, v7936, v7918, v7938, v8926, v8917};
next(vec) := case
player = B & vec = v1234: {v1248, v1239};
player = B & vec = v1236: {v1246, v1268, v1237};
player = B & vec = v1246: {v1236, v1269, v1247};
player = B & vec = v1237: {v1247, v1278, v1236};
player = B & vec = v1247: {v1237, v1279, v1246};
player = B & vec = v1267: {5};
player = B & vec = v1238: {v1248};
player = B & vec = v1248: {v1289};
player = B & vec = v1268: {v1278, v1236};
player = B & vec = v1278: {v1268, v1237};
player = B & vec = v1239: {v1289};
player = B & vec = v1249: {v1239};
player = B & vec = v1269: {v1279, v1246};
player = B & vec = v1279: {v1269, v1247};
player = B & vec = v1289: {v1239, v1248};
player = B & vec = v1324: {v1347, v1349, v1329};
player = B & vec = v1326: {v1367, v1369, v1327};
player = B & vec = v1346: {v1369, v1347};
player = B & vec = v1327: {v1379};
player = B & vec = v1347: {v1346};
player = B & vec = v1367: {v1326};
player = B & vec = v1328: {v1378, v1389};
player = B & vec = v1348: {v1389};
player = B & vec = v1368: {v1378};
player = B & vec = v1378: {v1328, v1368};
player = B & vec = v1329: {v1379};
player = B & vec = v1349: {v1324};
player = B & vec = v1369: {v1346};
player = B & vec = v1379: {v1329, v1369, v1327, v1347};
player = B & vec = v1389: {v1328, v1348};
player = B & vec = v2314: {v2346, v2348, v2319};
player = B & vec = v2316: {v2368, v2317};
player = B & vec = v2346: {v2369, v2314, v2347};
player = B & vec = v2317: {v2378};
player = B & vec = v2347: {v2379, v2346};
player = B & vec = v2367: {v2317};
player = B & vec = v2318: {v2368};
player = B & vec = v2348: {v2389, v2314};
player = B & vec = v2368: {v2378};
player = B & vec = v2378: {v2368, v2317};
player = B & vec = v2319: {v2369, v2389, v2314};
player = B & vec = v2349: {5};
player = B & vec = v2369: {v2319, v2379, v2346};
player = B & vec = v2379: {v2369, v2347};
player = B & vec = v2389: {v2319, v2348};
player = B & vec = v1423: {v1437, v1439, v1428};
player = B & vec = v1426: {v1469};
player = B & vec = v1436: {v1468, v1437};
player = B & vec = v1427: {v1479, v1426};
player = B & vec = v1437: {v1478, v1423, v1436};
player = B & vec = v1467: {v1426};
player = B & vec = v1428: {v1478, v1489, v1423};
player = B & vec = v1438: {5};
player = B & vec = v1468: {v1478, v1436};
player = B & vec = v1478: {v1428, v1468, v1437};
player = B & vec = v1429: {v1479};
player = B & vec = v1439: {v1489, v1423};
player = B & vec = v1469: {v1479, v1426};
player = B & vec = v1479: {v1469};
player = B & vec = v1489: {v1439, v1428};
player = B & vec = v2413: {v2436, v2438, v2418};
player = B & vec = v2416: {v2468};
player = B & vec = v2436: {v2437};
player = B & vec = v2417: {v2467, v2478, v2416};
player = B & vec = v2437: {v2478, v2436};
player = B & vec = v2467: {v2417};
player = B & vec = v2418: {v2468};
player = B & vec = v2438: {v2413};
player = B & vec = v2468: {v2418, v2478, v2416, v2436};
player = B & vec = v2478: {v2437};
player = B & vec = v2419: {v2469, v2489};
player = B & vec = v2439: {v2489};
player = B & vec = v2469: {v2419, v2479};
player = B & vec = v2479: {v2469};
player = B & vec = v2489: {v2419, v2439};
player = B & vec = v3412: {v3426, v3428, v3417, v3419};
player = B & vec = v3416: {v3468, v3417};
player = B & vec = v3426: {v3469};
player = B & vec = v3417: {v3478};
player = B & vec = v3427: {v3479, v3426};
player = B & vec = v3467: {v3417, v3426};
player = B & vec = v3418: {v3468};
player = B & vec = v3428: {v3489};
player = B & vec = v3468: {v3478};
player = B & vec = v3478: {v3428, v3468, v3417};
player = B & vec = v3419: {v3489};
player = B & vec = v3429: {v3479};
player = B & vec = v3469: {v3419, v3479, v3426};
player = B & vec = v3479: {v3469};
player = B & vec = v3489: {v3419, v3428};
player = B & vec = v1623: {v1637, v1639, v1624, v1628};
player = B & vec = v1624: {v1647};
player = B & vec = v1634: {v1648, v1639};
player = B & vec = v1627: {v1679};
player = B & vec = v1637: {v1678};
player = B & vec = v1647: {v1637, v1679, v1624};
player = B & vec = v1628: {v1678};
player = B & vec = v1638: {v1648};
player = B & vec = v1648: {v1689};
player = B & vec = v1678: {v1628, v1637};
player = B & vec = v1629: {v1679, v1624};
player = B & vec = v1639: {v1689};
player = B & vec = v1649: {v1639, v1624};
player = B & vec = v1679: {v1647};
player = B & vec = v1689: {v1639, v1628, v1648};
player = B & vec = v2613: {v2638, v2614, v2618};
player = B & vec = v2614: {v2619};
player = B & vec = v2634: {v2648};
player = B & vec = v2617: {v2678};
player = B & vec = v2637: {v2647, v2678};
player = B & vec = v2647: {v2637, v2679};
player = B & vec = v2618: {v2613};
player = B & vec = v2638: {v2648};
player = B & vec = v2648: {v2638, v2689, v2614, v2634};
player = B & vec = v2678: {v2617, v2637};
player = B & vec = v2619: {v2689, v2614};
player = B & vec = v2639: {v2649, v2689, v2634};
player = B & vec = v2649: {v2639};
player = B & vec = v2679: {v2647};
player = B & vec = v2689: {v2619};
player = B & vec = v3612: {v3628, v3617, v3619};
player = B & vec = v3614: {v3648, v3619};
player = B & vec = v3624: {v3647};
player = B & vec = v3617: {v3678, v3612};
player = B & vec = v3627: {v3679};
player = B & vec = v3647: {v3679, v3624};
player = B & vec = v3618: {5};
player = B & vec = v3628: {v3678, v3689, v3612};
player = B & vec = v3648: {v3689, v3614};
player = B & vec = v3678: {v3628, v3617};
player = B & vec = v3619: {v3689, v3612, v3614};
player = B & vec = v3629: {v3679, v3624};
player = B & vec = v3649: {v3624};
player = B & vec = v3679: {v3647};
player = B & vec = v3689: {v3619, v3628, v3648};
player = B & vec = v4612: {v4628, v4617, v4619};
player = B & vec = v4613: {v4638, v4618};
player = B & vec = v4623: {v4637, v4639, v4628};
player = B & vec = v4617: {v4678, v4612};
player = B & vec = v4627: {v4679};
player = B & vec = v4637: {v4678, v4623};
player = B & vec = v4618: {v4613};
player = B & vec = v4628: {v4678, v4689, v4612, v4623};
player = B & vec = v4638: {v4613};
player = B & vec = v4678: {v4628, v4617, v4637};
player = B & vec = v4619: {v4689, v4612};
player = B & vec = v4629: {v4679};
player = B & vec = v4639: {v4689, v4623};
player = B & vec = v4679: {v4629, v4627};
player = B & vec = v4689: {v4619, v4639, v4628};
player = B & vec = v1723: {v1728};
player = B & vec = v1724: {v1749, v1723, v1729};
player = B & vec = v1734: {v1739};
player = B & vec = v1726: {v1769};
player = B & vec = v1736: {v1746, v1768};
player = B & vec = v1746: {v1736, v1769};
player = B & vec = v1728: {v1789, v1723};
player = B & vec = v1738: {v1748};
player = B & vec = v1748: {v1738, v1789, v1734};
player = B & vec = v1768: {v1736};
player = B & vec = v1729: {v1724};
player = B & vec = v1739: {v1749, v1789, v1723, v1734};
player = B & vec = v1749: {v1739};
player = B & vec = v1769: {v1726, v1746};
player = B & vec = v1789: {v1728};
player = B & vec = v2713: {v2736};
player = B & vec = v2714: {v2746, v2748, v2713, v2719};
player = B & vec = v2734: {v2748, v2739};
player = B & vec = v2716: {v2768};
player = B & vec = v2736: {v2746, v2768, v2713};
player = B & vec = v2746: {v2769};
player = B & vec = v2718: {v2768, v2713};
player = B & vec = v2738: {v2748, v2713};
player = B & vec = v2748: {v2789};
player = B & vec = v2768: {v2736};
player = B & vec = v2719: {v2769};
player = B & vec = v2739: {v2789};
player = B & vec = v2749: {v2739};
player = B & vec = v2769: {v2719, v2746};
player = B & vec = v2789: {v2719, v2739, v2748};
player = B & vec = v3712: {v3726, v3728, v3719};
player = B & vec = v3714: {v3746, v3748, v3719};
player = B & vec = v3724: {v3749, v3729};
player = B & vec = v3716: {v3768};
player = B & vec = v3726: {v3769, v3712};
player = B & vec = v3746: {v3769, v3714};
player = B & vec = v3718: {v3768};
player = B & vec = v3728: {v3789, v3712};
player = B & vec = v3748: {v3789, v3714};
player = B & vec = v3768: {v3718, v3716};
player = B & vec = v3719: {v3769, v3789, v3712, v3714};
player = B & vec = v3729: {v3724};
player = B & vec = v3749: {v3724};
player = B & vec = v3769: {v3719, v3726, v3746};
player = B & vec = v3789: {v3719, v3728, v3748};
player = B & vec = v4712: {v4726, v4728, v4719};
player = B & vec = v4713: {v4736};
player = B & vec = v4723: {v4739, v4728};
player = B & vec = v4716: {v4768};
player = B & vec = v4726: {v4769, v4712};
player = B & vec = v4736: {v4768, v4713};
player = B & vec = v4718: {v4768, v4713};
player = B & vec = v4728: {v4789, v4712, v4723};
player = B & vec = v4738: {v4713};
player = B & vec = v4768: {v4736};
player = B & vec = v4719: {v4769, v4789, v4712};
player = B & vec = v4729: {5};
player = B & vec = v4739: {v4789, v4723};
player = B & vec = v4769: {v4719, v4726};
player = B & vec = v4789: {v4719, v4739, v4728};
player = B & vec = v6712: {v6728, v6719};
player = B & vec = v6713: {v6714};
player = B & vec = v6723: {v6739, v6724, v6728};
player = B & vec = v6714: {v6748, v6713, v6719};
player = B & vec = v6724: {v6723};
player = B & vec = v6734: {v6748, v6739};
player = B & vec = v6718: {v6713};
player = B & vec = v6728: {v6712};
player = B & vec = v6738: {v6748, v6713};
player = B & vec = v6748: {v6714};
player = B & vec = v6719: {v6712};
player = B & vec = v6729: {v6724};
player = B & vec = v6739: {v6723};
player = B & vec = v6749: {v6739, v6724};
player = B & vec = v6789: {v6719, v6739, v6728, v6748};
player = B & vec = v1823: {v1837, v1839, v1824};
player = B & vec = v1824: {v1823};
player = B & vec = v1834: {v1839};
player = B & vec = v1826: {v1869};
player = B & vec = v1836: {v1846, v1837};
player = B & vec = v1846: {v1836};
player = B & vec = v1827: {v1879, v1826};
player = B & vec = v1837: {v1836};
player = B & vec = v1847: {v1837, v1879, v1824, v1846};
player = B & vec = v1867: {v1826};
player = B & vec = v1829: {v1879, v1824};
player = B & vec = v1839: {v1823};
player = B & vec = v1849: {v1839, v1824};
player = B & vec = v1869: {v1879, v1826, v1846};
player = B & vec = v1879: {v1869};
player = B & vec = v2813: {v2836, v2814};
player = B & vec = v2814: {v2846, v2813, v2819};
player = B & vec = v2834: {v2839};
player = B & vec = v2816: {v2817};
player = B & vec = v2836: {v2846, v2813, v2837};
player = B & vec = v2846: {v2836, v2869, v2814, v2847};
player = B & vec = v2817: {v2867, v2816};
player = B & vec = v2837: {v2847, v2836};
player = B & vec = v2847: {v2837, v2879, v2846};
player = B & vec = v2867: {v2817};
player = B & vec = v2819: {v2869, v2814};
player = B & vec = v2839: {v2849, v2834};
player = B & vec = v2849: {v2839};
player = B & vec = v2869: {v2819, v2879, v2846};
player = B & vec = v2879: {v2869, v2847};
player = B & vec = v3812: {v3826, v3817, v3819};
player = B & vec = v3814: {v3846, v3819};
player = B & vec = v3824: {v3847};
player = B & vec = v3816: {v3817};
player = B & vec = v3826: {v3812};
player = B & vec = v3846: {v3814};
player = B & vec = v3817: {v3812};
player = B & vec = v3827: {v3879, v3826};
player = B & vec = v3847: {v3879, v3824, v3846};
player = B & vec = v3867: {v3817, v3826};
player = B & vec = v3819: {v3814};
player = B & vec = v3829: {v3879, v3824};
player = B & vec = v3849: {v3824};
player = B & vec = v3869: {v3819, v3879, v3826, v3846};
player = B & vec = v3879: {v3847};
player = B & vec = v4812: {v4819};
player = B & vec = v4813: {v4836};
player = B & vec = v4823: {v4837};
player = B & vec = v4816: {v4817};
player = B & vec = v4826: {v4867, v4869, v4812, v4827};
player = B & vec = v4836: {v4813, v4837};
player = B & vec = v4817: {v4867, v4812, v4816};
player = B & vec = v4827: {v4826};
player = B & vec = v4837: {v4823, v4836};
player = B & vec = v4867: {v4826};
player = B & vec = v4819: {v4869, v4812};
player = B & vec = v4829: {v4879};
player = B & vec = v4839: {v4823};
player = B & vec = v4869: {v4819};
player = B & vec = v4879: {v4829, v4869, v4827};
player = B & vec = v6812: {v6817, v6819};
player = B & vec = v6813: {v6814};
player = B & vec = v6823: {v6837};
player = B & vec = v6814: {v6813, v6819};
player = B & vec = v6824: {v6847, v6849, v6823, v6829};
player = B & vec = v6834: {v6839};
player = B & vec = v6817: {v6812};
player = B & vec = v6827: {v6879};
player = B & vec = v6837: {v6847, v6823};
player = B & vec = v6847: {v6837};
player = B & vec = v6819: {v6812, v6814};
player = B & vec = v6829: {v6824};
player = B & vec = v6839: {v6849, v6823, v6834};
player = B & vec = v6849: {v6824};
player = B & vec = v6879: {v6829, v6827, v6847};
player = B & vec = v7812: {v7826, v7819};
player = B & vec = v7813: {v7836, v7814};
player = B & vec = v7823: {v7839, v7824};
player = B & vec = v7814: {v7846, v7813, v7819};
player = B & vec = v7824: {v7823};
player = B & vec = v7834: {v7839};
player = B & vec = v7816: {5};
player = B & vec = v7826: {v7869, v7812};
player = B & vec = v7836: {v7846, v7813};
player = B & vec = v7846: {v7836, v7869, v7814};
player = B & vec = v7819: {v7869, v7812, v7814};
player = B & vec = v7829: {v7824};
player = B & vec = v7839: {v7823};
player = B & vec = v7849: {v7839, v7824};
player = B & vec = v7869: {v7819, v7826, v7846};
player = B & vec = v1923: {v1937, v1924, v1928};
player = B & vec = v1924: {v1947, v1923};
player = B & vec = v1934: {v1948};
player = B & vec = v1926: {v1967, v1927};
player = B & vec = v1936: {v1946, v1968, v1937};
player = B & vec = v1946: {v1936, v1947};
player = B & vec = v1927: {v1926};
player = B & vec = v1937: {v1947, v1978, v1923, v1936};
player = B & vec = v1947: {v1937, v1924, v1946};
player = B & vec = v1967: {v1926};
player = B & vec = v1928: {v1978, v1923};
player = B & vec = v1938: {v1948};
player = B & vec = v1948: {v1938, v1934};
player = B & vec = v1968: {v1978, v1936};
player = B & vec = v1978: {v1928, v1968, v1937};
player = B & vec = v2913: {v2914};
player = B & vec = v2914: {v2946, v2948, v2913};
player = B & vec = v2934: {v2948};
player = B & vec = v2916: {v2968, v2917};
player = B & vec = v2936: {v2946, v2968, v2913, v2937};
player = B & vec = v2946: {v2947};
player = B & vec = v2917: {v2978};
player = B & vec = v2937: {v2947};
player = B & vec = v2947: {v2937, v2946};
player = B & vec = v2967: {v2917};
player = B & vec = v2918: {v2968, v2913};
player = B & vec = v2938: {v2948, v2913};
player = B & vec = v2948: {v2914};
player = B & vec = v2968: {v2978};
player = B & vec = v2978: {v2968, v2917, v2937};
player = B & vec = v3912: {v3928};
player = B & vec = v3914: {v3946, v3948};
player = B & vec = v3924: {v3947};
player = B & vec = v3916: {v3917};
player = B & vec = v3926: {v3967, v3912, v3927};
player = B & vec = v3946: {v3914, v3947};
player = B & vec = v3917: {v3967, v3978, v3912, v3916};
player = B & vec = v3927: {v3926};
player = B & vec = v3947: {v3924, v3946};
player = B & vec = v3967: {v3917};
player = B & vec = v3918: {v3968};
player = B & vec = v3928: {v3978, v3912};
player = B & vec = v3948: {v3914};
player = B & vec = v3968: {v3918, v3978, v3916};
player = B & vec = v3978: {v3928};
player = B & vec = v4912: {v4926, v4928, v4917};
player = B & vec = v4913: {v4936};
player = B & vec = v4923: {v4937, v4928};
player = B & vec = v4916: {v4968, v4917};
player = B & vec = v4926: {v4912};
player = B & vec = v4936: {v4968, v4913, v4937};
player = B & vec = v4917: {v4912};
player = B & vec = v4927: {v4926};
player = B & vec = v4937: {v4923};
player = B & vec = v4967: {v4917, v4926};
player = B & vec = v4918: {v4968, v4913};
player = B & vec = v4928: {v4923};
player = B & vec = v4938: {v4913};
player = B & vec = v4968: {v4936};
player = B & vec = v4978: {v4928, v4968, v4917, v4937};
player = B & vec = v6912: {v6928, v6917};
player = B & vec = v6913: {v6914};
player = B & vec = v6923: {v6937, v6924, v6928};
player = B & vec = v6914: {v6948, v6913};
player = B & vec = v6924: {v6947, v6923};
player = B & vec = v6934: {v6948};
player = B & vec = v6917: {v6978, v6912};
player = B & vec = v6927: {5};
player = B & vec = v6937: {v6947, v6978, v6923};
player = B & vec = v6947: {v6937, v6924};
player = B & vec = v6918: {v6913};
player = B & vec = v6928: {v6978, v6912, v6923};
player = B & vec = v6938: {v6948, v6913};
player = B & vec = v6948: {v6914};
player = B & vec = v6978: {v6928, v6917, v6937};
player = B & vec = v7912: {v7926, v7928};
player = B & vec = v7913: {v7936, v7938, v7914, v7918};
player = B & vec = v7923: {v7924, v7928};
player = B & vec = v7914: {v7946};
player = B & vec = v7924: {v7923};
player = B & vec = v7934: {v7948};
player = B & vec = v7916: {v7968};
player = B & vec = v7926: {v7912};
player = B & vec = v7936: {v7946};
player = B & vec = v7946: {v7936, v7914};
player = B & vec = v7918: {v7913};
player = B & vec = v7928: {v7912, v7923};
player = B & vec = v7938: {v7913};
player = B & vec = v7948: {v7938, v7914, v7934};
player = B & vec = v7968: {v7918, v7916, v7936};
player = B & vec = v8912: {v8926, v8917};
player = B & vec = v8913: {v8936, v8914};
player = B & vec = v8923: {v8937, v8924};
player = B & vec = v8914: {v8946, v8913};
player = B & vec = v8924: {v8947, v8923};
player = B & vec = v8934: {5};
player = B & vec = v8916: {v8917};
player = B & vec = v8926: {v8912};
player = B & vec = v8936: {v8946, v8913, v8937};
player = B & vec = v8946: {v8936, v8914, v8947};
player = B & vec = v8917: {v8912};
player = B & vec = v8927: {v8926};
player = B & vec = v8937: {v8947, v8923, v8936};
player = B & vec = v8947: {v8937, v8924, v8946};
player = B & vec = v8967: {v8917, v8926};
TRUE : vec;
esac;
Проверка LTL (0 означает, что черный — победитель):
check_ltlspec -p "F ((vec = 0) & (player = B))"
и получил:
-- спецификация F (vec = 0 и player = B) верна
В прошлом комментарии я написал черную стратегию. это белые варианты (все варианты перемещения для каждой позиции):
player = W & vec = v1234: {v2634,v2834,v1734,v1934};
player = W & vec = v1236: {v2836,v1736,v1936};
player = W & vec = v1246: {v2846,v1746,v1946};
player = W & vec = v1237: {v2637,v2837,v1937};
player = W & vec = v1247: {v2647,v2847,v1947};
player = W & vec = v1267: {v2867,v1967};
player = W & vec = v1238: {v2638,v1738,v1938};
player = W & vec = v1248: {v2648,v1748,v1948};
player = W & vec = v1268: {v1768,v1968};
player = W & vec = v1278: {v2678,v1978};
player = W & vec = v1239: {v2639,v2839,v1739};
player = W & vec = v1249: {v2649,v2849,v1749};
player = W & vec = v1269: {v2869,v1769};
player = W & vec = v1279: {v2679,v2879};
player = W & vec = v1289: {v2689,v1789};
player = W & vec = v1324: {v3624,v3824,v1824};
player = W & vec = v1326: {v3826,v1426,v1826};
player = W & vec = v1346: {v3846,v1846};
player = W & vec = v1327: {v3627,v3827,v1427,v1827};
player = W & vec = v1347: {v3647,v3847,v1847};
player = W & vec = v1367: {v3867,v1467,v1867};
player = W & vec = v1328: {v3628,v1428};
player = W & vec = v1348: {v3648};
player = W & vec = v1368: {v1468};
player = W & vec = v1378: {v3678,v1478};
player = W & vec = v1329: {v3629,v3829,v1429,v1829};
player = W & vec = v1349: {v3649,v3849,v1849};
player = W & vec = v1369: {v3869,v1469,v1869};
player = W & vec = v1379: {v3679,v3879,v1479,v1879};
player = W & vec = v1389: {v3689,v1489};
player = W & vec = v2314: {v3714,v3914,v2814};
player = W & vec = v2316: {v3716,v3916,v2416,v2816};
player = W & vec = v2346: {v3746,v3946,v2846};
player = W & vec = v2317: {v3917,v2417,v2817};
player = W & vec = v2347: {v3947,v2847};
player = W & vec = v2367: {v3967,v2467,v2867};
player = W & vec = v2318: {v3718,v3918,v2418};
player = W & vec = v2348: {v3748,v3948};
player = W & vec = v2368: {v3768,v3968,v2468};
player = W & vec = v2378: {v3978,v2478};
player = W & vec = v2319: {v3719,v2419,v2819};
player = W & vec = v2349: {v3749,v2849};
player = W & vec = v2369: {v3769,v2469,v2869};
player = W & vec = v2379: {v2479,v2879};
player = W & vec = v2389: {v3789,v2489};
player = W & vec = v1423: {v4623,v4823,v1923};
player = W & vec = v1426: {v4826,v1326,v1926};
player = W & vec = v1436: {v4836,v1936};
player = W & vec = v1427: {v4627,v4827,v1327,v1927};
player = W & vec = v1437: {v4637,v4837,v1937};
player = W & vec = v1467: {v4867,v1367,v1967};
player = W & vec = v1428: {v4628,v1328,v1928};
player = W & vec = v1438: {v4638,v1938};
player = W & vec = v1468: {v1368,v1968};
player = W & vec = v1478: {v4678,v1378,v1978};
player = W & vec = v1429: {v4629,v4829,v1329};
player = W & vec = v1439: {v4639,v4839};
player = W & vec = v1469: {v4869,v1369};
player = W & vec = v1479: {v4679,v4879,v1379};
player = W & vec = v1489: {v4689,v1389};
player = W & vec = v2413: {v4713,v4913,v2913};
player = W & vec = v2416: {v4716,v4916,v2316,v2916};
player = W & vec = v2436: {v4736,v4936,v2936};
player = W & vec = v2417: {v4917,v2317,v2917};
player = W & vec = v2437: {v4937,v2937};
player = W & vec = v2467: {v4967,v2367,v2967};
player = W & vec = v2418: {v4718,v4918,v2318,v2918};
player = W & vec = v2438: {v4738,v4938,v2938};
player = W & vec = v2468: {v4768,v4968,v2368,v2968};
player = W & vec = v2478: {v4978,v2378,v2978};
player = W & vec = v2419: {v4719,v2319};
player = W & vec = v2439: {v4739};
player = W & vec = v2469: {v4769,v2369};
player = W & vec = v2479: {v2379};
player = W & vec = v2489: {v4789,v2389};
player = W & vec = v3412: {v4812,v3912};
player = W & vec = v3416: {v4816,v3916};
player = W & vec = v3426: {v4826,v3926};
player = W & vec = v3417: {v4817,v3917};
player = W & vec = v3427: {v4827,v3927};
player = W & vec = v3467: {v4867,v3967};
player = W & vec = v3418: {v3918};
player = W & vec = v3428: {v3928};
player = W & vec = v3468: {v3968};
player = W & vec = v3478: {v3978};
player = W & vec = v3419: {v4819};
player = W & vec = v3429: {v4829};
player = W & vec = v3469: {v4869};
player = W & vec = v3479: {v4879};
player = W & vec = v3489: {0};
player = W & vec = v1623: {v6823,v1723};
player = W & vec = v1624: {v6824,v1724};
player = W & vec = v1634: {v6834,v1734};
player = W & vec = v1627: {v6827};
player = W & vec = v1637: {v6837};
player = W & vec = v1647: {v6847};
player = W & vec = v1628: {v1728};
player = W & vec = v1638: {v1738};
player = W & vec = v1648: {v1748};
player = W & vec = v1678: {0};
player = W & vec = v1629: {v6829,v1729};
player = W & vec = v1639: {v6839,v1739};
player = W & vec = v1649: {v6849,v1749};
player = W & vec = v1679: {v6879};
player = W & vec = v1689: {v1789};
player = W & vec = v2613: {v6713,v6913,v2713};
player = W & vec = v2614: {v6714,v6914,v2714};
player = W & vec = v2634: {v6734,v6934,v1234,v2734};
player = W & vec = v2617: {v6917};
player = W & vec = v2637: {v6937,v1237};
player = W & vec = v2647: {v6947,v1247};
player = W & vec = v2618: {v6718,v6918,v2718};
player = W & vec = v2638: {v6738,v6938,v1238,v2738};
player = W & vec = v2648: {v6748,v6948,v1248,v2748};
player = W & vec = v2678: {v6978,v1278};
player = W & vec = v2619: {v6719,v2719};
player = W & vec = v2639: {v6739,v1239,v2739};
player = W & vec = v2649: {v6749,v1249,v2749};
player = W & vec = v2679: {v1279};
player = W & vec = v2689: {v6789,v1289,v2789};
player = W & vec = v3612: {v4612,v6812,v3712};
player = W & vec = v3614: {v6814,v3714};
player = W & vec = v3624: {v6824,v1324,v3724};
player = W & vec = v3617: {v4617,v6817};
player = W & vec = v3627: {v4627,v6827,v1327};
player = W & vec = v3647: {v6847,v1347};
player = W & vec = v3618: {v4618,v3718};
player = W & vec = v3628: {v4628,v1328,v3728};
player = W & vec = v3648: {v1348,v3748};
player = W & vec = v3678: {v4678,v1378};
player = W & vec = v3619: {v4619,v6819,v3719};
player = W & vec = v3629: {v4629,v6829,v1329,v3729};
player = W & vec = v3649: {v6849,v1349,v3749};
player = W & vec = v3679: {v4679,v6879,v1379};
player = W & vec = v3689: {v4689,v1389,v3789};
player = W & vec = v4612: {v3612,v6912,v4712};
player = W & vec = v4613: {v6913,v4713};
player = W & vec = v4623: {v6923,v1423,v4723};
player = W & vec = v4617: {v3617,v6917};
player = W & vec = v4627: {v3627,v6927,v1427};
player = W & vec = v4637: {v6937,v1437};
player = W & vec = v4618: {v3618,v6918,v4718};
player = W & vec = v4628: {v3628,v6928,v1428,v4728};
player = W & vec = v4638: {v6938,v1438,v4738};
player = W & vec = v4678: {v3678,v6978,v1478};
player = W & vec = v4619: {v3619,v4719};
player = W & vec = v4629: {v3629,v1429,v4729};
player = W & vec = v4639: {v1439,v4739};
player = W & vec = v4679: {v3679,v1479};
player = W & vec = v4689: {v3689,v1489,v4789};
player = W & vec = v1723: {v6723,v7823,v1623};
player = W & vec = v1724: {v6724,v7824,v1624};
player = W & vec = v1734: {v6734,v7834,v1234,v1634};
player = W & vec = v1726: {v7826};
player = W & vec = v1736: {v7836,v1236};
player = W & vec = v1746: {v7846,v1246};
player = W & vec = v1728: {v6728,v1628};
player = W & vec = v1738: {v6738,v1238,v1638};
player = W & vec = v1748: {v6748,v1248,v1648};
player = W & vec = v1768: {v1268};
player = W & vec = v1729: {v6729,v7829,v1629};
player = W & vec = v1739: {v6739,v7839,v1239,v1639};
player = W & vec = v1749: {v6749,v7849,v1249,v1649};
player = W & vec = v1769: {v7869,v1269};
player = W & vec = v1789: {v6789,v1289,v1689};
player = W & vec = v2713: {v7913,v2613};
player = W & vec = v2714: {v7914,v2614};
player = W & vec = v2734: {v7934,v2634};
player = W & vec = v2716: {v7916};
player = W & vec = v2736: {v7936};
player = W & vec = v2746: {v7946};
player = W & vec = v2718: {v7918,v2618};
player = W & vec = v2738: {v7938,v2638};
player = W & vec = v2748: {v7948,v2648};
player = W & vec = v2768: {v7968};
player = W & vec = v2719: {v2619};
player = W & vec = v2739: {v2639};
player = W & vec = v2749: {v2649};
player = W & vec = v2769: {0};
player = W & vec = v2789: {v2689};
player = W & vec = v3712: {v4712,v7812,v3612};
player = W & vec = v3714: {v7814,v2314,v3614};
player = W & vec = v3724: {v7824,v3624};
player = W & vec = v3716: {v4716,v7816,v2316};
player = W & vec = v3726: {v4726,v7826};
player = W & vec = v3746: {v7846,v2346};
player = W & vec = v3718: {v4718,v2318,v3618};
player = W & vec = v3728: {v4728,v3628};
player = W & vec = v3748: {v2348,v3648};
player = W & vec = v3768: {v4768,v2368};
player = W & vec = v3719: {v4719,v7819,v2319,v3619};
player = W & vec = v3729: {v4729,v7829,v3629};
player = W & vec = v3749: {v7849,v2349,v3649};
player = W & vec = v3769: {v4769,v7869,v2369};
player = W & vec = v3789: {v4789,v2389,v3689};
player = W & vec = v4712: {v3712,v7912,v4612};
player = W & vec = v4713: {v7913,v2413,v4613};
player = W & vec = v4723: {v7923,v4623};
player = W & vec = v4716: {v3716,v7916,v2416};
player = W & vec = v4726: {v3726,v7926};
player = W & vec = v4736: {v7936,v2436};
player = W & vec = v4718: {v3718,v7918,v2418,v4618};
player = W & vec = v4728: {v3728,v7928,v4628};
player = W & vec = v4738: {v7938,v2438,v4638};
player = W & vec = v4768: {v3768,v7968,v2468};
player = W & vec = v4719: {v3719,v2419,v4619};
player = W & vec = v4729: {v3729,v4629};
player = W & vec = v4739: {v2439,v4639};
player = W & vec = v4769: {v3769,v2469};
player = W & vec = v4789: {v3789,v2489,v4689};
player = W & vec = v6712: {0};
player = W & vec = v6713: {v2613};
player = W & vec = v6723: {v1723};
player = W & vec = v6714: {v2614};
player = W & vec = v6724: {v1724};
player = W & vec = v6734: {v1734,v2634};
player = W & vec = v6718: {v2618};
player = W & vec = v6728: {v1728};
player = W & vec = v6738: {v1738,v2638};
player = W & vec = v6748: {v1748,v2648};
player = W & vec = v6719: {v2619};
player = W & vec = v6729: {v1729};
player = W & vec = v6739: {v1739,v2639};
player = W & vec = v6749: {v1749,v2649};
player = W & vec = v6789: {v1789,v2689};
player = W & vec = v1823: {v6823};
player = W & vec = v1824: {v6824,v1324};
player = W & vec = v1834: {v6834};
player = W & vec = v1826: {v1326};
player = W & vec = v1836: {0};
player = W & vec = v1846: {v1346};
player = W & vec = v1827: {v6827,v1327};
player = W & vec = v1837: {v6837};
player = W & vec = v1847: {v6847,v1347};
player = W & vec = v1867: {v1367};
player = W & vec = v1829: {v6829,v1329};
player = W & vec = v1839: {v6839};
player = W & vec = v1849: {v6849,v1349};
player = W & vec = v1869: {v1369};
player = W & vec = v1879: {v6879,v1379};
player = W & vec = v2813: {v7813,v8913};
player = W & vec = v2814: {v7814,v8914,v2314};
player = W & vec = v2834: {v7834,v8934,v1234};
player = W & vec = v2816: {v7816,v8916,v2316};
player = W & vec = v2836: {v7836,v8936,v1236};
player = W & vec = v2846: {v7846,v8946,v1246,v2346};
player = W & vec = v2817: {v8917,v2317};
player = W & vec = v2837: {v8937,v1237};
player = W & vec = v2847: {v8947,v1247,v2347};
player = W & vec = v2867: {v8967,v1267,v2367};
player = W & vec = v2819: {v7819,v2319};
player = W & vec = v2839: {v7839,v1239};
player = W & vec = v2849: {v7849,v1249,v2349};
player = W & vec = v2869: {v7869,v1269,v2369};
player = W & vec = v2879: {v1279,v2379};
player = W & vec = v3812: {v4812};
player = W & vec = v3814: {0};
player = W & vec = v3824: {v1324};
player = W & vec = v3816: {v4816};
player = W & vec = v3826: {v4826,v1326};
player = W & vec = v3846: {v1346};
player = W & vec = v3817: {v4817};
player = W & vec = v3827: {v4827,v1327};
player = W & vec = v3847: {v1347};
player = W & vec = v3867: {v4867,v1367};
player = W & vec = v3819: {v4819};
player = W & vec = v3829: {v4829,v1329};
player = W & vec = v3849: {v1349};
player = W & vec = v3869: {v4869,v1369};
player = W & vec = v3879: {v4879,v1379};
player = W & vec = v4812: {v3812,v8912,v3412};
player = W & vec = v4813: {v8913};
player = W & vec = v4823: {v8923,v1423};
player = W & vec = v4816: {v3816,v8916,v3416};
player = W & vec = v4826: {v3826,v8926,v1426,v3426};
player = W & vec = v4836: {v8936,v1436};
player = W & vec = v4817: {v3817,v8917,v3417};
player = W & vec = v4827: {v3827,v8927,v1427,v3427};
player = W & vec = v4837: {v8937,v1437};
player = W & vec = v4867: {v3867,v8967,v1467,v3467};
player = W & vec = v4819: {v3819,v3419};
player = W & vec = v4829: {v3829,v1429,v3429};
player = W & vec = v4839: {v1439};
player = W & vec = v4869: {v3869,v1469,v3469};
player = W & vec = v4879: {v3879,v1479,v3479};
player = W & vec = v6812: {v7812,v3612};
player = W & vec = v6813: {v7813};
player = W & vec = v6823: {v1823,v7823,v1623};
player = W & vec = v6814: {v7814,v3614};
player = W & vec = v6824: {v1824,v7824,v1624,v3624};
player = W & vec = v6834: {v1834,v7834,v1634};
player = W & vec = v6817: {v3617};
player = W & vec = v6827: {v1827,v1627,v3627};
player = W & vec = v6837: {v1837,v1637};
player = W & vec = v6847: {v1847,v1647,v3647};
player = W & vec = v6819: {v7819,v3619};
player = W & vec = v6829: {v1829,v7829,v1629,v3629};
player = W & vec = v6839: {v1839,v7839,v1639};
player = W & vec = v6849: {v1849,v7849,v1649,v3649};
player = W & vec = v6879: {v1879,v1679,v3679};
player = W & vec = v7812: {v6812,v3712};
player = W & vec = v7813: {v2813,v6813};
player = W & vec = v7823: {v6823,v1723};
player = W & vec = v7814: {v2814,v6814,v3714};
player = W & vec = v7824: {v6824,v1724,v3724};
player = W & vec = v7834: {v2834,v6834,v1734};
player = W & vec = v7816: {v2816,v3716};
player = W & vec = v7826: {v1726,v3726};
player = W & vec = v7836: {v2836,v1736};
player = W & vec = v7846: {v2846,v1746,v3746};
player = W & vec = v7819: {v2819,v6819,v3719};
player = W & vec = v7829: {v6829,v1729,v3729};
player = W & vec = v7839: {v2839,v6839,v1739};
player = W & vec = v7849: {v2849,v6849,v1749,v3749};
player = W & vec = v7869: {v2869,v1769,v3769};
player = W & vec = v1923: {v6923,v8923,v1423};
player = W & vec = v1924: {v6924,v8924};
player = W & vec = v1934: {v6934,v8934,v1234};
player = W & vec = v1926: {v8926,v1426};
player = W & vec = v1936: {v8936,v1236,v1436};
player = W & vec = v1946: {v8946,v1246};
player = W & vec = v1927: {v6927,v8927,v1427};
player = W & vec = v1937: {v6937,v8937,v1237,v1437};
player = W & vec = v1947: {v6947,v8947,v1247};
player = W & vec = v1967: {v8967,v1267,v1467};
player = W & vec = v1928: {v6928,v1428};
player = W & vec = v1938: {v6938,v1238,v1438};
player = W & vec = v1948: {v6948,v1248};
player = W & vec = v1968: {v1268,v1468};
player = W & vec = v1978: {v6978,v1278,v1478};
player = W & vec = v2913: {v7913,v2413};
player = W & vec = v2914: {v7914};
player = W & vec = v2934: {v7934};
player = W & vec = v2916: {v7916,v2416};
player = W & vec = v2936: {v7936,v2436};
player = W & vec = v2946: {v7946};
player = W & vec = v2917: {v2417};
player = W & vec = v2937: {v2437};
player = W & vec = v2947: {0};
player = W & vec = v2967: {v2467};
player = W & vec = v2918: {v7918,v2418};
player = W & vec = v2938: {v7938,v2438};
player = W & vec = v2948: {v7948};
player = W & vec = v2968: {v7968,v2468};
player = W & vec = v2978: {v2478};
player = W & vec = v3912: {v4912,v8912,v3412};
player = W & vec = v3914: {v8914,v2314};
player = W & vec = v3924: {v8924};
player = W & vec = v3916: {v4916,v8916,v2316,v3416};
player = W & vec = v3926: {v4926,v8926,v3426};
player = W & vec = v3946: {v8946,v2346};
player = W & vec = v3917: {v4917,v8917,v2317,v3417};
player = W & vec = v3927: {v4927,v8927,v3427};
player = W & vec = v3947: {v8947,v2347};
player = W & vec = v3967: {v4967,v8967,v2367,v3467};
player = W & vec = v3918: {v4918,v2318,v3418};
player = W & vec = v3928: {v4928,v3428};
player = W & vec = v3948: {v2348};
player = W & vec = v3968: {v4968,v2368,v3468};
player = W & vec = v3978: {v4978,v2378,v3478};
player = W & vec = v4912: {v3912};
player = W & vec = v4913: {v2413};
player = W & vec = v4923: {0};
player = W & vec = v4916: {v3916,v2416};
player = W & vec = v4926: {v3926};
player = W & vec = v4936: {v2436};
player = W & vec = v4917: {v3917,v2417};
player = W & vec = v4927: {v3927};
player = W & vec = v4937: {v2437};
player = W & vec = v4967: {v3967,v2467};
player = W & vec = v4918: {v3918,v2418};
player = W & vec = v4928: {v3928};
player = W & vec = v4938: {v2438};
player = W & vec = v4968: {v3968,v2468};
player = W & vec = v4978: {v3978,v2478};
player = W & vec = v6912: {v7912,v4612};
player = W & vec = v6913: {v7913,v2613,v4613};
player = W & vec = v6923: {v1923,v7923,v4623};
player = W & vec = v6914: {v7914,v2614};
player = W & vec = v6924: {v1924,v7924};
player = W & vec = v6934: {v1934,v7934,v2634};
player = W & vec = v6917: {v2617,v4617};
player = W & vec = v6927: {v1927,v4627};
player = W & vec = v6937: {v1937,v2637,v4637};
player = W & vec = v6947: {v1947,v2647};
player = W & vec = v6918: {v7918,v2618,v4618};
player = W & vec = v6928: {v1928,v7928,v4628};
player = W & vec = v6938: {v1938,v7938,v2638,v4638};
player = W & vec = v6948: {v1948,v7948,v2648};
player = W & vec = v6978: {v1978,v2678,v4678};
player = W & vec = v7912: {v6912,v4712};
player = W & vec = v7913: {v2913,v6913,v2713,v4713};
player = W & vec = v7923: {v6923,v4723};
player = W & vec = v7914: {v2914,v6914,v2714};
player = W & vec = v7924: {v6924};
player = W & vec = v7934: {v2934,v6934,v2734};
player = W & vec = v7916: {v2916,v2716,v4716};
player = W & vec = v7926: {v4726};
player = W & vec = v7936: {v2936,v2736,v4736};
player = W & vec = v7946: {v2946,v2746};
player = W & vec = v7918: {v2918,v6918,v2718,v4718};
player = W & vec = v7928: {v6928,v4728};
player = W & vec = v7938: {v2938,v6938,v2738,v4738};
player = W & vec = v7948: {v2948,v6948,v2748};
player = W & vec = v7968: {v2968,v2768,v4768};
player = W & vec = v8912: {v3912,v4812};
player = W & vec = v8913: {v2813,v4813};
player = W & vec = v8923: {v1923,v4823};
player = W & vec = v8914: {v3914,v2814};
player = W & vec = v8924: {v1924,v3924};
player = W & vec = v8934: {v1934,v2834};
player = W & vec = v8916: {v3916,v2816,v4816};
player = W & vec = v8926: {v1926,v3926,v4826};
player = W & vec = v8936: {v1936,v2836,v4836};
player = W & vec = v8946: {v1946,v3946,v2846};
player = W & vec = v8917: {v3917,v2817,v4817};
player = W & vec = v8927: {v1927,v3927,v4827};
player = W & vec = v8937: {v1937,v2837,v4837};
player = W & vec = v8947: {v1947,v3947,v2847};
player = W & vec = v8967: {v1967,v3967,v2867,v4867};
