nix-grpc-store-claims-spec
checks.aarch64-linux.claims-spec
· build #94
· 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: true,68 outputs: false,69 phase: Pending,70 res: RNone,71 slot: true,72 srv: SNeed,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: Idle,102 res: RNone,103 slot: false,104 srv: SNone,105 token: 0106 },107 "w2" ->108 {109 conn: false,110 outputs: false,111 phase: Pending,112 res: RNone,113 slot: true,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: false,142 outputs: false,143 phase: Idle,144 res: RNone,145 slot: false,146 srv: SNone,147 token: 0148 },149 "w2" ->150 {151 conn: true,152 outputs: false,153 phase: Pending,154 res: RNone,155 slot: true,156 srv: SNeed,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: Idle,186 res: RNone,187 slot: false,188 srv: SNone,189 token: 0190 },191 "w2" ->192 {193 conn: false,194 outputs: false,195 phase: Pending,196 res: RNone,197 slot: true,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: false,226 outputs: false,227 phase: Idle,228 res: RNone,229 slot: false,230 srv: SNone,231 token: 0232 },233 "w2" ->234 {235 conn: true,236 outputs: false,237 phase: Pending,238 res: RNone,239 slot: true,240 srv: SNeed,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: Idle,270 res: RNone,271 slot: false,272 srv: SNone,273 token: 0274 },275 "w2" ->276 {277 conn: false,278 outputs: false,279 phase: Pending,280 res: RNone,281 slot: true,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: 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: 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: Done,364 res: RUnavailable,365 slot: false,366 srv: SNone,367 token: 0368 },369 "w3" ->370 {371 conn: true,372 outputs: false,373 phase: Pending,374 res: RNone,375 slot: true,376 srv: SNeed,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: true,498 outputs: false,499 phase: Pending,500 res: RNone,501 slot: true,502 srv: SNeed,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: 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: Pending,542 res: RNone,543 slot: true,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: Idle,564 res: RNone,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: true,582 outputs: false,583 phase: Pending,584 res: RNone,585 slot: true,586 srv: SNeed,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: Idle,606 res: RNone,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: false,624 outputs: false,625 phase: Pending,626 res: RNone,627 slot: true,628 srv: SNone,629 token: 0630 }631 )632}633634[State 15]635{636 nextToken: 1,637 present: false,638 rowStale: false,639 rowToken: 0,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: Idle,658 res: RNone,659 slot: false,660 srv: SNone,661 token: 0662 },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: 1,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: Idle,690 res: RNone,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: Idle,710 res: RNone,711 slot: false,712 srv: SNone,713 token: 0714 }715 )716}717718[State 17]719{720 nextToken: 1,721 present: false,722 rowStale: false,723 rowToken: 0,724 touched: false,725 ws:726 Map(727 "w1" ->728 {729 conn: true,730 outputs: false,731 phase: Pending,732 res: RNone,733 slot: true,734 srv: SNeed,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: Idle,752 res: RNone,753 slot: false,754 srv: SNone,755 token: 0756 }757 )758}759760[State 18]761{762 nextToken: 1,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: 1,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: 1,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: 1,889 present: false,890 rowStale: false,891 rowToken: 0,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: 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: 1,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: Done,942 res: RUnavailable,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: Pending,962 res: RNone,963 slot: true,964 srv: SNeed,965 token: 0966 }967 )968}969970[State 23]971{972 nextToken: 1,973 present: false,974 rowStale: false,975 rowToken: 0,976 touched: false,977 ws:978 Map(979 "w1" ->980 {981 conn: false,982 outputs: false,983 phase: Done,984 res: RUnavailable,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: Pending,1004 res: RNone,1005 slot: true,1006 srv: SNone,1007 token: 01008 }1009 )1010}10111012[State 24]1013{1014 nextToken: 1,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: Done,1026 res: RUnavailable,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: true,1044 outputs: false,1045 phase: Pending,1046 res: RNone,1047 slot: true,1048 srv: SNeed,1049 token: 01050 }1051 )1052}10531054[State 25]1055{1056 nextToken: 1,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: Idle,1068 res: RNone,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: true,1086 outputs: false,1087 phase: Pending,1088 res: RNone,1089 slot: true,1090 srv: SNeed,1091 token: 01092 }1093 )1094}10951096[State 26]1097{1098 nextToken: 1,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: Idle,1110 res: RNone,1111 slot: false,1112 srv: SNone,1113 token: 01114 },1115 "w2" ->1116 {1117 conn: false,1118 outputs: false,1119 phase: Idle,1120 res: RNone,1121 slot: false,1122 srv: SNone,1123 token: 01124 },1125 "w3" ->1126 {1127 conn: false,1128 outputs: false,1129 phase: Pending,1130 res: RNone,1131 slot: true,1132 srv: SNone,1133 token: 01134 }1135 )1136}11371138[State 27]1139{1140 nextToken: 1,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: Idle,1162 res: RNone,1163 slot: false,1164 srv: SNone,1165 token: 01166 },1167 "w3" ->1168 {1169 conn: true,1170 outputs: false,1171 phase: Pending,1172 res: RNone,1173 slot: true,1174 srv: SNeed,1175 token: 01176 }1177 )1178}11791180[State 28]1181{1182 nextToken: 1,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: Idle,1204 res: RNone,1205 slot: false,1206 srv: SNone,1207 token: 01208 },1209 "w3" ->1210 {1211 conn: false,1212 outputs: false,1213 phase: Pending,1214 res: RNone,1215 slot: true,1216 srv: SNone,1217 token: 01218 }1219 )1220}12211222[State 29]1223{1224 nextToken: 1,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: Idle,1246 res: RNone,1247 slot: false,1248 srv: SNone,1249 token: 01250 },1251 "w3" ->1252 {1253 conn: false,1254 outputs: false,1255 phase: Done,1256 res: RUnavailable,1257 slot: false,1258 srv: SNone,1259 token: 01260 }1261 )1262}12631264[State 30]1265{1266 nextToken: 1,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: 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: Done,1298 res: RUnavailable,1299 slot: false,1300 srv: SNone,1301 token: 01302 }1303 )1304}13051306[ok] No violation found (463ms at 43197 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=0x41c813bfd8c7477d --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: false,1367 outputs: false,1368 phase: Idle,1369 res: RNone,1370 slot: false,1371 srv: SNone,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: true,1387 outputs: false,1388 phase: Pending,1389 res: RNone,1390 slot: true,1391 srv: SNeed,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: Idle,1411 res: RNone,1412 slot: false,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: Pending,1431 res: RNone,1432 slot: true,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: false,1451 outputs: false,1452 phase: Idle,1453 res: RNone,1454 slot: false,1455 srv: SNone,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: true,1471 outputs: false,1472 phase: Pending,1473 res: RNone,1474 slot: true,1475 srv: SNeed,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: Idle,1495 res: RNone,1496 slot: false,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: Pending,1515 res: RNone,1516 slot: true,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: false,1535 outputs: false,1536 phase: Idle,1537 res: RNone,1538 slot: false,1539 srv: SNone,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: true,1555 outputs: false,1556 phase: Pending,1557 res: RNone,1558 slot: true,1559 srv: SNeed,1560 token: 01561 }1562 )1563}15641565[State 6]1566{1567 nextToken: 1,1568 present: false,1569 rowStale: false,1570 rowToken: 0,1571 touched: false,1572 ws:1573 Map(1574 "w1" ->1575 {1576 conn: false,1577 outputs: false,1578 phase: Idle,1579 res: RNone,1580 slot: false,1581 srv: SNone,1582 token: 01583 },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: Pending,1599 res: RNone,1600 slot: true,1601 srv: SNone,1602 token: 01603 }1604 )1605}16061607[State 7]1608{1609 nextToken: 1,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: Idle,1621 res: RNone,1622 slot: false,1623 srv: SNone,1624 token: 01625 },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: true,1639 outputs: false,1640 phase: Pending,1641 res: RNone,1642 slot: true,1643 srv: SNeed,1644 token: 01645 }1646 )1647}16481649[State 8]1650{1651 nextToken: 1,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: Idle,1663 res: RNone,1664 slot: false,1665 srv: SNone,1666 token: 01667 },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: false,1681 outputs: false,1682 phase: Pending,1683 res: RNone,1684 slot: true,1685 srv: SNone,1686 token: 01687 }1688 )1689}16901691[State 9]1692{1693 nextToken: 1,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: Idle,1705 res: RNone,1706 slot: false,1707 srv: SNone,1708 token: 01709 },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: true,1723 outputs: false,1724 phase: Pending,1725 res: RNone,1726 slot: true,1727 srv: SNeed,1728 token: 01729 }1730 )1731}17321733[State 10]1734{1735 nextToken: 1,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: Idle,1747 res: RNone,1748 slot: false,1749 srv: SNone,1750 token: 01751 },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: false,1765 outputs: false,1766 phase: Pending,1767 res: RNone,1768 slot: true,1769 srv: SNone,1770 token: 01771 }1772 )1773}17741775[State 11]1776{1777 nextToken: 1,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: Idle,1789 res: RNone,1790 slot: false,1791 srv: SNone,1792 token: 01793 },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: true,1807 outputs: false,1808 phase: Pending,1809 res: RNone,1810 slot: true,1811 srv: SNeed,1812 token: 01813 }1814 )1815}18161817[State 12]1818{1819 nextToken: 2,1820 present: false,1821 rowStale: false,1822 rowToken: 1,1823 touched: false,1824 ws:1825 Map(1826 "w1" ->1827 {1828 conn: false,1829 outputs: false,1830 phase: Idle,1831 res: RNone,1832 slot: false,1833 srv: SNone,1834 token: 01835 },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: Building,1851 res: RNone,1852 slot: true,1853 srv: SHolder(1),1854 token: 11855 }1856 )1857}18581859[State 13]1860{1861 nextToken: 2,1862 present: false,1863 rowStale: false,1864 rowToken: 0,1865 touched: false,1866 ws:1867 Map(1868 "w1" ->1869 {1870 conn: false,1871 outputs: false,1872 phase: Idle,1873 res: RNone,1874 slot: false,1875 srv: SNone,1876 token: 01877 },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: false,1891 outputs: false,1892 phase: Done,1893 res: RUnavailable,1894 slot: false,1895 srv: SNone,1896 token: 11897 }1898 )1899}19001901[State 14]1902{1903 nextToken: 2,1904 present: false,1905 rowStale: false,1906 rowToken: 0,1907 touched: false,1908 ws:1909 Map(1910 "w1" ->1911 {1912 conn: false,1913 outputs: false,1914 phase: Idle,1915 res: RNone,1916 slot: false,1917 srv: SNone,1918 token: 01919 },1920 "w2" ->1921 {1922 conn: true,1923 outputs: false,1924 phase: Pending,1925 res: RNone,1926 slot: true,1927 srv: SNeed,1928 token: 01929 },1930 "w3" ->1931 {1932 conn: false,1933 outputs: false,1934 phase: Done,1935 res: RUnavailable,1936 slot: false,1937 srv: SNone,1938 token: 11939 }1940 )1941}19421943[State 15]1944{1945 nextToken: 2,1946 present: false,1947 rowStale: false,1948 rowToken: 0,1949 touched: false,1950 ws:1951 Map(1952 "w1" ->1953 {1954 conn: false,1955 outputs: false,1956 phase: Idle,1957 res: RNone,1958 slot: false,1959 srv: SNone,1960 token: 01961 },1962 "w2" ->1963 {1964 conn: false,1965 outputs: false,1966 phase: Pending,1967 res: RNone,1968 slot: true,1969 srv: SNone,1970 token: 01971 },1972 "w3" ->1973 {1974 conn: false,1975 outputs: false,1976 phase: Done,1977 res: RUnavailable,1978 slot: false,1979 srv: SNone,1980 token: 11981 }1982 )1983}19841985[State 16]1986{1987 nextToken: 2,1988 present: false,1989 rowStale: false,1990 rowToken: 0,1991 touched: false,1992 ws:1993 Map(1994 "w1" ->1995 {1996 conn: false,1997 outputs: false,1998 phase: Idle,1999 res: RNone,2000 slot: false,2001 srv: SNone,2002 token: 02003 },2004 "w2" ->2005 {2006 conn: true,2007 outputs: false,2008 phase: Pending,2009 res: RNone,2010 slot: true,2011 srv: SNeed,2012 token: 02013 },2014 "w3" ->2015 {2016 conn: false,2017 outputs: false,2018 phase: Done,2019 res: RUnavailable,2020 slot: false,2021 srv: SNone,2022 token: 12023 }2024 )2025}20262027[State 17]2028{2029 nextToken: 2,2030 present: false,2031 rowStale: false,2032 rowToken: 0,2033 touched: false,2034 ws:2035 Map(2036 "w1" ->2037 {2038 conn: false,2039 outputs: false,2040 phase: Idle,2041 res: RNone,2042 slot: false,2043 srv: SNone,2044 token: 02045 },2046 "w2" ->2047 {2048 conn: false,2049 outputs: false,2050 phase: Pending,2051 res: RNone,2052 slot: true,2053 srv: SNone,2054 token: 02055 },2056 "w3" ->2057 {2058 conn: false,2059 outputs: false,2060 phase: Done,2061 res: RUnavailable,2062 slot: false,2063 srv: SNone,2064 token: 12065 }2066 )2067}20682069[State 18]2070{2071 nextToken: 2,2072 present: false,2073 rowStale: false,2074 rowToken: 0,2075 touched: false,2076 ws:2077 Map(2078 "w1" ->2079 {2080 conn: false,2081 outputs: false,2082 phase: Idle,2083 res: RNone,2084 slot: false,2085 srv: SNone,2086 token: 02087 },2088 "w2" ->2089 {2090 conn: true,2091 outputs: false,2092 phase: Pending,2093 res: RNone,2094 slot: true,2095 srv: SNeed,2096 token: 02097 },2098 "w3" ->2099 {2100 conn: false,2101 outputs: false,2102 phase: Done,2103 res: RUnavailable,2104 slot: false,2105 srv: SNone,2106 token: 12107 }2108 )2109}21102111[State 19]2112{2113 nextToken: 2,2114 present: false,2115 rowStale: false,2116 rowToken: 0,2117 touched: false,2118 ws:2119 Map(2120 "w1" ->2121 {2122 conn: false,2123 outputs: false,2124 phase: Idle,2125 res: RNone,2126 slot: false,2127 srv: SNone,2128 token: 02129 },2130 "w2" ->2131 {2132 conn: false,2133 outputs: false,2134 phase: Pending,2135 res: RNone,2136 slot: true,2137 srv: SNone,2138 token: 02139 },2140 "w3" ->2141 {2142 conn: false,2143 outputs: false,2144 phase: Done,2145 res: RUnavailable,2146 slot: false,2147 srv: SNone,2148 token: 12149 }2150 )2151}21522153[State 20]2154{2155 nextToken: 2,2156 present: false,2157 rowStale: false,2158 rowToken: 0,2159 touched: false,2160 ws:2161 Map(2162 "w1" ->2163 {2164 conn: false,2165 outputs: false,2166 phase: Idle,2167 res: RNone,2168 slot: false,2169 srv: SNone,2170 token: 02171 },2172 "w2" ->2173 {2174 conn: true,2175 outputs: false,2176 phase: Pending,2177 res: RNone,2178 slot: true,2179 srv: SNeed,2180 token: 02181 },2182 "w3" ->2183 {2184 conn: false,2185 outputs: false,2186 phase: Done,2187 res: RUnavailable,2188 slot: false,2189 srv: SNone,2190 token: 12191 }2192 )2193}21942195[State 21]2196{2197 nextToken: 2,2198 present: false,2199 rowStale: false,2200 rowToken: 0,2201 touched: false,2202 ws:2203 Map(2204 "w1" ->2205 {2206 conn: false,2207 outputs: false,2208 phase: Idle,2209 res: RNone,2210 slot: false,2211 srv: SNone,2212 token: 02213 },2214 "w2" ->2215 {2216 conn: false,2217 outputs: false,2218 phase: Pending,2219 res: RNone,2220 slot: true,2221 srv: SNone,2222 token: 02223 },2224 "w3" ->2225 {2226 conn: false,2227 outputs: false,2228 phase: Done,2229 res: RUnavailable,2230 slot: false,2231 srv: SNone,2232 token: 12233 }2234 )2235}22362237[State 22]2238{2239 nextToken: 2,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: Idle,2251 res: RNone,2252 slot: false,2253 srv: SNone,2254 token: 02255 },2256 "w2" ->2257 {2258 conn: true,2259 outputs: false,2260 phase: Pending,2261 res: RNone,2262 slot: true,2263 srv: SNeed,2264 token: 02265 },2266 "w3" ->2267 {2268 conn: false,2269 outputs: false,2270 phase: Done,2271 res: RUnavailable,2272 slot: false,2273 srv: SNone,2274 token: 12275 }2276 )2277}22782279[State 23]2280{2281 nextToken: 3,2282 present: false,2283 rowStale: false,2284 rowToken: 2,2285 touched: false,2286 ws:2287 Map(2288 "w1" ->2289 {2290 conn: false,2291 outputs: false,2292 phase: Idle,2293 res: RNone,2294 slot: false,2295 srv: SNone,2296 token: 02297 },2298 "w2" ->2299 {2300 conn: true,2301 outputs: false,2302 phase: Building,2303 res: RNone,2304 slot: true,2305 srv: SHolder(2),2306 token: 22307 },2308 "w3" ->2309 {2310 conn: false,2311 outputs: false,2312 phase: Done,2313 res: RUnavailable,2314 slot: false,2315 srv: SNone,2316 token: 12317 }2318 )2319}23202321[State 24]2322{2323 nextToken: 3,2324 present: false,2325 rowStale: false,2326 rowToken: 2,2327 touched: false,2328 ws:2329 Map(2330 "w1" ->2331 {2332 conn: false,2333 outputs: false,2334 phase: Idle,2335 res: RNone,2336 slot: false,2337 srv: SNone,2338 token: 02339 },2340 "w2" ->2341 {2342 conn: false,2343 outputs: false,2344 phase: Building,2345 res: RNone,2346 slot: true,2347 srv: SNone,2348 token: 22349 },2350 "w3" ->2351 {2352 conn: false,2353 outputs: false,2354 phase: Done,2355 res: RUnavailable,2356 slot: false,2357 srv: SNone,2358 token: 12359 }2360 )2361}23622363[State 25]2364{2365 nextToken: 3,2366 present: false,2367 rowStale: false,2368 rowToken: 2,2369 touched: false,2370 ws:2371 Map(2372 "w1" ->2373 {2374 conn: false,2375 outputs: false,2376 phase: Idle,2377 res: RNone,2378 slot: false,2379 srv: SNone,2380 token: 02381 },2382 "w2" ->2383 {2384 conn: true,2385 outputs: false,2386 phase: Building,2387 res: RNone,2388 slot: true,2389 srv: SNeed,2390 token: 22391 },2392 "w3" ->2393 {2394 conn: false,2395 outputs: false,2396 phase: Done,2397 res: RUnavailable,2398 slot: false,2399 srv: SNone,2400 token: 12401 }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: Idle,2419 res: RNone,2420 slot: false,2421 srv: SNone,2422 token: 02423 },2424 "w2" ->2425 {2426 conn: false,2427 outputs: false,2428 phase: Done,2429 res: RFailed,2430 slot: false,2431 srv: SNone,2432 token: 22433 },2434 "w3" ->2435 {2436 conn: false,2437 outputs: false,2438 phase: Done,2439 res: RUnavailable,2440 slot: false,2441 srv: SNone,2442 token: 12443 }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: true,2459 outputs: false,2460 phase: Pending,2461 res: RNone,2462 slot: true,2463 srv: SNeed,2464 token: 02465 },2466 "w2" ->2467 {2468 conn: false,2469 outputs: false,2470 phase: Done,2471 res: RFailed,2472 slot: false,2473 srv: SNone,2474 token: 22475 },2476 "w3" ->2477 {2478 conn: false,2479 outputs: false,2480 phase: Done,2481 res: RUnavailable,2482 slot: false,2483 srv: SNone,2484 token: 12485 }2486 )2487}24882489[State 28]2490{2491 nextToken: 4,2492 present: false,2493 rowStale: false,2494 rowToken: 3,2495 touched: false,2496 ws:2497 Map(2498 "w1" ->2499 {2500 conn: true,2501 outputs: false,2502 phase: Building,2503 res: RNone,2504 slot: true,2505 srv: SHolder(3),2506 token: 32507 },2508 "w2" ->2509 {2510 conn: false,2511 outputs: false,2512 phase: Done,2513 res: RFailed,2514 slot: false,2515 srv: SNone,2516 token: 22517 },2518 "w3" ->2519 {2520 conn: false,2521 outputs: false,2522 phase: Done,2523 res: RUnavailable,2524 slot: false,2525 srv: SNone,2526 token: 12527 }2528 )2529}25302531[State 29]2532{2533 nextToken: 4,2534 present: false,2535 rowStale: false,2536 rowToken: 3,2537 touched: false,2538 ws:2539 Map(2540 "w1" ->2541 {2542 conn: false,2543 outputs: false,2544 phase: Building,2545 res: RNone,2546 slot: true,2547 srv: SNone,2548 token: 32549 },2550 "w2" ->2551 {2552 conn: false,2553 outputs: false,2554 phase: Done,2555 res: RFailed,2556 slot: false,2557 srv: SNone,2558 token: 22559 },2560 "w3" ->2561 {2562 conn: false,2563 outputs: false,2564 phase: Done,2565 res: RUnavailable,2566 slot: false,2567 srv: SNone,2568 token: 12569 }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: true,2585 outputs: false,2586 phase: Building,2587 res: RNone,2588 slot: true,2589 srv: SNeed,2590 token: 32591 },2592 "w2" ->2593 {2594 conn: false,2595 outputs: false,2596 phase: Done,2597 res: RFailed,2598 slot: false,2599 srv: SNone,2600 token: 22601 },2602 "w3" ->2603 {2604 conn: false,2605 outputs: false,2606 phase: Done,2607 res: RUnavailable,2608 slot: false,2609 srv: SNone,2610 token: 12611 }2612 )2613}26142615[ok] No violation found (356ms at 56180 traces/second).2616Trace length statistics: max=31, min=9, average=18.422617You may increase --max-samples and --max-steps.2618Use --verbosity to produce more (or less) output.2619Use --seed=0xc4f3492c7b5ba278 --backend=rust to reproduce.