nix-grpc-store-claims-spec
checks.x86_64-linux.claims-spec
· build #94
· raw
1tribuchet: building on jamie2An example execution:34[State 0]5{6 nextToken: 1,7 present: false,8 rowStale: false,9 rowToken: 0,10 touched: false,11 ws:12 Map(13 "w1" ->14 {15 conn: false,16 outputs: false,17 phase: Idle,18 res: RNone,19 slot: false,20 srv: SNone,21 token: 022 },23 "w2" ->24 {25 conn: false,26 outputs: false,27 phase: Idle,28 res: RNone,29 slot: false,30 srv: SNone,31 token: 032 },33 "w3" ->34 {35 conn: false,36 outputs: false,37 phase: Idle,38 res: RNone,39 slot: false,40 srv: SNone,41 token: 042 }43 )44}4546[State 1]47{48 nextToken: 1,49 present: false,50 rowStale: false,51 rowToken: 0,52 touched: false,53 ws:54 Map(55 "w1" ->56 {57 conn: false,58 outputs: false,59 phase: Idle,60 res: RNone,61 slot: false,62 srv: SNone,63 token: 064 },65 "w2" ->66 {67 conn: false,68 outputs: false,69 phase: Idle,70 res: RNone,71 slot: false,72 srv: SNone,73 token: 074 },75 "w3" ->76 {77 conn: true,78 outputs: false,79 phase: Pending,80 res: RNone,81 slot: true,82 srv: SNeed,83 token: 084 }85 )86}8788[State 2]89{90 nextToken: 2,91 present: false,92 rowStale: false,93 rowToken: 1,94 touched: false,95 ws:96 Map(97 "w1" ->98 {99 conn: false,100 outputs: false,101 phase: Idle,102 res: RNone,103 slot: false,104 srv: SNone,105 token: 0106 },107 "w2" ->108 {109 conn: false,110 outputs: false,111 phase: Idle,112 res: RNone,113 slot: false,114 srv: SNone,115 token: 0116 },117 "w3" ->118 {119 conn: true,120 outputs: false,121 phase: Building,122 res: RNone,123 slot: true,124 srv: SHolder(1),125 token: 1126 }127 )128}129130[State 3]131{132 nextToken: 2,133 present: false,134 rowStale: false,135 rowToken: 1,136 touched: false,137 ws:138 Map(139 "w1" ->140 {141 conn: false,142 outputs: false,143 phase: Idle,144 res: RNone,145 slot: false,146 srv: SNone,147 token: 0148 },149 "w2" ->150 {151 conn: false,152 outputs: false,153 phase: Idle,154 res: RNone,155 slot: false,156 srv: SNone,157 token: 0158 },159 "w3" ->160 {161 conn: false,162 outputs: false,163 phase: Building,164 res: RNone,165 slot: true,166 srv: SNone,167 token: 1168 }169 )170}171172[State 4]173{174 nextToken: 2,175 present: false,176 rowStale: false,177 rowToken: 1,178 touched: false,179 ws:180 Map(181 "w1" ->182 {183 conn: false,184 outputs: false,185 phase: Idle,186 res: RNone,187 slot: false,188 srv: SNone,189 token: 0190 },191 "w2" ->192 {193 conn: false,194 outputs: false,195 phase: Idle,196 res: RNone,197 slot: false,198 srv: SNone,199 token: 0200 },201 "w3" ->202 {203 conn: true,204 outputs: false,205 phase: Building,206 res: RNone,207 slot: true,208 srv: SNeed,209 token: 1210 }211 )212}213214[State 5]215{216 nextToken: 2,217 present: false,218 rowStale: true,219 rowToken: 1,220 touched: false,221 ws:222 Map(223 "w1" ->224 {225 conn: false,226 outputs: false,227 phase: Idle,228 res: RNone,229 slot: false,230 srv: SNone,231 token: 0232 },233 "w2" ->234 {235 conn: false,236 outputs: false,237 phase: Idle,238 res: RNone,239 slot: false,240 srv: SNone,241 token: 0242 },243 "w3" ->244 {245 conn: true,246 outputs: false,247 phase: Building,248 res: RNone,249 slot: true,250 srv: SNeed,251 token: 1252 }253 )254}255256[State 6]257{258 nextToken: 2,259 present: false,260 rowStale: true,261 rowToken: 1,262 touched: false,263 ws:264 Map(265 "w1" ->266 {267 conn: false,268 outputs: false,269 phase: Idle,270 res: RNone,271 slot: false,272 srv: SNone,273 token: 0274 },275 "w2" ->276 {277 conn: false,278 outputs: false,279 phase: Idle,280 res: RNone,281 slot: false,282 srv: SNone,283 token: 0284 },285 "w3" ->286 {287 conn: false,288 outputs: false,289 phase: Building,290 res: RNone,291 slot: true,292 srv: SNone,293 token: 1294 }295 )296}297298[State 7]299{300 nextToken: 2,301 present: false,302 rowStale: true,303 rowToken: 1,304 touched: false,305 ws:306 Map(307 "w1" ->308 {309 conn: false,310 outputs: false,311 phase: Idle,312 res: RNone,313 slot: false,314 srv: SNone,315 token: 0316 },317 "w2" ->318 {319 conn: false,320 outputs: false,321 phase: Idle,322 res: RNone,323 slot: false,324 srv: SNone,325 token: 0326 },327 "w3" ->328 {329 conn: false,330 outputs: false,331 phase: Done,332 res: RUnavailable,333 slot: false,334 srv: SNone,335 token: 1336 }337 )338}339340[State 8]341{342 nextToken: 2,343 present: false,344 rowStale: true,345 rowToken: 1,346 touched: false,347 ws:348 Map(349 "w1" ->350 {351 conn: false,352 outputs: false,353 phase: Idle,354 res: RNone,355 slot: false,356 srv: SNone,357 token: 0358 },359 "w2" ->360 {361 conn: true,362 outputs: false,363 phase: Pending,364 res: RNone,365 slot: true,366 srv: SNeed,367 token: 0368 },369 "w3" ->370 {371 conn: false,372 outputs: false,373 phase: Done,374 res: RUnavailable,375 slot: false,376 srv: SNone,377 token: 1378 }379 )380}381382[State 9]383{384 nextToken: 2,385 present: false,386 rowStale: true,387 rowToken: 1,388 touched: false,389 ws:390 Map(391 "w1" ->392 {393 conn: false,394 outputs: false,395 phase: Idle,396 res: RNone,397 slot: false,398 srv: SNone,399 token: 0400 },401 "w2" ->402 {403 conn: false,404 outputs: false,405 phase: Pending,406 res: RNone,407 slot: true,408 srv: SNone,409 token: 0410 },411 "w3" ->412 {413 conn: false,414 outputs: false,415 phase: Done,416 res: RUnavailable,417 slot: false,418 srv: SNone,419 token: 1420 }421 )422}423424[State 10]425{426 nextToken: 2,427 present: false,428 rowStale: true,429 rowToken: 1,430 touched: false,431 ws:432 Map(433 "w1" ->434 {435 conn: false,436 outputs: false,437 phase: Idle,438 res: RNone,439 slot: false,440 srv: SNone,441 token: 0442 },443 "w2" ->444 {445 conn: true,446 outputs: false,447 phase: Pending,448 res: RNone,449 slot: true,450 srv: SNeed,451 token: 0452 },453 "w3" ->454 {455 conn: false,456 outputs: false,457 phase: Done,458 res: RUnavailable,459 slot: false,460 srv: SNone,461 token: 1462 }463 )464}465466[State 11]467{468 nextToken: 2,469 present: false,470 rowStale: true,471 rowToken: 1,472 touched: false,473 ws:474 Map(475 "w1" ->476 {477 conn: false,478 outputs: false,479 phase: Idle,480 res: RNone,481 slot: false,482 srv: SNone,483 token: 0484 },485 "w2" ->486 {487 conn: false,488 outputs: false,489 phase: Pending,490 res: RNone,491 slot: true,492 srv: SNone,493 token: 0494 },495 "w3" ->496 {497 conn: false,498 outputs: false,499 phase: Done,500 res: RUnavailable,501 slot: false,502 srv: SNone,503 token: 1504 }505 )506}507508[State 12]509{510 nextToken: 2,511 present: false,512 rowStale: true,513 rowToken: 1,514 touched: false,515 ws:516 Map(517 "w1" ->518 {519 conn: false,520 outputs: false,521 phase: Idle,522 res: RNone,523 slot: false,524 srv: SNone,525 token: 0526 },527 "w2" ->528 {529 conn: true,530 outputs: false,531 phase: Pending,532 res: RNone,533 slot: true,534 srv: SNeed,535 token: 0536 },537 "w3" ->538 {539 conn: false,540 outputs: false,541 phase: Done,542 res: RUnavailable,543 slot: false,544 srv: SNone,545 token: 1546 }547 )548}549550[State 13]551{552 nextToken: 2,553 present: false,554 rowStale: true,555 rowToken: 1,556 touched: false,557 ws:558 Map(559 "w1" ->560 {561 conn: false,562 outputs: false,563 phase: Idle,564 res: RNone,565 slot: false,566 srv: SNone,567 token: 0568 },569 "w2" ->570 {571 conn: true,572 outputs: false,573 phase: Pending,574 res: RNone,575 slot: true,576 srv: SNeed,577 token: 0578 },579 "w3" ->580 {581 conn: false,582 outputs: false,583 phase: Idle,584 res: RNone,585 slot: false,586 srv: SNone,587 token: 0588 }589 )590}591592[State 14]593{594 nextToken: 2,595 present: false,596 rowStale: true,597 rowToken: 1,598 touched: false,599 ws:600 Map(601 "w1" ->602 {603 conn: false,604 outputs: false,605 phase: Idle,606 res: RNone,607 slot: false,608 srv: SNone,609 token: 0610 },611 "w2" ->612 {613 conn: false,614 outputs: false,615 phase: Pending,616 res: RNone,617 slot: true,618 srv: SNone,619 token: 0620 },621 "w3" ->622 {623 conn: false,624 outputs: false,625 phase: Idle,626 res: RNone,627 slot: false,628 srv: SNone,629 token: 0630 }631 )632}633634[State 15]635{636 nextToken: 2,637 present: false,638 rowStale: true,639 rowToken: 1,640 touched: false,641 ws:642 Map(643 "w1" ->644 {645 conn: false,646 outputs: false,647 phase: Idle,648 res: RNone,649 slot: false,650 srv: SNone,651 token: 0652 },653 "w2" ->654 {655 conn: false,656 outputs: false,657 phase: Done,658 res: RUnavailable,659 slot: false,660 srv: SNone,661 token: 0662 },663 "w3" ->664 {665 conn: false,666 outputs: false,667 phase: Idle,668 res: RNone,669 slot: false,670 srv: SNone,671 token: 0672 }673 )674}675676[State 16]677{678 nextToken: 2,679 present: false,680 rowStale: true,681 rowToken: 1,682 touched: false,683 ws:684 Map(685 "w1" ->686 {687 conn: true,688 outputs: false,689 phase: Pending,690 res: RNone,691 slot: true,692 srv: SNeed,693 token: 0694 },695 "w2" ->696 {697 conn: false,698 outputs: false,699 phase: Done,700 res: RUnavailable,701 slot: false,702 srv: SNone,703 token: 0704 },705 "w3" ->706 {707 conn: false,708 outputs: false,709 phase: Idle,710 res: RNone,711 slot: false,712 srv: SNone,713 token: 0714 }715 )716}717718[State 17]719{720 nextToken: 2,721 present: false,722 rowStale: true,723 rowToken: 1,724 touched: false,725 ws:726 Map(727 "w1" ->728 {729 conn: false,730 outputs: false,731 phase: Pending,732 res: RNone,733 slot: true,734 srv: SNone,735 token: 0736 },737 "w2" ->738 {739 conn: false,740 outputs: false,741 phase: Done,742 res: RUnavailable,743 slot: false,744 srv: SNone,745 token: 0746 },747 "w3" ->748 {749 conn: false,750 outputs: false,751 phase: Idle,752 res: RNone,753 slot: false,754 srv: SNone,755 token: 0756 }757 )758}759760[State 18]761{762 nextToken: 2,763 present: false,764 rowStale: true,765 rowToken: 1,766 touched: false,767 ws:768 Map(769 "w1" ->770 {771 conn: false,772 outputs: false,773 phase: Done,774 res: RUnavailable,775 slot: false,776 srv: SNone,777 token: 0778 },779 "w2" ->780 {781 conn: false,782 outputs: false,783 phase: Done,784 res: RUnavailable,785 slot: false,786 srv: SNone,787 token: 0788 },789 "w3" ->790 {791 conn: false,792 outputs: false,793 phase: Idle,794 res: RNone,795 slot: false,796 srv: SNone,797 token: 0798 }799 )800}801802[State 19]803{804 nextToken: 2,805 present: false,806 rowStale: true,807 rowToken: 1,808 touched: false,809 ws:810 Map(811 "w1" ->812 {813 conn: false,814 outputs: false,815 phase: Done,816 res: RUnavailable,817 slot: false,818 srv: SNone,819 token: 0820 },821 "w2" ->822 {823 conn: false,824 outputs: false,825 phase: Done,826 res: RUnavailable,827 slot: false,828 srv: SNone,829 token: 0830 },831 "w3" ->832 {833 conn: true,834 outputs: false,835 phase: Pending,836 res: RNone,837 slot: true,838 srv: SNeed,839 token: 0840 }841 )842}843844[State 20]845{846 nextToken: 2,847 present: false,848 rowStale: true,849 rowToken: 1,850 touched: false,851 ws:852 Map(853 "w1" ->854 {855 conn: false,856 outputs: false,857 phase: Done,858 res: RUnavailable,859 slot: false,860 srv: SNone,861 token: 0862 },863 "w2" ->864 {865 conn: false,866 outputs: false,867 phase: Idle,868 res: RNone,869 slot: false,870 srv: SNone,871 token: 0872 },873 "w3" ->874 {875 conn: true,876 outputs: false,877 phase: Pending,878 res: RNone,879 slot: true,880 srv: SNeed,881 token: 0882 }883 )884}885886[State 21]887{888 nextToken: 3,889 present: false,890 rowStale: false,891 rowToken: 2,892 touched: false,893 ws:894 Map(895 "w1" ->896 {897 conn: false,898 outputs: false,899 phase: Done,900 res: RUnavailable,901 slot: false,902 srv: SNone,903 token: 0904 },905 "w2" ->906 {907 conn: false,908 outputs: false,909 phase: Idle,910 res: RNone,911 slot: false,912 srv: SNone,913 token: 0914 },915 "w3" ->916 {917 conn: true,918 outputs: false,919 phase: Building,920 res: RNone,921 slot: true,922 srv: SHolder(2),923 token: 2924 }925 )926}927928[State 22]929{930 nextToken: 3,931 present: false,932 rowStale: false,933 rowToken: 2,934 touched: false,935 ws:936 Map(937 "w1" ->938 {939 conn: false,940 outputs: false,941 phase: Idle,942 res: RNone,943 slot: false,944 srv: SNone,945 token: 0946 },947 "w2" ->948 {949 conn: false,950 outputs: false,951 phase: Idle,952 res: RNone,953 slot: false,954 srv: SNone,955 token: 0956 },957 "w3" ->958 {959 conn: true,960 outputs: false,961 phase: Building,962 res: RNone,963 slot: true,964 srv: SHolder(2),965 token: 2966 }967 )968}969970[State 23]971{972 nextToken: 3,973 present: false,974 rowStale: false,975 rowToken: 2,976 touched: false,977 ws:978 Map(979 "w1" ->980 {981 conn: false,982 outputs: false,983 phase: Idle,984 res: RNone,985 slot: false,986 srv: SNone,987 token: 0988 },989 "w2" ->990 {991 conn: false,992 outputs: false,993 phase: Idle,994 res: RNone,995 slot: false,996 srv: SNone,997 token: 0998 },999 "w3" ->1000 {1001 conn: false,1002 outputs: false,1003 phase: Building,1004 res: RNone,1005 slot: true,1006 srv: SNone,1007 token: 21008 }1009 )1010}10111012[State 24]1013{1014 nextToken: 3,1015 present: false,1016 rowStale: false,1017 rowToken: 2,1018 touched: false,1019 ws:1020 Map(1021 "w1" ->1022 {1023 conn: false,1024 outputs: false,1025 phase: Idle,1026 res: RNone,1027 slot: false,1028 srv: SNone,1029 token: 01030 },1031 "w2" ->1032 {1033 conn: false,1034 outputs: false,1035 phase: Idle,1036 res: RNone,1037 slot: false,1038 srv: SNone,1039 token: 01040 },1041 "w3" ->1042 {1043 conn: false,1044 outputs: false,1045 phase: Done,1046 res: RUnavailable,1047 slot: false,1048 srv: SNone,1049 token: 21050 }1051 )1052}10531054[State 25]1055{1056 nextToken: 3,1057 present: false,1058 rowStale: false,1059 rowToken: 2,1060 touched: false,1061 ws:1062 Map(1063 "w1" ->1064 {1065 conn: false,1066 outputs: false,1067 phase: Idle,1068 res: RNone,1069 slot: false,1070 srv: SNone,1071 token: 01072 },1073 "w2" ->1074 {1075 conn: true,1076 outputs: false,1077 phase: Pending,1078 res: RNone,1079 slot: true,1080 srv: SNeed,1081 token: 01082 },1083 "w3" ->1084 {1085 conn: false,1086 outputs: false,1087 phase: Done,1088 res: RUnavailable,1089 slot: false,1090 srv: SNone,1091 token: 21092 }1093 )1094}10951096[State 26]1097{1098 nextToken: 3,1099 present: false,1100 rowStale: false,1101 rowToken: 2,1102 touched: false,1103 ws:1104 Map(1105 "w1" ->1106 {1107 conn: false,1108 outputs: false,1109 phase: Idle,1110 res: RNone,1111 slot: false,1112 srv: SNone,1113 token: 01114 },1115 "w2" ->1116 {1117 conn: false,1118 outputs: false,1119 phase: Pending,1120 res: RNone,1121 slot: true,1122 srv: SNone,1123 token: 01124 },1125 "w3" ->1126 {1127 conn: false,1128 outputs: false,1129 phase: Done,1130 res: RUnavailable,1131 slot: false,1132 srv: SNone,1133 token: 21134 }1135 )1136}11371138[State 27]1139{1140 nextToken: 3,1141 present: false,1142 rowStale: true,1143 rowToken: 2,1144 touched: false,1145 ws:1146 Map(1147 "w1" ->1148 {1149 conn: false,1150 outputs: false,1151 phase: Idle,1152 res: RNone,1153 slot: false,1154 srv: SNone,1155 token: 01156 },1157 "w2" ->1158 {1159 conn: false,1160 outputs: false,1161 phase: Pending,1162 res: RNone,1163 slot: true,1164 srv: SNone,1165 token: 01166 },1167 "w3" ->1168 {1169 conn: false,1170 outputs: false,1171 phase: Done,1172 res: RUnavailable,1173 slot: false,1174 srv: SNone,1175 token: 21176 }1177 )1178}11791180[State 28]1181{1182 nextToken: 3,1183 present: false,1184 rowStale: true,1185 rowToken: 2,1186 touched: false,1187 ws:1188 Map(1189 "w1" ->1190 {1191 conn: false,1192 outputs: false,1193 phase: Idle,1194 res: RNone,1195 slot: false,1196 srv: SNone,1197 token: 01198 },1199 "w2" ->1200 {1201 conn: false,1202 outputs: false,1203 phase: Pending,1204 res: RNone,1205 slot: true,1206 srv: SNone,1207 token: 01208 },1209 "w3" ->1210 {1211 conn: false,1212 outputs: false,1213 phase: Idle,1214 res: RNone,1215 slot: false,1216 srv: SNone,1217 token: 01218 }1219 )1220}12211222[State 29]1223{1224 nextToken: 3,1225 present: false,1226 rowStale: true,1227 rowToken: 2,1228 touched: false,1229 ws:1230 Map(1231 "w1" ->1232 {1233 conn: false,1234 outputs: false,1235 phase: Idle,1236 res: RNone,1237 slot: false,1238 srv: SNone,1239 token: 01240 },1241 "w2" ->1242 {1243 conn: true,1244 outputs: false,1245 phase: Pending,1246 res: RNone,1247 slot: true,1248 srv: SNeed,1249 token: 01250 },1251 "w3" ->1252 {1253 conn: false,1254 outputs: false,1255 phase: Idle,1256 res: RNone,1257 slot: false,1258 srv: SNone,1259 token: 01260 }1261 )1262}12631264[State 30]1265{1266 nextToken: 3,1267 present: false,1268 rowStale: true,1269 rowToken: 2,1270 touched: false,1271 ws:1272 Map(1273 "w1" ->1274 {1275 conn: false,1276 outputs: false,1277 phase: Idle,1278 res: RNone,1279 slot: false,1280 srv: SNone,1281 token: 01282 },1283 "w2" ->1284 {1285 conn: false,1286 outputs: false,1287 phase: Pending,1288 res: RNone,1289 slot: true,1290 srv: SNone,1291 token: 01292 },1293 "w3" ->1294 {1295 conn: false,1296 outputs: false,1297 phase: Idle,1298 res: RNone,1299 slot: false,1300 srv: SNone,1301 token: 01302 }1303 )1304}13051306[ok] No violation found (461ms at 43384 traces/second).1307Trace length statistics: max=31, min=31, average=31.001308You may increase --max-samples and --max-steps.1309Use --verbosity to produce more (or less) output.1310Use --seed=0x21f2cccde9193da --backend=rust to reproduce.1311An example execution:13121313[State 0]1314{1315 nextToken: 1,1316 present: false,1317 rowStale: false,1318 rowToken: 0,1319 touched: false,1320 ws:1321 Map(1322 "w1" ->1323 {1324 conn: false,1325 outputs: false,1326 phase: Idle,1327 res: RNone,1328 slot: false,1329 srv: SNone,1330 token: 01331 },1332 "w2" ->1333 {1334 conn: false,1335 outputs: false,1336 phase: Idle,1337 res: RNone,1338 slot: false,1339 srv: SNone,1340 token: 01341 },1342 "w3" ->1343 {1344 conn: false,1345 outputs: false,1346 phase: Idle,1347 res: RNone,1348 slot: false,1349 srv: SNone,1350 token: 01351 }1352 )1353}13541355[State 1]1356{1357 nextToken: 1,1358 present: false,1359 rowStale: false,1360 rowToken: 0,1361 touched: false,1362 ws:1363 Map(1364 "w1" ->1365 {1366 conn: true,1367 outputs: false,1368 phase: Pending,1369 res: RNone,1370 slot: true,1371 srv: SNeed,1372 token: 01373 },1374 "w2" ->1375 {1376 conn: false,1377 outputs: false,1378 phase: Idle,1379 res: RNone,1380 slot: false,1381 srv: SNone,1382 token: 01383 },1384 "w3" ->1385 {1386 conn: false,1387 outputs: false,1388 phase: Idle,1389 res: RNone,1390 slot: false,1391 srv: SNone,1392 token: 01393 }1394 )1395}13961397[State 2]1398{1399 nextToken: 1,1400 present: false,1401 rowStale: false,1402 rowToken: 0,1403 touched: false,1404 ws:1405 Map(1406 "w1" ->1407 {1408 conn: false,1409 outputs: false,1410 phase: Pending,1411 res: RNone,1412 slot: true,1413 srv: SNone,1414 token: 01415 },1416 "w2" ->1417 {1418 conn: false,1419 outputs: false,1420 phase: Idle,1421 res: RNone,1422 slot: false,1423 srv: SNone,1424 token: 01425 },1426 "w3" ->1427 {1428 conn: false,1429 outputs: false,1430 phase: Idle,1431 res: RNone,1432 slot: false,1433 srv: SNone,1434 token: 01435 }1436 )1437}14381439[State 3]1440{1441 nextToken: 1,1442 present: false,1443 rowStale: false,1444 rowToken: 0,1445 touched: false,1446 ws:1447 Map(1448 "w1" ->1449 {1450 conn: true,1451 outputs: false,1452 phase: Pending,1453 res: RNone,1454 slot: true,1455 srv: SNeed,1456 token: 01457 },1458 "w2" ->1459 {1460 conn: false,1461 outputs: false,1462 phase: Idle,1463 res: RNone,1464 slot: false,1465 srv: SNone,1466 token: 01467 },1468 "w3" ->1469 {1470 conn: false,1471 outputs: false,1472 phase: Idle,1473 res: RNone,1474 slot: false,1475 srv: SNone,1476 token: 01477 }1478 )1479}14801481[State 4]1482{1483 nextToken: 1,1484 present: false,1485 rowStale: false,1486 rowToken: 0,1487 touched: false,1488 ws:1489 Map(1490 "w1" ->1491 {1492 conn: false,1493 outputs: false,1494 phase: Pending,1495 res: RNone,1496 slot: true,1497 srv: SNone,1498 token: 01499 },1500 "w2" ->1501 {1502 conn: false,1503 outputs: false,1504 phase: Idle,1505 res: RNone,1506 slot: false,1507 srv: SNone,1508 token: 01509 },1510 "w3" ->1511 {1512 conn: false,1513 outputs: false,1514 phase: Idle,1515 res: RNone,1516 slot: false,1517 srv: SNone,1518 token: 01519 }1520 )1521}15221523[State 5]1524{1525 nextToken: 1,1526 present: false,1527 rowStale: false,1528 rowToken: 0,1529 touched: false,1530 ws:1531 Map(1532 "w1" ->1533 {1534 conn: true,1535 outputs: false,1536 phase: Pending,1537 res: RNone,1538 slot: true,1539 srv: SNeed,1540 token: 01541 },1542 "w2" ->1543 {1544 conn: false,1545 outputs: false,1546 phase: Idle,1547 res: RNone,1548 slot: false,1549 srv: SNone,1550 token: 01551 },1552 "w3" ->1553 {1554 conn: false,1555 outputs: false,1556 phase: Idle,1557 res: RNone,1558 slot: false,1559 srv: SNone,1560 token: 01561 }1562 )1563}15641565[State 6]1566{1567 nextToken: 2,1568 present: false,1569 rowStale: false,1570 rowToken: 1,1571 touched: false,1572 ws:1573 Map(1574 "w1" ->1575 {1576 conn: true,1577 outputs: false,1578 phase: Building,1579 res: RNone,1580 slot: true,1581 srv: SHolder(1),1582 token: 11583 },1584 "w2" ->1585 {1586 conn: false,1587 outputs: false,1588 phase: Idle,1589 res: RNone,1590 slot: false,1591 srv: SNone,1592 token: 01593 },1594 "w3" ->1595 {1596 conn: false,1597 outputs: false,1598 phase: Idle,1599 res: RNone,1600 slot: false,1601 srv: SNone,1602 token: 01603 }1604 )1605}16061607[State 7]1608{1609 nextToken: 2,1610 present: false,1611 rowStale: false,1612 rowToken: 0,1613 touched: false,1614 ws:1615 Map(1616 "w1" ->1617 {1618 conn: false,1619 outputs: false,1620 phase: Done,1621 res: RFailed,1622 slot: false,1623 srv: SNone,1624 token: 11625 },1626 "w2" ->1627 {1628 conn: false,1629 outputs: false,1630 phase: Idle,1631 res: RNone,1632 slot: false,1633 srv: SNone,1634 token: 01635 },1636 "w3" ->1637 {1638 conn: false,1639 outputs: false,1640 phase: Idle,1641 res: RNone,1642 slot: false,1643 srv: SNone,1644 token: 01645 }1646 )1647}16481649[State 8]1650{1651 nextToken: 2,1652 present: false,1653 rowStale: false,1654 rowToken: 0,1655 touched: false,1656 ws:1657 Map(1658 "w1" ->1659 {1660 conn: false,1661 outputs: false,1662 phase: Done,1663 res: RFailed,1664 slot: false,1665 srv: SNone,1666 token: 11667 },1668 "w2" ->1669 {1670 conn: false,1671 outputs: false,1672 phase: Idle,1673 res: RNone,1674 slot: false,1675 srv: SNone,1676 token: 01677 },1678 "w3" ->1679 {1680 conn: true,1681 outputs: false,1682 phase: Pending,1683 res: RNone,1684 slot: true,1685 srv: SNeed,1686 token: 01687 }1688 )1689}16901691[State 9]1692{1693 nextToken: 2,1694 present: false,1695 rowStale: false,1696 rowToken: 0,1697 touched: false,1698 ws:1699 Map(1700 "w1" ->1701 {1702 conn: false,1703 outputs: false,1704 phase: Done,1705 res: RFailed,1706 slot: false,1707 srv: SNone,1708 token: 11709 },1710 "w2" ->1711 {1712 conn: false,1713 outputs: false,1714 phase: Idle,1715 res: RNone,1716 slot: false,1717 srv: SNone,1718 token: 01719 },1720 "w3" ->1721 {1722 conn: false,1723 outputs: false,1724 phase: Pending,1725 res: RNone,1726 slot: true,1727 srv: SNone,1728 token: 01729 }1730 )1731}17321733[State 10]1734{1735 nextToken: 2,1736 present: false,1737 rowStale: false,1738 rowToken: 0,1739 touched: false,1740 ws:1741 Map(1742 "w1" ->1743 {1744 conn: false,1745 outputs: false,1746 phase: Done,1747 res: RFailed,1748 slot: false,1749 srv: SNone,1750 token: 11751 },1752 "w2" ->1753 {1754 conn: false,1755 outputs: false,1756 phase: Idle,1757 res: RNone,1758 slot: false,1759 srv: SNone,1760 token: 01761 },1762 "w3" ->1763 {1764 conn: true,1765 outputs: false,1766 phase: Pending,1767 res: RNone,1768 slot: true,1769 srv: SNeed,1770 token: 01771 }1772 )1773}17741775[State 11]1776{1777 nextToken: 2,1778 present: false,1779 rowStale: false,1780 rowToken: 0,1781 touched: false,1782 ws:1783 Map(1784 "w1" ->1785 {1786 conn: false,1787 outputs: false,1788 phase: Done,1789 res: RFailed,1790 slot: false,1791 srv: SNone,1792 token: 11793 },1794 "w2" ->1795 {1796 conn: false,1797 outputs: false,1798 phase: Idle,1799 res: RNone,1800 slot: false,1801 srv: SNone,1802 token: 01803 },1804 "w3" ->1805 {1806 conn: false,1807 outputs: false,1808 phase: Pending,1809 res: RNone,1810 slot: true,1811 srv: SNone,1812 token: 01813 }1814 )1815}18161817[State 12]1818{1819 nextToken: 2,1820 present: false,1821 rowStale: false,1822 rowToken: 0,1823 touched: false,1824 ws:1825 Map(1826 "w1" ->1827 {1828 conn: false,1829 outputs: false,1830 phase: Done,1831 res: RFailed,1832 slot: false,1833 srv: SNone,1834 token: 11835 },1836 "w2" ->1837 {1838 conn: false,1839 outputs: false,1840 phase: Idle,1841 res: RNone,1842 slot: false,1843 srv: SNone,1844 token: 01845 },1846 "w3" ->1847 {1848 conn: true,1849 outputs: false,1850 phase: Pending,1851 res: RNone,1852 slot: true,1853 srv: SNeed,1854 token: 01855 }1856 )1857}18581859[State 13]1860{1861 nextToken: 3,1862 present: false,1863 rowStale: false,1864 rowToken: 2,1865 touched: false,1866 ws:1867 Map(1868 "w1" ->1869 {1870 conn: false,1871 outputs: false,1872 phase: Done,1873 res: RFailed,1874 slot: false,1875 srv: SNone,1876 token: 11877 },1878 "w2" ->1879 {1880 conn: false,1881 outputs: false,1882 phase: Idle,1883 res: RNone,1884 slot: false,1885 srv: SNone,1886 token: 01887 },1888 "w3" ->1889 {1890 conn: true,1891 outputs: false,1892 phase: Building,1893 res: RNone,1894 slot: true,1895 srv: SHolder(2),1896 token: 21897 }1898 )1899}19001901[State 14]1902{1903 nextToken: 3,1904 present: false,1905 rowStale: false,1906 rowToken: 2,1907 touched: false,1908 ws:1909 Map(1910 "w1" ->1911 {1912 conn: false,1913 outputs: false,1914 phase: Done,1915 res: RFailed,1916 slot: false,1917 srv: SNone,1918 token: 11919 },1920 "w2" ->1921 {1922 conn: false,1923 outputs: false,1924 phase: Idle,1925 res: RNone,1926 slot: false,1927 srv: SNone,1928 token: 01929 },1930 "w3" ->1931 {1932 conn: false,1933 outputs: false,1934 phase: Building,1935 res: RNone,1936 slot: true,1937 srv: SNone,1938 token: 21939 }1940 )1941}19421943[State 15]1944{1945 nextToken: 3,1946 present: false,1947 rowStale: false,1948 rowToken: 2,1949 touched: false,1950 ws:1951 Map(1952 "w1" ->1953 {1954 conn: false,1955 outputs: false,1956 phase: Done,1957 res: RFailed,1958 slot: false,1959 srv: SNone,1960 token: 11961 },1962 "w2" ->1963 {1964 conn: false,1965 outputs: false,1966 phase: Idle,1967 res: RNone,1968 slot: false,1969 srv: SNone,1970 token: 01971 },1972 "w3" ->1973 {1974 conn: true,1975 outputs: false,1976 phase: Building,1977 res: RNone,1978 slot: true,1979 srv: SNeed,1980 token: 21981 }1982 )1983}19841985[State 16]1986{1987 nextToken: 3,1988 present: false,1989 rowStale: false,1990 rowToken: 2,1991 touched: false,1992 ws:1993 Map(1994 "w1" ->1995 {1996 conn: false,1997 outputs: false,1998 phase: Done,1999 res: RFailed,2000 slot: false,2001 srv: SNone,2002 token: 12003 },2004 "w2" ->2005 {2006 conn: false,2007 outputs: false,2008 phase: Idle,2009 res: RNone,2010 slot: false,2011 srv: SNone,2012 token: 02013 },2014 "w3" ->2015 {2016 conn: false,2017 outputs: false,2018 phase: Building,2019 res: RNone,2020 slot: true,2021 srv: SNone,2022 token: 22023 }2024 )2025}20262027[State 17]2028{2029 nextToken: 3,2030 present: false,2031 rowStale: false,2032 rowToken: 2,2033 touched: false,2034 ws:2035 Map(2036 "w1" ->2037 {2038 conn: false,2039 outputs: false,2040 phase: Done,2041 res: RFailed,2042 slot: false,2043 srv: SNone,2044 token: 12045 },2046 "w2" ->2047 {2048 conn: false,2049 outputs: false,2050 phase: Idle,2051 res: RNone,2052 slot: false,2053 srv: SNone,2054 token: 02055 },2056 "w3" ->2057 {2058 conn: true,2059 outputs: false,2060 phase: Building,2061 res: RNone,2062 slot: true,2063 srv: SNeed,2064 token: 22065 }2066 )2067}20682069[State 18]2070{2071 nextToken: 3,2072 present: false,2073 rowStale: false,2074 rowToken: 2,2075 touched: false,2076 ws:2077 Map(2078 "w1" ->2079 {2080 conn: false,2081 outputs: false,2082 phase: Done,2083 res: RFailed,2084 slot: false,2085 srv: SNone,2086 token: 12087 },2088 "w2" ->2089 {2090 conn: false,2091 outputs: false,2092 phase: Idle,2093 res: RNone,2094 slot: false,2095 srv: SNone,2096 token: 02097 },2098 "w3" ->2099 {2100 conn: false,2101 outputs: false,2102 phase: Building,2103 res: RNone,2104 slot: true,2105 srv: SNone,2106 token: 22107 }2108 )2109}21102111[State 19]2112{2113 nextToken: 3,2114 present: false,2115 rowStale: false,2116 rowToken: 2,2117 touched: false,2118 ws:2119 Map(2120 "w1" ->2121 {2122 conn: false,2123 outputs: false,2124 phase: Done,2125 res: RFailed,2126 slot: false,2127 srv: SNone,2128 token: 12129 },2130 "w2" ->2131 {2132 conn: false,2133 outputs: false,2134 phase: Idle,2135 res: RNone,2136 slot: false,2137 srv: SNone,2138 token: 02139 },2140 "w3" ->2141 {2142 conn: true,2143 outputs: false,2144 phase: Building,2145 res: RNone,2146 slot: true,2147 srv: SNeed,2148 token: 22149 }2150 )2151}21522153[State 20]2154{2155 nextToken: 3,2156 present: false,2157 rowStale: false,2158 rowToken: 2,2159 touched: false,2160 ws:2161 Map(2162 "w1" ->2163 {2164 conn: false,2165 outputs: false,2166 phase: Done,2167 res: RFailed,2168 slot: false,2169 srv: SNone,2170 token: 12171 },2172 "w2" ->2173 {2174 conn: false,2175 outputs: false,2176 phase: Idle,2177 res: RNone,2178 slot: false,2179 srv: SNone,2180 token: 02181 },2182 "w3" ->2183 {2184 conn: false,2185 outputs: false,2186 phase: Building,2187 res: RNone,2188 slot: true,2189 srv: SNone,2190 token: 22191 }2192 )2193}21942195[State 21]2196{2197 nextToken: 3,2198 present: false,2199 rowStale: false,2200 rowToken: 2,2201 touched: false,2202 ws:2203 Map(2204 "w1" ->2205 {2206 conn: false,2207 outputs: false,2208 phase: Done,2209 res: RFailed,2210 slot: false,2211 srv: SNone,2212 token: 12213 },2214 "w2" ->2215 {2216 conn: false,2217 outputs: false,2218 phase: Idle,2219 res: RNone,2220 slot: false,2221 srv: SNone,2222 token: 02223 },2224 "w3" ->2225 {2226 conn: true,2227 outputs: false,2228 phase: Building,2229 res: RNone,2230 slot: true,2231 srv: SNeed,2232 token: 22233 }2234 )2235}22362237[State 22]2238{2239 nextToken: 3,2240 present: false,2241 rowStale: false,2242 rowToken: 0,2243 touched: false,2244 ws:2245 Map(2246 "w1" ->2247 {2248 conn: false,2249 outputs: false,2250 phase: Done,2251 res: RFailed,2252 slot: false,2253 srv: SNone,2254 token: 12255 },2256 "w2" ->2257 {2258 conn: false,2259 outputs: false,2260 phase: Idle,2261 res: RNone,2262 slot: false,2263 srv: SNone,2264 token: 02265 },2266 "w3" ->2267 {2268 conn: false,2269 outputs: false,2270 phase: Done,2271 res: RFailed,2272 slot: false,2273 srv: SNone,2274 token: 22275 }2276 )2277}22782279[State 23]2280{2281 nextToken: 3,2282 present: false,2283 rowStale: false,2284 rowToken: 0,2285 touched: false,2286 ws:2287 Map(2288 "w1" ->2289 {2290 conn: false,2291 outputs: false,2292 phase: Done,2293 res: RFailed,2294 slot: false,2295 srv: SNone,2296 token: 12297 },2298 "w2" ->2299 {2300 conn: true,2301 outputs: false,2302 phase: Pending,2303 res: RNone,2304 slot: true,2305 srv: SNeed,2306 token: 02307 },2308 "w3" ->2309 {2310 conn: false,2311 outputs: false,2312 phase: Done,2313 res: RFailed,2314 slot: false,2315 srv: SNone,2316 token: 22317 }2318 )2319}23202321[State 24]2322{2323 nextToken: 3,2324 present: false,2325 rowStale: false,2326 rowToken: 0,2327 touched: false,2328 ws:2329 Map(2330 "w1" ->2331 {2332 conn: false,2333 outputs: false,2334 phase: Done,2335 res: RFailed,2336 slot: false,2337 srv: SNone,2338 token: 12339 },2340 "w2" ->2341 {2342 conn: false,2343 outputs: false,2344 phase: Pending,2345 res: RNone,2346 slot: true,2347 srv: SNone,2348 token: 02349 },2350 "w3" ->2351 {2352 conn: false,2353 outputs: false,2354 phase: Done,2355 res: RFailed,2356 slot: false,2357 srv: SNone,2358 token: 22359 }2360 )2361}23622363[State 25]2364{2365 nextToken: 3,2366 present: false,2367 rowStale: false,2368 rowToken: 0,2369 touched: false,2370 ws:2371 Map(2372 "w1" ->2373 {2374 conn: false,2375 outputs: false,2376 phase: Done,2377 res: RFailed,2378 slot: false,2379 srv: SNone,2380 token: 12381 },2382 "w2" ->2383 {2384 conn: true,2385 outputs: false,2386 phase: Pending,2387 res: RNone,2388 slot: true,2389 srv: SNeed,2390 token: 02391 },2392 "w3" ->2393 {2394 conn: false,2395 outputs: false,2396 phase: Done,2397 res: RFailed,2398 slot: false,2399 srv: SNone,2400 token: 22401 }2402 )2403}24042405[State 26]2406{2407 nextToken: 3,2408 present: false,2409 rowStale: false,2410 rowToken: 0,2411 touched: false,2412 ws:2413 Map(2414 "w1" ->2415 {2416 conn: false,2417 outputs: false,2418 phase: Done,2419 res: RFailed,2420 slot: false,2421 srv: SNone,2422 token: 12423 },2424 "w2" ->2425 {2426 conn: false,2427 outputs: false,2428 phase: Pending,2429 res: RNone,2430 slot: true,2431 srv: SNone,2432 token: 02433 },2434 "w3" ->2435 {2436 conn: false,2437 outputs: false,2438 phase: Done,2439 res: RFailed,2440 slot: false,2441 srv: SNone,2442 token: 22443 }2444 )2445}24462447[State 27]2448{2449 nextToken: 3,2450 present: false,2451 rowStale: false,2452 rowToken: 0,2453 touched: false,2454 ws:2455 Map(2456 "w1" ->2457 {2458 conn: false,2459 outputs: false,2460 phase: Done,2461 res: RFailed,2462 slot: false,2463 srv: SNone,2464 token: 12465 },2466 "w2" ->2467 {2468 conn: true,2469 outputs: false,2470 phase: Pending,2471 res: RNone,2472 slot: true,2473 srv: SNeed,2474 token: 02475 },2476 "w3" ->2477 {2478 conn: false,2479 outputs: false,2480 phase: Done,2481 res: RFailed,2482 slot: false,2483 srv: SNone,2484 token: 22485 }2486 )2487}24882489[State 28]2490{2491 nextToken: 3,2492 present: false,2493 rowStale: false,2494 rowToken: 0,2495 touched: false,2496 ws:2497 Map(2498 "w1" ->2499 {2500 conn: false,2501 outputs: false,2502 phase: Done,2503 res: RFailed,2504 slot: false,2505 srv: SNone,2506 token: 12507 },2508 "w2" ->2509 {2510 conn: false,2511 outputs: false,2512 phase: Pending,2513 res: RNone,2514 slot: true,2515 srv: SNone,2516 token: 02517 },2518 "w3" ->2519 {2520 conn: false,2521 outputs: false,2522 phase: Done,2523 res: RFailed,2524 slot: false,2525 srv: SNone,2526 token: 22527 }2528 )2529}25302531[State 29]2532{2533 nextToken: 3,2534 present: false,2535 rowStale: false,2536 rowToken: 0,2537 touched: false,2538 ws:2539 Map(2540 "w1" ->2541 {2542 conn: false,2543 outputs: false,2544 phase: Done,2545 res: RFailed,2546 slot: false,2547 srv: SNone,2548 token: 12549 },2550 "w2" ->2551 {2552 conn: true,2553 outputs: false,2554 phase: Pending,2555 res: RNone,2556 slot: true,2557 srv: SNeed,2558 token: 02559 },2560 "w3" ->2561 {2562 conn: false,2563 outputs: false,2564 phase: Done,2565 res: RFailed,2566 slot: false,2567 srv: SNone,2568 token: 22569 }2570 )2571}25722573[State 30]2574{2575 nextToken: 4,2576 present: false,2577 rowStale: false,2578 rowToken: 3,2579 touched: false,2580 ws:2581 Map(2582 "w1" ->2583 {2584 conn: false,2585 outputs: false,2586 phase: Done,2587 res: RFailed,2588 slot: false,2589 srv: SNone,2590 token: 12591 },2592 "w2" ->2593 {2594 conn: true,2595 outputs: false,2596 phase: Building,2597 res: RNone,2598 slot: true,2599 srv: SHolder(3),2600 token: 32601 },2602 "w3" ->2603 {2604 conn: false,2605 outputs: false,2606 phase: Done,2607 res: RFailed,2608 slot: false,2609 srv: SNone,2610 token: 22611 }2612 )2613}26142615[ok] No violation found (340ms at 58824 traces/second).2616Trace length statistics: max=31, min=10, average=18.332617You may increase --max-samples and --max-steps.2618Use --verbosity to produce more (or less) output.2619Use --seed=0x5cd48efbabd97df --backend=rust to reproduce.