nix-grpc-store-spec
checks.aarch64-linux.spec
· build #215
· raw
1tribuchet: building on eliza2An example execution:34[State 0]5{6 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),7 schedFixed::scheduler::crashes: 0,8 schedFixed::scheduler::entry: [],9 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),10 schedFixed::scheduler::mAssigned: Set(),11 schedFixed::scheduler::mBuild: Set(),12 schedFixed::scheduler::mDone: Set(),13 schedFixed::scheduler::mExpect: Set(),14 schedFixed::scheduler::mResult: Set(),15 schedFixed::scheduler::mRetry: Set(),16 schedFixed::scheduler::mRevoke: Set(),17 schedFixed::scheduler::mSchedule: Set(),18 schedFixed::scheduler::published: 0,19 schedFixed::scheduler::publishedBy: Set(),20 schedFixed::scheduler::ws:21 Map(22 "w1" ->23 {24 attached: Set(),25 built: false,26 expecting: false,27 running: false,28 session: true,29 up: true30 },31 "w2" ->32 {33 attached: Set(),34 built: false,35 expecting: false,36 running: false,37 session: true,38 up: true39 }40 )41}4243[State 1]44{45 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),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("c2"),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" -> CIdle, "c2" -> CQueued),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("c2"),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: false,116 up: true117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),124 schedFixed::scheduler::crashes: 1,125 schedFixed::scheduler::entry: [],126 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),127 schedFixed::scheduler::mAssigned: Set(),128 schedFixed::scheduler::mBuild: Set(),129 schedFixed::scheduler::mDone: Set(),130 schedFixed::scheduler::mExpect: Set(),131 schedFixed::scheduler::mResult: Set(),132 schedFixed::scheduler::mRetry: Set("c2"),133 schedFixed::scheduler::mRevoke: Set(),134 schedFixed::scheduler::mSchedule: Set("c1"),135 schedFixed::scheduler::published: 0,136 schedFixed::scheduler::publishedBy: Set(),137 schedFixed::scheduler::ws:138 Map(139 "w1" ->140 {141 attached: Set(),142 built: false,143 expecting: false,144 running: false,145 session: false,146 up: true147 },148 "w2" ->149 {150 attached: Set(),151 built: false,152 expecting: false,153 running: false,154 session: false,155 up: true156 }157 )158}159160[State 4]161{162 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),163 schedFixed::scheduler::crashes: 1,164 schedFixed::scheduler::entry: [],165 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),166 schedFixed::scheduler::mAssigned: Set(),167 schedFixed::scheduler::mBuild: Set(),168 schedFixed::scheduler::mDone: Set(),169 schedFixed::scheduler::mExpect: Set(),170 schedFixed::scheduler::mResult: Set(),171 schedFixed::scheduler::mRetry: Set("c2"),172 schedFixed::scheduler::mRevoke: Set(),173 schedFixed::scheduler::mSchedule: Set("c1"),174 schedFixed::scheduler::published: 0,175 schedFixed::scheduler::publishedBy: Set(),176 schedFixed::scheduler::ws:177 Map(178 "w1" ->179 {180 attached: Set(),181 built: false,182 expecting: false,183 running: false,184 session: false,185 up: true186 },187 "w2" ->188 {189 attached: Set(),190 built: false,191 expecting: false,192 running: false,193 session: true,194 up: true195 }196 )197}198199[State 5]200{201 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),202 schedFixed::scheduler::crashes: 1,203 schedFixed::scheduler::entry:204 [{ followers: Set("c1"), leased: true, worker: "w2" }],205 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),206 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),207 schedFixed::scheduler::mBuild: Set(),208 schedFixed::scheduler::mDone: Set(),209 schedFixed::scheduler::mExpect: Set("w2"),210 schedFixed::scheduler::mResult: Set(),211 schedFixed::scheduler::mRetry: Set("c2"),212 schedFixed::scheduler::mRevoke: Set(),213 schedFixed::scheduler::mSchedule: Set(),214 schedFixed::scheduler::published: 0,215 schedFixed::scheduler::publishedBy: Set(),216 schedFixed::scheduler::ws:217 Map(218 "w1" ->219 {220 attached: Set(),221 built: false,222 expecting: false,223 running: false,224 session: false,225 up: true226 },227 "w2" ->228 {229 attached: Set(),230 built: false,231 expecting: false,232 running: false,233 session: true,234 up: true235 }236 )237}238239[State 6]240{241 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),242 schedFixed::scheduler::crashes: 2,243 schedFixed::scheduler::entry: [],244 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),245 schedFixed::scheduler::mAssigned: Set(),246 schedFixed::scheduler::mBuild: Set(),247 schedFixed::scheduler::mDone: Set(),248 schedFixed::scheduler::mExpect: Set(),249 schedFixed::scheduler::mResult: Set(),250 schedFixed::scheduler::mRetry: Set("c1", "c2"),251 schedFixed::scheduler::mRevoke: Set(),252 schedFixed::scheduler::mSchedule: Set(),253 schedFixed::scheduler::published: 0,254 schedFixed::scheduler::publishedBy: Set(),255 schedFixed::scheduler::ws:256 Map(257 "w1" ->258 {259 attached: Set(),260 built: false,261 expecting: false,262 running: false,263 session: false,264 up: true265 },266 "w2" ->267 {268 attached: Set(),269 built: false,270 expecting: false,271 running: false,272 session: false,273 up: true274 }275 )276}277278[State 7]279{280 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),281 schedFixed::scheduler::crashes: 2,282 schedFixed::scheduler::entry: [],283 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),284 schedFixed::scheduler::mAssigned: Set(),285 schedFixed::scheduler::mBuild: Set(),286 schedFixed::scheduler::mDone: Set(),287 schedFixed::scheduler::mExpect: Set(),288 schedFixed::scheduler::mResult: Set(),289 schedFixed::scheduler::mRetry: Set("c1", "c2"),290 schedFixed::scheduler::mRevoke: Set(),291 schedFixed::scheduler::mSchedule: Set(),292 schedFixed::scheduler::published: 0,293 schedFixed::scheduler::publishedBy: Set(),294 schedFixed::scheduler::ws:295 Map(296 "w1" ->297 {298 attached: Set(),299 built: false,300 expecting: false,301 running: false,302 session: false,303 up: 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 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),323 schedFixed::scheduler::mAssigned: Set(),324 schedFixed::scheduler::mBuild: Set(),325 schedFixed::scheduler::mDone: Set(),326 schedFixed::scheduler::mExpect: Set(),327 schedFixed::scheduler::mResult: Set(),328 schedFixed::scheduler::mRetry: Set("c2"),329 schedFixed::scheduler::mRevoke: Set(),330 schedFixed::scheduler::mSchedule: Set("c1"),331 schedFixed::scheduler::published: 0,332 schedFixed::scheduler::publishedBy: Set(),333 schedFixed::scheduler::ws:334 Map(335 "w1" ->336 {337 attached: Set(),338 built: false,339 expecting: false,340 running: false,341 session: false,342 up: true343 },344 "w2" ->345 {346 attached: Set(),347 built: false,348 expecting: false,349 running: false,350 session: true,351 up: true352 }353 )354}355356[State 9]357{358 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),359 schedFixed::scheduler::crashes: 2,360 schedFixed::scheduler::entry: [],361 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),362 schedFixed::scheduler::mAssigned: Set(),363 schedFixed::scheduler::mBuild: Set(),364 schedFixed::scheduler::mDone: Set(),365 schedFixed::scheduler::mExpect: Set(),366 schedFixed::scheduler::mResult: Set(),367 schedFixed::scheduler::mRetry: Set(),368 schedFixed::scheduler::mRevoke: Set(),369 schedFixed::scheduler::mSchedule: Set("c1", "c2"),370 schedFixed::scheduler::published: 0,371 schedFixed::scheduler::publishedBy: Set(),372 schedFixed::scheduler::ws:373 Map(374 "w1" ->375 {376 attached: Set(),377 built: false,378 expecting: false,379 running: false,380 session: false,381 up: true382 },383 "w2" ->384 {385 attached: Set(),386 built: false,387 expecting: false,388 running: false,389 session: true,390 up: true391 }392 )393}394395[State 10]396{397 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),398 schedFixed::scheduler::crashes: 2,399 schedFixed::scheduler::entry:400 [{ followers: Set("c1"), leased: true, worker: "w2" }],401 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),402 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),403 schedFixed::scheduler::mBuild: Set(),404 schedFixed::scheduler::mDone: Set(),405 schedFixed::scheduler::mExpect: Set("w2"),406 schedFixed::scheduler::mResult: Set(),407 schedFixed::scheduler::mRetry: Set(),408 schedFixed::scheduler::mRevoke: Set(),409 schedFixed::scheduler::mSchedule: Set("c2"),410 schedFixed::scheduler::published: 0,411 schedFixed::scheduler::publishedBy: Set(),412 schedFixed::scheduler::ws:413 Map(414 "w1" ->415 {416 attached: Set(),417 built: false,418 expecting: false,419 running: false,420 session: false,421 up: true422 },423 "w2" ->424 {425 attached: Set(),426 built: false,427 expecting: false,428 running: false,429 session: true,430 up: true431 }432 )433}434435[State 11]436{437 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),438 schedFixed::scheduler::crashes: 2,439 schedFixed::scheduler::entry:440 [{ followers: Set("c1"), leased: true, worker: "w2" }],441 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),442 schedFixed::scheduler::mAssigned: Set(),443 schedFixed::scheduler::mBuild: Set(("c1", "w2")),444 schedFixed::scheduler::mDone: Set(),445 schedFixed::scheduler::mExpect: Set("w2"),446 schedFixed::scheduler::mResult: Set(),447 schedFixed::scheduler::mRetry: Set(),448 schedFixed::scheduler::mRevoke: Set(),449 schedFixed::scheduler::mSchedule: Set("c2"),450 schedFixed::scheduler::published: 0,451 schedFixed::scheduler::publishedBy: Set(),452 schedFixed::scheduler::ws:453 Map(454 "w1" ->455 {456 attached: Set(),457 built: false,458 expecting: false,459 running: false,460 session: false,461 up: true462 },463 "w2" ->464 {465 attached: Set(),466 built: false,467 expecting: false,468 running: false,469 session: true,470 up: true471 }472 )473}474475[State 12]476{477 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),478 schedFixed::scheduler::crashes: 2,479 schedFixed::scheduler::entry:480 [{ followers: Set("c1"), leased: true, worker: "w2" }],481 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),482 schedFixed::scheduler::mAssigned: Set(),483 schedFixed::scheduler::mBuild: Set(("c1", "w2")),484 schedFixed::scheduler::mDone: Set(),485 schedFixed::scheduler::mExpect: Set("w2"),486 schedFixed::scheduler::mResult: Set(),487 schedFixed::scheduler::mRetry: Set(),488 schedFixed::scheduler::mRevoke: Set(),489 schedFixed::scheduler::mSchedule: Set("c2"),490 schedFixed::scheduler::published: 0,491 schedFixed::scheduler::publishedBy: Set(),492 schedFixed::scheduler::ws:493 Map(494 "w1" ->495 {496 attached: Set(),497 built: false,498 expecting: false,499 running: false,500 session: true,501 up: true502 },503 "w2" ->504 {505 attached: Set(),506 built: false,507 expecting: false,508 running: false,509 session: true,510 up: true511 }512 )513}514515[State 13]516{517 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),518 schedFixed::scheduler::crashes: 2,519 schedFixed::scheduler::entry:520 [{ followers: Set("c1"), leased: true, worker: "w2" }],521 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),522 schedFixed::scheduler::mAssigned: Set(),523 schedFixed::scheduler::mBuild: Set(),524 schedFixed::scheduler::mDone: Set(),525 schedFixed::scheduler::mExpect: Set("w2"),526 schedFixed::scheduler::mResult: Set(),527 schedFixed::scheduler::mRetry: Set("c1"),528 schedFixed::scheduler::mRevoke: Set(),529 schedFixed::scheduler::mSchedule: Set("c2"),530 schedFixed::scheduler::published: 0,531 schedFixed::scheduler::publishedBy: Set(),532 schedFixed::scheduler::ws:533 Map(534 "w1" ->535 {536 attached: Set(),537 built: false,538 expecting: false,539 running: false,540 session: true,541 up: true542 },543 "w2" ->544 {545 attached: Set(),546 built: false,547 expecting: false,548 running: false,549 session: true,550 up: true551 }552 )553}554555[State 14]556{557 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),558 schedFixed::scheduler::crashes: 2,559 schedFixed::scheduler::entry:560 [{ followers: Set("c1"), leased: true, worker: "w2" }],561 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),562 schedFixed::scheduler::mAssigned: Set(),563 schedFixed::scheduler::mBuild: Set(),564 schedFixed::scheduler::mDone: Set(),565 schedFixed::scheduler::mExpect: Set("w2"),566 schedFixed::scheduler::mResult: Set(),567 schedFixed::scheduler::mRetry: Set(),568 schedFixed::scheduler::mRevoke: Set(),569 schedFixed::scheduler::mSchedule: Set("c1", "c2"),570 schedFixed::scheduler::published: 0,571 schedFixed::scheduler::publishedBy: Set(),572 schedFixed::scheduler::ws:573 Map(574 "w1" ->575 {576 attached: Set(),577 built: false,578 expecting: false,579 running: false,580 session: true,581 up: true582 },583 "w2" ->584 {585 attached: Set(),586 built: false,587 expecting: false,588 running: false,589 session: true,590 up: true591 }592 )593}594595[State 15]596{597 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),598 schedFixed::scheduler::crashes: 2,599 schedFixed::scheduler::entry:600 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],601 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),602 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),603 schedFixed::scheduler::mBuild: Set(),604 schedFixed::scheduler::mDone: Set(),605 schedFixed::scheduler::mExpect: Set("w2"),606 schedFixed::scheduler::mResult: Set(),607 schedFixed::scheduler::mRetry: Set(),608 schedFixed::scheduler::mRevoke: Set(),609 schedFixed::scheduler::mSchedule: Set("c1"),610 schedFixed::scheduler::published: 0,611 schedFixed::scheduler::publishedBy: Set(),612 schedFixed::scheduler::ws:613 Map(614 "w1" ->615 {616 attached: Set(),617 built: false,618 expecting: false,619 running: false,620 session: true,621 up: true622 },623 "w2" ->624 {625 attached: Set(),626 built: false,627 expecting: false,628 running: false,629 session: true,630 up: true631 }632 )633}634635[State 16]636{637 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),638 schedFixed::scheduler::crashes: 2,639 schedFixed::scheduler::entry:640 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],641 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),642 schedFixed::scheduler::mAssigned: Set(),643 schedFixed::scheduler::mBuild: Set(("c2", "w2")),644 schedFixed::scheduler::mDone: Set(),645 schedFixed::scheduler::mExpect: Set("w2"),646 schedFixed::scheduler::mResult: Set(),647 schedFixed::scheduler::mRetry: Set(),648 schedFixed::scheduler::mRevoke: Set(),649 schedFixed::scheduler::mSchedule: Set("c1"),650 schedFixed::scheduler::published: 0,651 schedFixed::scheduler::publishedBy: Set(),652 schedFixed::scheduler::ws:653 Map(654 "w1" ->655 {656 attached: Set(),657 built: false,658 expecting: false,659 running: false,660 session: true,661 up: true662 },663 "w2" ->664 {665 attached: Set(),666 built: false,667 expecting: false,668 running: false,669 session: true,670 up: true671 }672 )673}674675[State 17]676{677 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),678 schedFixed::scheduler::crashes: 2,679 schedFixed::scheduler::entry:680 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],681 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),682 schedFixed::scheduler::mAssigned: Set(),683 schedFixed::scheduler::mBuild: Set(),684 schedFixed::scheduler::mDone: Set(),685 schedFixed::scheduler::mExpect: Set("w2"),686 schedFixed::scheduler::mResult: Set(),687 schedFixed::scheduler::mRetry: Set("c2"),688 schedFixed::scheduler::mRevoke: Set(),689 schedFixed::scheduler::mSchedule: Set("c1"),690 schedFixed::scheduler::published: 0,691 schedFixed::scheduler::publishedBy: Set(),692 schedFixed::scheduler::ws:693 Map(694 "w1" ->695 {696 attached: Set(),697 built: false,698 expecting: false,699 running: false,700 session: true,701 up: true702 },703 "w2" ->704 {705 attached: Set(),706 built: false,707 expecting: false,708 running: false,709 session: true,710 up: true711 }712 )713}714715[State 18]716{717 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),718 schedFixed::scheduler::crashes: 2,719 schedFixed::scheduler::entry:720 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],721 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),722 schedFixed::scheduler::mAssigned: Set(),723 schedFixed::scheduler::mBuild: Set(),724 schedFixed::scheduler::mDone: Set(),725 schedFixed::scheduler::mExpect: Set("w2"),726 schedFixed::scheduler::mResult: Set(),727 schedFixed::scheduler::mRetry: Set(),728 schedFixed::scheduler::mRevoke: Set(),729 schedFixed::scheduler::mSchedule: Set("c1", "c2"),730 schedFixed::scheduler::published: 0,731 schedFixed::scheduler::publishedBy: Set(),732 schedFixed::scheduler::ws:733 Map(734 "w1" ->735 {736 attached: Set(),737 built: false,738 expecting: false,739 running: false,740 session: true,741 up: true742 },743 "w2" ->744 {745 attached: Set(),746 built: false,747 expecting: false,748 running: false,749 session: true,750 up: true751 }752 )753}754755[State 19]756{757 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),758 schedFixed::scheduler::crashes: 2,759 schedFixed::scheduler::entry:760 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],761 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),762 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),763 schedFixed::scheduler::mBuild: Set(),764 schedFixed::scheduler::mDone: Set(),765 schedFixed::scheduler::mExpect: Set("w2"),766 schedFixed::scheduler::mResult: Set(),767 schedFixed::scheduler::mRetry: Set(),768 schedFixed::scheduler::mRevoke: Set(),769 schedFixed::scheduler::mSchedule: Set("c1"),770 schedFixed::scheduler::published: 0,771 schedFixed::scheduler::publishedBy: Set(),772 schedFixed::scheduler::ws:773 Map(774 "w1" ->775 {776 attached: Set(),777 built: false,778 expecting: false,779 running: false,780 session: true,781 up: true782 },783 "w2" ->784 {785 attached: Set(),786 built: false,787 expecting: false,788 running: false,789 session: true,790 up: true791 }792 )793}794795[State 20]796{797 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),798 schedFixed::scheduler::crashes: 2,799 schedFixed::scheduler::entry:800 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],801 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),802 schedFixed::scheduler::mAssigned: Set(),803 schedFixed::scheduler::mBuild: Set(("c2", "w2")),804 schedFixed::scheduler::mDone: Set(),805 schedFixed::scheduler::mExpect: Set("w2"),806 schedFixed::scheduler::mResult: Set(),807 schedFixed::scheduler::mRetry: Set(),808 schedFixed::scheduler::mRevoke: Set(),809 schedFixed::scheduler::mSchedule: Set("c1"),810 schedFixed::scheduler::published: 0,811 schedFixed::scheduler::publishedBy: Set(),812 schedFixed::scheduler::ws:813 Map(814 "w1" ->815 {816 attached: Set(),817 built: false,818 expecting: false,819 running: false,820 session: true,821 up: true822 },823 "w2" ->824 {825 attached: Set(),826 built: false,827 expecting: false,828 running: false,829 session: true,830 up: true831 }832 )833}834835[State 21]836{837 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),838 schedFixed::scheduler::crashes: 2,839 schedFixed::scheduler::entry:840 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],841 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),842 schedFixed::scheduler::mAssigned: Set(),843 schedFixed::scheduler::mBuild: Set(),844 schedFixed::scheduler::mDone: Set(),845 schedFixed::scheduler::mExpect: Set("w2"),846 schedFixed::scheduler::mResult: Set(),847 schedFixed::scheduler::mRetry: Set("c2"),848 schedFixed::scheduler::mRevoke: Set(),849 schedFixed::scheduler::mSchedule: Set("c1"),850 schedFixed::scheduler::published: 0,851 schedFixed::scheduler::publishedBy: Set(),852 schedFixed::scheduler::ws:853 Map(854 "w1" ->855 {856 attached: Set(),857 built: false,858 expecting: false,859 running: false,860 session: true,861 up: true862 },863 "w2" ->864 {865 attached: Set(),866 built: false,867 expecting: false,868 running: false,869 session: true,870 up: true871 }872 )873}874875[State 22]876{877 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),878 schedFixed::scheduler::crashes: 2,879 schedFixed::scheduler::entry:880 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],881 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),882 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),883 schedFixed::scheduler::mBuild: Set(),884 schedFixed::scheduler::mDone: Set(),885 schedFixed::scheduler::mExpect: Set("w2"),886 schedFixed::scheduler::mResult: Set(),887 schedFixed::scheduler::mRetry: Set("c2"),888 schedFixed::scheduler::mRevoke: Set(),889 schedFixed::scheduler::mSchedule: Set(),890 schedFixed::scheduler::published: 0,891 schedFixed::scheduler::publishedBy: Set(),892 schedFixed::scheduler::ws:893 Map(894 "w1" ->895 {896 attached: Set(),897 built: false,898 expecting: false,899 running: false,900 session: true,901 up: true902 },903 "w2" ->904 {905 attached: Set(),906 built: false,907 expecting: false,908 running: false,909 session: true,910 up: true911 }912 )913}914915[State 23]916{917 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),918 schedFixed::scheduler::crashes: 2,919 schedFixed::scheduler::entry:920 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],921 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),922 schedFixed::scheduler::mAssigned: Set(),923 schedFixed::scheduler::mBuild: Set(("c1", "w2")),924 schedFixed::scheduler::mDone: Set(),925 schedFixed::scheduler::mExpect: Set("w2"),926 schedFixed::scheduler::mResult: Set(),927 schedFixed::scheduler::mRetry: Set("c2"),928 schedFixed::scheduler::mRevoke: Set(),929 schedFixed::scheduler::mSchedule: Set(),930 schedFixed::scheduler::published: 0,931 schedFixed::scheduler::publishedBy: Set(),932 schedFixed::scheduler::ws:933 Map(934 "w1" ->935 {936 attached: Set(),937 built: false,938 expecting: false,939 running: false,940 session: true,941 up: true942 },943 "w2" ->944 {945 attached: Set(),946 built: false,947 expecting: false,948 running: false,949 session: true,950 up: true951 }952 )953}954955[State 24]956{957 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),958 schedFixed::scheduler::crashes: 2,959 schedFixed::scheduler::entry:960 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],961 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),962 schedFixed::scheduler::mAssigned: Set(),963 schedFixed::scheduler::mBuild: Set(("c1", "w2")),964 schedFixed::scheduler::mDone: Set(),965 schedFixed::scheduler::mExpect: Set("w2"),966 schedFixed::scheduler::mResult: Set(),967 schedFixed::scheduler::mRetry: Set(),968 schedFixed::scheduler::mRevoke: Set(),969 schedFixed::scheduler::mSchedule: Set("c2"),970 schedFixed::scheduler::published: 0,971 schedFixed::scheduler::publishedBy: Set(),972 schedFixed::scheduler::ws:973 Map(974 "w1" ->975 {976 attached: Set(),977 built: false,978 expecting: false,979 running: false,980 session: true,981 up: true982 },983 "w2" ->984 {985 attached: Set(),986 built: false,987 expecting: false,988 running: false,989 session: true,990 up: true991 }992 )993}994995[State 25]996{997 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),998 schedFixed::scheduler::crashes: 2,999 schedFixed::scheduler::entry:1000 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1001 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1002 schedFixed::scheduler::mAssigned: Set(),1003 schedFixed::scheduler::mBuild: Set(),1004 schedFixed::scheduler::mDone: Set(),1005 schedFixed::scheduler::mExpect: Set("w2"),1006 schedFixed::scheduler::mResult: Set(),1007 schedFixed::scheduler::mRetry: Set("c1"),1008 schedFixed::scheduler::mRevoke: Set(),1009 schedFixed::scheduler::mSchedule: Set("c2"),1010 schedFixed::scheduler::published: 0,1011 schedFixed::scheduler::publishedBy: Set(),1012 schedFixed::scheduler::ws:1013 Map(1014 "w1" ->1015 {1016 attached: Set(),1017 built: false,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" -> CQueued, "c2" -> CQueued),1038 schedFixed::scheduler::crashes: 2,1039 schedFixed::scheduler::entry:1040 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1041 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1042 schedFixed::scheduler::mAssigned: Set(),1043 schedFixed::scheduler::mBuild: Set(),1044 schedFixed::scheduler::mDone: Set(),1045 schedFixed::scheduler::mExpect: Set("w2"),1046 schedFixed::scheduler::mResult: Set(),1047 schedFixed::scheduler::mRetry: Set(),1048 schedFixed::scheduler::mRevoke: Set(),1049 schedFixed::scheduler::mSchedule: Set("c1", "c2"),1050 schedFixed::scheduler::published: 0,1051 schedFixed::scheduler::publishedBy: Set(),1052 schedFixed::scheduler::ws:1053 Map(1054 "w1" ->1055 {1056 attached: Set(),1057 built: false,1058 expecting: false,1059 running: false,1060 session: true,1061 up: true1062 },1063 "w2" ->1064 {1065 attached: Set(),1066 built: false,1067 expecting: false,1068 running: false,1069 session: true,1070 up: true1071 }1072 )1073}10741075[State 27]1076{1077 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1078 schedFixed::scheduler::crashes: 2,1079 schedFixed::scheduler::entry:1080 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1081 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1082 schedFixed::scheduler::mAssigned: Set(),1083 schedFixed::scheduler::mBuild: Set(),1084 schedFixed::scheduler::mDone: Set(),1085 schedFixed::scheduler::mExpect: Set(),1086 schedFixed::scheduler::mResult: Set(),1087 schedFixed::scheduler::mRetry: Set(),1088 schedFixed::scheduler::mRevoke: Set(),1089 schedFixed::scheduler::mSchedule: Set("c1", "c2"),1090 schedFixed::scheduler::published: 0,1091 schedFixed::scheduler::publishedBy: Set(),1092 schedFixed::scheduler::ws:1093 Map(1094 "w1" ->1095 {1096 attached: Set(),1097 built: false,1098 expecting: false,1099 running: false,1100 session: true,1101 up: true1102 },1103 "w2" ->1104 {1105 attached: Set(),1106 built: false,1107 expecting: true,1108 running: true,1109 session: true,1110 up: true1111 }1112 )1113}11141115[State 28]1116{1117 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1118 schedFixed::scheduler::crashes: 2,1119 schedFixed::scheduler::entry:1120 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1121 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1122 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1123 schedFixed::scheduler::mBuild: Set(),1124 schedFixed::scheduler::mDone: Set(),1125 schedFixed::scheduler::mExpect: Set(),1126 schedFixed::scheduler::mResult: Set(),1127 schedFixed::scheduler::mRetry: Set(),1128 schedFixed::scheduler::mRevoke: Set(),1129 schedFixed::scheduler::mSchedule: Set("c1"),1130 schedFixed::scheduler::published: 0,1131 schedFixed::scheduler::publishedBy: Set(),1132 schedFixed::scheduler::ws:1133 Map(1134 "w1" ->1135 {1136 attached: Set(),1137 built: false,1138 expecting: false,1139 running: false,1140 session: true,1141 up: true1142 },1143 "w2" ->1144 {1145 attached: Set(),1146 built: false,1147 expecting: true,1148 running: true,1149 session: true,1150 up: true1151 }1152 )1153}11541155[State 29]1156{1157 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1158 schedFixed::scheduler::crashes: 2,1159 schedFixed::scheduler::entry:1160 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1161 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1162 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1163 schedFixed::scheduler::mBuild: Set(),1164 schedFixed::scheduler::mDone: Set("w2"),1165 schedFixed::scheduler::mExpect: Set(),1166 schedFixed::scheduler::mResult: Set(),1167 schedFixed::scheduler::mRetry: Set(),1168 schedFixed::scheduler::mRevoke: Set(),1169 schedFixed::scheduler::mSchedule: Set("c1"),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" -> CQueued, "c2" -> CQueued),1198 schedFixed::scheduler::crashes: 2,1199 schedFixed::scheduler::entry: [],1200 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1201 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1202 schedFixed::scheduler::mBuild: Set(),1203 schedFixed::scheduler::mDone: Set(),1204 schedFixed::scheduler::mExpect: Set(),1205 schedFixed::scheduler::mResult: Set(),1206 schedFixed::scheduler::mRetry: Set(),1207 schedFixed::scheduler::mRevoke: Set(),1208 schedFixed::scheduler::mSchedule: Set("c1"),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 (2657ms at 11291 traces/second).1235Trace length statistics: max=30, min=15, average=18.581236You may increase --max-samples and --max-steps.1237Use --verbosity to produce more (or less) output.1238Use --seed=0x95e64994fdca37a4 --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" -> CQueued, "c2" -> CIdle),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("c1"),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" -> CQueued, "c2" -> CIdle),1322 schedNoRevoke::scheduler::crashes: 1,1323 schedNoRevoke::scheduler::entry: [],1324 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1325 schedNoRevoke::scheduler::mAssigned: Set(),1326 schedNoRevoke::scheduler::mBuild: Set(),1327 schedNoRevoke::scheduler::mDone: Set(),1328 schedNoRevoke::scheduler::mExpect: Set(),1329 schedNoRevoke::scheduler::mResult: Set(),1330 schedNoRevoke::scheduler::mRetry: Set(),1331 schedNoRevoke::scheduler::mRevoke: Set(),1332 schedNoRevoke::scheduler::mSchedule: Set("c1"),1333 schedNoRevoke::scheduler::published: 0,1334 schedNoRevoke::scheduler::publishedBy: Set(),1335 schedNoRevoke::scheduler::ws:1336 Map(1337 "w1" ->1338 {1339 attached: Set(),1340 built: false,1341 expecting: false,1342 running: false,1343 session: true,1344 up: true1345 },1346 "w2" ->1347 {1348 attached: Set(),1349 built: false,1350 expecting: false,1351 running: false,1352 session: false,1353 up: false1354 }1355 )1356}13571358[State 3]1359{1360 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1361 schedNoRevoke::scheduler::crashes: 1,1362 schedNoRevoke::scheduler::entry:1363 [{ followers: Set("c1"), leased: true, worker: "w1" }],1364 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1365 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1366 schedNoRevoke::scheduler::mBuild: Set(),1367 schedNoRevoke::scheduler::mDone: Set(),1368 schedNoRevoke::scheduler::mExpect: Set("w1"),1369 schedNoRevoke::scheduler::mResult: Set(),1370 schedNoRevoke::scheduler::mRetry: Set(),1371 schedNoRevoke::scheduler::mRevoke: Set(),1372 schedNoRevoke::scheduler::mSchedule: Set(),1373 schedNoRevoke::scheduler::published: 0,1374 schedNoRevoke::scheduler::publishedBy: Set(),1375 schedNoRevoke::scheduler::ws:1376 Map(1377 "w1" ->1378 {1379 attached: Set(),1380 built: false,1381 expecting: false,1382 running: false,1383 session: true,1384 up: true1385 },1386 "w2" ->1387 {1388 attached: Set(),1389 built: false,1390 expecting: false,1391 running: false,1392 session: false,1393 up: false1394 }1395 )1396}13971398[State 4]1399{1400 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1401 schedNoRevoke::scheduler::crashes: 1,1402 schedNoRevoke::scheduler::entry:1403 [{ followers: Set("c1"), leased: true, worker: "w1" }],1404 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1405 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1406 schedNoRevoke::scheduler::mBuild: Set(),1407 schedNoRevoke::scheduler::mDone: Set(),1408 schedNoRevoke::scheduler::mExpect: Set(),1409 schedNoRevoke::scheduler::mResult: Set(),1410 schedNoRevoke::scheduler::mRetry: Set(),1411 schedNoRevoke::scheduler::mRevoke: Set(),1412 schedNoRevoke::scheduler::mSchedule: Set(),1413 schedNoRevoke::scheduler::published: 0,1414 schedNoRevoke::scheduler::publishedBy: Set(),1415 schedNoRevoke::scheduler::ws:1416 Map(1417 "w1" ->1418 {1419 attached: Set(),1420 built: false,1421 expecting: true,1422 running: true,1423 session: true,1424 up: true1425 },1426 "w2" ->1427 {1428 attached: Set(),1429 built: false,1430 expecting: false,1431 running: false,1432 session: false,1433 up: false1434 }1435 )1436}14371438[State 5]1439{1440 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1441 schedNoRevoke::scheduler::crashes: 2,1442 schedNoRevoke::scheduler::entry: [],1443 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1444 schedNoRevoke::scheduler::mAssigned: Set(),1445 schedNoRevoke::scheduler::mBuild: Set(),1446 schedNoRevoke::scheduler::mDone: Set(),1447 schedNoRevoke::scheduler::mExpect: Set(),1448 schedNoRevoke::scheduler::mResult: Set(),1449 schedNoRevoke::scheduler::mRetry: Set("c1"),1450 schedNoRevoke::scheduler::mRevoke: Set(),1451 schedNoRevoke::scheduler::mSchedule: Set(),1452 schedNoRevoke::scheduler::published: 0,1453 schedNoRevoke::scheduler::publishedBy: Set(),1454 schedNoRevoke::scheduler::ws:1455 Map(1456 "w1" ->1457 {1458 attached: Set(),1459 built: false,1460 expecting: true,1461 running: true,1462 session: false,1463 up: true1464 },1465 "w2" ->1466 {1467 attached: Set(),1468 built: false,1469 expecting: false,1470 running: false,1471 session: false,1472 up: false1473 }1474 )1475}14761477[State 6]1478{1479 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1480 schedNoRevoke::scheduler::crashes: 2,1481 schedNoRevoke::scheduler::entry: [],1482 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1483 schedNoRevoke::scheduler::mAssigned: Set(),1484 schedNoRevoke::scheduler::mBuild: Set(),1485 schedNoRevoke::scheduler::mDone: Set(),1486 schedNoRevoke::scheduler::mExpect: Set(),1487 schedNoRevoke::scheduler::mResult: Set(),1488 schedNoRevoke::scheduler::mRetry: Set("c1"),1489 schedNoRevoke::scheduler::mRevoke: Set(),1490 schedNoRevoke::scheduler::mSchedule: Set(),1491 schedNoRevoke::scheduler::published: 0,1492 schedNoRevoke::scheduler::publishedBy: Set(),1493 schedNoRevoke::scheduler::ws:1494 Map(1495 "w1" ->1496 {1497 attached: Set(),1498 built: false,1499 expecting: true,1500 running: true,1501 session: false,1502 up: true1503 },1504 "w2" ->1505 {1506 attached: Set(),1507 built: false,1508 expecting: false,1509 running: false,1510 session: true,1511 up: true1512 }1513 )1514}15151516[State 7]1517{1518 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1519 schedNoRevoke::scheduler::crashes: 2,1520 schedNoRevoke::scheduler::entry: [],1521 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1522 schedNoRevoke::scheduler::mAssigned: Set(),1523 schedNoRevoke::scheduler::mBuild: Set(),1524 schedNoRevoke::scheduler::mDone: Set(),1525 schedNoRevoke::scheduler::mExpect: Set(),1526 schedNoRevoke::scheduler::mResult: Set(),1527 schedNoRevoke::scheduler::mRetry: Set(),1528 schedNoRevoke::scheduler::mRevoke: Set(),1529 schedNoRevoke::scheduler::mSchedule: Set("c1"),1530 schedNoRevoke::scheduler::published: 0,1531 schedNoRevoke::scheduler::publishedBy: Set(),1532 schedNoRevoke::scheduler::ws:1533 Map(1534 "w1" ->1535 {1536 attached: Set(),1537 built: false,1538 expecting: true,1539 running: true,1540 session: false,1541 up: true1542 },1543 "w2" ->1544 {1545 attached: Set(),1546 built: false,1547 expecting: false,1548 running: false,1549 session: true,1550 up: true1551 }1552 )1553}15541555[State 8]1556{1557 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1558 schedNoRevoke::scheduler::crashes: 2,1559 schedNoRevoke::scheduler::entry:1560 [{ followers: Set("c1"), leased: true, worker: "w2" }],1561 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1562 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1563 schedNoRevoke::scheduler::mBuild: Set(),1564 schedNoRevoke::scheduler::mDone: Set(),1565 schedNoRevoke::scheduler::mExpect: Set("w2"),1566 schedNoRevoke::scheduler::mResult: Set(),1567 schedNoRevoke::scheduler::mRetry: Set(),1568 schedNoRevoke::scheduler::mRevoke: Set(),1569 schedNoRevoke::scheduler::mSchedule: Set(),1570 schedNoRevoke::scheduler::published: 0,1571 schedNoRevoke::scheduler::publishedBy: Set(),1572 schedNoRevoke::scheduler::ws:1573 Map(1574 "w1" ->1575 {1576 attached: Set(),1577 built: false,1578 expecting: true,1579 running: true,1580 session: false,1581 up: true1582 },1583 "w2" ->1584 {1585 attached: Set(),1586 built: false,1587 expecting: false,1588 running: false,1589 session: true,1590 up: true1591 }1592 )1593}15941595[State 9]1596{1597 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1598 schedNoRevoke::scheduler::crashes: 2,1599 schedNoRevoke::scheduler::entry:1600 [{ followers: Set("c1"), leased: true, worker: "w2" }],1601 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1602 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1603 schedNoRevoke::scheduler::mBuild: Set(),1604 schedNoRevoke::scheduler::mDone: Set(),1605 schedNoRevoke::scheduler::mExpect: Set(),1606 schedNoRevoke::scheduler::mResult: Set(),1607 schedNoRevoke::scheduler::mRetry: Set(),1608 schedNoRevoke::scheduler::mRevoke: Set(),1609 schedNoRevoke::scheduler::mSchedule: Set(),1610 schedNoRevoke::scheduler::published: 0,1611 schedNoRevoke::scheduler::publishedBy: Set(),1612 schedNoRevoke::scheduler::ws:1613 Map(1614 "w1" ->1615 {1616 attached: Set(),1617 built: false,1618 expecting: true,1619 running: true,1620 session: false,1621 up: true1622 },1623 "w2" ->1624 {1625 attached: Set(),1626 built: false,1627 expecting: true,1628 running: true,1629 session: true,1630 up: true1631 }1632 )1633}16341635[State 10]1636{1637 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1638 schedNoRevoke::scheduler::crashes: 2,1639 schedNoRevoke::scheduler::entry:1640 [{ followers: Set("c1"), leased: true, worker: "w2" }],1641 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1642 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1643 schedNoRevoke::scheduler::mBuild: Set(),1644 schedNoRevoke::scheduler::mDone: Set(),1645 schedNoRevoke::scheduler::mExpect: Set(),1646 schedNoRevoke::scheduler::mResult: Set(),1647 schedNoRevoke::scheduler::mRetry: Set(),1648 schedNoRevoke::scheduler::mRevoke: Set(),1649 schedNoRevoke::scheduler::mSchedule: Set(),1650 schedNoRevoke::scheduler::published: 0,1651 schedNoRevoke::scheduler::publishedBy: Set(),1652 schedNoRevoke::scheduler::ws:1653 Map(1654 "w1" ->1655 {1656 attached: Set(),1657 built: false,1658 expecting: true,1659 running: true,1660 session: true,1661 up: true1662 },1663 "w2" ->1664 {1665 attached: Set(),1666 built: false,1667 expecting: true,1668 running: true,1669 session: true,1670 up: true1671 }1672 )1673}16741675[violation] Found an issue (5262ms at 5296 traces/second).1676Use --verbosity=3 to show executions.1677Use --seed=0xaa69b67aa8291c1 --backend=rust to reproduce.1678error: Invariant violated1679An example execution:16801681[State 0]1682{1683 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1684 schedNoFence::scheduler::crashes: 0,1685 schedNoFence::scheduler::entry: [],1686 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1687 schedNoFence::scheduler::mAssigned: Set(),1688 schedNoFence::scheduler::mBuild: Set(),1689 schedNoFence::scheduler::mDone: Set(),1690 schedNoFence::scheduler::mExpect: Set(),1691 schedNoFence::scheduler::mResult: Set(),1692 schedNoFence::scheduler::mRetry: Set(),1693 schedNoFence::scheduler::mRevoke: Set(),1694 schedNoFence::scheduler::mSchedule: Set(),1695 schedNoFence::scheduler::published: 0,1696 schedNoFence::scheduler::publishedBy: Set(),1697 schedNoFence::scheduler::ws:1698 Map(1699 "w1" ->1700 {1701 attached: Set(),1702 built: false,1703 expecting: false,1704 running: false,1705 session: true,1706 up: true1707 },1708 "w2" ->1709 {1710 attached: Set(),1711 built: false,1712 expecting: false,1713 running: false,1714 session: true,1715 up: true1716 }1717 )1718}17191720[State 1]1721{1722 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1723 schedNoFence::scheduler::crashes: 1,1724 schedNoFence::scheduler::entry: [],1725 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1726 schedNoFence::scheduler::mAssigned: Set(),1727 schedNoFence::scheduler::mBuild: Set(),1728 schedNoFence::scheduler::mDone: Set(),1729 schedNoFence::scheduler::mExpect: Set(),1730 schedNoFence::scheduler::mResult: Set(),1731 schedNoFence::scheduler::mRetry: Set(),1732 schedNoFence::scheduler::mRevoke: Set(),1733 schedNoFence::scheduler::mSchedule: Set(),1734 schedNoFence::scheduler::published: 0,1735 schedNoFence::scheduler::publishedBy: Set(),1736 schedNoFence::scheduler::ws:1737 Map(1738 "w1" ->1739 {1740 attached: Set(),1741 built: false,1742 expecting: false,1743 running: false,1744 session: false,1745 up: false1746 },1747 "w2" ->1748 {1749 attached: Set(),1750 built: false,1751 expecting: false,1752 running: false,1753 session: true,1754 up: true1755 }1756 )1757}17581759[State 2]1760{1761 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1762 schedNoFence::scheduler::crashes: 1,1763 schedNoFence::scheduler::entry: [],1764 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1765 schedNoFence::scheduler::mAssigned: Set(),1766 schedNoFence::scheduler::mBuild: Set(),1767 schedNoFence::scheduler::mDone: Set(),1768 schedNoFence::scheduler::mExpect: Set(),1769 schedNoFence::scheduler::mResult: Set(),1770 schedNoFence::scheduler::mRetry: Set(),1771 schedNoFence::scheduler::mRevoke: Set(),1772 schedNoFence::scheduler::mSchedule: Set("c2"),1773 schedNoFence::scheduler::published: 0,1774 schedNoFence::scheduler::publishedBy: Set(),1775 schedNoFence::scheduler::ws:1776 Map(1777 "w1" ->1778 {1779 attached: Set(),1780 built: false,1781 expecting: false,1782 running: false,1783 session: false,1784 up: false1785 },1786 "w2" ->1787 {1788 attached: Set(),1789 built: false,1790 expecting: false,1791 running: false,1792 session: true,1793 up: true1794 }1795 )1796}17971798[State 3]1799{1800 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1801 schedNoFence::scheduler::crashes: 1,1802 schedNoFence::scheduler::entry:1803 [{ followers: Set("c2"), leased: true, worker: "w2" }],1804 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1805 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1806 schedNoFence::scheduler::mBuild: Set(),1807 schedNoFence::scheduler::mDone: Set(),1808 schedNoFence::scheduler::mExpect: Set("w2"),1809 schedNoFence::scheduler::mResult: Set(),1810 schedNoFence::scheduler::mRetry: Set(),1811 schedNoFence::scheduler::mRevoke: Set(),1812 schedNoFence::scheduler::mSchedule: Set(),1813 schedNoFence::scheduler::published: 0,1814 schedNoFence::scheduler::publishedBy: Set(),1815 schedNoFence::scheduler::ws:1816 Map(1817 "w1" ->1818 {1819 attached: Set(),1820 built: false,1821 expecting: false,1822 running: false,1823 session: false,1824 up: false1825 },1826 "w2" ->1827 {1828 attached: Set(),1829 built: false,1830 expecting: false,1831 running: false,1832 session: true,1833 up: true1834 }1835 )1836}18371838[State 4]1839{1840 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1841 schedNoFence::scheduler::crashes: 1,1842 schedNoFence::scheduler::entry:1843 [{ followers: Set("c2"), leased: true, worker: "w2" }],1844 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1845 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1846 schedNoFence::scheduler::mBuild: Set(),1847 schedNoFence::scheduler::mDone: Set(),1848 schedNoFence::scheduler::mExpect: Set(),1849 schedNoFence::scheduler::mResult: Set(),1850 schedNoFence::scheduler::mRetry: Set(),1851 schedNoFence::scheduler::mRevoke: Set(),1852 schedNoFence::scheduler::mSchedule: Set(),1853 schedNoFence::scheduler::published: 0,1854 schedNoFence::scheduler::publishedBy: Set(),1855 schedNoFence::scheduler::ws:1856 Map(1857 "w1" ->1858 {1859 attached: Set(),1860 built: false,1861 expecting: false,1862 running: false,1863 session: false,1864 up: false1865 },1866 "w2" ->1867 {1868 attached: Set(),1869 built: false,1870 expecting: true,1871 running: true,1872 session: true,1873 up: true1874 }1875 )1876}18771878[State 5]1879{1880 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1881 schedNoFence::scheduler::crashes: 2,1882 schedNoFence::scheduler::entry: [],1883 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1884 schedNoFence::scheduler::mAssigned: Set(),1885 schedNoFence::scheduler::mBuild: Set(),1886 schedNoFence::scheduler::mDone: Set(),1887 schedNoFence::scheduler::mExpect: Set(),1888 schedNoFence::scheduler::mResult: Set(),1889 schedNoFence::scheduler::mRetry: Set("c2"),1890 schedNoFence::scheduler::mRevoke: Set(),1891 schedNoFence::scheduler::mSchedule: Set(),1892 schedNoFence::scheduler::published: 0,1893 schedNoFence::scheduler::publishedBy: Set(),1894 schedNoFence::scheduler::ws:1895 Map(1896 "w1" ->1897 {1898 attached: Set(),1899 built: false,1900 expecting: false,1901 running: false,1902 session: false,1903 up: false1904 },1905 "w2" ->1906 {1907 attached: Set(),1908 built: false,1909 expecting: true,1910 running: true,1911 session: false,1912 up: true1913 }1914 )1915}19161917[State 6]1918{1919 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1920 schedNoFence::scheduler::crashes: 2,1921 schedNoFence::scheduler::entry: [],1922 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1923 schedNoFence::scheduler::mAssigned: Set(),1924 schedNoFence::scheduler::mBuild: Set(),1925 schedNoFence::scheduler::mDone: Set(),1926 schedNoFence::scheduler::mExpect: Set(),1927 schedNoFence::scheduler::mResult: Set(),1928 schedNoFence::scheduler::mRetry: Set("c2"),1929 schedNoFence::scheduler::mRevoke: Set(),1930 schedNoFence::scheduler::mSchedule: Set("c1"),1931 schedNoFence::scheduler::published: 0,1932 schedNoFence::scheduler::publishedBy: Set(),1933 schedNoFence::scheduler::ws:1934 Map(1935 "w1" ->1936 {1937 attached: Set(),1938 built: false,1939 expecting: false,1940 running: false,1941 session: false,1942 up: false1943 },1944 "w2" ->1945 {1946 attached: Set(),1947 built: false,1948 expecting: true,1949 running: true,1950 session: false,1951 up: true1952 }1953 )1954}19551956[State 7]1957{1958 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1959 schedNoFence::scheduler::crashes: 2,1960 schedNoFence::scheduler::entry: [],1961 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1962 schedNoFence::scheduler::mAssigned: Set(),1963 schedNoFence::scheduler::mBuild: Set(),1964 schedNoFence::scheduler::mDone: Set(),1965 schedNoFence::scheduler::mExpect: Set(),1966 schedNoFence::scheduler::mResult: Set(),1967 schedNoFence::scheduler::mRetry: Set("c2"),1968 schedNoFence::scheduler::mRevoke: Set(),1969 schedNoFence::scheduler::mSchedule: Set("c1"),1970 schedNoFence::scheduler::published: 0,1971 schedNoFence::scheduler::publishedBy: Set(),1972 schedNoFence::scheduler::ws:1973 Map(1974 "w1" ->1975 {1976 attached: Set(),1977 built: false,1978 expecting: false,1979 running: false,1980 session: true,1981 up: true1982 },1983 "w2" ->1984 {1985 attached: Set(),1986 built: false,1987 expecting: true,1988 running: true,1989 session: false,1990 up: true1991 }1992 )1993}19941995[State 8]1996{1997 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1998 schedNoFence::scheduler::crashes: 2,1999 schedNoFence::scheduler::entry:2000 [{ followers: Set("c1"), leased: true, worker: "w1" }],2001 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2002 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2003 schedNoFence::scheduler::mBuild: Set(),2004 schedNoFence::scheduler::mDone: Set(),2005 schedNoFence::scheduler::mExpect: Set("w1"),2006 schedNoFence::scheduler::mResult: Set(),2007 schedNoFence::scheduler::mRetry: Set("c2"),2008 schedNoFence::scheduler::mRevoke: Set(),2009 schedNoFence::scheduler::mSchedule: Set(),2010 schedNoFence::scheduler::published: 0,2011 schedNoFence::scheduler::publishedBy: Set(),2012 schedNoFence::scheduler::ws:2013 Map(2014 "w1" ->2015 {2016 attached: Set(),2017 built: false,2018 expecting: false,2019 running: false,2020 session: true,2021 up: true2022 },2023 "w2" ->2024 {2025 attached: Set(),2026 built: false,2027 expecting: true,2028 running: true,2029 session: false,2030 up: true2031 }2032 )2033}20342035[State 9]2036{2037 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2038 schedNoFence::scheduler::crashes: 2,2039 schedNoFence::scheduler::entry:2040 [{ followers: Set("c1"), leased: true, worker: "w1" }],2041 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2042 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2043 schedNoFence::scheduler::mBuild: Set(),2044 schedNoFence::scheduler::mDone: Set(),2045 schedNoFence::scheduler::mExpect: Set("w1"),2046 schedNoFence::scheduler::mResult: Set(),2047 schedNoFence::scheduler::mRetry: Set("c2"),2048 schedNoFence::scheduler::mRevoke: Set(),2049 schedNoFence::scheduler::mSchedule: Set(),2050 schedNoFence::scheduler::published: 1,2051 schedNoFence::scheduler::publishedBy: Set("w2"),2052 schedNoFence::scheduler::ws:2053 Map(2054 "w1" ->2055 {2056 attached: Set(),2057 built: false,2058 expecting: false,2059 running: false,2060 session: true,2061 up: true2062 },2063 "w2" ->2064 {2065 attached: Set(),2066 built: true,2067 expecting: false,2068 running: false,2069 session: false,2070 up: true2071 }2072 )2073}20742075[State 10]2076{2077 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2078 schedNoFence::scheduler::crashes: 2,2079 schedNoFence::scheduler::entry:2080 [{ followers: Set("c1"), leased: true, worker: "w1" }],2081 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2082 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2083 schedNoFence::scheduler::mBuild: Set(),2084 schedNoFence::scheduler::mDone: Set(),2085 schedNoFence::scheduler::mExpect: Set("w1"),2086 schedNoFence::scheduler::mResult: Set(),2087 schedNoFence::scheduler::mRetry: Set(),2088 schedNoFence::scheduler::mRevoke: Set(),2089 schedNoFence::scheduler::mSchedule: Set("c2"),2090 schedNoFence::scheduler::published: 1,2091 schedNoFence::scheduler::publishedBy: Set("w2"),2092 schedNoFence::scheduler::ws:2093 Map(2094 "w1" ->2095 {2096 attached: Set(),2097 built: false,2098 expecting: false,2099 running: false,2100 session: true,2101 up: true2102 },2103 "w2" ->2104 {2105 attached: Set(),2106 built: true,2107 expecting: false,2108 running: false,2109 session: false,2110 up: true2111 }2112 )2113}21142115[State 11]2116{2117 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2118 schedNoFence::scheduler::crashes: 2,2119 schedNoFence::scheduler::entry:2120 [{ followers: Set("c1"), leased: true, worker: "w1" }],2121 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2122 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2123 schedNoFence::scheduler::mBuild: Set(),2124 schedNoFence::scheduler::mDone: Set(),2125 schedNoFence::scheduler::mExpect: Set(),2126 schedNoFence::scheduler::mResult: Set(),2127 schedNoFence::scheduler::mRetry: Set(),2128 schedNoFence::scheduler::mRevoke: Set(),2129 schedNoFence::scheduler::mSchedule: Set("c2"),2130 schedNoFence::scheduler::published: 1,2131 schedNoFence::scheduler::publishedBy: Set("w2"),2132 schedNoFence::scheduler::ws:2133 Map(2134 "w1" ->2135 {2136 attached: Set(),2137 built: false,2138 expecting: true,2139 running: true,2140 session: true,2141 up: true2142 },2143 "w2" ->2144 {2145 attached: Set(),2146 built: true,2147 expecting: false,2148 running: false,2149 session: false,2150 up: true2151 }2152 )2153}21542155[State 12]2156{2157 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2158 schedNoFence::scheduler::crashes: 2,2159 schedNoFence::scheduler::entry:2160 [{ followers: Set("c1"), leased: true, worker: "w1" }],2161 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2162 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2163 schedNoFence::scheduler::mBuild: Set(),2164 schedNoFence::scheduler::mDone: Set("w1"),2165 schedNoFence::scheduler::mExpect: Set(),2166 schedNoFence::scheduler::mResult: Set(),2167 schedNoFence::scheduler::mRetry: Set(),2168 schedNoFence::scheduler::mRevoke: Set(),2169 schedNoFence::scheduler::mSchedule: Set("c2"),2170 schedNoFence::scheduler::published: 2,2171 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2172 schedNoFence::scheduler::ws:2173 Map(2174 "w1" ->2175 {2176 attached: Set(),2177 built: true,2178 expecting: false,2179 running: false,2180 session: true,2181 up: true2182 },2183 "w2" ->2184 {2185 attached: Set(),2186 built: true,2187 expecting: false,2188 running: false,2189 session: false,2190 up: true2191 }2192 )2193}21942195[violation] Found an issue (3054ms at 8491 traces/second).2196Use --verbosity=3 to show executions.2197Use --seed=0x44272350b1022780 --backend=rust to reproduce.2198error: Invariant violated2199An example execution:22002201[State 0]2202{2203 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2204 schedNoPush::scheduler::crashes: 0,2205 schedNoPush::scheduler::entry: [],2206 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2207 schedNoPush::scheduler::mAssigned: Set(),2208 schedNoPush::scheduler::mBuild: Set(),2209 schedNoPush::scheduler::mDone: Set(),2210 schedNoPush::scheduler::mExpect: Set(),2211 schedNoPush::scheduler::mResult: Set(),2212 schedNoPush::scheduler::mRetry: Set(),2213 schedNoPush::scheduler::mRevoke: Set(),2214 schedNoPush::scheduler::mSchedule: Set(),2215 schedNoPush::scheduler::published: 0,2216 schedNoPush::scheduler::publishedBy: Set(),2217 schedNoPush::scheduler::ws:2218 Map(2219 "w1" ->2220 {2221 attached: Set(),2222 built: false,2223 expecting: false,2224 running: false,2225 session: true,2226 up: true2227 },2228 "w2" ->2229 {2230 attached: Set(),2231 built: false,2232 expecting: false,2233 running: false,2234 session: true,2235 up: true2236 }2237 )2238}22392240[State 1]2241{2242 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2243 schedNoPush::scheduler::crashes: 0,2244 schedNoPush::scheduler::entry: [],2245 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2246 schedNoPush::scheduler::mAssigned: Set(),2247 schedNoPush::scheduler::mBuild: Set(),2248 schedNoPush::scheduler::mDone: Set(),2249 schedNoPush::scheduler::mExpect: Set(),2250 schedNoPush::scheduler::mResult: Set(),2251 schedNoPush::scheduler::mRetry: Set(),2252 schedNoPush::scheduler::mRevoke: Set(),2253 schedNoPush::scheduler::mSchedule: Set("c1"),2254 schedNoPush::scheduler::published: 0,2255 schedNoPush::scheduler::publishedBy: Set(),2256 schedNoPush::scheduler::ws:2257 Map(2258 "w1" ->2259 {2260 attached: Set(),2261 built: false,2262 expecting: false,2263 running: false,2264 session: true,2265 up: true2266 },2267 "w2" ->2268 {2269 attached: Set(),2270 built: false,2271 expecting: false,2272 running: false,2273 session: true,2274 up: true2275 }2276 )2277}22782279[State 2]2280{2281 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2282 schedNoPush::scheduler::crashes: 1,2283 schedNoPush::scheduler::entry: [],2284 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2285 schedNoPush::scheduler::mAssigned: Set(),2286 schedNoPush::scheduler::mBuild: Set(),2287 schedNoPush::scheduler::mDone: Set(),2288 schedNoPush::scheduler::mExpect: Set(),2289 schedNoPush::scheduler::mResult: Set(),2290 schedNoPush::scheduler::mRetry: Set(),2291 schedNoPush::scheduler::mRevoke: Set(),2292 schedNoPush::scheduler::mSchedule: Set("c1"),2293 schedNoPush::scheduler::published: 0,2294 schedNoPush::scheduler::publishedBy: Set(),2295 schedNoPush::scheduler::ws:2296 Map(2297 "w1" ->2298 {2299 attached: Set(),2300 built: false,2301 expecting: false,2302 running: false,2303 session: false,2304 up: false2305 },2306 "w2" ->2307 {2308 attached: Set(),2309 built: false,2310 expecting: false,2311 running: false,2312 session: true,2313 up: true2314 }2315 )2316}23172318[State 3]2319{2320 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2321 schedNoPush::scheduler::crashes: 1,2322 schedNoPush::scheduler::entry:2323 [{ followers: Set("c1"), leased: true, worker: "w2" }],2324 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2325 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2326 schedNoPush::scheduler::mBuild: Set(),2327 schedNoPush::scheduler::mDone: Set(),2328 schedNoPush::scheduler::mExpect: Set(),2329 schedNoPush::scheduler::mResult: Set(),2330 schedNoPush::scheduler::mRetry: Set(),2331 schedNoPush::scheduler::mRevoke: Set(),2332 schedNoPush::scheduler::mSchedule: Set(),2333 schedNoPush::scheduler::published: 0,2334 schedNoPush::scheduler::publishedBy: Set(),2335 schedNoPush::scheduler::ws:2336 Map(2337 "w1" ->2338 {2339 attached: Set(),2340 built: false,2341 expecting: false,2342 running: false,2343 session: false,2344 up: false2345 },2346 "w2" ->2347 {2348 attached: Set(),2349 built: false,2350 expecting: false,2351 running: false,2352 session: true,2353 up: true2354 }2355 )2356}23572358[State 4]2359{2360 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2361 schedNoPush::scheduler::crashes: 2,2362 schedNoPush::scheduler::entry:2363 [{ followers: Set("c1"), leased: true, worker: "w2" }],2364 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2365 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2366 schedNoPush::scheduler::mBuild: Set(),2367 schedNoPush::scheduler::mDone: Set(),2368 schedNoPush::scheduler::mExpect: Set(),2369 schedNoPush::scheduler::mResult: Set(),2370 schedNoPush::scheduler::mRetry: Set(),2371 schedNoPush::scheduler::mRevoke: Set(),2372 schedNoPush::scheduler::mSchedule: Set(),2373 schedNoPush::scheduler::published: 0,2374 schedNoPush::scheduler::publishedBy: Set(),2375 schedNoPush::scheduler::ws:2376 Map(2377 "w1" ->2378 {2379 attached: Set(),2380 built: false,2381 expecting: false,2382 running: false,2383 session: false,2384 up: false2385 },2386 "w2" ->2387 {2388 attached: Set(),2389 built: false,2390 expecting: false,2391 running: false,2392 session: false,2393 up: false2394 }2395 )2396}23972398[State 5]2399{2400 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2401 schedNoPush::scheduler::crashes: 2,2402 schedNoPush::scheduler::entry: [],2403 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2404 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2405 schedNoPush::scheduler::mBuild: Set(),2406 schedNoPush::scheduler::mDone: Set(),2407 schedNoPush::scheduler::mExpect: Set(),2408 schedNoPush::scheduler::mResult: Set(),2409 schedNoPush::scheduler::mRetry: Set("c1"),2410 schedNoPush::scheduler::mRevoke: Set(),2411 schedNoPush::scheduler::mSchedule: Set(),2412 schedNoPush::scheduler::published: 0,2413 schedNoPush::scheduler::publishedBy: Set(),2414 schedNoPush::scheduler::ws:2415 Map(2416 "w1" ->2417 {2418 attached: Set(),2419 built: false,2420 expecting: false,2421 running: false,2422 session: false,2423 up: false2424 },2425 "w2" ->2426 {2427 attached: Set(),2428 built: false,2429 expecting: false,2430 running: false,2431 session: true,2432 up: true2433 }2434 )2435}24362437[State 6]2438{2439 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2440 schedNoPush::scheduler::crashes: 2,2441 schedNoPush::scheduler::entry: [],2442 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2443 schedNoPush::scheduler::mAssigned: Set(),2444 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2445 schedNoPush::scheduler::mDone: Set(),2446 schedNoPush::scheduler::mExpect: Set(),2447 schedNoPush::scheduler::mResult: Set(),2448 schedNoPush::scheduler::mRetry: Set("c1"),2449 schedNoPush::scheduler::mRevoke: Set(),2450 schedNoPush::scheduler::mSchedule: Set(),2451 schedNoPush::scheduler::published: 0,2452 schedNoPush::scheduler::publishedBy: Set(),2453 schedNoPush::scheduler::ws:2454 Map(2455 "w1" ->2456 {2457 attached: Set(),2458 built: false,2459 expecting: false,2460 running: false,2461 session: false,2462 up: false2463 },2464 "w2" ->2465 {2466 attached: Set(),2467 built: false,2468 expecting: false,2469 running: false,2470 session: true,2471 up: true2472 }2473 )2474}24752476[State 7]2477{2478 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2479 schedNoPush::scheduler::crashes: 2,2480 schedNoPush::scheduler::entry: [],2481 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2482 schedNoPush::scheduler::mAssigned: Set(),2483 schedNoPush::scheduler::mBuild: Set(),2484 schedNoPush::scheduler::mDone: Set(),2485 schedNoPush::scheduler::mExpect: Set(),2486 schedNoPush::scheduler::mResult: Set(),2487 schedNoPush::scheduler::mRetry: Set("c1"),2488 schedNoPush::scheduler::mRevoke: Set(),2489 schedNoPush::scheduler::mSchedule: Set(),2490 schedNoPush::scheduler::published: 0,2491 schedNoPush::scheduler::publishedBy: Set(),2492 schedNoPush::scheduler::ws:2493 Map(2494 "w1" ->2495 {2496 attached: Set(),2497 built: false,2498 expecting: false,2499 running: false,2500 session: false,2501 up: false2502 },2503 "w2" ->2504 {2505 attached: Set("c1"),2506 built: false,2507 expecting: true,2508 running: true,2509 session: true,2510 up: true2511 }2512 )2513}25142515[violation] Found an issue (4281ms at 2772 traces/second).2516Use --verbosity=3 to show executions.2517Use --seed=0x2806bbe8df4a39f9 --backend=rust to reproduce.2518error: Invariant violated2519An example execution:25202521[State 0]2522{2523 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2524 schedNoReport::scheduler::crashes: 0,2525 schedNoReport::scheduler::entry: [],2526 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2527 schedNoReport::scheduler::mAssigned: Set(),2528 schedNoReport::scheduler::mBuild: Set(),2529 schedNoReport::scheduler::mDone: Set(),2530 schedNoReport::scheduler::mExpect: Set(),2531 schedNoReport::scheduler::mResult: Set(),2532 schedNoReport::scheduler::mRetry: Set(),2533 schedNoReport::scheduler::mRevoke: Set(),2534 schedNoReport::scheduler::mSchedule: Set(),2535 schedNoReport::scheduler::published: 0,2536 schedNoReport::scheduler::publishedBy: Set(),2537 schedNoReport::scheduler::ws:2538 Map(2539 "w1" ->2540 {2541 attached: Set(),2542 built: false,2543 expecting: false,2544 running: false,2545 session: true,2546 up: true2547 },2548 "w2" ->2549 {2550 attached: Set(),2551 built: false,2552 expecting: false,2553 running: false,2554 session: true,2555 up: true2556 }2557 )2558}25592560[State 1]2561{2562 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2563 schedNoReport::scheduler::crashes: 0,2564 schedNoReport::scheduler::entry: [],2565 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2566 schedNoReport::scheduler::mAssigned: Set(),2567 schedNoReport::scheduler::mBuild: Set(),2568 schedNoReport::scheduler::mDone: Set(),2569 schedNoReport::scheduler::mExpect: Set(),2570 schedNoReport::scheduler::mResult: Set(),2571 schedNoReport::scheduler::mRetry: Set(),2572 schedNoReport::scheduler::mRevoke: Set(),2573 schedNoReport::scheduler::mSchedule: Set("c2"),2574 schedNoReport::scheduler::published: 0,2575 schedNoReport::scheduler::publishedBy: Set(),2576 schedNoReport::scheduler::ws:2577 Map(2578 "w1" ->2579 {2580 attached: Set(),2581 built: false,2582 expecting: false,2583 running: false,2584 session: true,2585 up: true2586 },2587 "w2" ->2588 {2589 attached: Set(),2590 built: false,2591 expecting: false,2592 running: false,2593 session: true,2594 up: true2595 }2596 )2597}25982599[State 2]2600{2601 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2602 schedNoReport::scheduler::crashes: 1,2603 schedNoReport::scheduler::entry: [],2604 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2605 schedNoReport::scheduler::mAssigned: Set(),2606 schedNoReport::scheduler::mBuild: Set(),2607 schedNoReport::scheduler::mDone: Set(),2608 schedNoReport::scheduler::mExpect: Set(),2609 schedNoReport::scheduler::mResult: Set(),2610 schedNoReport::scheduler::mRetry: Set(),2611 schedNoReport::scheduler::mRevoke: Set(),2612 schedNoReport::scheduler::mSchedule: Set("c2"),2613 schedNoReport::scheduler::published: 0,2614 schedNoReport::scheduler::publishedBy: Set(),2615 schedNoReport::scheduler::ws:2616 Map(2617 "w1" ->2618 {2619 attached: Set(),2620 built: false,2621 expecting: false,2622 running: false,2623 session: false,2624 up: false2625 },2626 "w2" ->2627 {2628 attached: Set(),2629 built: false,2630 expecting: false,2631 running: false,2632 session: true,2633 up: true2634 }2635 )2636}26372638[State 3]2639{2640 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2641 schedNoReport::scheduler::crashes: 1,2642 schedNoReport::scheduler::entry:2643 [{ followers: Set("c2"), leased: true, worker: "w2" }],2644 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2645 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2646 schedNoReport::scheduler::mBuild: Set(),2647 schedNoReport::scheduler::mDone: Set(),2648 schedNoReport::scheduler::mExpect: Set("w2"),2649 schedNoReport::scheduler::mResult: Set(),2650 schedNoReport::scheduler::mRetry: Set(),2651 schedNoReport::scheduler::mRevoke: Set(),2652 schedNoReport::scheduler::mSchedule: Set(),2653 schedNoReport::scheduler::published: 0,2654 schedNoReport::scheduler::publishedBy: Set(),2655 schedNoReport::scheduler::ws:2656 Map(2657 "w1" ->2658 {2659 attached: Set(),2660 built: false,2661 expecting: false,2662 running: false,2663 session: false,2664 up: false2665 },2666 "w2" ->2667 {2668 attached: Set(),2669 built: false,2670 expecting: false,2671 running: false,2672 session: true,2673 up: true2674 }2675 )2676}26772678[State 4]2679{2680 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2681 schedNoReport::scheduler::crashes: 1,2682 schedNoReport::scheduler::entry:2683 [{ followers: Set("c2"), leased: true, worker: "w2" }],2684 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2685 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2686 schedNoReport::scheduler::mBuild: Set(),2687 schedNoReport::scheduler::mDone: Set(),2688 schedNoReport::scheduler::mExpect: Set(),2689 schedNoReport::scheduler::mResult: Set(),2690 schedNoReport::scheduler::mRetry: Set(),2691 schedNoReport::scheduler::mRevoke: Set(),2692 schedNoReport::scheduler::mSchedule: Set(),2693 schedNoReport::scheduler::published: 0,2694 schedNoReport::scheduler::publishedBy: Set(),2695 schedNoReport::scheduler::ws:2696 Map(2697 "w1" ->2698 {2699 attached: Set(),2700 built: false,2701 expecting: false,2702 running: false,2703 session: false,2704 up: false2705 },2706 "w2" ->2707 {2708 attached: Set(),2709 built: false,2710 expecting: true,2711 running: true,2712 session: true,2713 up: true2714 }2715 )2716}27172718[State 5]2719{2720 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2721 schedNoReport::scheduler::crashes: 2,2722 schedNoReport::scheduler::entry: [],2723 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2724 schedNoReport::scheduler::mAssigned: Set(),2725 schedNoReport::scheduler::mBuild: Set(),2726 schedNoReport::scheduler::mDone: Set(),2727 schedNoReport::scheduler::mExpect: Set(),2728 schedNoReport::scheduler::mResult: Set(),2729 schedNoReport::scheduler::mRetry: Set("c2"),2730 schedNoReport::scheduler::mRevoke: Set(),2731 schedNoReport::scheduler::mSchedule: Set(),2732 schedNoReport::scheduler::published: 0,2733 schedNoReport::scheduler::publishedBy: Set(),2734 schedNoReport::scheduler::ws:2735 Map(2736 "w1" ->2737 {2738 attached: Set(),2739 built: false,2740 expecting: false,2741 running: false,2742 session: false,2743 up: false2744 },2745 "w2" ->2746 {2747 attached: Set(),2748 built: false,2749 expecting: true,2750 running: true,2751 session: false,2752 up: true2753 }2754 )2755}27562757[State 6]2758{2759 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2760 schedNoReport::scheduler::crashes: 2,2761 schedNoReport::scheduler::entry: [],2762 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2763 schedNoReport::scheduler::mAssigned: Set(),2764 schedNoReport::scheduler::mBuild: Set(),2765 schedNoReport::scheduler::mDone: Set(),2766 schedNoReport::scheduler::mExpect: Set(),2767 schedNoReport::scheduler::mResult: Set(),2768 schedNoReport::scheduler::mRetry: Set("c2"),2769 schedNoReport::scheduler::mRevoke: Set(),2770 schedNoReport::scheduler::mSchedule: Set(),2771 schedNoReport::scheduler::published: 0,2772 schedNoReport::scheduler::publishedBy: Set(),2773 schedNoReport::scheduler::ws:2774 Map(2775 "w1" ->2776 {2777 attached: Set(),2778 built: false,2779 expecting: false,2780 running: false,2781 session: true,2782 up: true2783 },2784 "w2" ->2785 {2786 attached: Set(),2787 built: false,2788 expecting: true,2789 running: true,2790 session: false,2791 up: true2792 }2793 )2794}27952796[State 7]2797{2798 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2799 schedNoReport::scheduler::crashes: 2,2800 schedNoReport::scheduler::entry: [],2801 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2802 schedNoReport::scheduler::mAssigned: Set(),2803 schedNoReport::scheduler::mBuild: Set(),2804 schedNoReport::scheduler::mDone: Set(),2805 schedNoReport::scheduler::mExpect: Set(),2806 schedNoReport::scheduler::mResult: Set(),2807 schedNoReport::scheduler::mRetry: Set(),2808 schedNoReport::scheduler::mRevoke: Set(),2809 schedNoReport::scheduler::mSchedule: Set("c2"),2810 schedNoReport::scheduler::published: 0,2811 schedNoReport::scheduler::publishedBy: Set(),2812 schedNoReport::scheduler::ws:2813 Map(2814 "w1" ->2815 {2816 attached: Set(),2817 built: false,2818 expecting: false,2819 running: false,2820 session: true,2821 up: true2822 },2823 "w2" ->2824 {2825 attached: Set(),2826 built: false,2827 expecting: true,2828 running: true,2829 session: false,2830 up: true2831 }2832 )2833}28342835[State 8]2836{2837 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2838 schedNoReport::scheduler::crashes: 2,2839 schedNoReport::scheduler::entry:2840 [{ followers: Set("c2"), leased: true, worker: "w1" }],2841 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2842 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2843 schedNoReport::scheduler::mBuild: Set(),2844 schedNoReport::scheduler::mDone: Set(),2845 schedNoReport::scheduler::mExpect: Set("w1"),2846 schedNoReport::scheduler::mResult: Set(),2847 schedNoReport::scheduler::mRetry: Set(),2848 schedNoReport::scheduler::mRevoke: Set(),2849 schedNoReport::scheduler::mSchedule: Set(),2850 schedNoReport::scheduler::published: 0,2851 schedNoReport::scheduler::publishedBy: Set(),2852 schedNoReport::scheduler::ws:2853 Map(2854 "w1" ->2855 {2856 attached: Set(),2857 built: false,2858 expecting: false,2859 running: false,2860 session: true,2861 up: true2862 },2863 "w2" ->2864 {2865 attached: Set(),2866 built: false,2867 expecting: true,2868 running: true,2869 session: false,2870 up: true2871 }2872 )2873}28742875[State 9]2876{2877 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2878 schedNoReport::scheduler::crashes: 2,2879 schedNoReport::scheduler::entry:2880 [{ followers: Set("c2"), leased: true, worker: "w1" }],2881 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2882 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2883 schedNoReport::scheduler::mBuild: Set(),2884 schedNoReport::scheduler::mDone: Set(),2885 schedNoReport::scheduler::mExpect: Set("w1"),2886 schedNoReport::scheduler::mResult: Set(),2887 schedNoReport::scheduler::mRetry: Set(),2888 schedNoReport::scheduler::mRevoke: Set(),2889 schedNoReport::scheduler::mSchedule: Set(),2890 schedNoReport::scheduler::published: 0,2891 schedNoReport::scheduler::publishedBy: Set(),2892 schedNoReport::scheduler::ws:2893 Map(2894 "w1" ->2895 {2896 attached: Set(),2897 built: false,2898 expecting: false,2899 running: false,2900 session: true,2901 up: true2902 },2903 "w2" ->2904 {2905 attached: Set(),2906 built: false,2907 expecting: true,2908 running: true,2909 session: true,2910 up: true2911 }2912 )2913}29142915[State 10]2916{2917 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2918 schedNoReport::scheduler::crashes: 2,2919 schedNoReport::scheduler::entry:2920 [{ followers: Set("c2"), leased: true, worker: "w1" }],2921 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2922 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2923 schedNoReport::scheduler::mBuild: Set(),2924 schedNoReport::scheduler::mDone: Set(),2925 schedNoReport::scheduler::mExpect: Set(),2926 schedNoReport::scheduler::mResult: Set(),2927 schedNoReport::scheduler::mRetry: Set(),2928 schedNoReport::scheduler::mRevoke: Set(),2929 schedNoReport::scheduler::mSchedule: Set(),2930 schedNoReport::scheduler::published: 0,2931 schedNoReport::scheduler::publishedBy: Set(),2932 schedNoReport::scheduler::ws:2933 Map(2934 "w1" ->2935 {2936 attached: Set(),2937 built: false,2938 expecting: true,2939 running: true,2940 session: true,2941 up: true2942 },2943 "w2" ->2944 {2945 attached: Set(),2946 built: false,2947 expecting: true,2948 running: true,2949 session: true,2950 up: true2951 }2952 )2953}29542955[violation] Found an issue (9489ms at 2486 traces/second).2956Use --verbosity=3 to show executions.2957Use --seed=0xe7d00fce5b9a2b71 --backend=rust to reproduce.2958error: Invariant violated2959An example execution:29602961[State 0]2962{2963 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2964 schedTerminal::scheduler::crashes: 0,2965 schedTerminal::scheduler::entry: [],2966 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2967 schedTerminal::scheduler::mAssigned: Set(),2968 schedTerminal::scheduler::mBuild: Set(),2969 schedTerminal::scheduler::mDone: Set(),2970 schedTerminal::scheduler::mExpect: Set(),2971 schedTerminal::scheduler::mResult: Set(),2972 schedTerminal::scheduler::mRetry: Set(),2973 schedTerminal::scheduler::mRevoke: Set(),2974 schedTerminal::scheduler::mSchedule: Set(),2975 schedTerminal::scheduler::published: 0,2976 schedTerminal::scheduler::publishedBy: Set(),2977 schedTerminal::scheduler::ws:2978 Map(2979 "w1" ->2980 {2981 attached: Set(),2982 built: false,2983 expecting: false,2984 running: false,2985 session: true,2986 up: true2987 },2988 "w2" ->2989 {2990 attached: Set(),2991 built: false,2992 expecting: false,2993 running: false,2994 session: true,2995 up: true2996 }2997 )2998}29993000[State 1]3001{3002 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3003 schedTerminal::scheduler::crashes: 1,3004 schedTerminal::scheduler::entry: [],3005 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3006 schedTerminal::scheduler::mAssigned: Set(),3007 schedTerminal::scheduler::mBuild: Set(),3008 schedTerminal::scheduler::mDone: Set(),3009 schedTerminal::scheduler::mExpect: Set(),3010 schedTerminal::scheduler::mResult: Set(),3011 schedTerminal::scheduler::mRetry: Set(),3012 schedTerminal::scheduler::mRevoke: Set(),3013 schedTerminal::scheduler::mSchedule: Set(),3014 schedTerminal::scheduler::published: 0,3015 schedTerminal::scheduler::publishedBy: Set(),3016 schedTerminal::scheduler::ws:3017 Map(3018 "w1" ->3019 {3020 attached: Set(),3021 built: false,3022 expecting: false,3023 running: false,3024 session: false,3025 up: true3026 },3027 "w2" ->3028 {3029 attached: Set(),3030 built: false,3031 expecting: false,3032 running: false,3033 session: false,3034 up: true3035 }3036 )3037}30383039[State 2]3040{3041 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3042 schedTerminal::scheduler::crashes: 1,3043 schedTerminal::scheduler::entry: [],3044 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3045 schedTerminal::scheduler::mAssigned: Set(),3046 schedTerminal::scheduler::mBuild: Set(),3047 schedTerminal::scheduler::mDone: Set(),3048 schedTerminal::scheduler::mExpect: Set(),3049 schedTerminal::scheduler::mResult: Set(),3050 schedTerminal::scheduler::mRetry: Set(),3051 schedTerminal::scheduler::mRevoke: Set(),3052 schedTerminal::scheduler::mSchedule: Set("c2"),3053 schedTerminal::scheduler::published: 0,3054 schedTerminal::scheduler::publishedBy: Set(),3055 schedTerminal::scheduler::ws:3056 Map(3057 "w1" ->3058 {3059 attached: Set(),3060 built: false,3061 expecting: false,3062 running: false,3063 session: false,3064 up: true3065 },3066 "w2" ->3067 {3068 attached: Set(),3069 built: false,3070 expecting: false,3071 running: false,3072 session: false,3073 up: true3074 }3075 )3076}30773078[State 3]3079{3080 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3081 schedTerminal::scheduler::crashes: 1,3082 schedTerminal::scheduler::entry: [],3083 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3084 schedTerminal::scheduler::mAssigned: Set(),3085 schedTerminal::scheduler::mBuild: Set(),3086 schedTerminal::scheduler::mDone: Set(),3087 schedTerminal::scheduler::mExpect: Set(),3088 schedTerminal::scheduler::mResult: Set(),3089 schedTerminal::scheduler::mRetry: Set(),3090 schedTerminal::scheduler::mRevoke: Set(),3091 schedTerminal::scheduler::mSchedule: Set(),3092 schedTerminal::scheduler::published: 0,3093 schedTerminal::scheduler::publishedBy: Set(),3094 schedTerminal::scheduler::ws:3095 Map(3096 "w1" ->3097 {3098 attached: Set(),3099 built: false,3100 expecting: false,3101 running: false,3102 session: false,3103 up: true3104 },3105 "w2" ->3106 {3107 attached: Set(),3108 built: false,3109 expecting: false,3110 running: false,3111 session: false,3112 up: true3113 }3114 )3115}31163117[violation] Found an issue (4028ms at 246 traces/second).3118Use --verbosity=3 to show executions.3119Use --seed=0x4416ab67947c9770 --backend=rust to reproduce.3120error: Invariant violated3121An example execution:31223123[State 0]3124{3125 pushFixed::push::byPath: Map(),3126 pushFixed::push::inflight: Set(),3127 pushFixed::push::left: Map(),3128 pushFixed::push::sent: Map()3129}31303131[State 1]3132{3133 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3134 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3135 pushFixed::push::left: Map(1 -> 2),3136 pushFixed::push::sent: Map(1 -> Set("a", "b"))3137}31383139[State 2]3140{3141 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3142 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (3, "a"), (3, "b")),3143 pushFixed::push::left: Map(1 -> 2, 3 -> 2),3144 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3145}31463147[State 3]3148{3149 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3150 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (3, "a")),3151 pushFixed::push::left: Map(1 -> 2, 3 -> 1),3152 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3153}31543155[State 4]3156{3157 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3158 pushFixed::push::inflight: Set((1, "a"), (3, "a")),3159 pushFixed::push::left: Map(1 -> 1, 3 -> 1),3160 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3161}31623163[State 5]3164{3165 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3166 pushFixed::push::inflight: Set((1, "a")),3167 pushFixed::push::left: Map(1 -> 1, 3 -> 0),3168 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3169}31703171[State 6]3172{3173 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3174 pushFixed::push::inflight: Set((1, "a"), (2, "a"), (2, "b")),3175 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 0),3176 pushFixed::push::sent:3177 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3178}31793180[State 7]3181{3182 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3183 pushFixed::push::inflight: Set((1, "a"), (2, "a")),3184 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 0),3185 pushFixed::push::sent:3186 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3187}31883189[State 8]3190{3191 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3192 pushFixed::push::inflight: Set((2, "a")),3193 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 0),3194 pushFixed::push::sent:3195 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3196}31973198[State 9]3199{3200 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3201 pushFixed::push::inflight: Set(),3202 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3203 pushFixed::push::sent:3204 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3205}32063207[ok] No violation found (694ms at 28818 traces/second).3208Trace length statistics: max=10, min=7, average=7.893209You may increase --max-samples and --max-steps.3210Use --verbosity to produce more (or less) output.3211Use --seed=0x29b4878db0bdca11 --backend=rust to reproduce.