nix-grpc-store-spec
checks.x86_64-linux.spec
· build #663
· raw
1tribuchet: building on jamie2An 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" -> CQueued),85 schedFixed::scheduler::crashes: 0,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", "c2"),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" -> CQueued, "c2" -> CQueued),124 schedFixed::scheduler::crashes: 1,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", "c2"),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" -> CQueued),163 schedFixed::scheduler::crashes: 1,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("c2"),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" -> CQueued),202 schedFixed::scheduler::crashes: 1,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("c1"),250 schedFixed::scheduler::mRevoke: Set(),251 schedFixed::scheduler::mSchedule: Set("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: false264 },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("c2"), leased: true, worker: "w2" }],283 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),284 schedFixed::scheduler::mAssigned: Set(("c2", "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("c1"),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: false,303 up: false304 },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("c2"), leased: true, worker: "w2" }],323 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),324 schedFixed::scheduler::mAssigned: Set(("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("c1"),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" -> CQueued, "c2" -> CSent("w2")),360 schedFixed::scheduler::crashes: 2,361 schedFixed::scheduler::entry:362 [{ followers: Set("c2"), leased: true, worker: "w2" }],363 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),364 schedFixed::scheduler::mAssigned: Set(),365 schedFixed::scheduler::mBuild: Set(("c2", "w2")),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" -> CQueued, "c2" -> CSent("w2")),400 schedFixed::scheduler::crashes: 2,401 schedFixed::scheduler::entry:402 [{ followers: Set("c2"), 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", "c2"),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("c2"), leased: true, worker: "w2" }],443 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),444 schedFixed::scheduler::mAssigned: Set(),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("c1"),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" -> CQueued, "c2" -> CQueued),480 schedFixed::scheduler::crashes: 2,481 schedFixed::scheduler::entry:482 [{ followers: Set("c2"), leased: true, worker: "w2" }],483 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),484 schedFixed::scheduler::mAssigned: Set(),485 schedFixed::scheduler::mBuild: Set(),486 schedFixed::scheduler::mDone: Set(),487 schedFixed::scheduler::mExpect: Set("w2"),488 schedFixed::scheduler::mResult: Set(),489 schedFixed::scheduler::mRetry: Set(),490 schedFixed::scheduler::mRevoke: Set(),491 schedFixed::scheduler::mSchedule: Set("c1", "c2"),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" -> CQueued, "c2" -> CQueued),520 schedFixed::scheduler::crashes: 2,521 schedFixed::scheduler::entry:522 [{ followers: Set("c2"), leased: true, worker: "w2" }],523 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),524 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),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(),530 schedFixed::scheduler::mRevoke: Set(),531 schedFixed::scheduler::mSchedule: Set("c1"),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("c2"), leased: true, worker: "w2" }],563 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),564 schedFixed::scheduler::mAssigned: Set(),565 schedFixed::scheduler::mBuild: Set(("c2", "w2")),566 schedFixed::scheduler::mDone: Set(),567 schedFixed::scheduler::mExpect: Set("w2"),568 schedFixed::scheduler::mResult: Set(),569 schedFixed::scheduler::mRetry: Set(),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(("c2", "w2")),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(),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" -> 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(("c1", "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("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" -> 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")),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("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(("c1", "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("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" -> CSent("w2"), "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("c1"),770 schedFixed::scheduler::mRevoke: Set(),771 schedFixed::scheduler::mSchedule: Set("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" -> CSent("w2"), "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("c1"),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" -> 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("w2"),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: false,870 running: false,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("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("w2"),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: 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(),966 schedFixed::scheduler::mDone: Set(),967 schedFixed::scheduler::mExpect: Set("w2"),968 schedFixed::scheduler::mResult: Set(),969 schedFixed::scheduler::mRetry: Set("c1"),970 schedFixed::scheduler::mRevoke: Set(),971 schedFixed::scheduler::mSchedule: Set(),972 schedFixed::scheduler::published: 0,973 schedFixed::scheduler::publishedBy: Set(),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: false,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" -> CSent("w2")),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(),1005 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1006 schedFixed::scheduler::mDone: Set(),1007 schedFixed::scheduler::mExpect: Set("w2"),1008 schedFixed::scheduler::mResult: Set(),1009 schedFixed::scheduler::mRetry: Set("c1"),1010 schedFixed::scheduler::mRevoke: Set(),1011 schedFixed::scheduler::mSchedule: Set(),1012 schedFixed::scheduler::published: 0,1013 schedFixed::scheduler::publishedBy: Set(),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: false,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" -> CSent("w2")),1040 schedFixed::scheduler::crashes: 2,1041 schedFixed::scheduler::entry:1042 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1043 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1044 schedFixed::scheduler::mAssigned: Set(),1045 schedFixed::scheduler::mBuild: Set(),1046 schedFixed::scheduler::mDone: Set(),1047 schedFixed::scheduler::mExpect: Set("w2"),1048 schedFixed::scheduler::mResult: Set(),1049 schedFixed::scheduler::mRetry: Set("c1", "c2"),1050 schedFixed::scheduler::mRevoke: Set(),1051 schedFixed::scheduler::mSchedule: Set(),1052 schedFixed::scheduler::published: 0,1053 schedFixed::scheduler::publishedBy: Set(),1054 schedFixed::scheduler::ws:1055 Map(1056 "w1" ->1057 {1058 attached: Set(),1059 built: false,1060 expecting: false,1061 running: false,1062 session: true,1063 up: true1064 },1065 "w2" ->1066 {1067 attached: Set(),1068 built: false,1069 expecting: false,1070 running: false,1071 session: true,1072 up: true1073 }1074 )1075}10761077[State 27]1078{1079 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),1080 schedFixed::scheduler::crashes: 2,1081 schedFixed::scheduler::entry:1082 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1083 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1084 schedFixed::scheduler::mAssigned: Set(),1085 schedFixed::scheduler::mBuild: Set(),1086 schedFixed::scheduler::mDone: Set(),1087 schedFixed::scheduler::mExpect: Set("w2"),1088 schedFixed::scheduler::mResult: Set(),1089 schedFixed::scheduler::mRetry: Set("c1"),1090 schedFixed::scheduler::mRevoke: Set(),1091 schedFixed::scheduler::mSchedule: Set("c2"),1092 schedFixed::scheduler::published: 0,1093 schedFixed::scheduler::publishedBy: Set(),1094 schedFixed::scheduler::ws:1095 Map(1096 "w1" ->1097 {1098 attached: Set(),1099 built: false,1100 expecting: false,1101 running: false,1102 session: true,1103 up: true1104 },1105 "w2" ->1106 {1107 attached: Set(),1108 built: false,1109 expecting: false,1110 running: false,1111 session: true,1112 up: true1113 }1114 )1115}11161117[State 28]1118{1119 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),1120 schedFixed::scheduler::crashes: 2,1121 schedFixed::scheduler::entry:1122 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1123 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1124 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1125 schedFixed::scheduler::mBuild: Set(),1126 schedFixed::scheduler::mDone: Set(),1127 schedFixed::scheduler::mExpect: Set("w2"),1128 schedFixed::scheduler::mResult: Set(),1129 schedFixed::scheduler::mRetry: Set("c1"),1130 schedFixed::scheduler::mRevoke: Set(),1131 schedFixed::scheduler::mSchedule: Set(),1132 schedFixed::scheduler::published: 0,1133 schedFixed::scheduler::publishedBy: Set(),1134 schedFixed::scheduler::ws:1135 Map(1136 "w1" ->1137 {1138 attached: Set(),1139 built: false,1140 expecting: false,1141 running: false,1142 session: true,1143 up: true1144 },1145 "w2" ->1146 {1147 attached: Set(),1148 built: false,1149 expecting: false,1150 running: false,1151 session: true,1152 up: true1153 }1154 )1155}11561157[State 29]1158{1159 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1160 schedFixed::scheduler::crashes: 2,1161 schedFixed::scheduler::entry:1162 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1163 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1164 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1165 schedFixed::scheduler::mBuild: Set(),1166 schedFixed::scheduler::mDone: Set(),1167 schedFixed::scheduler::mExpect: Set("w2"),1168 schedFixed::scheduler::mResult: Set(),1169 schedFixed::scheduler::mRetry: Set(),1170 schedFixed::scheduler::mRevoke: Set(),1171 schedFixed::scheduler::mSchedule: Set("c1"),1172 schedFixed::scheduler::published: 0,1173 schedFixed::scheduler::publishedBy: Set(),1174 schedFixed::scheduler::ws:1175 Map(1176 "w1" ->1177 {1178 attached: Set(),1179 built: false,1180 expecting: false,1181 running: false,1182 session: true,1183 up: true1184 },1185 "w2" ->1186 {1187 attached: Set(),1188 built: false,1189 expecting: false,1190 running: false,1191 session: true,1192 up: true1193 }1194 )1195}11961197[State 30]1198{1199 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1200 schedFixed::scheduler::crashes: 2,1201 schedFixed::scheduler::entry:1202 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1203 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1204 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1205 schedFixed::scheduler::mBuild: Set(),1206 schedFixed::scheduler::mDone: Set(),1207 schedFixed::scheduler::mExpect: Set(),1208 schedFixed::scheduler::mResult: Set(),1209 schedFixed::scheduler::mRetry: Set(),1210 schedFixed::scheduler::mRevoke: Set(),1211 schedFixed::scheduler::mSchedule: Set("c1"),1212 schedFixed::scheduler::published: 0,1213 schedFixed::scheduler::publishedBy: Set(),1214 schedFixed::scheduler::ws:1215 Map(1216 "w1" ->1217 {1218 attached: Set(),1219 built: false,1220 expecting: false,1221 running: false,1222 session: true,1223 up: true1224 },1225 "w2" ->1226 {1227 attached: Set(),1228 built: false,1229 expecting: true,1230 running: true,1231 session: true,1232 up: true1233 }1234 )1235}12361237[ok] No violation found (485ms at 61856 traces/second).1238Trace length statistics: max=26, min=16, average=18.721239You may increase --max-samples and --max-steps.1240Use --verbosity to produce more (or less) output.1241Use --seed=0xa893584319a50976 --backend=rust to reproduce.1242An example execution:12431244[State 0]1245{1246 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1247 schedNoRevoke::scheduler::crashes: 0,1248 schedNoRevoke::scheduler::entry: [],1249 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1250 schedNoRevoke::scheduler::mAssigned: Set(),1251 schedNoRevoke::scheduler::mBuild: Set(),1252 schedNoRevoke::scheduler::mDone: Set(),1253 schedNoRevoke::scheduler::mExpect: Set(),1254 schedNoRevoke::scheduler::mResult: Set(),1255 schedNoRevoke::scheduler::mRetry: Set(),1256 schedNoRevoke::scheduler::mRevoke: Set(),1257 schedNoRevoke::scheduler::mSchedule: Set(),1258 schedNoRevoke::scheduler::published: 0,1259 schedNoRevoke::scheduler::publishedBy: Set(),1260 schedNoRevoke::scheduler::ws:1261 Map(1262 "w1" ->1263 {1264 attached: Set(),1265 built: false,1266 expecting: false,1267 running: false,1268 session: true,1269 up: true1270 },1271 "w2" ->1272 {1273 attached: Set(),1274 built: false,1275 expecting: false,1276 running: false,1277 session: true,1278 up: true1279 }1280 )1281}12821283[State 1]1284{1285 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1286 schedNoRevoke::scheduler::crashes: 0,1287 schedNoRevoke::scheduler::entry: [],1288 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1289 schedNoRevoke::scheduler::mAssigned: Set(),1290 schedNoRevoke::scheduler::mBuild: Set(),1291 schedNoRevoke::scheduler::mDone: Set(),1292 schedNoRevoke::scheduler::mExpect: Set(),1293 schedNoRevoke::scheduler::mResult: Set(),1294 schedNoRevoke::scheduler::mRetry: Set(),1295 schedNoRevoke::scheduler::mRevoke: Set(),1296 schedNoRevoke::scheduler::mSchedule: Set("c2"),1297 schedNoRevoke::scheduler::published: 0,1298 schedNoRevoke::scheduler::publishedBy: Set(),1299 schedNoRevoke::scheduler::ws:1300 Map(1301 "w1" ->1302 {1303 attached: Set(),1304 built: false,1305 expecting: false,1306 running: false,1307 session: true,1308 up: true1309 },1310 "w2" ->1311 {1312 attached: Set(),1313 built: false,1314 expecting: false,1315 running: false,1316 session: true,1317 up: true1318 }1319 )1320}13211322[State 2]1323{1324 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1325 schedNoRevoke::scheduler::crashes: 0,1326 schedNoRevoke::scheduler::entry:1327 [{ followers: Set("c2"), leased: true, worker: "w1" }],1328 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1329 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1330 schedNoRevoke::scheduler::mBuild: Set(),1331 schedNoRevoke::scheduler::mDone: Set(),1332 schedNoRevoke::scheduler::mExpect: Set("w1"),1333 schedNoRevoke::scheduler::mResult: Set(),1334 schedNoRevoke::scheduler::mRetry: Set(),1335 schedNoRevoke::scheduler::mRevoke: Set(),1336 schedNoRevoke::scheduler::mSchedule: Set(),1337 schedNoRevoke::scheduler::published: 0,1338 schedNoRevoke::scheduler::publishedBy: Set(),1339 schedNoRevoke::scheduler::ws:1340 Map(1341 "w1" ->1342 {1343 attached: Set(),1344 built: false,1345 expecting: false,1346 running: false,1347 session: true,1348 up: true1349 },1350 "w2" ->1351 {1352 attached: Set(),1353 built: false,1354 expecting: false,1355 running: false,1356 session: true,1357 up: true1358 }1359 )1360}13611362[State 3]1363{1364 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1365 schedNoRevoke::scheduler::crashes: 0,1366 schedNoRevoke::scheduler::entry:1367 [{ followers: Set("c2"), leased: true, worker: "w1" }],1368 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1369 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1370 schedNoRevoke::scheduler::mBuild: Set(),1371 schedNoRevoke::scheduler::mDone: Set(),1372 schedNoRevoke::scheduler::mExpect: Set(),1373 schedNoRevoke::scheduler::mResult: Set(),1374 schedNoRevoke::scheduler::mRetry: Set(),1375 schedNoRevoke::scheduler::mRevoke: Set(),1376 schedNoRevoke::scheduler::mSchedule: Set(),1377 schedNoRevoke::scheduler::published: 0,1378 schedNoRevoke::scheduler::publishedBy: Set(),1379 schedNoRevoke::scheduler::ws:1380 Map(1381 "w1" ->1382 {1383 attached: Set(),1384 built: false,1385 expecting: true,1386 running: true,1387 session: true,1388 up: true1389 },1390 "w2" ->1391 {1392 attached: Set(),1393 built: false,1394 expecting: false,1395 running: false,1396 session: true,1397 up: true1398 }1399 )1400}14011402[State 4]1403{1404 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1405 schedNoRevoke::scheduler::crashes: 1,1406 schedNoRevoke::scheduler::entry: [],1407 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1408 schedNoRevoke::scheduler::mAssigned: Set(),1409 schedNoRevoke::scheduler::mBuild: Set(),1410 schedNoRevoke::scheduler::mDone: Set(),1411 schedNoRevoke::scheduler::mExpect: Set(),1412 schedNoRevoke::scheduler::mResult: Set(),1413 schedNoRevoke::scheduler::mRetry: Set("c2"),1414 schedNoRevoke::scheduler::mRevoke: Set(),1415 schedNoRevoke::scheduler::mSchedule: Set(),1416 schedNoRevoke::scheduler::published: 0,1417 schedNoRevoke::scheduler::publishedBy: Set(),1418 schedNoRevoke::scheduler::ws:1419 Map(1420 "w1" ->1421 {1422 attached: Set(),1423 built: false,1424 expecting: true,1425 running: true,1426 session: false,1427 up: true1428 },1429 "w2" ->1430 {1431 attached: Set(),1432 built: false,1433 expecting: false,1434 running: false,1435 session: false,1436 up: true1437 }1438 )1439}14401441[State 5]1442{1443 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1444 schedNoRevoke::scheduler::crashes: 2,1445 schedNoRevoke::scheduler::entry: [],1446 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1447 schedNoRevoke::scheduler::mAssigned: Set(),1448 schedNoRevoke::scheduler::mBuild: Set(),1449 schedNoRevoke::scheduler::mDone: Set(),1450 schedNoRevoke::scheduler::mExpect: Set(),1451 schedNoRevoke::scheduler::mResult: Set(),1452 schedNoRevoke::scheduler::mRetry: Set("c2"),1453 schedNoRevoke::scheduler::mRevoke: Set(),1454 schedNoRevoke::scheduler::mSchedule: Set(),1455 schedNoRevoke::scheduler::published: 0,1456 schedNoRevoke::scheduler::publishedBy: Set(),1457 schedNoRevoke::scheduler::ws:1458 Map(1459 "w1" ->1460 {1461 attached: Set(),1462 built: false,1463 expecting: true,1464 running: true,1465 session: false,1466 up: true1467 },1468 "w2" ->1469 {1470 attached: Set(),1471 built: false,1472 expecting: false,1473 running: false,1474 session: false,1475 up: true1476 }1477 )1478}14791480[State 6]1481{1482 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1483 schedNoRevoke::scheduler::crashes: 2,1484 schedNoRevoke::scheduler::entry: [],1485 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1486 schedNoRevoke::scheduler::mAssigned: Set(),1487 schedNoRevoke::scheduler::mBuild: Set(),1488 schedNoRevoke::scheduler::mDone: Set(),1489 schedNoRevoke::scheduler::mExpect: Set(),1490 schedNoRevoke::scheduler::mResult: Set(),1491 schedNoRevoke::scheduler::mRetry: Set("c2"),1492 schedNoRevoke::scheduler::mRevoke: Set(),1493 schedNoRevoke::scheduler::mSchedule: Set(),1494 schedNoRevoke::scheduler::published: 0,1495 schedNoRevoke::scheduler::publishedBy: Set(),1496 schedNoRevoke::scheduler::ws:1497 Map(1498 "w1" ->1499 {1500 attached: Set(),1501 built: false,1502 expecting: true,1503 running: true,1504 session: false,1505 up: true1506 },1507 "w2" ->1508 {1509 attached: Set(),1510 built: false,1511 expecting: false,1512 running: false,1513 session: true,1514 up: true1515 }1516 )1517}15181519[State 7]1520{1521 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1522 schedNoRevoke::scheduler::crashes: 2,1523 schedNoRevoke::scheduler::entry: [],1524 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1525 schedNoRevoke::scheduler::mAssigned: Set(),1526 schedNoRevoke::scheduler::mBuild: Set(),1527 schedNoRevoke::scheduler::mDone: Set(),1528 schedNoRevoke::scheduler::mExpect: Set(),1529 schedNoRevoke::scheduler::mResult: Set(),1530 schedNoRevoke::scheduler::mRetry: Set(),1531 schedNoRevoke::scheduler::mRevoke: Set(),1532 schedNoRevoke::scheduler::mSchedule: Set("c2"),1533 schedNoRevoke::scheduler::published: 0,1534 schedNoRevoke::scheduler::publishedBy: Set(),1535 schedNoRevoke::scheduler::ws:1536 Map(1537 "w1" ->1538 {1539 attached: Set(),1540 built: false,1541 expecting: true,1542 running: true,1543 session: false,1544 up: true1545 },1546 "w2" ->1547 {1548 attached: Set(),1549 built: false,1550 expecting: false,1551 running: false,1552 session: true,1553 up: true1554 }1555 )1556}15571558[State 8]1559{1560 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1561 schedNoRevoke::scheduler::crashes: 2,1562 schedNoRevoke::scheduler::entry: [],1563 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1564 schedNoRevoke::scheduler::mAssigned: Set(),1565 schedNoRevoke::scheduler::mBuild: Set(),1566 schedNoRevoke::scheduler::mDone: Set(),1567 schedNoRevoke::scheduler::mExpect: Set(),1568 schedNoRevoke::scheduler::mResult: Set(),1569 schedNoRevoke::scheduler::mRetry: Set(),1570 schedNoRevoke::scheduler::mRevoke: Set(),1571 schedNoRevoke::scheduler::mSchedule: Set("c1", "c2"),1572 schedNoRevoke::scheduler::published: 0,1573 schedNoRevoke::scheduler::publishedBy: Set(),1574 schedNoRevoke::scheduler::ws:1575 Map(1576 "w1" ->1577 {1578 attached: Set(),1579 built: false,1580 expecting: true,1581 running: true,1582 session: false,1583 up: true1584 },1585 "w2" ->1586 {1587 attached: Set(),1588 built: false,1589 expecting: false,1590 running: false,1591 session: true,1592 up: true1593 }1594 )1595}15961597[State 9]1598{1599 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1600 schedNoRevoke::scheduler::crashes: 2,1601 schedNoRevoke::scheduler::entry:1602 [{ followers: Set("c1"), leased: true, worker: "w2" }],1603 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1604 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1605 schedNoRevoke::scheduler::mBuild: Set(),1606 schedNoRevoke::scheduler::mDone: Set(),1607 schedNoRevoke::scheduler::mExpect: Set("w2"),1608 schedNoRevoke::scheduler::mResult: Set(),1609 schedNoRevoke::scheduler::mRetry: Set(),1610 schedNoRevoke::scheduler::mRevoke: Set(),1611 schedNoRevoke::scheduler::mSchedule: Set("c2"),1612 schedNoRevoke::scheduler::published: 0,1613 schedNoRevoke::scheduler::publishedBy: Set(),1614 schedNoRevoke::scheduler::ws:1615 Map(1616 "w1" ->1617 {1618 attached: Set(),1619 built: false,1620 expecting: true,1621 running: true,1622 session: false,1623 up: true1624 },1625 "w2" ->1626 {1627 attached: Set(),1628 built: false,1629 expecting: false,1630 running: false,1631 session: true,1632 up: true1633 }1634 )1635}16361637[State 10]1638{1639 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1640 schedNoRevoke::scheduler::crashes: 2,1641 schedNoRevoke::scheduler::entry:1642 [{ followers: Set("c1"), leased: true, worker: "w2" }],1643 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1644 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1645 schedNoRevoke::scheduler::mBuild: Set(),1646 schedNoRevoke::scheduler::mDone: Set(),1647 schedNoRevoke::scheduler::mExpect: Set(),1648 schedNoRevoke::scheduler::mResult: Set(),1649 schedNoRevoke::scheduler::mRetry: Set(),1650 schedNoRevoke::scheduler::mRevoke: Set(),1651 schedNoRevoke::scheduler::mSchedule: Set("c2"),1652 schedNoRevoke::scheduler::published: 0,1653 schedNoRevoke::scheduler::publishedBy: Set(),1654 schedNoRevoke::scheduler::ws:1655 Map(1656 "w1" ->1657 {1658 attached: Set(),1659 built: false,1660 expecting: true,1661 running: true,1662 session: false,1663 up: true1664 },1665 "w2" ->1666 {1667 attached: Set(),1668 built: false,1669 expecting: true,1670 running: true,1671 session: true,1672 up: true1673 }1674 )1675}16761677[State 11]1678{1679 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1680 schedNoRevoke::scheduler::crashes: 2,1681 schedNoRevoke::scheduler::entry:1682 [{ followers: Set("c1"), leased: true, worker: "w2" }],1683 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1684 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1685 schedNoRevoke::scheduler::mBuild: Set(),1686 schedNoRevoke::scheduler::mDone: Set(),1687 schedNoRevoke::scheduler::mExpect: Set(),1688 schedNoRevoke::scheduler::mResult: Set(),1689 schedNoRevoke::scheduler::mRetry: Set(),1690 schedNoRevoke::scheduler::mRevoke: Set(),1691 schedNoRevoke::scheduler::mSchedule: Set("c2"),1692 schedNoRevoke::scheduler::published: 0,1693 schedNoRevoke::scheduler::publishedBy: Set(),1694 schedNoRevoke::scheduler::ws:1695 Map(1696 "w1" ->1697 {1698 attached: Set(),1699 built: false,1700 expecting: true,1701 running: true,1702 session: true,1703 up: true1704 },1705 "w2" ->1706 {1707 attached: Set(),1708 built: false,1709 expecting: true,1710 running: true,1711 session: true,1712 up: true1713 }1714 )1715}17161717[violation] Found an issue (499ms at 58160 traces/second).1718Use --verbosity=3 to show executions.1719Use --seed=0xbd746800ad65d9de --backend=rust to reproduce.1720error: Invariant violated1721An example execution:17221723[State 0]1724{1725 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1726 schedNoFence::scheduler::crashes: 0,1727 schedNoFence::scheduler::entry: [],1728 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1729 schedNoFence::scheduler::mAssigned: Set(),1730 schedNoFence::scheduler::mBuild: Set(),1731 schedNoFence::scheduler::mDone: Set(),1732 schedNoFence::scheduler::mExpect: Set(),1733 schedNoFence::scheduler::mResult: Set(),1734 schedNoFence::scheduler::mRetry: Set(),1735 schedNoFence::scheduler::mRevoke: Set(),1736 schedNoFence::scheduler::mSchedule: Set(),1737 schedNoFence::scheduler::published: 0,1738 schedNoFence::scheduler::publishedBy: Set(),1739 schedNoFence::scheduler::ws:1740 Map(1741 "w1" ->1742 {1743 attached: Set(),1744 built: false,1745 expecting: false,1746 running: false,1747 session: true,1748 up: true1749 },1750 "w2" ->1751 {1752 attached: Set(),1753 built: false,1754 expecting: false,1755 running: false,1756 session: true,1757 up: true1758 }1759 )1760}17611762[State 1]1763{1764 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1765 schedNoFence::scheduler::crashes: 0,1766 schedNoFence::scheduler::entry: [],1767 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1768 schedNoFence::scheduler::mAssigned: Set(),1769 schedNoFence::scheduler::mBuild: Set(),1770 schedNoFence::scheduler::mDone: Set(),1771 schedNoFence::scheduler::mExpect: Set(),1772 schedNoFence::scheduler::mResult: Set(),1773 schedNoFence::scheduler::mRetry: Set(),1774 schedNoFence::scheduler::mRevoke: Set(),1775 schedNoFence::scheduler::mSchedule: Set("c1"),1776 schedNoFence::scheduler::published: 0,1777 schedNoFence::scheduler::publishedBy: Set(),1778 schedNoFence::scheduler::ws:1779 Map(1780 "w1" ->1781 {1782 attached: Set(),1783 built: false,1784 expecting: false,1785 running: false,1786 session: true,1787 up: true1788 },1789 "w2" ->1790 {1791 attached: Set(),1792 built: false,1793 expecting: false,1794 running: false,1795 session: true,1796 up: true1797 }1798 )1799}18001801[State 2]1802{1803 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1804 schedNoFence::scheduler::crashes: 1,1805 schedNoFence::scheduler::entry: [],1806 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1807 schedNoFence::scheduler::mAssigned: Set(),1808 schedNoFence::scheduler::mBuild: Set(),1809 schedNoFence::scheduler::mDone: Set(),1810 schedNoFence::scheduler::mExpect: Set(),1811 schedNoFence::scheduler::mResult: Set(),1812 schedNoFence::scheduler::mRetry: Set(),1813 schedNoFence::scheduler::mRevoke: Set(),1814 schedNoFence::scheduler::mSchedule: Set("c1"),1815 schedNoFence::scheduler::published: 0,1816 schedNoFence::scheduler::publishedBy: Set(),1817 schedNoFence::scheduler::ws:1818 Map(1819 "w1" ->1820 {1821 attached: Set(),1822 built: false,1823 expecting: false,1824 running: false,1825 session: false,1826 up: false1827 },1828 "w2" ->1829 {1830 attached: Set(),1831 built: false,1832 expecting: false,1833 running: false,1834 session: true,1835 up: true1836 }1837 )1838}18391840[State 3]1841{1842 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1843 schedNoFence::scheduler::crashes: 1,1844 schedNoFence::scheduler::entry:1845 [{ followers: Set("c1"), leased: true, worker: "w2" }],1846 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1847 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),1848 schedNoFence::scheduler::mBuild: Set(),1849 schedNoFence::scheduler::mDone: Set(),1850 schedNoFence::scheduler::mExpect: Set("w2"),1851 schedNoFence::scheduler::mResult: Set(),1852 schedNoFence::scheduler::mRetry: Set(),1853 schedNoFence::scheduler::mRevoke: Set(),1854 schedNoFence::scheduler::mSchedule: Set(),1855 schedNoFence::scheduler::published: 0,1856 schedNoFence::scheduler::publishedBy: Set(),1857 schedNoFence::scheduler::ws:1858 Map(1859 "w1" ->1860 {1861 attached: Set(),1862 built: false,1863 expecting: false,1864 running: false,1865 session: false,1866 up: false1867 },1868 "w2" ->1869 {1870 attached: Set(),1871 built: false,1872 expecting: false,1873 running: false,1874 session: true,1875 up: true1876 }1877 )1878}18791880[State 4]1881{1882 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1883 schedNoFence::scheduler::crashes: 1,1884 schedNoFence::scheduler::entry:1885 [{ followers: Set("c1"), leased: true, worker: "w2" }],1886 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1887 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),1888 schedNoFence::scheduler::mBuild: Set(),1889 schedNoFence::scheduler::mDone: Set(),1890 schedNoFence::scheduler::mExpect: Set(),1891 schedNoFence::scheduler::mResult: Set(),1892 schedNoFence::scheduler::mRetry: Set(),1893 schedNoFence::scheduler::mRevoke: Set(),1894 schedNoFence::scheduler::mSchedule: Set(),1895 schedNoFence::scheduler::published: 0,1896 schedNoFence::scheduler::publishedBy: Set(),1897 schedNoFence::scheduler::ws:1898 Map(1899 "w1" ->1900 {1901 attached: Set(),1902 built: false,1903 expecting: false,1904 running: false,1905 session: false,1906 up: false1907 },1908 "w2" ->1909 {1910 attached: Set(),1911 built: false,1912 expecting: true,1913 running: true,1914 session: true,1915 up: true1916 }1917 )1918}19191920[State 5]1921{1922 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1923 schedNoFence::scheduler::crashes: 2,1924 schedNoFence::scheduler::entry: [],1925 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1926 schedNoFence::scheduler::mAssigned: Set(),1927 schedNoFence::scheduler::mBuild: Set(),1928 schedNoFence::scheduler::mDone: Set(),1929 schedNoFence::scheduler::mExpect: Set(),1930 schedNoFence::scheduler::mResult: Set(),1931 schedNoFence::scheduler::mRetry: Set("c1"),1932 schedNoFence::scheduler::mRevoke: Set(),1933 schedNoFence::scheduler::mSchedule: Set(),1934 schedNoFence::scheduler::published: 0,1935 schedNoFence::scheduler::publishedBy: Set(),1936 schedNoFence::scheduler::ws:1937 Map(1938 "w1" ->1939 {1940 attached: Set(),1941 built: false,1942 expecting: false,1943 running: false,1944 session: false,1945 up: false1946 },1947 "w2" ->1948 {1949 attached: Set(),1950 built: false,1951 expecting: true,1952 running: true,1953 session: false,1954 up: true1955 }1956 )1957}19581959[State 6]1960{1961 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1962 schedNoFence::scheduler::crashes: 2,1963 schedNoFence::scheduler::entry: [],1964 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1965 schedNoFence::scheduler::mAssigned: Set(),1966 schedNoFence::scheduler::mBuild: Set(),1967 schedNoFence::scheduler::mDone: Set(),1968 schedNoFence::scheduler::mExpect: Set(),1969 schedNoFence::scheduler::mResult: Set(),1970 schedNoFence::scheduler::mRetry: Set("c1"),1971 schedNoFence::scheduler::mRevoke: Set(),1972 schedNoFence::scheduler::mSchedule: Set(),1973 schedNoFence::scheduler::published: 0,1974 schedNoFence::scheduler::publishedBy: Set(),1975 schedNoFence::scheduler::ws:1976 Map(1977 "w1" ->1978 {1979 attached: Set(),1980 built: false,1981 expecting: false,1982 running: false,1983 session: true,1984 up: true1985 },1986 "w2" ->1987 {1988 attached: Set(),1989 built: false,1990 expecting: true,1991 running: true,1992 session: false,1993 up: true1994 }1995 )1996}19971998[State 7]1999{2000 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2001 schedNoFence::scheduler::crashes: 2,2002 schedNoFence::scheduler::entry: [],2003 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),2004 schedNoFence::scheduler::mAssigned: Set(),2005 schedNoFence::scheduler::mBuild: Set(),2006 schedNoFence::scheduler::mDone: Set(),2007 schedNoFence::scheduler::mExpect: Set(),2008 schedNoFence::scheduler::mResult: Set(),2009 schedNoFence::scheduler::mRetry: Set("c1"),2010 schedNoFence::scheduler::mRevoke: Set(),2011 schedNoFence::scheduler::mSchedule: Set("c2"),2012 schedNoFence::scheduler::published: 0,2013 schedNoFence::scheduler::publishedBy: Set(),2014 schedNoFence::scheduler::ws:2015 Map(2016 "w1" ->2017 {2018 attached: Set(),2019 built: false,2020 expecting: false,2021 running: false,2022 session: true,2023 up: true2024 },2025 "w2" ->2026 {2027 attached: Set(),2028 built: false,2029 expecting: true,2030 running: true,2031 session: false,2032 up: true2033 }2034 )2035}20362037[State 8]2038{2039 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2040 schedNoFence::scheduler::crashes: 2,2041 schedNoFence::scheduler::entry:2042 [{ followers: Set("c2"), leased: true, worker: "w1" }],2043 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2044 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2045 schedNoFence::scheduler::mBuild: Set(),2046 schedNoFence::scheduler::mDone: Set(),2047 schedNoFence::scheduler::mExpect: Set("w1"),2048 schedNoFence::scheduler::mResult: Set(),2049 schedNoFence::scheduler::mRetry: Set("c1"),2050 schedNoFence::scheduler::mRevoke: Set(),2051 schedNoFence::scheduler::mSchedule: Set(),2052 schedNoFence::scheduler::published: 0,2053 schedNoFence::scheduler::publishedBy: Set(),2054 schedNoFence::scheduler::ws:2055 Map(2056 "w1" ->2057 {2058 attached: Set(),2059 built: false,2060 expecting: false,2061 running: false,2062 session: true,2063 up: true2064 },2065 "w2" ->2066 {2067 attached: Set(),2068 built: false,2069 expecting: true,2070 running: true,2071 session: false,2072 up: true2073 }2074 )2075}20762077[State 9]2078{2079 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2080 schedNoFence::scheduler::crashes: 2,2081 schedNoFence::scheduler::entry:2082 [{ followers: Set("c2"), leased: true, worker: "w1" }],2083 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2084 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2085 schedNoFence::scheduler::mBuild: Set(),2086 schedNoFence::scheduler::mDone: Set(),2087 schedNoFence::scheduler::mExpect: Set("w1"),2088 schedNoFence::scheduler::mResult: Set(),2089 schedNoFence::scheduler::mRetry: Set("c1"),2090 schedNoFence::scheduler::mRevoke: Set(),2091 schedNoFence::scheduler::mSchedule: Set(),2092 schedNoFence::scheduler::published: 1,2093 schedNoFence::scheduler::publishedBy: Set("w2"),2094 schedNoFence::scheduler::ws:2095 Map(2096 "w1" ->2097 {2098 attached: Set(),2099 built: false,2100 expecting: false,2101 running: false,2102 session: true,2103 up: true2104 },2105 "w2" ->2106 {2107 attached: Set(),2108 built: true,2109 expecting: false,2110 running: false,2111 session: false,2112 up: true2113 }2114 )2115}21162117[State 10]2118{2119 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2120 schedNoFence::scheduler::crashes: 2,2121 schedNoFence::scheduler::entry:2122 [{ followers: Set("c2"), leased: true, worker: "w1" }],2123 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2124 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2125 schedNoFence::scheduler::mBuild: Set(),2126 schedNoFence::scheduler::mDone: Set(),2127 schedNoFence::scheduler::mExpect: Set("w1"),2128 schedNoFence::scheduler::mResult: Set(),2129 schedNoFence::scheduler::mRetry: Set("c1"),2130 schedNoFence::scheduler::mRevoke: Set(),2131 schedNoFence::scheduler::mSchedule: Set(),2132 schedNoFence::scheduler::published: 1,2133 schedNoFence::scheduler::publishedBy: Set("w2"),2134 schedNoFence::scheduler::ws:2135 Map(2136 "w1" ->2137 {2138 attached: Set(),2139 built: false,2140 expecting: false,2141 running: false,2142 session: true,2143 up: true2144 },2145 "w2" ->2146 {2147 attached: Set(),2148 built: true,2149 expecting: false,2150 running: false,2151 session: true,2152 up: true2153 }2154 )2155}21562157[State 11]2158{2159 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2160 schedNoFence::scheduler::crashes: 2,2161 schedNoFence::scheduler::entry:2162 [{ followers: Set("c2"), leased: true, worker: "w1" }],2163 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2164 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2165 schedNoFence::scheduler::mBuild: Set(),2166 schedNoFence::scheduler::mDone: Set(),2167 schedNoFence::scheduler::mExpect: Set(),2168 schedNoFence::scheduler::mResult: Set(),2169 schedNoFence::scheduler::mRetry: Set("c1"),2170 schedNoFence::scheduler::mRevoke: Set(),2171 schedNoFence::scheduler::mSchedule: Set(),2172 schedNoFence::scheduler::published: 1,2173 schedNoFence::scheduler::publishedBy: Set("w2"),2174 schedNoFence::scheduler::ws:2175 Map(2176 "w1" ->2177 {2178 attached: Set(),2179 built: false,2180 expecting: true,2181 running: true,2182 session: true,2183 up: true2184 },2185 "w2" ->2186 {2187 attached: Set(),2188 built: true,2189 expecting: false,2190 running: false,2191 session: true,2192 up: true2193 }2194 )2195}21962197[State 12]2198{2199 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2200 schedNoFence::scheduler::crashes: 2,2201 schedNoFence::scheduler::entry:2202 [{ followers: Set("c2"), leased: true, worker: "w1" }],2203 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2204 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2205 schedNoFence::scheduler::mBuild: Set(),2206 schedNoFence::scheduler::mDone: Set("w1"),2207 schedNoFence::scheduler::mExpect: Set(),2208 schedNoFence::scheduler::mResult: Set(),2209 schedNoFence::scheduler::mRetry: Set("c1"),2210 schedNoFence::scheduler::mRevoke: Set(),2211 schedNoFence::scheduler::mSchedule: Set(),2212 schedNoFence::scheduler::published: 2,2213 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2214 schedNoFence::scheduler::ws:2215 Map(2216 "w1" ->2217 {2218 attached: Set(),2219 built: true,2220 expecting: false,2221 running: false,2222 session: true,2223 up: true2224 },2225 "w2" ->2226 {2227 attached: Set(),2228 built: true,2229 expecting: false,2230 running: false,2231 session: true,2232 up: true2233 }2234 )2235}22362237[violation] Found an issue (455ms at 60387 traces/second).2238Use --verbosity=3 to show executions.2239Use --seed=0xd34a9ffdadb6c093 --backend=rust to reproduce.2240error: Invariant violated2241An example execution:22422243[State 0]2244{2245 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2246 schedNoPush::scheduler::crashes: 0,2247 schedNoPush::scheduler::entry: [],2248 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2249 schedNoPush::scheduler::mAssigned: Set(),2250 schedNoPush::scheduler::mBuild: Set(),2251 schedNoPush::scheduler::mDone: Set(),2252 schedNoPush::scheduler::mExpect: Set(),2253 schedNoPush::scheduler::mResult: Set(),2254 schedNoPush::scheduler::mRetry: Set(),2255 schedNoPush::scheduler::mRevoke: Set(),2256 schedNoPush::scheduler::mSchedule: Set(),2257 schedNoPush::scheduler::published: 0,2258 schedNoPush::scheduler::publishedBy: Set(),2259 schedNoPush::scheduler::ws:2260 Map(2261 "w1" ->2262 {2263 attached: Set(),2264 built: false,2265 expecting: false,2266 running: false,2267 session: true,2268 up: true2269 },2270 "w2" ->2271 {2272 attached: Set(),2273 built: false,2274 expecting: false,2275 running: false,2276 session: true,2277 up: true2278 }2279 )2280}22812282[State 1]2283{2284 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2285 schedNoPush::scheduler::crashes: 0,2286 schedNoPush::scheduler::entry: [],2287 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2288 schedNoPush::scheduler::mAssigned: Set(),2289 schedNoPush::scheduler::mBuild: Set(),2290 schedNoPush::scheduler::mDone: Set(),2291 schedNoPush::scheduler::mExpect: Set(),2292 schedNoPush::scheduler::mResult: Set(),2293 schedNoPush::scheduler::mRetry: Set(),2294 schedNoPush::scheduler::mRevoke: Set(),2295 schedNoPush::scheduler::mSchedule: Set("c1"),2296 schedNoPush::scheduler::published: 0,2297 schedNoPush::scheduler::publishedBy: Set(),2298 schedNoPush::scheduler::ws:2299 Map(2300 "w1" ->2301 {2302 attached: Set(),2303 built: false,2304 expecting: false,2305 running: false,2306 session: true,2307 up: true2308 },2309 "w2" ->2310 {2311 attached: Set(),2312 built: false,2313 expecting: false,2314 running: false,2315 session: true,2316 up: true2317 }2318 )2319}23202321[State 2]2322{2323 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2324 schedNoPush::scheduler::crashes: 0,2325 schedNoPush::scheduler::entry:2326 [{ followers: Set("c1"), leased: true, worker: "w2" }],2327 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2328 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2329 schedNoPush::scheduler::mBuild: Set(),2330 schedNoPush::scheduler::mDone: Set(),2331 schedNoPush::scheduler::mExpect: Set(),2332 schedNoPush::scheduler::mResult: Set(),2333 schedNoPush::scheduler::mRetry: Set(),2334 schedNoPush::scheduler::mRevoke: Set(),2335 schedNoPush::scheduler::mSchedule: Set(),2336 schedNoPush::scheduler::published: 0,2337 schedNoPush::scheduler::publishedBy: Set(),2338 schedNoPush::scheduler::ws:2339 Map(2340 "w1" ->2341 {2342 attached: Set(),2343 built: false,2344 expecting: false,2345 running: false,2346 session: true,2347 up: true2348 },2349 "w2" ->2350 {2351 attached: Set(),2352 built: false,2353 expecting: false,2354 running: false,2355 session: true,2356 up: true2357 }2358 )2359}23602361[State 3]2362{2363 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2364 schedNoPush::scheduler::crashes: 1,2365 schedNoPush::scheduler::entry:2366 [{ followers: Set("c1"), leased: true, worker: "w2" }],2367 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2368 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2369 schedNoPush::scheduler::mBuild: Set(),2370 schedNoPush::scheduler::mDone: Set(),2371 schedNoPush::scheduler::mExpect: Set(),2372 schedNoPush::scheduler::mResult: Set(),2373 schedNoPush::scheduler::mRetry: Set(),2374 schedNoPush::scheduler::mRevoke: Set(),2375 schedNoPush::scheduler::mSchedule: Set(),2376 schedNoPush::scheduler::published: 0,2377 schedNoPush::scheduler::publishedBy: Set(),2378 schedNoPush::scheduler::ws:2379 Map(2380 "w1" ->2381 {2382 attached: Set(),2383 built: false,2384 expecting: false,2385 running: false,2386 session: true,2387 up: true2388 },2389 "w2" ->2390 {2391 attached: Set(),2392 built: false,2393 expecting: false,2394 running: false,2395 session: false,2396 up: false2397 }2398 )2399}24002401[State 4]2402{2403 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2404 schedNoPush::scheduler::crashes: 1,2405 schedNoPush::scheduler::entry:2406 [{ followers: Set("c1"), leased: true, worker: "w2" }],2407 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2408 schedNoPush::scheduler::mAssigned: Set(),2409 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2410 schedNoPush::scheduler::mDone: Set(),2411 schedNoPush::scheduler::mExpect: Set(),2412 schedNoPush::scheduler::mResult: Set(),2413 schedNoPush::scheduler::mRetry: Set(),2414 schedNoPush::scheduler::mRevoke: Set(),2415 schedNoPush::scheduler::mSchedule: Set(),2416 schedNoPush::scheduler::published: 0,2417 schedNoPush::scheduler::publishedBy: Set(),2418 schedNoPush::scheduler::ws:2419 Map(2420 "w1" ->2421 {2422 attached: Set(),2423 built: false,2424 expecting: false,2425 running: false,2426 session: true,2427 up: true2428 },2429 "w2" ->2430 {2431 attached: Set(),2432 built: false,2433 expecting: false,2434 running: false,2435 session: false,2436 up: false2437 }2438 )2439}24402441[State 5]2442{2443 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2444 schedNoPush::scheduler::crashes: 1,2445 schedNoPush::scheduler::entry: [],2446 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2447 schedNoPush::scheduler::mAssigned: Set(),2448 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2449 schedNoPush::scheduler::mDone: Set(),2450 schedNoPush::scheduler::mExpect: Set(),2451 schedNoPush::scheduler::mResult: Set(),2452 schedNoPush::scheduler::mRetry: Set("c1"),2453 schedNoPush::scheduler::mRevoke: Set(),2454 schedNoPush::scheduler::mSchedule: Set(),2455 schedNoPush::scheduler::published: 0,2456 schedNoPush::scheduler::publishedBy: Set(),2457 schedNoPush::scheduler::ws:2458 Map(2459 "w1" ->2460 {2461 attached: Set(),2462 built: false,2463 expecting: false,2464 running: false,2465 session: true,2466 up: true2467 },2468 "w2" ->2469 {2470 attached: Set(),2471 built: false,2472 expecting: false,2473 running: false,2474 session: true,2475 up: true2476 }2477 )2478}24792480[State 6]2481{2482 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2483 schedNoPush::scheduler::crashes: 1,2484 schedNoPush::scheduler::entry: [],2485 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2486 schedNoPush::scheduler::mAssigned: Set(),2487 schedNoPush::scheduler::mBuild: Set(),2488 schedNoPush::scheduler::mDone: Set(),2489 schedNoPush::scheduler::mExpect: Set(),2490 schedNoPush::scheduler::mResult: Set(),2491 schedNoPush::scheduler::mRetry: Set("c1"),2492 schedNoPush::scheduler::mRevoke: Set(),2493 schedNoPush::scheduler::mSchedule: Set(),2494 schedNoPush::scheduler::published: 0,2495 schedNoPush::scheduler::publishedBy: Set(),2496 schedNoPush::scheduler::ws:2497 Map(2498 "w1" ->2499 {2500 attached: Set(),2501 built: false,2502 expecting: false,2503 running: false,2504 session: true,2505 up: true2506 },2507 "w2" ->2508 {2509 attached: Set("c1"),2510 built: false,2511 expecting: true,2512 running: true,2513 session: true,2514 up: true2515 }2516 )2517}25182519[violation] Found an issue (404ms at 45245 traces/second).2520Use --verbosity=3 to show executions.2521Use --seed=0x5be90713559e0f7e --backend=rust to reproduce.2522error: Invariant violated2523An example execution:25242525[State 0]2526{2527 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2528 schedNoReport::scheduler::crashes: 0,2529 schedNoReport::scheduler::entry: [],2530 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2531 schedNoReport::scheduler::mAssigned: Set(),2532 schedNoReport::scheduler::mBuild: Set(),2533 schedNoReport::scheduler::mDone: Set(),2534 schedNoReport::scheduler::mExpect: Set(),2535 schedNoReport::scheduler::mResult: Set(),2536 schedNoReport::scheduler::mRetry: Set(),2537 schedNoReport::scheduler::mRevoke: Set(),2538 schedNoReport::scheduler::mSchedule: Set(),2539 schedNoReport::scheduler::published: 0,2540 schedNoReport::scheduler::publishedBy: Set(),2541 schedNoReport::scheduler::ws:2542 Map(2543 "w1" ->2544 {2545 attached: Set(),2546 built: false,2547 expecting: false,2548 running: false,2549 session: true,2550 up: true2551 },2552 "w2" ->2553 {2554 attached: Set(),2555 built: false,2556 expecting: false,2557 running: false,2558 session: true,2559 up: true2560 }2561 )2562}25632564[State 1]2565{2566 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2567 schedNoReport::scheduler::crashes: 0,2568 schedNoReport::scheduler::entry: [],2569 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2570 schedNoReport::scheduler::mAssigned: Set(),2571 schedNoReport::scheduler::mBuild: Set(),2572 schedNoReport::scheduler::mDone: Set(),2573 schedNoReport::scheduler::mExpect: Set(),2574 schedNoReport::scheduler::mResult: Set(),2575 schedNoReport::scheduler::mRetry: Set(),2576 schedNoReport::scheduler::mRevoke: Set(),2577 schedNoReport::scheduler::mSchedule: Set("c2"),2578 schedNoReport::scheduler::published: 0,2579 schedNoReport::scheduler::publishedBy: Set(),2580 schedNoReport::scheduler::ws:2581 Map(2582 "w1" ->2583 {2584 attached: Set(),2585 built: false,2586 expecting: false,2587 running: false,2588 session: true,2589 up: true2590 },2591 "w2" ->2592 {2593 attached: Set(),2594 built: false,2595 expecting: false,2596 running: false,2597 session: true,2598 up: true2599 }2600 )2601}26022603[State 2]2604{2605 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2606 schedNoReport::scheduler::crashes: 0,2607 schedNoReport::scheduler::entry:2608 [{ followers: Set("c2"), leased: true, worker: "w1" }],2609 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2610 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2611 schedNoReport::scheduler::mBuild: Set(),2612 schedNoReport::scheduler::mDone: Set(),2613 schedNoReport::scheduler::mExpect: Set("w1"),2614 schedNoReport::scheduler::mResult: Set(),2615 schedNoReport::scheduler::mRetry: Set(),2616 schedNoReport::scheduler::mRevoke: Set(),2617 schedNoReport::scheduler::mSchedule: Set(),2618 schedNoReport::scheduler::published: 0,2619 schedNoReport::scheduler::publishedBy: Set(),2620 schedNoReport::scheduler::ws:2621 Map(2622 "w1" ->2623 {2624 attached: Set(),2625 built: false,2626 expecting: false,2627 running: false,2628 session: true,2629 up: true2630 },2631 "w2" ->2632 {2633 attached: Set(),2634 built: false,2635 expecting: false,2636 running: false,2637 session: true,2638 up: true2639 }2640 )2641}26422643[State 3]2644{2645 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2646 schedNoReport::scheduler::crashes: 0,2647 schedNoReport::scheduler::entry:2648 [{ followers: Set("c2"), leased: true, worker: "w1" }],2649 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2650 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2651 schedNoReport::scheduler::mBuild: Set(),2652 schedNoReport::scheduler::mDone: Set(),2653 schedNoReport::scheduler::mExpect: Set(),2654 schedNoReport::scheduler::mResult: Set(),2655 schedNoReport::scheduler::mRetry: Set(),2656 schedNoReport::scheduler::mRevoke: Set(),2657 schedNoReport::scheduler::mSchedule: Set(),2658 schedNoReport::scheduler::published: 0,2659 schedNoReport::scheduler::publishedBy: Set(),2660 schedNoReport::scheduler::ws:2661 Map(2662 "w1" ->2663 {2664 attached: Set(),2665 built: false,2666 expecting: true,2667 running: true,2668 session: true,2669 up: true2670 },2671 "w2" ->2672 {2673 attached: Set(),2674 built: false,2675 expecting: false,2676 running: false,2677 session: true,2678 up: true2679 }2680 )2681}26822683[State 4]2684{2685 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2686 schedNoReport::scheduler::crashes: 1,2687 schedNoReport::scheduler::entry: [],2688 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2689 schedNoReport::scheduler::mAssigned: Set(),2690 schedNoReport::scheduler::mBuild: Set(),2691 schedNoReport::scheduler::mDone: Set(),2692 schedNoReport::scheduler::mExpect: Set(),2693 schedNoReport::scheduler::mResult: Set(),2694 schedNoReport::scheduler::mRetry: Set("c2"),2695 schedNoReport::scheduler::mRevoke: Set(),2696 schedNoReport::scheduler::mSchedule: Set(),2697 schedNoReport::scheduler::published: 0,2698 schedNoReport::scheduler::publishedBy: Set(),2699 schedNoReport::scheduler::ws:2700 Map(2701 "w1" ->2702 {2703 attached: Set(),2704 built: false,2705 expecting: true,2706 running: true,2707 session: false,2708 up: true2709 },2710 "w2" ->2711 {2712 attached: Set(),2713 built: false,2714 expecting: false,2715 running: false,2716 session: false,2717 up: true2718 }2719 )2720}27212722[State 5]2723{2724 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2725 schedNoReport::scheduler::crashes: 2,2726 schedNoReport::scheduler::entry: [],2727 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2728 schedNoReport::scheduler::mAssigned: Set(),2729 schedNoReport::scheduler::mBuild: Set(),2730 schedNoReport::scheduler::mDone: Set(),2731 schedNoReport::scheduler::mExpect: Set(),2732 schedNoReport::scheduler::mResult: Set(),2733 schedNoReport::scheduler::mRetry: Set("c2"),2734 schedNoReport::scheduler::mRevoke: Set(),2735 schedNoReport::scheduler::mSchedule: Set(),2736 schedNoReport::scheduler::published: 0,2737 schedNoReport::scheduler::publishedBy: Set(),2738 schedNoReport::scheduler::ws:2739 Map(2740 "w1" ->2741 {2742 attached: Set(),2743 built: false,2744 expecting: true,2745 running: true,2746 session: false,2747 up: true2748 },2749 "w2" ->2750 {2751 attached: Set(),2752 built: false,2753 expecting: false,2754 running: false,2755 session: false,2756 up: false2757 }2758 )2759}27602761[State 6]2762{2763 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2764 schedNoReport::scheduler::crashes: 2,2765 schedNoReport::scheduler::entry: [],2766 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2767 schedNoReport::scheduler::mAssigned: Set(),2768 schedNoReport::scheduler::mBuild: Set(),2769 schedNoReport::scheduler::mDone: Set(),2770 schedNoReport::scheduler::mExpect: Set(),2771 schedNoReport::scheduler::mResult: Set(),2772 schedNoReport::scheduler::mRetry: Set("c2"),2773 schedNoReport::scheduler::mRevoke: Set(),2774 schedNoReport::scheduler::mSchedule: Set("c1"),2775 schedNoReport::scheduler::published: 0,2776 schedNoReport::scheduler::publishedBy: Set(),2777 schedNoReport::scheduler::ws:2778 Map(2779 "w1" ->2780 {2781 attached: Set(),2782 built: false,2783 expecting: true,2784 running: true,2785 session: false,2786 up: true2787 },2788 "w2" ->2789 {2790 attached: Set(),2791 built: false,2792 expecting: false,2793 running: false,2794 session: false,2795 up: false2796 }2797 )2798}27992800[State 7]2801{2802 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2803 schedNoReport::scheduler::crashes: 2,2804 schedNoReport::scheduler::entry: [],2805 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2806 schedNoReport::scheduler::mAssigned: Set(),2807 schedNoReport::scheduler::mBuild: Set(),2808 schedNoReport::scheduler::mDone: Set(),2809 schedNoReport::scheduler::mExpect: Set(),2810 schedNoReport::scheduler::mResult: Set(),2811 schedNoReport::scheduler::mRetry: Set("c2"),2812 schedNoReport::scheduler::mRevoke: Set(),2813 schedNoReport::scheduler::mSchedule: Set("c1"),2814 schedNoReport::scheduler::published: 0,2815 schedNoReport::scheduler::publishedBy: Set(),2816 schedNoReport::scheduler::ws:2817 Map(2818 "w1" ->2819 {2820 attached: Set(),2821 built: false,2822 expecting: true,2823 running: true,2824 session: false,2825 up: true2826 },2827 "w2" ->2828 {2829 attached: Set(),2830 built: false,2831 expecting: false,2832 running: false,2833 session: true,2834 up: true2835 }2836 )2837}28382839[State 8]2840{2841 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2842 schedNoReport::scheduler::crashes: 2,2843 schedNoReport::scheduler::entry:2844 [{ followers: Set("c1"), leased: true, worker: "w2" }],2845 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2846 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2847 schedNoReport::scheduler::mBuild: Set(),2848 schedNoReport::scheduler::mDone: Set(),2849 schedNoReport::scheduler::mExpect: Set("w2"),2850 schedNoReport::scheduler::mResult: Set(),2851 schedNoReport::scheduler::mRetry: Set("c2"),2852 schedNoReport::scheduler::mRevoke: Set(),2853 schedNoReport::scheduler::mSchedule: Set(),2854 schedNoReport::scheduler::published: 0,2855 schedNoReport::scheduler::publishedBy: Set(),2856 schedNoReport::scheduler::ws:2857 Map(2858 "w1" ->2859 {2860 attached: Set(),2861 built: false,2862 expecting: true,2863 running: true,2864 session: false,2865 up: true2866 },2867 "w2" ->2868 {2869 attached: Set(),2870 built: false,2871 expecting: false,2872 running: false,2873 session: true,2874 up: true2875 }2876 )2877}28782879[State 9]2880{2881 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2882 schedNoReport::scheduler::crashes: 2,2883 schedNoReport::scheduler::entry:2884 [{ followers: Set("c1"), leased: true, worker: "w2" }],2885 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2886 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2887 schedNoReport::scheduler::mBuild: Set(),2888 schedNoReport::scheduler::mDone: Set(),2889 schedNoReport::scheduler::mExpect: Set(),2890 schedNoReport::scheduler::mResult: Set(),2891 schedNoReport::scheduler::mRetry: Set("c2"),2892 schedNoReport::scheduler::mRevoke: Set(),2893 schedNoReport::scheduler::mSchedule: Set(),2894 schedNoReport::scheduler::published: 0,2895 schedNoReport::scheduler::publishedBy: Set(),2896 schedNoReport::scheduler::ws:2897 Map(2898 "w1" ->2899 {2900 attached: Set(),2901 built: false,2902 expecting: true,2903 running: true,2904 session: false,2905 up: true2906 },2907 "w2" ->2908 {2909 attached: Set(),2910 built: false,2911 expecting: true,2912 running: true,2913 session: true,2914 up: true2915 }2916 )2917}29182919[State 10]2920{2921 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2922 schedNoReport::scheduler::crashes: 2,2923 schedNoReport::scheduler::entry:2924 [{ followers: Set("c1"), leased: true, worker: "w2" }],2925 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2926 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2927 schedNoReport::scheduler::mBuild: Set(),2928 schedNoReport::scheduler::mDone: Set(),2929 schedNoReport::scheduler::mExpect: Set(),2930 schedNoReport::scheduler::mResult: Set(),2931 schedNoReport::scheduler::mRetry: Set("c2"),2932 schedNoReport::scheduler::mRevoke: Set(),2933 schedNoReport::scheduler::mSchedule: Set(),2934 schedNoReport::scheduler::published: 0,2935 schedNoReport::scheduler::publishedBy: Set(),2936 schedNoReport::scheduler::ws:2937 Map(2938 "w1" ->2939 {2940 attached: Set(),2941 built: false,2942 expecting: true,2943 running: true,2944 session: true,2945 up: true2946 },2947 "w2" ->2948 {2949 attached: Set(),2950 built: false,2951 expecting: true,2952 running: true,2953 session: true,2954 up: true2955 }2956 )2957}29582959[violation] Found an issue (435ms at 61092 traces/second).2960Use --verbosity=3 to show executions.2961Use --seed=0xc898d70abd146758 --backend=rust to reproduce.2962error: Invariant violated2963An example execution:29642965[State 0]2966{2967 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2968 schedTerminal::scheduler::crashes: 0,2969 schedTerminal::scheduler::entry: [],2970 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2971 schedTerminal::scheduler::mAssigned: Set(),2972 schedTerminal::scheduler::mBuild: Set(),2973 schedTerminal::scheduler::mDone: Set(),2974 schedTerminal::scheduler::mExpect: Set(),2975 schedTerminal::scheduler::mResult: Set(),2976 schedTerminal::scheduler::mRetry: Set(),2977 schedTerminal::scheduler::mRevoke: Set(),2978 schedTerminal::scheduler::mSchedule: Set(),2979 schedTerminal::scheduler::published: 0,2980 schedTerminal::scheduler::publishedBy: Set(),2981 schedTerminal::scheduler::ws:2982 Map(2983 "w1" ->2984 {2985 attached: Set(),2986 built: false,2987 expecting: false,2988 running: false,2989 session: true,2990 up: true2991 },2992 "w2" ->2993 {2994 attached: Set(),2995 built: false,2996 expecting: false,2997 running: false,2998 session: true,2999 up: true3000 }3001 )3002}30033004[State 1]3005{3006 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3007 schedTerminal::scheduler::crashes: 1,3008 schedTerminal::scheduler::entry: [],3009 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3010 schedTerminal::scheduler::mAssigned: Set(),3011 schedTerminal::scheduler::mBuild: Set(),3012 schedTerminal::scheduler::mDone: Set(),3013 schedTerminal::scheduler::mExpect: Set(),3014 schedTerminal::scheduler::mResult: Set(),3015 schedTerminal::scheduler::mRetry: Set(),3016 schedTerminal::scheduler::mRevoke: Set(),3017 schedTerminal::scheduler::mSchedule: Set(),3018 schedTerminal::scheduler::published: 0,3019 schedTerminal::scheduler::publishedBy: Set(),3020 schedTerminal::scheduler::ws:3021 Map(3022 "w1" ->3023 {3024 attached: Set(),3025 built: false,3026 expecting: false,3027 running: false,3028 session: false,3029 up: true3030 },3031 "w2" ->3032 {3033 attached: Set(),3034 built: false,3035 expecting: false,3036 running: false,3037 session: false,3038 up: true3039 }3040 )3041}30423043[State 2]3044{3045 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3046 schedTerminal::scheduler::crashes: 1,3047 schedTerminal::scheduler::entry: [],3048 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3049 schedTerminal::scheduler::mAssigned: Set(),3050 schedTerminal::scheduler::mBuild: Set(),3051 schedTerminal::scheduler::mDone: Set(),3052 schedTerminal::scheduler::mExpect: Set(),3053 schedTerminal::scheduler::mResult: Set(),3054 schedTerminal::scheduler::mRetry: Set(),3055 schedTerminal::scheduler::mRevoke: Set(),3056 schedTerminal::scheduler::mSchedule: Set("c2"),3057 schedTerminal::scheduler::published: 0,3058 schedTerminal::scheduler::publishedBy: Set(),3059 schedTerminal::scheduler::ws:3060 Map(3061 "w1" ->3062 {3063 attached: Set(),3064 built: false,3065 expecting: false,3066 running: false,3067 session: false,3068 up: true3069 },3070 "w2" ->3071 {3072 attached: Set(),3073 built: false,3074 expecting: false,3075 running: false,3076 session: false,3077 up: true3078 }3079 )3080}30813082[State 3]3083{3084 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3085 schedTerminal::scheduler::crashes: 1,3086 schedTerminal::scheduler::entry: [],3087 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3088 schedTerminal::scheduler::mAssigned: Set(),3089 schedTerminal::scheduler::mBuild: Set(),3090 schedTerminal::scheduler::mDone: Set(),3091 schedTerminal::scheduler::mExpect: Set(),3092 schedTerminal::scheduler::mResult: Set(),3093 schedTerminal::scheduler::mRetry: Set(),3094 schedTerminal::scheduler::mRevoke: Set(),3095 schedTerminal::scheduler::mSchedule: Set(),3096 schedTerminal::scheduler::published: 0,3097 schedTerminal::scheduler::publishedBy: Set(),3098 schedTerminal::scheduler::ws:3099 Map(3100 "w1" ->3101 {3102 attached: Set(),3103 built: false,3104 expecting: false,3105 running: false,3106 session: false,3107 up: true3108 },3109 "w2" ->3110 {3111 attached: Set(),3112 built: false,3113 expecting: false,3114 running: false,3115 session: false,3116 up: true3117 }3118 )3119}31203121[violation] Found an issue (338ms at 6050 traces/second).3122Use --verbosity=3 to show executions.3123Use --seed=0x426faae65279aef6 --backend=rust to reproduce.3124error: Invariant violated3125An example execution:31263127[State 0]3128{3129 pushFixed::push::byPath: Map(),3130 pushFixed::push::inflight: Set(),3131 pushFixed::push::left: Map(),3132 pushFixed::push::sent: Map()3133}31343135[State 1]3136{3137 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3138 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3139 pushFixed::push::left: Map(2 -> 2),3140 pushFixed::push::sent: Map(2 -> Set("a", "b"))3141}31423143[State 2]3144{3145 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3146 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),3147 pushFixed::push::left: Map(1 -> 2, 2 -> 2),3148 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3149}31503151[State 3]3152{3153 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3154 pushFixed::push::inflight:3155 Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),3156 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 2),3157 pushFixed::push::sent:3158 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3159}31603161[State 4]3162{3163 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3164 pushFixed::push::inflight:3165 Set((1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),3166 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 2),3167 pushFixed::push::sent:3168 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3169}31703171[State 5]3172{3173 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3174 pushFixed::push::inflight: Set((1, "b"), (2, "b"), (3, "a"), (3, "b")),3175 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 2),3176 pushFixed::push::sent:3177 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3178}31793180[State 6]3181{3182 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3183 pushFixed::push::inflight: Set((1, "b"), (2, "b"), (3, "b")),3184 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 1),3185 pushFixed::push::sent:3186 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3187}31883189[State 7]3190{3191 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3192 pushFixed::push::inflight: Set((1, "b"), (2, "b")),3193 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 0),3194 pushFixed::push::sent:3195 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3196}31973198[State 8]3199{3200 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3201 pushFixed::push::inflight: Set((1, "b")),3202 pushFixed::push::left: Map(1 -> 1, 2 -> 0, 3 -> 0),3203 pushFixed::push::sent:3204 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3205}32063207[State 9]3208{3209 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3210 pushFixed::push::inflight: Set(),3211 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3212 pushFixed::push::sent:3213 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3214}32153216[ok] No violation found (97ms at 206186 traces/second).3217Trace length statistics: max=10, min=7, average=7.943218You may increase --max-samples and --max-steps.3219Use --verbosity to produce more (or less) output.3220Use --seed=0x4d1b152b1a46d1be --backend=rust to reproduce.