nix-grpc-store-spec
checks.aarch64-linux.spec
· build #607
· 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" -> CIdle, "c2" -> CIdle),46 schedFixed::scheduler::crashes: 1,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(),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: false,77 up: false78 }79 )80}8182[State 2]83{84 schedFixed::scheduler::cl: Map("c1" -> CIdle, "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(),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: true,116 up: true117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CIdle, "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(),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: true156 }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(),172 schedFixed::scheduler::mRevoke: Set(),173 schedFixed::scheduler::mSchedule: Set("c1"),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: false,194 up: true195 }196 )197}198199[State 5]200{201 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),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(),211 schedFixed::scheduler::mRevoke: Set(),212 schedFixed::scheduler::mSchedule: Set("c1"),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: true,224 up: true225 },226 "w2" ->227 {228 attached: Set(),229 built: false,230 expecting: false,231 running: false,232 session: false,233 up: true234 }235 )236}237238[State 6]239{240 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),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"),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: true,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" -> CIdle),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(),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: true,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" -> CSent("w2"), "c2" -> CIdle),320 schedFixed::scheduler::crashes: 2,321 schedFixed::scheduler::entry:322 [{ followers: Set("c1"), leased: true, worker: "w2" }],323 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),324 schedFixed::scheduler::mAssigned: Set(),325 schedFixed::scheduler::mBuild: Set(("c1", "w2")),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: true,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" -> CSent("w2"), "c2" -> CIdle),360 schedFixed::scheduler::crashes: 2,361 schedFixed::scheduler::entry:362 [{ followers: Set("c1"), leased: true, worker: "w2" }],363 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),364 schedFixed::scheduler::mAssigned: Set(),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("c1"),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" -> CSent("w2"), "c2" -> CQueued),400 schedFixed::scheduler::crashes: 2,401 schedFixed::scheduler::entry:402 [{ followers: Set("c1"), leased: true, worker: "w2" }],403 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),404 schedFixed::scheduler::mAssigned: Set(),405 schedFixed::scheduler::mBuild: Set(),406 schedFixed::scheduler::mDone: Set(),407 schedFixed::scheduler::mExpect: Set("w2"),408 schedFixed::scheduler::mResult: Set(),409 schedFixed::scheduler::mRetry: Set("c1"),410 schedFixed::scheduler::mRevoke: Set(),411 schedFixed::scheduler::mSchedule: Set("c2"),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" -> CSent("w2"), "c2" -> CQueued),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(("c2", "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("c1"),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(("c2", "w2")),486 schedFixed::scheduler::mDone: Set(),487 schedFixed::scheduler::mExpect: Set("w2"),488 schedFixed::scheduler::mResult: Set(),489 schedFixed::scheduler::mRetry: Set("c1"),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" -> CSent("w2"), "c2" -> CQueued),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("c1"),570 schedFixed::scheduler::mRevoke: Set(),571 schedFixed::scheduler::mSchedule: Set("c2"),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" -> CQueued),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(),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(),610 schedFixed::scheduler::mRevoke: Set(),611 schedFixed::scheduler::mSchedule: Set("c1", "c2"),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" -> CQueued, "c2" -> CQueued),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(("c2", "w2")),645 schedFixed::scheduler::mBuild: Set(),646 schedFixed::scheduler::mDone: Set(),647 schedFixed::scheduler::mExpect: Set("w2"),648 schedFixed::scheduler::mResult: Set(),649 schedFixed::scheduler::mRetry: Set(),650 schedFixed::scheduler::mRevoke: Set(),651 schedFixed::scheduler::mSchedule: Set("c1"),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" -> CQueued, "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(("c1", "w2"), ("c2", "w2")),685 schedFixed::scheduler::mBuild: Set(),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(),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" -> CQueued, "c2" -> CSent("w2")),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(("c1", "w2")),725 schedFixed::scheduler::mBuild: Set(("c2", "w2")),726 schedFixed::scheduler::mDone: Set(),727 schedFixed::scheduler::mExpect: Set("w2"),728 schedFixed::scheduler::mResult: Set(),729 schedFixed::scheduler::mRetry: Set(),730 schedFixed::scheduler::mRevoke: Set(),731 schedFixed::scheduler::mSchedule: Set(),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" -> CSent("w2"), "c2" -> CSent("w2")),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(("c1", "w2"), ("c2", "w2")),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(),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" -> CSent("w2"), "c2" -> CSent("w2")),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(),805 schedFixed::scheduler::mBuild: Set(("c1", "w2")),806 schedFixed::scheduler::mDone: Set(),807 schedFixed::scheduler::mExpect: Set("w2"),808 schedFixed::scheduler::mResult: Set(),809 schedFixed::scheduler::mRetry: Set("c2"),810 schedFixed::scheduler::mRevoke: Set(),811 schedFixed::scheduler::mSchedule: Set(),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" -> CSent("w2"), "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(),845 schedFixed::scheduler::mBuild: Set(("c1", "w2")),846 schedFixed::scheduler::mDone: Set(),847 schedFixed::scheduler::mExpect: Set("w2"),848 schedFixed::scheduler::mResult: Set(),849 schedFixed::scheduler::mRetry: Set(),850 schedFixed::scheduler::mRevoke: Set(),851 schedFixed::scheduler::mSchedule: Set("c2"),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: false,870 running: false,871 session: true,872 up: true873 }874 )875}876877[State 22]878{879 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "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(("c2", "w2")),885 schedFixed::scheduler::mBuild: Set(("c1", "w2")),886 schedFixed::scheduler::mDone: Set(),887 schedFixed::scheduler::mExpect: Set("w2"),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: false,910 running: false,911 session: true,912 up: true913 }914 )915}916917[State 23]918{919 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "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(("c2", "w2")),925 schedFixed::scheduler::mBuild: Set(("c1", "w2")),926 schedFixed::scheduler::mDone: Set(),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: 0,933 schedFixed::scheduler::publishedBy: Set(),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: false,949 expecting: true,950 running: true,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 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1003 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1004 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1005 schedFixed::scheduler::mBuild: Set(),1006 schedFixed::scheduler::mDone: Set("w2"),1007 schedFixed::scheduler::mExpect: Set(),1008 schedFixed::scheduler::mResult: Set("c1"),1009 schedFixed::scheduler::mRetry: Set(),1010 schedFixed::scheduler::mRevoke: Set(),1011 schedFixed::scheduler::mSchedule: Set(),1012 schedFixed::scheduler::published: 1,1013 schedFixed::scheduler::publishedBy: Set("w2"),1014 schedFixed::scheduler::ws:1015 Map(1016 "w1" ->1017 {1018 attached: Set(),1019 built: false,1020 expecting: false,1021 running: false,1022 session: true,1023 up: true1024 },1025 "w2" ->1026 {1027 attached: Set(),1028 built: true,1029 expecting: false,1030 running: false,1031 session: true,1032 up: true1033 }1034 )1035}10361037[State 26]1038{1039 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),1040 schedFixed::scheduler::crashes: 2,1041 schedFixed::scheduler::entry: [],1042 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1043 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1044 schedFixed::scheduler::mBuild: Set(),1045 schedFixed::scheduler::mDone: Set(),1046 schedFixed::scheduler::mExpect: Set(),1047 schedFixed::scheduler::mResult: Set("c1"),1048 schedFixed::scheduler::mRetry: Set(),1049 schedFixed::scheduler::mRevoke: Set(),1050 schedFixed::scheduler::mSchedule: Set(),1051 schedFixed::scheduler::published: 1,1052 schedFixed::scheduler::publishedBy: Set("w2"),1053 schedFixed::scheduler::ws:1054 Map(1055 "w1" ->1056 {1057 attached: Set(),1058 built: false,1059 expecting: false,1060 running: false,1061 session: true,1062 up: true1063 },1064 "w2" ->1065 {1066 attached: Set(),1067 built: true,1068 expecting: false,1069 running: false,1070 session: true,1071 up: true1072 }1073 )1074}10751076[State 27]1077{1078 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CQueued),1079 schedFixed::scheduler::crashes: 2,1080 schedFixed::scheduler::entry: [],1081 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1082 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1083 schedFixed::scheduler::mBuild: Set(),1084 schedFixed::scheduler::mDone: Set(),1085 schedFixed::scheduler::mExpect: Set(),1086 schedFixed::scheduler::mResult: Set(),1087 schedFixed::scheduler::mRetry: Set(),1088 schedFixed::scheduler::mRevoke: Set(),1089 schedFixed::scheduler::mSchedule: Set(),1090 schedFixed::scheduler::published: 1,1091 schedFixed::scheduler::publishedBy: Set("w2"),1092 schedFixed::scheduler::ws:1093 Map(1094 "w1" ->1095 {1096 attached: Set(),1097 built: false,1098 expecting: false,1099 running: false,1100 session: true,1101 up: true1102 },1103 "w2" ->1104 {1105 attached: Set(),1106 built: true,1107 expecting: false,1108 running: false,1109 session: true,1110 up: true1111 }1112 )1113}11141115[State 28]1116{1117 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w2")),1118 schedFixed::scheduler::crashes: 2,1119 schedFixed::scheduler::entry: [],1120 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1121 schedFixed::scheduler::mAssigned: Set(),1122 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1123 schedFixed::scheduler::mDone: Set(),1124 schedFixed::scheduler::mExpect: Set(),1125 schedFixed::scheduler::mResult: Set(),1126 schedFixed::scheduler::mRetry: Set(),1127 schedFixed::scheduler::mRevoke: Set(),1128 schedFixed::scheduler::mSchedule: Set(),1129 schedFixed::scheduler::published: 1,1130 schedFixed::scheduler::publishedBy: Set("w2"),1131 schedFixed::scheduler::ws:1132 Map(1133 "w1" ->1134 {1135 attached: Set(),1136 built: false,1137 expecting: false,1138 running: false,1139 session: true,1140 up: true1141 },1142 "w2" ->1143 {1144 attached: Set(),1145 built: true,1146 expecting: false,1147 running: false,1148 session: true,1149 up: true1150 }1151 )1152}11531154[State 29]1155{1156 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w2")),1157 schedFixed::scheduler::crashes: 2,1158 schedFixed::scheduler::entry: [],1159 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1160 schedFixed::scheduler::mAssigned: Set(),1161 schedFixed::scheduler::mBuild: Set(),1162 schedFixed::scheduler::mDone: Set(),1163 schedFixed::scheduler::mExpect: Set(),1164 schedFixed::scheduler::mResult: Set("c2"),1165 schedFixed::scheduler::mRetry: Set(),1166 schedFixed::scheduler::mRevoke: Set(),1167 schedFixed::scheduler::mSchedule: Set(),1168 schedFixed::scheduler::published: 1,1169 schedFixed::scheduler::publishedBy: Set("w2"),1170 schedFixed::scheduler::ws:1171 Map(1172 "w1" ->1173 {1174 attached: Set(),1175 built: false,1176 expecting: false,1177 running: false,1178 session: true,1179 up: true1180 },1181 "w2" ->1182 {1183 attached: Set(),1184 built: true,1185 expecting: false,1186 running: false,1187 session: true,1188 up: true1189 }1190 )1191}11921193[State 30]1194{1195 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),1196 schedFixed::scheduler::crashes: 2,1197 schedFixed::scheduler::entry: [],1198 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1199 schedFixed::scheduler::mAssigned: Set(),1200 schedFixed::scheduler::mBuild: Set(),1201 schedFixed::scheduler::mDone: Set(),1202 schedFixed::scheduler::mExpect: Set(),1203 schedFixed::scheduler::mResult: Set(),1204 schedFixed::scheduler::mRetry: Set(),1205 schedFixed::scheduler::mRevoke: Set(),1206 schedFixed::scheduler::mSchedule: Set(),1207 schedFixed::scheduler::published: 1,1208 schedFixed::scheduler::publishedBy: Set("w2"),1209 schedFixed::scheduler::ws:1210 Map(1211 "w1" ->1212 {1213 attached: Set(),1214 built: false,1215 expecting: false,1216 running: false,1217 session: true,1218 up: true1219 },1220 "w2" ->1221 {1222 attached: Set(),1223 built: true,1224 expecting: false,1225 running: false,1226 session: true,1227 up: true1228 }1229 )1230}12311232[ok] No violation found (579ms at 51813 traces/second).1233Trace length statistics: max=30, min=16, average=19.131234You may increase --max-samples and --max-steps.1235Use --verbosity to produce more (or less) output.1236Use --seed=0xa7c140fca5a5ec72 --backend=rust to reproduce.1237An example execution:12381239[State 0]1240{1241 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1242 schedNoRevoke::scheduler::crashes: 0,1243 schedNoRevoke::scheduler::entry: [],1244 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1245 schedNoRevoke::scheduler::mAssigned: Set(),1246 schedNoRevoke::scheduler::mBuild: Set(),1247 schedNoRevoke::scheduler::mDone: Set(),1248 schedNoRevoke::scheduler::mExpect: Set(),1249 schedNoRevoke::scheduler::mResult: Set(),1250 schedNoRevoke::scheduler::mRetry: Set(),1251 schedNoRevoke::scheduler::mRevoke: Set(),1252 schedNoRevoke::scheduler::mSchedule: Set(),1253 schedNoRevoke::scheduler::published: 0,1254 schedNoRevoke::scheduler::publishedBy: Set(),1255 schedNoRevoke::scheduler::ws:1256 Map(1257 "w1" ->1258 {1259 attached: Set(),1260 built: false,1261 expecting: false,1262 running: false,1263 session: true,1264 up: true1265 },1266 "w2" ->1267 {1268 attached: Set(),1269 built: false,1270 expecting: false,1271 running: false,1272 session: true,1273 up: true1274 }1275 )1276}12771278[State 1]1279{1280 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1281 schedNoRevoke::scheduler::crashes: 0,1282 schedNoRevoke::scheduler::entry: [],1283 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1284 schedNoRevoke::scheduler::mAssigned: Set(),1285 schedNoRevoke::scheduler::mBuild: Set(),1286 schedNoRevoke::scheduler::mDone: Set(),1287 schedNoRevoke::scheduler::mExpect: Set(),1288 schedNoRevoke::scheduler::mResult: Set(),1289 schedNoRevoke::scheduler::mRetry: Set(),1290 schedNoRevoke::scheduler::mRevoke: Set(),1291 schedNoRevoke::scheduler::mSchedule: Set("c1"),1292 schedNoRevoke::scheduler::published: 0,1293 schedNoRevoke::scheduler::publishedBy: Set(),1294 schedNoRevoke::scheduler::ws:1295 Map(1296 "w1" ->1297 {1298 attached: Set(),1299 built: false,1300 expecting: false,1301 running: false,1302 session: true,1303 up: true1304 },1305 "w2" ->1306 {1307 attached: Set(),1308 built: false,1309 expecting: false,1310 running: false,1311 session: true,1312 up: true1313 }1314 )1315}13161317[State 2]1318{1319 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1320 schedNoRevoke::scheduler::crashes: 0,1321 schedNoRevoke::scheduler::entry:1322 [{ followers: Set("c1"), leased: true, worker: "w1" }],1323 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1324 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1325 schedNoRevoke::scheduler::mBuild: Set(),1326 schedNoRevoke::scheduler::mDone: Set(),1327 schedNoRevoke::scheduler::mExpect: Set("w1"),1328 schedNoRevoke::scheduler::mResult: Set(),1329 schedNoRevoke::scheduler::mRetry: Set(),1330 schedNoRevoke::scheduler::mRevoke: Set(),1331 schedNoRevoke::scheduler::mSchedule: Set(),1332 schedNoRevoke::scheduler::published: 0,1333 schedNoRevoke::scheduler::publishedBy: Set(),1334 schedNoRevoke::scheduler::ws:1335 Map(1336 "w1" ->1337 {1338 attached: Set(),1339 built: false,1340 expecting: false,1341 running: false,1342 session: true,1343 up: true1344 },1345 "w2" ->1346 {1347 attached: Set(),1348 built: false,1349 expecting: false,1350 running: false,1351 session: true,1352 up: true1353 }1354 )1355}13561357[State 3]1358{1359 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1360 schedNoRevoke::scheduler::crashes: 0,1361 schedNoRevoke::scheduler::entry:1362 [{ followers: Set("c1"), leased: true, worker: "w1" }],1363 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1364 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1365 schedNoRevoke::scheduler::mBuild: Set(),1366 schedNoRevoke::scheduler::mDone: Set(),1367 schedNoRevoke::scheduler::mExpect: Set(),1368 schedNoRevoke::scheduler::mResult: Set(),1369 schedNoRevoke::scheduler::mRetry: Set(),1370 schedNoRevoke::scheduler::mRevoke: Set(),1371 schedNoRevoke::scheduler::mSchedule: Set(),1372 schedNoRevoke::scheduler::published: 0,1373 schedNoRevoke::scheduler::publishedBy: Set(),1374 schedNoRevoke::scheduler::ws:1375 Map(1376 "w1" ->1377 {1378 attached: Set(),1379 built: false,1380 expecting: true,1381 running: true,1382 session: true,1383 up: true1384 },1385 "w2" ->1386 {1387 attached: Set(),1388 built: false,1389 expecting: false,1390 running: false,1391 session: true,1392 up: true1393 }1394 )1395}13961397[State 4]1398{1399 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1400 schedNoRevoke::scheduler::crashes: 0,1401 schedNoRevoke::scheduler::entry:1402 [{ followers: Set("c1"), leased: true, worker: "w1" }],1403 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1404 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1405 schedNoRevoke::scheduler::mBuild: Set(),1406 schedNoRevoke::scheduler::mDone: Set(),1407 schedNoRevoke::scheduler::mExpect: Set(),1408 schedNoRevoke::scheduler::mResult: Set(),1409 schedNoRevoke::scheduler::mRetry: Set(),1410 schedNoRevoke::scheduler::mRevoke: Set(),1411 schedNoRevoke::scheduler::mSchedule: Set("c2"),1412 schedNoRevoke::scheduler::published: 0,1413 schedNoRevoke::scheduler::publishedBy: Set(),1414 schedNoRevoke::scheduler::ws:1415 Map(1416 "w1" ->1417 {1418 attached: Set(),1419 built: false,1420 expecting: true,1421 running: true,1422 session: true,1423 up: true1424 },1425 "w2" ->1426 {1427 attached: Set(),1428 built: false,1429 expecting: false,1430 running: false,1431 session: true,1432 up: true1433 }1434 )1435}14361437[State 5]1438{1439 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1440 schedNoRevoke::scheduler::crashes: 1,1441 schedNoRevoke::scheduler::entry: [],1442 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1443 schedNoRevoke::scheduler::mAssigned: Set(),1444 schedNoRevoke::scheduler::mBuild: Set(),1445 schedNoRevoke::scheduler::mDone: Set(),1446 schedNoRevoke::scheduler::mExpect: Set(),1447 schedNoRevoke::scheduler::mResult: Set(),1448 schedNoRevoke::scheduler::mRetry: Set("c1", "c2"),1449 schedNoRevoke::scheduler::mRevoke: Set(),1450 schedNoRevoke::scheduler::mSchedule: Set(),1451 schedNoRevoke::scheduler::published: 0,1452 schedNoRevoke::scheduler::publishedBy: Set(),1453 schedNoRevoke::scheduler::ws:1454 Map(1455 "w1" ->1456 {1457 attached: Set(),1458 built: false,1459 expecting: true,1460 running: true,1461 session: false,1462 up: true1463 },1464 "w2" ->1465 {1466 attached: Set(),1467 built: false,1468 expecting: false,1469 running: false,1470 session: false,1471 up: true1472 }1473 )1474}14751476[State 6]1477{1478 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1479 schedNoRevoke::scheduler::crashes: 2,1480 schedNoRevoke::scheduler::entry: [],1481 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1482 schedNoRevoke::scheduler::mAssigned: Set(),1483 schedNoRevoke::scheduler::mBuild: Set(),1484 schedNoRevoke::scheduler::mDone: Set(),1485 schedNoRevoke::scheduler::mExpect: Set(),1486 schedNoRevoke::scheduler::mResult: Set(),1487 schedNoRevoke::scheduler::mRetry: Set("c1", "c2"),1488 schedNoRevoke::scheduler::mRevoke: Set(),1489 schedNoRevoke::scheduler::mSchedule: Set(),1490 schedNoRevoke::scheduler::published: 0,1491 schedNoRevoke::scheduler::publishedBy: Set(),1492 schedNoRevoke::scheduler::ws:1493 Map(1494 "w1" ->1495 {1496 attached: Set(),1497 built: false,1498 expecting: true,1499 running: true,1500 session: false,1501 up: true1502 },1503 "w2" ->1504 {1505 attached: Set(),1506 built: false,1507 expecting: false,1508 running: false,1509 session: false,1510 up: true1511 }1512 )1513}15141515[State 7]1516{1517 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1518 schedNoRevoke::scheduler::crashes: 2,1519 schedNoRevoke::scheduler::entry: [],1520 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1521 schedNoRevoke::scheduler::mAssigned: Set(),1522 schedNoRevoke::scheduler::mBuild: Set(),1523 schedNoRevoke::scheduler::mDone: Set(),1524 schedNoRevoke::scheduler::mExpect: Set(),1525 schedNoRevoke::scheduler::mResult: Set(),1526 schedNoRevoke::scheduler::mRetry: Set("c1", "c2"),1527 schedNoRevoke::scheduler::mRevoke: Set(),1528 schedNoRevoke::scheduler::mSchedule: Set(),1529 schedNoRevoke::scheduler::published: 0,1530 schedNoRevoke::scheduler::publishedBy: Set(),1531 schedNoRevoke::scheduler::ws:1532 Map(1533 "w1" ->1534 {1535 attached: Set(),1536 built: false,1537 expecting: true,1538 running: true,1539 session: false,1540 up: true1541 },1542 "w2" ->1543 {1544 attached: Set(),1545 built: false,1546 expecting: false,1547 running: false,1548 session: true,1549 up: true1550 }1551 )1552}15531554[State 8]1555{1556 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1557 schedNoRevoke::scheduler::crashes: 2,1558 schedNoRevoke::scheduler::entry: [],1559 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1560 schedNoRevoke::scheduler::mAssigned: Set(),1561 schedNoRevoke::scheduler::mBuild: Set(),1562 schedNoRevoke::scheduler::mDone: Set(),1563 schedNoRevoke::scheduler::mExpect: Set(),1564 schedNoRevoke::scheduler::mResult: Set(),1565 schedNoRevoke::scheduler::mRetry: Set("c1"),1566 schedNoRevoke::scheduler::mRevoke: Set(),1567 schedNoRevoke::scheduler::mSchedule: Set("c2"),1568 schedNoRevoke::scheduler::published: 0,1569 schedNoRevoke::scheduler::publishedBy: Set(),1570 schedNoRevoke::scheduler::ws:1571 Map(1572 "w1" ->1573 {1574 attached: Set(),1575 built: false,1576 expecting: true,1577 running: true,1578 session: false,1579 up: true1580 },1581 "w2" ->1582 {1583 attached: Set(),1584 built: false,1585 expecting: false,1586 running: false,1587 session: true,1588 up: true1589 }1590 )1591}15921593[State 9]1594{1595 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1596 schedNoRevoke::scheduler::crashes: 2,1597 schedNoRevoke::scheduler::entry:1598 [{ followers: Set("c2"), leased: true, worker: "w2" }],1599 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1600 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1601 schedNoRevoke::scheduler::mBuild: Set(),1602 schedNoRevoke::scheduler::mDone: Set(),1603 schedNoRevoke::scheduler::mExpect: Set("w2"),1604 schedNoRevoke::scheduler::mResult: Set(),1605 schedNoRevoke::scheduler::mRetry: Set("c1"),1606 schedNoRevoke::scheduler::mRevoke: Set(),1607 schedNoRevoke::scheduler::mSchedule: Set(),1608 schedNoRevoke::scheduler::published: 0,1609 schedNoRevoke::scheduler::publishedBy: Set(),1610 schedNoRevoke::scheduler::ws:1611 Map(1612 "w1" ->1613 {1614 attached: Set(),1615 built: false,1616 expecting: true,1617 running: true,1618 session: false,1619 up: true1620 },1621 "w2" ->1622 {1623 attached: Set(),1624 built: false,1625 expecting: false,1626 running: false,1627 session: true,1628 up: true1629 }1630 )1631}16321633[State 10]1634{1635 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1636 schedNoRevoke::scheduler::crashes: 2,1637 schedNoRevoke::scheduler::entry:1638 [{ followers: Set("c2"), leased: true, worker: "w2" }],1639 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1640 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1641 schedNoRevoke::scheduler::mBuild: Set(),1642 schedNoRevoke::scheduler::mDone: Set(),1643 schedNoRevoke::scheduler::mExpect: Set("w2"),1644 schedNoRevoke::scheduler::mResult: Set(),1645 schedNoRevoke::scheduler::mRetry: Set("c1"),1646 schedNoRevoke::scheduler::mRevoke: Set(),1647 schedNoRevoke::scheduler::mSchedule: Set(),1648 schedNoRevoke::scheduler::published: 0,1649 schedNoRevoke::scheduler::publishedBy: Set(),1650 schedNoRevoke::scheduler::ws:1651 Map(1652 "w1" ->1653 {1654 attached: Set(),1655 built: false,1656 expecting: true,1657 running: true,1658 session: true,1659 up: true1660 },1661 "w2" ->1662 {1663 attached: Set(),1664 built: false,1665 expecting: false,1666 running: false,1667 session: true,1668 up: true1669 }1670 )1671}16721673[State 11]1674{1675 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1676 schedNoRevoke::scheduler::crashes: 2,1677 schedNoRevoke::scheduler::entry:1678 [{ followers: Set("c2"), leased: true, worker: "w2" }],1679 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1680 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1681 schedNoRevoke::scheduler::mBuild: Set(),1682 schedNoRevoke::scheduler::mDone: Set(),1683 schedNoRevoke::scheduler::mExpect: Set(),1684 schedNoRevoke::scheduler::mResult: Set(),1685 schedNoRevoke::scheduler::mRetry: Set("c1"),1686 schedNoRevoke::scheduler::mRevoke: Set(),1687 schedNoRevoke::scheduler::mSchedule: Set(),1688 schedNoRevoke::scheduler::published: 0,1689 schedNoRevoke::scheduler::publishedBy: Set(),1690 schedNoRevoke::scheduler::ws:1691 Map(1692 "w1" ->1693 {1694 attached: Set(),1695 built: false,1696 expecting: true,1697 running: true,1698 session: true,1699 up: true1700 },1701 "w2" ->1702 {1703 attached: Set(),1704 built: false,1705 expecting: true,1706 running: true,1707 session: true,1708 up: true1709 }1710 )1711}17121713[violation] Found an issue (656ms at 44117 traces/second).1714Use --verbosity=3 to show executions.1715Use --seed=0x49fa852c93eb9252 --backend=rust to reproduce.1716error: Invariant violated1717An example execution:17181719[State 0]1720{1721 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1722 schedNoFence::scheduler::crashes: 0,1723 schedNoFence::scheduler::entry: [],1724 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1725 schedNoFence::scheduler::mAssigned: Set(),1726 schedNoFence::scheduler::mBuild: Set(),1727 schedNoFence::scheduler::mDone: Set(),1728 schedNoFence::scheduler::mExpect: Set(),1729 schedNoFence::scheduler::mResult: Set(),1730 schedNoFence::scheduler::mRetry: Set(),1731 schedNoFence::scheduler::mRevoke: Set(),1732 schedNoFence::scheduler::mSchedule: Set(),1733 schedNoFence::scheduler::published: 0,1734 schedNoFence::scheduler::publishedBy: Set(),1735 schedNoFence::scheduler::ws:1736 Map(1737 "w1" ->1738 {1739 attached: Set(),1740 built: false,1741 expecting: false,1742 running: false,1743 session: true,1744 up: true1745 },1746 "w2" ->1747 {1748 attached: Set(),1749 built: false,1750 expecting: false,1751 running: false,1752 session: true,1753 up: true1754 }1755 )1756}17571758[State 1]1759{1760 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1761 schedNoFence::scheduler::crashes: 0,1762 schedNoFence::scheduler::entry: [],1763 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1764 schedNoFence::scheduler::mAssigned: Set(),1765 schedNoFence::scheduler::mBuild: Set(),1766 schedNoFence::scheduler::mDone: Set(),1767 schedNoFence::scheduler::mExpect: Set(),1768 schedNoFence::scheduler::mResult: Set(),1769 schedNoFence::scheduler::mRetry: Set(),1770 schedNoFence::scheduler::mRevoke: Set(),1771 schedNoFence::scheduler::mSchedule: Set("c2"),1772 schedNoFence::scheduler::published: 0,1773 schedNoFence::scheduler::publishedBy: Set(),1774 schedNoFence::scheduler::ws:1775 Map(1776 "w1" ->1777 {1778 attached: Set(),1779 built: false,1780 expecting: false,1781 running: false,1782 session: true,1783 up: true1784 },1785 "w2" ->1786 {1787 attached: Set(),1788 built: false,1789 expecting: false,1790 running: false,1791 session: true,1792 up: true1793 }1794 )1795}17961797[State 2]1798{1799 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1800 schedNoFence::scheduler::crashes: 0,1801 schedNoFence::scheduler::entry:1802 [{ followers: Set("c2"), leased: true, worker: "w1" }],1803 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1804 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1805 schedNoFence::scheduler::mBuild: Set(),1806 schedNoFence::scheduler::mDone: Set(),1807 schedNoFence::scheduler::mExpect: Set("w1"),1808 schedNoFence::scheduler::mResult: Set(),1809 schedNoFence::scheduler::mRetry: Set(),1810 schedNoFence::scheduler::mRevoke: Set(),1811 schedNoFence::scheduler::mSchedule: Set(),1812 schedNoFence::scheduler::published: 0,1813 schedNoFence::scheduler::publishedBy: Set(),1814 schedNoFence::scheduler::ws:1815 Map(1816 "w1" ->1817 {1818 attached: Set(),1819 built: false,1820 expecting: false,1821 running: false,1822 session: true,1823 up: true1824 },1825 "w2" ->1826 {1827 attached: Set(),1828 built: false,1829 expecting: false,1830 running: false,1831 session: true,1832 up: true1833 }1834 )1835}18361837[State 3]1838{1839 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1840 schedNoFence::scheduler::crashes: 0,1841 schedNoFence::scheduler::entry:1842 [{ followers: Set("c2"), leased: true, worker: "w1" }],1843 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1844 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1845 schedNoFence::scheduler::mBuild: Set(),1846 schedNoFence::scheduler::mDone: Set(),1847 schedNoFence::scheduler::mExpect: Set(),1848 schedNoFence::scheduler::mResult: Set(),1849 schedNoFence::scheduler::mRetry: Set(),1850 schedNoFence::scheduler::mRevoke: Set(),1851 schedNoFence::scheduler::mSchedule: Set(),1852 schedNoFence::scheduler::published: 0,1853 schedNoFence::scheduler::publishedBy: Set(),1854 schedNoFence::scheduler::ws:1855 Map(1856 "w1" ->1857 {1858 attached: Set(),1859 built: false,1860 expecting: true,1861 running: true,1862 session: true,1863 up: true1864 },1865 "w2" ->1866 {1867 attached: Set(),1868 built: false,1869 expecting: false,1870 running: false,1871 session: true,1872 up: true1873 }1874 )1875}18761877[State 4]1878{1879 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1880 schedNoFence::scheduler::crashes: 1,1881 schedNoFence::scheduler::entry:1882 [{ followers: Set("c2"), leased: true, worker: "w1" }],1883 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1884 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1885 schedNoFence::scheduler::mBuild: Set(),1886 schedNoFence::scheduler::mDone: Set(),1887 schedNoFence::scheduler::mExpect: Set(),1888 schedNoFence::scheduler::mResult: Set(),1889 schedNoFence::scheduler::mRetry: Set(),1890 schedNoFence::scheduler::mRevoke: Set(),1891 schedNoFence::scheduler::mSchedule: Set(),1892 schedNoFence::scheduler::published: 0,1893 schedNoFence::scheduler::publishedBy: Set(),1894 schedNoFence::scheduler::ws:1895 Map(1896 "w1" ->1897 {1898 attached: Set(),1899 built: false,1900 expecting: true,1901 running: true,1902 session: true,1903 up: true1904 },1905 "w2" ->1906 {1907 attached: Set(),1908 built: false,1909 expecting: false,1910 running: false,1911 session: false,1912 up: false1913 }1914 )1915}19161917[State 5]1918{1919 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1920 schedNoFence::scheduler::crashes: 2,1921 schedNoFence::scheduler::entry: [],1922 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1923 schedNoFence::scheduler::mAssigned: Set(),1924 schedNoFence::scheduler::mBuild: Set(),1925 schedNoFence::scheduler::mDone: Set(),1926 schedNoFence::scheduler::mExpect: Set(),1927 schedNoFence::scheduler::mResult: Set(),1928 schedNoFence::scheduler::mRetry: Set("c2"),1929 schedNoFence::scheduler::mRevoke: Set(),1930 schedNoFence::scheduler::mSchedule: Set(),1931 schedNoFence::scheduler::published: 0,1932 schedNoFence::scheduler::publishedBy: Set(),1933 schedNoFence::scheduler::ws:1934 Map(1935 "w1" ->1936 {1937 attached: Set(),1938 built: false,1939 expecting: true,1940 running: true,1941 session: false,1942 up: true1943 },1944 "w2" ->1945 {1946 attached: Set(),1947 built: false,1948 expecting: false,1949 running: false,1950 session: false,1951 up: false1952 }1953 )1954}19551956[State 6]1957{1958 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1959 schedNoFence::scheduler::crashes: 2,1960 schedNoFence::scheduler::entry: [],1961 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1962 schedNoFence::scheduler::mAssigned: Set(),1963 schedNoFence::scheduler::mBuild: Set(),1964 schedNoFence::scheduler::mDone: Set(),1965 schedNoFence::scheduler::mExpect: Set(),1966 schedNoFence::scheduler::mResult: Set(),1967 schedNoFence::scheduler::mRetry: Set("c2"),1968 schedNoFence::scheduler::mRevoke: Set(),1969 schedNoFence::scheduler::mSchedule: Set(),1970 schedNoFence::scheduler::published: 0,1971 schedNoFence::scheduler::publishedBy: Set(),1972 schedNoFence::scheduler::ws:1973 Map(1974 "w1" ->1975 {1976 attached: Set(),1977 built: false,1978 expecting: true,1979 running: true,1980 session: false,1981 up: true1982 },1983 "w2" ->1984 {1985 attached: Set(),1986 built: false,1987 expecting: false,1988 running: false,1989 session: true,1990 up: true1991 }1992 )1993}19941995[State 7]1996{1997 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1998 schedNoFence::scheduler::crashes: 2,1999 schedNoFence::scheduler::entry: [],2000 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),2001 schedNoFence::scheduler::mAssigned: Set(),2002 schedNoFence::scheduler::mBuild: Set(),2003 schedNoFence::scheduler::mDone: Set(),2004 schedNoFence::scheduler::mExpect: Set(),2005 schedNoFence::scheduler::mResult: Set(),2006 schedNoFence::scheduler::mRetry: Set(),2007 schedNoFence::scheduler::mRevoke: Set(),2008 schedNoFence::scheduler::mSchedule: Set("c2"),2009 schedNoFence::scheduler::published: 0,2010 schedNoFence::scheduler::publishedBy: Set(),2011 schedNoFence::scheduler::ws:2012 Map(2013 "w1" ->2014 {2015 attached: Set(),2016 built: false,2017 expecting: true,2018 running: true,2019 session: false,2020 up: true2021 },2022 "w2" ->2023 {2024 attached: Set(),2025 built: false,2026 expecting: false,2027 running: false,2028 session: true,2029 up: true2030 }2031 )2032}20332034[State 8]2035{2036 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2037 schedNoFence::scheduler::crashes: 2,2038 schedNoFence::scheduler::entry:2039 [{ followers: Set("c2"), leased: true, worker: "w2" }],2040 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2041 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2042 schedNoFence::scheduler::mBuild: Set(),2043 schedNoFence::scheduler::mDone: Set(),2044 schedNoFence::scheduler::mExpect: Set("w2"),2045 schedNoFence::scheduler::mResult: Set(),2046 schedNoFence::scheduler::mRetry: Set(),2047 schedNoFence::scheduler::mRevoke: Set(),2048 schedNoFence::scheduler::mSchedule: Set(),2049 schedNoFence::scheduler::published: 0,2050 schedNoFence::scheduler::publishedBy: Set(),2051 schedNoFence::scheduler::ws:2052 Map(2053 "w1" ->2054 {2055 attached: Set(),2056 built: false,2057 expecting: true,2058 running: true,2059 session: false,2060 up: true2061 },2062 "w2" ->2063 {2064 attached: Set(),2065 built: false,2066 expecting: false,2067 running: false,2068 session: true,2069 up: true2070 }2071 )2072}20732074[State 9]2075{2076 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2077 schedNoFence::scheduler::crashes: 2,2078 schedNoFence::scheduler::entry:2079 [{ followers: Set("c2"), leased: true, worker: "w2" }],2080 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2081 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2082 schedNoFence::scheduler::mBuild: Set(),2083 schedNoFence::scheduler::mDone: Set(),2084 schedNoFence::scheduler::mExpect: Set(),2085 schedNoFence::scheduler::mResult: Set(),2086 schedNoFence::scheduler::mRetry: Set(),2087 schedNoFence::scheduler::mRevoke: Set(),2088 schedNoFence::scheduler::mSchedule: Set(),2089 schedNoFence::scheduler::published: 0,2090 schedNoFence::scheduler::publishedBy: Set(),2091 schedNoFence::scheduler::ws:2092 Map(2093 "w1" ->2094 {2095 attached: Set(),2096 built: false,2097 expecting: true,2098 running: true,2099 session: false,2100 up: true2101 },2102 "w2" ->2103 {2104 attached: Set(),2105 built: false,2106 expecting: true,2107 running: true,2108 session: true,2109 up: true2110 }2111 )2112}21132114[State 10]2115{2116 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2117 schedNoFence::scheduler::crashes: 2,2118 schedNoFence::scheduler::entry:2119 [{ followers: Set("c2"), leased: true, worker: "w2" }],2120 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2121 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2122 schedNoFence::scheduler::mBuild: Set(),2123 schedNoFence::scheduler::mDone: Set(),2124 schedNoFence::scheduler::mExpect: Set(),2125 schedNoFence::scheduler::mResult: Set(),2126 schedNoFence::scheduler::mRetry: Set(),2127 schedNoFence::scheduler::mRevoke: Set(),2128 schedNoFence::scheduler::mSchedule: Set(),2129 schedNoFence::scheduler::published: 1,2130 schedNoFence::scheduler::publishedBy: Set("w1"),2131 schedNoFence::scheduler::ws:2132 Map(2133 "w1" ->2134 {2135 attached: Set(),2136 built: true,2137 expecting: false,2138 running: false,2139 session: false,2140 up: true2141 },2142 "w2" ->2143 {2144 attached: Set(),2145 built: false,2146 expecting: true,2147 running: true,2148 session: true,2149 up: true2150 }2151 )2152}21532154[State 11]2155{2156 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2157 schedNoFence::scheduler::crashes: 2,2158 schedNoFence::scheduler::entry:2159 [{ followers: Set("c2"), leased: true, worker: "w2" }],2160 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2161 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2162 schedNoFence::scheduler::mBuild: Set(),2163 schedNoFence::scheduler::mDone: Set("w2"),2164 schedNoFence::scheduler::mExpect: Set(),2165 schedNoFence::scheduler::mResult: Set(),2166 schedNoFence::scheduler::mRetry: Set(),2167 schedNoFence::scheduler::mRevoke: Set(),2168 schedNoFence::scheduler::mSchedule: Set(),2169 schedNoFence::scheduler::published: 2,2170 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2171 schedNoFence::scheduler::ws:2172 Map(2173 "w1" ->2174 {2175 attached: Set(),2176 built: true,2177 expecting: false,2178 running: false,2179 session: false,2180 up: true2181 },2182 "w2" ->2183 {2184 attached: Set(),2185 built: true,2186 expecting: false,2187 running: false,2188 session: true,2189 up: true2190 }2191 )2192}21932194[violation] Found an issue (564ms at 46186 traces/second).2195Use --verbosity=3 to show executions.2196Use --seed=0x5cd2594a42082d9b --backend=rust to reproduce.2197error: Invariant violated2198An example execution:21992200[State 0]2201{2202 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2203 schedNoPush::scheduler::crashes: 0,2204 schedNoPush::scheduler::entry: [],2205 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2206 schedNoPush::scheduler::mAssigned: Set(),2207 schedNoPush::scheduler::mBuild: Set(),2208 schedNoPush::scheduler::mDone: Set(),2209 schedNoPush::scheduler::mExpect: Set(),2210 schedNoPush::scheduler::mResult: Set(),2211 schedNoPush::scheduler::mRetry: Set(),2212 schedNoPush::scheduler::mRevoke: Set(),2213 schedNoPush::scheduler::mSchedule: Set(),2214 schedNoPush::scheduler::published: 0,2215 schedNoPush::scheduler::publishedBy: Set(),2216 schedNoPush::scheduler::ws:2217 Map(2218 "w1" ->2219 {2220 attached: Set(),2221 built: false,2222 expecting: false,2223 running: false,2224 session: true,2225 up: true2226 },2227 "w2" ->2228 {2229 attached: Set(),2230 built: false,2231 expecting: false,2232 running: false,2233 session: true,2234 up: true2235 }2236 )2237}22382239[State 1]2240{2241 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2242 schedNoPush::scheduler::crashes: 0,2243 schedNoPush::scheduler::entry: [],2244 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2245 schedNoPush::scheduler::mAssigned: Set(),2246 schedNoPush::scheduler::mBuild: Set(),2247 schedNoPush::scheduler::mDone: Set(),2248 schedNoPush::scheduler::mExpect: Set(),2249 schedNoPush::scheduler::mResult: Set(),2250 schedNoPush::scheduler::mRetry: Set(),2251 schedNoPush::scheduler::mRevoke: Set(),2252 schedNoPush::scheduler::mSchedule: Set("c1"),2253 schedNoPush::scheduler::published: 0,2254 schedNoPush::scheduler::publishedBy: Set(),2255 schedNoPush::scheduler::ws:2256 Map(2257 "w1" ->2258 {2259 attached: Set(),2260 built: false,2261 expecting: false,2262 running: false,2263 session: true,2264 up: true2265 },2266 "w2" ->2267 {2268 attached: Set(),2269 built: false,2270 expecting: false,2271 running: false,2272 session: true,2273 up: true2274 }2275 )2276}22772278[State 2]2279{2280 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2281 schedNoPush::scheduler::crashes: 0,2282 schedNoPush::scheduler::entry:2283 [{ followers: Set("c1"), leased: true, worker: "w1" }],2284 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2285 schedNoPush::scheduler::mAssigned: Set(("c1", "w1")),2286 schedNoPush::scheduler::mBuild: Set(),2287 schedNoPush::scheduler::mDone: Set(),2288 schedNoPush::scheduler::mExpect: Set(),2289 schedNoPush::scheduler::mResult: Set(),2290 schedNoPush::scheduler::mRetry: Set(),2291 schedNoPush::scheduler::mRevoke: Set(),2292 schedNoPush::scheduler::mSchedule: Set(),2293 schedNoPush::scheduler::published: 0,2294 schedNoPush::scheduler::publishedBy: Set(),2295 schedNoPush::scheduler::ws:2296 Map(2297 "w1" ->2298 {2299 attached: Set(),2300 built: false,2301 expecting: false,2302 running: false,2303 session: true,2304 up: true2305 },2306 "w2" ->2307 {2308 attached: Set(),2309 built: false,2310 expecting: false,2311 running: false,2312 session: true,2313 up: true2314 }2315 )2316}23172318[State 3]2319{2320 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2321 schedNoPush::scheduler::crashes: 0,2322 schedNoPush::scheduler::entry:2323 [{ followers: Set("c1"), leased: true, worker: "w1" }],2324 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2325 schedNoPush::scheduler::mAssigned: Set(),2326 schedNoPush::scheduler::mBuild: Set(("c1", "w1")),2327 schedNoPush::scheduler::mDone: Set(),2328 schedNoPush::scheduler::mExpect: Set(),2329 schedNoPush::scheduler::mResult: Set(),2330 schedNoPush::scheduler::mRetry: Set(),2331 schedNoPush::scheduler::mRevoke: Set(),2332 schedNoPush::scheduler::mSchedule: Set(),2333 schedNoPush::scheduler::published: 0,2334 schedNoPush::scheduler::publishedBy: Set(),2335 schedNoPush::scheduler::ws:2336 Map(2337 "w1" ->2338 {2339 attached: Set(),2340 built: false,2341 expecting: false,2342 running: false,2343 session: true,2344 up: true2345 },2346 "w2" ->2347 {2348 attached: Set(),2349 built: false,2350 expecting: false,2351 running: false,2352 session: true,2353 up: true2354 }2355 )2356}23572358[State 4]2359{2360 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2361 schedNoPush::scheduler::crashes: 1,2362 schedNoPush::scheduler::entry: [],2363 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2364 schedNoPush::scheduler::mAssigned: Set(),2365 schedNoPush::scheduler::mBuild: Set(("c1", "w1")),2366 schedNoPush::scheduler::mDone: Set(),2367 schedNoPush::scheduler::mExpect: Set(),2368 schedNoPush::scheduler::mResult: Set(),2369 schedNoPush::scheduler::mRetry: Set(),2370 schedNoPush::scheduler::mRevoke: Set(),2371 schedNoPush::scheduler::mSchedule: Set(),2372 schedNoPush::scheduler::published: 0,2373 schedNoPush::scheduler::publishedBy: Set(),2374 schedNoPush::scheduler::ws:2375 Map(2376 "w1" ->2377 {2378 attached: Set(),2379 built: false,2380 expecting: false,2381 running: false,2382 session: false,2383 up: true2384 },2385 "w2" ->2386 {2387 attached: Set(),2388 built: false,2389 expecting: false,2390 running: false,2391 session: false,2392 up: true2393 }2394 )2395}23962397[State 5]2398{2399 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2400 schedNoPush::scheduler::crashes: 1,2401 schedNoPush::scheduler::entry: [],2402 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2403 schedNoPush::scheduler::mAssigned: Set(),2404 schedNoPush::scheduler::mBuild: Set(("c1", "w1")),2405 schedNoPush::scheduler::mDone: Set(),2406 schedNoPush::scheduler::mExpect: Set(),2407 schedNoPush::scheduler::mResult: Set(),2408 schedNoPush::scheduler::mRetry: Set(),2409 schedNoPush::scheduler::mRevoke: Set(),2410 schedNoPush::scheduler::mSchedule: Set(),2411 schedNoPush::scheduler::published: 0,2412 schedNoPush::scheduler::publishedBy: Set(),2413 schedNoPush::scheduler::ws:2414 Map(2415 "w1" ->2416 {2417 attached: Set(),2418 built: false,2419 expecting: false,2420 running: false,2421 session: true,2422 up: true2423 },2424 "w2" ->2425 {2426 attached: Set(),2427 built: false,2428 expecting: false,2429 running: false,2430 session: false,2431 up: true2432 }2433 )2434}24352436[State 6]2437{2438 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2439 schedNoPush::scheduler::crashes: 1,2440 schedNoPush::scheduler::entry: [],2441 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2442 schedNoPush::scheduler::mAssigned: Set(),2443 schedNoPush::scheduler::mBuild: Set(),2444 schedNoPush::scheduler::mDone: Set(),2445 schedNoPush::scheduler::mExpect: Set(),2446 schedNoPush::scheduler::mResult: Set(),2447 schedNoPush::scheduler::mRetry: Set(),2448 schedNoPush::scheduler::mRevoke: Set(),2449 schedNoPush::scheduler::mSchedule: Set(),2450 schedNoPush::scheduler::published: 0,2451 schedNoPush::scheduler::publishedBy: Set(),2452 schedNoPush::scheduler::ws:2453 Map(2454 "w1" ->2455 {2456 attached: Set("c1"),2457 built: false,2458 expecting: true,2459 running: true,2460 session: true,2461 up: true2462 },2463 "w2" ->2464 {2465 attached: Set(),2466 built: false,2467 expecting: false,2468 running: false,2469 session: false,2470 up: true2471 }2472 )2473}24742475[violation] Found an issue (439ms at 28282 traces/second).2476Use --verbosity=3 to show executions.2477Use --seed=0xcd9f14a1c77efd3e --backend=rust to reproduce.2478error: Invariant violated2479An example execution:24802481[State 0]2482{2483 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2484 schedNoReport::scheduler::crashes: 0,2485 schedNoReport::scheduler::entry: [],2486 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2487 schedNoReport::scheduler::mAssigned: Set(),2488 schedNoReport::scheduler::mBuild: Set(),2489 schedNoReport::scheduler::mDone: Set(),2490 schedNoReport::scheduler::mExpect: Set(),2491 schedNoReport::scheduler::mResult: Set(),2492 schedNoReport::scheduler::mRetry: Set(),2493 schedNoReport::scheduler::mRevoke: Set(),2494 schedNoReport::scheduler::mSchedule: Set(),2495 schedNoReport::scheduler::published: 0,2496 schedNoReport::scheduler::publishedBy: Set(),2497 schedNoReport::scheduler::ws:2498 Map(2499 "w1" ->2500 {2501 attached: Set(),2502 built: false,2503 expecting: false,2504 running: false,2505 session: true,2506 up: true2507 },2508 "w2" ->2509 {2510 attached: Set(),2511 built: false,2512 expecting: false,2513 running: false,2514 session: true,2515 up: true2516 }2517 )2518}25192520[State 1]2521{2522 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2523 schedNoReport::scheduler::crashes: 0,2524 schedNoReport::scheduler::entry: [],2525 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2526 schedNoReport::scheduler::mAssigned: Set(),2527 schedNoReport::scheduler::mBuild: Set(),2528 schedNoReport::scheduler::mDone: Set(),2529 schedNoReport::scheduler::mExpect: Set(),2530 schedNoReport::scheduler::mResult: Set(),2531 schedNoReport::scheduler::mRetry: Set(),2532 schedNoReport::scheduler::mRevoke: Set(),2533 schedNoReport::scheduler::mSchedule: Set("c2"),2534 schedNoReport::scheduler::published: 0,2535 schedNoReport::scheduler::publishedBy: Set(),2536 schedNoReport::scheduler::ws:2537 Map(2538 "w1" ->2539 {2540 attached: Set(),2541 built: false,2542 expecting: false,2543 running: false,2544 session: true,2545 up: true2546 },2547 "w2" ->2548 {2549 attached: Set(),2550 built: false,2551 expecting: false,2552 running: false,2553 session: true,2554 up: true2555 }2556 )2557}25582559[State 2]2560{2561 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2562 schedNoReport::scheduler::crashes: 0,2563 schedNoReport::scheduler::entry:2564 [{ followers: Set("c2"), leased: true, worker: "w1" }],2565 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2566 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2567 schedNoReport::scheduler::mBuild: Set(),2568 schedNoReport::scheduler::mDone: Set(),2569 schedNoReport::scheduler::mExpect: Set("w1"),2570 schedNoReport::scheduler::mResult: Set(),2571 schedNoReport::scheduler::mRetry: Set(),2572 schedNoReport::scheduler::mRevoke: Set(),2573 schedNoReport::scheduler::mSchedule: Set(),2574 schedNoReport::scheduler::published: 0,2575 schedNoReport::scheduler::publishedBy: Set(),2576 schedNoReport::scheduler::ws:2577 Map(2578 "w1" ->2579 {2580 attached: Set(),2581 built: false,2582 expecting: false,2583 running: false,2584 session: true,2585 up: true2586 },2587 "w2" ->2588 {2589 attached: Set(),2590 built: false,2591 expecting: false,2592 running: false,2593 session: true,2594 up: true2595 }2596 )2597}25982599[State 3]2600{2601 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2602 schedNoReport::scheduler::crashes: 0,2603 schedNoReport::scheduler::entry:2604 [{ followers: Set("c2"), leased: true, worker: "w1" }],2605 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2606 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2607 schedNoReport::scheduler::mBuild: Set(),2608 schedNoReport::scheduler::mDone: Set(),2609 schedNoReport::scheduler::mExpect: Set(),2610 schedNoReport::scheduler::mResult: Set(),2611 schedNoReport::scheduler::mRetry: Set(),2612 schedNoReport::scheduler::mRevoke: Set(),2613 schedNoReport::scheduler::mSchedule: Set(),2614 schedNoReport::scheduler::published: 0,2615 schedNoReport::scheduler::publishedBy: Set(),2616 schedNoReport::scheduler::ws:2617 Map(2618 "w1" ->2619 {2620 attached: Set(),2621 built: false,2622 expecting: true,2623 running: true,2624 session: true,2625 up: true2626 },2627 "w2" ->2628 {2629 attached: Set(),2630 built: false,2631 expecting: false,2632 running: false,2633 session: true,2634 up: true2635 }2636 )2637}26382639[State 4]2640{2641 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2642 schedNoReport::scheduler::crashes: 1,2643 schedNoReport::scheduler::entry: [],2644 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2645 schedNoReport::scheduler::mAssigned: Set(),2646 schedNoReport::scheduler::mBuild: Set(),2647 schedNoReport::scheduler::mDone: Set(),2648 schedNoReport::scheduler::mExpect: Set(),2649 schedNoReport::scheduler::mResult: Set(),2650 schedNoReport::scheduler::mRetry: Set("c2"),2651 schedNoReport::scheduler::mRevoke: Set(),2652 schedNoReport::scheduler::mSchedule: Set(),2653 schedNoReport::scheduler::published: 0,2654 schedNoReport::scheduler::publishedBy: Set(),2655 schedNoReport::scheduler::ws:2656 Map(2657 "w1" ->2658 {2659 attached: Set(),2660 built: false,2661 expecting: true,2662 running: true,2663 session: false,2664 up: true2665 },2666 "w2" ->2667 {2668 attached: Set(),2669 built: false,2670 expecting: false,2671 running: false,2672 session: false,2673 up: true2674 }2675 )2676}26772678[State 5]2679{2680 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2681 schedNoReport::scheduler::crashes: 2,2682 schedNoReport::scheduler::entry: [],2683 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2684 schedNoReport::scheduler::mAssigned: Set(),2685 schedNoReport::scheduler::mBuild: Set(),2686 schedNoReport::scheduler::mDone: Set(),2687 schedNoReport::scheduler::mExpect: Set(),2688 schedNoReport::scheduler::mResult: Set(),2689 schedNoReport::scheduler::mRetry: Set("c2"),2690 schedNoReport::scheduler::mRevoke: Set(),2691 schedNoReport::scheduler::mSchedule: Set(),2692 schedNoReport::scheduler::published: 0,2693 schedNoReport::scheduler::publishedBy: Set(),2694 schedNoReport::scheduler::ws:2695 Map(2696 "w1" ->2697 {2698 attached: Set(),2699 built: false,2700 expecting: true,2701 running: true,2702 session: false,2703 up: true2704 },2705 "w2" ->2706 {2707 attached: Set(),2708 built: false,2709 expecting: false,2710 running: false,2711 session: false,2712 up: false2713 }2714 )2715}27162717[State 6]2718{2719 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2720 schedNoReport::scheduler::crashes: 2,2721 schedNoReport::scheduler::entry: [],2722 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2723 schedNoReport::scheduler::mAssigned: Set(),2724 schedNoReport::scheduler::mBuild: Set(),2725 schedNoReport::scheduler::mDone: Set(),2726 schedNoReport::scheduler::mExpect: Set(),2727 schedNoReport::scheduler::mResult: Set(),2728 schedNoReport::scheduler::mRetry: Set("c2"),2729 schedNoReport::scheduler::mRevoke: Set(),2730 schedNoReport::scheduler::mSchedule: Set(),2731 schedNoReport::scheduler::published: 0,2732 schedNoReport::scheduler::publishedBy: Set(),2733 schedNoReport::scheduler::ws:2734 Map(2735 "w1" ->2736 {2737 attached: Set(),2738 built: false,2739 expecting: true,2740 running: true,2741 session: false,2742 up: true2743 },2744 "w2" ->2745 {2746 attached: Set(),2747 built: false,2748 expecting: false,2749 running: false,2750 session: true,2751 up: true2752 }2753 )2754}27552756[State 7]2757{2758 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2759 schedNoReport::scheduler::crashes: 2,2760 schedNoReport::scheduler::entry: [],2761 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2762 schedNoReport::scheduler::mAssigned: Set(),2763 schedNoReport::scheduler::mBuild: Set(),2764 schedNoReport::scheduler::mDone: Set(),2765 schedNoReport::scheduler::mExpect: Set(),2766 schedNoReport::scheduler::mResult: Set(),2767 schedNoReport::scheduler::mRetry: Set("c2"),2768 schedNoReport::scheduler::mRevoke: Set(),2769 schedNoReport::scheduler::mSchedule: Set("c1"),2770 schedNoReport::scheduler::published: 0,2771 schedNoReport::scheduler::publishedBy: Set(),2772 schedNoReport::scheduler::ws:2773 Map(2774 "w1" ->2775 {2776 attached: Set(),2777 built: false,2778 expecting: true,2779 running: true,2780 session: false,2781 up: true2782 },2783 "w2" ->2784 {2785 attached: Set(),2786 built: false,2787 expecting: false,2788 running: false,2789 session: true,2790 up: true2791 }2792 )2793}27942795[State 8]2796{2797 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2798 schedNoReport::scheduler::crashes: 2,2799 schedNoReport::scheduler::entry: [],2800 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2801 schedNoReport::scheduler::mAssigned: Set(),2802 schedNoReport::scheduler::mBuild: Set(),2803 schedNoReport::scheduler::mDone: Set(),2804 schedNoReport::scheduler::mExpect: Set(),2805 schedNoReport::scheduler::mResult: Set(),2806 schedNoReport::scheduler::mRetry: Set("c2"),2807 schedNoReport::scheduler::mRevoke: Set(),2808 schedNoReport::scheduler::mSchedule: Set("c1"),2809 schedNoReport::scheduler::published: 0,2810 schedNoReport::scheduler::publishedBy: Set(),2811 schedNoReport::scheduler::ws:2812 Map(2813 "w1" ->2814 {2815 attached: Set(),2816 built: false,2817 expecting: true,2818 running: true,2819 session: true,2820 up: true2821 },2822 "w2" ->2823 {2824 attached: Set(),2825 built: false,2826 expecting: false,2827 running: false,2828 session: true,2829 up: true2830 }2831 )2832}28332834[State 9]2835{2836 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2837 schedNoReport::scheduler::crashes: 2,2838 schedNoReport::scheduler::entry:2839 [{ followers: Set("c1"), leased: true, worker: "w2" }],2840 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2841 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2842 schedNoReport::scheduler::mBuild: Set(),2843 schedNoReport::scheduler::mDone: Set(),2844 schedNoReport::scheduler::mExpect: Set("w2"),2845 schedNoReport::scheduler::mResult: Set(),2846 schedNoReport::scheduler::mRetry: Set("c2"),2847 schedNoReport::scheduler::mRevoke: Set(),2848 schedNoReport::scheduler::mSchedule: Set(),2849 schedNoReport::scheduler::published: 0,2850 schedNoReport::scheduler::publishedBy: Set(),2851 schedNoReport::scheduler::ws:2852 Map(2853 "w1" ->2854 {2855 attached: Set(),2856 built: false,2857 expecting: true,2858 running: true,2859 session: true,2860 up: true2861 },2862 "w2" ->2863 {2864 attached: Set(),2865 built: false,2866 expecting: false,2867 running: false,2868 session: true,2869 up: true2870 }2871 )2872}28732874[State 10]2875{2876 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2877 schedNoReport::scheduler::crashes: 2,2878 schedNoReport::scheduler::entry:2879 [{ followers: Set("c1"), leased: true, worker: "w2" }],2880 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2881 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2882 schedNoReport::scheduler::mBuild: Set(),2883 schedNoReport::scheduler::mDone: Set(),2884 schedNoReport::scheduler::mExpect: Set(),2885 schedNoReport::scheduler::mResult: Set(),2886 schedNoReport::scheduler::mRetry: Set("c2"),2887 schedNoReport::scheduler::mRevoke: Set(),2888 schedNoReport::scheduler::mSchedule: Set(),2889 schedNoReport::scheduler::published: 0,2890 schedNoReport::scheduler::publishedBy: Set(),2891 schedNoReport::scheduler::ws:2892 Map(2893 "w1" ->2894 {2895 attached: Set(),2896 built: false,2897 expecting: true,2898 running: true,2899 session: true,2900 up: true2901 },2902 "w2" ->2903 {2904 attached: Set(),2905 built: false,2906 expecting: true,2907 running: true,2908 session: true,2909 up: true2910 }2911 )2912}29132914[violation] Found an issue (435ms at 50644 traces/second).2915Use --verbosity=3 to show executions.2916Use --seed=0x6b111781e09be124 --backend=rust to reproduce.2917error: Invariant violated2918An example execution:29192920[State 0]2921{2922 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2923 schedTerminal::scheduler::crashes: 0,2924 schedTerminal::scheduler::entry: [],2925 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2926 schedTerminal::scheduler::mAssigned: Set(),2927 schedTerminal::scheduler::mBuild: Set(),2928 schedTerminal::scheduler::mDone: Set(),2929 schedTerminal::scheduler::mExpect: Set(),2930 schedTerminal::scheduler::mResult: Set(),2931 schedTerminal::scheduler::mRetry: Set(),2932 schedTerminal::scheduler::mRevoke: Set(),2933 schedTerminal::scheduler::mSchedule: Set(),2934 schedTerminal::scheduler::published: 0,2935 schedTerminal::scheduler::publishedBy: Set(),2936 schedTerminal::scheduler::ws:2937 Map(2938 "w1" ->2939 {2940 attached: Set(),2941 built: false,2942 expecting: false,2943 running: false,2944 session: true,2945 up: true2946 },2947 "w2" ->2948 {2949 attached: Set(),2950 built: false,2951 expecting: false,2952 running: false,2953 session: true,2954 up: true2955 }2956 )2957}29582959[State 1]2960{2961 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2962 schedTerminal::scheduler::crashes: 1,2963 schedTerminal::scheduler::entry: [],2964 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2965 schedTerminal::scheduler::mAssigned: Set(),2966 schedTerminal::scheduler::mBuild: Set(),2967 schedTerminal::scheduler::mDone: Set(),2968 schedTerminal::scheduler::mExpect: Set(),2969 schedTerminal::scheduler::mResult: Set(),2970 schedTerminal::scheduler::mRetry: Set(),2971 schedTerminal::scheduler::mRevoke: Set(),2972 schedTerminal::scheduler::mSchedule: Set(),2973 schedTerminal::scheduler::published: 0,2974 schedTerminal::scheduler::publishedBy: Set(),2975 schedTerminal::scheduler::ws:2976 Map(2977 "w1" ->2978 {2979 attached: Set(),2980 built: false,2981 expecting: false,2982 running: false,2983 session: false,2984 up: true2985 },2986 "w2" ->2987 {2988 attached: Set(),2989 built: false,2990 expecting: false,2991 running: false,2992 session: false,2993 up: true2994 }2995 )2996}29972998[State 2]2999{3000 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3001 schedTerminal::scheduler::crashes: 1,3002 schedTerminal::scheduler::entry: [],3003 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3004 schedTerminal::scheduler::mAssigned: Set(),3005 schedTerminal::scheduler::mBuild: Set(),3006 schedTerminal::scheduler::mDone: Set(),3007 schedTerminal::scheduler::mExpect: Set(),3008 schedTerminal::scheduler::mResult: Set(),3009 schedTerminal::scheduler::mRetry: Set(),3010 schedTerminal::scheduler::mRevoke: Set(),3011 schedTerminal::scheduler::mSchedule: Set("c2"),3012 schedTerminal::scheduler::published: 0,3013 schedTerminal::scheduler::publishedBy: Set(),3014 schedTerminal::scheduler::ws:3015 Map(3016 "w1" ->3017 {3018 attached: Set(),3019 built: false,3020 expecting: false,3021 running: false,3022 session: false,3023 up: true3024 },3025 "w2" ->3026 {3027 attached: Set(),3028 built: false,3029 expecting: false,3030 running: false,3031 session: false,3032 up: true3033 }3034 )3035}30363037[State 3]3038{3039 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3040 schedTerminal::scheduler::crashes: 1,3041 schedTerminal::scheduler::entry: [],3042 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3043 schedTerminal::scheduler::mAssigned: Set(),3044 schedTerminal::scheduler::mBuild: Set(),3045 schedTerminal::scheduler::mDone: Set(),3046 schedTerminal::scheduler::mExpect: Set(),3047 schedTerminal::scheduler::mResult: Set(),3048 schedTerminal::scheduler::mRetry: Set(),3049 schedTerminal::scheduler::mRevoke: Set(),3050 schedTerminal::scheduler::mSchedule: Set(),3051 schedTerminal::scheduler::published: 0,3052 schedTerminal::scheduler::publishedBy: Set(),3053 schedTerminal::scheduler::ws:3054 Map(3055 "w1" ->3056 {3057 attached: Set(),3058 built: false,3059 expecting: false,3060 running: false,3061 session: false,3062 up: true3063 },3064 "w2" ->3065 {3066 attached: Set(),3067 built: false,3068 expecting: false,3069 running: false,3070 session: false,3071 up: true3072 }3073 )3074}30753076[violation] Found an issue (167ms at 5754 traces/second).3077Use --verbosity=3 to show executions.3078Use --seed=0xb4ad4a025469fc80 --backend=rust to reproduce.3079error: Invariant violated3080An example execution:30813082[State 0]3083{3084 pushFixed::push::byPath: Map(),3085 pushFixed::push::inflight: Set(),3086 pushFixed::push::left: Map(),3087 pushFixed::push::sent: Map()3088}30893090[State 1]3091{3092 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3093 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3094 pushFixed::push::left: Map(1 -> 2),3095 pushFixed::push::sent: Map(1 -> Set("a", "b"))3096}30973098[State 2]3099{3100 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3101 pushFixed::push::inflight: Set((1, "b")),3102 pushFixed::push::left: Map(1 -> 1),3103 pushFixed::push::sent: Map(1 -> Set("a", "b"))3104}31053106[State 3]3107{3108 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3109 pushFixed::push::inflight: Set(),3110 pushFixed::push::left: Map(1 -> 0),3111 pushFixed::push::sent: Map(1 -> Set("a", "b"))3112}31133114[State 4]3115{3116 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3117 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3118 pushFixed::push::left: Map(1 -> 0, 3 -> 2),3119 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3120}31213122[State 5]3123{3124 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3125 pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "a"), (3, "b")),3126 pushFixed::push::left: Map(1 -> 0, 2 -> 2, 3 -> 2),3127 pushFixed::push::sent:3128 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3129}31303131[State 6]3132{3133 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3134 pushFixed::push::inflight: Set((2, "a"), (3, "a"), (3, "b")),3135 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 2),3136 pushFixed::push::sent:3137 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3138}31393140[State 7]3141{3142 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3143 pushFixed::push::inflight: Set((2, "a"), (3, "a")),3144 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 1),3145 pushFixed::push::sent:3146 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3147}31483149[State 8]3150{3151 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3152 pushFixed::push::inflight: Set((3, "a")),3153 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 1),3154 pushFixed::push::sent:3155 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3156}31573158[State 9]3159{3160 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3161 pushFixed::push::inflight: Set(),3162 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3163 pushFixed::push::sent:3164 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3165}31663167[ok] No violation found (89ms at 224719 traces/second).3168Trace length statistics: max=10, min=7, average=8.073169You may increase --max-samples and --max-steps.3170Use --verbosity to produce more (or less) output.3171Use --seed=0xa6dc1a12a0bad404 --backend=rust to reproduce.