nixbot

builds
sign in

nix-grpc-store-claims-spec checks.aarch64-linux.claims-spec · build #156 · raw

1tribuchet: building on eliza2An 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: 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: 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: false,120 outputs: false,121 phase: Pending,122 res: RNone,123 slot: true,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: 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: Done,164 res: RUnavailable,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: Idle,186 res: RNone,187 slot: false,188 srv: SNone,189 token: 0190 },191 "w2" ->192 {193 conn: true,194 outputs: false,195 phase: Pending,196 res: RNone,197 slot: true,198 srv: SNeed,199 token: 0200 },201 "w3" ->202 {203 conn: false,204 outputs: false,205 phase: Done,206 res: RUnavailable,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: 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: Pending,238 res: RNone,239 slot: true,240 srv: SNone,241 token: 0242 },243 "w3" ->244 {245 conn: false,246 outputs: false,247 phase: Done,248 res: RUnavailable,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: Idle,270 res: RNone,271 slot: false,272 srv: SNone,273 token: 0274 },275 "w2" ->276 {277 conn: false,278 outputs: false,279 phase: Done,280 res: RUnavailable,281 slot: false,282 srv: SNone,283 token: 0284 },285 "w3" ->286 {287 conn: false,288 outputs: false,289 phase: Done,290 res: RUnavailable,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: Idle,312 res: RNone,313 slot: false,314 srv: SNone,315 token: 0316 },317 "w2" ->318 {319 conn: false,320 outputs: false,321 phase: Done,322 res: RUnavailable,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: true,352 outputs: false,353 phase: Pending,354 res: RNone,355 slot: true,356 srv: SNeed,357 token: 0358 },359 "w2" ->360 {361 conn: false,362 outputs: false,363 phase: Done,364 res: RUnavailable,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: Pending,396 res: RNone,397 slot: true,398 srv: SNone,399 token: 0400 },401 "w2" ->402 {403 conn: false,404 outputs: false,405 phase: Done,406 res: RUnavailable,407 slot: false,408 srv: SNone,409 token: 0410 },411 "w3" ->412 {413 conn: false,414 outputs: false,415 phase: Idle,416 res: RNone,417 slot: false,418 srv: SNone,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: Pending,438 res: RNone,439 slot: true,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: Idle,458 res: RNone,459 slot: false,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: true,478 outputs: false,479 phase: Pending,480 res: RNone,481 slot: true,482 srv: SNeed,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: Idle,500 res: RNone,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: Pending,522 res: RNone,523 slot: true,524 srv: SNone,525 token: 0526 },527 "w2" ->528 {529 conn: false,530 outputs: false,531 phase: Idle,532 res: RNone,533 slot: false,534 srv: SNone,535 token: 0536 },537 "w3" ->538 {539 conn: false,540 outputs: false,541 phase: Idle,542 res: RNone,543 slot: false,544 srv: SNone,545 token: 0546 }547 )548}549550[State 13]551{552 nextToken: 1,553 present: false,554 rowStale: false,555 rowToken: 0,556 touched: false,557 ws:558 Map(559 "w1" ->560 {561 conn: false,562 outputs: false,563 phase: Done,564 res: RUnavailable,565 slot: false,566 srv: SNone,567 token: 0568 },569 "w2" ->570 {571 conn: false,572 outputs: false,573 phase: Idle,574 res: RNone,575 slot: false,576 srv: SNone,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: 1,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: Done,606 res: RUnavailable,607 slot: false,608 srv: SNone,609 token: 0610 },611 "w2" ->612 {613 conn: false,614 outputs: false,615 phase: Idle,616 res: RNone,617 slot: false,618 srv: SNone,619 token: 0620 },621 "w3" ->622 {623 conn: true,624 outputs: false,625 phase: Pending,626 res: RNone,627 slot: true,628 srv: SNeed,629 token: 0630 }631 )632}633634[State 15]635{636 nextToken: 2,637 present: false,638 rowStale: false,639 rowToken: 1,640 touched: false,641 ws:642 Map(643 "w1" ->644 {645 conn: false,646 outputs: false,647 phase: Done,648 res: RUnavailable,649 slot: false,650 srv: SNone,651 token: 0652 },653 "w2" ->654 {655 conn: false,656 outputs: false,657 phase: Idle,658 res: RNone,659 slot: false,660 srv: SNone,661 token: 0662 },663 "w3" ->664 {665 conn: true,666 outputs: false,667 phase: Building,668 res: RNone,669 slot: true,670 srv: SHolder(1),671 token: 1672 }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: false,688 outputs: false,689 phase: Done,690 res: RUnavailable,691 slot: false,692 srv: SNone,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: 1714 }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: Done,732 res: RUnavailable,733 slot: false,734 srv: SNone,735 token: 0736 },737 "w2" ->738 {739 conn: true,740 outputs: false,741 phase: Pending,742 res: RNone,743 slot: true,744 srv: SNeed,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: 1756 }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: Done,774 res: RUnavailable,775 slot: false,776 srv: SNone,777 token: 0778 },779 "w2" ->780 {781 conn: true,782 outputs: false,783 phase: Pending,784 res: RNone,785 slot: true,786 srv: SNeed,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: false,814 outputs: false,815 phase: Idle,816 res: RNone,817 slot: false,818 srv: SNone,819 token: 0820 },821 "w2" ->822 {823 conn: true,824 outputs: false,825 phase: Pending,826 res: RNone,827 slot: true,828 srv: SNeed,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: 3,847 present: false,848 rowStale: false,849 rowToken: 2,850 touched: false,851 ws:852 Map(853 "w1" ->854 {855 conn: false,856 outputs: false,857 phase: Idle,858 res: RNone,859 slot: false,860 srv: SNone,861 token: 0862 },863 "w2" ->864 {865 conn: true,866 outputs: false,867 phase: Building,868 res: RNone,869 slot: true,870 srv: SHolder(2),871 token: 2872 },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: 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: Idle,900 res: RNone,901 slot: false,902 srv: SNone,903 token: 0904 },905 "w2" ->906 {907 conn: false,908 outputs: false,909 phase: Building,910 res: RNone,911 slot: true,912 srv: SNone,913 token: 2914 },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: 3,931 present: false,932 rowStale: true,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: Building,952 res: RNone,953 slot: true,954 srv: SNone,955 token: 2956 },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: 3,973 present: false,974 rowStale: true,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: Done,994 res: RUnavailable,995 slot: false,996 srv: SNone,997 token: 2998 },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: 3,1015 present: false,1016 rowStale: true,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: Idle,1046 res: RNone,1047 slot: false,1048 srv: SNone,1049 token: 01050 }1051 )1052}10531054[State 25]1055{1056 nextToken: 3,1057 present: false,1058 rowStale: true,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: Idle,1088 res: RNone,1089 slot: false,1090 srv: SNone,1091 token: 01092 }1093 )1094}10951096[State 26]1097{1098 nextToken: 4,1099 present: false,1100 rowStale: false,1101 rowToken: 3,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: true,1118 outputs: false,1119 phase: Building,1120 res: RNone,1121 slot: true,1122 srv: SHolder(3),1123 token: 31124 },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: 4,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: Idle,1152 res: RNone,1153 slot: false,1154 srv: SNone,1155 token: 01156 },1157 "w2" ->1158 {1159 conn: false,1160 outputs: false,1161 phase: Done,1162 res: RUnavailable,1163 slot: false,1164 srv: SNone,1165 token: 31166 },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: 4,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: Idle,1194 res: RNone,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: 31208 },1209 "w3" ->1210 {1211 conn: true,1212 outputs: false,1213 phase: Pending,1214 res: RNone,1215 slot: true,1216 srv: SNeed,1217 token: 01218 }1219 )1220}12211222[State 29]1223{1224 nextToken: 4,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: Idle,1236 res: RNone,1237 slot: false,1238 srv: SNone,1239 token: 01240 },1241 "w2" ->1242 {1243 conn: false,1244 outputs: false,1245 phase: Done,1246 res: RUnavailable,1247 slot: false,1248 srv: SNone,1249 token: 31250 },1251 "w3" ->1252 {1253 conn: false,1254 outputs: false,1255 phase: Pending,1256 res: RNone,1257 slot: true,1258 srv: SNone,1259 token: 01260 }1261 )1262}12631264[State 30]1265{1266 nextToken: 4,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: Idle,1278 res: RNone,1279 slot: false,1280 srv: SNone,1281 token: 01282 },1283 "w2" ->1284 {1285 conn: false,1286 outputs: false,1287 phase: Idle,1288 res: RNone,1289 slot: false,1290 srv: SNone,1291 token: 01292 },1293 "w3" ->1294 {1295 conn: false,1296 outputs: false,1297 phase: Pending,1298 res: RNone,1299 slot: true,1300 srv: SNone,1301 token: 01302 }1303 )1304}13051306[ok] No violation found (498ms at 40161 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=0xd44067200ec46775 --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("in"), "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("in"),1327 hookFixed::hook::drvUploaded: false,1328 hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1329 hookFixed::hook::phase: Upload,1330 hookFixed::hook::restarts: 0,1331 hookFixed::hook::retries: 0,1332 hookFixed::hook::toUpload: Set("drv")1333}13341335[State 2]1336{1337 hookFixed::hook::cache: Set("in"),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")1344}13451346[State 3]1347{1348 hookFixed::hook::cache: Set("in"),1349 hookFixed::hook::drvUploaded: false,1350 hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set("drv")),1351 hookFixed::hook::phase: Upload,1352 hookFixed::hook::restarts: 2,1353 hookFixed::hook::retries: 2,1354 hookFixed::hook::toUpload: Set("drv")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("drv")),1362 hookFixed::hook::phase: Build,1363 hookFixed::hook::restarts: 2,1364 hookFixed::hook::retries: 2,1365 hookFixed::hook::toUpload: Set("drv")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"), "w2" -> Set("drv", "in", "out")),1374 hookFixed::hook::phase: Fetch,1375 hookFixed::hook::restarts: 2,1376 hookFixed::hook::retries: 2,1377 hookFixed::hook::toUpload: Set("drv")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"), "w2" -> Set("drv", "in", "out")),1386 hookFixed::hook::phase: Done,1387 hookFixed::hook::restarts: 2,1388 hookFixed::hook::retries: 2,1389 hookFixed::hook::toUpload: Set("drv")1390}13911392[ok] No violation found (111ms at 180180 traces/second).1393Trace length statistics: max=7, min=5, average=6.751394You may increase --max-samples and --max-steps.1395Use --verbosity to produce more (or less) output.1396Use --seed=0x136369ae0b3fba3e --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 (67ms at 22164 traces/second).1433Use --verbosity=3 to show executions.1434Use --seed=0x130e35162a30c779 --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()),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(),1452 hookNoSubstituteDrv::hook::drvUploaded: false,1453 hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set()),1454 hookNoSubstituteDrv::hook::phase: Upload,1455 hookNoSubstituteDrv::hook::restarts: 0,1456 hookNoSubstituteDrv::hook::retries: 0,1457 hookNoSubstituteDrv::hook::toUpload: Set("drv", "in")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", "in")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", "in")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", "in")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", "in")1506}15071508[violation] Found an issue (85ms at 22482 traces/second).1509Use --verbosity=3 to show executions.1510Use --seed=0x8c31480bd064c82 --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" -> 1, "b" -> 1),1525 pushFixed::push::inflight: Set((1, "a"), (1, "b")),1526 pushFixed::push::left: Map(1 -> 2),1527 pushFixed::push::sent: Map(1 -> Set("a", "b"))1528}15291530[State 2]1531{1532 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1533 pushFixed::push::inflight: Set((1, "a")),1534 pushFixed::push::left: Map(1 -> 1),1535 pushFixed::push::sent: Map(1 -> Set("a", "b"))1536}15371538[State 3]1539{1540 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),1541 pushFixed::push::inflight: Set((1, "a"), (2, "a"), (2, "b")),1542 pushFixed::push::left: Map(1 -> 1, 2 -> 2),1543 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))1544}15451546[State 4]1547{1548 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),1549 pushFixed::push::inflight: Set((2, "a"), (2, "b")),1550 pushFixed::push::left: Map(1 -> 0, 2 -> 2),1551 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))1552}15531554[State 5]1555{1556 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),1557 pushFixed::push::inflight: Set((2, "b")),1558 pushFixed::push::left: Map(1 -> 0, 2 -> 1),1559 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))1560}15611562[State 6]1563{1564 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),1565 pushFixed::push::inflight: Set((2, "b"), (3, "a"), (3, "b")),1566 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 2),1567 pushFixed::push::sent:1568 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1569}15701571[State 7]1572{1573 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),1574 pushFixed::push::inflight: Set((2, "b"), (3, "a")),1575 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 1),1576 pushFixed::push::sent:1577 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1578}15791580[State 8]1581{1582 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),1583 pushFixed::push::inflight: Set((2, "b")),1584 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 0),1585 pushFixed::push::sent:1586 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1587}15881589[State 9]1590{1591 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),1592 pushFixed::push::inflight: Set(),1593 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),1594 pushFixed::push::sent:1595 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1596}15971598[ok] No violation found (115ms at 173913 traces/second).1599Trace length statistics: max=10, min=7, average=7.931600You may increase --max-samples and --max-steps.1601Use --verbosity to produce more (or less) output.1602Use --seed=0x180e43fdadf691a2 --backend=rust to reproduce.1603An example execution:16041605[State 0]1606{1607 nextToken: 1,1608 present: false,1609 rowStale: false,1610 rowToken: 0,1611 touched: false,1612 ws:1613 Map(1614 "w1" ->1615 {1616 conn: false,1617 outputs: false,1618 phase: Idle,1619 res: RNone,1620 slot: false,1621 srv: SNone,1622 token: 01623 },1624 "w2" ->1625 {1626 conn: false,1627 outputs: false,1628 phase: Idle,1629 res: RNone,1630 slot: false,1631 srv: SNone,1632 token: 01633 },1634 "w3" ->1635 {1636 conn: false,1637 outputs: false,1638 phase: Idle,1639 res: RNone,1640 slot: false,1641 srv: SNone,1642 token: 01643 }1644 )1645}16461647[State 1]1648{1649 nextToken: 1,1650 present: false,1651 rowStale: false,1652 rowToken: 0,1653 touched: false,1654 ws:1655 Map(1656 "w1" ->1657 {1658 conn: false,1659 outputs: false,1660 phase: Idle,1661 res: RNone,1662 slot: false,1663 srv: SNone,1664 token: 01665 },1666 "w2" ->1667 {1668 conn: true,1669 outputs: false,1670 phase: Pending,1671 res: RNone,1672 slot: true,1673 srv: SNeed,1674 token: 01675 },1676 "w3" ->1677 {1678 conn: false,1679 outputs: false,1680 phase: Idle,1681 res: RNone,1682 slot: false,1683 srv: SNone,1684 token: 01685 }1686 )1687}16881689[State 2]1690{1691 nextToken: 1,1692 present: false,1693 rowStale: false,1694 rowToken: 0,1695 touched: false,1696 ws:1697 Map(1698 "w1" ->1699 {1700 conn: false,1701 outputs: false,1702 phase: Idle,1703 res: RNone,1704 slot: false,1705 srv: SNone,1706 token: 01707 },1708 "w2" ->1709 {1710 conn: false,1711 outputs: false,1712 phase: Pending,1713 res: RNone,1714 slot: true,1715 srv: SNone,1716 token: 01717 },1718 "w3" ->1719 {1720 conn: false,1721 outputs: false,1722 phase: Idle,1723 res: RNone,1724 slot: false,1725 srv: SNone,1726 token: 01727 }1728 )1729}17301731[State 3]1732{1733 nextToken: 1,1734 present: false,1735 rowStale: false,1736 rowToken: 0,1737 touched: false,1738 ws:1739 Map(1740 "w1" ->1741 {1742 conn: false,1743 outputs: false,1744 phase: Idle,1745 res: RNone,1746 slot: false,1747 srv: SNone,1748 token: 01749 },1750 "w2" ->1751 {1752 conn: true,1753 outputs: false,1754 phase: Pending,1755 res: RNone,1756 slot: true,1757 srv: SNeed,1758 token: 01759 },1760 "w3" ->1761 {1762 conn: false,1763 outputs: false,1764 phase: Idle,1765 res: RNone,1766 slot: false,1767 srv: SNone,1768 token: 01769 }1770 )1771}17721773[State 4]1774{1775 nextToken: 2,1776 present: false,1777 rowStale: false,1778 rowToken: 1,1779 touched: false,1780 ws:1781 Map(1782 "w1" ->1783 {1784 conn: false,1785 outputs: false,1786 phase: Idle,1787 res: RNone,1788 slot: false,1789 srv: SNone,1790 token: 01791 },1792 "w2" ->1793 {1794 conn: true,1795 outputs: false,1796 phase: Building,1797 res: RNone,1798 slot: true,1799 srv: SHolder(1),1800 token: 11801 },1802 "w3" ->1803 {1804 conn: false,1805 outputs: false,1806 phase: Idle,1807 res: RNone,1808 slot: false,1809 srv: SNone,1810 token: 01811 }1812 )1813}18141815[State 5]1816{1817 nextToken: 2,1818 present: false,1819 rowStale: false,1820 rowToken: 1,1821 touched: false,1822 ws:1823 Map(1824 "w1" ->1825 {1826 conn: false,1827 outputs: false,1828 phase: Idle,1829 res: RNone,1830 slot: false,1831 srv: SNone,1832 token: 01833 },1834 "w2" ->1835 {1836 conn: false,1837 outputs: false,1838 phase: Building,1839 res: RNone,1840 slot: true,1841 srv: SNone,1842 token: 11843 },1844 "w3" ->1845 {1846 conn: false,1847 outputs: false,1848 phase: Idle,1849 res: RNone,1850 slot: false,1851 srv: SNone,1852 token: 01853 }1854 )1855}18561857[State 6]1858{1859 nextToken: 2,1860 present: false,1861 rowStale: false,1862 rowToken: 1,1863 touched: false,1864 ws:1865 Map(1866 "w1" ->1867 {1868 conn: false,1869 outputs: false,1870 phase: Idle,1871 res: RNone,1872 slot: false,1873 srv: SNone,1874 token: 01875 },1876 "w2" ->1877 {1878 conn: true,1879 outputs: false,1880 phase: Building,1881 res: RNone,1882 slot: true,1883 srv: SNeed,1884 token: 11885 },1886 "w3" ->1887 {1888 conn: false,1889 outputs: false,1890 phase: Idle,1891 res: RNone,1892 slot: false,1893 srv: SNone,1894 token: 01895 }1896 )1897}18981899[State 7]1900{1901 nextToken: 2,1902 present: false,1903 rowStale: false,1904 rowToken: 1,1905 touched: false,1906 ws:1907 Map(1908 "w1" ->1909 {1910 conn: false,1911 outputs: false,1912 phase: Idle,1913 res: RNone,1914 slot: false,1915 srv: SNone,1916 token: 01917 },1918 "w2" ->1919 {1920 conn: false,1921 outputs: false,1922 phase: Building,1923 res: RNone,1924 slot: true,1925 srv: SNone,1926 token: 11927 },1928 "w3" ->1929 {1930 conn: false,1931 outputs: false,1932 phase: Idle,1933 res: RNone,1934 slot: false,1935 srv: SNone,1936 token: 01937 }1938 )1939}19401941[State 8]1942{1943 nextToken: 2,1944 present: false,1945 rowStale: false,1946 rowToken: 1,1947 touched: false,1948 ws:1949 Map(1950 "w1" ->1951 {1952 conn: false,1953 outputs: false,1954 phase: Idle,1955 res: RNone,1956 slot: false,1957 srv: SNone,1958 token: 01959 },1960 "w2" ->1961 {1962 conn: true,1963 outputs: false,1964 phase: Building,1965 res: RNone,1966 slot: true,1967 srv: SNeed,1968 token: 11969 },1970 "w3" ->1971 {1972 conn: false,1973 outputs: false,1974 phase: Idle,1975 res: RNone,1976 slot: false,1977 srv: SNone,1978 token: 01979 }1980 )1981}19821983[State 9]1984{1985 nextToken: 2,1986 present: false,1987 rowStale: false,1988 rowToken: 0,1989 touched: false,1990 ws:1991 Map(1992 "w1" ->1993 {1994 conn: false,1995 outputs: false,1996 phase: Idle,1997 res: RNone,1998 slot: false,1999 srv: SNone,2000 token: 02001 },2002 "w2" ->2003 {2004 conn: false,2005 outputs: false,2006 phase: Done,2007 res: RUnavailable,2008 slot: false,2009 srv: SNone,2010 token: 12011 },2012 "w3" ->2013 {2014 conn: false,2015 outputs: false,2016 phase: Idle,2017 res: RNone,2018 slot: false,2019 srv: SNone,2020 token: 02021 }2022 )2023}20242025[State 10]2026{2027 nextToken: 2,2028 present: false,2029 rowStale: false,2030 rowToken: 0,2031 touched: false,2032 ws:2033 Map(2034 "w1" ->2035 {2036 conn: false,2037 outputs: false,2038 phase: Idle,2039 res: RNone,2040 slot: false,2041 srv: SNone,2042 token: 02043 },2044 "w2" ->2045 {2046 conn: false,2047 outputs: false,2048 phase: Done,2049 res: RUnavailable,2050 slot: false,2051 srv: SNone,2052 token: 12053 },2054 "w3" ->2055 {2056 conn: true,2057 outputs: false,2058 phase: Pending,2059 res: RNone,2060 slot: true,2061 srv: SNeed,2062 token: 02063 }2064 )2065}20662067[State 11]2068{2069 nextToken: 2,2070 present: false,2071 rowStale: false,2072 rowToken: 0,2073 touched: false,2074 ws:2075 Map(2076 "w1" ->2077 {2078 conn: false,2079 outputs: false,2080 phase: Idle,2081 res: RNone,2082 slot: false,2083 srv: SNone,2084 token: 02085 },2086 "w2" ->2087 {2088 conn: false,2089 outputs: false,2090 phase: Done,2091 res: RUnavailable,2092 slot: false,2093 srv: SNone,2094 token: 12095 },2096 "w3" ->2097 {2098 conn: false,2099 outputs: false,2100 phase: Pending,2101 res: RNone,2102 slot: true,2103 srv: SNone,2104 token: 02105 }2106 )2107}21082109[State 12]2110{2111 nextToken: 2,2112 present: false,2113 rowStale: false,2114 rowToken: 0,2115 touched: false,2116 ws:2117 Map(2118 "w1" ->2119 {2120 conn: false,2121 outputs: false,2122 phase: Idle,2123 res: RNone,2124 slot: false,2125 srv: SNone,2126 token: 02127 },2128 "w2" ->2129 {2130 conn: false,2131 outputs: false,2132 phase: Done,2133 res: RUnavailable,2134 slot: false,2135 srv: SNone,2136 token: 12137 },2138 "w3" ->2139 {2140 conn: true,2141 outputs: false,2142 phase: Pending,2143 res: RNone,2144 slot: true,2145 srv: SNeed,2146 token: 02147 }2148 )2149}21502151[State 13]2152{2153 nextToken: 2,2154 present: false,2155 rowStale: false,2156 rowToken: 0,2157 touched: false,2158 ws:2159 Map(2160 "w1" ->2161 {2162 conn: false,2163 outputs: false,2164 phase: Idle,2165 res: RNone,2166 slot: false,2167 srv: SNone,2168 token: 02169 },2170 "w2" ->2171 {2172 conn: false,2173 outputs: false,2174 phase: Done,2175 res: RUnavailable,2176 slot: false,2177 srv: SNone,2178 token: 12179 },2180 "w3" ->2181 {2182 conn: false,2183 outputs: false,2184 phase: Pending,2185 res: RNone,2186 slot: true,2187 srv: SNone,2188 token: 02189 }2190 )2191}21922193[State 14]2194{2195 nextToken: 2,2196 present: false,2197 rowStale: false,2198 rowToken: 0,2199 touched: false,2200 ws:2201 Map(2202 "w1" ->2203 {2204 conn: false,2205 outputs: false,2206 phase: Idle,2207 res: RNone,2208 slot: false,2209 srv: SNone,2210 token: 02211 },2212 "w2" ->2213 {2214 conn: false,2215 outputs: false,2216 phase: Done,2217 res: RUnavailable,2218 slot: false,2219 srv: SNone,2220 token: 12221 },2222 "w3" ->2223 {2224 conn: true,2225 outputs: false,2226 phase: Pending,2227 res: RNone,2228 slot: true,2229 srv: SNeed,2230 token: 02231 }2232 )2233}22342235[State 15]2236{2237 nextToken: 2,2238 present: false,2239 rowStale: false,2240 rowToken: 0,2241 touched: false,2242 ws:2243 Map(2244 "w1" ->2245 {2246 conn: false,2247 outputs: false,2248 phase: Idle,2249 res: RNone,2250 slot: false,2251 srv: SNone,2252 token: 02253 },2254 "w2" ->2255 {2256 conn: false,2257 outputs: false,2258 phase: Done,2259 res: RUnavailable,2260 slot: false,2261 srv: SNone,2262 token: 12263 },2264 "w3" ->2265 {2266 conn: false,2267 outputs: false,2268 phase: Pending,2269 res: RNone,2270 slot: true,2271 srv: SNone,2272 token: 02273 }2274 )2275}22762277[State 16]2278{2279 nextToken: 2,2280 present: false,2281 rowStale: false,2282 rowToken: 0,2283 touched: false,2284 ws:2285 Map(2286 "w1" ->2287 {2288 conn: false,2289 outputs: false,2290 phase: Idle,2291 res: RNone,2292 slot: false,2293 srv: SNone,2294 token: 02295 },2296 "w2" ->2297 {2298 conn: false,2299 outputs: false,2300 phase: Done,2301 res: RUnavailable,2302 slot: false,2303 srv: SNone,2304 token: 12305 },2306 "w3" ->2307 {2308 conn: true,2309 outputs: false,2310 phase: Pending,2311 res: RNone,2312 slot: true,2313 srv: SNeed,2314 token: 02315 }2316 )2317}23182319[State 17]2320{2321 nextToken: 2,2322 present: false,2323 rowStale: false,2324 rowToken: 0,2325 touched: false,2326 ws:2327 Map(2328 "w1" ->2329 {2330 conn: false,2331 outputs: false,2332 phase: Idle,2333 res: RNone,2334 slot: false,2335 srv: SNone,2336 token: 02337 },2338 "w2" ->2339 {2340 conn: false,2341 outputs: false,2342 phase: Done,2343 res: RUnavailable,2344 slot: false,2345 srv: SNone,2346 token: 12347 },2348 "w3" ->2349 {2350 conn: false,2351 outputs: false,2352 phase: Pending,2353 res: RNone,2354 slot: true,2355 srv: SNone,2356 token: 02357 }2358 )2359}23602361[State 18]2362{2363 nextToken: 2,2364 present: false,2365 rowStale: false,2366 rowToken: 0,2367 touched: false,2368 ws:2369 Map(2370 "w1" ->2371 {2372 conn: false,2373 outputs: false,2374 phase: Idle,2375 res: RNone,2376 slot: false,2377 srv: SNone,2378 token: 02379 },2380 "w2" ->2381 {2382 conn: false,2383 outputs: false,2384 phase: Done,2385 res: RUnavailable,2386 slot: false,2387 srv: SNone,2388 token: 12389 },2390 "w3" ->2391 {2392 conn: true,2393 outputs: false,2394 phase: Pending,2395 res: RNone,2396 slot: true,2397 srv: SNeed,2398 token: 02399 }2400 )2401}24022403[State 19]2404{2405 nextToken: 2,2406 present: false,2407 rowStale: false,2408 rowToken: 0,2409 touched: false,2410 ws:2411 Map(2412 "w1" ->2413 {2414 conn: false,2415 outputs: false,2416 phase: Idle,2417 res: RNone,2418 slot: false,2419 srv: SNone,2420 token: 02421 },2422 "w2" ->2423 {2424 conn: false,2425 outputs: false,2426 phase: Done,2427 res: RUnavailable,2428 slot: false,2429 srv: SNone,2430 token: 12431 },2432 "w3" ->2433 {2434 conn: false,2435 outputs: false,2436 phase: Pending,2437 res: RNone,2438 slot: true,2439 srv: SNone,2440 token: 02441 }2442 )2443}24442445[State 20]2446{2447 nextToken: 2,2448 present: false,2449 rowStale: false,2450 rowToken: 0,2451 touched: false,2452 ws:2453 Map(2454 "w1" ->2455 {2456 conn: false,2457 outputs: false,2458 phase: Idle,2459 res: RNone,2460 slot: false,2461 srv: SNone,2462 token: 02463 },2464 "w2" ->2465 {2466 conn: false,2467 outputs: false,2468 phase: Done,2469 res: RUnavailable,2470 slot: false,2471 srv: SNone,2472 token: 12473 },2474 "w3" ->2475 {2476 conn: true,2477 outputs: false,2478 phase: Pending,2479 res: RNone,2480 slot: true,2481 srv: SNeed,2482 token: 02483 }2484 )2485}24862487[State 21]2488{2489 nextToken: 2,2490 present: false,2491 rowStale: false,2492 rowToken: 0,2493 touched: false,2494 ws:2495 Map(2496 "w1" ->2497 {2498 conn: false,2499 outputs: false,2500 phase: Idle,2501 res: RNone,2502 slot: false,2503 srv: SNone,2504 token: 02505 },2506 "w2" ->2507 {2508 conn: false,2509 outputs: false,2510 phase: Done,2511 res: RUnavailable,2512 slot: false,2513 srv: SNone,2514 token: 12515 },2516 "w3" ->2517 {2518 conn: false,2519 outputs: false,2520 phase: Pending,2521 res: RNone,2522 slot: true,2523 srv: SNone,2524 token: 02525 }2526 )2527}25282529[State 22]2530{2531 nextToken: 2,2532 present: false,2533 rowStale: false,2534 rowToken: 0,2535 touched: false,2536 ws:2537 Map(2538 "w1" ->2539 {2540 conn: false,2541 outputs: false,2542 phase: Idle,2543 res: RNone,2544 slot: false,2545 srv: SNone,2546 token: 02547 },2548 "w2" ->2549 {2550 conn: false,2551 outputs: false,2552 phase: Done,2553 res: RUnavailable,2554 slot: false,2555 srv: SNone,2556 token: 12557 },2558 "w3" ->2559 {2560 conn: true,2561 outputs: false,2562 phase: Pending,2563 res: RNone,2564 slot: true,2565 srv: SNeed,2566 token: 02567 }2568 )2569}25702571[State 23]2572{2573 nextToken: 2,2574 present: false,2575 rowStale: false,2576 rowToken: 0,2577 touched: false,2578 ws:2579 Map(2580 "w1" ->2581 {2582 conn: false,2583 outputs: false,2584 phase: Idle,2585 res: RNone,2586 slot: false,2587 srv: SNone,2588 token: 02589 },2590 "w2" ->2591 {2592 conn: false,2593 outputs: false,2594 phase: Done,2595 res: RUnavailable,2596 slot: false,2597 srv: SNone,2598 token: 12599 },2600 "w3" ->2601 {2602 conn: false,2603 outputs: false,2604 phase: Pending,2605 res: RNone,2606 slot: true,2607 srv: SNone,2608 token: 02609 }2610 )2611}26122613[State 24]2614{2615 nextToken: 2,2616 present: false,2617 rowStale: false,2618 rowToken: 0,2619 touched: false,2620 ws:2621 Map(2622 "w1" ->2623 {2624 conn: false,2625 outputs: false,2626 phase: Idle,2627 res: RNone,2628 slot: false,2629 srv: SNone,2630 token: 02631 },2632 "w2" ->2633 {2634 conn: false,2635 outputs: false,2636 phase: Done,2637 res: RUnavailable,2638 slot: false,2639 srv: SNone,2640 token: 12641 },2642 "w3" ->2643 {2644 conn: true,2645 outputs: false,2646 phase: Pending,2647 res: RNone,2648 slot: true,2649 srv: SNeed,2650 token: 02651 }2652 )2653}26542655[State 25]2656{2657 nextToken: 2,2658 present: false,2659 rowStale: false,2660 rowToken: 0,2661 touched: false,2662 ws:2663 Map(2664 "w1" ->2665 {2666 conn: false,2667 outputs: false,2668 phase: Idle,2669 res: RNone,2670 slot: false,2671 srv: SNone,2672 token: 02673 },2674 "w2" ->2675 {2676 conn: false,2677 outputs: false,2678 phase: Done,2679 res: RUnavailable,2680 slot: false,2681 srv: SNone,2682 token: 12683 },2684 "w3" ->2685 {2686 conn: false,2687 outputs: false,2688 phase: Pending,2689 res: RNone,2690 slot: true,2691 srv: SNone,2692 token: 02693 }2694 )2695}26962697[State 26]2698{2699 nextToken: 2,2700 present: false,2701 rowStale: false,2702 rowToken: 0,2703 touched: false,2704 ws:2705 Map(2706 "w1" ->2707 {2708 conn: false,2709 outputs: false,2710 phase: Idle,2711 res: RNone,2712 slot: false,2713 srv: SNone,2714 token: 02715 },2716 "w2" ->2717 {2718 conn: false,2719 outputs: false,2720 phase: Done,2721 res: RUnavailable,2722 slot: false,2723 srv: SNone,2724 token: 12725 },2726 "w3" ->2727 {2728 conn: true,2729 outputs: false,2730 phase: Pending,2731 res: RNone,2732 slot: true,2733 srv: SNeed,2734 token: 02735 }2736 )2737}27382739[State 27]2740{2741 nextToken: 2,2742 present: false,2743 rowStale: false,2744 rowToken: 0,2745 touched: false,2746 ws:2747 Map(2748 "w1" ->2749 {2750 conn: false,2751 outputs: false,2752 phase: Idle,2753 res: RNone,2754 slot: false,2755 srv: SNone,2756 token: 02757 },2758 "w2" ->2759 {2760 conn: false,2761 outputs: false,2762 phase: Done,2763 res: RUnavailable,2764 slot: false,2765 srv: SNone,2766 token: 12767 },2768 "w3" ->2769 {2770 conn: false,2771 outputs: false,2772 phase: Pending,2773 res: RNone,2774 slot: true,2775 srv: SNone,2776 token: 02777 }2778 )2779}27802781[State 28]2782{2783 nextToken: 2,2784 present: false,2785 rowStale: false,2786 rowToken: 0,2787 touched: false,2788 ws:2789 Map(2790 "w1" ->2791 {2792 conn: false,2793 outputs: false,2794 phase: Idle,2795 res: RNone,2796 slot: false,2797 srv: SNone,2798 token: 02799 },2800 "w2" ->2801 {2802 conn: false,2803 outputs: false,2804 phase: Done,2805 res: RUnavailable,2806 slot: false,2807 srv: SNone,2808 token: 12809 },2810 "w3" ->2811 {2812 conn: true,2813 outputs: false,2814 phase: Pending,2815 res: RNone,2816 slot: true,2817 srv: SNeed,2818 token: 02819 }2820 )2821}28222823[State 29]2824{2825 nextToken: 2,2826 present: false,2827 rowStale: false,2828 rowToken: 0,2829 touched: false,2830 ws:2831 Map(2832 "w1" ->2833 {2834 conn: false,2835 outputs: false,2836 phase: Idle,2837 res: RNone,2838 slot: false,2839 srv: SNone,2840 token: 02841 },2842 "w2" ->2843 {2844 conn: false,2845 outputs: false,2846 phase: Done,2847 res: RUnavailable,2848 slot: false,2849 srv: SNone,2850 token: 12851 },2852 "w3" ->2853 {2854 conn: false,2855 outputs: false,2856 phase: Pending,2857 res: RNone,2858 slot: true,2859 srv: SNone,2860 token: 02861 }2862 )2863}28642865[State 30]2866{2867 nextToken: 2,2868 present: false,2869 rowStale: false,2870 rowToken: 0,2871 touched: false,2872 ws:2873 Map(2874 "w1" ->2875 {2876 conn: false,2877 outputs: false,2878 phase: Idle,2879 res: RNone,2880 slot: false,2881 srv: SNone,2882 token: 02883 },2884 "w2" ->2885 {2886 conn: false,2887 outputs: false,2888 phase: Done,2889 res: RUnavailable,2890 slot: false,2891 srv: SNone,2892 token: 12893 },2894 "w3" ->2895 {2896 conn: true,2897 outputs: false,2898 phase: Pending,2899 res: RNone,2900 slot: true,2901 srv: SNeed,2902 token: 02903 }2904 )2905}29062907[ok] No violation found (362ms at 55249 traces/second).2908Trace length statistics: max=31, min=10, average=18.262909You may increase --max-samples and --max-steps.2910Use --verbosity to produce more (or less) output.2911Use --seed=0xfd36ccc650258871 --backend=rust to reproduce.