nixbot

builds

succeeded nix-grpc-store-claims-spec checks.x86_64-linux.claims-spec · build #156 · 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: true,58 outputs: false,59 phase: Pending,60 res: RNone,61 slot: true,62 srv: SNeed,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: false,78 outputs: false,79 phase: Idle,80 res: RNone,81 slot: false,82 srv: SNone,83 token: 084 }85 )86}8788[State 2]89{90 nextToken: 1,91 present: false,92 rowStale: false,93 rowToken: 0,94 touched: false,95 ws:96 Map(97 "w1" ->98 {99 conn: false,100 outputs: false,101 phase: Pending,102 res: RNone,103 slot: true,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: false,120 outputs: false,121 phase: Idle,122 res: RNone,123 slot: false,124 srv: SNone,125 token: 0126 }127 )128}129130[State 3]131{132 nextToken: 1,133 present: false,134 rowStale: false,135 rowToken: 0,136 touched: false,137 ws:138 Map(139 "w1" ->140 {141 conn: true,142 outputs: false,143 phase: Pending,144 res: RNone,145 slot: true,146 srv: SNeed,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: Idle,164 res: RNone,165 slot: false,166 srv: SNone,167 token: 0168 }169 )170}171172[State 4]173{174 nextToken: 1,175 present: false,176 rowStale: false,177 rowToken: 0,178 touched: false,179 ws:180 Map(181 "w1" ->182 {183 conn: false,184 outputs: false,185 phase: Pending,186 res: RNone,187 slot: true,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: false,204 outputs: false,205 phase: Idle,206 res: RNone,207 slot: false,208 srv: SNone,209 token: 0210 }211 )212}213214[State 5]215{216 nextToken: 1,217 present: false,218 rowStale: false,219 rowToken: 0,220 touched: false,221 ws:222 Map(223 "w1" ->224 {225 conn: true,226 outputs: false,227 phase: Pending,228 res: RNone,229 slot: true,230 srv: SNeed,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: false,246 outputs: false,247 phase: Idle,248 res: RNone,249 slot: false,250 srv: SNone,251 token: 0252 }253 )254}255256[State 6]257{258 nextToken: 1,259 present: false,260 rowStale: false,261 rowToken: 0,262 touched: false,263 ws:264 Map(265 "w1" ->266 {267 conn: false,268 outputs: false,269 phase: Pending,270 res: RNone,271 slot: true,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: Idle,290 res: RNone,291 slot: false,292 srv: SNone,293 token: 0294 }295 )296}297298[State 7]299{300 nextToken: 1,301 present: false,302 rowStale: false,303 rowToken: 0,304 touched: false,305 ws:306 Map(307 "w1" ->308 {309 conn: false,310 outputs: false,311 phase: Done,312 res: RUnavailable,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: Idle,332 res: RNone,333 slot: false,334 srv: SNone,335 token: 0336 }337 )338}339340[State 8]341{342 nextToken: 1,343 present: false,344 rowStale: false,345 rowToken: 0,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: false,362 outputs: false,363 phase: Idle,364 res: RNone,365 slot: false,366 srv: SNone,367 token: 0368 },369 "w3" ->370 {371 conn: false,372 outputs: false,373 phase: Idle,374 res: RNone,375 slot: false,376 srv: SNone,377 token: 0378 }379 )380}381382[State 9]383{384 nextToken: 1,385 present: false,386 rowStale: false,387 rowToken: 0,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: Idle,406 res: RNone,407 slot: false,408 srv: SNone,409 token: 0410 },411 "w3" ->412 {413 conn: true,414 outputs: false,415 phase: Pending,416 res: RNone,417 slot: true,418 srv: SNeed,419 token: 0420 }421 )422}423424[State 10]425{426 nextToken: 1,427 present: false,428 rowStale: false,429 rowToken: 0,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: false,446 outputs: false,447 phase: Idle,448 res: RNone,449 slot: false,450 srv: SNone,451 token: 0452 },453 "w3" ->454 {455 conn: false,456 outputs: false,457 phase: Pending,458 res: RNone,459 slot: true,460 srv: SNone,461 token: 0462 }463 )464}465466[State 11]467{468 nextToken: 1,469 present: false,470 rowStale: false,471 rowToken: 0,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: Idle,490 res: RNone,491 slot: false,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: 0504 }505 )506}507508[State 12]509{510 nextToken: 1,511 present: false,512 rowStale: false,513 rowToken: 0,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: 0546 }547 )548}549550[State 13]551{552 nextToken: 2,553 present: false,554 rowStale: false,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: Building,574 res: RNone,575 slot: true,576 srv: SHolder(1),577 token: 1578 },579 "w3" ->580 {581 conn: false,582 outputs: false,583 phase: Done,584 res: RUnavailable,585 slot: false,586 srv: SNone,587 token: 0588 }589 )590}591592[State 14]593{594 nextToken: 2,595 present: false,596 rowStale: false,597 rowToken: 0,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: Done,616 res: RUnavailable,617 slot: false,618 srv: SNone,619 token: 1620 },621 "w3" ->622 {623 conn: false,624 outputs: false,625 phase: Done,626 res: RUnavailable,627 slot: false,628 srv: SNone,629 token: 0630 }631 )632}633634[State 15]635{636 nextToken: 2,637 present: false,638 rowStale: false,639 rowToken: 0,640 touched: false,641 ws:642 Map(643 "w1" ->644 {645 conn: true,646 outputs: false,647 phase: Pending,648 res: RNone,649 slot: true,650 srv: SNeed,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: 1662 },663 "w3" ->664 {665 conn: false,666 outputs: false,667 phase: Done,668 res: RUnavailable,669 slot: false,670 srv: SNone,671 token: 0672 }673 )674}675676[State 16]677{678 nextToken: 2,679 present: false,680 rowStale: false,681 rowToken: 0,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: Idle,700 res: RNone,701 slot: false,702 srv: SNone,703 token: 0704 },705 "w3" ->706 {707 conn: false,708 outputs: false,709 phase: Done,710 res: RUnavailable,711 slot: false,712 srv: SNone,713 token: 0714 }715 )716}717718[State 17]719{720 nextToken: 2,721 present: false,722 rowStale: false,723 rowToken: 0,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: Idle,742 res: RNone,743 slot: false,744 srv: SNone,745 token: 0746 },747 "w3" ->748 {749 conn: false,750 outputs: false,751 phase: Done,752 res: RUnavailable,753 slot: false,754 srv: SNone,755 token: 0756 }757 )758}759760[State 18]761{762 nextToken: 2,763 present: false,764 rowStale: false,765 rowToken: 0,766 touched: false,767 ws:768 Map(769 "w1" ->770 {771 conn: false,772 outputs: false,773 phase: Pending,774 res: RNone,775 slot: true,776 srv: SNone,777 token: 0778 },779 "w2" ->780 {781 conn: false,782 outputs: false,783 phase: Idle,784 res: RNone,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: false,807 rowToken: 0,808 touched: false,809 ws:810 Map(811 "w1" ->812 {813 conn: true,814 outputs: false,815 phase: Pending,816 res: RNone,817 slot: true,818 srv: SNeed,819 token: 0820 },821 "w2" ->822 {823 conn: false,824 outputs: false,825 phase: Idle,826 res: RNone,827 slot: false,828 srv: SNone,829 token: 0830 },831 "w3" ->832 {833 conn: false,834 outputs: false,835 phase: Idle,836 res: RNone,837 slot: false,838 srv: SNone,839 token: 0840 }841 )842}843844[State 20]845{846 nextToken: 2,847 present: false,848 rowStale: false,849 rowToken: 0,850 touched: false,851 ws:852 Map(853 "w1" ->854 {855 conn: false,856 outputs: false,857 phase: Pending,858 res: RNone,859 slot: true,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: false,876 outputs: false,877 phase: Idle,878 res: RNone,879 slot: false,880 srv: SNone,881 token: 0882 }883 )884}885886[State 21]887{888 nextToken: 2,889 present: false,890 rowStale: false,891 rowToken: 0,892 touched: false,893 ws:894 Map(895 "w1" ->896 {897 conn: true,898 outputs: false,899 phase: Pending,900 res: RNone,901 slot: true,902 srv: SNeed,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: false,918 outputs: false,919 phase: Idle,920 res: RNone,921 slot: false,922 srv: SNone,923 token: 0924 }925 )926}927928[State 22]929{930 nextToken: 2,931 present: false,932 rowStale: false,933 rowToken: 0,934 touched: false,935 ws:936 Map(937 "w1" ->938 {939 conn: false,940 outputs: false,941 phase: Pending,942 res: RNone,943 slot: true,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: false,960 outputs: false,961 phase: Idle,962 res: RNone,963 slot: false,964 srv: SNone,965 token: 0966 }967 )968}969970[State 23]971{972 nextToken: 2,973 present: false,974 rowStale: false,975 rowToken: 0,976 touched: false,977 ws:978 Map(979 "w1" ->980 {981 conn: true,982 outputs: false,983 phase: Pending,984 res: RNone,985 slot: true,986 srv: SNeed,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: Idle,1004 res: RNone,1005 slot: false,1006 srv: SNone,1007 token: 01008 }1009 )1010}10111012[State 24]1013{1014 nextToken: 2,1015 present: false,1016 rowStale: false,1017 rowToken: 0,1018 touched: false,1019 ws:1020 Map(1021 "w1" ->1022 {1023 conn: false,1024 outputs: false,1025 phase: Pending,1026 res: RNone,1027 slot: true,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: Idle,1046 res: RNone,1047 slot: false,1048 srv: SNone,1049 token: 01050 }1051 )1052}10531054[State 25]1055{1056 nextToken: 2,1057 present: false,1058 rowStale: false,1059 rowToken: 0,1060 touched: false,1061 ws:1062 Map(1063 "w1" ->1064 {1065 conn: false,1066 outputs: false,1067 phase: Done,1068 res: RUnavailable,1069 slot: false,1070 srv: SNone,1071 token: 01072 },1073 "w2" ->1074 {1075 conn: false,1076 outputs: false,1077 phase: Idle,1078 res: RNone,1079 slot: false,1080 srv: SNone,1081 token: 01082 },1083 "w3" ->1084 {1085 conn: false,1086 outputs: false,1087 phase: Idle,1088 res: RNone,1089 slot: false,1090 srv: SNone,1091 token: 01092 }1093 )1094}10951096[State 26]1097{1098 nextToken: 2,1099 present: false,1100 rowStale: false,1101 rowToken: 0,1102 touched: false,1103 ws:1104 Map(1105 "w1" ->1106 {1107 conn: false,1108 outputs: false,1109 phase: Done,1110 res: RUnavailable,1111 slot: false,1112 srv: SNone,1113 token: 01114 },1115 "w2" ->1116 {1117 conn: true,1118 outputs: false,1119 phase: Pending,1120 res: RNone,1121 slot: true,1122 srv: SNeed,1123 token: 01124 },1125 "w3" ->1126 {1127 conn: false,1128 outputs: false,1129 phase: Idle,1130 res: RNone,1131 slot: false,1132 srv: SNone,1133 token: 01134 }1135 )1136}11371138[State 27]1139{1140 nextToken: 2,1141 present: false,1142 rowStale: false,1143 rowToken: 0,1144 touched: false,1145 ws:1146 Map(1147 "w1" ->1148 {1149 conn: false,1150 outputs: false,1151 phase: Done,1152 res: RUnavailable,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: Idle,1172 res: RNone,1173 slot: false,1174 srv: SNone,1175 token: 01176 }1177 )1178}11791180[State 28]1181{1182 nextToken: 2,1183 present: false,1184 rowStale: false,1185 rowToken: 0,1186 touched: false,1187 ws:1188 Map(1189 "w1" ->1190 {1191 conn: false,1192 outputs: false,1193 phase: Done,1194 res: RUnavailable,1195 slot: false,1196 srv: SNone,1197 token: 01198 },1199 "w2" ->1200 {1201 conn: false,1202 outputs: false,1203 phase: Done,1204 res: RUnavailable,1205 slot: false,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: 2,1225 present: false,1226 rowStale: false,1227 rowToken: 0,1228 touched: false,1229 ws:1230 Map(1231 "w1" ->1232 {1233 conn: false,1234 outputs: false,1235 phase: Done,1236 res: RUnavailable,1237 slot: false,1238 srv: SNone,1239 token: 01240 },1241 "w2" ->1242 {1243 conn: false,1244 outputs: false,1245 phase: Idle,1246 res: RNone,1247 slot: false,1248 srv: SNone,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: 2,1267 present: false,1268 rowStale: false,1269 rowToken: 0,1270 touched: false,1271 ws:1272 Map(1273 "w1" ->1274 {1275 conn: false,1276 outputs: false,1277 phase: Done,1278 res: RUnavailable,1279 slot: false,1280 srv: SNone,1281 token: 01282 },1283 "w2" ->1284 {1285 conn: true,1286 outputs: false,1287 phase: Pending,1288 res: RNone,1289 slot: true,1290 srv: SNeed,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 (408ms at 49020 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=0xceb661e7c6e06d70 --backend=rust to reproduce.1311An example execution:13121313[State 0]1314{1315 hookFixed::hook::cache: Set(),1316 hookFixed::hook::drvUploaded: false,1317 hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set()),1318 hookFixed::hook::phase: Query,1319 hookFixed::hook::restarts: 0,1320 hookFixed::hook::retries: 0,1321 hookFixed::hook::toUpload: Set()1322}13231324[State 1]1325{1326 hookFixed::hook::cache: Set(),1327 hookFixed::hook::drvUploaded: false,1328 hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set()),1329 hookFixed::hook::phase: Upload,1330 hookFixed::hook::restarts: 0,1331 hookFixed::hook::retries: 0,1332 hookFixed::hook::toUpload: Set("drv", "in")1333}13341335[State 2]1336{1337 hookFixed::hook::cache: Set(),1338 hookFixed::hook::drvUploaded: false,1339 hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1340 hookFixed::hook::phase: Upload,1341 hookFixed::hook::restarts: 1,1342 hookFixed::hook::retries: 1,1343 hookFixed::hook::toUpload: Set("drv", "in")1344}13451346[State 3]1347{1348 hookFixed::hook::cache: Set(),1349 hookFixed::hook::drvUploaded: false,1350 hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set("in")),1351 hookFixed::hook::phase: Upload,1352 hookFixed::hook::restarts: 2,1353 hookFixed::hook::retries: 2,1354 hookFixed::hook::toUpload: Set("drv", "in")1355}13561357[State 4]1358{1359 hookFixed::hook::cache: Set("drv", "in"),1360 hookFixed::hook::drvUploaded: false,1361 hookFixed::hook::local: Map("w1" -> Set("drv", "in"), "w2" -> Set("in")),1362 hookFixed::hook::phase: Build,1363 hookFixed::hook::restarts: 2,1364 hookFixed::hook::retries: 2,1365 hookFixed::hook::toUpload: Set("drv", "in")1366}13671368[State 5]1369{1370 hookFixed::hook::cache: Set("drv", "in", "out"),1371 hookFixed::hook::drvUploaded: false,1372 hookFixed::hook::local:1373 Map("w1" -> Set("drv", "in", "out"), "w2" -> Set("in")),1374 hookFixed::hook::phase: Fetch,1375 hookFixed::hook::restarts: 2,1376 hookFixed::hook::retries: 2,1377 hookFixed::hook::toUpload: Set("drv", "in")1378}13791380[State 6]1381{1382 hookFixed::hook::cache: Set("drv", "in", "out"),1383 hookFixed::hook::drvUploaded: false,1384 hookFixed::hook::local:1385 Map("w1" -> Set("drv", "in", "out"), "w2" -> Set("in")),1386 hookFixed::hook::phase: Done,1387 hookFixed::hook::restarts: 2,1388 hookFixed::hook::retries: 2,1389 hookFixed::hook::toUpload: Set("drv", "in")1390}13911392[ok] No violation found (159ms at 125786 traces/second).1393Trace length statistics: max=7, min=5, average=6.811394You may increase --max-samples and --max-steps.1395Use --verbosity to produce more (or less) output.1396Use --seed=0x222f0e0a3bfff342 --backend=rust to reproduce.1397An example execution:13981399[State 0]1400{1401 hookNoSubstituteRefs::hook::cache: Set(),1402 hookNoSubstituteRefs::hook::drvUploaded: false,1403 hookNoSubstituteRefs::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1404 hookNoSubstituteRefs::hook::phase: Query,1405 hookNoSubstituteRefs::hook::restarts: 0,1406 hookNoSubstituteRefs::hook::retries: 0,1407 hookNoSubstituteRefs::hook::toUpload: Set()1408}14091410[State 1]1411{1412 hookNoSubstituteRefs::hook::cache: Set("in"),1413 hookNoSubstituteRefs::hook::drvUploaded: false,1414 hookNoSubstituteRefs::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1415 hookNoSubstituteRefs::hook::phase: Upload,1416 hookNoSubstituteRefs::hook::restarts: 0,1417 hookNoSubstituteRefs::hook::retries: 0,1418 hookNoSubstituteRefs::hook::toUpload: Set("drv")1419}14201421[State 2]1422{1423 hookNoSubstituteRefs::hook::cache: Set("in"),1424 hookNoSubstituteRefs::hook::drvUploaded: false,1425 hookNoSubstituteRefs::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1426 hookNoSubstituteRefs::hook::phase: Failed,1427 hookNoSubstituteRefs::hook::restarts: 0,1428 hookNoSubstituteRefs::hook::retries: 0,1429 hookNoSubstituteRefs::hook::toUpload: Set("drv")1430}14311432[violation] Found an issue (179ms at 18419 traces/second).1433Use --verbosity=3 to show executions.1434Use --seed=0x21b0c40934ef3e28 --backend=rust to reproduce.1435error: Invariant violated1436An example execution:14371438[State 0]1439{1440 hookNoSubstituteDrv::hook::cache: Set(),1441 hookNoSubstituteDrv::hook::drvUploaded: false,1442 hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set("in")),1443 hookNoSubstituteDrv::hook::phase: Query,1444 hookNoSubstituteDrv::hook::restarts: 0,1445 hookNoSubstituteDrv::hook::retries: 0,1446 hookNoSubstituteDrv::hook::toUpload: Set()1447}14481449[State 1]1450{1451 hookNoSubstituteDrv::hook::cache: Set("in"),1452 hookNoSubstituteDrv::hook::drvUploaded: false,1453 hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set("in")),1454 hookNoSubstituteDrv::hook::phase: Upload,1455 hookNoSubstituteDrv::hook::restarts: 0,1456 hookNoSubstituteDrv::hook::retries: 0,1457 hookNoSubstituteDrv::hook::toUpload: Set("drv")1458}14591460[State 2]1461{1462 hookNoSubstituteDrv::hook::cache: Set("drv", "in"),1463 hookNoSubstituteDrv::hook::drvUploaded: false,1464 hookNoSubstituteDrv::hook::local:1465 Map("w1" -> Set(), "w2" -> Set("drv", "in")),1466 hookNoSubstituteDrv::hook::phase: Build,1467 hookNoSubstituteDrv::hook::restarts: 0,1468 hookNoSubstituteDrv::hook::retries: 0,1469 hookNoSubstituteDrv::hook::toUpload: Set("drv")1470}14711472[State 3]1473{1474 hookNoSubstituteDrv::hook::cache: Set("drv", "in"),1475 hookNoSubstituteDrv::hook::drvUploaded: false,1476 hookNoSubstituteDrv::hook::local:1477 Map("w1" -> Set(), "w2" -> Set("drv", "in")),1478 hookNoSubstituteDrv::hook::phase: UploadDrv,1479 hookNoSubstituteDrv::hook::restarts: 0,1480 hookNoSubstituteDrv::hook::retries: 0,1481 hookNoSubstituteDrv::hook::toUpload: Set("drv")1482}14831484[State 4]1485{1486 hookNoSubstituteDrv::hook::cache: Set("drv", "in"),1487 hookNoSubstituteDrv::hook::drvUploaded: true,1488 hookNoSubstituteDrv::hook::local:1489 Map("w1" -> Set(), "w2" -> Set("drv", "in")),1490 hookNoSubstituteDrv::hook::phase: Build,1491 hookNoSubstituteDrv::hook::restarts: 0,1492 hookNoSubstituteDrv::hook::retries: 0,1493 hookNoSubstituteDrv::hook::toUpload: Set("drv")1494}14951496[State 5]1497{1498 hookNoSubstituteDrv::hook::cache: Set("drv", "in"),1499 hookNoSubstituteDrv::hook::drvUploaded: true,1500 hookNoSubstituteDrv::hook::local:1501 Map("w1" -> Set(), "w2" -> Set("drv", "in")),1502 hookNoSubstituteDrv::hook::phase: Failed,1503 hookNoSubstituteDrv::hook::restarts: 0,1504 hookNoSubstituteDrv::hook::retries: 0,1505 hookNoSubstituteDrv::hook::toUpload: Set("drv")1506}15071508[violation] Found an issue (146ms at 24815 traces/second).1509Use --verbosity=3 to show executions.1510Use --seed=0x398ce1cf449da2d5 --backend=rust to reproduce.1511error: Invariant violated1512An example execution:15131514[State 0]1515{1516 pushFixed::push::byPath: Map(),1517 pushFixed::push::inflight: Set(),1518 pushFixed::push::left: Map(),1519 pushFixed::push::sent: Map()1520}15211522[State 1]1523{1524 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),1525 pushFixed::push::inflight: Set((3, "a"), (3, "b")),1526 pushFixed::push::left: Map(3 -> 2),1527 pushFixed::push::sent: Map(3 -> Set("a", "b"))1528}15291530[State 2]1531{1532 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),1533 pushFixed::push::inflight: Set((3, "a")),1534 pushFixed::push::left: Map(3 -> 1),1535 pushFixed::push::sent: Map(3 -> Set("a", "b"))1536}15371538[State 3]1539{1540 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),1541 pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "a")),1542 pushFixed::push::left: Map(2 -> 2, 3 -> 1),1543 pushFixed::push::sent: Map(2 -> Set("a", "b"), 3 -> Set("a", "b"))1544}15451546[State 4]1547{1548 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1549 pushFixed::push::inflight:1550 Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a")),1551 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 1),1552 pushFixed::push::sent:1553 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1554}15551556[State 5]1557{1558 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1559 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),1560 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 0),1561 pushFixed::push::sent:1562 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1563}15641565[State 6]1566{1567 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1568 pushFixed::push::inflight: Set((1, "b"), (2, "a"), (2, "b")),1569 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 0),1570 pushFixed::push::sent:1571 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1572}15731574[State 7]1575{1576 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1577 pushFixed::push::inflight: Set((1, "b"), (2, "a")),1578 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 0),1579 pushFixed::push::sent:1580 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1581}15821583[State 8]1584{1585 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1586 pushFixed::push::inflight: Set((2, "a")),1587 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 0),1588 pushFixed::push::sent:1589 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1590}15911592[State 9]1593{1594 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1595 pushFixed::push::inflight: Set(),1596 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),1597 pushFixed::push::sent:1598 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1599}16001601[ok] No violation found (114ms at 175439 traces/second).1602Trace length statistics: max=10, min=7, average=8.081603You may increase --max-samples and --max-steps.1604Use --verbosity to produce more (or less) output.1605Use --seed=0xdbaf7d45430c43ae --backend=rust to reproduce.1606An example execution:16071608[State 0]1609{1610 nextToken: 1,1611 present: false,1612 rowStale: false,1613 rowToken: 0,1614 touched: false,1615 ws:1616 Map(1617 "w1" ->1618 {1619 conn: false,1620 outputs: false,1621 phase: Idle,1622 res: RNone,1623 slot: false,1624 srv: SNone,1625 token: 01626 },1627 "w2" ->1628 {1629 conn: false,1630 outputs: false,1631 phase: Idle,1632 res: RNone,1633 slot: false,1634 srv: SNone,1635 token: 01636 },1637 "w3" ->1638 {1639 conn: false,1640 outputs: false,1641 phase: Idle,1642 res: RNone,1643 slot: false,1644 srv: SNone,1645 token: 01646 }1647 )1648}16491650[State 1]1651{1652 nextToken: 1,1653 present: false,1654 rowStale: false,1655 rowToken: 0,1656 touched: false,1657 ws:1658 Map(1659 "w1" ->1660 {1661 conn: false,1662 outputs: false,1663 phase: Idle,1664 res: RNone,1665 slot: false,1666 srv: SNone,1667 token: 01668 },1669 "w2" ->1670 {1671 conn: true,1672 outputs: false,1673 phase: Pending,1674 res: RNone,1675 slot: true,1676 srv: SNeed,1677 token: 01678 },1679 "w3" ->1680 {1681 conn: false,1682 outputs: false,1683 phase: Idle,1684 res: RNone,1685 slot: false,1686 srv: SNone,1687 token: 01688 }1689 )1690}16911692[State 2]1693{1694 nextToken: 1,1695 present: false,1696 rowStale: false,1697 rowToken: 0,1698 touched: false,1699 ws:1700 Map(1701 "w1" ->1702 {1703 conn: false,1704 outputs: false,1705 phase: Idle,1706 res: RNone,1707 slot: false,1708 srv: SNone,1709 token: 01710 },1711 "w2" ->1712 {1713 conn: false,1714 outputs: false,1715 phase: Pending,1716 res: RNone,1717 slot: true,1718 srv: SNone,1719 token: 01720 },1721 "w3" ->1722 {1723 conn: false,1724 outputs: false,1725 phase: Idle,1726 res: RNone,1727 slot: false,1728 srv: SNone,1729 token: 01730 }1731 )1732}17331734[State 3]1735{1736 nextToken: 1,1737 present: false,1738 rowStale: false,1739 rowToken: 0,1740 touched: false,1741 ws:1742 Map(1743 "w1" ->1744 {1745 conn: false,1746 outputs: false,1747 phase: Idle,1748 res: RNone,1749 slot: false,1750 srv: SNone,1751 token: 01752 },1753 "w2" ->1754 {1755 conn: true,1756 outputs: false,1757 phase: Pending,1758 res: RNone,1759 slot: true,1760 srv: SNeed,1761 token: 01762 },1763 "w3" ->1764 {1765 conn: false,1766 outputs: false,1767 phase: Idle,1768 res: RNone,1769 slot: false,1770 srv: SNone,1771 token: 01772 }1773 )1774}17751776[State 4]1777{1778 nextToken: 1,1779 present: false,1780 rowStale: false,1781 rowToken: 0,1782 touched: false,1783 ws:1784 Map(1785 "w1" ->1786 {1787 conn: false,1788 outputs: false,1789 phase: Idle,1790 res: RNone,1791 slot: false,1792 srv: SNone,1793 token: 01794 },1795 "w2" ->1796 {1797 conn: false,1798 outputs: false,1799 phase: Pending,1800 res: RNone,1801 slot: true,1802 srv: SNone,1803 token: 01804 },1805 "w3" ->1806 {1807 conn: false,1808 outputs: false,1809 phase: Idle,1810 res: RNone,1811 slot: false,1812 srv: SNone,1813 token: 01814 }1815 )1816}18171818[State 5]1819{1820 nextToken: 1,1821 present: false,1822 rowStale: false,1823 rowToken: 0,1824 touched: false,1825 ws:1826 Map(1827 "w1" ->1828 {1829 conn: false,1830 outputs: false,1831 phase: Idle,1832 res: RNone,1833 slot: false,1834 srv: SNone,1835 token: 01836 },1837 "w2" ->1838 {1839 conn: true,1840 outputs: false,1841 phase: Pending,1842 res: RNone,1843 slot: true,1844 srv: SNeed,1845 token: 01846 },1847 "w3" ->1848 {1849 conn: false,1850 outputs: false,1851 phase: Idle,1852 res: RNone,1853 slot: false,1854 srv: SNone,1855 token: 01856 }1857 )1858}18591860[State 6]1861{1862 nextToken: 1,1863 present: false,1864 rowStale: false,1865 rowToken: 0,1866 touched: false,1867 ws:1868 Map(1869 "w1" ->1870 {1871 conn: false,1872 outputs: false,1873 phase: Idle,1874 res: RNone,1875 slot: false,1876 srv: SNone,1877 token: 01878 },1879 "w2" ->1880 {1881 conn: false,1882 outputs: false,1883 phase: Pending,1884 res: RNone,1885 slot: true,1886 srv: SNone,1887 token: 01888 },1889 "w3" ->1890 {1891 conn: false,1892 outputs: false,1893 phase: Idle,1894 res: RNone,1895 slot: false,1896 srv: SNone,1897 token: 01898 }1899 )1900}19011902[State 7]1903{1904 nextToken: 1,1905 present: false,1906 rowStale: false,1907 rowToken: 0,1908 touched: false,1909 ws:1910 Map(1911 "w1" ->1912 {1913 conn: false,1914 outputs: false,1915 phase: Idle,1916 res: RNone,1917 slot: false,1918 srv: SNone,1919 token: 01920 },1921 "w2" ->1922 {1923 conn: true,1924 outputs: false,1925 phase: Pending,1926 res: RNone,1927 slot: true,1928 srv: SNeed,1929 token: 01930 },1931 "w3" ->1932 {1933 conn: false,1934 outputs: false,1935 phase: Idle,1936 res: RNone,1937 slot: false,1938 srv: SNone,1939 token: 01940 }1941 )1942}19431944[State 8]1945{1946 nextToken: 1,1947 present: false,1948 rowStale: false,1949 rowToken: 0,1950 touched: false,1951 ws:1952 Map(1953 "w1" ->1954 {1955 conn: false,1956 outputs: false,1957 phase: Idle,1958 res: RNone,1959 slot: false,1960 srv: SNone,1961 token: 01962 },1963 "w2" ->1964 {1965 conn: false,1966 outputs: false,1967 phase: Pending,1968 res: RNone,1969 slot: true,1970 srv: SNone,1971 token: 01972 },1973 "w3" ->1974 {1975 conn: false,1976 outputs: false,1977 phase: Idle,1978 res: RNone,1979 slot: false,1980 srv: SNone,1981 token: 01982 }1983 )1984}19851986[State 9]1987{1988 nextToken: 1,1989 present: false,1990 rowStale: false,1991 rowToken: 0,1992 touched: false,1993 ws:1994 Map(1995 "w1" ->1996 {1997 conn: false,1998 outputs: false,1999 phase: Idle,2000 res: RNone,2001 slot: false,2002 srv: SNone,2003 token: 02004 },2005 "w2" ->2006 {2007 conn: true,2008 outputs: false,2009 phase: Pending,2010 res: RNone,2011 slot: true,2012 srv: SNeed,2013 token: 02014 },2015 "w3" ->2016 {2017 conn: false,2018 outputs: false,2019 phase: Idle,2020 res: RNone,2021 slot: false,2022 srv: SNone,2023 token: 02024 }2025 )2026}20272028[State 10]2029{2030 nextToken: 1,2031 present: false,2032 rowStale: false,2033 rowToken: 0,2034 touched: false,2035 ws:2036 Map(2037 "w1" ->2038 {2039 conn: false,2040 outputs: false,2041 phase: Idle,2042 res: RNone,2043 slot: false,2044 srv: SNone,2045 token: 02046 },2047 "w2" ->2048 {2049 conn: false,2050 outputs: false,2051 phase: Pending,2052 res: RNone,2053 slot: true,2054 srv: SNone,2055 token: 02056 },2057 "w3" ->2058 {2059 conn: false,2060 outputs: false,2061 phase: Idle,2062 res: RNone,2063 slot: false,2064 srv: SNone,2065 token: 02066 }2067 )2068}20692070[State 11]2071{2072 nextToken: 1,2073 present: false,2074 rowStale: false,2075 rowToken: 0,2076 touched: false,2077 ws:2078 Map(2079 "w1" ->2080 {2081 conn: false,2082 outputs: false,2083 phase: Idle,2084 res: RNone,2085 slot: false,2086 srv: SNone,2087 token: 02088 },2089 "w2" ->2090 {2091 conn: true,2092 outputs: false,2093 phase: Pending,2094 res: RNone,2095 slot: true,2096 srv: SNeed,2097 token: 02098 },2099 "w3" ->2100 {2101 conn: false,2102 outputs: false,2103 phase: Idle,2104 res: RNone,2105 slot: false,2106 srv: SNone,2107 token: 02108 }2109 )2110}21112112[State 12]2113{2114 nextToken: 2,2115 present: false,2116 rowStale: false,2117 rowToken: 1,2118 touched: false,2119 ws:2120 Map(2121 "w1" ->2122 {2123 conn: false,2124 outputs: false,2125 phase: Idle,2126 res: RNone,2127 slot: false,2128 srv: SNone,2129 token: 02130 },2131 "w2" ->2132 {2133 conn: true,2134 outputs: false,2135 phase: Building,2136 res: RNone,2137 slot: true,2138 srv: SHolder(1),2139 token: 12140 },2141 "w3" ->2142 {2143 conn: false,2144 outputs: false,2145 phase: Idle,2146 res: RNone,2147 slot: false,2148 srv: SNone,2149 token: 02150 }2151 )2152}21532154[State 13]2155{2156 nextToken: 2,2157 present: false,2158 rowStale: false,2159 rowToken: 0,2160 touched: false,2161 ws:2162 Map(2163 "w1" ->2164 {2165 conn: false,2166 outputs: false,2167 phase: Idle,2168 res: RNone,2169 slot: false,2170 srv: SNone,2171 token: 02172 },2173 "w2" ->2174 {2175 conn: false,2176 outputs: false,2177 phase: Done,2178 res: RUnavailable,2179 slot: false,2180 srv: SNone,2181 token: 12182 },2183 "w3" ->2184 {2185 conn: false,2186 outputs: false,2187 phase: Idle,2188 res: RNone,2189 slot: false,2190 srv: SNone,2191 token: 02192 }2193 )2194}21952196[State 14]2197{2198 nextToken: 2,2199 present: false,2200 rowStale: false,2201 rowToken: 0,2202 touched: false,2203 ws:2204 Map(2205 "w1" ->2206 {2207 conn: false,2208 outputs: false,2209 phase: Idle,2210 res: RNone,2211 slot: false,2212 srv: SNone,2213 token: 02214 },2215 "w2" ->2216 {2217 conn: false,2218 outputs: false,2219 phase: Done,2220 res: RUnavailable,2221 slot: false,2222 srv: SNone,2223 token: 12224 },2225 "w3" ->2226 {2227 conn: true,2228 outputs: false,2229 phase: Pending,2230 res: RNone,2231 slot: true,2232 srv: SNeed,2233 token: 02234 }2235 )2236}22372238[State 15]2239{2240 nextToken: 3,2241 present: false,2242 rowStale: false,2243 rowToken: 2,2244 touched: false,2245 ws:2246 Map(2247 "w1" ->2248 {2249 conn: false,2250 outputs: false,2251 phase: Idle,2252 res: RNone,2253 slot: false,2254 srv: SNone,2255 token: 02256 },2257 "w2" ->2258 {2259 conn: false,2260 outputs: false,2261 phase: Done,2262 res: RUnavailable,2263 slot: false,2264 srv: SNone,2265 token: 12266 },2267 "w3" ->2268 {2269 conn: true,2270 outputs: false,2271 phase: Building,2272 res: RNone,2273 slot: true,2274 srv: SHolder(2),2275 token: 22276 }2277 )2278}22792280[State 16]2281{2282 nextToken: 3,2283 present: false,2284 rowStale: false,2285 rowToken: 2,2286 touched: false,2287 ws:2288 Map(2289 "w1" ->2290 {2291 conn: false,2292 outputs: false,2293 phase: Idle,2294 res: RNone,2295 slot: false,2296 srv: SNone,2297 token: 02298 },2299 "w2" ->2300 {2301 conn: false,2302 outputs: false,2303 phase: Done,2304 res: RUnavailable,2305 slot: false,2306 srv: SNone,2307 token: 12308 },2309 "w3" ->2310 {2311 conn: false,2312 outputs: false,2313 phase: Building,2314 res: RNone,2315 slot: true,2316 srv: SNone,2317 token: 22318 }2319 )2320}23212322[State 17]2323{2324 nextToken: 3,2325 present: false,2326 rowStale: false,2327 rowToken: 2,2328 touched: false,2329 ws:2330 Map(2331 "w1" ->2332 {2333 conn: false,2334 outputs: false,2335 phase: Idle,2336 res: RNone,2337 slot: false,2338 srv: SNone,2339 token: 02340 },2341 "w2" ->2342 {2343 conn: false,2344 outputs: false,2345 phase: Done,2346 res: RUnavailable,2347 slot: false,2348 srv: SNone,2349 token: 12350 },2351 "w3" ->2352 {2353 conn: true,2354 outputs: false,2355 phase: Building,2356 res: RNone,2357 slot: true,2358 srv: SNeed,2359 token: 22360 }2361 )2362}23632364[State 18]2365{2366 nextToken: 3,2367 present: false,2368 rowStale: false,2369 rowToken: 0,2370 touched: false,2371 ws:2372 Map(2373 "w1" ->2374 {2375 conn: false,2376 outputs: false,2377 phase: Idle,2378 res: RNone,2379 slot: false,2380 srv: SNone,2381 token: 02382 },2383 "w2" ->2384 {2385 conn: false,2386 outputs: false,2387 phase: Done,2388 res: RUnavailable,2389 slot: false,2390 srv: SNone,2391 token: 12392 },2393 "w3" ->2394 {2395 conn: false,2396 outputs: false,2397 phase: Done,2398 res: RUnavailable,2399 slot: false,2400 srv: SNone,2401 token: 22402 }2403 )2404}24052406[State 19]2407{2408 nextToken: 3,2409 present: false,2410 rowStale: false,2411 rowToken: 0,2412 touched: false,2413 ws:2414 Map(2415 "w1" ->2416 {2417 conn: true,2418 outputs: false,2419 phase: Pending,2420 res: RNone,2421 slot: true,2422 srv: SNeed,2423 token: 02424 },2425 "w2" ->2426 {2427 conn: false,2428 outputs: false,2429 phase: Done,2430 res: RUnavailable,2431 slot: false,2432 srv: SNone,2433 token: 12434 },2435 "w3" ->2436 {2437 conn: false,2438 outputs: false,2439 phase: Done,2440 res: RUnavailable,2441 slot: false,2442 srv: SNone,2443 token: 22444 }2445 )2446}24472448[State 20]2449{2450 nextToken: 3,2451 present: false,2452 rowStale: false,2453 rowToken: 0,2454 touched: false,2455 ws:2456 Map(2457 "w1" ->2458 {2459 conn: false,2460 outputs: false,2461 phase: Pending,2462 res: RNone,2463 slot: true,2464 srv: SNone,2465 token: 02466 },2467 "w2" ->2468 {2469 conn: false,2470 outputs: false,2471 phase: Done,2472 res: RUnavailable,2473 slot: false,2474 srv: SNone,2475 token: 12476 },2477 "w3" ->2478 {2479 conn: false,2480 outputs: false,2481 phase: Done,2482 res: RUnavailable,2483 slot: false,2484 srv: SNone,2485 token: 22486 }2487 )2488}24892490[State 21]2491{2492 nextToken: 3,2493 present: false,2494 rowStale: false,2495 rowToken: 0,2496 touched: false,2497 ws:2498 Map(2499 "w1" ->2500 {2501 conn: true,2502 outputs: false,2503 phase: Pending,2504 res: RNone,2505 slot: true,2506 srv: SNeed,2507 token: 02508 },2509 "w2" ->2510 {2511 conn: false,2512 outputs: false,2513 phase: Done,2514 res: RUnavailable,2515 slot: false,2516 srv: SNone,2517 token: 12518 },2519 "w3" ->2520 {2521 conn: false,2522 outputs: false,2523 phase: Done,2524 res: RUnavailable,2525 slot: false,2526 srv: SNone,2527 token: 22528 }2529 )2530}25312532[State 22]2533{2534 nextToken: 3,2535 present: false,2536 rowStale: false,2537 rowToken: 0,2538 touched: false,2539 ws:2540 Map(2541 "w1" ->2542 {2543 conn: false,2544 outputs: false,2545 phase: Pending,2546 res: RNone,2547 slot: true,2548 srv: SNone,2549 token: 02550 },2551 "w2" ->2552 {2553 conn: false,2554 outputs: false,2555 phase: Done,2556 res: RUnavailable,2557 slot: false,2558 srv: SNone,2559 token: 12560 },2561 "w3" ->2562 {2563 conn: false,2564 outputs: false,2565 phase: Done,2566 res: RUnavailable,2567 slot: false,2568 srv: SNone,2569 token: 22570 }2571 )2572}25732574[State 23]2575{2576 nextToken: 3,2577 present: false,2578 rowStale: false,2579 rowToken: 0,2580 touched: false,2581 ws:2582 Map(2583 "w1" ->2584 {2585 conn: true,2586 outputs: false,2587 phase: Pending,2588 res: RNone,2589 slot: true,2590 srv: SNeed,2591 token: 02592 },2593 "w2" ->2594 {2595 conn: false,2596 outputs: false,2597 phase: Done,2598 res: RUnavailable,2599 slot: false,2600 srv: SNone,2601 token: 12602 },2603 "w3" ->2604 {2605 conn: false,2606 outputs: false,2607 phase: Done,2608 res: RUnavailable,2609 slot: false,2610 srv: SNone,2611 token: 22612 }2613 )2614}26152616[State 24]2617{2618 nextToken: 4,2619 present: false,2620 rowStale: false,2621 rowToken: 3,2622 touched: false,2623 ws:2624 Map(2625 "w1" ->2626 {2627 conn: true,2628 outputs: false,2629 phase: Building,2630 res: RNone,2631 slot: true,2632 srv: SHolder(3),2633 token: 32634 },2635 "w2" ->2636 {2637 conn: false,2638 outputs: false,2639 phase: Done,2640 res: RUnavailable,2641 slot: false,2642 srv: SNone,2643 token: 12644 },2645 "w3" ->2646 {2647 conn: false,2648 outputs: false,2649 phase: Done,2650 res: RUnavailable,2651 slot: false,2652 srv: SNone,2653 token: 22654 }2655 )2656}26572658[State 25]2659{2660 nextToken: 4,2661 present: false,2662 rowStale: false,2663 rowToken: 3,2664 touched: false,2665 ws:2666 Map(2667 "w1" ->2668 {2669 conn: false,2670 outputs: false,2671 phase: Building,2672 res: RNone,2673 slot: true,2674 srv: SNone,2675 token: 32676 },2677 "w2" ->2678 {2679 conn: false,2680 outputs: false,2681 phase: Done,2682 res: RUnavailable,2683 slot: false,2684 srv: SNone,2685 token: 12686 },2687 "w3" ->2688 {2689 conn: false,2690 outputs: false,2691 phase: Done,2692 res: RUnavailable,2693 slot: false,2694 srv: SNone,2695 token: 22696 }2697 )2698}26992700[State 26]2701{2702 nextToken: 4,2703 present: false,2704 rowStale: false,2705 rowToken: 3,2706 touched: false,2707 ws:2708 Map(2709 "w1" ->2710 {2711 conn: true,2712 outputs: false,2713 phase: Building,2714 res: RNone,2715 slot: true,2716 srv: SNeed,2717 token: 32718 },2719 "w2" ->2720 {2721 conn: false,2722 outputs: false,2723 phase: Done,2724 res: RUnavailable,2725 slot: false,2726 srv: SNone,2727 token: 12728 },2729 "w3" ->2730 {2731 conn: false,2732 outputs: false,2733 phase: Done,2734 res: RUnavailable,2735 slot: false,2736 srv: SNone,2737 token: 22738 }2739 )2740}27412742[State 27]2743{2744 nextToken: 4,2745 present: false,2746 rowStale: false,2747 rowToken: 3,2748 touched: false,2749 ws:2750 Map(2751 "w1" ->2752 {2753 conn: true,2754 outputs: false,2755 phase: Building,2756 res: RNone,2757 slot: true,2758 srv: SHolder(3),2759 token: 32760 },2761 "w2" ->2762 {2763 conn: false,2764 outputs: false,2765 phase: Done,2766 res: RUnavailable,2767 slot: false,2768 srv: SNone,2769 token: 12770 },2771 "w3" ->2772 {2773 conn: false,2774 outputs: false,2775 phase: Done,2776 res: RUnavailable,2777 slot: false,2778 srv: SNone,2779 token: 22780 }2781 )2782}27832784[State 28]2785{2786 nextToken: 4,2787 present: false,2788 rowStale: false,2789 rowToken: 3,2790 touched: false,2791 ws:2792 Map(2793 "w1" ->2794 {2795 conn: false,2796 outputs: false,2797 phase: Building,2798 res: RNone,2799 slot: true,2800 srv: SNone,2801 token: 32802 },2803 "w2" ->2804 {2805 conn: false,2806 outputs: false,2807 phase: Done,2808 res: RUnavailable,2809 slot: false,2810 srv: SNone,2811 token: 12812 },2813 "w3" ->2814 {2815 conn: false,2816 outputs: false,2817 phase: Done,2818 res: RUnavailable,2819 slot: false,2820 srv: SNone,2821 token: 22822 }2823 )2824}28252826[State 29]2827{2828 nextToken: 4,2829 present: false,2830 rowStale: false,2831 rowToken: 3,2832 touched: false,2833 ws:2834 Map(2835 "w1" ->2836 {2837 conn: true,2838 outputs: false,2839 phase: Building,2840 res: RNone,2841 slot: true,2842 srv: SNeed,2843 token: 32844 },2845 "w2" ->2846 {2847 conn: false,2848 outputs: false,2849 phase: Done,2850 res: RUnavailable,2851 slot: false,2852 srv: SNone,2853 token: 12854 },2855 "w3" ->2856 {2857 conn: false,2858 outputs: false,2859 phase: Done,2860 res: RUnavailable,2861 slot: false,2862 srv: SNone,2863 token: 22864 }2865 )2866}28672868[State 30]2869{2870 nextToken: 4,2871 present: false,2872 rowStale: false,2873 rowToken: 3,2874 touched: false,2875 ws:2876 Map(2877 "w1" ->2878 {2879 conn: false,2880 outputs: false,2881 phase: Building,2882 res: RNone,2883 slot: true,2884 srv: SNone,2885 token: 32886 },2887 "w2" ->2888 {2889 conn: false,2890 outputs: false,2891 phase: Done,2892 res: RUnavailable,2893 slot: false,2894 srv: SNone,2895 token: 12896 },2897 "w3" ->2898 {2899 conn: false,2900 outputs: false,2901 phase: Done,2902 res: RUnavailable,2903 slot: false,2904 srv: SNone,2905 token: 22906 }2907 )2908}29092910[ok] No violation found (367ms at 54496 traces/second).2911Trace length statistics: max=31, min=10, average=18.102912You may increase --max-samples and --max-steps.2913Use --verbosity to produce more (or less) output.2914Use --seed=0x18501680ac21c29d --backend=rust to reproduce.