nix-grpc-store-spec
checks.aarch64-linux.spec
· build #766
· raw
1tribuchet: building on eliza2An example execution:34[State 0]5{6 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),7 schedFixed::scheduler::crashes: 0,8 schedFixed::scheduler::entry: [],9 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),10 schedFixed::scheduler::mAssigned: Set(),11 schedFixed::scheduler::mBuild: Set(),12 schedFixed::scheduler::mDone: Set(),13 schedFixed::scheduler::mExpect: Set(),14 schedFixed::scheduler::mResult: Set(),15 schedFixed::scheduler::mRetry: Set(),16 schedFixed::scheduler::mRevoke: Set(),17 schedFixed::scheduler::mSchedule: Set(),18 schedFixed::scheduler::published: 0,19 schedFixed::scheduler::publishedBy: Set(),20 schedFixed::scheduler::ws:21 Map(22 "w1" ->23 {24 attached: Set(),25 built: false,26 expecting: false,27 running: false,28 session: true,29 up: true30 },31 "w2" ->32 {33 attached: Set(),34 built: false,35 expecting: false,36 running: false,37 session: true,38 up: true39 }40 )41}4243[State 1]44{45 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),46 schedFixed::scheduler::crashes: 0,47 schedFixed::scheduler::entry: [],48 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),49 schedFixed::scheduler::mAssigned: Set(),50 schedFixed::scheduler::mBuild: Set(),51 schedFixed::scheduler::mDone: Set(),52 schedFixed::scheduler::mExpect: Set(),53 schedFixed::scheduler::mResult: Set(),54 schedFixed::scheduler::mRetry: Set(),55 schedFixed::scheduler::mRevoke: Set(),56 schedFixed::scheduler::mSchedule: Set("c1"),57 schedFixed::scheduler::published: 0,58 schedFixed::scheduler::publishedBy: Set(),59 schedFixed::scheduler::ws:60 Map(61 "w1" ->62 {63 attached: Set(),64 built: false,65 expecting: false,66 running: false,67 session: true,68 up: true69 },70 "w2" ->71 {72 attached: Set(),73 built: false,74 expecting: false,75 running: false,76 session: true,77 up: true78 }79 )80}8182[State 2]83{84 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),85 schedFixed::scheduler::crashes: 1,86 schedFixed::scheduler::entry: [],87 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),88 schedFixed::scheduler::mAssigned: Set(),89 schedFixed::scheduler::mBuild: Set(),90 schedFixed::scheduler::mDone: Set(),91 schedFixed::scheduler::mExpect: Set(),92 schedFixed::scheduler::mResult: Set(),93 schedFixed::scheduler::mRetry: Set(),94 schedFixed::scheduler::mRevoke: Set(),95 schedFixed::scheduler::mSchedule: Set("c1"),96 schedFixed::scheduler::published: 0,97 schedFixed::scheduler::publishedBy: Set(),98 schedFixed::scheduler::ws:99 Map(100 "w1" ->101 {102 attached: Set(),103 built: false,104 expecting: false,105 running: false,106 session: true,107 up: true108 },109 "w2" ->110 {111 attached: Set(),112 built: false,113 expecting: false,114 running: false,115 session: false,116 up: false117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),124 schedFixed::scheduler::crashes: 1,125 schedFixed::scheduler::entry:126 [{ followers: Set("c1"), leased: true, worker: "w1" }],127 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),128 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),129 schedFixed::scheduler::mBuild: Set(),130 schedFixed::scheduler::mDone: Set(),131 schedFixed::scheduler::mExpect: Set("w1"),132 schedFixed::scheduler::mResult: Set(),133 schedFixed::scheduler::mRetry: Set(),134 schedFixed::scheduler::mRevoke: Set(),135 schedFixed::scheduler::mSchedule: Set(),136 schedFixed::scheduler::published: 0,137 schedFixed::scheduler::publishedBy: Set(),138 schedFixed::scheduler::ws:139 Map(140 "w1" ->141 {142 attached: Set(),143 built: false,144 expecting: false,145 running: false,146 session: true,147 up: true148 },149 "w2" ->150 {151 attached: Set(),152 built: false,153 expecting: false,154 running: false,155 session: false,156 up: false157 }158 )159}160161[State 4]162{163 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),164 schedFixed::scheduler::crashes: 1,165 schedFixed::scheduler::entry:166 [{ followers: Set("c1"), leased: true, worker: "w1" }],167 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),168 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),169 schedFixed::scheduler::mBuild: Set(),170 schedFixed::scheduler::mDone: Set(),171 schedFixed::scheduler::mExpect: Set("w1"),172 schedFixed::scheduler::mResult: Set(),173 schedFixed::scheduler::mRetry: Set(),174 schedFixed::scheduler::mRevoke: Set(),175 schedFixed::scheduler::mSchedule: Set("c2"),176 schedFixed::scheduler::published: 0,177 schedFixed::scheduler::publishedBy: Set(),178 schedFixed::scheduler::ws:179 Map(180 "w1" ->181 {182 attached: Set(),183 built: false,184 expecting: false,185 running: false,186 session: true,187 up: true188 },189 "w2" ->190 {191 attached: Set(),192 built: false,193 expecting: false,194 running: false,195 session: false,196 up: false197 }198 )199}200201[State 5]202{203 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),204 schedFixed::scheduler::crashes: 1,205 schedFixed::scheduler::entry:206 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],207 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),208 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),209 schedFixed::scheduler::mBuild: Set(),210 schedFixed::scheduler::mDone: Set(),211 schedFixed::scheduler::mExpect: Set("w1"),212 schedFixed::scheduler::mResult: Set(),213 schedFixed::scheduler::mRetry: Set(),214 schedFixed::scheduler::mRevoke: Set(),215 schedFixed::scheduler::mSchedule: Set(),216 schedFixed::scheduler::published: 0,217 schedFixed::scheduler::publishedBy: Set(),218 schedFixed::scheduler::ws:219 Map(220 "w1" ->221 {222 attached: Set(),223 built: false,224 expecting: false,225 running: false,226 session: true,227 up: true228 },229 "w2" ->230 {231 attached: Set(),232 built: false,233 expecting: false,234 running: false,235 session: false,236 up: false237 }238 )239}240241[State 6]242{243 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),244 schedFixed::scheduler::crashes: 2,245 schedFixed::scheduler::entry: [],246 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),247 schedFixed::scheduler::mAssigned: Set(),248 schedFixed::scheduler::mBuild: Set(),249 schedFixed::scheduler::mDone: Set(),250 schedFixed::scheduler::mExpect: Set(),251 schedFixed::scheduler::mResult: Set(),252 schedFixed::scheduler::mRetry: Set("c1", "c2"),253 schedFixed::scheduler::mRevoke: Set(),254 schedFixed::scheduler::mSchedule: Set(),255 schedFixed::scheduler::published: 0,256 schedFixed::scheduler::publishedBy: Set(),257 schedFixed::scheduler::ws:258 Map(259 "w1" ->260 {261 attached: Set(),262 built: false,263 expecting: false,264 running: false,265 session: false,266 up: true267 },268 "w2" ->269 {270 attached: Set(),271 built: false,272 expecting: false,273 running: false,274 session: false,275 up: false276 }277 )278}279280[State 7]281{282 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),283 schedFixed::scheduler::crashes: 2,284 schedFixed::scheduler::entry: [],285 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),286 schedFixed::scheduler::mAssigned: Set(),287 schedFixed::scheduler::mBuild: Set(),288 schedFixed::scheduler::mDone: Set(),289 schedFixed::scheduler::mExpect: Set(),290 schedFixed::scheduler::mResult: Set(),291 schedFixed::scheduler::mRetry: Set("c1", "c2"),292 schedFixed::scheduler::mRevoke: Set(),293 schedFixed::scheduler::mSchedule: Set(),294 schedFixed::scheduler::published: 0,295 schedFixed::scheduler::publishedBy: Set(),296 schedFixed::scheduler::ws:297 Map(298 "w1" ->299 {300 attached: Set(),301 built: false,302 expecting: false,303 running: false,304 session: false,305 up: true306 },307 "w2" ->308 {309 attached: Set(),310 built: false,311 expecting: false,312 running: false,313 session: true,314 up: true315 }316 )317}318319[State 8]320{321 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),322 schedFixed::scheduler::crashes: 2,323 schedFixed::scheduler::entry: [],324 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),325 schedFixed::scheduler::mAssigned: Set(),326 schedFixed::scheduler::mBuild: Set(),327 schedFixed::scheduler::mDone: Set(),328 schedFixed::scheduler::mExpect: Set(),329 schedFixed::scheduler::mResult: Set(),330 schedFixed::scheduler::mRetry: Set("c2"),331 schedFixed::scheduler::mRevoke: Set(),332 schedFixed::scheduler::mSchedule: Set("c1"),333 schedFixed::scheduler::published: 0,334 schedFixed::scheduler::publishedBy: Set(),335 schedFixed::scheduler::ws:336 Map(337 "w1" ->338 {339 attached: Set(),340 built: false,341 expecting: false,342 running: false,343 session: false,344 up: true345 },346 "w2" ->347 {348 attached: Set(),349 built: false,350 expecting: false,351 running: false,352 session: true,353 up: true354 }355 )356}357358[State 9]359{360 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),361 schedFixed::scheduler::crashes: 2,362 schedFixed::scheduler::entry: [],363 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),364 schedFixed::scheduler::mAssigned: Set(),365 schedFixed::scheduler::mBuild: Set(),366 schedFixed::scheduler::mDone: Set(),367 schedFixed::scheduler::mExpect: Set(),368 schedFixed::scheduler::mResult: Set(),369 schedFixed::scheduler::mRetry: Set(),370 schedFixed::scheduler::mRevoke: Set(),371 schedFixed::scheduler::mSchedule: Set("c1", "c2"),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: false,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" -> CQueued),400 schedFixed::scheduler::crashes: 2,401 schedFixed::scheduler::entry:402 [{ followers: Set("c1"), leased: true, worker: "w2" }],403 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),404 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),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(),410 schedFixed::scheduler::mRevoke: Set(),411 schedFixed::scheduler::mSchedule: Set("c2"),412 schedFixed::scheduler::published: 0,413 schedFixed::scheduler::publishedBy: Set(),414 schedFixed::scheduler::ws:415 Map(416 "w1" ->417 {418 attached: Set(),419 built: false,420 expecting: false,421 running: false,422 session: false,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" -> CQueued),440 schedFixed::scheduler::crashes: 2,441 schedFixed::scheduler::entry:442 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],443 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),444 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),445 schedFixed::scheduler::mBuild: Set(),446 schedFixed::scheduler::mDone: Set(),447 schedFixed::scheduler::mExpect: Set("w2"),448 schedFixed::scheduler::mResult: Set(),449 schedFixed::scheduler::mRetry: Set(),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: false,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" -> CSent("w2")),480 schedFixed::scheduler::crashes: 2,481 schedFixed::scheduler::entry:482 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],483 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),484 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),485 schedFixed::scheduler::mBuild: Set(("c2", "w2")),486 schedFixed::scheduler::mDone: Set(),487 schedFixed::scheduler::mExpect: Set("w2"),488 schedFixed::scheduler::mResult: Set(),489 schedFixed::scheduler::mRetry: Set(),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: false,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("w2")),520 schedFixed::scheduler::crashes: 2,521 schedFixed::scheduler::entry:522 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],523 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),524 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),525 schedFixed::scheduler::mBuild: Set(("c2", "w2")),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(),532 schedFixed::scheduler::published: 0,533 schedFixed::scheduler::publishedBy: Set(),534 schedFixed::scheduler::ws:535 Map(536 "w1" ->537 {538 attached: Set(),539 built: false,540 expecting: false,541 running: false,542 session: true,543 up: true544 },545 "w2" ->546 {547 attached: Set(),548 built: false,549 expecting: false,550 running: false,551 session: true,552 up: true553 }554 )555}556557[State 14]558{559 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),560 schedFixed::scheduler::crashes: 2,561 schedFixed::scheduler::entry:562 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],563 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),564 schedFixed::scheduler::mAssigned: Set(),565 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("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(),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" -> CSent("w2"), "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(),605 schedFixed::scheduler::mBuild: Set(("c1", "w2")),606 schedFixed::scheduler::mDone: Set(),607 schedFixed::scheduler::mExpect: Set("w2"),608 schedFixed::scheduler::mResult: Set(),609 schedFixed::scheduler::mRetry: Set("c2"),610 schedFixed::scheduler::mRevoke: Set(),611 schedFixed::scheduler::mSchedule: Set(),612 schedFixed::scheduler::published: 0,613 schedFixed::scheduler::publishedBy: Set(),614 schedFixed::scheduler::ws:615 Map(616 "w1" ->617 {618 attached: Set(),619 built: false,620 expecting: false,621 running: false,622 session: true,623 up: true624 },625 "w2" ->626 {627 attached: Set(),628 built: false,629 expecting: false,630 running: false,631 session: true,632 up: true633 }634 )635}636637[State 16]638{639 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),640 schedFixed::scheduler::crashes: 2,641 schedFixed::scheduler::entry:642 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],643 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),644 schedFixed::scheduler::mAssigned: Set(),645 schedFixed::scheduler::mBuild: Set(("c1", "w2")),646 schedFixed::scheduler::mDone: Set(),647 schedFixed::scheduler::mExpect: Set("w2"),648 schedFixed::scheduler::mResult: Set(),649 schedFixed::scheduler::mRetry: Set(),650 schedFixed::scheduler::mRevoke: Set(),651 schedFixed::scheduler::mSchedule: Set("c2"),652 schedFixed::scheduler::published: 0,653 schedFixed::scheduler::publishedBy: Set(),654 schedFixed::scheduler::ws:655 Map(656 "w1" ->657 {658 attached: Set(),659 built: false,660 expecting: false,661 running: false,662 session: true,663 up: true664 },665 "w2" ->666 {667 attached: Set(),668 built: false,669 expecting: false,670 running: false,671 session: true,672 up: true673 }674 )675}676677[State 17]678{679 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),680 schedFixed::scheduler::crashes: 2,681 schedFixed::scheduler::entry:682 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],683 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),684 schedFixed::scheduler::mAssigned: Set(),685 schedFixed::scheduler::mBuild: Set(),686 schedFixed::scheduler::mDone: Set(),687 schedFixed::scheduler::mExpect: Set("w2"),688 schedFixed::scheduler::mResult: Set(),689 schedFixed::scheduler::mRetry: Set("c1"),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" -> CQueued, "c2" -> CQueued),720 schedFixed::scheduler::crashes: 2,721 schedFixed::scheduler::entry:722 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],723 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),724 schedFixed::scheduler::mAssigned: Set(),725 schedFixed::scheduler::mBuild: Set(),726 schedFixed::scheduler::mDone: Set(),727 schedFixed::scheduler::mExpect: Set("w2"),728 schedFixed::scheduler::mResult: Set(),729 schedFixed::scheduler::mRetry: Set(),730 schedFixed::scheduler::mRevoke: Set(),731 schedFixed::scheduler::mSchedule: Set("c1", "c2"),732 schedFixed::scheduler::published: 0,733 schedFixed::scheduler::publishedBy: Set(),734 schedFixed::scheduler::ws:735 Map(736 "w1" ->737 {738 attached: Set(),739 built: false,740 expecting: false,741 running: false,742 session: true,743 up: true744 },745 "w2" ->746 {747 attached: Set(),748 built: false,749 expecting: false,750 running: false,751 session: true,752 up: true753 }754 )755}756757[State 19]758{759 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),760 schedFixed::scheduler::crashes: 2,761 schedFixed::scheduler::entry:762 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],763 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),764 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),765 schedFixed::scheduler::mBuild: Set(),766 schedFixed::scheduler::mDone: Set(),767 schedFixed::scheduler::mExpect: Set("w2"),768 schedFixed::scheduler::mResult: Set(),769 schedFixed::scheduler::mRetry: Set(),770 schedFixed::scheduler::mRevoke: Set(),771 schedFixed::scheduler::mSchedule: Set("c2"),772 schedFixed::scheduler::published: 0,773 schedFixed::scheduler::publishedBy: Set(),774 schedFixed::scheduler::ws:775 Map(776 "w1" ->777 {778 attached: Set(),779 built: false,780 expecting: false,781 running: false,782 session: true,783 up: true784 },785 "w2" ->786 {787 attached: Set(),788 built: false,789 expecting: false,790 running: false,791 session: true,792 up: true793 }794 )795}796797[State 20]798{799 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),800 schedFixed::scheduler::crashes: 2,801 schedFixed::scheduler::entry:802 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],803 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),804 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),805 schedFixed::scheduler::mBuild: Set(),806 schedFixed::scheduler::mDone: Set(),807 schedFixed::scheduler::mExpect: Set("w2"),808 schedFixed::scheduler::mResult: Set(),809 schedFixed::scheduler::mRetry: Set(),810 schedFixed::scheduler::mRevoke: Set(),811 schedFixed::scheduler::mSchedule: Set(),812 schedFixed::scheduler::published: 0,813 schedFixed::scheduler::publishedBy: Set(),814 schedFixed::scheduler::ws:815 Map(816 "w1" ->817 {818 attached: Set(),819 built: false,820 expecting: false,821 running: false,822 session: true,823 up: true824 },825 "w2" ->826 {827 attached: Set(),828 built: false,829 expecting: false,830 running: false,831 session: true,832 up: true833 }834 )835}836837[State 21]838{839 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),840 schedFixed::scheduler::crashes: 2,841 schedFixed::scheduler::entry:842 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],843 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),844 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),845 schedFixed::scheduler::mBuild: Set(("c1", "w2")),846 schedFixed::scheduler::mDone: Set(),847 schedFixed::scheduler::mExpect: Set("w2"),848 schedFixed::scheduler::mResult: Set(),849 schedFixed::scheduler::mRetry: Set(),850 schedFixed::scheduler::mRevoke: Set(),851 schedFixed::scheduler::mSchedule: Set(),852 schedFixed::scheduler::published: 0,853 schedFixed::scheduler::publishedBy: Set(),854 schedFixed::scheduler::ws:855 Map(856 "w1" ->857 {858 attached: Set(),859 built: false,860 expecting: false,861 running: false,862 session: true,863 up: true864 },865 "w2" ->866 {867 attached: Set(),868 built: false,869 expecting: false,870 running: false,871 session: true,872 up: true873 }874 )875}876877[State 22]878{879 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),880 schedFixed::scheduler::crashes: 2,881 schedFixed::scheduler::entry:882 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],883 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),884 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),885 schedFixed::scheduler::mBuild: Set(),886 schedFixed::scheduler::mDone: Set(),887 schedFixed::scheduler::mExpect: Set("w2"),888 schedFixed::scheduler::mResult: Set(),889 schedFixed::scheduler::mRetry: Set("c1"),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(),926 schedFixed::scheduler::mDone: Set(),927 schedFixed::scheduler::mExpect: Set(),928 schedFixed::scheduler::mResult: Set(),929 schedFixed::scheduler::mRetry: Set("c1"),930 schedFixed::scheduler::mRevoke: Set(),931 schedFixed::scheduler::mSchedule: Set(),932 schedFixed::scheduler::published: 0,933 schedFixed::scheduler::publishedBy: Set(),934 schedFixed::scheduler::ws:935 Map(936 "w1" ->937 {938 attached: Set(),939 built: false,940 expecting: false,941 running: false,942 session: true,943 up: true944 },945 "w2" ->946 {947 attached: Set(),948 built: false,949 expecting: true,950 running: true,951 session: true,952 up: true953 }954 )955}956957[State 24]958{959 schedFixed::scheduler::cl: Map("c1" -> CQueued, "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(),968 schedFixed::scheduler::mResult: Set(),969 schedFixed::scheduler::mRetry: Set(),970 schedFixed::scheduler::mRevoke: Set(),971 schedFixed::scheduler::mSchedule: Set("c1"),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: true,990 running: true,991 session: true,992 up: true993 }994 )995}996997[State 25]998{999 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1000 schedFixed::scheduler::crashes: 2,1001 schedFixed::scheduler::entry:1002 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1003 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1004 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1005 schedFixed::scheduler::mBuild: Set(),1006 schedFixed::scheduler::mDone: Set("w2"),1007 schedFixed::scheduler::mExpect: Set(),1008 schedFixed::scheduler::mResult: Set(),1009 schedFixed::scheduler::mRetry: Set(),1010 schedFixed::scheduler::mRevoke: Set(),1011 schedFixed::scheduler::mSchedule: Set("c1"),1012 schedFixed::scheduler::published: 1,1013 schedFixed::scheduler::publishedBy: Set("w2"),1014 schedFixed::scheduler::ws:1015 Map(1016 "w1" ->1017 {1018 attached: Set(),1019 built: false,1020 expecting: false,1021 running: false,1022 session: true,1023 up: true1024 },1025 "w2" ->1026 {1027 attached: Set(),1028 built: true,1029 expecting: false,1030 running: false,1031 session: true,1032 up: true1033 }1034 )1035}10361037[State 26]1038{1039 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),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(("c2", "w2")),1045 schedFixed::scheduler::mBuild: Set(),1046 schedFixed::scheduler::mDone: Set("w2"),1047 schedFixed::scheduler::mExpect: Set(),1048 schedFixed::scheduler::mResult: Set("c1"),1049 schedFixed::scheduler::mRetry: Set(),1050 schedFixed::scheduler::mRevoke: Set(),1051 schedFixed::scheduler::mSchedule: Set(),1052 schedFixed::scheduler::published: 1,1053 schedFixed::scheduler::publishedBy: Set("w2"),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: true,1069 expecting: false,1070 running: false,1071 session: true,1072 up: true1073 }1074 )1075}10761077[State 27]1078{1079 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),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(("c2", "w2")),1086 schedFixed::scheduler::mDone: Set("w2"),1087 schedFixed::scheduler::mExpect: Set(),1088 schedFixed::scheduler::mResult: Set("c1"),1089 schedFixed::scheduler::mRetry: Set(),1090 schedFixed::scheduler::mRevoke: Set(),1091 schedFixed::scheduler::mSchedule: Set(),1092 schedFixed::scheduler::published: 1,1093 schedFixed::scheduler::publishedBy: Set("w2"),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: true,1109 expecting: false,1110 running: false,1111 session: true,1112 up: true1113 }1114 )1115}11161117[State 28]1118{1119 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),1120 schedFixed::scheduler::crashes: 2,1121 schedFixed::scheduler::entry: [],1122 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1123 schedFixed::scheduler::mAssigned: Set(),1124 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1125 schedFixed::scheduler::mDone: Set(),1126 schedFixed::scheduler::mExpect: Set(),1127 schedFixed::scheduler::mResult: Set("c1"),1128 schedFixed::scheduler::mRetry: Set(),1129 schedFixed::scheduler::mRevoke: Set(),1130 schedFixed::scheduler::mSchedule: Set(),1131 schedFixed::scheduler::published: 1,1132 schedFixed::scheduler::publishedBy: Set("w2"),1133 schedFixed::scheduler::ws:1134 Map(1135 "w1" ->1136 {1137 attached: Set(),1138 built: false,1139 expecting: false,1140 running: false,1141 session: true,1142 up: true1143 },1144 "w2" ->1145 {1146 attached: Set(),1147 built: true,1148 expecting: false,1149 running: false,1150 session: true,1151 up: true1152 }1153 )1154}11551156[State 29]1157{1158 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),1159 schedFixed::scheduler::crashes: 2,1160 schedFixed::scheduler::entry: [],1161 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1162 schedFixed::scheduler::mAssigned: Set(),1163 schedFixed::scheduler::mBuild: Set(),1164 schedFixed::scheduler::mDone: Set(),1165 schedFixed::scheduler::mExpect: Set(),1166 schedFixed::scheduler::mResult: Set("c1", "c2"),1167 schedFixed::scheduler::mRetry: Set(),1168 schedFixed::scheduler::mRevoke: Set(),1169 schedFixed::scheduler::mSchedule: Set(),1170 schedFixed::scheduler::published: 1,1171 schedFixed::scheduler::publishedBy: Set("w2"),1172 schedFixed::scheduler::ws:1173 Map(1174 "w1" ->1175 {1176 attached: Set(),1177 built: false,1178 expecting: false,1179 running: false,1180 session: true,1181 up: true1182 },1183 "w2" ->1184 {1185 attached: Set(),1186 built: true,1187 expecting: false,1188 running: false,1189 session: true,1190 up: true1191 }1192 )1193}11941195[State 30]1196{1197 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w2")),1198 schedFixed::scheduler::crashes: 2,1199 schedFixed::scheduler::entry: [],1200 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1201 schedFixed::scheduler::mAssigned: Set(),1202 schedFixed::scheduler::mBuild: Set(),1203 schedFixed::scheduler::mDone: Set(),1204 schedFixed::scheduler::mExpect: Set(),1205 schedFixed::scheduler::mResult: Set("c2"),1206 schedFixed::scheduler::mRetry: Set(),1207 schedFixed::scheduler::mRevoke: Set(),1208 schedFixed::scheduler::mSchedule: Set(),1209 schedFixed::scheduler::published: 1,1210 schedFixed::scheduler::publishedBy: Set("w2"),1211 schedFixed::scheduler::ws:1212 Map(1213 "w1" ->1214 {1215 attached: Set(),1216 built: false,1217 expecting: false,1218 running: false,1219 session: true,1220 up: true1221 },1222 "w2" ->1223 {1224 attached: Set(),1225 built: true,1226 expecting: false,1227 running: false,1228 session: true,1229 up: true1230 }1231 )1232}12331234[ok] No violation found (1046ms at 28681 traces/second).1235Trace length statistics: max=31, min=15, average=19.181236You may increase --max-samples and --max-steps.1237Use --verbosity to produce more (or less) output.1238Use --seed=0xba3a9e6e908f447b --backend=rust to reproduce.1239An example execution:12401241[State 0]1242{1243 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1244 schedNoRevoke::scheduler::crashes: 0,1245 schedNoRevoke::scheduler::entry: [],1246 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1247 schedNoRevoke::scheduler::mAssigned: Set(),1248 schedNoRevoke::scheduler::mBuild: Set(),1249 schedNoRevoke::scheduler::mDone: Set(),1250 schedNoRevoke::scheduler::mExpect: Set(),1251 schedNoRevoke::scheduler::mResult: Set(),1252 schedNoRevoke::scheduler::mRetry: Set(),1253 schedNoRevoke::scheduler::mRevoke: Set(),1254 schedNoRevoke::scheduler::mSchedule: Set(),1255 schedNoRevoke::scheduler::published: 0,1256 schedNoRevoke::scheduler::publishedBy: Set(),1257 schedNoRevoke::scheduler::ws:1258 Map(1259 "w1" ->1260 {1261 attached: Set(),1262 built: false,1263 expecting: false,1264 running: false,1265 session: true,1266 up: true1267 },1268 "w2" ->1269 {1270 attached: Set(),1271 built: false,1272 expecting: false,1273 running: false,1274 session: true,1275 up: true1276 }1277 )1278}12791280[State 1]1281{1282 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1283 schedNoRevoke::scheduler::crashes: 0,1284 schedNoRevoke::scheduler::entry: [],1285 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1286 schedNoRevoke::scheduler::mAssigned: Set(),1287 schedNoRevoke::scheduler::mBuild: Set(),1288 schedNoRevoke::scheduler::mDone: Set(),1289 schedNoRevoke::scheduler::mExpect: Set(),1290 schedNoRevoke::scheduler::mResult: Set(),1291 schedNoRevoke::scheduler::mRetry: Set(),1292 schedNoRevoke::scheduler::mRevoke: Set(),1293 schedNoRevoke::scheduler::mSchedule: Set("c2"),1294 schedNoRevoke::scheduler::published: 0,1295 schedNoRevoke::scheduler::publishedBy: Set(),1296 schedNoRevoke::scheduler::ws:1297 Map(1298 "w1" ->1299 {1300 attached: Set(),1301 built: false,1302 expecting: false,1303 running: false,1304 session: true,1305 up: true1306 },1307 "w2" ->1308 {1309 attached: Set(),1310 built: false,1311 expecting: false,1312 running: false,1313 session: true,1314 up: true1315 }1316 )1317}13181319[State 2]1320{1321 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1322 schedNoRevoke::scheduler::crashes: 0,1323 schedNoRevoke::scheduler::entry:1324 [{ followers: Set("c2"), leased: true, worker: "w1" }],1325 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1326 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1327 schedNoRevoke::scheduler::mBuild: Set(),1328 schedNoRevoke::scheduler::mDone: Set(),1329 schedNoRevoke::scheduler::mExpect: Set("w1"),1330 schedNoRevoke::scheduler::mResult: Set(),1331 schedNoRevoke::scheduler::mRetry: Set(),1332 schedNoRevoke::scheduler::mRevoke: Set(),1333 schedNoRevoke::scheduler::mSchedule: Set(),1334 schedNoRevoke::scheduler::published: 0,1335 schedNoRevoke::scheduler::publishedBy: Set(),1336 schedNoRevoke::scheduler::ws:1337 Map(1338 "w1" ->1339 {1340 attached: Set(),1341 built: false,1342 expecting: false,1343 running: false,1344 session: true,1345 up: true1346 },1347 "w2" ->1348 {1349 attached: Set(),1350 built: false,1351 expecting: false,1352 running: false,1353 session: true,1354 up: true1355 }1356 )1357}13581359[State 3]1360{1361 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1362 schedNoRevoke::scheduler::crashes: 1,1363 schedNoRevoke::scheduler::entry:1364 [{ followers: Set("c2"), leased: true, worker: "w1" }],1365 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1366 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1367 schedNoRevoke::scheduler::mBuild: Set(),1368 schedNoRevoke::scheduler::mDone: Set(),1369 schedNoRevoke::scheduler::mExpect: Set("w1"),1370 schedNoRevoke::scheduler::mResult: Set(),1371 schedNoRevoke::scheduler::mRetry: Set(),1372 schedNoRevoke::scheduler::mRevoke: Set(),1373 schedNoRevoke::scheduler::mSchedule: Set(),1374 schedNoRevoke::scheduler::published: 0,1375 schedNoRevoke::scheduler::publishedBy: Set(),1376 schedNoRevoke::scheduler::ws:1377 Map(1378 "w1" ->1379 {1380 attached: Set(),1381 built: false,1382 expecting: false,1383 running: false,1384 session: true,1385 up: true1386 },1387 "w2" ->1388 {1389 attached: Set(),1390 built: false,1391 expecting: false,1392 running: false,1393 session: false,1394 up: false1395 }1396 )1397}13981399[State 4]1400{1401 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1402 schedNoRevoke::scheduler::crashes: 1,1403 schedNoRevoke::scheduler::entry:1404 [{ followers: Set("c2"), leased: true, worker: "w1" }],1405 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1406 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1407 schedNoRevoke::scheduler::mBuild: Set(),1408 schedNoRevoke::scheduler::mDone: Set(),1409 schedNoRevoke::scheduler::mExpect: Set(),1410 schedNoRevoke::scheduler::mResult: Set(),1411 schedNoRevoke::scheduler::mRetry: Set(),1412 schedNoRevoke::scheduler::mRevoke: Set(),1413 schedNoRevoke::scheduler::mSchedule: Set(),1414 schedNoRevoke::scheduler::published: 0,1415 schedNoRevoke::scheduler::publishedBy: Set(),1416 schedNoRevoke::scheduler::ws:1417 Map(1418 "w1" ->1419 {1420 attached: Set(),1421 built: false,1422 expecting: true,1423 running: true,1424 session: true,1425 up: true1426 },1427 "w2" ->1428 {1429 attached: Set(),1430 built: false,1431 expecting: false,1432 running: false,1433 session: false,1434 up: false1435 }1436 )1437}14381439[State 5]1440{1441 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1442 schedNoRevoke::scheduler::crashes: 2,1443 schedNoRevoke::scheduler::entry: [],1444 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1445 schedNoRevoke::scheduler::mAssigned: Set(),1446 schedNoRevoke::scheduler::mBuild: Set(),1447 schedNoRevoke::scheduler::mDone: Set(),1448 schedNoRevoke::scheduler::mExpect: Set(),1449 schedNoRevoke::scheduler::mResult: Set(),1450 schedNoRevoke::scheduler::mRetry: Set("c2"),1451 schedNoRevoke::scheduler::mRevoke: Set(),1452 schedNoRevoke::scheduler::mSchedule: Set(),1453 schedNoRevoke::scheduler::published: 0,1454 schedNoRevoke::scheduler::publishedBy: Set(),1455 schedNoRevoke::scheduler::ws:1456 Map(1457 "w1" ->1458 {1459 attached: Set(),1460 built: false,1461 expecting: true,1462 running: true,1463 session: false,1464 up: true1465 },1466 "w2" ->1467 {1468 attached: Set(),1469 built: false,1470 expecting: false,1471 running: false,1472 session: false,1473 up: false1474 }1475 )1476}14771478[State 6]1479{1480 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1481 schedNoRevoke::scheduler::crashes: 2,1482 schedNoRevoke::scheduler::entry: [],1483 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1484 schedNoRevoke::scheduler::mAssigned: Set(),1485 schedNoRevoke::scheduler::mBuild: Set(),1486 schedNoRevoke::scheduler::mDone: Set(),1487 schedNoRevoke::scheduler::mExpect: Set(),1488 schedNoRevoke::scheduler::mResult: Set(),1489 schedNoRevoke::scheduler::mRetry: Set("c2"),1490 schedNoRevoke::scheduler::mRevoke: Set(),1491 schedNoRevoke::scheduler::mSchedule: Set(),1492 schedNoRevoke::scheduler::published: 0,1493 schedNoRevoke::scheduler::publishedBy: Set(),1494 schedNoRevoke::scheduler::ws:1495 Map(1496 "w1" ->1497 {1498 attached: Set(),1499 built: false,1500 expecting: true,1501 running: true,1502 session: false,1503 up: true1504 },1505 "w2" ->1506 {1507 attached: Set(),1508 built: false,1509 expecting: false,1510 running: false,1511 session: true,1512 up: true1513 }1514 )1515}15161517[State 7]1518{1519 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1520 schedNoRevoke::scheduler::crashes: 2,1521 schedNoRevoke::scheduler::entry: [],1522 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1523 schedNoRevoke::scheduler::mAssigned: Set(),1524 schedNoRevoke::scheduler::mBuild: Set(),1525 schedNoRevoke::scheduler::mDone: Set(),1526 schedNoRevoke::scheduler::mExpect: Set(),1527 schedNoRevoke::scheduler::mResult: Set(),1528 schedNoRevoke::scheduler::mRetry: Set("c2"),1529 schedNoRevoke::scheduler::mRevoke: Set(),1530 schedNoRevoke::scheduler::mSchedule: Set("c1"),1531 schedNoRevoke::scheduler::published: 0,1532 schedNoRevoke::scheduler::publishedBy: Set(),1533 schedNoRevoke::scheduler::ws:1534 Map(1535 "w1" ->1536 {1537 attached: Set(),1538 built: false,1539 expecting: true,1540 running: true,1541 session: false,1542 up: true1543 },1544 "w2" ->1545 {1546 attached: Set(),1547 built: false,1548 expecting: false,1549 running: false,1550 session: true,1551 up: true1552 }1553 )1554}15551556[State 8]1557{1558 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1559 schedNoRevoke::scheduler::crashes: 2,1560 schedNoRevoke::scheduler::entry:1561 [{ followers: Set("c1"), leased: true, worker: "w2" }],1562 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1563 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1564 schedNoRevoke::scheduler::mBuild: Set(),1565 schedNoRevoke::scheduler::mDone: Set(),1566 schedNoRevoke::scheduler::mExpect: Set("w2"),1567 schedNoRevoke::scheduler::mResult: Set(),1568 schedNoRevoke::scheduler::mRetry: Set("c2"),1569 schedNoRevoke::scheduler::mRevoke: Set(),1570 schedNoRevoke::scheduler::mSchedule: Set(),1571 schedNoRevoke::scheduler::published: 0,1572 schedNoRevoke::scheduler::publishedBy: Set(),1573 schedNoRevoke::scheduler::ws:1574 Map(1575 "w1" ->1576 {1577 attached: Set(),1578 built: false,1579 expecting: true,1580 running: true,1581 session: false,1582 up: true1583 },1584 "w2" ->1585 {1586 attached: Set(),1587 built: false,1588 expecting: false,1589 running: false,1590 session: true,1591 up: true1592 }1593 )1594}15951596[State 9]1597{1598 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1599 schedNoRevoke::scheduler::crashes: 2,1600 schedNoRevoke::scheduler::entry:1601 [{ followers: Set("c1"), leased: true, worker: "w2" }],1602 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1603 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1604 schedNoRevoke::scheduler::mBuild: Set(),1605 schedNoRevoke::scheduler::mDone: Set(),1606 schedNoRevoke::scheduler::mExpect: Set(),1607 schedNoRevoke::scheduler::mResult: Set(),1608 schedNoRevoke::scheduler::mRetry: Set("c2"),1609 schedNoRevoke::scheduler::mRevoke: Set(),1610 schedNoRevoke::scheduler::mSchedule: Set(),1611 schedNoRevoke::scheduler::published: 0,1612 schedNoRevoke::scheduler::publishedBy: Set(),1613 schedNoRevoke::scheduler::ws:1614 Map(1615 "w1" ->1616 {1617 attached: Set(),1618 built: false,1619 expecting: true,1620 running: true,1621 session: false,1622 up: true1623 },1624 "w2" ->1625 {1626 attached: Set(),1627 built: false,1628 expecting: true,1629 running: true,1630 session: true,1631 up: true1632 }1633 )1634}16351636[State 10]1637{1638 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1639 schedNoRevoke::scheduler::crashes: 2,1640 schedNoRevoke::scheduler::entry:1641 [{ followers: Set("c1"), leased: true, worker: "w2" }],1642 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1643 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1644 schedNoRevoke::scheduler::mBuild: Set(),1645 schedNoRevoke::scheduler::mDone: Set(),1646 schedNoRevoke::scheduler::mExpect: Set(),1647 schedNoRevoke::scheduler::mResult: Set(),1648 schedNoRevoke::scheduler::mRetry: Set("c2"),1649 schedNoRevoke::scheduler::mRevoke: Set(),1650 schedNoRevoke::scheduler::mSchedule: Set(),1651 schedNoRevoke::scheduler::published: 0,1652 schedNoRevoke::scheduler::publishedBy: Set(),1653 schedNoRevoke::scheduler::ws:1654 Map(1655 "w1" ->1656 {1657 attached: Set(),1658 built: false,1659 expecting: true,1660 running: true,1661 session: true,1662 up: true1663 },1664 "w2" ->1665 {1666 attached: Set(),1667 built: false,1668 expecting: true,1669 running: true,1670 session: true,1671 up: true1672 }1673 )1674}16751676[violation] Found an issue (2157ms at 12842 traces/second).1677Use --verbosity=3 to show executions.1678Use --seed=0x44fcab3a383ef124 --backend=rust to reproduce.1679error: Invariant violated1680An example execution:16811682[State 0]1683{1684 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1685 schedNoFence::scheduler::crashes: 0,1686 schedNoFence::scheduler::entry: [],1687 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1688 schedNoFence::scheduler::mAssigned: Set(),1689 schedNoFence::scheduler::mBuild: Set(),1690 schedNoFence::scheduler::mDone: Set(),1691 schedNoFence::scheduler::mExpect: Set(),1692 schedNoFence::scheduler::mResult: Set(),1693 schedNoFence::scheduler::mRetry: Set(),1694 schedNoFence::scheduler::mRevoke: Set(),1695 schedNoFence::scheduler::mSchedule: Set(),1696 schedNoFence::scheduler::published: 0,1697 schedNoFence::scheduler::publishedBy: Set(),1698 schedNoFence::scheduler::ws:1699 Map(1700 "w1" ->1701 {1702 attached: Set(),1703 built: false,1704 expecting: false,1705 running: false,1706 session: true,1707 up: true1708 },1709 "w2" ->1710 {1711 attached: Set(),1712 built: false,1713 expecting: false,1714 running: false,1715 session: true,1716 up: true1717 }1718 )1719}17201721[State 1]1722{1723 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1724 schedNoFence::scheduler::crashes: 0,1725 schedNoFence::scheduler::entry: [],1726 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1727 schedNoFence::scheduler::mAssigned: Set(),1728 schedNoFence::scheduler::mBuild: Set(),1729 schedNoFence::scheduler::mDone: Set(),1730 schedNoFence::scheduler::mExpect: Set(),1731 schedNoFence::scheduler::mResult: Set(),1732 schedNoFence::scheduler::mRetry: Set(),1733 schedNoFence::scheduler::mRevoke: Set(),1734 schedNoFence::scheduler::mSchedule: Set("c2"),1735 schedNoFence::scheduler::published: 0,1736 schedNoFence::scheduler::publishedBy: Set(),1737 schedNoFence::scheduler::ws:1738 Map(1739 "w1" ->1740 {1741 attached: Set(),1742 built: false,1743 expecting: false,1744 running: false,1745 session: true,1746 up: true1747 },1748 "w2" ->1749 {1750 attached: Set(),1751 built: false,1752 expecting: false,1753 running: false,1754 session: true,1755 up: true1756 }1757 )1758}17591760[State 2]1761{1762 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1763 schedNoFence::scheduler::crashes: 0,1764 schedNoFence::scheduler::entry:1765 [{ followers: Set("c2"), leased: true, worker: "w2" }],1766 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1767 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1768 schedNoFence::scheduler::mBuild: Set(),1769 schedNoFence::scheduler::mDone: Set(),1770 schedNoFence::scheduler::mExpect: Set("w2"),1771 schedNoFence::scheduler::mResult: Set(),1772 schedNoFence::scheduler::mRetry: Set(),1773 schedNoFence::scheduler::mRevoke: Set(),1774 schedNoFence::scheduler::mSchedule: Set(),1775 schedNoFence::scheduler::published: 0,1776 schedNoFence::scheduler::publishedBy: Set(),1777 schedNoFence::scheduler::ws:1778 Map(1779 "w1" ->1780 {1781 attached: Set(),1782 built: false,1783 expecting: false,1784 running: false,1785 session: true,1786 up: true1787 },1788 "w2" ->1789 {1790 attached: Set(),1791 built: false,1792 expecting: false,1793 running: false,1794 session: true,1795 up: true1796 }1797 )1798}17991800[State 3]1801{1802 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1803 schedNoFence::scheduler::crashes: 1,1804 schedNoFence::scheduler::entry:1805 [{ followers: Set("c2"), leased: true, worker: "w2" }],1806 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1807 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1808 schedNoFence::scheduler::mBuild: Set(),1809 schedNoFence::scheduler::mDone: Set(),1810 schedNoFence::scheduler::mExpect: Set("w2"),1811 schedNoFence::scheduler::mResult: Set(),1812 schedNoFence::scheduler::mRetry: Set(),1813 schedNoFence::scheduler::mRevoke: Set(),1814 schedNoFence::scheduler::mSchedule: Set(),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 4]1841{1842 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1843 schedNoFence::scheduler::crashes: 1,1844 schedNoFence::scheduler::entry:1845 [{ followers: Set("c2"), leased: true, worker: "w2" }],1846 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1847 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1848 schedNoFence::scheduler::mBuild: Set(),1849 schedNoFence::scheduler::mDone: Set(),1850 schedNoFence::scheduler::mExpect: Set(),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: true,1873 running: true,1874 session: true,1875 up: true1876 }1877 )1878}18791880[State 5]1881{1882 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1883 schedNoFence::scheduler::crashes: 2,1884 schedNoFence::scheduler::entry: [],1885 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1886 schedNoFence::scheduler::mAssigned: Set(),1887 schedNoFence::scheduler::mBuild: Set(),1888 schedNoFence::scheduler::mDone: Set(),1889 schedNoFence::scheduler::mExpect: Set(),1890 schedNoFence::scheduler::mResult: Set(),1891 schedNoFence::scheduler::mRetry: Set("c2"),1892 schedNoFence::scheduler::mRevoke: Set(),1893 schedNoFence::scheduler::mSchedule: Set(),1894 schedNoFence::scheduler::published: 0,1895 schedNoFence::scheduler::publishedBy: Set(),1896 schedNoFence::scheduler::ws:1897 Map(1898 "w1" ->1899 {1900 attached: Set(),1901 built: false,1902 expecting: false,1903 running: false,1904 session: false,1905 up: false1906 },1907 "w2" ->1908 {1909 attached: Set(),1910 built: false,1911 expecting: true,1912 running: true,1913 session: false,1914 up: true1915 }1916 )1917}19181919[State 6]1920{1921 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1922 schedNoFence::scheduler::crashes: 2,1923 schedNoFence::scheduler::entry: [],1924 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1925 schedNoFence::scheduler::mAssigned: Set(),1926 schedNoFence::scheduler::mBuild: Set(),1927 schedNoFence::scheduler::mDone: Set(),1928 schedNoFence::scheduler::mExpect: Set(),1929 schedNoFence::scheduler::mResult: Set(),1930 schedNoFence::scheduler::mRetry: Set(),1931 schedNoFence::scheduler::mRevoke: Set(),1932 schedNoFence::scheduler::mSchedule: Set("c2"),1933 schedNoFence::scheduler::published: 0,1934 schedNoFence::scheduler::publishedBy: Set(),1935 schedNoFence::scheduler::ws:1936 Map(1937 "w1" ->1938 {1939 attached: Set(),1940 built: false,1941 expecting: false,1942 running: false,1943 session: false,1944 up: false1945 },1946 "w2" ->1947 {1948 attached: Set(),1949 built: false,1950 expecting: true,1951 running: true,1952 session: false,1953 up: true1954 }1955 )1956}19571958[State 7]1959{1960 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1961 schedNoFence::scheduler::crashes: 2,1962 schedNoFence::scheduler::entry: [],1963 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1964 schedNoFence::scheduler::mAssigned: Set(),1965 schedNoFence::scheduler::mBuild: Set(),1966 schedNoFence::scheduler::mDone: Set(),1967 schedNoFence::scheduler::mExpect: Set(),1968 schedNoFence::scheduler::mResult: Set(),1969 schedNoFence::scheduler::mRetry: Set(),1970 schedNoFence::scheduler::mRevoke: Set(),1971 schedNoFence::scheduler::mSchedule: Set("c2"),1972 schedNoFence::scheduler::published: 0,1973 schedNoFence::scheduler::publishedBy: Set(),1974 schedNoFence::scheduler::ws:1975 Map(1976 "w1" ->1977 {1978 attached: Set(),1979 built: false,1980 expecting: false,1981 running: false,1982 session: true,1983 up: true1984 },1985 "w2" ->1986 {1987 attached: Set(),1988 built: false,1989 expecting: true,1990 running: true,1991 session: false,1992 up: true1993 }1994 )1995}19961997[State 8]1998{1999 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2000 schedNoFence::scheduler::crashes: 2,2001 schedNoFence::scheduler::entry:2002 [{ followers: Set("c2"), leased: true, worker: "w1" }],2003 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2004 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2005 schedNoFence::scheduler::mBuild: Set(),2006 schedNoFence::scheduler::mDone: Set(),2007 schedNoFence::scheduler::mExpect: Set("w1"),2008 schedNoFence::scheduler::mResult: Set(),2009 schedNoFence::scheduler::mRetry: Set(),2010 schedNoFence::scheduler::mRevoke: Set(),2011 schedNoFence::scheduler::mSchedule: Set(),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 9]2038{2039 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "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(),2050 schedNoFence::scheduler::mRevoke: Set(),2051 schedNoFence::scheduler::mSchedule: Set(),2052 schedNoFence::scheduler::published: 1,2053 schedNoFence::scheduler::publishedBy: Set("w2"),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: true,2069 expecting: false,2070 running: false,2071 session: false,2072 up: true2073 }2074 )2075}20762077[State 10]2078{2079 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "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(),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: true,2112 up: true2113 }2114 )2115}21162117[State 11]2118{2119 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "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(),2128 schedNoFence::scheduler::mResult: Set(),2129 schedNoFence::scheduler::mRetry: Set(),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: true,2141 running: true,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 12]2158{2159 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "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("w1"),2167 schedNoFence::scheduler::mExpect: Set(),2168 schedNoFence::scheduler::mResult: Set(),2169 schedNoFence::scheduler::mRetry: Set(),2170 schedNoFence::scheduler::mRevoke: Set(),2171 schedNoFence::scheduler::mSchedule: Set(),2172 schedNoFence::scheduler::published: 2,2173 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2174 schedNoFence::scheduler::ws:2175 Map(2176 "w1" ->2177 {2178 attached: Set(),2179 built: true,2180 expecting: false,2181 running: false,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[violation] Found an issue (625ms at 41334 traces/second).2198Use --verbosity=3 to show executions.2199Use --seed=0xf76f297c308b48a5 --backend=rust to reproduce.2200error: Invariant violated2201An example execution:22022203[State 0]2204{2205 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2206 schedNoPush::scheduler::crashes: 0,2207 schedNoPush::scheduler::entry: [],2208 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2209 schedNoPush::scheduler::mAssigned: Set(),2210 schedNoPush::scheduler::mBuild: Set(),2211 schedNoPush::scheduler::mDone: Set(),2212 schedNoPush::scheduler::mExpect: Set(),2213 schedNoPush::scheduler::mResult: Set(),2214 schedNoPush::scheduler::mRetry: Set(),2215 schedNoPush::scheduler::mRevoke: Set(),2216 schedNoPush::scheduler::mSchedule: Set(),2217 schedNoPush::scheduler::published: 0,2218 schedNoPush::scheduler::publishedBy: Set(),2219 schedNoPush::scheduler::ws:2220 Map(2221 "w1" ->2222 {2223 attached: Set(),2224 built: false,2225 expecting: false,2226 running: false,2227 session: true,2228 up: true2229 },2230 "w2" ->2231 {2232 attached: Set(),2233 built: false,2234 expecting: false,2235 running: false,2236 session: true,2237 up: true2238 }2239 )2240}22412242[State 1]2243{2244 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2245 schedNoPush::scheduler::crashes: 0,2246 schedNoPush::scheduler::entry: [],2247 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2248 schedNoPush::scheduler::mAssigned: Set(),2249 schedNoPush::scheduler::mBuild: Set(),2250 schedNoPush::scheduler::mDone: Set(),2251 schedNoPush::scheduler::mExpect: Set(),2252 schedNoPush::scheduler::mResult: Set(),2253 schedNoPush::scheduler::mRetry: Set(),2254 schedNoPush::scheduler::mRevoke: Set(),2255 schedNoPush::scheduler::mSchedule: Set("c1"),2256 schedNoPush::scheduler::published: 0,2257 schedNoPush::scheduler::publishedBy: Set(),2258 schedNoPush::scheduler::ws:2259 Map(2260 "w1" ->2261 {2262 attached: Set(),2263 built: false,2264 expecting: false,2265 running: false,2266 session: true,2267 up: true2268 },2269 "w2" ->2270 {2271 attached: Set(),2272 built: false,2273 expecting: false,2274 running: false,2275 session: true,2276 up: true2277 }2278 )2279}22802281[State 2]2282{2283 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2284 schedNoPush::scheduler::crashes: 1,2285 schedNoPush::scheduler::entry: [],2286 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2287 schedNoPush::scheduler::mAssigned: Set(),2288 schedNoPush::scheduler::mBuild: Set(),2289 schedNoPush::scheduler::mDone: Set(),2290 schedNoPush::scheduler::mExpect: Set(),2291 schedNoPush::scheduler::mResult: Set(),2292 schedNoPush::scheduler::mRetry: Set(),2293 schedNoPush::scheduler::mRevoke: Set(),2294 schedNoPush::scheduler::mSchedule: Set("c1"),2295 schedNoPush::scheduler::published: 0,2296 schedNoPush::scheduler::publishedBy: Set(),2297 schedNoPush::scheduler::ws:2298 Map(2299 "w1" ->2300 {2301 attached: Set(),2302 built: false,2303 expecting: false,2304 running: false,2305 session: false,2306 up: false2307 },2308 "w2" ->2309 {2310 attached: Set(),2311 built: false,2312 expecting: false,2313 running: false,2314 session: true,2315 up: true2316 }2317 )2318}23192320[State 3]2321{2322 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2323 schedNoPush::scheduler::crashes: 1,2324 schedNoPush::scheduler::entry:2325 [{ followers: Set("c1"), leased: true, worker: "w2" }],2326 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2327 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2328 schedNoPush::scheduler::mBuild: Set(),2329 schedNoPush::scheduler::mDone: Set(),2330 schedNoPush::scheduler::mExpect: Set(),2331 schedNoPush::scheduler::mResult: Set(),2332 schedNoPush::scheduler::mRetry: Set(),2333 schedNoPush::scheduler::mRevoke: Set(),2334 schedNoPush::scheduler::mSchedule: Set(),2335 schedNoPush::scheduler::published: 0,2336 schedNoPush::scheduler::publishedBy: Set(),2337 schedNoPush::scheduler::ws:2338 Map(2339 "w1" ->2340 {2341 attached: Set(),2342 built: false,2343 expecting: false,2344 running: false,2345 session: false,2346 up: false2347 },2348 "w2" ->2349 {2350 attached: Set(),2351 built: false,2352 expecting: false,2353 running: false,2354 session: true,2355 up: true2356 }2357 )2358}23592360[State 4]2361{2362 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2363 schedNoPush::scheduler::crashes: 1,2364 schedNoPush::scheduler::entry:2365 [{ followers: Set("c1"), leased: true, worker: "w2" }],2366 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2367 schedNoPush::scheduler::mAssigned: Set(),2368 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2369 schedNoPush::scheduler::mDone: Set(),2370 schedNoPush::scheduler::mExpect: Set(),2371 schedNoPush::scheduler::mResult: Set(),2372 schedNoPush::scheduler::mRetry: Set(),2373 schedNoPush::scheduler::mRevoke: Set(),2374 schedNoPush::scheduler::mSchedule: Set(),2375 schedNoPush::scheduler::published: 0,2376 schedNoPush::scheduler::publishedBy: Set(),2377 schedNoPush::scheduler::ws:2378 Map(2379 "w1" ->2380 {2381 attached: Set(),2382 built: false,2383 expecting: false,2384 running: false,2385 session: false,2386 up: false2387 },2388 "w2" ->2389 {2390 attached: Set(),2391 built: false,2392 expecting: false,2393 running: false,2394 session: true,2395 up: true2396 }2397 )2398}23992400[State 5]2401{2402 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2403 schedNoPush::scheduler::crashes: 2,2404 schedNoPush::scheduler::entry: [],2405 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2406 schedNoPush::scheduler::mAssigned: Set(),2407 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2408 schedNoPush::scheduler::mDone: Set(),2409 schedNoPush::scheduler::mExpect: Set(),2410 schedNoPush::scheduler::mResult: Set(),2411 schedNoPush::scheduler::mRetry: Set(),2412 schedNoPush::scheduler::mRevoke: Set(),2413 schedNoPush::scheduler::mSchedule: Set(),2414 schedNoPush::scheduler::published: 0,2415 schedNoPush::scheduler::publishedBy: Set(),2416 schedNoPush::scheduler::ws:2417 Map(2418 "w1" ->2419 {2420 attached: Set(),2421 built: false,2422 expecting: false,2423 running: false,2424 session: false,2425 up: false2426 },2427 "w2" ->2428 {2429 attached: Set(),2430 built: false,2431 expecting: false,2432 running: false,2433 session: false,2434 up: true2435 }2436 )2437}24382439[State 6]2440{2441 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2442 schedNoPush::scheduler::crashes: 2,2443 schedNoPush::scheduler::entry: [],2444 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2445 schedNoPush::scheduler::mAssigned: Set(),2446 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2447 schedNoPush::scheduler::mDone: Set(),2448 schedNoPush::scheduler::mExpect: Set(),2449 schedNoPush::scheduler::mResult: Set(),2450 schedNoPush::scheduler::mRetry: Set(),2451 schedNoPush::scheduler::mRevoke: Set(),2452 schedNoPush::scheduler::mSchedule: Set(),2453 schedNoPush::scheduler::published: 0,2454 schedNoPush::scheduler::publishedBy: Set(),2455 schedNoPush::scheduler::ws:2456 Map(2457 "w1" ->2458 {2459 attached: Set(),2460 built: false,2461 expecting: false,2462 running: false,2463 session: false,2464 up: false2465 },2466 "w2" ->2467 {2468 attached: Set(),2469 built: false,2470 expecting: false,2471 running: false,2472 session: true,2473 up: true2474 }2475 )2476}24772478[State 7]2479{2480 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2481 schedNoPush::scheduler::crashes: 2,2482 schedNoPush::scheduler::entry: [],2483 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2484 schedNoPush::scheduler::mAssigned: Set(),2485 schedNoPush::scheduler::mBuild: Set(),2486 schedNoPush::scheduler::mDone: Set(),2487 schedNoPush::scheduler::mExpect: Set(),2488 schedNoPush::scheduler::mResult: Set(),2489 schedNoPush::scheduler::mRetry: Set(),2490 schedNoPush::scheduler::mRevoke: Set(),2491 schedNoPush::scheduler::mSchedule: Set(),2492 schedNoPush::scheduler::published: 0,2493 schedNoPush::scheduler::publishedBy: Set(),2494 schedNoPush::scheduler::ws:2495 Map(2496 "w1" ->2497 {2498 attached: Set(),2499 built: false,2500 expecting: false,2501 running: false,2502 session: false,2503 up: false2504 },2505 "w2" ->2506 {2507 attached: Set("c1"),2508 built: false,2509 expecting: true,2510 running: true,2511 session: true,2512 up: true2513 }2514 )2515}25162517[violation] Found an issue (435ms at 30807 traces/second).2518Use --verbosity=3 to show executions.2519Use --seed=0x5513fc8a1289d872 --backend=rust to reproduce.2520error: Invariant violated2521An example execution:25222523[State 0]2524{2525 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2526 schedNoReport::scheduler::crashes: 0,2527 schedNoReport::scheduler::entry: [],2528 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2529 schedNoReport::scheduler::mAssigned: Set(),2530 schedNoReport::scheduler::mBuild: Set(),2531 schedNoReport::scheduler::mDone: Set(),2532 schedNoReport::scheduler::mExpect: Set(),2533 schedNoReport::scheduler::mResult: Set(),2534 schedNoReport::scheduler::mRetry: Set(),2535 schedNoReport::scheduler::mRevoke: Set(),2536 schedNoReport::scheduler::mSchedule: Set(),2537 schedNoReport::scheduler::published: 0,2538 schedNoReport::scheduler::publishedBy: Set(),2539 schedNoReport::scheduler::ws:2540 Map(2541 "w1" ->2542 {2543 attached: Set(),2544 built: false,2545 expecting: false,2546 running: false,2547 session: true,2548 up: true2549 },2550 "w2" ->2551 {2552 attached: Set(),2553 built: false,2554 expecting: false,2555 running: false,2556 session: true,2557 up: true2558 }2559 )2560}25612562[State 1]2563{2564 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2565 schedNoReport::scheduler::crashes: 0,2566 schedNoReport::scheduler::entry: [],2567 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2568 schedNoReport::scheduler::mAssigned: Set(),2569 schedNoReport::scheduler::mBuild: Set(),2570 schedNoReport::scheduler::mDone: Set(),2571 schedNoReport::scheduler::mExpect: Set(),2572 schedNoReport::scheduler::mResult: Set(),2573 schedNoReport::scheduler::mRetry: Set(),2574 schedNoReport::scheduler::mRevoke: Set(),2575 schedNoReport::scheduler::mSchedule: Set("c2"),2576 schedNoReport::scheduler::published: 0,2577 schedNoReport::scheduler::publishedBy: Set(),2578 schedNoReport::scheduler::ws:2579 Map(2580 "w1" ->2581 {2582 attached: Set(),2583 built: false,2584 expecting: false,2585 running: false,2586 session: true,2587 up: true2588 },2589 "w2" ->2590 {2591 attached: Set(),2592 built: false,2593 expecting: false,2594 running: false,2595 session: true,2596 up: true2597 }2598 )2599}26002601[State 2]2602{2603 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2604 schedNoReport::scheduler::crashes: 0,2605 schedNoReport::scheduler::entry:2606 [{ followers: Set("c2"), leased: true, worker: "w1" }],2607 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2608 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2609 schedNoReport::scheduler::mBuild: Set(),2610 schedNoReport::scheduler::mDone: Set(),2611 schedNoReport::scheduler::mExpect: Set("w1"),2612 schedNoReport::scheduler::mResult: Set(),2613 schedNoReport::scheduler::mRetry: Set(),2614 schedNoReport::scheduler::mRevoke: Set(),2615 schedNoReport::scheduler::mSchedule: Set(),2616 schedNoReport::scheduler::published: 0,2617 schedNoReport::scheduler::publishedBy: Set(),2618 schedNoReport::scheduler::ws:2619 Map(2620 "w1" ->2621 {2622 attached: Set(),2623 built: false,2624 expecting: false,2625 running: false,2626 session: true,2627 up: true2628 },2629 "w2" ->2630 {2631 attached: Set(),2632 built: false,2633 expecting: false,2634 running: false,2635 session: true,2636 up: true2637 }2638 )2639}26402641[State 3]2642{2643 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2644 schedNoReport::scheduler::crashes: 1,2645 schedNoReport::scheduler::entry:2646 [{ followers: Set("c2"), leased: true, worker: "w1" }],2647 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2648 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2649 schedNoReport::scheduler::mBuild: Set(),2650 schedNoReport::scheduler::mDone: Set(),2651 schedNoReport::scheduler::mExpect: Set("w1"),2652 schedNoReport::scheduler::mResult: Set(),2653 schedNoReport::scheduler::mRetry: Set(),2654 schedNoReport::scheduler::mRevoke: Set(),2655 schedNoReport::scheduler::mSchedule: Set(),2656 schedNoReport::scheduler::published: 0,2657 schedNoReport::scheduler::publishedBy: Set(),2658 schedNoReport::scheduler::ws:2659 Map(2660 "w1" ->2661 {2662 attached: Set(),2663 built: false,2664 expecting: false,2665 running: false,2666 session: true,2667 up: true2668 },2669 "w2" ->2670 {2671 attached: Set(),2672 built: false,2673 expecting: false,2674 running: false,2675 session: false,2676 up: false2677 }2678 )2679}26802681[State 4]2682{2683 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2684 schedNoReport::scheduler::crashes: 1,2685 schedNoReport::scheduler::entry:2686 [{ followers: Set("c2"), leased: true, worker: "w1" }],2687 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2688 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2689 schedNoReport::scheduler::mBuild: Set(),2690 schedNoReport::scheduler::mDone: Set(),2691 schedNoReport::scheduler::mExpect: Set(),2692 schedNoReport::scheduler::mResult: Set(),2693 schedNoReport::scheduler::mRetry: Set(),2694 schedNoReport::scheduler::mRevoke: Set(),2695 schedNoReport::scheduler::mSchedule: Set(),2696 schedNoReport::scheduler::published: 0,2697 schedNoReport::scheduler::publishedBy: Set(),2698 schedNoReport::scheduler::ws:2699 Map(2700 "w1" ->2701 {2702 attached: Set(),2703 built: false,2704 expecting: true,2705 running: true,2706 session: true,2707 up: true2708 },2709 "w2" ->2710 {2711 attached: Set(),2712 built: false,2713 expecting: false,2714 running: false,2715 session: false,2716 up: false2717 }2718 )2719}27202721[State 5]2722{2723 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2724 schedNoReport::scheduler::crashes: 2,2725 schedNoReport::scheduler::entry: [],2726 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2727 schedNoReport::scheduler::mAssigned: Set(),2728 schedNoReport::scheduler::mBuild: Set(),2729 schedNoReport::scheduler::mDone: Set(),2730 schedNoReport::scheduler::mExpect: Set(),2731 schedNoReport::scheduler::mResult: Set(),2732 schedNoReport::scheduler::mRetry: Set("c2"),2733 schedNoReport::scheduler::mRevoke: Set(),2734 schedNoReport::scheduler::mSchedule: Set(),2735 schedNoReport::scheduler::published: 0,2736 schedNoReport::scheduler::publishedBy: Set(),2737 schedNoReport::scheduler::ws:2738 Map(2739 "w1" ->2740 {2741 attached: Set(),2742 built: false,2743 expecting: true,2744 running: true,2745 session: false,2746 up: true2747 },2748 "w2" ->2749 {2750 attached: Set(),2751 built: false,2752 expecting: false,2753 running: false,2754 session: false,2755 up: false2756 }2757 )2758}27592760[State 6]2761{2762 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2763 schedNoReport::scheduler::crashes: 2,2764 schedNoReport::scheduler::entry: [],2765 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2766 schedNoReport::scheduler::mAssigned: Set(),2767 schedNoReport::scheduler::mBuild: Set(),2768 schedNoReport::scheduler::mDone: Set(),2769 schedNoReport::scheduler::mExpect: Set(),2770 schedNoReport::scheduler::mResult: Set(),2771 schedNoReport::scheduler::mRetry: Set("c2"),2772 schedNoReport::scheduler::mRevoke: Set(),2773 schedNoReport::scheduler::mSchedule: Set(),2774 schedNoReport::scheduler::published: 0,2775 schedNoReport::scheduler::publishedBy: Set(),2776 schedNoReport::scheduler::ws:2777 Map(2778 "w1" ->2779 {2780 attached: Set(),2781 built: false,2782 expecting: true,2783 running: true,2784 session: true,2785 up: true2786 },2787 "w2" ->2788 {2789 attached: Set(),2790 built: false,2791 expecting: false,2792 running: false,2793 session: false,2794 up: false2795 }2796 )2797}27982799[State 7]2800{2801 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2802 schedNoReport::scheduler::crashes: 2,2803 schedNoReport::scheduler::entry: [],2804 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2805 schedNoReport::scheduler::mAssigned: Set(),2806 schedNoReport::scheduler::mBuild: Set(),2807 schedNoReport::scheduler::mDone: Set(),2808 schedNoReport::scheduler::mExpect: Set(),2809 schedNoReport::scheduler::mResult: Set(),2810 schedNoReport::scheduler::mRetry: Set("c2"),2811 schedNoReport::scheduler::mRevoke: Set(),2812 schedNoReport::scheduler::mSchedule: Set(),2813 schedNoReport::scheduler::published: 0,2814 schedNoReport::scheduler::publishedBy: Set(),2815 schedNoReport::scheduler::ws:2816 Map(2817 "w1" ->2818 {2819 attached: Set(),2820 built: false,2821 expecting: true,2822 running: true,2823 session: true,2824 up: true2825 },2826 "w2" ->2827 {2828 attached: Set(),2829 built: false,2830 expecting: false,2831 running: false,2832 session: true,2833 up: true2834 }2835 )2836}28372838[State 8]2839{2840 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2841 schedNoReport::scheduler::crashes: 2,2842 schedNoReport::scheduler::entry: [],2843 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2844 schedNoReport::scheduler::mAssigned: Set(),2845 schedNoReport::scheduler::mBuild: Set(),2846 schedNoReport::scheduler::mDone: Set(),2847 schedNoReport::scheduler::mExpect: Set(),2848 schedNoReport::scheduler::mResult: Set(),2849 schedNoReport::scheduler::mRetry: Set("c2"),2850 schedNoReport::scheduler::mRevoke: Set(),2851 schedNoReport::scheduler::mSchedule: Set("c1"),2852 schedNoReport::scheduler::published: 0,2853 schedNoReport::scheduler::publishedBy: Set(),2854 schedNoReport::scheduler::ws:2855 Map(2856 "w1" ->2857 {2858 attached: Set(),2859 built: false,2860 expecting: true,2861 running: true,2862 session: true,2863 up: true2864 },2865 "w2" ->2866 {2867 attached: Set(),2868 built: false,2869 expecting: false,2870 running: false,2871 session: true,2872 up: true2873 }2874 )2875}28762877[State 9]2878{2879 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2880 schedNoReport::scheduler::crashes: 2,2881 schedNoReport::scheduler::entry:2882 [{ followers: Set("c1"), leased: true, worker: "w2" }],2883 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2884 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2885 schedNoReport::scheduler::mBuild: Set(),2886 schedNoReport::scheduler::mDone: Set(),2887 schedNoReport::scheduler::mExpect: Set("w2"),2888 schedNoReport::scheduler::mResult: Set(),2889 schedNoReport::scheduler::mRetry: Set("c2"),2890 schedNoReport::scheduler::mRevoke: Set(),2891 schedNoReport::scheduler::mSchedule: Set(),2892 schedNoReport::scheduler::published: 0,2893 schedNoReport::scheduler::publishedBy: Set(),2894 schedNoReport::scheduler::ws:2895 Map(2896 "w1" ->2897 {2898 attached: Set(),2899 built: false,2900 expecting: true,2901 running: true,2902 session: true,2903 up: true2904 },2905 "w2" ->2906 {2907 attached: Set(),2908 built: false,2909 expecting: false,2910 running: false,2911 session: true,2912 up: true2913 }2914 )2915}29162917[State 10]2918{2919 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2920 schedNoReport::scheduler::crashes: 2,2921 schedNoReport::scheduler::entry:2922 [{ followers: Set("c1"), leased: true, worker: "w2" }],2923 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2924 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2925 schedNoReport::scheduler::mBuild: Set(),2926 schedNoReport::scheduler::mDone: Set(),2927 schedNoReport::scheduler::mExpect: Set(),2928 schedNoReport::scheduler::mResult: Set(),2929 schedNoReport::scheduler::mRetry: Set("c2"),2930 schedNoReport::scheduler::mRevoke: Set(),2931 schedNoReport::scheduler::mSchedule: Set(),2932 schedNoReport::scheduler::published: 0,2933 schedNoReport::scheduler::publishedBy: Set(),2934 schedNoReport::scheduler::ws:2935 Map(2936 "w1" ->2937 {2938 attached: Set(),2939 built: false,2940 expecting: true,2941 running: true,2942 session: true,2943 up: true2944 },2945 "w2" ->2946 {2947 attached: Set(),2948 built: false,2949 expecting: true,2950 running: true,2951 session: true,2952 up: true2953 }2954 )2955}29562957[violation] Found an issue (468ms at 47295 traces/second).2958Use --verbosity=3 to show executions.2959Use --seed=0x569bf8bfbca3e65a --backend=rust to reproduce.2960error: Invariant violated2961An example execution:29622963[State 0]2964{2965 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2966 schedTerminal::scheduler::crashes: 0,2967 schedTerminal::scheduler::entry: [],2968 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2969 schedTerminal::scheduler::mAssigned: Set(),2970 schedTerminal::scheduler::mBuild: Set(),2971 schedTerminal::scheduler::mDone: Set(),2972 schedTerminal::scheduler::mExpect: Set(),2973 schedTerminal::scheduler::mResult: Set(),2974 schedTerminal::scheduler::mRetry: Set(),2975 schedTerminal::scheduler::mRevoke: Set(),2976 schedTerminal::scheduler::mSchedule: Set(),2977 schedTerminal::scheduler::published: 0,2978 schedTerminal::scheduler::publishedBy: Set(),2979 schedTerminal::scheduler::ws:2980 Map(2981 "w1" ->2982 {2983 attached: Set(),2984 built: false,2985 expecting: false,2986 running: false,2987 session: true,2988 up: true2989 },2990 "w2" ->2991 {2992 attached: Set(),2993 built: false,2994 expecting: false,2995 running: false,2996 session: true,2997 up: true2998 }2999 )3000}30013002[State 1]3003{3004 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3005 schedTerminal::scheduler::crashes: 1,3006 schedTerminal::scheduler::entry: [],3007 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3008 schedTerminal::scheduler::mAssigned: Set(),3009 schedTerminal::scheduler::mBuild: Set(),3010 schedTerminal::scheduler::mDone: Set(),3011 schedTerminal::scheduler::mExpect: Set(),3012 schedTerminal::scheduler::mResult: Set(),3013 schedTerminal::scheduler::mRetry: Set(),3014 schedTerminal::scheduler::mRevoke: Set(),3015 schedTerminal::scheduler::mSchedule: Set(),3016 schedTerminal::scheduler::published: 0,3017 schedTerminal::scheduler::publishedBy: Set(),3018 schedTerminal::scheduler::ws:3019 Map(3020 "w1" ->3021 {3022 attached: Set(),3023 built: false,3024 expecting: false,3025 running: false,3026 session: false,3027 up: true3028 },3029 "w2" ->3030 {3031 attached: Set(),3032 built: false,3033 expecting: false,3034 running: false,3035 session: false,3036 up: true3037 }3038 )3039}30403041[State 2]3042{3043 schedTerminal::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),3044 schedTerminal::scheduler::crashes: 1,3045 schedTerminal::scheduler::entry: [],3046 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3047 schedTerminal::scheduler::mAssigned: Set(),3048 schedTerminal::scheduler::mBuild: Set(),3049 schedTerminal::scheduler::mDone: Set(),3050 schedTerminal::scheduler::mExpect: Set(),3051 schedTerminal::scheduler::mResult: Set(),3052 schedTerminal::scheduler::mRetry: Set(),3053 schedTerminal::scheduler::mRevoke: Set(),3054 schedTerminal::scheduler::mSchedule: Set("c1"),3055 schedTerminal::scheduler::published: 0,3056 schedTerminal::scheduler::publishedBy: Set(),3057 schedTerminal::scheduler::ws:3058 Map(3059 "w1" ->3060 {3061 attached: Set(),3062 built: false,3063 expecting: false,3064 running: false,3065 session: false,3066 up: true3067 },3068 "w2" ->3069 {3070 attached: Set(),3071 built: false,3072 expecting: false,3073 running: false,3074 session: false,3075 up: true3076 }3077 )3078}30793080[State 3]3081{3082 schedTerminal::scheduler::cl: Map("c1" -> CFailed, "c2" -> CIdle),3083 schedTerminal::scheduler::crashes: 1,3084 schedTerminal::scheduler::entry: [],3085 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3086 schedTerminal::scheduler::mAssigned: Set(),3087 schedTerminal::scheduler::mBuild: Set(),3088 schedTerminal::scheduler::mDone: Set(),3089 schedTerminal::scheduler::mExpect: Set(),3090 schedTerminal::scheduler::mResult: Set(),3091 schedTerminal::scheduler::mRetry: Set(),3092 schedTerminal::scheduler::mRevoke: Set(),3093 schedTerminal::scheduler::mSchedule: Set(),3094 schedTerminal::scheduler::published: 0,3095 schedTerminal::scheduler::publishedBy: Set(),3096 schedTerminal::scheduler::ws:3097 Map(3098 "w1" ->3099 {3100 attached: Set(),3101 built: false,3102 expecting: false,3103 running: false,3104 session: false,3105 up: true3106 },3107 "w2" ->3108 {3109 attached: Set(),3110 built: false,3111 expecting: false,3112 running: false,3113 session: false,3114 up: true3115 }3116 )3117}31183119[violation] Found an issue (152ms at 5888 traces/second).3120Use --verbosity=3 to show executions.3121Use --seed=0x505fb545b61fb2ef --backend=rust to reproduce.3122error: Invariant violated3123An example execution:31243125[State 0]3126{3127 pushFixed::push::byPath: Map(),3128 pushFixed::push::inflight: Set(),3129 pushFixed::push::left: Map(),3130 pushFixed::push::sent: Map()3131}31323133[State 1]3134{3135 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3136 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3137 pushFixed::push::left: Map(2 -> 2),3138 pushFixed::push::sent: Map(2 -> Set("a", "b"))3139}31403141[State 2]3142{3143 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3144 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),3145 pushFixed::push::left: Map(1 -> 2, 2 -> 2),3146 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3147}31483149[State 3]3150{3151 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3152 pushFixed::push::inflight: Set((1, "a"), (2, "a"), (2, "b")),3153 pushFixed::push::left: Map(1 -> 1, 2 -> 2),3154 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3155}31563157[State 4]3158{3159 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3160 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3161 pushFixed::push::left: Map(1 -> 0, 2 -> 2),3162 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3163}31643165[State 5]3166{3167 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3168 pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "a"), (3, "b")),3169 pushFixed::push::left: Map(1 -> 0, 2 -> 2, 3 -> 2),3170 pushFixed::push::sent:3171 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3172}31733174[State 6]3175{3176 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3177 pushFixed::push::inflight: Set((2, "a"), (3, "a"), (3, "b")),3178 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 2),3179 pushFixed::push::sent:3180 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3181}31823183[State 7]3184{3185 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3186 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3187 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 2),3188 pushFixed::push::sent:3189 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3190}31913192[State 8]3193{3194 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3195 pushFixed::push::inflight: Set((3, "a")),3196 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 1),3197 pushFixed::push::sent:3198 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3199}32003201[State 9]3202{3203 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3204 pushFixed::push::inflight: Set(),3205 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3206 pushFixed::push::sent:3207 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3208}32093210[ok] No violation found (91ms at 219780 traces/second).3211Trace length statistics: max=10, min=7, average=7.993212You may increase --max-samples and --max-steps.3213Use --verbosity to produce more (or less) output.3214Use --seed=0x52476f7214d825a2 --backend=rust to reproduce.