nix-grpc-store-spec
checks.aarch64-linux.spec
· build #803
· raw
1tribuchet: building on eliza2An example execution:34[State 0]5{6 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),7 schedFixed::scheduler::crashes: 0,8 schedFixed::scheduler::entry: [],9 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),10 schedFixed::scheduler::mAssigned: Set(),11 schedFixed::scheduler::mBuild: Set(),12 schedFixed::scheduler::mDone: Set(),13 schedFixed::scheduler::mExpect: Set(),14 schedFixed::scheduler::mResult: Set(),15 schedFixed::scheduler::mRetry: Set(),16 schedFixed::scheduler::mRevoke: Set(),17 schedFixed::scheduler::mSchedule: Set(),18 schedFixed::scheduler::published: 0,19 schedFixed::scheduler::publishedBy: Set(),20 schedFixed::scheduler::ws:21 Map(22 "w1" ->23 {24 attached: Set(),25 built: false,26 expecting: false,27 running: false,28 session: true,29 up: true30 },31 "w2" ->32 {33 attached: Set(),34 built: false,35 expecting: false,36 running: false,37 session: true,38 up: true39 }40 )41}4243[State 1]44{45 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),46 schedFixed::scheduler::crashes: 0,47 schedFixed::scheduler::entry: [],48 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),49 schedFixed::scheduler::mAssigned: Set(),50 schedFixed::scheduler::mBuild: Set(),51 schedFixed::scheduler::mDone: Set(),52 schedFixed::scheduler::mExpect: Set(),53 schedFixed::scheduler::mResult: Set(),54 schedFixed::scheduler::mRetry: Set(),55 schedFixed::scheduler::mRevoke: Set(),56 schedFixed::scheduler::mSchedule: Set("c1"),57 schedFixed::scheduler::published: 0,58 schedFixed::scheduler::publishedBy: Set(),59 schedFixed::scheduler::ws:60 Map(61 "w1" ->62 {63 attached: Set(),64 built: false,65 expecting: false,66 running: false,67 session: true,68 up: true69 },70 "w2" ->71 {72 attached: Set(),73 built: false,74 expecting: false,75 running: false,76 session: true,77 up: true78 }79 )80}8182[State 2]83{84 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),85 schedFixed::scheduler::crashes: 1,86 schedFixed::scheduler::entry: [],87 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),88 schedFixed::scheduler::mAssigned: Set(),89 schedFixed::scheduler::mBuild: Set(),90 schedFixed::scheduler::mDone: Set(),91 schedFixed::scheduler::mExpect: Set(),92 schedFixed::scheduler::mResult: Set(),93 schedFixed::scheduler::mRetry: Set(),94 schedFixed::scheduler::mRevoke: Set(),95 schedFixed::scheduler::mSchedule: Set("c1"),96 schedFixed::scheduler::published: 0,97 schedFixed::scheduler::publishedBy: Set(),98 schedFixed::scheduler::ws:99 Map(100 "w1" ->101 {102 attached: Set(),103 built: false,104 expecting: false,105 running: false,106 session: true,107 up: true108 },109 "w2" ->110 {111 attached: Set(),112 built: false,113 expecting: false,114 running: false,115 session: false,116 up: false117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),124 schedFixed::scheduler::crashes: 2,125 schedFixed::scheduler::entry: [],126 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),127 schedFixed::scheduler::mAssigned: Set(),128 schedFixed::scheduler::mBuild: Set(),129 schedFixed::scheduler::mDone: Set(),130 schedFixed::scheduler::mExpect: Set(),131 schedFixed::scheduler::mResult: Set(),132 schedFixed::scheduler::mRetry: Set("c1"),133 schedFixed::scheduler::mRevoke: Set(),134 schedFixed::scheduler::mSchedule: Set(),135 schedFixed::scheduler::published: 0,136 schedFixed::scheduler::publishedBy: Set(),137 schedFixed::scheduler::ws:138 Map(139 "w1" ->140 {141 attached: Set(),142 built: false,143 expecting: false,144 running: false,145 session: false,146 up: true147 },148 "w2" ->149 {150 attached: Set(),151 built: false,152 expecting: false,153 running: false,154 session: false,155 up: false156 }157 )158}159160[State 4]161{162 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),163 schedFixed::scheduler::crashes: 2,164 schedFixed::scheduler::entry: [],165 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),166 schedFixed::scheduler::mAssigned: Set(),167 schedFixed::scheduler::mBuild: Set(),168 schedFixed::scheduler::mDone: Set(),169 schedFixed::scheduler::mExpect: Set(),170 schedFixed::scheduler::mResult: Set(),171 schedFixed::scheduler::mRetry: Set("c1"),172 schedFixed::scheduler::mRevoke: Set(),173 schedFixed::scheduler::mSchedule: Set(),174 schedFixed::scheduler::published: 0,175 schedFixed::scheduler::publishedBy: Set(),176 schedFixed::scheduler::ws:177 Map(178 "w1" ->179 {180 attached: Set(),181 built: false,182 expecting: false,183 running: false,184 session: false,185 up: true186 },187 "w2" ->188 {189 attached: Set(),190 built: false,191 expecting: false,192 running: false,193 session: true,194 up: true195 }196 )197}198199[State 5]200{201 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),202 schedFixed::scheduler::crashes: 2,203 schedFixed::scheduler::entry: [],204 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),205 schedFixed::scheduler::mAssigned: Set(),206 schedFixed::scheduler::mBuild: Set(),207 schedFixed::scheduler::mDone: Set(),208 schedFixed::scheduler::mExpect: Set(),209 schedFixed::scheduler::mResult: Set(),210 schedFixed::scheduler::mRetry: Set("c1"),211 schedFixed::scheduler::mRevoke: Set(),212 schedFixed::scheduler::mSchedule: Set("c2"),213 schedFixed::scheduler::published: 0,214 schedFixed::scheduler::publishedBy: Set(),215 schedFixed::scheduler::ws:216 Map(217 "w1" ->218 {219 attached: Set(),220 built: false,221 expecting: false,222 running: false,223 session: false,224 up: true225 },226 "w2" ->227 {228 attached: Set(),229 built: false,230 expecting: false,231 running: false,232 session: true,233 up: true234 }235 )236}237238[State 6]239{240 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),241 schedFixed::scheduler::crashes: 2,242 schedFixed::scheduler::entry: [],243 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),244 schedFixed::scheduler::mAssigned: Set(),245 schedFixed::scheduler::mBuild: Set(),246 schedFixed::scheduler::mDone: Set(),247 schedFixed::scheduler::mExpect: Set(),248 schedFixed::scheduler::mResult: Set(),249 schedFixed::scheduler::mRetry: Set(),250 schedFixed::scheduler::mRevoke: Set(),251 schedFixed::scheduler::mSchedule: Set("c1", "c2"),252 schedFixed::scheduler::published: 0,253 schedFixed::scheduler::publishedBy: Set(),254 schedFixed::scheduler::ws:255 Map(256 "w1" ->257 {258 attached: Set(),259 built: false,260 expecting: false,261 running: false,262 session: false,263 up: true264 },265 "w2" ->266 {267 attached: Set(),268 built: false,269 expecting: false,270 running: false,271 session: true,272 up: true273 }274 )275}276277[State 7]278{279 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),280 schedFixed::scheduler::crashes: 2,281 schedFixed::scheduler::entry:282 [{ followers: Set("c1"), leased: true, worker: "w2" }],283 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),284 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),285 schedFixed::scheduler::mBuild: Set(),286 schedFixed::scheduler::mDone: Set(),287 schedFixed::scheduler::mExpect: Set("w2"),288 schedFixed::scheduler::mResult: Set(),289 schedFixed::scheduler::mRetry: Set(),290 schedFixed::scheduler::mRevoke: Set(),291 schedFixed::scheduler::mSchedule: Set("c2"),292 schedFixed::scheduler::published: 0,293 schedFixed::scheduler::publishedBy: Set(),294 schedFixed::scheduler::ws:295 Map(296 "w1" ->297 {298 attached: Set(),299 built: false,300 expecting: false,301 running: false,302 session: false,303 up: true304 },305 "w2" ->306 {307 attached: Set(),308 built: false,309 expecting: false,310 running: false,311 session: true,312 up: true313 }314 )315}316317[State 8]318{319 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),320 schedFixed::scheduler::crashes: 2,321 schedFixed::scheduler::entry:322 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],323 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),324 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),325 schedFixed::scheduler::mBuild: Set(),326 schedFixed::scheduler::mDone: Set(),327 schedFixed::scheduler::mExpect: Set("w2"),328 schedFixed::scheduler::mResult: Set(),329 schedFixed::scheduler::mRetry: Set(),330 schedFixed::scheduler::mRevoke: Set(),331 schedFixed::scheduler::mSchedule: Set(),332 schedFixed::scheduler::published: 0,333 schedFixed::scheduler::publishedBy: Set(),334 schedFixed::scheduler::ws:335 Map(336 "w1" ->337 {338 attached: Set(),339 built: false,340 expecting: false,341 running: false,342 session: false,343 up: true344 },345 "w2" ->346 {347 attached: Set(),348 built: false,349 expecting: false,350 running: false,351 session: true,352 up: true353 }354 )355}356357[State 9]358{359 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),360 schedFixed::scheduler::crashes: 2,361 schedFixed::scheduler::entry:362 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],363 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),364 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),365 schedFixed::scheduler::mBuild: Set(),366 schedFixed::scheduler::mDone: Set(),367 schedFixed::scheduler::mExpect: Set("w2"),368 schedFixed::scheduler::mResult: Set(),369 schedFixed::scheduler::mRetry: Set(),370 schedFixed::scheduler::mRevoke: Set(),371 schedFixed::scheduler::mSchedule: Set(),372 schedFixed::scheduler::published: 0,373 schedFixed::scheduler::publishedBy: Set(),374 schedFixed::scheduler::ws:375 Map(376 "w1" ->377 {378 attached: Set(),379 built: false,380 expecting: false,381 running: false,382 session: true,383 up: true384 },385 "w2" ->386 {387 attached: Set(),388 built: false,389 expecting: false,390 running: false,391 session: true,392 up: true393 }394 )395}396397[State 10]398{399 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),400 schedFixed::scheduler::crashes: 2,401 schedFixed::scheduler::entry:402 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],403 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),404 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),405 schedFixed::scheduler::mBuild: Set(("c2", "w2")),406 schedFixed::scheduler::mDone: Set(),407 schedFixed::scheduler::mExpect: Set("w2"),408 schedFixed::scheduler::mResult: Set(),409 schedFixed::scheduler::mRetry: Set(),410 schedFixed::scheduler::mRevoke: Set(),411 schedFixed::scheduler::mSchedule: Set(),412 schedFixed::scheduler::published: 0,413 schedFixed::scheduler::publishedBy: Set(),414 schedFixed::scheduler::ws:415 Map(416 "w1" ->417 {418 attached: Set(),419 built: false,420 expecting: false,421 running: false,422 session: true,423 up: true424 },425 "w2" ->426 {427 attached: Set(),428 built: false,429 expecting: false,430 running: false,431 session: true,432 up: true433 }434 )435}436437[State 11]438{439 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),440 schedFixed::scheduler::crashes: 2,441 schedFixed::scheduler::entry:442 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],443 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),444 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),445 schedFixed::scheduler::mBuild: Set(),446 schedFixed::scheduler::mDone: Set(),447 schedFixed::scheduler::mExpect: Set("w2"),448 schedFixed::scheduler::mResult: Set(),449 schedFixed::scheduler::mRetry: Set("c2"),450 schedFixed::scheduler::mRevoke: Set(),451 schedFixed::scheduler::mSchedule: Set(),452 schedFixed::scheduler::published: 0,453 schedFixed::scheduler::publishedBy: Set(),454 schedFixed::scheduler::ws:455 Map(456 "w1" ->457 {458 attached: Set(),459 built: false,460 expecting: false,461 running: false,462 session: true,463 up: true464 },465 "w2" ->466 {467 attached: Set(),468 built: false,469 expecting: false,470 running: false,471 session: true,472 up: true473 }474 )475}476477[State 12]478{479 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),480 schedFixed::scheduler::crashes: 2,481 schedFixed::scheduler::entry:482 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],483 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),484 schedFixed::scheduler::mAssigned: Set(),485 schedFixed::scheduler::mBuild: Set(("c1", "w2")),486 schedFixed::scheduler::mDone: Set(),487 schedFixed::scheduler::mExpect: Set("w2"),488 schedFixed::scheduler::mResult: Set(),489 schedFixed::scheduler::mRetry: Set("c2"),490 schedFixed::scheduler::mRevoke: Set(),491 schedFixed::scheduler::mSchedule: Set(),492 schedFixed::scheduler::published: 0,493 schedFixed::scheduler::publishedBy: Set(),494 schedFixed::scheduler::ws:495 Map(496 "w1" ->497 {498 attached: Set(),499 built: false,500 expecting: false,501 running: false,502 session: true,503 up: true504 },505 "w2" ->506 {507 attached: Set(),508 built: false,509 expecting: false,510 running: false,511 session: true,512 up: true513 }514 )515}516517[State 13]518{519 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),520 schedFixed::scheduler::crashes: 2,521 schedFixed::scheduler::entry:522 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],523 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),524 schedFixed::scheduler::mAssigned: Set(),525 schedFixed::scheduler::mBuild: Set(),526 schedFixed::scheduler::mDone: Set(),527 schedFixed::scheduler::mExpect: Set("w2"),528 schedFixed::scheduler::mResult: Set(),529 schedFixed::scheduler::mRetry: Set("c1", "c2"),530 schedFixed::scheduler::mRevoke: Set(),531 schedFixed::scheduler::mSchedule: Set(),532 schedFixed::scheduler::published: 0,533 schedFixed::scheduler::publishedBy: Set(),534 schedFixed::scheduler::ws:535 Map(536 "w1" ->537 {538 attached: Set(),539 built: false,540 expecting: false,541 running: false,542 session: true,543 up: true544 },545 "w2" ->546 {547 attached: Set(),548 built: false,549 expecting: false,550 running: false,551 session: true,552 up: true553 }554 )555}556557[State 14]558{559 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),560 schedFixed::scheduler::crashes: 2,561 schedFixed::scheduler::entry:562 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],563 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),564 schedFixed::scheduler::mAssigned: Set(),565 schedFixed::scheduler::mBuild: Set(),566 schedFixed::scheduler::mDone: Set(),567 schedFixed::scheduler::mExpect: Set("w2"),568 schedFixed::scheduler::mResult: Set(),569 schedFixed::scheduler::mRetry: Set("c2"),570 schedFixed::scheduler::mRevoke: Set(),571 schedFixed::scheduler::mSchedule: Set("c1"),572 schedFixed::scheduler::published: 0,573 schedFixed::scheduler::publishedBy: Set(),574 schedFixed::scheduler::ws:575 Map(576 "w1" ->577 {578 attached: Set(),579 built: false,580 expecting: false,581 running: false,582 session: true,583 up: true584 },585 "w2" ->586 {587 attached: Set(),588 built: false,589 expecting: false,590 running: false,591 session: true,592 up: true593 }594 )595}596597[State 15]598{599 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),600 schedFixed::scheduler::crashes: 2,601 schedFixed::scheduler::entry:602 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],603 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),604 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),605 schedFixed::scheduler::mBuild: Set(),606 schedFixed::scheduler::mDone: Set(),607 schedFixed::scheduler::mExpect: Set("w2"),608 schedFixed::scheduler::mResult: Set(),609 schedFixed::scheduler::mRetry: Set("c2"),610 schedFixed::scheduler::mRevoke: Set(),611 schedFixed::scheduler::mSchedule: Set(),612 schedFixed::scheduler::published: 0,613 schedFixed::scheduler::publishedBy: Set(),614 schedFixed::scheduler::ws:615 Map(616 "w1" ->617 {618 attached: Set(),619 built: false,620 expecting: false,621 running: false,622 session: true,623 up: true624 },625 "w2" ->626 {627 attached: Set(),628 built: false,629 expecting: false,630 running: false,631 session: true,632 up: true633 }634 )635}636637[State 16]638{639 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),640 schedFixed::scheduler::crashes: 2,641 schedFixed::scheduler::entry:642 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],643 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),644 schedFixed::scheduler::mAssigned: Set(),645 schedFixed::scheduler::mBuild: Set(("c1", "w2")),646 schedFixed::scheduler::mDone: Set(),647 schedFixed::scheduler::mExpect: Set("w2"),648 schedFixed::scheduler::mResult: Set(),649 schedFixed::scheduler::mRetry: Set("c2"),650 schedFixed::scheduler::mRevoke: Set(),651 schedFixed::scheduler::mSchedule: Set(),652 schedFixed::scheduler::published: 0,653 schedFixed::scheduler::publishedBy: Set(),654 schedFixed::scheduler::ws:655 Map(656 "w1" ->657 {658 attached: Set(),659 built: false,660 expecting: false,661 running: false,662 session: true,663 up: true664 },665 "w2" ->666 {667 attached: Set(),668 built: false,669 expecting: false,670 running: false,671 session: true,672 up: true673 }674 )675}676677[State 17]678{679 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),680 schedFixed::scheduler::crashes: 2,681 schedFixed::scheduler::entry:682 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],683 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),684 schedFixed::scheduler::mAssigned: Set(),685 schedFixed::scheduler::mBuild: Set(("c1", "w2")),686 schedFixed::scheduler::mDone: Set(),687 schedFixed::scheduler::mExpect: Set("w2"),688 schedFixed::scheduler::mResult: Set(),689 schedFixed::scheduler::mRetry: Set(),690 schedFixed::scheduler::mRevoke: Set(),691 schedFixed::scheduler::mSchedule: Set("c2"),692 schedFixed::scheduler::published: 0,693 schedFixed::scheduler::publishedBy: Set(),694 schedFixed::scheduler::ws:695 Map(696 "w1" ->697 {698 attached: Set(),699 built: false,700 expecting: false,701 running: false,702 session: true,703 up: true704 },705 "w2" ->706 {707 attached: Set(),708 built: false,709 expecting: false,710 running: false,711 session: true,712 up: true713 }714 )715}716717[State 18]718{719 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),720 schedFixed::scheduler::crashes: 2,721 schedFixed::scheduler::entry:722 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],723 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),724 schedFixed::scheduler::mAssigned: Set(),725 schedFixed::scheduler::mBuild: Set(),726 schedFixed::scheduler::mDone: Set(),727 schedFixed::scheduler::mExpect: Set("w2"),728 schedFixed::scheduler::mResult: Set(),729 schedFixed::scheduler::mRetry: Set("c1"),730 schedFixed::scheduler::mRevoke: Set(),731 schedFixed::scheduler::mSchedule: Set("c2"),732 schedFixed::scheduler::published: 0,733 schedFixed::scheduler::publishedBy: Set(),734 schedFixed::scheduler::ws:735 Map(736 "w1" ->737 {738 attached: Set(),739 built: false,740 expecting: false,741 running: false,742 session: true,743 up: true744 },745 "w2" ->746 {747 attached: Set(),748 built: false,749 expecting: false,750 running: false,751 session: true,752 up: true753 }754 )755}756757[State 19]758{759 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),760 schedFixed::scheduler::crashes: 2,761 schedFixed::scheduler::entry:762 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],763 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),764 schedFixed::scheduler::mAssigned: Set(),765 schedFixed::scheduler::mBuild: Set(),766 schedFixed::scheduler::mDone: Set(),767 schedFixed::scheduler::mExpect: Set("w2"),768 schedFixed::scheduler::mResult: Set(),769 schedFixed::scheduler::mRetry: Set(),770 schedFixed::scheduler::mRevoke: Set(),771 schedFixed::scheduler::mSchedule: Set("c1", "c2"),772 schedFixed::scheduler::published: 0,773 schedFixed::scheduler::publishedBy: Set(),774 schedFixed::scheduler::ws:775 Map(776 "w1" ->777 {778 attached: Set(),779 built: false,780 expecting: false,781 running: false,782 session: true,783 up: true784 },785 "w2" ->786 {787 attached: Set(),788 built: false,789 expecting: false,790 running: false,791 session: true,792 up: true793 }794 )795}796797[State 20]798{799 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),800 schedFixed::scheduler::crashes: 2,801 schedFixed::scheduler::entry:802 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],803 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),804 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),805 schedFixed::scheduler::mBuild: Set(),806 schedFixed::scheduler::mDone: Set(),807 schedFixed::scheduler::mExpect: Set("w2"),808 schedFixed::scheduler::mResult: Set(),809 schedFixed::scheduler::mRetry: Set(),810 schedFixed::scheduler::mRevoke: Set(),811 schedFixed::scheduler::mSchedule: Set("c1"),812 schedFixed::scheduler::published: 0,813 schedFixed::scheduler::publishedBy: Set(),814 schedFixed::scheduler::ws:815 Map(816 "w1" ->817 {818 attached: Set(),819 built: false,820 expecting: false,821 running: false,822 session: true,823 up: true824 },825 "w2" ->826 {827 attached: Set(),828 built: false,829 expecting: false,830 running: false,831 session: true,832 up: true833 }834 )835}836837[State 21]838{839 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),840 schedFixed::scheduler::crashes: 2,841 schedFixed::scheduler::entry:842 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],843 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),844 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),845 schedFixed::scheduler::mBuild: Set(),846 schedFixed::scheduler::mDone: Set(),847 schedFixed::scheduler::mExpect: Set(),848 schedFixed::scheduler::mResult: Set(),849 schedFixed::scheduler::mRetry: Set(),850 schedFixed::scheduler::mRevoke: Set(),851 schedFixed::scheduler::mSchedule: Set("c1"),852 schedFixed::scheduler::published: 0,853 schedFixed::scheduler::publishedBy: Set(),854 schedFixed::scheduler::ws:855 Map(856 "w1" ->857 {858 attached: Set(),859 built: false,860 expecting: false,861 running: false,862 session: true,863 up: true864 },865 "w2" ->866 {867 attached: Set(),868 built: false,869 expecting: true,870 running: true,871 session: true,872 up: true873 }874 )875}876877[State 22]878{879 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),880 schedFixed::scheduler::crashes: 2,881 schedFixed::scheduler::entry:882 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],883 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),884 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),885 schedFixed::scheduler::mBuild: Set(),886 schedFixed::scheduler::mDone: Set(),887 schedFixed::scheduler::mExpect: Set(),888 schedFixed::scheduler::mResult: Set(),889 schedFixed::scheduler::mRetry: Set(),890 schedFixed::scheduler::mRevoke: Set(),891 schedFixed::scheduler::mSchedule: Set(),892 schedFixed::scheduler::published: 0,893 schedFixed::scheduler::publishedBy: Set(),894 schedFixed::scheduler::ws:895 Map(896 "w1" ->897 {898 attached: Set(),899 built: false,900 expecting: false,901 running: false,902 session: true,903 up: true904 },905 "w2" ->906 {907 attached: Set(),908 built: false,909 expecting: true,910 running: true,911 session: true,912 up: true913 }914 )915}916917[State 23]918{919 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),920 schedFixed::scheduler::crashes: 2,921 schedFixed::scheduler::entry:922 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],923 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),924 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),925 schedFixed::scheduler::mBuild: Set(),926 schedFixed::scheduler::mDone: Set("w2"),927 schedFixed::scheduler::mExpect: Set(),928 schedFixed::scheduler::mResult: Set(),929 schedFixed::scheduler::mRetry: Set(),930 schedFixed::scheduler::mRevoke: Set(),931 schedFixed::scheduler::mSchedule: Set(),932 schedFixed::scheduler::published: 1,933 schedFixed::scheduler::publishedBy: Set("w2"),934 schedFixed::scheduler::ws:935 Map(936 "w1" ->937 {938 attached: Set(),939 built: false,940 expecting: false,941 running: false,942 session: true,943 up: true944 },945 "w2" ->946 {947 attached: Set(),948 built: true,949 expecting: false,950 running: false,951 session: true,952 up: true953 }954 )955}956957[State 24]958{959 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),960 schedFixed::scheduler::crashes: 2,961 schedFixed::scheduler::entry:962 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],963 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),964 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),965 schedFixed::scheduler::mBuild: Set(("c1", "w2")),966 schedFixed::scheduler::mDone: Set("w2"),967 schedFixed::scheduler::mExpect: Set(),968 schedFixed::scheduler::mResult: Set(),969 schedFixed::scheduler::mRetry: Set(),970 schedFixed::scheduler::mRevoke: Set(),971 schedFixed::scheduler::mSchedule: Set(),972 schedFixed::scheduler::published: 1,973 schedFixed::scheduler::publishedBy: Set("w2"),974 schedFixed::scheduler::ws:975 Map(976 "w1" ->977 {978 attached: Set(),979 built: false,980 expecting: false,981 running: false,982 session: true,983 up: true984 },985 "w2" ->986 {987 attached: Set(),988 built: true,989 expecting: false,990 running: false,991 session: true,992 up: true993 }994 )995}996997[State 25]998{999 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),1000 schedFixed::scheduler::crashes: 2,1001 schedFixed::scheduler::entry: [],1002 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1003 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1004 schedFixed::scheduler::mBuild: Set(("c1", "w2")),1005 schedFixed::scheduler::mDone: Set(),1006 schedFixed::scheduler::mExpect: Set(),1007 schedFixed::scheduler::mResult: Set(),1008 schedFixed::scheduler::mRetry: Set(),1009 schedFixed::scheduler::mRevoke: Set(),1010 schedFixed::scheduler::mSchedule: Set(),1011 schedFixed::scheduler::published: 1,1012 schedFixed::scheduler::publishedBy: Set("w2"),1013 schedFixed::scheduler::ws:1014 Map(1015 "w1" ->1016 {1017 attached: Set(),1018 built: false,1019 expecting: false,1020 running: false,1021 session: true,1022 up: true1023 },1024 "w2" ->1025 {1026 attached: Set(),1027 built: true,1028 expecting: false,1029 running: false,1030 session: true,1031 up: true1032 }1033 )1034}10351036[State 26]1037{1038 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),1039 schedFixed::scheduler::crashes: 2,1040 schedFixed::scheduler::entry: [],1041 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1042 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1043 schedFixed::scheduler::mBuild: Set(),1044 schedFixed::scheduler::mDone: Set(),1045 schedFixed::scheduler::mExpect: Set(),1046 schedFixed::scheduler::mResult: Set("c1"),1047 schedFixed::scheduler::mRetry: Set(),1048 schedFixed::scheduler::mRevoke: Set(),1049 schedFixed::scheduler::mSchedule: Set(),1050 schedFixed::scheduler::published: 1,1051 schedFixed::scheduler::publishedBy: Set("w2"),1052 schedFixed::scheduler::ws:1053 Map(1054 "w1" ->1055 {1056 attached: Set(),1057 built: false,1058 expecting: false,1059 running: false,1060 session: true,1061 up: true1062 },1063 "w2" ->1064 {1065 attached: Set(),1066 built: true,1067 expecting: false,1068 running: false,1069 session: true,1070 up: true1071 }1072 )1073}10741075[State 27]1076{1077 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CQueued),1078 schedFixed::scheduler::crashes: 2,1079 schedFixed::scheduler::entry: [],1080 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1081 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1082 schedFixed::scheduler::mBuild: Set(),1083 schedFixed::scheduler::mDone: Set(),1084 schedFixed::scheduler::mExpect: Set(),1085 schedFixed::scheduler::mResult: Set(),1086 schedFixed::scheduler::mRetry: Set(),1087 schedFixed::scheduler::mRevoke: Set(),1088 schedFixed::scheduler::mSchedule: Set(),1089 schedFixed::scheduler::published: 1,1090 schedFixed::scheduler::publishedBy: Set("w2"),1091 schedFixed::scheduler::ws:1092 Map(1093 "w1" ->1094 {1095 attached: Set(),1096 built: false,1097 expecting: false,1098 running: false,1099 session: true,1100 up: true1101 },1102 "w2" ->1103 {1104 attached: Set(),1105 built: true,1106 expecting: false,1107 running: false,1108 session: true,1109 up: true1110 }1111 )1112}11131114[State 28]1115{1116 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w2")),1117 schedFixed::scheduler::crashes: 2,1118 schedFixed::scheduler::entry: [],1119 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1120 schedFixed::scheduler::mAssigned: Set(),1121 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1122 schedFixed::scheduler::mDone: Set(),1123 schedFixed::scheduler::mExpect: Set(),1124 schedFixed::scheduler::mResult: Set(),1125 schedFixed::scheduler::mRetry: Set(),1126 schedFixed::scheduler::mRevoke: Set(),1127 schedFixed::scheduler::mSchedule: Set(),1128 schedFixed::scheduler::published: 1,1129 schedFixed::scheduler::publishedBy: Set("w2"),1130 schedFixed::scheduler::ws:1131 Map(1132 "w1" ->1133 {1134 attached: Set(),1135 built: false,1136 expecting: false,1137 running: false,1138 session: true,1139 up: true1140 },1141 "w2" ->1142 {1143 attached: Set(),1144 built: true,1145 expecting: false,1146 running: false,1147 session: true,1148 up: true1149 }1150 )1151}11521153[State 29]1154{1155 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w2")),1156 schedFixed::scheduler::crashes: 2,1157 schedFixed::scheduler::entry: [],1158 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1159 schedFixed::scheduler::mAssigned: Set(),1160 schedFixed::scheduler::mBuild: Set(),1161 schedFixed::scheduler::mDone: Set(),1162 schedFixed::scheduler::mExpect: Set(),1163 schedFixed::scheduler::mResult: Set("c2"),1164 schedFixed::scheduler::mRetry: Set(),1165 schedFixed::scheduler::mRevoke: Set(),1166 schedFixed::scheduler::mSchedule: Set(),1167 schedFixed::scheduler::published: 1,1168 schedFixed::scheduler::publishedBy: Set("w2"),1169 schedFixed::scheduler::ws:1170 Map(1171 "w1" ->1172 {1173 attached: Set(),1174 built: false,1175 expecting: false,1176 running: false,1177 session: true,1178 up: true1179 },1180 "w2" ->1181 {1182 attached: Set(),1183 built: true,1184 expecting: false,1185 running: false,1186 session: true,1187 up: true1188 }1189 )1190}11911192[State 30]1193{1194 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),1195 schedFixed::scheduler::crashes: 2,1196 schedFixed::scheduler::entry: [],1197 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1198 schedFixed::scheduler::mAssigned: Set(),1199 schedFixed::scheduler::mBuild: Set(),1200 schedFixed::scheduler::mDone: Set(),1201 schedFixed::scheduler::mExpect: Set(),1202 schedFixed::scheduler::mResult: Set(),1203 schedFixed::scheduler::mRetry: Set(),1204 schedFixed::scheduler::mRevoke: Set(),1205 schedFixed::scheduler::mSchedule: Set(),1206 schedFixed::scheduler::published: 1,1207 schedFixed::scheduler::publishedBy: Set("w2"),1208 schedFixed::scheduler::ws:1209 Map(1210 "w1" ->1211 {1212 attached: Set(),1213 built: false,1214 expecting: false,1215 running: false,1216 session: true,1217 up: true1218 },1219 "w2" ->1220 {1221 attached: Set(),1222 built: true,1223 expecting: false,1224 running: false,1225 session: true,1226 up: true1227 }1228 )1229}12301231[ok] No violation found (508ms at 59055 traces/second).1232Trace length statistics: max=27, min=16, average=18.851233You may increase --max-samples and --max-steps.1234Use --verbosity to produce more (or less) output.1235Use --seed=0xe071e7b8471042ba --backend=rust to reproduce.1236An example execution:12371238[State 0]1239{1240 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1241 schedNoRevoke::scheduler::crashes: 0,1242 schedNoRevoke::scheduler::entry: [],1243 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1244 schedNoRevoke::scheduler::mAssigned: Set(),1245 schedNoRevoke::scheduler::mBuild: Set(),1246 schedNoRevoke::scheduler::mDone: Set(),1247 schedNoRevoke::scheduler::mExpect: Set(),1248 schedNoRevoke::scheduler::mResult: Set(),1249 schedNoRevoke::scheduler::mRetry: Set(),1250 schedNoRevoke::scheduler::mRevoke: Set(),1251 schedNoRevoke::scheduler::mSchedule: Set(),1252 schedNoRevoke::scheduler::published: 0,1253 schedNoRevoke::scheduler::publishedBy: Set(),1254 schedNoRevoke::scheduler::ws:1255 Map(1256 "w1" ->1257 {1258 attached: Set(),1259 built: false,1260 expecting: false,1261 running: false,1262 session: true,1263 up: true1264 },1265 "w2" ->1266 {1267 attached: Set(),1268 built: false,1269 expecting: false,1270 running: false,1271 session: true,1272 up: true1273 }1274 )1275}12761277[State 1]1278{1279 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1280 schedNoRevoke::scheduler::crashes: 1,1281 schedNoRevoke::scheduler::entry: [],1282 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1283 schedNoRevoke::scheduler::mAssigned: Set(),1284 schedNoRevoke::scheduler::mBuild: Set(),1285 schedNoRevoke::scheduler::mDone: Set(),1286 schedNoRevoke::scheduler::mExpect: Set(),1287 schedNoRevoke::scheduler::mResult: Set(),1288 schedNoRevoke::scheduler::mRetry: Set(),1289 schedNoRevoke::scheduler::mRevoke: Set(),1290 schedNoRevoke::scheduler::mSchedule: Set(),1291 schedNoRevoke::scheduler::published: 0,1292 schedNoRevoke::scheduler::publishedBy: Set(),1293 schedNoRevoke::scheduler::ws:1294 Map(1295 "w1" ->1296 {1297 attached: Set(),1298 built: false,1299 expecting: false,1300 running: false,1301 session: true,1302 up: true1303 },1304 "w2" ->1305 {1306 attached: Set(),1307 built: false,1308 expecting: false,1309 running: false,1310 session: false,1311 up: false1312 }1313 )1314}13151316[State 2]1317{1318 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1319 schedNoRevoke::scheduler::crashes: 1,1320 schedNoRevoke::scheduler::entry: [],1321 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1322 schedNoRevoke::scheduler::mAssigned: Set(),1323 schedNoRevoke::scheduler::mBuild: Set(),1324 schedNoRevoke::scheduler::mDone: Set(),1325 schedNoRevoke::scheduler::mExpect: Set(),1326 schedNoRevoke::scheduler::mResult: Set(),1327 schedNoRevoke::scheduler::mRetry: Set(),1328 schedNoRevoke::scheduler::mRevoke: Set(),1329 schedNoRevoke::scheduler::mSchedule: Set("c1"),1330 schedNoRevoke::scheduler::published: 0,1331 schedNoRevoke::scheduler::publishedBy: Set(),1332 schedNoRevoke::scheduler::ws:1333 Map(1334 "w1" ->1335 {1336 attached: Set(),1337 built: false,1338 expecting: false,1339 running: false,1340 session: true,1341 up: true1342 },1343 "w2" ->1344 {1345 attached: Set(),1346 built: false,1347 expecting: false,1348 running: false,1349 session: false,1350 up: false1351 }1352 )1353}13541355[State 3]1356{1357 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1358 schedNoRevoke::scheduler::crashes: 1,1359 schedNoRevoke::scheduler::entry:1360 [{ followers: Set("c1"), leased: true, worker: "w1" }],1361 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1362 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1363 schedNoRevoke::scheduler::mBuild: Set(),1364 schedNoRevoke::scheduler::mDone: Set(),1365 schedNoRevoke::scheduler::mExpect: Set("w1"),1366 schedNoRevoke::scheduler::mResult: Set(),1367 schedNoRevoke::scheduler::mRetry: Set(),1368 schedNoRevoke::scheduler::mRevoke: Set(),1369 schedNoRevoke::scheduler::mSchedule: Set(),1370 schedNoRevoke::scheduler::published: 0,1371 schedNoRevoke::scheduler::publishedBy: Set(),1372 schedNoRevoke::scheduler::ws:1373 Map(1374 "w1" ->1375 {1376 attached: Set(),1377 built: false,1378 expecting: false,1379 running: false,1380 session: true,1381 up: true1382 },1383 "w2" ->1384 {1385 attached: Set(),1386 built: false,1387 expecting: false,1388 running: false,1389 session: false,1390 up: false1391 }1392 )1393}13941395[State 4]1396{1397 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1398 schedNoRevoke::scheduler::crashes: 1,1399 schedNoRevoke::scheduler::entry:1400 [{ followers: Set("c1"), leased: true, worker: "w1" }],1401 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1402 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1403 schedNoRevoke::scheduler::mBuild: Set(),1404 schedNoRevoke::scheduler::mDone: Set(),1405 schedNoRevoke::scheduler::mExpect: Set(),1406 schedNoRevoke::scheduler::mResult: Set(),1407 schedNoRevoke::scheduler::mRetry: Set(),1408 schedNoRevoke::scheduler::mRevoke: Set(),1409 schedNoRevoke::scheduler::mSchedule: Set(),1410 schedNoRevoke::scheduler::published: 0,1411 schedNoRevoke::scheduler::publishedBy: Set(),1412 schedNoRevoke::scheduler::ws:1413 Map(1414 "w1" ->1415 {1416 attached: Set(),1417 built: false,1418 expecting: true,1419 running: true,1420 session: true,1421 up: true1422 },1423 "w2" ->1424 {1425 attached: Set(),1426 built: false,1427 expecting: false,1428 running: false,1429 session: false,1430 up: false1431 }1432 )1433}14341435[State 5]1436{1437 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1438 schedNoRevoke::scheduler::crashes: 2,1439 schedNoRevoke::scheduler::entry: [],1440 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1441 schedNoRevoke::scheduler::mAssigned: Set(),1442 schedNoRevoke::scheduler::mBuild: Set(),1443 schedNoRevoke::scheduler::mDone: Set(),1444 schedNoRevoke::scheduler::mExpect: Set(),1445 schedNoRevoke::scheduler::mResult: Set(),1446 schedNoRevoke::scheduler::mRetry: Set("c1"),1447 schedNoRevoke::scheduler::mRevoke: Set(),1448 schedNoRevoke::scheduler::mSchedule: Set(),1449 schedNoRevoke::scheduler::published: 0,1450 schedNoRevoke::scheduler::publishedBy: Set(),1451 schedNoRevoke::scheduler::ws:1452 Map(1453 "w1" ->1454 {1455 attached: Set(),1456 built: false,1457 expecting: true,1458 running: true,1459 session: false,1460 up: true1461 },1462 "w2" ->1463 {1464 attached: Set(),1465 built: false,1466 expecting: false,1467 running: false,1468 session: false,1469 up: false1470 }1471 )1472}14731474[State 6]1475{1476 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1477 schedNoRevoke::scheduler::crashes: 2,1478 schedNoRevoke::scheduler::entry: [],1479 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1480 schedNoRevoke::scheduler::mAssigned: Set(),1481 schedNoRevoke::scheduler::mBuild: Set(),1482 schedNoRevoke::scheduler::mDone: Set(),1483 schedNoRevoke::scheduler::mExpect: Set(),1484 schedNoRevoke::scheduler::mResult: Set(),1485 schedNoRevoke::scheduler::mRetry: Set("c1"),1486 schedNoRevoke::scheduler::mRevoke: Set(),1487 schedNoRevoke::scheduler::mSchedule: Set(),1488 schedNoRevoke::scheduler::published: 0,1489 schedNoRevoke::scheduler::publishedBy: Set(),1490 schedNoRevoke::scheduler::ws:1491 Map(1492 "w1" ->1493 {1494 attached: Set(),1495 built: false,1496 expecting: true,1497 running: true,1498 session: false,1499 up: true1500 },1501 "w2" ->1502 {1503 attached: Set(),1504 built: false,1505 expecting: false,1506 running: false,1507 session: true,1508 up: true1509 }1510 )1511}15121513[State 7]1514{1515 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1516 schedNoRevoke::scheduler::crashes: 2,1517 schedNoRevoke::scheduler::entry: [],1518 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1519 schedNoRevoke::scheduler::mAssigned: Set(),1520 schedNoRevoke::scheduler::mBuild: Set(),1521 schedNoRevoke::scheduler::mDone: Set(),1522 schedNoRevoke::scheduler::mExpect: Set(),1523 schedNoRevoke::scheduler::mResult: Set(),1524 schedNoRevoke::scheduler::mRetry: Set("c1"),1525 schedNoRevoke::scheduler::mRevoke: Set(),1526 schedNoRevoke::scheduler::mSchedule: Set("c2"),1527 schedNoRevoke::scheduler::published: 0,1528 schedNoRevoke::scheduler::publishedBy: Set(),1529 schedNoRevoke::scheduler::ws:1530 Map(1531 "w1" ->1532 {1533 attached: Set(),1534 built: false,1535 expecting: true,1536 running: true,1537 session: false,1538 up: true1539 },1540 "w2" ->1541 {1542 attached: Set(),1543 built: false,1544 expecting: false,1545 running: false,1546 session: true,1547 up: true1548 }1549 )1550}15511552[State 8]1553{1554 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1555 schedNoRevoke::scheduler::crashes: 2,1556 schedNoRevoke::scheduler::entry: [],1557 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1558 schedNoRevoke::scheduler::mAssigned: Set(),1559 schedNoRevoke::scheduler::mBuild: Set(),1560 schedNoRevoke::scheduler::mDone: Set(),1561 schedNoRevoke::scheduler::mExpect: Set(),1562 schedNoRevoke::scheduler::mResult: Set(),1563 schedNoRevoke::scheduler::mRetry: Set(),1564 schedNoRevoke::scheduler::mRevoke: Set(),1565 schedNoRevoke::scheduler::mSchedule: Set("c1", "c2"),1566 schedNoRevoke::scheduler::published: 0,1567 schedNoRevoke::scheduler::publishedBy: Set(),1568 schedNoRevoke::scheduler::ws:1569 Map(1570 "w1" ->1571 {1572 attached: Set(),1573 built: false,1574 expecting: true,1575 running: true,1576 session: false,1577 up: true1578 },1579 "w2" ->1580 {1581 attached: Set(),1582 built: false,1583 expecting: false,1584 running: false,1585 session: true,1586 up: true1587 }1588 )1589}15901591[State 9]1592{1593 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1594 schedNoRevoke::scheduler::crashes: 2,1595 schedNoRevoke::scheduler::entry:1596 [{ followers: Set("c1"), leased: true, worker: "w2" }],1597 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1598 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1599 schedNoRevoke::scheduler::mBuild: Set(),1600 schedNoRevoke::scheduler::mDone: Set(),1601 schedNoRevoke::scheduler::mExpect: Set("w2"),1602 schedNoRevoke::scheduler::mResult: Set(),1603 schedNoRevoke::scheduler::mRetry: Set(),1604 schedNoRevoke::scheduler::mRevoke: Set(),1605 schedNoRevoke::scheduler::mSchedule: Set("c2"),1606 schedNoRevoke::scheduler::published: 0,1607 schedNoRevoke::scheduler::publishedBy: Set(),1608 schedNoRevoke::scheduler::ws:1609 Map(1610 "w1" ->1611 {1612 attached: Set(),1613 built: false,1614 expecting: true,1615 running: true,1616 session: false,1617 up: true1618 },1619 "w2" ->1620 {1621 attached: Set(),1622 built: false,1623 expecting: false,1624 running: false,1625 session: true,1626 up: true1627 }1628 )1629}16301631[State 10]1632{1633 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1634 schedNoRevoke::scheduler::crashes: 2,1635 schedNoRevoke::scheduler::entry:1636 [{ followers: Set("c1"), leased: true, worker: "w2" }],1637 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1638 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1639 schedNoRevoke::scheduler::mBuild: Set(),1640 schedNoRevoke::scheduler::mDone: Set(),1641 schedNoRevoke::scheduler::mExpect: Set("w2"),1642 schedNoRevoke::scheduler::mResult: Set(),1643 schedNoRevoke::scheduler::mRetry: Set(),1644 schedNoRevoke::scheduler::mRevoke: Set(),1645 schedNoRevoke::scheduler::mSchedule: Set("c2"),1646 schedNoRevoke::scheduler::published: 0,1647 schedNoRevoke::scheduler::publishedBy: Set(),1648 schedNoRevoke::scheduler::ws:1649 Map(1650 "w1" ->1651 {1652 attached: Set(),1653 built: false,1654 expecting: true,1655 running: true,1656 session: true,1657 up: true1658 },1659 "w2" ->1660 {1661 attached: Set(),1662 built: false,1663 expecting: false,1664 running: false,1665 session: true,1666 up: true1667 }1668 )1669}16701671[State 11]1672{1673 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1674 schedNoRevoke::scheduler::crashes: 2,1675 schedNoRevoke::scheduler::entry:1676 [{ followers: Set("c1"), leased: true, worker: "w2" }],1677 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1678 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1679 schedNoRevoke::scheduler::mBuild: Set(),1680 schedNoRevoke::scheduler::mDone: Set(),1681 schedNoRevoke::scheduler::mExpect: Set(),1682 schedNoRevoke::scheduler::mResult: Set(),1683 schedNoRevoke::scheduler::mRetry: Set(),1684 schedNoRevoke::scheduler::mRevoke: Set(),1685 schedNoRevoke::scheduler::mSchedule: Set("c2"),1686 schedNoRevoke::scheduler::published: 0,1687 schedNoRevoke::scheduler::publishedBy: Set(),1688 schedNoRevoke::scheduler::ws:1689 Map(1690 "w1" ->1691 {1692 attached: Set(),1693 built: false,1694 expecting: true,1695 running: true,1696 session: true,1697 up: true1698 },1699 "w2" ->1700 {1701 attached: Set(),1702 built: false,1703 expecting: true,1704 running: true,1705 session: true,1706 up: true1707 }1708 )1709}17101711[violation] Found an issue (585ms at 48954 traces/second).1712Use --verbosity=3 to show executions.1713Use --seed=0xf30f9c0fcd7fb25d --backend=rust to reproduce.1714error: Invariant violated1715An example execution:17161717[State 0]1718{1719 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1720 schedNoFence::scheduler::crashes: 0,1721 schedNoFence::scheduler::entry: [],1722 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1723 schedNoFence::scheduler::mAssigned: Set(),1724 schedNoFence::scheduler::mBuild: Set(),1725 schedNoFence::scheduler::mDone: Set(),1726 schedNoFence::scheduler::mExpect: Set(),1727 schedNoFence::scheduler::mResult: Set(),1728 schedNoFence::scheduler::mRetry: Set(),1729 schedNoFence::scheduler::mRevoke: Set(),1730 schedNoFence::scheduler::mSchedule: Set(),1731 schedNoFence::scheduler::published: 0,1732 schedNoFence::scheduler::publishedBy: Set(),1733 schedNoFence::scheduler::ws:1734 Map(1735 "w1" ->1736 {1737 attached: Set(),1738 built: false,1739 expecting: false,1740 running: false,1741 session: true,1742 up: true1743 },1744 "w2" ->1745 {1746 attached: Set(),1747 built: false,1748 expecting: false,1749 running: false,1750 session: true,1751 up: true1752 }1753 )1754}17551756[State 1]1757{1758 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1759 schedNoFence::scheduler::crashes: 0,1760 schedNoFence::scheduler::entry: [],1761 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1762 schedNoFence::scheduler::mAssigned: Set(),1763 schedNoFence::scheduler::mBuild: Set(),1764 schedNoFence::scheduler::mDone: Set(),1765 schedNoFence::scheduler::mExpect: Set(),1766 schedNoFence::scheduler::mResult: Set(),1767 schedNoFence::scheduler::mRetry: Set(),1768 schedNoFence::scheduler::mRevoke: Set(),1769 schedNoFence::scheduler::mSchedule: Set("c2"),1770 schedNoFence::scheduler::published: 0,1771 schedNoFence::scheduler::publishedBy: Set(),1772 schedNoFence::scheduler::ws:1773 Map(1774 "w1" ->1775 {1776 attached: Set(),1777 built: false,1778 expecting: false,1779 running: false,1780 session: true,1781 up: true1782 },1783 "w2" ->1784 {1785 attached: Set(),1786 built: false,1787 expecting: false,1788 running: false,1789 session: true,1790 up: true1791 }1792 )1793}17941795[State 2]1796{1797 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1798 schedNoFence::scheduler::crashes: 0,1799 schedNoFence::scheduler::entry:1800 [{ followers: Set("c2"), leased: true, worker: "w2" }],1801 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1802 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1803 schedNoFence::scheduler::mBuild: Set(),1804 schedNoFence::scheduler::mDone: Set(),1805 schedNoFence::scheduler::mExpect: Set("w2"),1806 schedNoFence::scheduler::mResult: Set(),1807 schedNoFence::scheduler::mRetry: Set(),1808 schedNoFence::scheduler::mRevoke: Set(),1809 schedNoFence::scheduler::mSchedule: Set(),1810 schedNoFence::scheduler::published: 0,1811 schedNoFence::scheduler::publishedBy: Set(),1812 schedNoFence::scheduler::ws:1813 Map(1814 "w1" ->1815 {1816 attached: Set(),1817 built: false,1818 expecting: false,1819 running: false,1820 session: true,1821 up: true1822 },1823 "w2" ->1824 {1825 attached: Set(),1826 built: false,1827 expecting: false,1828 running: false,1829 session: true,1830 up: true1831 }1832 )1833}18341835[State 3]1836{1837 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1838 schedNoFence::scheduler::crashes: 0,1839 schedNoFence::scheduler::entry:1840 [{ followers: Set("c2"), leased: true, worker: "w2" }],1841 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1842 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1843 schedNoFence::scheduler::mBuild: Set(),1844 schedNoFence::scheduler::mDone: Set(),1845 schedNoFence::scheduler::mExpect: Set(),1846 schedNoFence::scheduler::mResult: Set(),1847 schedNoFence::scheduler::mRetry: Set(),1848 schedNoFence::scheduler::mRevoke: Set(),1849 schedNoFence::scheduler::mSchedule: Set(),1850 schedNoFence::scheduler::published: 0,1851 schedNoFence::scheduler::publishedBy: Set(),1852 schedNoFence::scheduler::ws:1853 Map(1854 "w1" ->1855 {1856 attached: Set(),1857 built: false,1858 expecting: false,1859 running: false,1860 session: true,1861 up: true1862 },1863 "w2" ->1864 {1865 attached: Set(),1866 built: false,1867 expecting: true,1868 running: true,1869 session: true,1870 up: true1871 }1872 )1873}18741875[State 4]1876{1877 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1878 schedNoFence::scheduler::crashes: 1,1879 schedNoFence::scheduler::entry: [],1880 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1881 schedNoFence::scheduler::mAssigned: Set(),1882 schedNoFence::scheduler::mBuild: Set(),1883 schedNoFence::scheduler::mDone: Set(),1884 schedNoFence::scheduler::mExpect: Set(),1885 schedNoFence::scheduler::mResult: Set(),1886 schedNoFence::scheduler::mRetry: Set("c2"),1887 schedNoFence::scheduler::mRevoke: Set(),1888 schedNoFence::scheduler::mSchedule: Set(),1889 schedNoFence::scheduler::published: 0,1890 schedNoFence::scheduler::publishedBy: Set(),1891 schedNoFence::scheduler::ws:1892 Map(1893 "w1" ->1894 {1895 attached: Set(),1896 built: false,1897 expecting: false,1898 running: false,1899 session: false,1900 up: true1901 },1902 "w2" ->1903 {1904 attached: Set(),1905 built: false,1906 expecting: true,1907 running: true,1908 session: false,1909 up: true1910 }1911 )1912}19131914[State 5]1915{1916 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1917 schedNoFence::scheduler::crashes: 2,1918 schedNoFence::scheduler::entry: [],1919 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1920 schedNoFence::scheduler::mAssigned: Set(),1921 schedNoFence::scheduler::mBuild: Set(),1922 schedNoFence::scheduler::mDone: Set(),1923 schedNoFence::scheduler::mExpect: Set(),1924 schedNoFence::scheduler::mResult: Set(),1925 schedNoFence::scheduler::mRetry: Set("c2"),1926 schedNoFence::scheduler::mRevoke: Set(),1927 schedNoFence::scheduler::mSchedule: Set(),1928 schedNoFence::scheduler::published: 0,1929 schedNoFence::scheduler::publishedBy: Set(),1930 schedNoFence::scheduler::ws:1931 Map(1932 "w1" ->1933 {1934 attached: Set(),1935 built: false,1936 expecting: false,1937 running: false,1938 session: false,1939 up: true1940 },1941 "w2" ->1942 {1943 attached: Set(),1944 built: false,1945 expecting: true,1946 running: true,1947 session: false,1948 up: true1949 }1950 )1951}19521953[State 6]1954{1955 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1956 schedNoFence::scheduler::crashes: 2,1957 schedNoFence::scheduler::entry: [],1958 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1959 schedNoFence::scheduler::mAssigned: Set(),1960 schedNoFence::scheduler::mBuild: Set(),1961 schedNoFence::scheduler::mDone: Set(),1962 schedNoFence::scheduler::mExpect: Set(),1963 schedNoFence::scheduler::mResult: Set(),1964 schedNoFence::scheduler::mRetry: Set("c2"),1965 schedNoFence::scheduler::mRevoke: Set(),1966 schedNoFence::scheduler::mSchedule: Set("c1"),1967 schedNoFence::scheduler::published: 0,1968 schedNoFence::scheduler::publishedBy: Set(),1969 schedNoFence::scheduler::ws:1970 Map(1971 "w1" ->1972 {1973 attached: Set(),1974 built: false,1975 expecting: false,1976 running: false,1977 session: false,1978 up: true1979 },1980 "w2" ->1981 {1982 attached: Set(),1983 built: false,1984 expecting: true,1985 running: true,1986 session: false,1987 up: true1988 }1989 )1990}19911992[State 7]1993{1994 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1995 schedNoFence::scheduler::crashes: 2,1996 schedNoFence::scheduler::entry: [],1997 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1998 schedNoFence::scheduler::mAssigned: Set(),1999 schedNoFence::scheduler::mBuild: Set(),2000 schedNoFence::scheduler::mDone: Set(),2001 schedNoFence::scheduler::mExpect: Set(),2002 schedNoFence::scheduler::mResult: Set(),2003 schedNoFence::scheduler::mRetry: Set("c2"),2004 schedNoFence::scheduler::mRevoke: Set(),2005 schedNoFence::scheduler::mSchedule: Set("c1"),2006 schedNoFence::scheduler::published: 0,2007 schedNoFence::scheduler::publishedBy: Set(),2008 schedNoFence::scheduler::ws:2009 Map(2010 "w1" ->2011 {2012 attached: Set(),2013 built: false,2014 expecting: false,2015 running: false,2016 session: true,2017 up: true2018 },2019 "w2" ->2020 {2021 attached: Set(),2022 built: false,2023 expecting: true,2024 running: true,2025 session: false,2026 up: true2027 }2028 )2029}20302031[State 8]2032{2033 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2034 schedNoFence::scheduler::crashes: 2,2035 schedNoFence::scheduler::entry:2036 [{ followers: Set("c1"), leased: true, worker: "w1" }],2037 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2038 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2039 schedNoFence::scheduler::mBuild: Set(),2040 schedNoFence::scheduler::mDone: Set(),2041 schedNoFence::scheduler::mExpect: Set("w1"),2042 schedNoFence::scheduler::mResult: Set(),2043 schedNoFence::scheduler::mRetry: Set("c2"),2044 schedNoFence::scheduler::mRevoke: Set(),2045 schedNoFence::scheduler::mSchedule: Set(),2046 schedNoFence::scheduler::published: 0,2047 schedNoFence::scheduler::publishedBy: Set(),2048 schedNoFence::scheduler::ws:2049 Map(2050 "w1" ->2051 {2052 attached: Set(),2053 built: false,2054 expecting: false,2055 running: false,2056 session: true,2057 up: true2058 },2059 "w2" ->2060 {2061 attached: Set(),2062 built: false,2063 expecting: true,2064 running: true,2065 session: false,2066 up: true2067 }2068 )2069}20702071[State 9]2072{2073 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2074 schedNoFence::scheduler::crashes: 2,2075 schedNoFence::scheduler::entry:2076 [{ followers: Set("c1"), leased: true, worker: "w1" }],2077 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2078 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2079 schedNoFence::scheduler::mBuild: Set(),2080 schedNoFence::scheduler::mDone: Set(),2081 schedNoFence::scheduler::mExpect: Set("w1"),2082 schedNoFence::scheduler::mResult: Set(),2083 schedNoFence::scheduler::mRetry: Set("c2"),2084 schedNoFence::scheduler::mRevoke: Set(),2085 schedNoFence::scheduler::mSchedule: Set(),2086 schedNoFence::scheduler::published: 1,2087 schedNoFence::scheduler::publishedBy: Set("w2"),2088 schedNoFence::scheduler::ws:2089 Map(2090 "w1" ->2091 {2092 attached: Set(),2093 built: false,2094 expecting: false,2095 running: false,2096 session: true,2097 up: true2098 },2099 "w2" ->2100 {2101 attached: Set(),2102 built: true,2103 expecting: false,2104 running: false,2105 session: false,2106 up: true2107 }2108 )2109}21102111[State 10]2112{2113 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2114 schedNoFence::scheduler::crashes: 2,2115 schedNoFence::scheduler::entry:2116 [{ followers: Set("c1"), leased: true, worker: "w1" }],2117 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2118 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2119 schedNoFence::scheduler::mBuild: Set(),2120 schedNoFence::scheduler::mDone: Set(),2121 schedNoFence::scheduler::mExpect: Set(),2122 schedNoFence::scheduler::mResult: Set(),2123 schedNoFence::scheduler::mRetry: Set("c2"),2124 schedNoFence::scheduler::mRevoke: Set(),2125 schedNoFence::scheduler::mSchedule: Set(),2126 schedNoFence::scheduler::published: 1,2127 schedNoFence::scheduler::publishedBy: Set("w2"),2128 schedNoFence::scheduler::ws:2129 Map(2130 "w1" ->2131 {2132 attached: Set(),2133 built: false,2134 expecting: true,2135 running: true,2136 session: true,2137 up: true2138 },2139 "w2" ->2140 {2141 attached: Set(),2142 built: true,2143 expecting: false,2144 running: false,2145 session: false,2146 up: true2147 }2148 )2149}21502151[State 11]2152{2153 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2154 schedNoFence::scheduler::crashes: 2,2155 schedNoFence::scheduler::entry:2156 [{ followers: Set("c1"), leased: true, worker: "w1" }],2157 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2158 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2159 schedNoFence::scheduler::mBuild: Set(),2160 schedNoFence::scheduler::mDone: Set("w1"),2161 schedNoFence::scheduler::mExpect: Set(),2162 schedNoFence::scheduler::mResult: Set(),2163 schedNoFence::scheduler::mRetry: Set("c2"),2164 schedNoFence::scheduler::mRevoke: Set(),2165 schedNoFence::scheduler::mSchedule: Set(),2166 schedNoFence::scheduler::published: 2,2167 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2168 schedNoFence::scheduler::ws:2169 Map(2170 "w1" ->2171 {2172 attached: Set(),2173 built: true,2174 expecting: false,2175 running: false,2176 session: true,2177 up: true2178 },2179 "w2" ->2180 {2181 attached: Set(),2182 built: true,2183 expecting: false,2184 running: false,2185 session: false,2186 up: true2187 }2188 )2189}21902191[violation] Found an issue (430ms at 58270 traces/second).2192Use --verbosity=3 to show executions.2193Use --seed=0xdb8dbc1eaff05e8e --backend=rust to reproduce.2194error: Invariant violated2195An example execution:21962197[State 0]2198{2199 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2200 schedNoPush::scheduler::crashes: 0,2201 schedNoPush::scheduler::entry: [],2202 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2203 schedNoPush::scheduler::mAssigned: Set(),2204 schedNoPush::scheduler::mBuild: Set(),2205 schedNoPush::scheduler::mDone: Set(),2206 schedNoPush::scheduler::mExpect: Set(),2207 schedNoPush::scheduler::mResult: Set(),2208 schedNoPush::scheduler::mRetry: Set(),2209 schedNoPush::scheduler::mRevoke: Set(),2210 schedNoPush::scheduler::mSchedule: Set(),2211 schedNoPush::scheduler::published: 0,2212 schedNoPush::scheduler::publishedBy: Set(),2213 schedNoPush::scheduler::ws:2214 Map(2215 "w1" ->2216 {2217 attached: Set(),2218 built: false,2219 expecting: false,2220 running: false,2221 session: true,2222 up: true2223 },2224 "w2" ->2225 {2226 attached: Set(),2227 built: false,2228 expecting: false,2229 running: false,2230 session: true,2231 up: true2232 }2233 )2234}22352236[State 1]2237{2238 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2239 schedNoPush::scheduler::crashes: 1,2240 schedNoPush::scheduler::entry: [],2241 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2242 schedNoPush::scheduler::mAssigned: Set(),2243 schedNoPush::scheduler::mBuild: Set(),2244 schedNoPush::scheduler::mDone: Set(),2245 schedNoPush::scheduler::mExpect: Set(),2246 schedNoPush::scheduler::mResult: Set(),2247 schedNoPush::scheduler::mRetry: Set(),2248 schedNoPush::scheduler::mRevoke: Set(),2249 schedNoPush::scheduler::mSchedule: Set(),2250 schedNoPush::scheduler::published: 0,2251 schedNoPush::scheduler::publishedBy: Set(),2252 schedNoPush::scheduler::ws:2253 Map(2254 "w1" ->2255 {2256 attached: Set(),2257 built: false,2258 expecting: false,2259 running: false,2260 session: true,2261 up: true2262 },2263 "w2" ->2264 {2265 attached: Set(),2266 built: false,2267 expecting: false,2268 running: false,2269 session: false,2270 up: false2271 }2272 )2273}22742275[State 2]2276{2277 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2278 schedNoPush::scheduler::crashes: 1,2279 schedNoPush::scheduler::entry: [],2280 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2281 schedNoPush::scheduler::mAssigned: Set(),2282 schedNoPush::scheduler::mBuild: Set(),2283 schedNoPush::scheduler::mDone: Set(),2284 schedNoPush::scheduler::mExpect: Set(),2285 schedNoPush::scheduler::mResult: Set(),2286 schedNoPush::scheduler::mRetry: Set(),2287 schedNoPush::scheduler::mRevoke: Set(),2288 schedNoPush::scheduler::mSchedule: Set("c1"),2289 schedNoPush::scheduler::published: 0,2290 schedNoPush::scheduler::publishedBy: Set(),2291 schedNoPush::scheduler::ws:2292 Map(2293 "w1" ->2294 {2295 attached: Set(),2296 built: false,2297 expecting: false,2298 running: false,2299 session: true,2300 up: true2301 },2302 "w2" ->2303 {2304 attached: Set(),2305 built: false,2306 expecting: false,2307 running: false,2308 session: false,2309 up: false2310 }2311 )2312}23132314[State 3]2315{2316 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2317 schedNoPush::scheduler::crashes: 1,2318 schedNoPush::scheduler::entry:2319 [{ followers: Set("c1"), leased: true, worker: "w1" }],2320 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2321 schedNoPush::scheduler::mAssigned: Set(("c1", "w1")),2322 schedNoPush::scheduler::mBuild: Set(),2323 schedNoPush::scheduler::mDone: Set(),2324 schedNoPush::scheduler::mExpect: Set(),2325 schedNoPush::scheduler::mResult: Set(),2326 schedNoPush::scheduler::mRetry: Set(),2327 schedNoPush::scheduler::mRevoke: Set(),2328 schedNoPush::scheduler::mSchedule: Set(),2329 schedNoPush::scheduler::published: 0,2330 schedNoPush::scheduler::publishedBy: Set(),2331 schedNoPush::scheduler::ws:2332 Map(2333 "w1" ->2334 {2335 attached: Set(),2336 built: false,2337 expecting: false,2338 running: false,2339 session: true,2340 up: true2341 },2342 "w2" ->2343 {2344 attached: Set(),2345 built: false,2346 expecting: false,2347 running: false,2348 session: false,2349 up: false2350 }2351 )2352}23532354[State 4]2355{2356 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2357 schedNoPush::scheduler::crashes: 1,2358 schedNoPush::scheduler::entry:2359 [{ followers: Set("c1"), leased: true, worker: "w1" }],2360 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2361 schedNoPush::scheduler::mAssigned: Set(),2362 schedNoPush::scheduler::mBuild: Set(("c1", "w1")),2363 schedNoPush::scheduler::mDone: Set(),2364 schedNoPush::scheduler::mExpect: Set(),2365 schedNoPush::scheduler::mResult: Set(),2366 schedNoPush::scheduler::mRetry: Set(),2367 schedNoPush::scheduler::mRevoke: Set(),2368 schedNoPush::scheduler::mSchedule: Set(),2369 schedNoPush::scheduler::published: 0,2370 schedNoPush::scheduler::publishedBy: Set(),2371 schedNoPush::scheduler::ws:2372 Map(2373 "w1" ->2374 {2375 attached: Set(),2376 built: false,2377 expecting: false,2378 running: false,2379 session: true,2380 up: true2381 },2382 "w2" ->2383 {2384 attached: Set(),2385 built: false,2386 expecting: false,2387 running: false,2388 session: false,2389 up: false2390 }2391 )2392}23932394[State 5]2395{2396 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2397 schedNoPush::scheduler::crashes: 2,2398 schedNoPush::scheduler::entry: [],2399 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2400 schedNoPush::scheduler::mAssigned: Set(),2401 schedNoPush::scheduler::mBuild: Set(("c1", "w1")),2402 schedNoPush::scheduler::mDone: Set(),2403 schedNoPush::scheduler::mExpect: Set(),2404 schedNoPush::scheduler::mResult: Set(),2405 schedNoPush::scheduler::mRetry: Set(),2406 schedNoPush::scheduler::mRevoke: Set(),2407 schedNoPush::scheduler::mSchedule: Set(),2408 schedNoPush::scheduler::published: 0,2409 schedNoPush::scheduler::publishedBy: Set(),2410 schedNoPush::scheduler::ws:2411 Map(2412 "w1" ->2413 {2414 attached: Set(),2415 built: false,2416 expecting: false,2417 running: false,2418 session: false,2419 up: true2420 },2421 "w2" ->2422 {2423 attached: Set(),2424 built: false,2425 expecting: false,2426 running: false,2427 session: false,2428 up: false2429 }2430 )2431}24322433[State 6]2434{2435 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2436 schedNoPush::scheduler::crashes: 2,2437 schedNoPush::scheduler::entry: [],2438 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2439 schedNoPush::scheduler::mAssigned: Set(),2440 schedNoPush::scheduler::mBuild: Set(("c1", "w1")),2441 schedNoPush::scheduler::mDone: Set(),2442 schedNoPush::scheduler::mExpect: Set(),2443 schedNoPush::scheduler::mResult: Set(),2444 schedNoPush::scheduler::mRetry: Set(),2445 schedNoPush::scheduler::mRevoke: Set(),2446 schedNoPush::scheduler::mSchedule: Set(),2447 schedNoPush::scheduler::published: 0,2448 schedNoPush::scheduler::publishedBy: Set(),2449 schedNoPush::scheduler::ws:2450 Map(2451 "w1" ->2452 {2453 attached: Set(),2454 built: false,2455 expecting: false,2456 running: false,2457 session: true,2458 up: true2459 },2460 "w2" ->2461 {2462 attached: Set(),2463 built: false,2464 expecting: false,2465 running: false,2466 session: false,2467 up: false2468 }2469 )2470}24712472[State 7]2473{2474 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2475 schedNoPush::scheduler::crashes: 2,2476 schedNoPush::scheduler::entry: [],2477 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2478 schedNoPush::scheduler::mAssigned: Set(),2479 schedNoPush::scheduler::mBuild: Set(),2480 schedNoPush::scheduler::mDone: Set(),2481 schedNoPush::scheduler::mExpect: Set(),2482 schedNoPush::scheduler::mResult: Set(),2483 schedNoPush::scheduler::mRetry: Set(),2484 schedNoPush::scheduler::mRevoke: Set(),2485 schedNoPush::scheduler::mSchedule: Set(),2486 schedNoPush::scheduler::published: 0,2487 schedNoPush::scheduler::publishedBy: Set(),2488 schedNoPush::scheduler::ws:2489 Map(2490 "w1" ->2491 {2492 attached: Set("c1"),2493 built: false,2494 expecting: true,2495 running: true,2496 session: true,2497 up: true2498 },2499 "w2" ->2500 {2501 attached: Set(),2502 built: false,2503 expecting: false,2504 running: false,2505 session: false,2506 up: false2507 }2508 )2509}25102511[violation] Found an issue (404ms at 30337 traces/second).2512Use --verbosity=3 to show executions.2513Use --seed=0x4e0d862b4ebb0b75 --backend=rust to reproduce.2514error: Invariant violated2515An example execution:25162517[State 0]2518{2519 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2520 schedNoReport::scheduler::crashes: 0,2521 schedNoReport::scheduler::entry: [],2522 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2523 schedNoReport::scheduler::mAssigned: Set(),2524 schedNoReport::scheduler::mBuild: Set(),2525 schedNoReport::scheduler::mDone: Set(),2526 schedNoReport::scheduler::mExpect: Set(),2527 schedNoReport::scheduler::mResult: Set(),2528 schedNoReport::scheduler::mRetry: Set(),2529 schedNoReport::scheduler::mRevoke: Set(),2530 schedNoReport::scheduler::mSchedule: Set(),2531 schedNoReport::scheduler::published: 0,2532 schedNoReport::scheduler::publishedBy: Set(),2533 schedNoReport::scheduler::ws:2534 Map(2535 "w1" ->2536 {2537 attached: Set(),2538 built: false,2539 expecting: false,2540 running: false,2541 session: true,2542 up: true2543 },2544 "w2" ->2545 {2546 attached: Set(),2547 built: false,2548 expecting: false,2549 running: false,2550 session: true,2551 up: true2552 }2553 )2554}25552556[State 1]2557{2558 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2559 schedNoReport::scheduler::crashes: 0,2560 schedNoReport::scheduler::entry: [],2561 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2562 schedNoReport::scheduler::mAssigned: Set(),2563 schedNoReport::scheduler::mBuild: Set(),2564 schedNoReport::scheduler::mDone: Set(),2565 schedNoReport::scheduler::mExpect: Set(),2566 schedNoReport::scheduler::mResult: Set(),2567 schedNoReport::scheduler::mRetry: Set(),2568 schedNoReport::scheduler::mRevoke: Set(),2569 schedNoReport::scheduler::mSchedule: Set("c2"),2570 schedNoReport::scheduler::published: 0,2571 schedNoReport::scheduler::publishedBy: Set(),2572 schedNoReport::scheduler::ws:2573 Map(2574 "w1" ->2575 {2576 attached: Set(),2577 built: false,2578 expecting: false,2579 running: false,2580 session: true,2581 up: true2582 },2583 "w2" ->2584 {2585 attached: Set(),2586 built: false,2587 expecting: false,2588 running: false,2589 session: true,2590 up: true2591 }2592 )2593}25942595[State 2]2596{2597 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2598 schedNoReport::scheduler::crashes: 0,2599 schedNoReport::scheduler::entry:2600 [{ followers: Set("c2"), leased: true, worker: "w2" }],2601 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2602 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2603 schedNoReport::scheduler::mBuild: Set(),2604 schedNoReport::scheduler::mDone: Set(),2605 schedNoReport::scheduler::mExpect: Set("w2"),2606 schedNoReport::scheduler::mResult: Set(),2607 schedNoReport::scheduler::mRetry: Set(),2608 schedNoReport::scheduler::mRevoke: Set(),2609 schedNoReport::scheduler::mSchedule: Set(),2610 schedNoReport::scheduler::published: 0,2611 schedNoReport::scheduler::publishedBy: Set(),2612 schedNoReport::scheduler::ws:2613 Map(2614 "w1" ->2615 {2616 attached: Set(),2617 built: false,2618 expecting: false,2619 running: false,2620 session: true,2621 up: true2622 },2623 "w2" ->2624 {2625 attached: Set(),2626 built: false,2627 expecting: false,2628 running: false,2629 session: true,2630 up: true2631 }2632 )2633}26342635[State 3]2636{2637 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2638 schedNoReport::scheduler::crashes: 0,2639 schedNoReport::scheduler::entry:2640 [{ followers: Set("c2"), leased: true, worker: "w2" }],2641 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2642 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2643 schedNoReport::scheduler::mBuild: Set(),2644 schedNoReport::scheduler::mDone: Set(),2645 schedNoReport::scheduler::mExpect: Set(),2646 schedNoReport::scheduler::mResult: Set(),2647 schedNoReport::scheduler::mRetry: Set(),2648 schedNoReport::scheduler::mRevoke: Set(),2649 schedNoReport::scheduler::mSchedule: Set(),2650 schedNoReport::scheduler::published: 0,2651 schedNoReport::scheduler::publishedBy: Set(),2652 schedNoReport::scheduler::ws:2653 Map(2654 "w1" ->2655 {2656 attached: Set(),2657 built: false,2658 expecting: false,2659 running: false,2660 session: true,2661 up: true2662 },2663 "w2" ->2664 {2665 attached: Set(),2666 built: false,2667 expecting: true,2668 running: true,2669 session: true,2670 up: true2671 }2672 )2673}26742675[State 4]2676{2677 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2678 schedNoReport::scheduler::crashes: 1,2679 schedNoReport::scheduler::entry: [],2680 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2681 schedNoReport::scheduler::mAssigned: Set(),2682 schedNoReport::scheduler::mBuild: Set(),2683 schedNoReport::scheduler::mDone: Set(),2684 schedNoReport::scheduler::mExpect: Set(),2685 schedNoReport::scheduler::mResult: Set(),2686 schedNoReport::scheduler::mRetry: Set("c2"),2687 schedNoReport::scheduler::mRevoke: Set(),2688 schedNoReport::scheduler::mSchedule: Set(),2689 schedNoReport::scheduler::published: 0,2690 schedNoReport::scheduler::publishedBy: Set(),2691 schedNoReport::scheduler::ws:2692 Map(2693 "w1" ->2694 {2695 attached: Set(),2696 built: false,2697 expecting: false,2698 running: false,2699 session: false,2700 up: true2701 },2702 "w2" ->2703 {2704 attached: Set(),2705 built: false,2706 expecting: true,2707 running: true,2708 session: false,2709 up: true2710 }2711 )2712}27132714[State 5]2715{2716 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2717 schedNoReport::scheduler::crashes: 2,2718 schedNoReport::scheduler::entry: [],2719 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2720 schedNoReport::scheduler::mAssigned: Set(),2721 schedNoReport::scheduler::mBuild: Set(),2722 schedNoReport::scheduler::mDone: Set(),2723 schedNoReport::scheduler::mExpect: Set(),2724 schedNoReport::scheduler::mResult: Set(),2725 schedNoReport::scheduler::mRetry: Set("c2"),2726 schedNoReport::scheduler::mRevoke: Set(),2727 schedNoReport::scheduler::mSchedule: Set(),2728 schedNoReport::scheduler::published: 0,2729 schedNoReport::scheduler::publishedBy: Set(),2730 schedNoReport::scheduler::ws:2731 Map(2732 "w1" ->2733 {2734 attached: Set(),2735 built: false,2736 expecting: false,2737 running: false,2738 session: false,2739 up: true2740 },2741 "w2" ->2742 {2743 attached: Set(),2744 built: false,2745 expecting: true,2746 running: true,2747 session: false,2748 up: true2749 }2750 )2751}27522753[State 6]2754{2755 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2756 schedNoReport::scheduler::crashes: 2,2757 schedNoReport::scheduler::entry: [],2758 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2759 schedNoReport::scheduler::mAssigned: Set(),2760 schedNoReport::scheduler::mBuild: Set(),2761 schedNoReport::scheduler::mDone: Set(),2762 schedNoReport::scheduler::mExpect: Set(),2763 schedNoReport::scheduler::mResult: Set(),2764 schedNoReport::scheduler::mRetry: Set("c2"),2765 schedNoReport::scheduler::mRevoke: Set(),2766 schedNoReport::scheduler::mSchedule: Set("c1"),2767 schedNoReport::scheduler::published: 0,2768 schedNoReport::scheduler::publishedBy: Set(),2769 schedNoReport::scheduler::ws:2770 Map(2771 "w1" ->2772 {2773 attached: Set(),2774 built: false,2775 expecting: false,2776 running: false,2777 session: false,2778 up: true2779 },2780 "w2" ->2781 {2782 attached: Set(),2783 built: false,2784 expecting: true,2785 running: true,2786 session: false,2787 up: true2788 }2789 )2790}27912792[State 7]2793{2794 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2795 schedNoReport::scheduler::crashes: 2,2796 schedNoReport::scheduler::entry: [],2797 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2798 schedNoReport::scheduler::mAssigned: Set(),2799 schedNoReport::scheduler::mBuild: Set(),2800 schedNoReport::scheduler::mDone: Set(),2801 schedNoReport::scheduler::mExpect: Set(),2802 schedNoReport::scheduler::mResult: Set(),2803 schedNoReport::scheduler::mRetry: Set("c2"),2804 schedNoReport::scheduler::mRevoke: Set(),2805 schedNoReport::scheduler::mSchedule: Set("c1"),2806 schedNoReport::scheduler::published: 0,2807 schedNoReport::scheduler::publishedBy: Set(),2808 schedNoReport::scheduler::ws:2809 Map(2810 "w1" ->2811 {2812 attached: Set(),2813 built: false,2814 expecting: false,2815 running: false,2816 session: true,2817 up: true2818 },2819 "w2" ->2820 {2821 attached: Set(),2822 built: false,2823 expecting: true,2824 running: true,2825 session: false,2826 up: true2827 }2828 )2829}28302831[State 8]2832{2833 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2834 schedNoReport::scheduler::crashes: 2,2835 schedNoReport::scheduler::entry: [],2836 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2837 schedNoReport::scheduler::mAssigned: Set(),2838 schedNoReport::scheduler::mBuild: Set(),2839 schedNoReport::scheduler::mDone: Set(),2840 schedNoReport::scheduler::mExpect: Set(),2841 schedNoReport::scheduler::mResult: Set(),2842 schedNoReport::scheduler::mRetry: Set(),2843 schedNoReport::scheduler::mRevoke: Set(),2844 schedNoReport::scheduler::mSchedule: Set("c1", "c2"),2845 schedNoReport::scheduler::published: 0,2846 schedNoReport::scheduler::publishedBy: Set(),2847 schedNoReport::scheduler::ws:2848 Map(2849 "w1" ->2850 {2851 attached: Set(),2852 built: false,2853 expecting: false,2854 running: false,2855 session: true,2856 up: true2857 },2858 "w2" ->2859 {2860 attached: Set(),2861 built: false,2862 expecting: true,2863 running: true,2864 session: false,2865 up: true2866 }2867 )2868}28692870[State 9]2871{2872 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2873 schedNoReport::scheduler::crashes: 2,2874 schedNoReport::scheduler::entry: [],2875 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2876 schedNoReport::scheduler::mAssigned: Set(),2877 schedNoReport::scheduler::mBuild: Set(),2878 schedNoReport::scheduler::mDone: Set(),2879 schedNoReport::scheduler::mExpect: Set(),2880 schedNoReport::scheduler::mResult: Set(),2881 schedNoReport::scheduler::mRetry: Set(),2882 schedNoReport::scheduler::mRevoke: Set(),2883 schedNoReport::scheduler::mSchedule: Set("c1", "c2"),2884 schedNoReport::scheduler::published: 0,2885 schedNoReport::scheduler::publishedBy: Set(),2886 schedNoReport::scheduler::ws:2887 Map(2888 "w1" ->2889 {2890 attached: Set(),2891 built: false,2892 expecting: false,2893 running: false,2894 session: true,2895 up: true2896 },2897 "w2" ->2898 {2899 attached: Set(),2900 built: false,2901 expecting: true,2902 running: true,2903 session: true,2904 up: true2905 }2906 )2907}29082909[State 10]2910{2911 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2912 schedNoReport::scheduler::crashes: 2,2913 schedNoReport::scheduler::entry:2914 [{ followers: Set("c1"), leased: true, worker: "w1" }],2915 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2916 schedNoReport::scheduler::mAssigned: Set(("c1", "w1")),2917 schedNoReport::scheduler::mBuild: Set(),2918 schedNoReport::scheduler::mDone: Set(),2919 schedNoReport::scheduler::mExpect: Set("w1"),2920 schedNoReport::scheduler::mResult: Set(),2921 schedNoReport::scheduler::mRetry: Set(),2922 schedNoReport::scheduler::mRevoke: Set(),2923 schedNoReport::scheduler::mSchedule: Set("c2"),2924 schedNoReport::scheduler::published: 0,2925 schedNoReport::scheduler::publishedBy: Set(),2926 schedNoReport::scheduler::ws:2927 Map(2928 "w1" ->2929 {2930 attached: Set(),2931 built: false,2932 expecting: false,2933 running: false,2934 session: true,2935 up: true2936 },2937 "w2" ->2938 {2939 attached: Set(),2940 built: false,2941 expecting: true,2942 running: true,2943 session: true,2944 up: true2945 }2946 )2947}29482949[State 11]2950{2951 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2952 schedNoReport::scheduler::crashes: 2,2953 schedNoReport::scheduler::entry:2954 [{ followers: Set("c1"), leased: true, worker: "w1" }],2955 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2956 schedNoReport::scheduler::mAssigned: Set(("c1", "w1")),2957 schedNoReport::scheduler::mBuild: Set(),2958 schedNoReport::scheduler::mDone: Set(),2959 schedNoReport::scheduler::mExpect: Set(),2960 schedNoReport::scheduler::mResult: Set(),2961 schedNoReport::scheduler::mRetry: Set(),2962 schedNoReport::scheduler::mRevoke: Set(),2963 schedNoReport::scheduler::mSchedule: Set("c2"),2964 schedNoReport::scheduler::published: 0,2965 schedNoReport::scheduler::publishedBy: Set(),2966 schedNoReport::scheduler::ws:2967 Map(2968 "w1" ->2969 {2970 attached: Set(),2971 built: false,2972 expecting: true,2973 running: true,2974 session: true,2975 up: true2976 },2977 "w2" ->2978 {2979 attached: Set(),2980 built: false,2981 expecting: true,2982 running: true,2983 session: true,2984 up: true2985 }2986 )2987}29882989[violation] Found an issue (416ms at 57683 traces/second).2990Use --verbosity=3 to show executions.2991Use --seed=0xb8c8aa4d3b18353f --backend=rust to reproduce.2992error: Invariant violated2993An example execution:29942995[State 0]2996{2997 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2998 schedTerminal::scheduler::crashes: 0,2999 schedTerminal::scheduler::entry: [],3000 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3001 schedTerminal::scheduler::mAssigned: Set(),3002 schedTerminal::scheduler::mBuild: Set(),3003 schedTerminal::scheduler::mDone: Set(),3004 schedTerminal::scheduler::mExpect: Set(),3005 schedTerminal::scheduler::mResult: Set(),3006 schedTerminal::scheduler::mRetry: Set(),3007 schedTerminal::scheduler::mRevoke: Set(),3008 schedTerminal::scheduler::mSchedule: Set(),3009 schedTerminal::scheduler::published: 0,3010 schedTerminal::scheduler::publishedBy: Set(),3011 schedTerminal::scheduler::ws:3012 Map(3013 "w1" ->3014 {3015 attached: Set(),3016 built: false,3017 expecting: false,3018 running: false,3019 session: true,3020 up: true3021 },3022 "w2" ->3023 {3024 attached: Set(),3025 built: false,3026 expecting: false,3027 running: false,3028 session: true,3029 up: true3030 }3031 )3032}30333034[State 1]3035{3036 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3037 schedTerminal::scheduler::crashes: 1,3038 schedTerminal::scheduler::entry: [],3039 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3040 schedTerminal::scheduler::mAssigned: Set(),3041 schedTerminal::scheduler::mBuild: Set(),3042 schedTerminal::scheduler::mDone: Set(),3043 schedTerminal::scheduler::mExpect: Set(),3044 schedTerminal::scheduler::mResult: Set(),3045 schedTerminal::scheduler::mRetry: Set(),3046 schedTerminal::scheduler::mRevoke: Set(),3047 schedTerminal::scheduler::mSchedule: Set(),3048 schedTerminal::scheduler::published: 0,3049 schedTerminal::scheduler::publishedBy: Set(),3050 schedTerminal::scheduler::ws:3051 Map(3052 "w1" ->3053 {3054 attached: Set(),3055 built: false,3056 expecting: false,3057 running: false,3058 session: false,3059 up: true3060 },3061 "w2" ->3062 {3063 attached: Set(),3064 built: false,3065 expecting: false,3066 running: false,3067 session: false,3068 up: true3069 }3070 )3071}30723073[State 2]3074{3075 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3076 schedTerminal::scheduler::crashes: 1,3077 schedTerminal::scheduler::entry: [],3078 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3079 schedTerminal::scheduler::mAssigned: Set(),3080 schedTerminal::scheduler::mBuild: Set(),3081 schedTerminal::scheduler::mDone: Set(),3082 schedTerminal::scheduler::mExpect: Set(),3083 schedTerminal::scheduler::mResult: Set(),3084 schedTerminal::scheduler::mRetry: Set(),3085 schedTerminal::scheduler::mRevoke: Set(),3086 schedTerminal::scheduler::mSchedule: Set("c2"),3087 schedTerminal::scheduler::published: 0,3088 schedTerminal::scheduler::publishedBy: Set(),3089 schedTerminal::scheduler::ws:3090 Map(3091 "w1" ->3092 {3093 attached: Set(),3094 built: false,3095 expecting: false,3096 running: false,3097 session: false,3098 up: true3099 },3100 "w2" ->3101 {3102 attached: Set(),3103 built: false,3104 expecting: false,3105 running: false,3106 session: false,3107 up: true3108 }3109 )3110}31113112[State 3]3113{3114 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3115 schedTerminal::scheduler::crashes: 1,3116 schedTerminal::scheduler::entry: [],3117 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3118 schedTerminal::scheduler::mAssigned: Set(),3119 schedTerminal::scheduler::mBuild: Set(),3120 schedTerminal::scheduler::mDone: Set(),3121 schedTerminal::scheduler::mExpect: Set(),3122 schedTerminal::scheduler::mResult: Set(),3123 schedTerminal::scheduler::mRetry: Set(),3124 schedTerminal::scheduler::mRevoke: Set(),3125 schedTerminal::scheduler::mSchedule: Set(),3126 schedTerminal::scheduler::published: 0,3127 schedTerminal::scheduler::publishedBy: Set(),3128 schedTerminal::scheduler::ws:3129 Map(3130 "w1" ->3131 {3132 attached: Set(),3133 built: false,3134 expecting: false,3135 running: false,3136 session: false,3137 up: true3138 },3139 "w2" ->3140 {3141 attached: Set(),3142 built: false,3143 expecting: false,3144 running: false,3145 session: false,3146 up: true3147 }3148 )3149}31503151[violation] Found an issue (166ms at 5982 traces/second).3152Use --verbosity=3 to show executions.3153Use --seed=0xfc4ad7849587f9c0 --backend=rust to reproduce.3154error: Invariant violated3155An example execution:31563157[State 0]3158{3159 pushFixed::push::byPath: Map(),3160 pushFixed::push::inflight: Set(),3161 pushFixed::push::left: Map(),3162 pushFixed::push::sent: Map()3163}31643165[State 1]3166{3167 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3168 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3169 pushFixed::push::left: Map(2 -> 2),3170 pushFixed::push::sent: Map(2 -> Set("a", "b"))3171}31723173[State 2]3174{3175 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3176 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),3177 pushFixed::push::left: Map(1 -> 2, 2 -> 2),3178 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3179}31803181[State 3]3182{3183 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3184 pushFixed::push::inflight:3185 Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),3186 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 2),3187 pushFixed::push::sent:3188 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3189}31903191[State 4]3192{3193 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3194 pushFixed::push::inflight:3195 Set((1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),3196 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 2),3197 pushFixed::push::sent:3198 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3199}32003201[State 5]3202{3203 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3204 pushFixed::push::inflight: Set((1, "b"), (2, "a"), (3, "a"), (3, "b")),3205 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 2),3206 pushFixed::push::sent:3207 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3208}32093210[State 6]3211{3212 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3213 pushFixed::push::inflight: Set((1, "b"), (2, "a"), (3, "a")),3214 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 1),3215 pushFixed::push::sent:3216 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3217}32183219[State 7]3220{3221 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3222 pushFixed::push::inflight: Set((1, "b"), (2, "a")),3223 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 0),3224 pushFixed::push::sent:3225 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3226}32273228[State 8]3229{3230 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3231 pushFixed::push::inflight: Set((1, "b")),3232 pushFixed::push::left: Map(1 -> 1, 2 -> 0, 3 -> 0),3233 pushFixed::push::sent:3234 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3235}32363237[State 9]3238{3239 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3240 pushFixed::push::inflight: Set(),3241 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3242 pushFixed::push::sent:3243 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3244}32453246[ok] No violation found (78ms at 256410 traces/second).3247Trace length statistics: max=10, min=7, average=7.993248You may increase --max-samples and --max-steps.3249Use --verbosity to produce more (or less) output.3250Use --seed=0x1f8d90672a9109b4 --backend=rust to reproduce.