nix-grpc-store-spec
checks.x86_64-linux.spec
· build #803
· 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" -> 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: false,68 up: true69 },70 "w2" ->71 {72 attached: Set(),73 built: false,74 expecting: false,75 running: false,76 session: false,77 up: true78 }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: false,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" -> CIdle, "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(),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: true,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" -> CIdle, "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(),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: true,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: "w1" }],283 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),284 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),285 schedFixed::scheduler::mBuild: Set(),286 schedFixed::scheduler::mDone: Set(),287 schedFixed::scheduler::mExpect: Set("w1"),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" -> CQueued, "c2" -> CQueued),320 schedFixed::scheduler::crashes: 2,321 schedFixed::scheduler::entry:322 [{ followers: Set("c1"), leased: true, worker: "w1" }],323 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),324 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),325 schedFixed::scheduler::mBuild: Set(),326 schedFixed::scheduler::mDone: Set(),327 schedFixed::scheduler::mExpect: Set("w1"),328 schedFixed::scheduler::mResult: Set(),329 schedFixed::scheduler::mRetry: Set(),330 schedFixed::scheduler::mRevoke: Set(),331 schedFixed::scheduler::mSchedule: Set("c2"),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" -> CQueued),360 schedFixed::scheduler::crashes: 2,361 schedFixed::scheduler::entry:362 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],363 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),364 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),365 schedFixed::scheduler::mBuild: Set(),366 schedFixed::scheduler::mDone: Set(),367 schedFixed::scheduler::mExpect: Set("w1"),368 schedFixed::scheduler::mResult: Set(),369 schedFixed::scheduler::mRetry: Set(),370 schedFixed::scheduler::mRevoke: Set(),371 schedFixed::scheduler::mSchedule: Set(),372 schedFixed::scheduler::published: 0,373 schedFixed::scheduler::publishedBy: Set(),374 schedFixed::scheduler::ws:375 Map(376 "w1" ->377 {378 attached: Set(),379 built: false,380 expecting: false,381 running: false,382 session: true,383 up: true384 },385 "w2" ->386 {387 attached: Set(),388 built: false,389 expecting: false,390 running: false,391 session: true,392 up: true393 }394 )395}396397[State 10]398{399 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),400 schedFixed::scheduler::crashes: 2,401 schedFixed::scheduler::entry:402 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],403 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),404 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),405 schedFixed::scheduler::mBuild: Set(("c1", "w1")),406 schedFixed::scheduler::mDone: Set(),407 schedFixed::scheduler::mExpect: Set("w1"),408 schedFixed::scheduler::mResult: Set(),409 schedFixed::scheduler::mRetry: Set(),410 schedFixed::scheduler::mRevoke: Set(),411 schedFixed::scheduler::mSchedule: Set(),412 schedFixed::scheduler::published: 0,413 schedFixed::scheduler::publishedBy: Set(),414 schedFixed::scheduler::ws:415 Map(416 "w1" ->417 {418 attached: Set(),419 built: false,420 expecting: false,421 running: false,422 session: true,423 up: true424 },425 "w2" ->426 {427 attached: Set(),428 built: false,429 expecting: false,430 running: false,431 session: true,432 up: true433 }434 )435}436437[State 11]438{439 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),440 schedFixed::scheduler::crashes: 2,441 schedFixed::scheduler::entry:442 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],443 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),444 schedFixed::scheduler::mAssigned: Set(),445 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),446 schedFixed::scheduler::mDone: Set(),447 schedFixed::scheduler::mExpect: Set("w1"),448 schedFixed::scheduler::mResult: Set(),449 schedFixed::scheduler::mRetry: Set(),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("w1"), "c2" -> CSent("w1")),480 schedFixed::scheduler::crashes: 2,481 schedFixed::scheduler::entry:482 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],483 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),484 schedFixed::scheduler::mAssigned: Set(),485 schedFixed::scheduler::mBuild: Set(("c2", "w1")),486 schedFixed::scheduler::mDone: Set(),487 schedFixed::scheduler::mExpect: Set("w1"),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" -> CQueued, "c2" -> CSent("w1")),520 schedFixed::scheduler::crashes: 2,521 schedFixed::scheduler::entry:522 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],523 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),524 schedFixed::scheduler::mAssigned: Set(),525 schedFixed::scheduler::mBuild: Set(("c2", "w1")),526 schedFixed::scheduler::mDone: Set(),527 schedFixed::scheduler::mExpect: Set("w1"),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("w1")),560 schedFixed::scheduler::crashes: 2,561 schedFixed::scheduler::entry:562 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],563 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),564 schedFixed::scheduler::mAssigned: Set(),565 schedFixed::scheduler::mBuild: Set(),566 schedFixed::scheduler::mDone: Set(),567 schedFixed::scheduler::mExpect: Set("w1"),568 schedFixed::scheduler::mResult: Set(),569 schedFixed::scheduler::mRetry: Set("c2"),570 schedFixed::scheduler::mRevoke: Set(),571 schedFixed::scheduler::mSchedule: Set("c1"),572 schedFixed::scheduler::published: 0,573 schedFixed::scheduler::publishedBy: Set(),574 schedFixed::scheduler::ws:575 Map(576 "w1" ->577 {578 attached: Set(),579 built: false,580 expecting: false,581 running: false,582 session: true,583 up: true584 },585 "w2" ->586 {587 attached: Set(),588 built: false,589 expecting: false,590 running: false,591 session: true,592 up: true593 }594 )595}596597[State 15]598{599 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),600 schedFixed::scheduler::crashes: 2,601 schedFixed::scheduler::entry:602 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],603 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),604 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),605 schedFixed::scheduler::mBuild: Set(),606 schedFixed::scheduler::mDone: Set(),607 schedFixed::scheduler::mExpect: Set("w1"),608 schedFixed::scheduler::mResult: Set(),609 schedFixed::scheduler::mRetry: Set("c2"),610 schedFixed::scheduler::mRevoke: Set(),611 schedFixed::scheduler::mSchedule: Set(),612 schedFixed::scheduler::published: 0,613 schedFixed::scheduler::publishedBy: Set(),614 schedFixed::scheduler::ws:615 Map(616 "w1" ->617 {618 attached: Set(),619 built: false,620 expecting: false,621 running: false,622 session: true,623 up: true624 },625 "w2" ->626 {627 attached: Set(),628 built: false,629 expecting: false,630 running: false,631 session: true,632 up: true633 }634 )635}636637[State 16]638{639 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),640 schedFixed::scheduler::crashes: 2,641 schedFixed::scheduler::entry:642 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],643 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),644 schedFixed::scheduler::mAssigned: Set(),645 schedFixed::scheduler::mBuild: Set(("c1", "w1")),646 schedFixed::scheduler::mDone: Set(),647 schedFixed::scheduler::mExpect: Set("w1"),648 schedFixed::scheduler::mResult: Set(),649 schedFixed::scheduler::mRetry: Set("c2"),650 schedFixed::scheduler::mRevoke: Set(),651 schedFixed::scheduler::mSchedule: Set(),652 schedFixed::scheduler::published: 0,653 schedFixed::scheduler::publishedBy: Set(),654 schedFixed::scheduler::ws:655 Map(656 "w1" ->657 {658 attached: Set(),659 built: false,660 expecting: false,661 running: false,662 session: true,663 up: true664 },665 "w2" ->666 {667 attached: Set(),668 built: false,669 expecting: false,670 running: false,671 session: true,672 up: true673 }674 )675}676677[State 17]678{679 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),680 schedFixed::scheduler::crashes: 2,681 schedFixed::scheduler::entry:682 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],683 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),684 schedFixed::scheduler::mAssigned: Set(),685 schedFixed::scheduler::mBuild: Set(),686 schedFixed::scheduler::mDone: Set(),687 schedFixed::scheduler::mExpect: Set("w1"),688 schedFixed::scheduler::mResult: Set(),689 schedFixed::scheduler::mRetry: Set("c1", "c2"),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" -> CSent("w1"), "c2" -> CQueued),720 schedFixed::scheduler::crashes: 2,721 schedFixed::scheduler::entry:722 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],723 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),724 schedFixed::scheduler::mAssigned: Set(),725 schedFixed::scheduler::mBuild: Set(),726 schedFixed::scheduler::mDone: Set(),727 schedFixed::scheduler::mExpect: Set("w1"),728 schedFixed::scheduler::mResult: Set(),729 schedFixed::scheduler::mRetry: Set("c1"),730 schedFixed::scheduler::mRevoke: Set(),731 schedFixed::scheduler::mSchedule: Set("c2"),732 schedFixed::scheduler::published: 0,733 schedFixed::scheduler::publishedBy: Set(),734 schedFixed::scheduler::ws:735 Map(736 "w1" ->737 {738 attached: Set(),739 built: false,740 expecting: false,741 running: false,742 session: true,743 up: true744 },745 "w2" ->746 {747 attached: Set(),748 built: false,749 expecting: false,750 running: false,751 session: true,752 up: true753 }754 )755}756757[State 19]758{759 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),760 schedFixed::scheduler::crashes: 2,761 schedFixed::scheduler::entry:762 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],763 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),764 schedFixed::scheduler::mAssigned: Set(),765 schedFixed::scheduler::mBuild: Set(),766 schedFixed::scheduler::mDone: Set(),767 schedFixed::scheduler::mExpect: Set("w1"),768 schedFixed::scheduler::mResult: Set(),769 schedFixed::scheduler::mRetry: Set(),770 schedFixed::scheduler::mRevoke: Set(),771 schedFixed::scheduler::mSchedule: Set("c1", "c2"),772 schedFixed::scheduler::published: 0,773 schedFixed::scheduler::publishedBy: Set(),774 schedFixed::scheduler::ws:775 Map(776 "w1" ->777 {778 attached: Set(),779 built: false,780 expecting: false,781 running: false,782 session: true,783 up: true784 },785 "w2" ->786 {787 attached: Set(),788 built: false,789 expecting: false,790 running: false,791 session: true,792 up: true793 }794 )795}796797[State 20]798{799 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),800 schedFixed::scheduler::crashes: 2,801 schedFixed::scheduler::entry:802 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],803 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),804 schedFixed::scheduler::mAssigned: Set(),805 schedFixed::scheduler::mBuild: Set(),806 schedFixed::scheduler::mDone: Set(),807 schedFixed::scheduler::mExpect: Set(),808 schedFixed::scheduler::mResult: Set(),809 schedFixed::scheduler::mRetry: Set(),810 schedFixed::scheduler::mRevoke: Set(),811 schedFixed::scheduler::mSchedule: Set("c1", "c2"),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: true,821 running: true,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: "w1" }],843 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),844 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),845 schedFixed::scheduler::mBuild: Set(),846 schedFixed::scheduler::mDone: Set(),847 schedFixed::scheduler::mExpect: Set(),848 schedFixed::scheduler::mResult: Set(),849 schedFixed::scheduler::mRetry: Set(),850 schedFixed::scheduler::mRevoke: Set(),851 schedFixed::scheduler::mSchedule: Set("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: true,861 running: true,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: "w1" }],883 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),884 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),885 schedFixed::scheduler::mBuild: Set(),886 schedFixed::scheduler::mDone: Set(),887 schedFixed::scheduler::mExpect: Set(),888 schedFixed::scheduler::mResult: Set(),889 schedFixed::scheduler::mRetry: Set(),890 schedFixed::scheduler::mRevoke: Set(),891 schedFixed::scheduler::mSchedule: Set(),892 schedFixed::scheduler::published: 0,893 schedFixed::scheduler::publishedBy: Set(),894 schedFixed::scheduler::ws:895 Map(896 "w1" ->897 {898 attached: Set(),899 built: false,900 expecting: true,901 running: true,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" -> CQueued, "c2" -> CQueued),920 schedFixed::scheduler::crashes: 2,921 schedFixed::scheduler::entry:922 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],923 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),924 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),925 schedFixed::scheduler::mBuild: Set(),926 schedFixed::scheduler::mDone: Set("w1"),927 schedFixed::scheduler::mExpect: Set(),928 schedFixed::scheduler::mResult: Set(),929 schedFixed::scheduler::mRetry: Set(),930 schedFixed::scheduler::mRevoke: Set(),931 schedFixed::scheduler::mSchedule: Set(),932 schedFixed::scheduler::published: 1,933 schedFixed::scheduler::publishedBy: Set("w1"),934 schedFixed::scheduler::ws:935 Map(936 "w1" ->937 {938 attached: Set(),939 built: true,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" -> CQueued, "c2" -> CQueued),960 schedFixed::scheduler::crashes: 2,961 schedFixed::scheduler::entry: [],962 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),963 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),964 schedFixed::scheduler::mBuild: Set(),965 schedFixed::scheduler::mDone: Set(),966 schedFixed::scheduler::mExpect: Set(),967 schedFixed::scheduler::mResult: Set(),968 schedFixed::scheduler::mRetry: Set(),969 schedFixed::scheduler::mRevoke: Set(),970 schedFixed::scheduler::mSchedule: Set(),971 schedFixed::scheduler::published: 1,972 schedFixed::scheduler::publishedBy: Set("w1"),973 schedFixed::scheduler::ws:974 Map(975 "w1" ->976 {977 attached: Set(),978 built: true,979 expecting: false,980 running: false,981 session: true,982 up: true983 },984 "w2" ->985 {986 attached: Set(),987 built: false,988 expecting: false,989 running: false,990 session: true,991 up: true992 }993 )994}995996[State 25]997{998 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),999 schedFixed::scheduler::crashes: 2,1000 schedFixed::scheduler::entry: [],1001 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1002 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),1003 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1004 schedFixed::scheduler::mDone: Set(),1005 schedFixed::scheduler::mExpect: Set(),1006 schedFixed::scheduler::mResult: Set(),1007 schedFixed::scheduler::mRetry: Set(),1008 schedFixed::scheduler::mRevoke: Set(),1009 schedFixed::scheduler::mSchedule: Set(),1010 schedFixed::scheduler::published: 1,1011 schedFixed::scheduler::publishedBy: Set("w1"),1012 schedFixed::scheduler::ws:1013 Map(1014 "w1" ->1015 {1016 attached: Set(),1017 built: true,1018 expecting: false,1019 running: false,1020 session: true,1021 up: true1022 },1023 "w2" ->1024 {1025 attached: Set(),1026 built: false,1027 expecting: false,1028 running: false,1029 session: true,1030 up: true1031 }1032 )1033}10341035[State 26]1036{1037 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1038 schedFixed::scheduler::crashes: 2,1039 schedFixed::scheduler::entry: [],1040 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1041 schedFixed::scheduler::mAssigned: Set(),1042 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),1043 schedFixed::scheduler::mDone: Set(),1044 schedFixed::scheduler::mExpect: Set(),1045 schedFixed::scheduler::mResult: Set(),1046 schedFixed::scheduler::mRetry: Set(),1047 schedFixed::scheduler::mRevoke: Set(),1048 schedFixed::scheduler::mSchedule: Set(),1049 schedFixed::scheduler::published: 1,1050 schedFixed::scheduler::publishedBy: Set("w1"),1051 schedFixed::scheduler::ws:1052 Map(1053 "w1" ->1054 {1055 attached: Set(),1056 built: true,1057 expecting: false,1058 running: false,1059 session: true,1060 up: true1061 },1062 "w2" ->1063 {1064 attached: Set(),1065 built: false,1066 expecting: false,1067 running: false,1068 session: true,1069 up: true1070 }1071 )1072}10731074[State 27]1075{1076 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1077 schedFixed::scheduler::crashes: 2,1078 schedFixed::scheduler::entry: [],1079 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1080 schedFixed::scheduler::mAssigned: Set(),1081 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1082 schedFixed::scheduler::mDone: Set(),1083 schedFixed::scheduler::mExpect: Set(),1084 schedFixed::scheduler::mResult: Set("c1"),1085 schedFixed::scheduler::mRetry: Set(),1086 schedFixed::scheduler::mRevoke: Set(),1087 schedFixed::scheduler::mSchedule: Set(),1088 schedFixed::scheduler::published: 1,1089 schedFixed::scheduler::publishedBy: Set("w1"),1090 schedFixed::scheduler::ws:1091 Map(1092 "w1" ->1093 {1094 attached: Set(),1095 built: true,1096 expecting: false,1097 running: false,1098 session: true,1099 up: true1100 },1101 "w2" ->1102 {1103 attached: Set(),1104 built: false,1105 expecting: false,1106 running: false,1107 session: true,1108 up: true1109 }1110 )1111}11121113[State 28]1114{1115 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1116 schedFixed::scheduler::crashes: 2,1117 schedFixed::scheduler::entry: [],1118 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1119 schedFixed::scheduler::mAssigned: Set(),1120 schedFixed::scheduler::mBuild: Set(),1121 schedFixed::scheduler::mDone: Set(),1122 schedFixed::scheduler::mExpect: Set(),1123 schedFixed::scheduler::mResult: Set("c1", "c2"),1124 schedFixed::scheduler::mRetry: Set(),1125 schedFixed::scheduler::mRevoke: Set(),1126 schedFixed::scheduler::mSchedule: Set(),1127 schedFixed::scheduler::published: 1,1128 schedFixed::scheduler::publishedBy: Set("w1"),1129 schedFixed::scheduler::ws:1130 Map(1131 "w1" ->1132 {1133 attached: Set(),1134 built: true,1135 expecting: false,1136 running: false,1137 session: true,1138 up: true1139 },1140 "w2" ->1141 {1142 attached: Set(),1143 built: false,1144 expecting: false,1145 running: false,1146 session: true,1147 up: true1148 }1149 )1150}11511152[State 29]1153{1154 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w1")),1155 schedFixed::scheduler::crashes: 2,1156 schedFixed::scheduler::entry: [],1157 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1158 schedFixed::scheduler::mAssigned: Set(),1159 schedFixed::scheduler::mBuild: Set(),1160 schedFixed::scheduler::mDone: Set(),1161 schedFixed::scheduler::mExpect: Set(),1162 schedFixed::scheduler::mResult: Set("c2"),1163 schedFixed::scheduler::mRetry: Set(),1164 schedFixed::scheduler::mRevoke: Set(),1165 schedFixed::scheduler::mSchedule: Set(),1166 schedFixed::scheduler::published: 1,1167 schedFixed::scheduler::publishedBy: Set("w1"),1168 schedFixed::scheduler::ws:1169 Map(1170 "w1" ->1171 {1172 attached: Set(),1173 built: true,1174 expecting: false,1175 running: false,1176 session: true,1177 up: true1178 },1179 "w2" ->1180 {1181 attached: Set(),1182 built: false,1183 expecting: false,1184 running: false,1185 session: true,1186 up: true1187 }1188 )1189}11901191[State 30]1192{1193 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),1194 schedFixed::scheduler::crashes: 2,1195 schedFixed::scheduler::entry: [],1196 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1197 schedFixed::scheduler::mAssigned: Set(),1198 schedFixed::scheduler::mBuild: Set(),1199 schedFixed::scheduler::mDone: Set(),1200 schedFixed::scheduler::mExpect: Set(),1201 schedFixed::scheduler::mResult: Set(),1202 schedFixed::scheduler::mRetry: Set(),1203 schedFixed::scheduler::mRevoke: Set(),1204 schedFixed::scheduler::mSchedule: Set(),1205 schedFixed::scheduler::published: 1,1206 schedFixed::scheduler::publishedBy: Set("w1"),1207 schedFixed::scheduler::ws:1208 Map(1209 "w1" ->1210 {1211 attached: Set(),1212 built: true,1213 expecting: false,1214 running: false,1215 session: true,1216 up: true1217 },1218 "w2" ->1219 {1220 attached: Set(),1221 built: false,1222 expecting: false,1223 running: false,1224 session: true,1225 up: true1226 }1227 )1228}12291230[ok] No violation found (571ms at 52539 traces/second).1231Trace length statistics: max=27, min=16, average=18.731232You may increase --max-samples and --max-steps.1233Use --verbosity to produce more (or less) output.1234Use --seed=0xf0ef0fd044793baa --backend=rust to reproduce.1235An example execution:12361237[State 0]1238{1239 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1240 schedNoRevoke::scheduler::crashes: 0,1241 schedNoRevoke::scheduler::entry: [],1242 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1243 schedNoRevoke::scheduler::mAssigned: Set(),1244 schedNoRevoke::scheduler::mBuild: Set(),1245 schedNoRevoke::scheduler::mDone: Set(),1246 schedNoRevoke::scheduler::mExpect: Set(),1247 schedNoRevoke::scheduler::mResult: Set(),1248 schedNoRevoke::scheduler::mRetry: Set(),1249 schedNoRevoke::scheduler::mRevoke: Set(),1250 schedNoRevoke::scheduler::mSchedule: Set(),1251 schedNoRevoke::scheduler::published: 0,1252 schedNoRevoke::scheduler::publishedBy: Set(),1253 schedNoRevoke::scheduler::ws:1254 Map(1255 "w1" ->1256 {1257 attached: Set(),1258 built: false,1259 expecting: false,1260 running: false,1261 session: true,1262 up: true1263 },1264 "w2" ->1265 {1266 attached: Set(),1267 built: false,1268 expecting: false,1269 running: false,1270 session: true,1271 up: true1272 }1273 )1274}12751276[State 1]1277{1278 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1279 schedNoRevoke::scheduler::crashes: 0,1280 schedNoRevoke::scheduler::entry: [],1281 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1282 schedNoRevoke::scheduler::mAssigned: Set(),1283 schedNoRevoke::scheduler::mBuild: Set(),1284 schedNoRevoke::scheduler::mDone: Set(),1285 schedNoRevoke::scheduler::mExpect: Set(),1286 schedNoRevoke::scheduler::mResult: Set(),1287 schedNoRevoke::scheduler::mRetry: Set(),1288 schedNoRevoke::scheduler::mRevoke: Set(),1289 schedNoRevoke::scheduler::mSchedule: Set("c2"),1290 schedNoRevoke::scheduler::published: 0,1291 schedNoRevoke::scheduler::publishedBy: Set(),1292 schedNoRevoke::scheduler::ws:1293 Map(1294 "w1" ->1295 {1296 attached: Set(),1297 built: false,1298 expecting: false,1299 running: false,1300 session: true,1301 up: true1302 },1303 "w2" ->1304 {1305 attached: Set(),1306 built: false,1307 expecting: false,1308 running: false,1309 session: true,1310 up: true1311 }1312 )1313}13141315[State 2]1316{1317 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1318 schedNoRevoke::scheduler::crashes: 0,1319 schedNoRevoke::scheduler::entry:1320 [{ followers: Set("c2"), leased: true, worker: "w1" }],1321 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1322 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1323 schedNoRevoke::scheduler::mBuild: Set(),1324 schedNoRevoke::scheduler::mDone: Set(),1325 schedNoRevoke::scheduler::mExpect: Set("w1"),1326 schedNoRevoke::scheduler::mResult: Set(),1327 schedNoRevoke::scheduler::mRetry: Set(),1328 schedNoRevoke::scheduler::mRevoke: Set(),1329 schedNoRevoke::scheduler::mSchedule: Set(),1330 schedNoRevoke::scheduler::published: 0,1331 schedNoRevoke::scheduler::publishedBy: Set(),1332 schedNoRevoke::scheduler::ws:1333 Map(1334 "w1" ->1335 {1336 attached: Set(),1337 built: false,1338 expecting: false,1339 running: false,1340 session: true,1341 up: true1342 },1343 "w2" ->1344 {1345 attached: Set(),1346 built: false,1347 expecting: false,1348 running: false,1349 session: true,1350 up: true1351 }1352 )1353}13541355[State 3]1356{1357 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1358 schedNoRevoke::scheduler::crashes: 0,1359 schedNoRevoke::scheduler::entry:1360 [{ followers: Set("c2"), leased: true, worker: "w1" }],1361 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1362 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1363 schedNoRevoke::scheduler::mBuild: Set(),1364 schedNoRevoke::scheduler::mDone: Set(),1365 schedNoRevoke::scheduler::mExpect: Set(),1366 schedNoRevoke::scheduler::mResult: Set(),1367 schedNoRevoke::scheduler::mRetry: Set(),1368 schedNoRevoke::scheduler::mRevoke: Set(),1369 schedNoRevoke::scheduler::mSchedule: Set(),1370 schedNoRevoke::scheduler::published: 0,1371 schedNoRevoke::scheduler::publishedBy: Set(),1372 schedNoRevoke::scheduler::ws:1373 Map(1374 "w1" ->1375 {1376 attached: Set(),1377 built: false,1378 expecting: true,1379 running: true,1380 session: true,1381 up: true1382 },1383 "w2" ->1384 {1385 attached: Set(),1386 built: false,1387 expecting: false,1388 running: false,1389 session: true,1390 up: true1391 }1392 )1393}13941395[State 4]1396{1397 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1398 schedNoRevoke::scheduler::crashes: 1,1399 schedNoRevoke::scheduler::entry: [],1400 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1401 schedNoRevoke::scheduler::mAssigned: Set(),1402 schedNoRevoke::scheduler::mBuild: Set(),1403 schedNoRevoke::scheduler::mDone: Set(),1404 schedNoRevoke::scheduler::mExpect: Set(),1405 schedNoRevoke::scheduler::mResult: Set(),1406 schedNoRevoke::scheduler::mRetry: Set("c2"),1407 schedNoRevoke::scheduler::mRevoke: Set(),1408 schedNoRevoke::scheduler::mSchedule: Set(),1409 schedNoRevoke::scheduler::published: 0,1410 schedNoRevoke::scheduler::publishedBy: Set(),1411 schedNoRevoke::scheduler::ws:1412 Map(1413 "w1" ->1414 {1415 attached: Set(),1416 built: false,1417 expecting: true,1418 running: true,1419 session: false,1420 up: true1421 },1422 "w2" ->1423 {1424 attached: Set(),1425 built: false,1426 expecting: false,1427 running: false,1428 session: false,1429 up: true1430 }1431 )1432}14331434[State 5]1435{1436 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1437 schedNoRevoke::scheduler::crashes: 2,1438 schedNoRevoke::scheduler::entry: [],1439 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1440 schedNoRevoke::scheduler::mAssigned: Set(),1441 schedNoRevoke::scheduler::mBuild: Set(),1442 schedNoRevoke::scheduler::mDone: Set(),1443 schedNoRevoke::scheduler::mExpect: Set(),1444 schedNoRevoke::scheduler::mResult: Set(),1445 schedNoRevoke::scheduler::mRetry: Set("c2"),1446 schedNoRevoke::scheduler::mRevoke: Set(),1447 schedNoRevoke::scheduler::mSchedule: Set(),1448 schedNoRevoke::scheduler::published: 0,1449 schedNoRevoke::scheduler::publishedBy: Set(),1450 schedNoRevoke::scheduler::ws:1451 Map(1452 "w1" ->1453 {1454 attached: Set(),1455 built: false,1456 expecting: true,1457 running: true,1458 session: false,1459 up: true1460 },1461 "w2" ->1462 {1463 attached: Set(),1464 built: false,1465 expecting: false,1466 running: false,1467 session: false,1468 up: false1469 }1470 )1471}14721473[State 6]1474{1475 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1476 schedNoRevoke::scheduler::crashes: 2,1477 schedNoRevoke::scheduler::entry: [],1478 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1479 schedNoRevoke::scheduler::mAssigned: Set(),1480 schedNoRevoke::scheduler::mBuild: Set(),1481 schedNoRevoke::scheduler::mDone: Set(),1482 schedNoRevoke::scheduler::mExpect: Set(),1483 schedNoRevoke::scheduler::mResult: Set(),1484 schedNoRevoke::scheduler::mRetry: Set("c2"),1485 schedNoRevoke::scheduler::mRevoke: Set(),1486 schedNoRevoke::scheduler::mSchedule: Set("c1"),1487 schedNoRevoke::scheduler::published: 0,1488 schedNoRevoke::scheduler::publishedBy: Set(),1489 schedNoRevoke::scheduler::ws:1490 Map(1491 "w1" ->1492 {1493 attached: Set(),1494 built: false,1495 expecting: true,1496 running: true,1497 session: false,1498 up: true1499 },1500 "w2" ->1501 {1502 attached: Set(),1503 built: false,1504 expecting: false,1505 running: false,1506 session: false,1507 up: false1508 }1509 )1510}15111512[State 7]1513{1514 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1515 schedNoRevoke::scheduler::crashes: 2,1516 schedNoRevoke::scheduler::entry: [],1517 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1518 schedNoRevoke::scheduler::mAssigned: Set(),1519 schedNoRevoke::scheduler::mBuild: Set(),1520 schedNoRevoke::scheduler::mDone: Set(),1521 schedNoRevoke::scheduler::mExpect: Set(),1522 schedNoRevoke::scheduler::mResult: Set(),1523 schedNoRevoke::scheduler::mRetry: Set("c2"),1524 schedNoRevoke::scheduler::mRevoke: Set(),1525 schedNoRevoke::scheduler::mSchedule: Set("c1"),1526 schedNoRevoke::scheduler::published: 0,1527 schedNoRevoke::scheduler::publishedBy: Set(),1528 schedNoRevoke::scheduler::ws:1529 Map(1530 "w1" ->1531 {1532 attached: Set(),1533 built: false,1534 expecting: true,1535 running: true,1536 session: false,1537 up: true1538 },1539 "w2" ->1540 {1541 attached: Set(),1542 built: false,1543 expecting: false,1544 running: false,1545 session: true,1546 up: true1547 }1548 )1549}15501551[State 8]1552{1553 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1554 schedNoRevoke::scheduler::crashes: 2,1555 schedNoRevoke::scheduler::entry:1556 [{ followers: Set("c1"), leased: true, worker: "w2" }],1557 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1558 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1559 schedNoRevoke::scheduler::mBuild: Set(),1560 schedNoRevoke::scheduler::mDone: Set(),1561 schedNoRevoke::scheduler::mExpect: Set("w2"),1562 schedNoRevoke::scheduler::mResult: Set(),1563 schedNoRevoke::scheduler::mRetry: Set("c2"),1564 schedNoRevoke::scheduler::mRevoke: Set(),1565 schedNoRevoke::scheduler::mSchedule: Set(),1566 schedNoRevoke::scheduler::published: 0,1567 schedNoRevoke::scheduler::publishedBy: Set(),1568 schedNoRevoke::scheduler::ws:1569 Map(1570 "w1" ->1571 {1572 attached: Set(),1573 built: false,1574 expecting: true,1575 running: true,1576 session: false,1577 up: true1578 },1579 "w2" ->1580 {1581 attached: Set(),1582 built: false,1583 expecting: false,1584 running: false,1585 session: true,1586 up: true1587 }1588 )1589}15901591[State 9]1592{1593 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1594 schedNoRevoke::scheduler::crashes: 2,1595 schedNoRevoke::scheduler::entry:1596 [{ followers: Set("c1"), leased: true, worker: "w2" }],1597 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1598 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1599 schedNoRevoke::scheduler::mBuild: Set(),1600 schedNoRevoke::scheduler::mDone: Set(),1601 schedNoRevoke::scheduler::mExpect: Set("w2"),1602 schedNoRevoke::scheduler::mResult: Set(),1603 schedNoRevoke::scheduler::mRetry: Set("c2"),1604 schedNoRevoke::scheduler::mRevoke: Set(),1605 schedNoRevoke::scheduler::mSchedule: Set(),1606 schedNoRevoke::scheduler::published: 0,1607 schedNoRevoke::scheduler::publishedBy: Set(),1608 schedNoRevoke::scheduler::ws:1609 Map(1610 "w1" ->1611 {1612 attached: Set(),1613 built: false,1614 expecting: true,1615 running: true,1616 session: true,1617 up: true1618 },1619 "w2" ->1620 {1621 attached: Set(),1622 built: false,1623 expecting: false,1624 running: false,1625 session: true,1626 up: true1627 }1628 )1629}16301631[State 10]1632{1633 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1634 schedNoRevoke::scheduler::crashes: 2,1635 schedNoRevoke::scheduler::entry:1636 [{ followers: Set("c1"), leased: true, worker: "w2" }],1637 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1638 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1639 schedNoRevoke::scheduler::mBuild: Set(),1640 schedNoRevoke::scheduler::mDone: Set(),1641 schedNoRevoke::scheduler::mExpect: Set(),1642 schedNoRevoke::scheduler::mResult: Set(),1643 schedNoRevoke::scheduler::mRetry: Set("c2"),1644 schedNoRevoke::scheduler::mRevoke: Set(),1645 schedNoRevoke::scheduler::mSchedule: Set(),1646 schedNoRevoke::scheduler::published: 0,1647 schedNoRevoke::scheduler::publishedBy: Set(),1648 schedNoRevoke::scheduler::ws:1649 Map(1650 "w1" ->1651 {1652 attached: Set(),1653 built: false,1654 expecting: true,1655 running: true,1656 session: true,1657 up: true1658 },1659 "w2" ->1660 {1661 attached: Set(),1662 built: false,1663 expecting: true,1664 running: true,1665 session: true,1666 up: true1667 }1668 )1669}16701671[violation] Found an issue (509ms at 57057 traces/second).1672Use --verbosity=3 to show executions.1673Use --seed=0x40fa2796d394874f --backend=rust to reproduce.1674error: Invariant violated1675An example execution:16761677[State 0]1678{1679 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1680 schedNoFence::scheduler::crashes: 0,1681 schedNoFence::scheduler::entry: [],1682 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1683 schedNoFence::scheduler::mAssigned: Set(),1684 schedNoFence::scheduler::mBuild: Set(),1685 schedNoFence::scheduler::mDone: Set(),1686 schedNoFence::scheduler::mExpect: Set(),1687 schedNoFence::scheduler::mResult: Set(),1688 schedNoFence::scheduler::mRetry: Set(),1689 schedNoFence::scheduler::mRevoke: Set(),1690 schedNoFence::scheduler::mSchedule: Set(),1691 schedNoFence::scheduler::published: 0,1692 schedNoFence::scheduler::publishedBy: Set(),1693 schedNoFence::scheduler::ws:1694 Map(1695 "w1" ->1696 {1697 attached: Set(),1698 built: false,1699 expecting: false,1700 running: false,1701 session: true,1702 up: true1703 },1704 "w2" ->1705 {1706 attached: Set(),1707 built: false,1708 expecting: false,1709 running: false,1710 session: true,1711 up: true1712 }1713 )1714}17151716[State 1]1717{1718 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1719 schedNoFence::scheduler::crashes: 0,1720 schedNoFence::scheduler::entry: [],1721 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1722 schedNoFence::scheduler::mAssigned: Set(),1723 schedNoFence::scheduler::mBuild: Set(),1724 schedNoFence::scheduler::mDone: Set(),1725 schedNoFence::scheduler::mExpect: Set(),1726 schedNoFence::scheduler::mResult: Set(),1727 schedNoFence::scheduler::mRetry: Set(),1728 schedNoFence::scheduler::mRevoke: Set(),1729 schedNoFence::scheduler::mSchedule: Set("c2"),1730 schedNoFence::scheduler::published: 0,1731 schedNoFence::scheduler::publishedBy: Set(),1732 schedNoFence::scheduler::ws:1733 Map(1734 "w1" ->1735 {1736 attached: Set(),1737 built: false,1738 expecting: false,1739 running: false,1740 session: true,1741 up: true1742 },1743 "w2" ->1744 {1745 attached: Set(),1746 built: false,1747 expecting: false,1748 running: false,1749 session: true,1750 up: true1751 }1752 )1753}17541755[State 2]1756{1757 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1758 schedNoFence::scheduler::crashes: 0,1759 schedNoFence::scheduler::entry:1760 [{ followers: Set("c2"), leased: true, worker: "w2" }],1761 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1762 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1763 schedNoFence::scheduler::mBuild: Set(),1764 schedNoFence::scheduler::mDone: Set(),1765 schedNoFence::scheduler::mExpect: Set("w2"),1766 schedNoFence::scheduler::mResult: Set(),1767 schedNoFence::scheduler::mRetry: Set(),1768 schedNoFence::scheduler::mRevoke: Set(),1769 schedNoFence::scheduler::mSchedule: Set(),1770 schedNoFence::scheduler::published: 0,1771 schedNoFence::scheduler::publishedBy: Set(),1772 schedNoFence::scheduler::ws:1773 Map(1774 "w1" ->1775 {1776 attached: Set(),1777 built: false,1778 expecting: false,1779 running: false,1780 session: true,1781 up: true1782 },1783 "w2" ->1784 {1785 attached: Set(),1786 built: false,1787 expecting: false,1788 running: false,1789 session: true,1790 up: true1791 }1792 )1793}17941795[State 3]1796{1797 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1798 schedNoFence::scheduler::crashes: 0,1799 schedNoFence::scheduler::entry:1800 [{ followers: Set("c2"), leased: true, worker: "w2" }],1801 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1802 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1803 schedNoFence::scheduler::mBuild: Set(),1804 schedNoFence::scheduler::mDone: Set(),1805 schedNoFence::scheduler::mExpect: Set(),1806 schedNoFence::scheduler::mResult: Set(),1807 schedNoFence::scheduler::mRetry: Set(),1808 schedNoFence::scheduler::mRevoke: Set(),1809 schedNoFence::scheduler::mSchedule: Set(),1810 schedNoFence::scheduler::published: 0,1811 schedNoFence::scheduler::publishedBy: Set(),1812 schedNoFence::scheduler::ws:1813 Map(1814 "w1" ->1815 {1816 attached: Set(),1817 built: false,1818 expecting: false,1819 running: false,1820 session: true,1821 up: true1822 },1823 "w2" ->1824 {1825 attached: Set(),1826 built: false,1827 expecting: true,1828 running: true,1829 session: true,1830 up: true1831 }1832 )1833}18341835[State 4]1836{1837 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1838 schedNoFence::scheduler::crashes: 1,1839 schedNoFence::scheduler::entry: [],1840 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1841 schedNoFence::scheduler::mAssigned: Set(),1842 schedNoFence::scheduler::mBuild: Set(),1843 schedNoFence::scheduler::mDone: Set(),1844 schedNoFence::scheduler::mExpect: Set(),1845 schedNoFence::scheduler::mResult: Set(),1846 schedNoFence::scheduler::mRetry: Set("c2"),1847 schedNoFence::scheduler::mRevoke: Set(),1848 schedNoFence::scheduler::mSchedule: Set(),1849 schedNoFence::scheduler::published: 0,1850 schedNoFence::scheduler::publishedBy: Set(),1851 schedNoFence::scheduler::ws:1852 Map(1853 "w1" ->1854 {1855 attached: Set(),1856 built: false,1857 expecting: false,1858 running: false,1859 session: false,1860 up: true1861 },1862 "w2" ->1863 {1864 attached: Set(),1865 built: false,1866 expecting: true,1867 running: true,1868 session: false,1869 up: true1870 }1871 )1872}18731874[State 5]1875{1876 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1877 schedNoFence::scheduler::crashes: 2,1878 schedNoFence::scheduler::entry: [],1879 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1880 schedNoFence::scheduler::mAssigned: Set(),1881 schedNoFence::scheduler::mBuild: Set(),1882 schedNoFence::scheduler::mDone: Set(),1883 schedNoFence::scheduler::mExpect: Set(),1884 schedNoFence::scheduler::mResult: Set(),1885 schedNoFence::scheduler::mRetry: Set("c2"),1886 schedNoFence::scheduler::mRevoke: Set(),1887 schedNoFence::scheduler::mSchedule: Set(),1888 schedNoFence::scheduler::published: 0,1889 schedNoFence::scheduler::publishedBy: Set(),1890 schedNoFence::scheduler::ws:1891 Map(1892 "w1" ->1893 {1894 attached: Set(),1895 built: false,1896 expecting: false,1897 running: false,1898 session: false,1899 up: false1900 },1901 "w2" ->1902 {1903 attached: Set(),1904 built: false,1905 expecting: true,1906 running: true,1907 session: false,1908 up: true1909 }1910 )1911}19121913[State 6]1914{1915 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1916 schedNoFence::scheduler::crashes: 2,1917 schedNoFence::scheduler::entry: [],1918 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1919 schedNoFence::scheduler::mAssigned: Set(),1920 schedNoFence::scheduler::mBuild: Set(),1921 schedNoFence::scheduler::mDone: Set(),1922 schedNoFence::scheduler::mExpect: Set(),1923 schedNoFence::scheduler::mResult: Set(),1924 schedNoFence::scheduler::mRetry: Set("c2"),1925 schedNoFence::scheduler::mRevoke: Set(),1926 schedNoFence::scheduler::mSchedule: Set(),1927 schedNoFence::scheduler::published: 0,1928 schedNoFence::scheduler::publishedBy: Set(),1929 schedNoFence::scheduler::ws:1930 Map(1931 "w1" ->1932 {1933 attached: Set(),1934 built: false,1935 expecting: false,1936 running: false,1937 session: true,1938 up: true1939 },1940 "w2" ->1941 {1942 attached: Set(),1943 built: false,1944 expecting: true,1945 running: true,1946 session: false,1947 up: true1948 }1949 )1950}19511952[State 7]1953{1954 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1955 schedNoFence::scheduler::crashes: 2,1956 schedNoFence::scheduler::entry: [],1957 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1958 schedNoFence::scheduler::mAssigned: Set(),1959 schedNoFence::scheduler::mBuild: Set(),1960 schedNoFence::scheduler::mDone: Set(),1961 schedNoFence::scheduler::mExpect: Set(),1962 schedNoFence::scheduler::mResult: Set(),1963 schedNoFence::scheduler::mRetry: Set("c2"),1964 schedNoFence::scheduler::mRevoke: Set(),1965 schedNoFence::scheduler::mSchedule: Set("c1"),1966 schedNoFence::scheduler::published: 0,1967 schedNoFence::scheduler::publishedBy: Set(),1968 schedNoFence::scheduler::ws:1969 Map(1970 "w1" ->1971 {1972 attached: Set(),1973 built: false,1974 expecting: false,1975 running: false,1976 session: true,1977 up: true1978 },1979 "w2" ->1980 {1981 attached: Set(),1982 built: false,1983 expecting: true,1984 running: true,1985 session: false,1986 up: true1987 }1988 )1989}19901991[State 8]1992{1993 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1994 schedNoFence::scheduler::crashes: 2,1995 schedNoFence::scheduler::entry:1996 [{ followers: Set("c1"), leased: true, worker: "w1" }],1997 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1998 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1999 schedNoFence::scheduler::mBuild: Set(),2000 schedNoFence::scheduler::mDone: Set(),2001 schedNoFence::scheduler::mExpect: Set("w1"),2002 schedNoFence::scheduler::mResult: Set(),2003 schedNoFence::scheduler::mRetry: Set("c2"),2004 schedNoFence::scheduler::mRevoke: Set(),2005 schedNoFence::scheduler::mSchedule: Set(),2006 schedNoFence::scheduler::published: 0,2007 schedNoFence::scheduler::publishedBy: Set(),2008 schedNoFence::scheduler::ws:2009 Map(2010 "w1" ->2011 {2012 attached: Set(),2013 built: false,2014 expecting: false,2015 running: false,2016 session: true,2017 up: true2018 },2019 "w2" ->2020 {2021 attached: Set(),2022 built: false,2023 expecting: true,2024 running: true,2025 session: false,2026 up: true2027 }2028 )2029}20302031[State 9]2032{2033 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2034 schedNoFence::scheduler::crashes: 2,2035 schedNoFence::scheduler::entry:2036 [{ followers: Set("c1"), leased: true, worker: "w1" }],2037 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2038 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2039 schedNoFence::scheduler::mBuild: Set(),2040 schedNoFence::scheduler::mDone: Set(),2041 schedNoFence::scheduler::mExpect: Set(),2042 schedNoFence::scheduler::mResult: Set(),2043 schedNoFence::scheduler::mRetry: Set("c2"),2044 schedNoFence::scheduler::mRevoke: Set(),2045 schedNoFence::scheduler::mSchedule: Set(),2046 schedNoFence::scheduler::published: 0,2047 schedNoFence::scheduler::publishedBy: Set(),2048 schedNoFence::scheduler::ws:2049 Map(2050 "w1" ->2051 {2052 attached: Set(),2053 built: false,2054 expecting: true,2055 running: true,2056 session: true,2057 up: true2058 },2059 "w2" ->2060 {2061 attached: Set(),2062 built: false,2063 expecting: true,2064 running: true,2065 session: false,2066 up: true2067 }2068 )2069}20702071[State 10]2072{2073 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2074 schedNoFence::scheduler::crashes: 2,2075 schedNoFence::scheduler::entry:2076 [{ followers: Set("c1"), leased: true, worker: "w1" }],2077 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2078 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2079 schedNoFence::scheduler::mBuild: Set(),2080 schedNoFence::scheduler::mDone: Set("w1"),2081 schedNoFence::scheduler::mExpect: Set(),2082 schedNoFence::scheduler::mResult: Set(),2083 schedNoFence::scheduler::mRetry: Set("c2"),2084 schedNoFence::scheduler::mRevoke: Set(),2085 schedNoFence::scheduler::mSchedule: Set(),2086 schedNoFence::scheduler::published: 1,2087 schedNoFence::scheduler::publishedBy: Set("w1"),2088 schedNoFence::scheduler::ws:2089 Map(2090 "w1" ->2091 {2092 attached: Set(),2093 built: true,2094 expecting: false,2095 running: false,2096 session: true,2097 up: true2098 },2099 "w2" ->2100 {2101 attached: Set(),2102 built: false,2103 expecting: true,2104 running: true,2105 session: false,2106 up: true2107 }2108 )2109}21102111[State 11]2112{2113 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2114 schedNoFence::scheduler::crashes: 2,2115 schedNoFence::scheduler::entry:2116 [{ followers: Set("c1"), leased: true, worker: "w1" }],2117 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2118 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2119 schedNoFence::scheduler::mBuild: Set(),2120 schedNoFence::scheduler::mDone: Set("w1"),2121 schedNoFence::scheduler::mExpect: Set(),2122 schedNoFence::scheduler::mResult: Set(),2123 schedNoFence::scheduler::mRetry: Set("c2"),2124 schedNoFence::scheduler::mRevoke: Set(),2125 schedNoFence::scheduler::mSchedule: Set(),2126 schedNoFence::scheduler::published: 2,2127 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2128 schedNoFence::scheduler::ws:2129 Map(2130 "w1" ->2131 {2132 attached: Set(),2133 built: true,2134 expecting: false,2135 running: false,2136 session: true,2137 up: true2138 },2139 "w2" ->2140 {2141 attached: Set(),2142 built: true,2143 expecting: false,2144 running: false,2145 session: false,2146 up: true2147 }2148 )2149}21502151[violation] Found an issue (491ms at 55927 traces/second).2152Use --verbosity=3 to show executions.2153Use --seed=0xf6c2b68e73302ecf --backend=rust to reproduce.2154error: Invariant violated2155An example execution:21562157[State 0]2158{2159 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2160 schedNoPush::scheduler::crashes: 0,2161 schedNoPush::scheduler::entry: [],2162 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2163 schedNoPush::scheduler::mAssigned: Set(),2164 schedNoPush::scheduler::mBuild: Set(),2165 schedNoPush::scheduler::mDone: Set(),2166 schedNoPush::scheduler::mExpect: Set(),2167 schedNoPush::scheduler::mResult: Set(),2168 schedNoPush::scheduler::mRetry: Set(),2169 schedNoPush::scheduler::mRevoke: Set(),2170 schedNoPush::scheduler::mSchedule: Set(),2171 schedNoPush::scheduler::published: 0,2172 schedNoPush::scheduler::publishedBy: Set(),2173 schedNoPush::scheduler::ws:2174 Map(2175 "w1" ->2176 {2177 attached: Set(),2178 built: false,2179 expecting: false,2180 running: false,2181 session: true,2182 up: true2183 },2184 "w2" ->2185 {2186 attached: Set(),2187 built: false,2188 expecting: false,2189 running: false,2190 session: true,2191 up: true2192 }2193 )2194}21952196[State 1]2197{2198 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2199 schedNoPush::scheduler::crashes: 0,2200 schedNoPush::scheduler::entry: [],2201 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2202 schedNoPush::scheduler::mAssigned: Set(),2203 schedNoPush::scheduler::mBuild: Set(),2204 schedNoPush::scheduler::mDone: Set(),2205 schedNoPush::scheduler::mExpect: Set(),2206 schedNoPush::scheduler::mResult: Set(),2207 schedNoPush::scheduler::mRetry: Set(),2208 schedNoPush::scheduler::mRevoke: Set(),2209 schedNoPush::scheduler::mSchedule: Set("c1"),2210 schedNoPush::scheduler::published: 0,2211 schedNoPush::scheduler::publishedBy: Set(),2212 schedNoPush::scheduler::ws:2213 Map(2214 "w1" ->2215 {2216 attached: Set(),2217 built: false,2218 expecting: false,2219 running: false,2220 session: true,2221 up: true2222 },2223 "w2" ->2224 {2225 attached: Set(),2226 built: false,2227 expecting: false,2228 running: false,2229 session: true,2230 up: true2231 }2232 )2233}22342235[State 2]2236{2237 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2238 schedNoPush::scheduler::crashes: 0,2239 schedNoPush::scheduler::entry:2240 [{ followers: Set("c1"), leased: true, worker: "w2" }],2241 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2242 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2243 schedNoPush::scheduler::mBuild: Set(),2244 schedNoPush::scheduler::mDone: Set(),2245 schedNoPush::scheduler::mExpect: Set(),2246 schedNoPush::scheduler::mResult: Set(),2247 schedNoPush::scheduler::mRetry: Set(),2248 schedNoPush::scheduler::mRevoke: Set(),2249 schedNoPush::scheduler::mSchedule: Set(),2250 schedNoPush::scheduler::published: 0,2251 schedNoPush::scheduler::publishedBy: Set(),2252 schedNoPush::scheduler::ws:2253 Map(2254 "w1" ->2255 {2256 attached: Set(),2257 built: false,2258 expecting: false,2259 running: false,2260 session: true,2261 up: true2262 },2263 "w2" ->2264 {2265 attached: Set(),2266 built: false,2267 expecting: false,2268 running: false,2269 session: true,2270 up: true2271 }2272 )2273}22742275[State 3]2276{2277 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2278 schedNoPush::scheduler::crashes: 0,2279 schedNoPush::scheduler::entry:2280 [{ followers: Set("c1"), leased: true, worker: "w2" }],2281 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2282 schedNoPush::scheduler::mAssigned: Set(),2283 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2284 schedNoPush::scheduler::mDone: Set(),2285 schedNoPush::scheduler::mExpect: Set(),2286 schedNoPush::scheduler::mResult: Set(),2287 schedNoPush::scheduler::mRetry: Set(),2288 schedNoPush::scheduler::mRevoke: Set(),2289 schedNoPush::scheduler::mSchedule: Set(),2290 schedNoPush::scheduler::published: 0,2291 schedNoPush::scheduler::publishedBy: Set(),2292 schedNoPush::scheduler::ws:2293 Map(2294 "w1" ->2295 {2296 attached: Set(),2297 built: false,2298 expecting: false,2299 running: false,2300 session: true,2301 up: true2302 },2303 "w2" ->2304 {2305 attached: Set(),2306 built: false,2307 expecting: false,2308 running: false,2309 session: true,2310 up: true2311 }2312 )2313}23142315[State 4]2316{2317 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2318 schedNoPush::scheduler::crashes: 1,2319 schedNoPush::scheduler::entry: [],2320 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2321 schedNoPush::scheduler::mAssigned: Set(),2322 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2323 schedNoPush::scheduler::mDone: Set(),2324 schedNoPush::scheduler::mExpect: Set(),2325 schedNoPush::scheduler::mResult: Set(),2326 schedNoPush::scheduler::mRetry: Set(),2327 schedNoPush::scheduler::mRevoke: Set(),2328 schedNoPush::scheduler::mSchedule: Set(),2329 schedNoPush::scheduler::published: 0,2330 schedNoPush::scheduler::publishedBy: Set(),2331 schedNoPush::scheduler::ws:2332 Map(2333 "w1" ->2334 {2335 attached: Set(),2336 built: false,2337 expecting: false,2338 running: false,2339 session: false,2340 up: true2341 },2342 "w2" ->2343 {2344 attached: Set(),2345 built: false,2346 expecting: false,2347 running: false,2348 session: false,2349 up: true2350 }2351 )2352}23532354[State 5]2355{2356 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2357 schedNoPush::scheduler::crashes: 2,2358 schedNoPush::scheduler::entry: [],2359 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2360 schedNoPush::scheduler::mAssigned: Set(),2361 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2362 schedNoPush::scheduler::mDone: Set(),2363 schedNoPush::scheduler::mExpect: Set(),2364 schedNoPush::scheduler::mResult: Set(),2365 schedNoPush::scheduler::mRetry: Set(),2366 schedNoPush::scheduler::mRevoke: Set(),2367 schedNoPush::scheduler::mSchedule: Set(),2368 schedNoPush::scheduler::published: 0,2369 schedNoPush::scheduler::publishedBy: Set(),2370 schedNoPush::scheduler::ws:2371 Map(2372 "w1" ->2373 {2374 attached: Set(),2375 built: false,2376 expecting: false,2377 running: false,2378 session: false,2379 up: true2380 },2381 "w2" ->2382 {2383 attached: Set(),2384 built: false,2385 expecting: false,2386 running: false,2387 session: false,2388 up: false2389 }2390 )2391}23922393[State 6]2394{2395 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2396 schedNoPush::scheduler::crashes: 2,2397 schedNoPush::scheduler::entry: [],2398 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2399 schedNoPush::scheduler::mAssigned: Set(),2400 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2401 schedNoPush::scheduler::mDone: Set(),2402 schedNoPush::scheduler::mExpect: Set(),2403 schedNoPush::scheduler::mResult: Set(),2404 schedNoPush::scheduler::mRetry: Set(),2405 schedNoPush::scheduler::mRevoke: Set(),2406 schedNoPush::scheduler::mSchedule: Set(),2407 schedNoPush::scheduler::published: 0,2408 schedNoPush::scheduler::publishedBy: Set(),2409 schedNoPush::scheduler::ws:2410 Map(2411 "w1" ->2412 {2413 attached: Set(),2414 built: false,2415 expecting: false,2416 running: false,2417 session: false,2418 up: true2419 },2420 "w2" ->2421 {2422 attached: Set(),2423 built: false,2424 expecting: false,2425 running: false,2426 session: true,2427 up: true2428 }2429 )2430}24312432[State 7]2433{2434 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2435 schedNoPush::scheduler::crashes: 2,2436 schedNoPush::scheduler::entry: [],2437 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2438 schedNoPush::scheduler::mAssigned: Set(),2439 schedNoPush::scheduler::mBuild: Set(),2440 schedNoPush::scheduler::mDone: Set(),2441 schedNoPush::scheduler::mExpect: Set(),2442 schedNoPush::scheduler::mResult: Set(),2443 schedNoPush::scheduler::mRetry: Set(),2444 schedNoPush::scheduler::mRevoke: Set(),2445 schedNoPush::scheduler::mSchedule: Set(),2446 schedNoPush::scheduler::published: 0,2447 schedNoPush::scheduler::publishedBy: Set(),2448 schedNoPush::scheduler::ws:2449 Map(2450 "w1" ->2451 {2452 attached: Set(),2453 built: false,2454 expecting: false,2455 running: false,2456 session: false,2457 up: true2458 },2459 "w2" ->2460 {2461 attached: Set("c1"),2462 built: false,2463 expecting: true,2464 running: true,2465 session: true,2466 up: true2467 }2468 )2469}24702471[violation] Found an issue (366ms at 47082 traces/second).2472Use --verbosity=3 to show executions.2473Use --seed=0x6bd5b97240cdb44e --backend=rust to reproduce.2474error: Invariant violated2475An example execution:24762477[State 0]2478{2479 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2480 schedNoReport::scheduler::crashes: 0,2481 schedNoReport::scheduler::entry: [],2482 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2483 schedNoReport::scheduler::mAssigned: Set(),2484 schedNoReport::scheduler::mBuild: Set(),2485 schedNoReport::scheduler::mDone: Set(),2486 schedNoReport::scheduler::mExpect: Set(),2487 schedNoReport::scheduler::mResult: Set(),2488 schedNoReport::scheduler::mRetry: Set(),2489 schedNoReport::scheduler::mRevoke: Set(),2490 schedNoReport::scheduler::mSchedule: Set(),2491 schedNoReport::scheduler::published: 0,2492 schedNoReport::scheduler::publishedBy: Set(),2493 schedNoReport::scheduler::ws:2494 Map(2495 "w1" ->2496 {2497 attached: Set(),2498 built: false,2499 expecting: false,2500 running: false,2501 session: true,2502 up: true2503 },2504 "w2" ->2505 {2506 attached: Set(),2507 built: false,2508 expecting: false,2509 running: false,2510 session: true,2511 up: true2512 }2513 )2514}25152516[State 1]2517{2518 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2519 schedNoReport::scheduler::crashes: 0,2520 schedNoReport::scheduler::entry: [],2521 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2522 schedNoReport::scheduler::mAssigned: Set(),2523 schedNoReport::scheduler::mBuild: Set(),2524 schedNoReport::scheduler::mDone: Set(),2525 schedNoReport::scheduler::mExpect: Set(),2526 schedNoReport::scheduler::mResult: Set(),2527 schedNoReport::scheduler::mRetry: Set(),2528 schedNoReport::scheduler::mRevoke: Set(),2529 schedNoReport::scheduler::mSchedule: Set("c2"),2530 schedNoReport::scheduler::published: 0,2531 schedNoReport::scheduler::publishedBy: Set(),2532 schedNoReport::scheduler::ws:2533 Map(2534 "w1" ->2535 {2536 attached: Set(),2537 built: false,2538 expecting: false,2539 running: false,2540 session: true,2541 up: true2542 },2543 "w2" ->2544 {2545 attached: Set(),2546 built: false,2547 expecting: false,2548 running: false,2549 session: true,2550 up: true2551 }2552 )2553}25542555[State 2]2556{2557 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2558 schedNoReport::scheduler::crashes: 0,2559 schedNoReport::scheduler::entry:2560 [{ followers: Set("c2"), leased: true, worker: "w2" }],2561 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2562 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2563 schedNoReport::scheduler::mBuild: Set(),2564 schedNoReport::scheduler::mDone: Set(),2565 schedNoReport::scheduler::mExpect: Set("w2"),2566 schedNoReport::scheduler::mResult: Set(),2567 schedNoReport::scheduler::mRetry: Set(),2568 schedNoReport::scheduler::mRevoke: Set(),2569 schedNoReport::scheduler::mSchedule: Set(),2570 schedNoReport::scheduler::published: 0,2571 schedNoReport::scheduler::publishedBy: Set(),2572 schedNoReport::scheduler::ws:2573 Map(2574 "w1" ->2575 {2576 attached: Set(),2577 built: false,2578 expecting: false,2579 running: false,2580 session: true,2581 up: true2582 },2583 "w2" ->2584 {2585 attached: Set(),2586 built: false,2587 expecting: false,2588 running: false,2589 session: true,2590 up: true2591 }2592 )2593}25942595[State 3]2596{2597 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2598 schedNoReport::scheduler::crashes: 0,2599 schedNoReport::scheduler::entry:2600 [{ followers: Set("c2"), leased: true, worker: "w2" }],2601 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2602 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2603 schedNoReport::scheduler::mBuild: Set(),2604 schedNoReport::scheduler::mDone: Set(),2605 schedNoReport::scheduler::mExpect: Set(),2606 schedNoReport::scheduler::mResult: Set(),2607 schedNoReport::scheduler::mRetry: Set(),2608 schedNoReport::scheduler::mRevoke: Set(),2609 schedNoReport::scheduler::mSchedule: Set(),2610 schedNoReport::scheduler::published: 0,2611 schedNoReport::scheduler::publishedBy: Set(),2612 schedNoReport::scheduler::ws:2613 Map(2614 "w1" ->2615 {2616 attached: Set(),2617 built: false,2618 expecting: false,2619 running: false,2620 session: true,2621 up: true2622 },2623 "w2" ->2624 {2625 attached: Set(),2626 built: false,2627 expecting: true,2628 running: true,2629 session: true,2630 up: true2631 }2632 )2633}26342635[State 4]2636{2637 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2638 schedNoReport::scheduler::crashes: 1,2639 schedNoReport::scheduler::entry: [],2640 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2641 schedNoReport::scheduler::mAssigned: Set(),2642 schedNoReport::scheduler::mBuild: Set(),2643 schedNoReport::scheduler::mDone: Set(),2644 schedNoReport::scheduler::mExpect: Set(),2645 schedNoReport::scheduler::mResult: Set(),2646 schedNoReport::scheduler::mRetry: Set("c2"),2647 schedNoReport::scheduler::mRevoke: Set(),2648 schedNoReport::scheduler::mSchedule: Set(),2649 schedNoReport::scheduler::published: 0,2650 schedNoReport::scheduler::publishedBy: Set(),2651 schedNoReport::scheduler::ws:2652 Map(2653 "w1" ->2654 {2655 attached: Set(),2656 built: false,2657 expecting: false,2658 running: false,2659 session: false,2660 up: true2661 },2662 "w2" ->2663 {2664 attached: Set(),2665 built: false,2666 expecting: true,2667 running: true,2668 session: false,2669 up: true2670 }2671 )2672}26732674[State 5]2675{2676 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2677 schedNoReport::scheduler::crashes: 2,2678 schedNoReport::scheduler::entry: [],2679 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2680 schedNoReport::scheduler::mAssigned: Set(),2681 schedNoReport::scheduler::mBuild: Set(),2682 schedNoReport::scheduler::mDone: Set(),2683 schedNoReport::scheduler::mExpect: Set(),2684 schedNoReport::scheduler::mResult: Set(),2685 schedNoReport::scheduler::mRetry: Set("c2"),2686 schedNoReport::scheduler::mRevoke: Set(),2687 schedNoReport::scheduler::mSchedule: Set(),2688 schedNoReport::scheduler::published: 0,2689 schedNoReport::scheduler::publishedBy: Set(),2690 schedNoReport::scheduler::ws:2691 Map(2692 "w1" ->2693 {2694 attached: Set(),2695 built: false,2696 expecting: false,2697 running: false,2698 session: false,2699 up: true2700 },2701 "w2" ->2702 {2703 attached: Set(),2704 built: false,2705 expecting: true,2706 running: true,2707 session: false,2708 up: true2709 }2710 )2711}27122713[State 6]2714{2715 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2716 schedNoReport::scheduler::crashes: 2,2717 schedNoReport::scheduler::entry: [],2718 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2719 schedNoReport::scheduler::mAssigned: Set(),2720 schedNoReport::scheduler::mBuild: Set(),2721 schedNoReport::scheduler::mDone: Set(),2722 schedNoReport::scheduler::mExpect: Set(),2723 schedNoReport::scheduler::mResult: Set(),2724 schedNoReport::scheduler::mRetry: Set("c2"),2725 schedNoReport::scheduler::mRevoke: Set(),2726 schedNoReport::scheduler::mSchedule: Set(),2727 schedNoReport::scheduler::published: 0,2728 schedNoReport::scheduler::publishedBy: Set(),2729 schedNoReport::scheduler::ws:2730 Map(2731 "w1" ->2732 {2733 attached: Set(),2734 built: false,2735 expecting: false,2736 running: false,2737 session: false,2738 up: true2739 },2740 "w2" ->2741 {2742 attached: Set(),2743 built: false,2744 expecting: true,2745 running: true,2746 session: true,2747 up: true2748 }2749 )2750}27512752[State 7]2753{2754 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2755 schedNoReport::scheduler::crashes: 2,2756 schedNoReport::scheduler::entry: [],2757 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2758 schedNoReport::scheduler::mAssigned: Set(),2759 schedNoReport::scheduler::mBuild: Set(),2760 schedNoReport::scheduler::mDone: Set(),2761 schedNoReport::scheduler::mExpect: Set(),2762 schedNoReport::scheduler::mResult: Set(),2763 schedNoReport::scheduler::mRetry: Set("c2"),2764 schedNoReport::scheduler::mRevoke: Set(),2765 schedNoReport::scheduler::mSchedule: Set(),2766 schedNoReport::scheduler::published: 0,2767 schedNoReport::scheduler::publishedBy: Set(),2768 schedNoReport::scheduler::ws:2769 Map(2770 "w1" ->2771 {2772 attached: Set(),2773 built: false,2774 expecting: false,2775 running: false,2776 session: true,2777 up: true2778 },2779 "w2" ->2780 {2781 attached: Set(),2782 built: false,2783 expecting: true,2784 running: true,2785 session: true,2786 up: true2787 }2788 )2789}27902791[State 8]2792{2793 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2794 schedNoReport::scheduler::crashes: 2,2795 schedNoReport::scheduler::entry: [],2796 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2797 schedNoReport::scheduler::mAssigned: Set(),2798 schedNoReport::scheduler::mBuild: Set(),2799 schedNoReport::scheduler::mDone: Set(),2800 schedNoReport::scheduler::mExpect: Set(),2801 schedNoReport::scheduler::mResult: Set(),2802 schedNoReport::scheduler::mRetry: Set("c2"),2803 schedNoReport::scheduler::mRevoke: Set(),2804 schedNoReport::scheduler::mSchedule: Set("c1"),2805 schedNoReport::scheduler::published: 0,2806 schedNoReport::scheduler::publishedBy: Set(),2807 schedNoReport::scheduler::ws:2808 Map(2809 "w1" ->2810 {2811 attached: Set(),2812 built: false,2813 expecting: false,2814 running: false,2815 session: true,2816 up: true2817 },2818 "w2" ->2819 {2820 attached: Set(),2821 built: false,2822 expecting: true,2823 running: true,2824 session: true,2825 up: true2826 }2827 )2828}28292830[State 9]2831{2832 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2833 schedNoReport::scheduler::crashes: 2,2834 schedNoReport::scheduler::entry:2835 [{ followers: Set("c1"), leased: true, worker: "w1" }],2836 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2837 schedNoReport::scheduler::mAssigned: Set(("c1", "w1")),2838 schedNoReport::scheduler::mBuild: Set(),2839 schedNoReport::scheduler::mDone: Set(),2840 schedNoReport::scheduler::mExpect: Set("w1"),2841 schedNoReport::scheduler::mResult: Set(),2842 schedNoReport::scheduler::mRetry: Set("c2"),2843 schedNoReport::scheduler::mRevoke: Set(),2844 schedNoReport::scheduler::mSchedule: Set(),2845 schedNoReport::scheduler::published: 0,2846 schedNoReport::scheduler::publishedBy: Set(),2847 schedNoReport::scheduler::ws:2848 Map(2849 "w1" ->2850 {2851 attached: Set(),2852 built: false,2853 expecting: false,2854 running: false,2855 session: true,2856 up: true2857 },2858 "w2" ->2859 {2860 attached: Set(),2861 built: false,2862 expecting: true,2863 running: true,2864 session: true,2865 up: true2866 }2867 )2868}28692870[State 10]2871{2872 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2873 schedNoReport::scheduler::crashes: 2,2874 schedNoReport::scheduler::entry:2875 [{ followers: Set("c1"), leased: true, worker: "w1" }],2876 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2877 schedNoReport::scheduler::mAssigned: Set(("c1", "w1")),2878 schedNoReport::scheduler::mBuild: Set(),2879 schedNoReport::scheduler::mDone: Set(),2880 schedNoReport::scheduler::mExpect: Set(),2881 schedNoReport::scheduler::mResult: Set(),2882 schedNoReport::scheduler::mRetry: Set("c2"),2883 schedNoReport::scheduler::mRevoke: Set(),2884 schedNoReport::scheduler::mSchedule: Set(),2885 schedNoReport::scheduler::published: 0,2886 schedNoReport::scheduler::publishedBy: Set(),2887 schedNoReport::scheduler::ws:2888 Map(2889 "w1" ->2890 {2891 attached: Set(),2892 built: false,2893 expecting: true,2894 running: true,2895 session: true,2896 up: true2897 },2898 "w2" ->2899 {2900 attached: Set(),2901 built: false,2902 expecting: true,2903 running: true,2904 session: true,2905 up: true2906 }2907 )2908}29092910[violation] Found an issue (407ms at 61799 traces/second).2911Use --verbosity=3 to show executions.2912Use --seed=0xe80773eb9ad4a8ad --backend=rust to reproduce.2913error: Invariant violated2914An example execution:29152916[State 0]2917{2918 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2919 schedTerminal::scheduler::crashes: 0,2920 schedTerminal::scheduler::entry: [],2921 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2922 schedTerminal::scheduler::mAssigned: Set(),2923 schedTerminal::scheduler::mBuild: Set(),2924 schedTerminal::scheduler::mDone: Set(),2925 schedTerminal::scheduler::mExpect: Set(),2926 schedTerminal::scheduler::mResult: Set(),2927 schedTerminal::scheduler::mRetry: Set(),2928 schedTerminal::scheduler::mRevoke: Set(),2929 schedTerminal::scheduler::mSchedule: Set(),2930 schedTerminal::scheduler::published: 0,2931 schedTerminal::scheduler::publishedBy: Set(),2932 schedTerminal::scheduler::ws:2933 Map(2934 "w1" ->2935 {2936 attached: Set(),2937 built: false,2938 expecting: false,2939 running: false,2940 session: true,2941 up: true2942 },2943 "w2" ->2944 {2945 attached: Set(),2946 built: false,2947 expecting: false,2948 running: false,2949 session: true,2950 up: true2951 }2952 )2953}29542955[State 1]2956{2957 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2958 schedTerminal::scheduler::crashes: 1,2959 schedTerminal::scheduler::entry: [],2960 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2961 schedTerminal::scheduler::mAssigned: Set(),2962 schedTerminal::scheduler::mBuild: Set(),2963 schedTerminal::scheduler::mDone: Set(),2964 schedTerminal::scheduler::mExpect: Set(),2965 schedTerminal::scheduler::mResult: Set(),2966 schedTerminal::scheduler::mRetry: Set(),2967 schedTerminal::scheduler::mRevoke: Set(),2968 schedTerminal::scheduler::mSchedule: Set(),2969 schedTerminal::scheduler::published: 0,2970 schedTerminal::scheduler::publishedBy: Set(),2971 schedTerminal::scheduler::ws:2972 Map(2973 "w1" ->2974 {2975 attached: Set(),2976 built: false,2977 expecting: false,2978 running: false,2979 session: false,2980 up: true2981 },2982 "w2" ->2983 {2984 attached: Set(),2985 built: false,2986 expecting: false,2987 running: false,2988 session: false,2989 up: true2990 }2991 )2992}29932994[State 2]2995{2996 schedTerminal::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2997 schedTerminal::scheduler::crashes: 1,2998 schedTerminal::scheduler::entry: [],2999 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3000 schedTerminal::scheduler::mAssigned: Set(),3001 schedTerminal::scheduler::mBuild: Set(),3002 schedTerminal::scheduler::mDone: Set(),3003 schedTerminal::scheduler::mExpect: Set(),3004 schedTerminal::scheduler::mResult: Set(),3005 schedTerminal::scheduler::mRetry: Set(),3006 schedTerminal::scheduler::mRevoke: Set(),3007 schedTerminal::scheduler::mSchedule: Set("c1"),3008 schedTerminal::scheduler::published: 0,3009 schedTerminal::scheduler::publishedBy: Set(),3010 schedTerminal::scheduler::ws:3011 Map(3012 "w1" ->3013 {3014 attached: Set(),3015 built: false,3016 expecting: false,3017 running: false,3018 session: false,3019 up: true3020 },3021 "w2" ->3022 {3023 attached: Set(),3024 built: false,3025 expecting: false,3026 running: false,3027 session: false,3028 up: true3029 }3030 )3031}30323033[State 3]3034{3035 schedTerminal::scheduler::cl: Map("c1" -> CFailed, "c2" -> CIdle),3036 schedTerminal::scheduler::crashes: 1,3037 schedTerminal::scheduler::entry: [],3038 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3039 schedTerminal::scheduler::mAssigned: Set(),3040 schedTerminal::scheduler::mBuild: Set(),3041 schedTerminal::scheduler::mDone: Set(),3042 schedTerminal::scheduler::mExpect: Set(),3043 schedTerminal::scheduler::mResult: Set(),3044 schedTerminal::scheduler::mRetry: Set(),3045 schedTerminal::scheduler::mRevoke: Set(),3046 schedTerminal::scheduler::mSchedule: Set(),3047 schedTerminal::scheduler::published: 0,3048 schedTerminal::scheduler::publishedBy: Set(),3049 schedTerminal::scheduler::ws:3050 Map(3051 "w1" ->3052 {3053 attached: Set(),3054 built: false,3055 expecting: false,3056 running: false,3057 session: false,3058 up: true3059 },3060 "w2" ->3061 {3062 attached: Set(),3063 built: false,3064 expecting: false,3065 running: false,3066 session: false,3067 up: true3068 }3069 )3070}30713072[violation] Found an issue (266ms at 7244 traces/second).3073Use --verbosity=3 to show executions.3074Use --seed=0x79091b7842899173 --backend=rust to reproduce.3075error: Invariant violated3076An example execution:30773078[State 0]3079{3080 pushFixed::push::byPath: Map(),3081 pushFixed::push::inflight: Set(),3082 pushFixed::push::left: Map(),3083 pushFixed::push::sent: Map()3084}30853086[State 1]3087{3088 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3089 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3090 pushFixed::push::left: Map(3 -> 2),3091 pushFixed::push::sent: Map(3 -> Set("a", "b"))3092}30933094[State 2]3095{3096 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3097 pushFixed::push::inflight: Set((3, "a")),3098 pushFixed::push::left: Map(3 -> 1),3099 pushFixed::push::sent: Map(3 -> Set("a", "b"))3100}31013102[State 3]3103{3104 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3105 pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "a")),3106 pushFixed::push::left: Map(2 -> 2, 3 -> 1),3107 pushFixed::push::sent: Map(2 -> Set("a", "b"), 3 -> Set("a", "b"))3108}31093110[State 4]3111{3112 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3113 pushFixed::push::inflight:3114 Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a")),3115 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 1),3116 pushFixed::push::sent:3117 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3118}31193120[State 5]3121{3122 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3123 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (3, "a")),3124 pushFixed::push::left: Map(1 -> 2, 2 -> 1, 3 -> 1),3125 pushFixed::push::sent:3126 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3127}31283129[State 6]3130{3131 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3132 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (3, "a")),3133 pushFixed::push::left: Map(1 -> 2, 2 -> 0, 3 -> 1),3134 pushFixed::push::sent:3135 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3136}31373138[State 7]3139{3140 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3141 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3142 pushFixed::push::left: Map(1 -> 2, 2 -> 0, 3 -> 0),3143 pushFixed::push::sent:3144 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3145}31463147[State 8]3148{3149 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3150 pushFixed::push::inflight: Set((1, "a")),3151 pushFixed::push::left: Map(1 -> 1, 2 -> 0, 3 -> 0),3152 pushFixed::push::sent:3153 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3154}31553156[State 9]3157{3158 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3159 pushFixed::push::inflight: Set(),3160 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3161 pushFixed::push::sent:3162 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3163}31643165[ok] No violation found (71ms at 281690 traces/second).3166Trace length statistics: max=10, min=7, average=8.043167You may increase --max-samples and --max-steps.3168Use --verbosity to produce more (or less) output.3169Use --seed=0x77acaaf62353993a --backend=rust to reproduce.