nix-grpc-store-claims-spec
checks.aarch64-darwin.claims-spec
· build #94
· raw
1Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [■■ ] 5% | ETA: 8s | 1084/20000 samples | 2569 samples/sRunning... [■■■ ] 7% | ETA: 7s | 1560/20000 samples | 2718 samples/sRunning... [■■■ ] 7% | ETA: 7s | 1560/20000 samples | 2718 samples/sRunning... [■■■■ ] 10% | ETA: 7s | 2062/20000 samples | 2805 samples/sRunning... [■■■■ ] 10% | ETA: 7s | 2062/20000 samples | 2805 samples/sRunning... [■■■■■■ ] 13% | ETA: 7s | 2764/20000 samples | 2806 samples/sRunning... [■■■■■■ ] 13% | ETA: 7s | 2764/20000 samples | 2806 samples/sRunning... [■■■■■■ ] 13% | ETA: 7s | 2764/20000 samples | 2806 samples/sRunning... [■■■■■■■ ] 17% | ETA: 7s | 3424/20000 samples | 2772 samples/sRunning... [■■■■■■■■ ] 19% | ETA: 6s | 3934/20000 samples | 2765 samples/sRunning... [■■■■■■■■ ] 19% | ETA: 6s | 3934/20000 samples | 2765 samples/sRunning... [■■■■■■■■■ ] 22% | ETA: 6s | 4444/20000 samples | 2813 samples/sRunning... [■■■■■■■■■■ ] 23% | ETA: 6s | 4763/20000 samples | 2833 samples/sRunning... [■■■■■■■■■■ ] 23% | ETA: 6s | 4763/20000 samples | 2833 samples/sRunning... [■■■■■■■■■■■ ] 26% | ETA: 6s | 5282/20000 samples | 2851 samples/sRunning... [■■■■■■■■■■■ ] 26% | ETA: 6s | 5282/20000 samples | 2851 samples/sRunning... [■■■■■■■■■■■■ ] 30% | ETA: 5s | 6088/20000 samples | 2896 samples/sRunning... [■■■■■■■■■■■■ ] 30% | ETA: 5s | 6088/20000 samples | 2896 samples/sRunning... [■■■■■■■■■■■■ ] 30% | ETA: 5s | 6088/20000 samples | 2896 samples/sRunning... [■■■■■■■■■■■■■■ ] 34% | ETA: 5s | 6900/20000 samples | 2934 samples/sRunning... [■■■■■■■■■■■■■■ ] 36% | ETA: 5s | 7209/20000 samples | 2939 samples/sRunning... [■■■■■■■■■■■■■■■■ ] 39% | ETA: 4s | 7839/20000 samples | 2956 samples/sRunning... [■■■■■■■■■■■■■■■■ ] 39% | ETA: 4s | 7839/20000 samples | 2956 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 41% | ETA: 4s | 8266/20000 samples | 2962 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 43% | ETA: 4s | 8724/20000 samples | 2982 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 43% | ETA: 4s | 8724/20000 samples | 2982 samples/sRunning... [■■■■■■■■■■■■■■■■■■■ ] 46% | ETA: 4s | 9275/20000 samples | 2990 samples/sRunning... [■■■■■■■■■■■■■■■■■■■ ] 48% | ETA: 4s | 9722/20000 samples | 2992 samples/sRunning... [■■■■■■■■■■■■■■■■■■■ ] 48% | ETA: 4s | 9722/20000 samples | 2992 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 50% | ETA: 4s | 10124/20000 samples | 3001 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 50% | ETA: 4s | 10124/20000 samples | 3001 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■ ] 54% | ETA: 3s | 10943/20000 samples | 3020 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■ ] 54% | ETA: 3s | 10943/20000 samples | 3020 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 58% | ETA: 3s | 11642/20000 samples | 3007 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 58% | ETA: 3s | 11642/20000 samples | 3007 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■ ] 61% | ETA: 3s | 12324/20000 samples | 3016 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■ ] 61% | ETA: 3s | 12324/20000 samples | 3016 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 64% | ETA: 3s | 12862/20000 samples | 3011 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 64% | ETA: 3s | 12862/20000 samples | 3011 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 67% | ETA: 3s | 13540/20000 samples | 3031 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 67% | ETA: 3s | 13540/20000 samples | 3031 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 69% | ETA: 2s | 13936/20000 samples | 3026 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 69% | ETA: 2s | 13936/20000 samples | 3026 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 73% | ETA: 2s | 14697/20000 samples | 3035 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 73% | ETA: 2s | 14697/20000 samples | 3035 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 76% | ETA: 2s | 15317/20000 samples | 3032 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 76% | ETA: 2s | 15317/20000 samples | 3032 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 79% | ETA: 2s | 15948/20000 samples | 3034 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 81% | ETA: 2s | 16359/20000 samples | 3040 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 81% | ETA: 2s | 16359/20000 samples | 3040 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 81% | ETA: 2s | 16359/20000 samples | 3040 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 85% | ETA: 1s | 17153/20000 samples | 3047 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 85% | ETA: 1s | 17153/20000 samples | 3047 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 89% | ETA: 1s | 17920/20000 samples | 3048 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 89% | ETA: 1s | 17920/20000 samples | 3048 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 89% | ETA: 1s | 17920/20000 samples | 3048 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 93% | ETA: 1s | 18647/20000 samples | 3042 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 95% | ETA: 1s | 19196/20000 samples | 3043 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 95% | ETA: 1s | 19196/20000 samples | 3043 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 98% | ETA: 1s | 19611/20000 samples | 3051 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 98% | ETA: 1s | 19611/20000 samples | 3051 samples/sAn example execution:23[State 0]4{5 nextToken: 1,6 present: false,7 rowStale: false,8 rowToken: 0,9 touched: false,10 ws:11 Map(12 "w1" ->13 {14 conn: false,15 outputs: false,16 phase: Idle,17 res: RNone,18 slot: false,19 srv: SNone,20 token: 021 },22 "w2" ->23 {24 conn: false,25 outputs: false,26 phase: Idle,27 res: RNone,28 slot: false,29 srv: SNone,30 token: 031 },32 "w3" ->33 {34 conn: false,35 outputs: false,36 phase: Idle,37 res: RNone,38 slot: false,39 srv: SNone,40 token: 041 }42 )43}4445[State 1]46{47 nextToken: 1,48 present: false,49 rowStale: false,50 rowToken: 0,51 touched: false,52 ws:53 Map(54 "w1" ->55 {56 conn: false,57 outputs: false,58 phase: Idle,59 res: RNone,60 slot: false,61 srv: SNone,62 token: 063 },64 "w2" ->65 {66 conn: true,67 outputs: false,68 phase: Pending,69 res: RNone,70 slot: true,71 srv: SNeed,72 token: 073 },74 "w3" ->75 {76 conn: false,77 outputs: false,78 phase: Idle,79 res: RNone,80 slot: false,81 srv: SNone,82 token: 083 }84 )85}8687[State 2]88{89 nextToken: 1,90 present: false,91 rowStale: false,92 rowToken: 0,93 touched: false,94 ws:95 Map(96 "w1" ->97 {98 conn: false,99 outputs: false,100 phase: Idle,101 res: RNone,102 slot: false,103 srv: SNone,104 token: 0105 },106 "w2" ->107 {108 conn: false,109 outputs: false,110 phase: Pending,111 res: RNone,112 slot: true,113 srv: SNone,114 token: 0115 },116 "w3" ->117 {118 conn: false,119 outputs: false,120 phase: Idle,121 res: RNone,122 slot: false,123 srv: SNone,124 token: 0125 }126 )127}128129[State 3]130{131 nextToken: 1,132 present: false,133 rowStale: false,134 rowToken: 0,135 touched: false,136 ws:137 Map(138 "w1" ->139 {140 conn: false,141 outputs: false,142 phase: Idle,143 res: RNone,144 slot: false,145 srv: SNone,146 token: 0147 },148 "w2" ->149 {150 conn: false,151 outputs: false,152 phase: Done,153 res: RUnavailable,154 slot: false,155 srv: SNone,156 token: 0157 },158 "w3" ->159 {160 conn: false,161 outputs: false,162 phase: Idle,163 res: RNone,164 slot: false,165 srv: SNone,166 token: 0167 }168 )169}170171[State 4]172{173 nextToken: 1,174 present: false,175 rowStale: false,176 rowToken: 0,177 touched: false,178 ws:179 Map(180 "w1" ->181 {182 conn: false,183 outputs: false,184 phase: Idle,185 res: RNone,186 slot: false,187 srv: SNone,188 token: 0189 },190 "w2" ->191 {192 conn: false,193 outputs: false,194 phase: Done,195 res: RUnavailable,196 slot: false,197 srv: SNone,198 token: 0199 },200 "w3" ->201 {202 conn: true,203 outputs: false,204 phase: Pending,205 res: RNone,206 slot: true,207 srv: SNeed,208 token: 0209 }210 )211}212213[State 5]214{215 nextToken: 1,216 present: false,217 rowStale: false,218 rowToken: 0,219 touched: false,220 ws:221 Map(222 "w1" ->223 {224 conn: false,225 outputs: false,226 phase: Idle,227 res: RNone,228 slot: false,229 srv: SNone,230 token: 0231 },232 "w2" ->233 {234 conn: false,235 outputs: false,236 phase: Done,237 res: RUnavailable,238 slot: false,239 srv: SNone,240 token: 0241 },242 "w3" ->243 {244 conn: false,245 outputs: false,246 phase: Pending,247 res: RNone,248 slot: true,249 srv: SNone,250 token: 0251 }252 )253}254255[State 6]256{257 nextToken: 1,258 present: false,259 rowStale: false,260 rowToken: 0,261 touched: false,262 ws:263 Map(264 "w1" ->265 {266 conn: false,267 outputs: false,268 phase: Idle,269 res: RNone,270 slot: false,271 srv: SNone,272 token: 0273 },274 "w2" ->275 {276 conn: false,277 outputs: false,278 phase: Idle,279 res: RNone,280 slot: false,281 srv: SNone,282 token: 0283 },284 "w3" ->285 {286 conn: false,287 outputs: false,288 phase: Pending,289 res: RNone,290 slot: true,291 srv: SNone,292 token: 0293 }294 )295}296297[State 7]298{299 nextToken: 1,300 present: false,301 rowStale: false,302 rowToken: 0,303 touched: false,304 ws:305 Map(306 "w1" ->307 {308 conn: false,309 outputs: false,310 phase: Idle,311 res: RNone,312 slot: false,313 srv: SNone,314 token: 0315 },316 "w2" ->317 {318 conn: false,319 outputs: false,320 phase: Idle,321 res: RNone,322 slot: false,323 srv: SNone,324 token: 0325 },326 "w3" ->327 {328 conn: true,329 outputs: false,330 phase: Pending,331 res: RNone,332 slot: true,333 srv: SNeed,334 token: 0335 }336 )337}338339[State 8]340{341 nextToken: 2,342 present: false,343 rowStale: false,344 rowToken: 1,345 touched: false,346 ws:347 Map(348 "w1" ->349 {350 conn: false,351 outputs: false,352 phase: Idle,353 res: RNone,354 slot: false,355 srv: SNone,356 token: 0357 },358 "w2" ->359 {360 conn: false,361 outputs: false,362 phase: Idle,363 res: RNone,364 slot: false,365 srv: SNone,366 token: 0367 },368 "w3" ->369 {370 conn: true,371 outputs: false,372 phase: Building,373 res: RNone,374 slot: true,375 srv: SHolder(1),376 token: 1377 }378 )379}380381[State 9]382{383 nextToken: 2,384 present: false,385 rowStale: false,386 rowToken: 1,387 touched: false,388 ws:389 Map(390 "w1" ->391 {392 conn: false,393 outputs: false,394 phase: Idle,395 res: RNone,396 slot: false,397 srv: SNone,398 token: 0399 },400 "w2" ->401 {402 conn: false,403 outputs: false,404 phase: Idle,405 res: RNone,406 slot: false,407 srv: SNone,408 token: 0409 },410 "w3" ->411 {412 conn: false,413 outputs: false,414 phase: Building,415 res: RNone,416 slot: true,417 srv: SNone,418 token: 1419 }420 )421}422423[State 10]424{425 nextToken: 2,426 present: false,427 rowStale: true,428 rowToken: 1,429 touched: false,430 ws:431 Map(432 "w1" ->433 {434 conn: false,435 outputs: false,436 phase: Idle,437 res: RNone,438 slot: false,439 srv: SNone,440 token: 0441 },442 "w2" ->443 {444 conn: false,445 outputs: false,446 phase: Idle,447 res: RNone,448 slot: false,449 srv: SNone,450 token: 0451 },452 "w3" ->453 {454 conn: false,455 outputs: false,456 phase: Building,457 res: RNone,458 slot: true,459 srv: SNone,460 token: 1461 }462 )463}464465[State 11]466{467 nextToken: 2,468 present: false,469 rowStale: true,470 rowToken: 1,471 touched: false,472 ws:473 Map(474 "w1" ->475 {476 conn: false,477 outputs: false,478 phase: Idle,479 res: RNone,480 slot: false,481 srv: SNone,482 token: 0483 },484 "w2" ->485 {486 conn: false,487 outputs: false,488 phase: Idle,489 res: RNone,490 slot: false,491 srv: SNone,492 token: 0493 },494 "w3" ->495 {496 conn: false,497 outputs: false,498 phase: Done,499 res: RUnavailable,500 slot: false,501 srv: SNone,502 token: 1503 }504 )505}506507[State 12]508{509 nextToken: 2,510 present: false,511 rowStale: true,512 rowToken: 1,513 touched: false,514 ws:515 Map(516 "w1" ->517 {518 conn: true,519 outputs: false,520 phase: Pending,521 res: RNone,522 slot: true,523 srv: SNeed,524 token: 0525 },526 "w2" ->527 {528 conn: false,529 outputs: false,530 phase: Idle,531 res: RNone,532 slot: false,533 srv: SNone,534 token: 0535 },536 "w3" ->537 {538 conn: false,539 outputs: false,540 phase: Done,541 res: RUnavailable,542 slot: false,543 srv: SNone,544 token: 1545 }546 )547}548549[State 13]550{551 nextToken: 2,552 present: false,553 rowStale: true,554 rowToken: 1,555 touched: false,556 ws:557 Map(558 "w1" ->559 {560 conn: true,561 outputs: false,562 phase: Pending,563 res: RNone,564 slot: true,565 srv: SNeed,566 token: 0567 },568 "w2" ->569 {570 conn: false,571 outputs: false,572 phase: Idle,573 res: RNone,574 slot: false,575 srv: SNone,576 token: 0577 },578 "w3" ->579 {580 conn: false,581 outputs: false,582 phase: Idle,583 res: RNone,584 slot: false,585 srv: SNone,586 token: 0587 }588 )589}590591[State 14]592{593 nextToken: 2,594 present: false,595 rowStale: true,596 rowToken: 1,597 touched: false,598 ws:599 Map(600 "w1" ->601 {602 conn: false,603 outputs: false,604 phase: Pending,605 res: RNone,606 slot: true,607 srv: SNone,608 token: 0609 },610 "w2" ->611 {612 conn: false,613 outputs: false,614 phase: Idle,615 res: RNone,616 slot: false,617 srv: SNone,618 token: 0619 },620 "w3" ->621 {622 conn: false,623 outputs: false,624 phase: Idle,625 res: RNone,626 slot: false,627 srv: SNone,628 token: 0629 }630 )631}632633[State 15]634{635 nextToken: 2,636 present: false,637 rowStale: true,638 rowToken: 1,639 touched: false,640 ws:641 Map(642 "w1" ->643 {644 conn: false,645 outputs: false,646 phase: Done,647 res: RUnavailable,648 slot: false,649 srv: SNone,650 token: 0651 },652 "w2" ->653 {654 conn: false,655 outputs: false,656 phase: Idle,657 res: RNone,658 slot: false,659 srv: SNone,660 token: 0661 },662 "w3" ->663 {664 conn: false,665 outputs: false,666 phase: Idle,667 res: RNone,668 slot: false,669 srv: SNone,670 token: 0671 }672 )673}674675[State 16]676{677 nextToken: 2,678 present: false,679 rowStale: true,680 rowToken: 1,681 touched: false,682 ws:683 Map(684 "w1" ->685 {686 conn: false,687 outputs: false,688 phase: Idle,689 res: RNone,690 slot: false,691 srv: SNone,692 token: 0693 },694 "w2" ->695 {696 conn: false,697 outputs: false,698 phase: Idle,699 res: RNone,700 slot: false,701 srv: SNone,702 token: 0703 },704 "w3" ->705 {706 conn: false,707 outputs: false,708 phase: Idle,709 res: RNone,710 slot: false,711 srv: SNone,712 token: 0713 }714 )715}716717[State 17]718{719 nextToken: 2,720 present: false,721 rowStale: true,722 rowToken: 1,723 touched: false,724 ws:725 Map(726 "w1" ->727 {728 conn: false,729 outputs: false,730 phase: Idle,731 res: RNone,732 slot: false,733 srv: SNone,734 token: 0735 },736 "w2" ->737 {738 conn: true,739 outputs: false,740 phase: Pending,741 res: RNone,742 slot: true,743 srv: SNeed,744 token: 0745 },746 "w3" ->747 {748 conn: false,749 outputs: false,750 phase: Idle,751 res: RNone,752 slot: false,753 srv: SNone,754 token: 0755 }756 )757}758759[State 18]760{761 nextToken: 3,762 present: false,763 rowStale: false,764 rowToken: 2,765 touched: false,766 ws:767 Map(768 "w1" ->769 {770 conn: false,771 outputs: false,772 phase: Idle,773 res: RNone,774 slot: false,775 srv: SNone,776 token: 0777 },778 "w2" ->779 {780 conn: true,781 outputs: false,782 phase: Building,783 res: RNone,784 slot: true,785 srv: SHolder(2),786 token: 2787 },788 "w3" ->789 {790 conn: false,791 outputs: false,792 phase: Idle,793 res: RNone,794 slot: false,795 srv: SNone,796 token: 0797 }798 )799}800801[State 19]802{803 nextToken: 3,804 present: false,805 rowStale: false,806 rowToken: 0,807 touched: false,808 ws:809 Map(810 "w1" ->811 {812 conn: false,813 outputs: false,814 phase: Idle,815 res: RNone,816 slot: false,817 srv: SNone,818 token: 0819 },820 "w2" ->821 {822 conn: false,823 outputs: false,824 phase: Done,825 res: RFailed,826 slot: false,827 srv: SNone,828 token: 2829 },830 "w3" ->831 {832 conn: false,833 outputs: false,834 phase: Idle,835 res: RNone,836 slot: false,837 srv: SNone,838 token: 0839 }840 )841}842843[State 20]844{845 nextToken: 3,846 present: false,847 rowStale: false,848 rowToken: 0,849 touched: false,850 ws:851 Map(852 "w1" ->853 {854 conn: true,855 outputs: false,856 phase: Pending,857 res: RNone,858 slot: true,859 srv: SNeed,860 token: 0861 },862 "w2" ->863 {864 conn: false,865 outputs: false,866 phase: Done,867 res: RFailed,868 slot: false,869 srv: SNone,870 token: 2871 },872 "w3" ->873 {874 conn: false,875 outputs: false,876 phase: Idle,877 res: RNone,878 slot: false,879 srv: SNone,880 token: 0881 }882 )883}884885[State 21]886{887 nextToken: 3,888 present: false,889 rowStale: false,890 rowToken: 0,891 touched: false,892 ws:893 Map(894 "w1" ->895 {896 conn: false,897 outputs: false,898 phase: Pending,899 res: RNone,900 slot: true,901 srv: SNone,902 token: 0903 },904 "w2" ->905 {906 conn: false,907 outputs: false,908 phase: Done,909 res: RFailed,910 slot: false,911 srv: SNone,912 token: 2913 },914 "w3" ->915 {916 conn: false,917 outputs: false,918 phase: Idle,919 res: RNone,920 slot: false,921 srv: SNone,922 token: 0923 }924 )925}926927[State 22]928{929 nextToken: 3,930 present: false,931 rowStale: false,932 rowToken: 0,933 touched: false,934 ws:935 Map(936 "w1" ->937 {938 conn: false,939 outputs: false,940 phase: Pending,941 res: RNone,942 slot: true,943 srv: SNone,944 token: 0945 },946 "w2" ->947 {948 conn: false,949 outputs: false,950 phase: Idle,951 res: RNone,952 slot: false,953 srv: SNone,954 token: 0955 },956 "w3" ->957 {958 conn: false,959 outputs: false,960 phase: Idle,961 res: RNone,962 slot: false,963 srv: SNone,964 token: 0965 }966 )967}968969[State 23]970{971 nextToken: 3,972 present: false,973 rowStale: false,974 rowToken: 0,975 touched: false,976 ws:977 Map(978 "w1" ->979 {980 conn: false,981 outputs: false,982 phase: Done,983 res: RUnavailable,984 slot: false,985 srv: SNone,986 token: 0987 },988 "w2" ->989 {990 conn: false,991 outputs: false,992 phase: Idle,993 res: RNone,994 slot: false,995 srv: SNone,996 token: 0997 },998 "w3" ->999 {1000 conn: false,1001 outputs: false,1002 phase: Idle,1003 res: RNone,1004 slot: false,1005 srv: SNone,1006 token: 01007 }1008 )1009}10101011[State 24]1012{1013 nextToken: 3,1014 present: false,1015 rowStale: false,1016 rowToken: 0,1017 touched: false,1018 ws:1019 Map(1020 "w1" ->1021 {1022 conn: false,1023 outputs: false,1024 phase: Done,1025 res: RUnavailable,1026 slot: false,1027 srv: SNone,1028 token: 01029 },1030 "w2" ->1031 {1032 conn: true,1033 outputs: false,1034 phase: Pending,1035 res: RNone,1036 slot: true,1037 srv: SNeed,1038 token: 01039 },1040 "w3" ->1041 {1042 conn: false,1043 outputs: false,1044 phase: Idle,1045 res: RNone,1046 slot: false,1047 srv: SNone,1048 token: 01049 }1050 )1051}10521053[State 25]1054{1055 nextToken: 3,1056 present: false,1057 rowStale: false,1058 rowToken: 0,1059 touched: false,1060 ws:1061 Map(1062 "w1" ->1063 {1064 conn: false,1065 outputs: false,1066 phase: Done,1067 res: RUnavailable,1068 slot: false,1069 srv: SNone,1070 token: 01071 },1072 "w2" ->1073 {1074 conn: false,1075 outputs: false,1076 phase: Pending,1077 res: RNone,1078 slot: true,1079 srv: SNone,1080 token: 01081 },1082 "w3" ->1083 {1084 conn: false,1085 outputs: false,1086 phase: Idle,1087 res: RNone,1088 slot: false,1089 srv: SNone,1090 token: 01091 }1092 )1093}10941095[State 26]1096{1097 nextToken: 3,1098 present: false,1099 rowStale: false,1100 rowToken: 0,1101 touched: false,1102 ws:1103 Map(1104 "w1" ->1105 {1106 conn: false,1107 outputs: false,1108 phase: Idle,1109 res: RNone,1110 slot: false,1111 srv: SNone,1112 token: 01113 },1114 "w2" ->1115 {1116 conn: false,1117 outputs: false,1118 phase: Pending,1119 res: RNone,1120 slot: true,1121 srv: SNone,1122 token: 01123 },1124 "w3" ->1125 {1126 conn: false,1127 outputs: false,1128 phase: Idle,1129 res: RNone,1130 slot: false,1131 srv: SNone,1132 token: 01133 }1134 )1135}11361137[State 27]1138{1139 nextToken: 3,1140 present: false,1141 rowStale: false,1142 rowToken: 0,1143 touched: false,1144 ws:1145 Map(1146 "w1" ->1147 {1148 conn: false,1149 outputs: false,1150 phase: Idle,1151 res: RNone,1152 slot: false,1153 srv: SNone,1154 token: 01155 },1156 "w2" ->1157 {1158 conn: true,1159 outputs: false,1160 phase: Pending,1161 res: RNone,1162 slot: true,1163 srv: SNeed,1164 token: 01165 },1166 "w3" ->1167 {1168 conn: false,1169 outputs: false,1170 phase: Idle,1171 res: RNone,1172 slot: false,1173 srv: SNone,1174 token: 01175 }1176 )1177}11781179[State 28]1180{1181 nextToken: 3,1182 present: false,1183 rowStale: false,1184 rowToken: 0,1185 touched: false,1186 ws:1187 Map(1188 "w1" ->1189 {1190 conn: false,1191 outputs: false,1192 phase: Idle,1193 res: RNone,1194 slot: false,1195 srv: SNone,1196 token: 01197 },1198 "w2" ->1199 {1200 conn: false,1201 outputs: false,1202 phase: Pending,1203 res: RNone,1204 slot: true,1205 srv: SNone,1206 token: 01207 },1208 "w3" ->1209 {1210 conn: false,1211 outputs: false,1212 phase: Idle,1213 res: RNone,1214 slot: false,1215 srv: SNone,1216 token: 01217 }1218 )1219}12201221[State 29]1222{1223 nextToken: 3,1224 present: false,1225 rowStale: false,1226 rowToken: 0,1227 touched: false,1228 ws:1229 Map(1230 "w1" ->1231 {1232 conn: false,1233 outputs: false,1234 phase: Idle,1235 res: RNone,1236 slot: false,1237 srv: SNone,1238 token: 01239 },1240 "w2" ->1241 {1242 conn: true,1243 outputs: false,1244 phase: Pending,1245 res: RNone,1246 slot: true,1247 srv: SNeed,1248 token: 01249 },1250 "w3" ->1251 {1252 conn: false,1253 outputs: false,1254 phase: Idle,1255 res: RNone,1256 slot: false,1257 srv: SNone,1258 token: 01259 }1260 )1261}12621263[State 30]1264{1265 nextToken: 3,1266 present: false,1267 rowStale: false,1268 rowToken: 0,1269 touched: false,1270 ws:1271 Map(1272 "w1" ->1273 {1274 conn: false,1275 outputs: false,1276 phase: Idle,1277 res: RNone,1278 slot: false,1279 srv: SNone,1280 token: 01281 },1282 "w2" ->1283 {1284 conn: false,1285 outputs: false,1286 phase: Pending,1287 res: RNone,1288 slot: true,1289 srv: SNone,1290 token: 01291 },1292 "w3" ->1293 {1294 conn: false,1295 outputs: false,1296 phase: Idle,1297 res: RNone,1298 slot: false,1299 srv: SNone,1300 token: 01301 }1302 )1303}13041305[ok] No violation found (6627ms at 3018 traces/second).1306Trace length statistics: max=31, min=31, average=31.001307You may increase --max-samples and --max-steps.1308Use --verbosity to produce more (or less) output.1309Use --seed=0x2c5078be84b7d636 --backend=rust to reproduce.1310Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [■■■■ ] 10% | ETA: 2s | 2006/20000 samples | 10670 samples/sRunning... [■■■■ ] 10% | ETA: 2s | 2006/20000 samples | 10670 samples/sRunning... [■■■■■■ ] 15% | ETA: 2s | 3040/20000 samples | 8761 samples/sRunning... [■■■■■■■■ ] 18% | ETA: 3s | 3755/20000 samples | 8075 samples/sRunning... [■■■■■■■■ ] 18% | ETA: 3s | 3755/20000 samples | 8075 samples/sRunning... [■■■■■■■■■ ] 23% | ETA: 3s | 4686/20000 samples | 7620 samples/sRunning... [■■■■■■■■■■■ ] 27% | ETA: 3s | 5577/20000 samples | 7132 samples/sRunning... [■■■■■■■■■■■■ ] 31% | ETA: 2s | 6242/20000 samples | 7053 samples/sRunning... [■■■■■■■■■■■■ ] 31% | ETA: 2s | 6242/20000 samples | 7053 samples/sRunning... [■■■■■■■■■■■■■■■ ] 37% | ETA: 2s | 7560/20000 samples | 6799 samples/sRunning... [■■■■■■■■■■■■■■■ ] 37% | ETA: 2s | 7560/20000 samples | 6799 samples/sRunning... [■■■■■■■■■■■■■■■■ ] 40% | ETA: 2s | 8171/20000 samples | 6600 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 44% | ETA: 2s | 8936/20000 samples | 6443 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 44% | ETA: 2s | 8936/20000 samples | 6443 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■ ] 51% | ETA: 2s | 10334/20000 samples | 6359 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■ ] 51% | ETA: 2s | 10334/20000 samples | 6359 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■ ] 51% | ETA: 2s | 10334/20000 samples | 6359 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■ ] 58% | ETA: 2s | 11754/20000 samples | 6323 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■ ] 58% | ETA: 2s | 11754/20000 samples | 6323 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 64% | ETA: 2s | 12991/20000 samples | 6282 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 68% | ETA: 2s | 13633/20000 samples | 6282 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 71% | ETA: 1s | 14308/20000 samples | 6264 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 75% | ETA: 1s | 15157/20000 samples | 6225 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 78% | ETA: 1s | 15716/20000 samples | 6151 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 78% | ETA: 1s | 15716/20000 samples | 6151 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 78% | ETA: 1s | 15716/20000 samples | 6151 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 84% | ETA: 1s | 16961/20000 samples | 6108 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 88% | ETA: 1s | 17703/20000 samples | 6094 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 88% | ETA: 1s | 17703/20000 samples | 6094 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 93% | ETA: 1s | 18677/20000 samples | 6068 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 93% | ETA: 1s | 18677/20000 samples | 6068 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19928/20000 samples | 6017 samples/sAn example execution:13111312[State 0]1313{1314 nextToken: 1,1315 present: false,1316 rowStale: false,1317 rowToken: 0,1318 touched: false,1319 ws:1320 Map(1321 "w1" ->1322 {1323 conn: false,1324 outputs: false,1325 phase: Idle,1326 res: RNone,1327 slot: false,1328 srv: SNone,1329 token: 01330 },1331 "w2" ->1332 {1333 conn: false,1334 outputs: false,1335 phase: Idle,1336 res: RNone,1337 slot: false,1338 srv: SNone,1339 token: 01340 },1341 "w3" ->1342 {1343 conn: false,1344 outputs: false,1345 phase: Idle,1346 res: RNone,1347 slot: false,1348 srv: SNone,1349 token: 01350 }1351 )1352}13531354[State 1]1355{1356 nextToken: 1,1357 present: false,1358 rowStale: false,1359 rowToken: 0,1360 touched: false,1361 ws:1362 Map(1363 "w1" ->1364 {1365 conn: false,1366 outputs: false,1367 phase: Idle,1368 res: RNone,1369 slot: false,1370 srv: SNone,1371 token: 01372 },1373 "w2" ->1374 {1375 conn: true,1376 outputs: false,1377 phase: Pending,1378 res: RNone,1379 slot: true,1380 srv: SNeed,1381 token: 01382 },1383 "w3" ->1384 {1385 conn: false,1386 outputs: false,1387 phase: Idle,1388 res: RNone,1389 slot: false,1390 srv: SNone,1391 token: 01392 }1393 )1394}13951396[State 2]1397{1398 nextToken: 1,1399 present: false,1400 rowStale: false,1401 rowToken: 0,1402 touched: false,1403 ws:1404 Map(1405 "w1" ->1406 {1407 conn: false,1408 outputs: false,1409 phase: Idle,1410 res: RNone,1411 slot: false,1412 srv: SNone,1413 token: 01414 },1415 "w2" ->1416 {1417 conn: false,1418 outputs: false,1419 phase: Pending,1420 res: RNone,1421 slot: true,1422 srv: SNone,1423 token: 01424 },1425 "w3" ->1426 {1427 conn: false,1428 outputs: false,1429 phase: Idle,1430 res: RNone,1431 slot: false,1432 srv: SNone,1433 token: 01434 }1435 )1436}14371438[State 3]1439{1440 nextToken: 1,1441 present: false,1442 rowStale: false,1443 rowToken: 0,1444 touched: false,1445 ws:1446 Map(1447 "w1" ->1448 {1449 conn: false,1450 outputs: false,1451 phase: Idle,1452 res: RNone,1453 slot: false,1454 srv: SNone,1455 token: 01456 },1457 "w2" ->1458 {1459 conn: true,1460 outputs: false,1461 phase: Pending,1462 res: RNone,1463 slot: true,1464 srv: SNeed,1465 token: 01466 },1467 "w3" ->1468 {1469 conn: false,1470 outputs: false,1471 phase: Idle,1472 res: RNone,1473 slot: false,1474 srv: SNone,1475 token: 01476 }1477 )1478}14791480[State 4]1481{1482 nextToken: 1,1483 present: false,1484 rowStale: false,1485 rowToken: 0,1486 touched: false,1487 ws:1488 Map(1489 "w1" ->1490 {1491 conn: false,1492 outputs: false,1493 phase: Idle,1494 res: RNone,1495 slot: false,1496 srv: SNone,1497 token: 01498 },1499 "w2" ->1500 {1501 conn: false,1502 outputs: false,1503 phase: Pending,1504 res: RNone,1505 slot: true,1506 srv: SNone,1507 token: 01508 },1509 "w3" ->1510 {1511 conn: false,1512 outputs: false,1513 phase: Idle,1514 res: RNone,1515 slot: false,1516 srv: SNone,1517 token: 01518 }1519 )1520}15211522[State 5]1523{1524 nextToken: 1,1525 present: false,1526 rowStale: false,1527 rowToken: 0,1528 touched: false,1529 ws:1530 Map(1531 "w1" ->1532 {1533 conn: false,1534 outputs: false,1535 phase: Idle,1536 res: RNone,1537 slot: false,1538 srv: SNone,1539 token: 01540 },1541 "w2" ->1542 {1543 conn: true,1544 outputs: false,1545 phase: Pending,1546 res: RNone,1547 slot: true,1548 srv: SNeed,1549 token: 01550 },1551 "w3" ->1552 {1553 conn: false,1554 outputs: false,1555 phase: Idle,1556 res: RNone,1557 slot: false,1558 srv: SNone,1559 token: 01560 }1561 )1562}15631564[State 6]1565{1566 nextToken: 1,1567 present: false,1568 rowStale: false,1569 rowToken: 0,1570 touched: false,1571 ws:1572 Map(1573 "w1" ->1574 {1575 conn: false,1576 outputs: false,1577 phase: Idle,1578 res: RNone,1579 slot: false,1580 srv: SNone,1581 token: 01582 },1583 "w2" ->1584 {1585 conn: false,1586 outputs: false,1587 phase: Pending,1588 res: RNone,1589 slot: true,1590 srv: SNone,1591 token: 01592 },1593 "w3" ->1594 {1595 conn: false,1596 outputs: false,1597 phase: Idle,1598 res: RNone,1599 slot: false,1600 srv: SNone,1601 token: 01602 }1603 )1604}16051606[State 7]1607{1608 nextToken: 1,1609 present: false,1610 rowStale: false,1611 rowToken: 0,1612 touched: false,1613 ws:1614 Map(1615 "w1" ->1616 {1617 conn: false,1618 outputs: false,1619 phase: Idle,1620 res: RNone,1621 slot: false,1622 srv: SNone,1623 token: 01624 },1625 "w2" ->1626 {1627 conn: true,1628 outputs: false,1629 phase: Pending,1630 res: RNone,1631 slot: true,1632 srv: SNeed,1633 token: 01634 },1635 "w3" ->1636 {1637 conn: false,1638 outputs: false,1639 phase: Idle,1640 res: RNone,1641 slot: false,1642 srv: SNone,1643 token: 01644 }1645 )1646}16471648[State 8]1649{1650 nextToken: 1,1651 present: false,1652 rowStale: false,1653 rowToken: 0,1654 touched: false,1655 ws:1656 Map(1657 "w1" ->1658 {1659 conn: false,1660 outputs: false,1661 phase: Idle,1662 res: RNone,1663 slot: false,1664 srv: SNone,1665 token: 01666 },1667 "w2" ->1668 {1669 conn: false,1670 outputs: false,1671 phase: Pending,1672 res: RNone,1673 slot: true,1674 srv: SNone,1675 token: 01676 },1677 "w3" ->1678 {1679 conn: false,1680 outputs: false,1681 phase: Idle,1682 res: RNone,1683 slot: false,1684 srv: SNone,1685 token: 01686 }1687 )1688}16891690[State 9]1691{1692 nextToken: 1,1693 present: false,1694 rowStale: false,1695 rowToken: 0,1696 touched: false,1697 ws:1698 Map(1699 "w1" ->1700 {1701 conn: false,1702 outputs: false,1703 phase: Idle,1704 res: RNone,1705 slot: false,1706 srv: SNone,1707 token: 01708 },1709 "w2" ->1710 {1711 conn: true,1712 outputs: false,1713 phase: Pending,1714 res: RNone,1715 slot: true,1716 srv: SNeed,1717 token: 01718 },1719 "w3" ->1720 {1721 conn: false,1722 outputs: false,1723 phase: Idle,1724 res: RNone,1725 slot: false,1726 srv: SNone,1727 token: 01728 }1729 )1730}17311732[State 10]1733{1734 nextToken: 1,1735 present: false,1736 rowStale: false,1737 rowToken: 0,1738 touched: false,1739 ws:1740 Map(1741 "w1" ->1742 {1743 conn: false,1744 outputs: false,1745 phase: Idle,1746 res: RNone,1747 slot: false,1748 srv: SNone,1749 token: 01750 },1751 "w2" ->1752 {1753 conn: false,1754 outputs: false,1755 phase: Pending,1756 res: RNone,1757 slot: true,1758 srv: SNone,1759 token: 01760 },1761 "w3" ->1762 {1763 conn: false,1764 outputs: false,1765 phase: Idle,1766 res: RNone,1767 slot: false,1768 srv: SNone,1769 token: 01770 }1771 )1772}17731774[State 11]1775{1776 nextToken: 1,1777 present: false,1778 rowStale: false,1779 rowToken: 0,1780 touched: false,1781 ws:1782 Map(1783 "w1" ->1784 {1785 conn: false,1786 outputs: false,1787 phase: Idle,1788 res: RNone,1789 slot: false,1790 srv: SNone,1791 token: 01792 },1793 "w2" ->1794 {1795 conn: true,1796 outputs: false,1797 phase: Pending,1798 res: RNone,1799 slot: true,1800 srv: SNeed,1801 token: 01802 },1803 "w3" ->1804 {1805 conn: false,1806 outputs: false,1807 phase: Idle,1808 res: RNone,1809 slot: false,1810 srv: SNone,1811 token: 01812 }1813 )1814}18151816[State 12]1817{1818 nextToken: 1,1819 present: false,1820 rowStale: false,1821 rowToken: 0,1822 touched: false,1823 ws:1824 Map(1825 "w1" ->1826 {1827 conn: false,1828 outputs: false,1829 phase: Idle,1830 res: RNone,1831 slot: false,1832 srv: SNone,1833 token: 01834 },1835 "w2" ->1836 {1837 conn: false,1838 outputs: false,1839 phase: Pending,1840 res: RNone,1841 slot: true,1842 srv: SNone,1843 token: 01844 },1845 "w3" ->1846 {1847 conn: false,1848 outputs: false,1849 phase: Idle,1850 res: RNone,1851 slot: false,1852 srv: SNone,1853 token: 01854 }1855 )1856}18571858[State 13]1859{1860 nextToken: 1,1861 present: false,1862 rowStale: false,1863 rowToken: 0,1864 touched: false,1865 ws:1866 Map(1867 "w1" ->1868 {1869 conn: false,1870 outputs: false,1871 phase: Idle,1872 res: RNone,1873 slot: false,1874 srv: SNone,1875 token: 01876 },1877 "w2" ->1878 {1879 conn: true,1880 outputs: false,1881 phase: Pending,1882 res: RNone,1883 slot: true,1884 srv: SNeed,1885 token: 01886 },1887 "w3" ->1888 {1889 conn: false,1890 outputs: false,1891 phase: Idle,1892 res: RNone,1893 slot: false,1894 srv: SNone,1895 token: 01896 }1897 )1898}18991900[State 14]1901{1902 nextToken: 1,1903 present: false,1904 rowStale: false,1905 rowToken: 0,1906 touched: false,1907 ws:1908 Map(1909 "w1" ->1910 {1911 conn: false,1912 outputs: false,1913 phase: Idle,1914 res: RNone,1915 slot: false,1916 srv: SNone,1917 token: 01918 },1919 "w2" ->1920 {1921 conn: false,1922 outputs: false,1923 phase: Pending,1924 res: RNone,1925 slot: true,1926 srv: SNone,1927 token: 01928 },1929 "w3" ->1930 {1931 conn: false,1932 outputs: false,1933 phase: Idle,1934 res: RNone,1935 slot: false,1936 srv: SNone,1937 token: 01938 }1939 )1940}19411942[State 15]1943{1944 nextToken: 1,1945 present: false,1946 rowStale: false,1947 rowToken: 0,1948 touched: false,1949 ws:1950 Map(1951 "w1" ->1952 {1953 conn: false,1954 outputs: false,1955 phase: Idle,1956 res: RNone,1957 slot: false,1958 srv: SNone,1959 token: 01960 },1961 "w2" ->1962 {1963 conn: true,1964 outputs: false,1965 phase: Pending,1966 res: RNone,1967 slot: true,1968 srv: SNeed,1969 token: 01970 },1971 "w3" ->1972 {1973 conn: false,1974 outputs: false,1975 phase: Idle,1976 res: RNone,1977 slot: false,1978 srv: SNone,1979 token: 01980 }1981 )1982}19831984[State 16]1985{1986 nextToken: 1,1987 present: false,1988 rowStale: false,1989 rowToken: 0,1990 touched: false,1991 ws:1992 Map(1993 "w1" ->1994 {1995 conn: false,1996 outputs: false,1997 phase: Idle,1998 res: RNone,1999 slot: false,2000 srv: SNone,2001 token: 02002 },2003 "w2" ->2004 {2005 conn: false,2006 outputs: false,2007 phase: Pending,2008 res: RNone,2009 slot: true,2010 srv: SNone,2011 token: 02012 },2013 "w3" ->2014 {2015 conn: false,2016 outputs: false,2017 phase: Idle,2018 res: RNone,2019 slot: false,2020 srv: SNone,2021 token: 02022 }2023 )2024}20252026[State 17]2027{2028 nextToken: 1,2029 present: false,2030 rowStale: false,2031 rowToken: 0,2032 touched: false,2033 ws:2034 Map(2035 "w1" ->2036 {2037 conn: false,2038 outputs: false,2039 phase: Idle,2040 res: RNone,2041 slot: false,2042 srv: SNone,2043 token: 02044 },2045 "w2" ->2046 {2047 conn: true,2048 outputs: false,2049 phase: Pending,2050 res: RNone,2051 slot: true,2052 srv: SNeed,2053 token: 02054 },2055 "w3" ->2056 {2057 conn: false,2058 outputs: false,2059 phase: Idle,2060 res: RNone,2061 slot: false,2062 srv: SNone,2063 token: 02064 }2065 )2066}20672068[State 18]2069{2070 nextToken: 2,2071 present: false,2072 rowStale: false,2073 rowToken: 1,2074 touched: false,2075 ws:2076 Map(2077 "w1" ->2078 {2079 conn: false,2080 outputs: false,2081 phase: Idle,2082 res: RNone,2083 slot: false,2084 srv: SNone,2085 token: 02086 },2087 "w2" ->2088 {2089 conn: true,2090 outputs: false,2091 phase: Building,2092 res: RNone,2093 slot: true,2094 srv: SHolder(1),2095 token: 12096 },2097 "w3" ->2098 {2099 conn: false,2100 outputs: false,2101 phase: Idle,2102 res: RNone,2103 slot: false,2104 srv: SNone,2105 token: 02106 }2107 )2108}21092110[State 19]2111{2112 nextToken: 2,2113 present: false,2114 rowStale: false,2115 rowToken: 1,2116 touched: false,2117 ws:2118 Map(2119 "w1" ->2120 {2121 conn: false,2122 outputs: false,2123 phase: Idle,2124 res: RNone,2125 slot: false,2126 srv: SNone,2127 token: 02128 },2129 "w2" ->2130 {2131 conn: false,2132 outputs: false,2133 phase: Building,2134 res: RNone,2135 slot: true,2136 srv: SNone,2137 token: 12138 },2139 "w3" ->2140 {2141 conn: false,2142 outputs: false,2143 phase: Idle,2144 res: RNone,2145 slot: false,2146 srv: SNone,2147 token: 02148 }2149 )2150}21512152[State 20]2153{2154 nextToken: 2,2155 present: false,2156 rowStale: false,2157 rowToken: 1,2158 touched: false,2159 ws:2160 Map(2161 "w1" ->2162 {2163 conn: false,2164 outputs: false,2165 phase: Idle,2166 res: RNone,2167 slot: false,2168 srv: SNone,2169 token: 02170 },2171 "w2" ->2172 {2173 conn: true,2174 outputs: false,2175 phase: Building,2176 res: RNone,2177 slot: true,2178 srv: SNeed,2179 token: 12180 },2181 "w3" ->2182 {2183 conn: false,2184 outputs: false,2185 phase: Idle,2186 res: RNone,2187 slot: false,2188 srv: SNone,2189 token: 02190 }2191 )2192}21932194[State 21]2195{2196 nextToken: 2,2197 present: false,2198 rowStale: false,2199 rowToken: 0,2200 touched: false,2201 ws:2202 Map(2203 "w1" ->2204 {2205 conn: false,2206 outputs: false,2207 phase: Idle,2208 res: RNone,2209 slot: false,2210 srv: SNone,2211 token: 02212 },2213 "w2" ->2214 {2215 conn: false,2216 outputs: false,2217 phase: Done,2218 res: RUnavailable,2219 slot: false,2220 srv: SNone,2221 token: 12222 },2223 "w3" ->2224 {2225 conn: false,2226 outputs: false,2227 phase: Idle,2228 res: RNone,2229 slot: false,2230 srv: SNone,2231 token: 02232 }2233 )2234}22352236[State 22]2237{2238 nextToken: 2,2239 present: false,2240 rowStale: false,2241 rowToken: 0,2242 touched: false,2243 ws:2244 Map(2245 "w1" ->2246 {2247 conn: true,2248 outputs: false,2249 phase: Pending,2250 res: RNone,2251 slot: true,2252 srv: SNeed,2253 token: 02254 },2255 "w2" ->2256 {2257 conn: false,2258 outputs: false,2259 phase: Done,2260 res: RUnavailable,2261 slot: false,2262 srv: SNone,2263 token: 12264 },2265 "w3" ->2266 {2267 conn: false,2268 outputs: false,2269 phase: Idle,2270 res: RNone,2271 slot: false,2272 srv: SNone,2273 token: 02274 }2275 )2276}22772278[State 23]2279{2280 nextToken: 2,2281 present: false,2282 rowStale: false,2283 rowToken: 0,2284 touched: false,2285 ws:2286 Map(2287 "w1" ->2288 {2289 conn: false,2290 outputs: false,2291 phase: Pending,2292 res: RNone,2293 slot: true,2294 srv: SNone,2295 token: 02296 },2297 "w2" ->2298 {2299 conn: false,2300 outputs: false,2301 phase: Done,2302 res: RUnavailable,2303 slot: false,2304 srv: SNone,2305 token: 12306 },2307 "w3" ->2308 {2309 conn: false,2310 outputs: false,2311 phase: Idle,2312 res: RNone,2313 slot: false,2314 srv: SNone,2315 token: 02316 }2317 )2318}23192320[State 24]2321{2322 nextToken: 2,2323 present: false,2324 rowStale: false,2325 rowToken: 0,2326 touched: false,2327 ws:2328 Map(2329 "w1" ->2330 {2331 conn: true,2332 outputs: false,2333 phase: Pending,2334 res: RNone,2335 slot: true,2336 srv: SNeed,2337 token: 02338 },2339 "w2" ->2340 {2341 conn: false,2342 outputs: false,2343 phase: Done,2344 res: RUnavailable,2345 slot: false,2346 srv: SNone,2347 token: 12348 },2349 "w3" ->2350 {2351 conn: false,2352 outputs: false,2353 phase: Idle,2354 res: RNone,2355 slot: false,2356 srv: SNone,2357 token: 02358 }2359 )2360}23612362[State 25]2363{2364 nextToken: 3,2365 present: false,2366 rowStale: false,2367 rowToken: 2,2368 touched: false,2369 ws:2370 Map(2371 "w1" ->2372 {2373 conn: true,2374 outputs: false,2375 phase: Building,2376 res: RNone,2377 slot: true,2378 srv: SHolder(2),2379 token: 22380 },2381 "w2" ->2382 {2383 conn: false,2384 outputs: false,2385 phase: Done,2386 res: RUnavailable,2387 slot: false,2388 srv: SNone,2389 token: 12390 },2391 "w3" ->2392 {2393 conn: false,2394 outputs: false,2395 phase: Idle,2396 res: RNone,2397 slot: false,2398 srv: SNone,2399 token: 02400 }2401 )2402}24032404[State 26]2405{2406 nextToken: 3,2407 present: false,2408 rowStale: false,2409 rowToken: 0,2410 touched: false,2411 ws:2412 Map(2413 "w1" ->2414 {2415 conn: false,2416 outputs: false,2417 phase: Done,2418 res: RFailed,2419 slot: false,2420 srv: SNone,2421 token: 22422 },2423 "w2" ->2424 {2425 conn: false,2426 outputs: false,2427 phase: Done,2428 res: RUnavailable,2429 slot: false,2430 srv: SNone,2431 token: 12432 },2433 "w3" ->2434 {2435 conn: false,2436 outputs: false,2437 phase: Idle,2438 res: RNone,2439 slot: false,2440 srv: SNone,2441 token: 02442 }2443 )2444}24452446[State 27]2447{2448 nextToken: 3,2449 present: false,2450 rowStale: false,2451 rowToken: 0,2452 touched: false,2453 ws:2454 Map(2455 "w1" ->2456 {2457 conn: false,2458 outputs: false,2459 phase: Done,2460 res: RFailed,2461 slot: false,2462 srv: SNone,2463 token: 22464 },2465 "w2" ->2466 {2467 conn: false,2468 outputs: false,2469 phase: Done,2470 res: RUnavailable,2471 slot: false,2472 srv: SNone,2473 token: 12474 },2475 "w3" ->2476 {2477 conn: true,2478 outputs: false,2479 phase: Pending,2480 res: RNone,2481 slot: true,2482 srv: SNeed,2483 token: 02484 }2485 )2486}24872488[State 28]2489{2490 nextToken: 4,2491 present: false,2492 rowStale: false,2493 rowToken: 3,2494 touched: false,2495 ws:2496 Map(2497 "w1" ->2498 {2499 conn: false,2500 outputs: false,2501 phase: Done,2502 res: RFailed,2503 slot: false,2504 srv: SNone,2505 token: 22506 },2507 "w2" ->2508 {2509 conn: false,2510 outputs: false,2511 phase: Done,2512 res: RUnavailable,2513 slot: false,2514 srv: SNone,2515 token: 12516 },2517 "w3" ->2518 {2519 conn: true,2520 outputs: false,2521 phase: Building,2522 res: RNone,2523 slot: true,2524 srv: SHolder(3),2525 token: 32526 }2527 )2528}25292530[State 29]2531{2532 nextToken: 4,2533 present: false,2534 rowStale: false,2535 rowToken: 3,2536 touched: false,2537 ws:2538 Map(2539 "w1" ->2540 {2541 conn: false,2542 outputs: false,2543 phase: Done,2544 res: RFailed,2545 slot: false,2546 srv: SNone,2547 token: 22548 },2549 "w2" ->2550 {2551 conn: false,2552 outputs: false,2553 phase: Done,2554 res: RUnavailable,2555 slot: false,2556 srv: SNone,2557 token: 12558 },2559 "w3" ->2560 {2561 conn: false,2562 outputs: false,2563 phase: Building,2564 res: RNone,2565 slot: true,2566 srv: SNone,2567 token: 32568 }2569 )2570}25712572[State 30]2573{2574 nextToken: 4,2575 present: false,2576 rowStale: false,2577 rowToken: 3,2578 touched: false,2579 ws:2580 Map(2581 "w1" ->2582 {2583 conn: false,2584 outputs: false,2585 phase: Done,2586 res: RFailed,2587 slot: false,2588 srv: SNone,2589 token: 22590 },2591 "w2" ->2592 {2593 conn: false,2594 outputs: false,2595 phase: Done,2596 res: RUnavailable,2597 slot: false,2598 srv: SNone,2599 token: 12600 },2601 "w3" ->2602 {2603 conn: true,2604 outputs: false,2605 phase: Building,2606 res: RNone,2607 slot: true,2608 srv: SNeed,2609 token: 32610 }2611 )2612}26132614[ok] No violation found (3404ms at 5875 traces/second).2615Trace length statistics: max=31, min=9, average=18.712616You may increase --max-samples and --max-steps.2617Use --verbosity to produce more (or less) output.2618Use --seed=0xaf2b0b3c492483bc --backend=rust to reproduce.