nix-grpc-store-spec
checks.aarch64-linux.spec
· build #468
· 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("c1"),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" -> CIdle),124 schedFixed::scheduler::crashes: 1,125 schedFixed::scheduler::entry: [],126 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),127 schedFixed::scheduler::mAssigned: Set(),128 schedFixed::scheduler::mBuild: Set(),129 schedFixed::scheduler::mDone: Set(),130 schedFixed::scheduler::mExpect: Set(),131 schedFixed::scheduler::mResult: Set(),132 schedFixed::scheduler::mRetry: Set("c1"),133 schedFixed::scheduler::mRevoke: Set(),134 schedFixed::scheduler::mSchedule: Set(),135 schedFixed::scheduler::published: 0,136 schedFixed::scheduler::publishedBy: Set(),137 schedFixed::scheduler::ws:138 Map(139 "w1" ->140 {141 attached: Set(),142 built: false,143 expecting: false,144 running: false,145 session: false,146 up: true147 },148 "w2" ->149 {150 attached: Set(),151 built: false,152 expecting: false,153 running: false,154 session: true,155 up: true156 }157 )158}159160[State 4]161{162 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),163 schedFixed::scheduler::crashes: 2,164 schedFixed::scheduler::entry: [],165 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),166 schedFixed::scheduler::mAssigned: Set(),167 schedFixed::scheduler::mBuild: Set(),168 schedFixed::scheduler::mDone: Set(),169 schedFixed::scheduler::mExpect: Set(),170 schedFixed::scheduler::mResult: Set(),171 schedFixed::scheduler::mRetry: Set("c1"),172 schedFixed::scheduler::mRevoke: Set(),173 schedFixed::scheduler::mSchedule: Set(),174 schedFixed::scheduler::published: 0,175 schedFixed::scheduler::publishedBy: Set(),176 schedFixed::scheduler::ws:177 Map(178 "w1" ->179 {180 attached: Set(),181 built: false,182 expecting: false,183 running: false,184 session: false,185 up: true186 },187 "w2" ->188 {189 attached: Set(),190 built: false,191 expecting: false,192 running: false,193 session: false,194 up: false195 }196 )197}198199[State 5]200{201 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),202 schedFixed::scheduler::crashes: 2,203 schedFixed::scheduler::entry: [],204 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),205 schedFixed::scheduler::mAssigned: Set(),206 schedFixed::scheduler::mBuild: Set(),207 schedFixed::scheduler::mDone: Set(),208 schedFixed::scheduler::mExpect: Set(),209 schedFixed::scheduler::mResult: Set(),210 schedFixed::scheduler::mRetry: Set(),211 schedFixed::scheduler::mRevoke: Set(),212 schedFixed::scheduler::mSchedule: Set("c1"),213 schedFixed::scheduler::published: 0,214 schedFixed::scheduler::publishedBy: Set(),215 schedFixed::scheduler::ws:216 Map(217 "w1" ->218 {219 attached: Set(),220 built: false,221 expecting: false,222 running: false,223 session: false,224 up: true225 },226 "w2" ->227 {228 attached: Set(),229 built: false,230 expecting: false,231 running: false,232 session: false,233 up: false234 }235 )236}237238[State 6]239{240 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),241 schedFixed::scheduler::crashes: 2,242 schedFixed::scheduler::entry: [],243 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),244 schedFixed::scheduler::mAssigned: Set(),245 schedFixed::scheduler::mBuild: Set(),246 schedFixed::scheduler::mDone: Set(),247 schedFixed::scheduler::mExpect: Set(),248 schedFixed::scheduler::mResult: Set(),249 schedFixed::scheduler::mRetry: Set(),250 schedFixed::scheduler::mRevoke: Set(),251 schedFixed::scheduler::mSchedule: Set("c1"),252 schedFixed::scheduler::published: 0,253 schedFixed::scheduler::publishedBy: Set(),254 schedFixed::scheduler::ws:255 Map(256 "w1" ->257 {258 attached: Set(),259 built: false,260 expecting: false,261 running: false,262 session: false,263 up: true264 },265 "w2" ->266 {267 attached: Set(),268 built: false,269 expecting: false,270 running: false,271 session: true,272 up: true273 }274 )275}276277[State 7]278{279 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),280 schedFixed::scheduler::crashes: 2,281 schedFixed::scheduler::entry: [],282 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),283 schedFixed::scheduler::mAssigned: Set(),284 schedFixed::scheduler::mBuild: Set(),285 schedFixed::scheduler::mDone: Set(),286 schedFixed::scheduler::mExpect: Set(),287 schedFixed::scheduler::mResult: Set(),288 schedFixed::scheduler::mRetry: Set(),289 schedFixed::scheduler::mRevoke: Set(),290 schedFixed::scheduler::mSchedule: Set("c1"),291 schedFixed::scheduler::published: 0,292 schedFixed::scheduler::publishedBy: Set(),293 schedFixed::scheduler::ws:294 Map(295 "w1" ->296 {297 attached: Set(),298 built: false,299 expecting: false,300 running: false,301 session: true,302 up: true303 },304 "w2" ->305 {306 attached: Set(),307 built: false,308 expecting: false,309 running: false,310 session: true,311 up: true312 }313 )314}315316[State 8]317{318 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),319 schedFixed::scheduler::crashes: 2,320 schedFixed::scheduler::entry: [],321 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),322 schedFixed::scheduler::mAssigned: Set(),323 schedFixed::scheduler::mBuild: Set(),324 schedFixed::scheduler::mDone: Set(),325 schedFixed::scheduler::mExpect: Set(),326 schedFixed::scheduler::mResult: Set(),327 schedFixed::scheduler::mRetry: Set(),328 schedFixed::scheduler::mRevoke: Set(),329 schedFixed::scheduler::mSchedule: Set("c1", "c2"),330 schedFixed::scheduler::published: 0,331 schedFixed::scheduler::publishedBy: Set(),332 schedFixed::scheduler::ws:333 Map(334 "w1" ->335 {336 attached: Set(),337 built: false,338 expecting: false,339 running: false,340 session: true,341 up: true342 },343 "w2" ->344 {345 attached: Set(),346 built: false,347 expecting: false,348 running: false,349 session: true,350 up: true351 }352 )353}354355[State 9]356{357 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),358 schedFixed::scheduler::crashes: 2,359 schedFixed::scheduler::entry:360 [{ followers: Set("c1"), leased: true, worker: "w2" }],361 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),362 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),363 schedFixed::scheduler::mBuild: Set(),364 schedFixed::scheduler::mDone: Set(),365 schedFixed::scheduler::mExpect: Set("w2"),366 schedFixed::scheduler::mResult: Set(),367 schedFixed::scheduler::mRetry: Set(),368 schedFixed::scheduler::mRevoke: Set(),369 schedFixed::scheduler::mSchedule: Set("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: true,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" -> CSent("w2"), "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(),403 schedFixed::scheduler::mBuild: Set(("c1", "w2")),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: true,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(),444 schedFixed::scheduler::mDone: Set(),445 schedFixed::scheduler::mExpect: Set("w2"),446 schedFixed::scheduler::mResult: Set(),447 schedFixed::scheduler::mRetry: Set("c1"),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: true,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" -> CQueued, "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(),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("c1", "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" -> CQueued, "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(("c1", "w2")),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(),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", "c2"), leased: true, worker: "w2" }],561 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),562 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),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(),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" -> CSent("w2")),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(("c1", "w2")),603 schedFixed::scheduler::mBuild: Set(("c2", "w2")),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(),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(("c1", "w2")),643 schedFixed::scheduler::mBuild: Set(),644 schedFixed::scheduler::mDone: Set(),645 schedFixed::scheduler::mExpect: Set("w2"),646 schedFixed::scheduler::mResult: Set(),647 schedFixed::scheduler::mRetry: Set("c2"),648 schedFixed::scheduler::mRevoke: Set(),649 schedFixed::scheduler::mSchedule: Set(),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" -> CQueued),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(("c1", "w2")),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(),688 schedFixed::scheduler::mRevoke: Set(),689 schedFixed::scheduler::mSchedule: Set("c2"),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(("c1", "w2"), ("c2", "w2")),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(),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" -> CSent("w2"), "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(("c1", "w2")),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(),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" -> CSent("w2"), "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(("c1", "w2"), ("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(),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" -> CSent("w2"), "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(("c2", "w2")),844 schedFixed::scheduler::mDone: Set(),845 schedFixed::scheduler::mExpect: Set("w2"),846 schedFixed::scheduler::mResult: Set(),847 schedFixed::scheduler::mRetry: Set("c1"),848 schedFixed::scheduler::mRevoke: Set(),849 schedFixed::scheduler::mSchedule: Set(),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(),883 schedFixed::scheduler::mBuild: Set(("c2", "w2")),884 schedFixed::scheduler::mDone: Set(),885 schedFixed::scheduler::mExpect: Set("w2"),886 schedFixed::scheduler::mResult: Set(),887 schedFixed::scheduler::mRetry: Set(),888 schedFixed::scheduler::mRevoke: Set(),889 schedFixed::scheduler::mSchedule: Set("c1"),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" -> CQueued, "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(("c2", "w2")),924 schedFixed::scheduler::mDone: Set(),925 schedFixed::scheduler::mExpect: Set(),926 schedFixed::scheduler::mResult: Set(),927 schedFixed::scheduler::mRetry: Set(),928 schedFixed::scheduler::mRevoke: Set(),929 schedFixed::scheduler::mSchedule: Set("c1"),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: true,948 running: true,949 session: true,950 up: true951 }952 )953}954955[State 24]956{957 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),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(),964 schedFixed::scheduler::mDone: Set(),965 schedFixed::scheduler::mExpect: Set(),966 schedFixed::scheduler::mResult: Set(),967 schedFixed::scheduler::mRetry: Set(),968 schedFixed::scheduler::mRevoke: Set(),969 schedFixed::scheduler::mSchedule: Set("c1"),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("c2"),986 built: false,987 expecting: true,988 running: true,989 session: true,990 up: true991 }992 )993}994995[State 25]996{997 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),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(("c1", "w2")),1003 schedFixed::scheduler::mBuild: Set(),1004 schedFixed::scheduler::mDone: Set(),1005 schedFixed::scheduler::mExpect: Set(),1006 schedFixed::scheduler::mResult: Set(),1007 schedFixed::scheduler::mRetry: Set(),1008 schedFixed::scheduler::mRevoke: Set(),1009 schedFixed::scheduler::mSchedule: Set(),1010 schedFixed::scheduler::published: 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("c2"),1026 built: false,1027 expecting: true,1028 running: true,1029 session: true,1030 up: true1031 }1032 )1033}10341035[State 26]1036{1037 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),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(("c1", "w2")),1043 schedFixed::scheduler::mBuild: Set(),1044 schedFixed::scheduler::mDone: Set("w2"),1045 schedFixed::scheduler::mExpect: Set(),1046 schedFixed::scheduler::mResult: Set("c2"),1047 schedFixed::scheduler::mRetry: Set(),1048 schedFixed::scheduler::mRevoke: Set(),1049 schedFixed::scheduler::mSchedule: Set(),1050 schedFixed::scheduler::published: 1,1051 schedFixed::scheduler::publishedBy: Set("w2"),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: true,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" -> CSent("w2")),1078 schedFixed::scheduler::crashes: 2,1079 schedFixed::scheduler::entry: [],1080 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1081 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),1082 schedFixed::scheduler::mBuild: Set(),1083 schedFixed::scheduler::mDone: Set(),1084 schedFixed::scheduler::mExpect: Set(),1085 schedFixed::scheduler::mResult: Set("c2"),1086 schedFixed::scheduler::mRetry: Set(),1087 schedFixed::scheduler::mRevoke: Set(),1088 schedFixed::scheduler::mSchedule: Set(),1089 schedFixed::scheduler::published: 1,1090 schedFixed::scheduler::publishedBy: Set("w2"),1091 schedFixed::scheduler::ws:1092 Map(1093 "w1" ->1094 {1095 attached: Set(),1096 built: false,1097 expecting: false,1098 running: false,1099 session: true,1100 up: true1101 },1102 "w2" ->1103 {1104 attached: Set(),1105 built: true,1106 expecting: false,1107 running: false,1108 session: true,1109 up: true1110 }1111 )1112}11131114[State 28]1115{1116 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CDone),1117 schedFixed::scheduler::crashes: 2,1118 schedFixed::scheduler::entry: [],1119 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1120 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),1121 schedFixed::scheduler::mBuild: Set(),1122 schedFixed::scheduler::mDone: Set(),1123 schedFixed::scheduler::mExpect: Set(),1124 schedFixed::scheduler::mResult: Set(),1125 schedFixed::scheduler::mRetry: Set(),1126 schedFixed::scheduler::mRevoke: Set(),1127 schedFixed::scheduler::mSchedule: Set(),1128 schedFixed::scheduler::published: 1,1129 schedFixed::scheduler::publishedBy: Set("w2"),1130 schedFixed::scheduler::ws:1131 Map(1132 "w1" ->1133 {1134 attached: Set(),1135 built: false,1136 expecting: false,1137 running: false,1138 session: true,1139 up: true1140 },1141 "w2" ->1142 {1143 attached: Set(),1144 built: true,1145 expecting: false,1146 running: false,1147 session: true,1148 up: true1149 }1150 )1151}11521153[State 29]1154{1155 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CDone),1156 schedFixed::scheduler::crashes: 2,1157 schedFixed::scheduler::entry: [],1158 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1159 schedFixed::scheduler::mAssigned: Set(),1160 schedFixed::scheduler::mBuild: Set(("c1", "w2")),1161 schedFixed::scheduler::mDone: Set(),1162 schedFixed::scheduler::mExpect: Set(),1163 schedFixed::scheduler::mResult: Set(),1164 schedFixed::scheduler::mRetry: Set(),1165 schedFixed::scheduler::mRevoke: Set(),1166 schedFixed::scheduler::mSchedule: Set(),1167 schedFixed::scheduler::published: 1,1168 schedFixed::scheduler::publishedBy: Set("w2"),1169 schedFixed::scheduler::ws:1170 Map(1171 "w1" ->1172 {1173 attached: Set(),1174 built: false,1175 expecting: false,1176 running: false,1177 session: true,1178 up: true1179 },1180 "w2" ->1181 {1182 attached: Set(),1183 built: true,1184 expecting: false,1185 running: false,1186 session: true,1187 up: true1188 }1189 )1190}11911192[State 30]1193{1194 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CDone),1195 schedFixed::scheduler::crashes: 2,1196 schedFixed::scheduler::entry: [],1197 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1198 schedFixed::scheduler::mAssigned: Set(),1199 schedFixed::scheduler::mBuild: Set(),1200 schedFixed::scheduler::mDone: Set(),1201 schedFixed::scheduler::mExpect: Set(),1202 schedFixed::scheduler::mResult: Set("c1"),1203 schedFixed::scheduler::mRetry: Set(),1204 schedFixed::scheduler::mRevoke: Set(),1205 schedFixed::scheduler::mSchedule: Set(),1206 schedFixed::scheduler::published: 1,1207 schedFixed::scheduler::publishedBy: Set("w2"),1208 schedFixed::scheduler::ws:1209 Map(1210 "w1" ->1211 {1212 attached: Set(),1213 built: false,1214 expecting: false,1215 running: false,1216 session: true,1217 up: true1218 },1219 "w2" ->1220 {1221 attached: Set(),1222 built: true,1223 expecting: false,1224 running: false,1225 session: true,1226 up: true1227 }1228 )1229}12301231[ok] No violation found (605ms at 49587 traces/second).1232Trace length statistics: max=31, min=16, average=18.921233You may increase --max-samples and --max-steps.1234Use --verbosity to produce more (or less) output.1235Use --seed=0xe347fa3b4024937f --backend=rust to reproduce.1236An example execution:12371238[State 0]1239{1240 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1241 schedNoRevoke::scheduler::crashes: 0,1242 schedNoRevoke::scheduler::entry: [],1243 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1244 schedNoRevoke::scheduler::mAssigned: Set(),1245 schedNoRevoke::scheduler::mBuild: Set(),1246 schedNoRevoke::scheduler::mDone: Set(),1247 schedNoRevoke::scheduler::mExpect: Set(),1248 schedNoRevoke::scheduler::mResult: Set(),1249 schedNoRevoke::scheduler::mRetry: Set(),1250 schedNoRevoke::scheduler::mRevoke: Set(),1251 schedNoRevoke::scheduler::mSchedule: Set(),1252 schedNoRevoke::scheduler::published: 0,1253 schedNoRevoke::scheduler::publishedBy: Set(),1254 schedNoRevoke::scheduler::ws:1255 Map(1256 "w1" ->1257 {1258 attached: Set(),1259 built: false,1260 expecting: false,1261 running: false,1262 session: true,1263 up: true1264 },1265 "w2" ->1266 {1267 attached: Set(),1268 built: false,1269 expecting: false,1270 running: false,1271 session: true,1272 up: true1273 }1274 )1275}12761277[State 1]1278{1279 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1280 schedNoRevoke::scheduler::crashes: 0,1281 schedNoRevoke::scheduler::entry: [],1282 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1283 schedNoRevoke::scheduler::mAssigned: Set(),1284 schedNoRevoke::scheduler::mBuild: Set(),1285 schedNoRevoke::scheduler::mDone: Set(),1286 schedNoRevoke::scheduler::mExpect: Set(),1287 schedNoRevoke::scheduler::mResult: Set(),1288 schedNoRevoke::scheduler::mRetry: Set(),1289 schedNoRevoke::scheduler::mRevoke: Set(),1290 schedNoRevoke::scheduler::mSchedule: Set("c2"),1291 schedNoRevoke::scheduler::published: 0,1292 schedNoRevoke::scheduler::publishedBy: Set(),1293 schedNoRevoke::scheduler::ws:1294 Map(1295 "w1" ->1296 {1297 attached: Set(),1298 built: false,1299 expecting: false,1300 running: false,1301 session: true,1302 up: true1303 },1304 "w2" ->1305 {1306 attached: Set(),1307 built: false,1308 expecting: false,1309 running: false,1310 session: true,1311 up: true1312 }1313 )1314}13151316[State 2]1317{1318 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1319 schedNoRevoke::scheduler::crashes: 0,1320 schedNoRevoke::scheduler::entry:1321 [{ followers: Set("c2"), leased: true, worker: "w1" }],1322 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1323 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1324 schedNoRevoke::scheduler::mBuild: Set(),1325 schedNoRevoke::scheduler::mDone: Set(),1326 schedNoRevoke::scheduler::mExpect: Set("w1"),1327 schedNoRevoke::scheduler::mResult: Set(),1328 schedNoRevoke::scheduler::mRetry: Set(),1329 schedNoRevoke::scheduler::mRevoke: Set(),1330 schedNoRevoke::scheduler::mSchedule: Set(),1331 schedNoRevoke::scheduler::published: 0,1332 schedNoRevoke::scheduler::publishedBy: Set(),1333 schedNoRevoke::scheduler::ws:1334 Map(1335 "w1" ->1336 {1337 attached: Set(),1338 built: false,1339 expecting: false,1340 running: false,1341 session: true,1342 up: true1343 },1344 "w2" ->1345 {1346 attached: Set(),1347 built: false,1348 expecting: false,1349 running: false,1350 session: true,1351 up: true1352 }1353 )1354}13551356[State 3]1357{1358 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1359 schedNoRevoke::scheduler::crashes: 0,1360 schedNoRevoke::scheduler::entry:1361 [{ followers: Set("c2"), leased: true, worker: "w1" }],1362 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1363 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1364 schedNoRevoke::scheduler::mBuild: Set(),1365 schedNoRevoke::scheduler::mDone: Set(),1366 schedNoRevoke::scheduler::mExpect: Set(),1367 schedNoRevoke::scheduler::mResult: Set(),1368 schedNoRevoke::scheduler::mRetry: Set(),1369 schedNoRevoke::scheduler::mRevoke: Set(),1370 schedNoRevoke::scheduler::mSchedule: Set(),1371 schedNoRevoke::scheduler::published: 0,1372 schedNoRevoke::scheduler::publishedBy: Set(),1373 schedNoRevoke::scheduler::ws:1374 Map(1375 "w1" ->1376 {1377 attached: Set(),1378 built: false,1379 expecting: true,1380 running: true,1381 session: true,1382 up: true1383 },1384 "w2" ->1385 {1386 attached: Set(),1387 built: false,1388 expecting: false,1389 running: false,1390 session: true,1391 up: true1392 }1393 )1394}13951396[State 4]1397{1398 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1399 schedNoRevoke::scheduler::crashes: 1,1400 schedNoRevoke::scheduler::entry: [],1401 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1402 schedNoRevoke::scheduler::mAssigned: Set(),1403 schedNoRevoke::scheduler::mBuild: Set(),1404 schedNoRevoke::scheduler::mDone: Set(),1405 schedNoRevoke::scheduler::mExpect: Set(),1406 schedNoRevoke::scheduler::mResult: Set(),1407 schedNoRevoke::scheduler::mRetry: Set("c2"),1408 schedNoRevoke::scheduler::mRevoke: Set(),1409 schedNoRevoke::scheduler::mSchedule: Set(),1410 schedNoRevoke::scheduler::published: 0,1411 schedNoRevoke::scheduler::publishedBy: Set(),1412 schedNoRevoke::scheduler::ws:1413 Map(1414 "w1" ->1415 {1416 attached: Set(),1417 built: false,1418 expecting: true,1419 running: true,1420 session: false,1421 up: true1422 },1423 "w2" ->1424 {1425 attached: Set(),1426 built: false,1427 expecting: false,1428 running: false,1429 session: false,1430 up: true1431 }1432 )1433}14341435[State 5]1436{1437 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1438 schedNoRevoke::scheduler::crashes: 2,1439 schedNoRevoke::scheduler::entry: [],1440 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1441 schedNoRevoke::scheduler::mAssigned: Set(),1442 schedNoRevoke::scheduler::mBuild: Set(),1443 schedNoRevoke::scheduler::mDone: Set(),1444 schedNoRevoke::scheduler::mExpect: Set(),1445 schedNoRevoke::scheduler::mResult: Set(),1446 schedNoRevoke::scheduler::mRetry: Set("c2"),1447 schedNoRevoke::scheduler::mRevoke: Set(),1448 schedNoRevoke::scheduler::mSchedule: Set(),1449 schedNoRevoke::scheduler::published: 0,1450 schedNoRevoke::scheduler::publishedBy: Set(),1451 schedNoRevoke::scheduler::ws:1452 Map(1453 "w1" ->1454 {1455 attached: Set(),1456 built: false,1457 expecting: true,1458 running: true,1459 session: false,1460 up: true1461 },1462 "w2" ->1463 {1464 attached: Set(),1465 built: false,1466 expecting: false,1467 running: false,1468 session: false,1469 up: false1470 }1471 )1472}14731474[State 6]1475{1476 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1477 schedNoRevoke::scheduler::crashes: 2,1478 schedNoRevoke::scheduler::entry: [],1479 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1480 schedNoRevoke::scheduler::mAssigned: Set(),1481 schedNoRevoke::scheduler::mBuild: Set(),1482 schedNoRevoke::scheduler::mDone: Set(),1483 schedNoRevoke::scheduler::mExpect: Set(),1484 schedNoRevoke::scheduler::mResult: Set(),1485 schedNoRevoke::scheduler::mRetry: Set("c2"),1486 schedNoRevoke::scheduler::mRevoke: Set(),1487 schedNoRevoke::scheduler::mSchedule: Set(),1488 schedNoRevoke::scheduler::published: 0,1489 schedNoRevoke::scheduler::publishedBy: Set(),1490 schedNoRevoke::scheduler::ws:1491 Map(1492 "w1" ->1493 {1494 attached: Set(),1495 built: false,1496 expecting: true,1497 running: true,1498 session: false,1499 up: true1500 },1501 "w2" ->1502 {1503 attached: Set(),1504 built: false,1505 expecting: false,1506 running: false,1507 session: true,1508 up: true1509 }1510 )1511}15121513[State 7]1514{1515 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1516 schedNoRevoke::scheduler::crashes: 2,1517 schedNoRevoke::scheduler::entry: [],1518 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1519 schedNoRevoke::scheduler::mAssigned: Set(),1520 schedNoRevoke::scheduler::mBuild: Set(),1521 schedNoRevoke::scheduler::mDone: Set(),1522 schedNoRevoke::scheduler::mExpect: Set(),1523 schedNoRevoke::scheduler::mResult: Set(),1524 schedNoRevoke::scheduler::mRetry: Set(),1525 schedNoRevoke::scheduler::mRevoke: Set(),1526 schedNoRevoke::scheduler::mSchedule: Set("c2"),1527 schedNoRevoke::scheduler::published: 0,1528 schedNoRevoke::scheduler::publishedBy: Set(),1529 schedNoRevoke::scheduler::ws:1530 Map(1531 "w1" ->1532 {1533 attached: Set(),1534 built: false,1535 expecting: true,1536 running: true,1537 session: false,1538 up: true1539 },1540 "w2" ->1541 {1542 attached: Set(),1543 built: false,1544 expecting: false,1545 running: false,1546 session: true,1547 up: true1548 }1549 )1550}15511552[State 8]1553{1554 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1555 schedNoRevoke::scheduler::crashes: 2,1556 schedNoRevoke::scheduler::entry:1557 [{ followers: Set("c2"), leased: true, worker: "w2" }],1558 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1559 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1560 schedNoRevoke::scheduler::mBuild: Set(),1561 schedNoRevoke::scheduler::mDone: Set(),1562 schedNoRevoke::scheduler::mExpect: Set("w2"),1563 schedNoRevoke::scheduler::mResult: Set(),1564 schedNoRevoke::scheduler::mRetry: Set(),1565 schedNoRevoke::scheduler::mRevoke: Set(),1566 schedNoRevoke::scheduler::mSchedule: Set(),1567 schedNoRevoke::scheduler::published: 0,1568 schedNoRevoke::scheduler::publishedBy: Set(),1569 schedNoRevoke::scheduler::ws:1570 Map(1571 "w1" ->1572 {1573 attached: Set(),1574 built: false,1575 expecting: true,1576 running: true,1577 session: false,1578 up: true1579 },1580 "w2" ->1581 {1582 attached: Set(),1583 built: false,1584 expecting: false,1585 running: false,1586 session: true,1587 up: true1588 }1589 )1590}15911592[State 9]1593{1594 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1595 schedNoRevoke::scheduler::crashes: 2,1596 schedNoRevoke::scheduler::entry:1597 [{ followers: Set("c2"), leased: true, worker: "w2" }],1598 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1599 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1600 schedNoRevoke::scheduler::mBuild: Set(),1601 schedNoRevoke::scheduler::mDone: Set(),1602 schedNoRevoke::scheduler::mExpect: Set(),1603 schedNoRevoke::scheduler::mResult: Set(),1604 schedNoRevoke::scheduler::mRetry: Set(),1605 schedNoRevoke::scheduler::mRevoke: Set(),1606 schedNoRevoke::scheduler::mSchedule: Set(),1607 schedNoRevoke::scheduler::published: 0,1608 schedNoRevoke::scheduler::publishedBy: Set(),1609 schedNoRevoke::scheduler::ws:1610 Map(1611 "w1" ->1612 {1613 attached: Set(),1614 built: false,1615 expecting: true,1616 running: true,1617 session: false,1618 up: true1619 },1620 "w2" ->1621 {1622 attached: Set(),1623 built: false,1624 expecting: true,1625 running: true,1626 session: true,1627 up: true1628 }1629 )1630}16311632[State 10]1633{1634 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1635 schedNoRevoke::scheduler::crashes: 2,1636 schedNoRevoke::scheduler::entry:1637 [{ followers: Set("c2"), leased: true, worker: "w2" }],1638 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1639 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1640 schedNoRevoke::scheduler::mBuild: Set(),1641 schedNoRevoke::scheduler::mDone: Set(),1642 schedNoRevoke::scheduler::mExpect: Set(),1643 schedNoRevoke::scheduler::mResult: Set(),1644 schedNoRevoke::scheduler::mRetry: Set(),1645 schedNoRevoke::scheduler::mRevoke: Set(),1646 schedNoRevoke::scheduler::mSchedule: Set(),1647 schedNoRevoke::scheduler::published: 0,1648 schedNoRevoke::scheduler::publishedBy: Set(),1649 schedNoRevoke::scheduler::ws:1650 Map(1651 "w1" ->1652 {1653 attached: Set(),1654 built: false,1655 expecting: true,1656 running: true,1657 session: true,1658 up: true1659 },1660 "w2" ->1661 {1662 attached: Set(),1663 built: false,1664 expecting: true,1665 running: true,1666 session: true,1667 up: true1668 }1669 )1670}16711672[violation] Found an issue (618ms at 46157 traces/second).1673Use --verbosity=3 to show executions.1674Use --seed=0xb3f356270994aba3 --backend=rust to reproduce.1675error: Invariant violated1676An example execution:16771678[State 0]1679{1680 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1681 schedNoFence::scheduler::crashes: 0,1682 schedNoFence::scheduler::entry: [],1683 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1684 schedNoFence::scheduler::mAssigned: Set(),1685 schedNoFence::scheduler::mBuild: Set(),1686 schedNoFence::scheduler::mDone: Set(),1687 schedNoFence::scheduler::mExpect: Set(),1688 schedNoFence::scheduler::mResult: Set(),1689 schedNoFence::scheduler::mRetry: Set(),1690 schedNoFence::scheduler::mRevoke: Set(),1691 schedNoFence::scheduler::mSchedule: Set(),1692 schedNoFence::scheduler::published: 0,1693 schedNoFence::scheduler::publishedBy: Set(),1694 schedNoFence::scheduler::ws:1695 Map(1696 "w1" ->1697 {1698 attached: Set(),1699 built: false,1700 expecting: false,1701 running: false,1702 session: true,1703 up: true1704 },1705 "w2" ->1706 {1707 attached: Set(),1708 built: false,1709 expecting: false,1710 running: false,1711 session: true,1712 up: true1713 }1714 )1715}17161717[State 1]1718{1719 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1720 schedNoFence::scheduler::crashes: 0,1721 schedNoFence::scheduler::entry: [],1722 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1723 schedNoFence::scheduler::mAssigned: Set(),1724 schedNoFence::scheduler::mBuild: Set(),1725 schedNoFence::scheduler::mDone: Set(),1726 schedNoFence::scheduler::mExpect: Set(),1727 schedNoFence::scheduler::mResult: Set(),1728 schedNoFence::scheduler::mRetry: Set(),1729 schedNoFence::scheduler::mRevoke: Set(),1730 schedNoFence::scheduler::mSchedule: Set("c2"),1731 schedNoFence::scheduler::published: 0,1732 schedNoFence::scheduler::publishedBy: Set(),1733 schedNoFence::scheduler::ws:1734 Map(1735 "w1" ->1736 {1737 attached: Set(),1738 built: false,1739 expecting: false,1740 running: false,1741 session: true,1742 up: true1743 },1744 "w2" ->1745 {1746 attached: Set(),1747 built: false,1748 expecting: false,1749 running: false,1750 session: true,1751 up: true1752 }1753 )1754}17551756[State 2]1757{1758 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1759 schedNoFence::scheduler::crashes: 0,1760 schedNoFence::scheduler::entry:1761 [{ followers: Set("c2"), leased: true, worker: "w1" }],1762 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1763 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1764 schedNoFence::scheduler::mBuild: Set(),1765 schedNoFence::scheduler::mDone: Set(),1766 schedNoFence::scheduler::mExpect: Set("w1"),1767 schedNoFence::scheduler::mResult: Set(),1768 schedNoFence::scheduler::mRetry: Set(),1769 schedNoFence::scheduler::mRevoke: Set(),1770 schedNoFence::scheduler::mSchedule: Set(),1771 schedNoFence::scheduler::published: 0,1772 schedNoFence::scheduler::publishedBy: Set(),1773 schedNoFence::scheduler::ws:1774 Map(1775 "w1" ->1776 {1777 attached: Set(),1778 built: false,1779 expecting: false,1780 running: false,1781 session: true,1782 up: true1783 },1784 "w2" ->1785 {1786 attached: Set(),1787 built: false,1788 expecting: false,1789 running: false,1790 session: true,1791 up: true1792 }1793 )1794}17951796[State 3]1797{1798 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1799 schedNoFence::scheduler::crashes: 1,1800 schedNoFence::scheduler::entry:1801 [{ followers: Set("c2"), leased: true, worker: "w1" }],1802 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1803 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1804 schedNoFence::scheduler::mBuild: Set(),1805 schedNoFence::scheduler::mDone: Set(),1806 schedNoFence::scheduler::mExpect: Set("w1"),1807 schedNoFence::scheduler::mResult: Set(),1808 schedNoFence::scheduler::mRetry: Set(),1809 schedNoFence::scheduler::mRevoke: Set(),1810 schedNoFence::scheduler::mSchedule: Set(),1811 schedNoFence::scheduler::published: 0,1812 schedNoFence::scheduler::publishedBy: Set(),1813 schedNoFence::scheduler::ws:1814 Map(1815 "w1" ->1816 {1817 attached: Set(),1818 built: false,1819 expecting: false,1820 running: false,1821 session: true,1822 up: true1823 },1824 "w2" ->1825 {1826 attached: Set(),1827 built: false,1828 expecting: false,1829 running: false,1830 session: false,1831 up: false1832 }1833 )1834}18351836[State 4]1837{1838 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1839 schedNoFence::scheduler::crashes: 1,1840 schedNoFence::scheduler::entry:1841 [{ followers: Set("c2"), leased: true, worker: "w1" }],1842 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1843 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1844 schedNoFence::scheduler::mBuild: Set(),1845 schedNoFence::scheduler::mDone: Set(),1846 schedNoFence::scheduler::mExpect: Set(),1847 schedNoFence::scheduler::mResult: Set(),1848 schedNoFence::scheduler::mRetry: Set(),1849 schedNoFence::scheduler::mRevoke: Set(),1850 schedNoFence::scheduler::mSchedule: Set(),1851 schedNoFence::scheduler::published: 0,1852 schedNoFence::scheduler::publishedBy: Set(),1853 schedNoFence::scheduler::ws:1854 Map(1855 "w1" ->1856 {1857 attached: Set(),1858 built: false,1859 expecting: true,1860 running: true,1861 session: true,1862 up: true1863 },1864 "w2" ->1865 {1866 attached: Set(),1867 built: false,1868 expecting: false,1869 running: false,1870 session: false,1871 up: false1872 }1873 )1874}18751876[State 5]1877{1878 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1879 schedNoFence::scheduler::crashes: 2,1880 schedNoFence::scheduler::entry: [],1881 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1882 schedNoFence::scheduler::mAssigned: Set(),1883 schedNoFence::scheduler::mBuild: Set(),1884 schedNoFence::scheduler::mDone: Set(),1885 schedNoFence::scheduler::mExpect: Set(),1886 schedNoFence::scheduler::mResult: Set(),1887 schedNoFence::scheduler::mRetry: Set("c2"),1888 schedNoFence::scheduler::mRevoke: Set(),1889 schedNoFence::scheduler::mSchedule: Set(),1890 schedNoFence::scheduler::published: 0,1891 schedNoFence::scheduler::publishedBy: Set(),1892 schedNoFence::scheduler::ws:1893 Map(1894 "w1" ->1895 {1896 attached: Set(),1897 built: false,1898 expecting: true,1899 running: true,1900 session: false,1901 up: true1902 },1903 "w2" ->1904 {1905 attached: Set(),1906 built: false,1907 expecting: false,1908 running: false,1909 session: false,1910 up: false1911 }1912 )1913}19141915[State 6]1916{1917 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1918 schedNoFence::scheduler::crashes: 2,1919 schedNoFence::scheduler::entry: [],1920 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1921 schedNoFence::scheduler::mAssigned: Set(),1922 schedNoFence::scheduler::mBuild: Set(),1923 schedNoFence::scheduler::mDone: Set(),1924 schedNoFence::scheduler::mExpect: Set(),1925 schedNoFence::scheduler::mResult: Set(),1926 schedNoFence::scheduler::mRetry: Set("c2"),1927 schedNoFence::scheduler::mRevoke: Set(),1928 schedNoFence::scheduler::mSchedule: Set("c1"),1929 schedNoFence::scheduler::published: 0,1930 schedNoFence::scheduler::publishedBy: Set(),1931 schedNoFence::scheduler::ws:1932 Map(1933 "w1" ->1934 {1935 attached: Set(),1936 built: false,1937 expecting: true,1938 running: true,1939 session: false,1940 up: true1941 },1942 "w2" ->1943 {1944 attached: Set(),1945 built: false,1946 expecting: false,1947 running: false,1948 session: false,1949 up: false1950 }1951 )1952}19531954[State 7]1955{1956 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1957 schedNoFence::scheduler::crashes: 2,1958 schedNoFence::scheduler::entry: [],1959 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1960 schedNoFence::scheduler::mAssigned: Set(),1961 schedNoFence::scheduler::mBuild: Set(),1962 schedNoFence::scheduler::mDone: Set(),1963 schedNoFence::scheduler::mExpect: Set(),1964 schedNoFence::scheduler::mResult: Set(),1965 schedNoFence::scheduler::mRetry: Set("c2"),1966 schedNoFence::scheduler::mRevoke: Set(),1967 schedNoFence::scheduler::mSchedule: Set("c1"),1968 schedNoFence::scheduler::published: 0,1969 schedNoFence::scheduler::publishedBy: Set(),1970 schedNoFence::scheduler::ws:1971 Map(1972 "w1" ->1973 {1974 attached: Set(),1975 built: false,1976 expecting: true,1977 running: true,1978 session: false,1979 up: true1980 },1981 "w2" ->1982 {1983 attached: Set(),1984 built: false,1985 expecting: false,1986 running: false,1987 session: true,1988 up: true1989 }1990 )1991}19921993[State 8]1994{1995 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1996 schedNoFence::scheduler::crashes: 2,1997 schedNoFence::scheduler::entry:1998 [{ followers: Set("c1"), leased: true, worker: "w2" }],1999 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2000 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2001 schedNoFence::scheduler::mBuild: Set(),2002 schedNoFence::scheduler::mDone: Set(),2003 schedNoFence::scheduler::mExpect: Set("w2"),2004 schedNoFence::scheduler::mResult: Set(),2005 schedNoFence::scheduler::mRetry: Set("c2"),2006 schedNoFence::scheduler::mRevoke: Set(),2007 schedNoFence::scheduler::mSchedule: Set(),2008 schedNoFence::scheduler::published: 0,2009 schedNoFence::scheduler::publishedBy: Set(),2010 schedNoFence::scheduler::ws:2011 Map(2012 "w1" ->2013 {2014 attached: Set(),2015 built: false,2016 expecting: true,2017 running: true,2018 session: false,2019 up: true2020 },2021 "w2" ->2022 {2023 attached: Set(),2024 built: false,2025 expecting: false,2026 running: false,2027 session: true,2028 up: true2029 }2030 )2031}20322033[State 9]2034{2035 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2036 schedNoFence::scheduler::crashes: 2,2037 schedNoFence::scheduler::entry:2038 [{ followers: Set("c1"), leased: true, worker: "w2" }],2039 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2040 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2041 schedNoFence::scheduler::mBuild: Set(),2042 schedNoFence::scheduler::mDone: Set(),2043 schedNoFence::scheduler::mExpect: Set("w2"),2044 schedNoFence::scheduler::mResult: Set(),2045 schedNoFence::scheduler::mRetry: Set("c2"),2046 schedNoFence::scheduler::mRevoke: Set(),2047 schedNoFence::scheduler::mSchedule: Set(),2048 schedNoFence::scheduler::published: 1,2049 schedNoFence::scheduler::publishedBy: Set("w1"),2050 schedNoFence::scheduler::ws:2051 Map(2052 "w1" ->2053 {2054 attached: Set(),2055 built: true,2056 expecting: false,2057 running: false,2058 session: false,2059 up: true2060 },2061 "w2" ->2062 {2063 attached: Set(),2064 built: false,2065 expecting: false,2066 running: false,2067 session: true,2068 up: true2069 }2070 )2071}20722073[State 10]2074{2075 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2076 schedNoFence::scheduler::crashes: 2,2077 schedNoFence::scheduler::entry:2078 [{ followers: Set("c1"), leased: true, worker: "w2" }],2079 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2080 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2081 schedNoFence::scheduler::mBuild: Set(),2082 schedNoFence::scheduler::mDone: Set(),2083 schedNoFence::scheduler::mExpect: Set("w2"),2084 schedNoFence::scheduler::mResult: Set(),2085 schedNoFence::scheduler::mRetry: Set("c2"),2086 schedNoFence::scheduler::mRevoke: Set(),2087 schedNoFence::scheduler::mSchedule: Set(),2088 schedNoFence::scheduler::published: 1,2089 schedNoFence::scheduler::publishedBy: Set("w1"),2090 schedNoFence::scheduler::ws:2091 Map(2092 "w1" ->2093 {2094 attached: Set(),2095 built: true,2096 expecting: false,2097 running: false,2098 session: true,2099 up: true2100 },2101 "w2" ->2102 {2103 attached: Set(),2104 built: false,2105 expecting: false,2106 running: false,2107 session: true,2108 up: true2109 }2110 )2111}21122113[State 11]2114{2115 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2116 schedNoFence::scheduler::crashes: 2,2117 schedNoFence::scheduler::entry:2118 [{ followers: Set("c1"), leased: true, worker: "w2" }],2119 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2120 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2121 schedNoFence::scheduler::mBuild: Set(),2122 schedNoFence::scheduler::mDone: Set(),2123 schedNoFence::scheduler::mExpect: Set(),2124 schedNoFence::scheduler::mResult: Set(),2125 schedNoFence::scheduler::mRetry: Set("c2"),2126 schedNoFence::scheduler::mRevoke: Set(),2127 schedNoFence::scheduler::mSchedule: Set(),2128 schedNoFence::scheduler::published: 1,2129 schedNoFence::scheduler::publishedBy: Set("w1"),2130 schedNoFence::scheduler::ws:2131 Map(2132 "w1" ->2133 {2134 attached: Set(),2135 built: true,2136 expecting: false,2137 running: false,2138 session: true,2139 up: true2140 },2141 "w2" ->2142 {2143 attached: Set(),2144 built: false,2145 expecting: true,2146 running: true,2147 session: true,2148 up: true2149 }2150 )2151}21522153[State 12]2154{2155 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2156 schedNoFence::scheduler::crashes: 2,2157 schedNoFence::scheduler::entry:2158 [{ followers: Set("c1"), leased: true, worker: "w2" }],2159 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2160 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2161 schedNoFence::scheduler::mBuild: Set(),2162 schedNoFence::scheduler::mDone: Set("w2"),2163 schedNoFence::scheduler::mExpect: Set(),2164 schedNoFence::scheduler::mResult: Set(),2165 schedNoFence::scheduler::mRetry: Set("c2"),2166 schedNoFence::scheduler::mRevoke: Set(),2167 schedNoFence::scheduler::mSchedule: Set(),2168 schedNoFence::scheduler::published: 2,2169 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2170 schedNoFence::scheduler::ws:2171 Map(2172 "w1" ->2173 {2174 attached: Set(),2175 built: true,2176 expecting: false,2177 running: false,2178 session: true,2179 up: true2180 },2181 "w2" ->2182 {2183 attached: Set(),2184 built: true,2185 expecting: false,2186 running: false,2187 session: true,2188 up: true2189 }2190 )2191}21922193[violation] Found an issue (532ms at 48009 traces/second).2194Use --verbosity=3 to show executions.2195Use --seed=0x62c8417706907d42 --backend=rust to reproduce.2196error: Invariant violated2197An example execution:21982199[State 0]2200{2201 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2202 schedNoPush::scheduler::crashes: 0,2203 schedNoPush::scheduler::entry: [],2204 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2205 schedNoPush::scheduler::mAssigned: Set(),2206 schedNoPush::scheduler::mBuild: Set(),2207 schedNoPush::scheduler::mDone: Set(),2208 schedNoPush::scheduler::mExpect: Set(),2209 schedNoPush::scheduler::mResult: Set(),2210 schedNoPush::scheduler::mRetry: Set(),2211 schedNoPush::scheduler::mRevoke: Set(),2212 schedNoPush::scheduler::mSchedule: Set(),2213 schedNoPush::scheduler::published: 0,2214 schedNoPush::scheduler::publishedBy: Set(),2215 schedNoPush::scheduler::ws:2216 Map(2217 "w1" ->2218 {2219 attached: Set(),2220 built: false,2221 expecting: false,2222 running: false,2223 session: true,2224 up: true2225 },2226 "w2" ->2227 {2228 attached: Set(),2229 built: false,2230 expecting: false,2231 running: false,2232 session: true,2233 up: true2234 }2235 )2236}22372238[State 1]2239{2240 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2241 schedNoPush::scheduler::crashes: 0,2242 schedNoPush::scheduler::entry: [],2243 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2244 schedNoPush::scheduler::mAssigned: Set(),2245 schedNoPush::scheduler::mBuild: Set(),2246 schedNoPush::scheduler::mDone: Set(),2247 schedNoPush::scheduler::mExpect: Set(),2248 schedNoPush::scheduler::mResult: Set(),2249 schedNoPush::scheduler::mRetry: Set(),2250 schedNoPush::scheduler::mRevoke: Set(),2251 schedNoPush::scheduler::mSchedule: Set("c1"),2252 schedNoPush::scheduler::published: 0,2253 schedNoPush::scheduler::publishedBy: Set(),2254 schedNoPush::scheduler::ws:2255 Map(2256 "w1" ->2257 {2258 attached: Set(),2259 built: false,2260 expecting: false,2261 running: false,2262 session: true,2263 up: true2264 },2265 "w2" ->2266 {2267 attached: Set(),2268 built: false,2269 expecting: false,2270 running: false,2271 session: true,2272 up: true2273 }2274 )2275}22762277[State 2]2278{2279 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2280 schedNoPush::scheduler::crashes: 0,2281 schedNoPush::scheduler::entry:2282 [{ followers: Set("c1"), leased: true, worker: "w1" }],2283 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2284 schedNoPush::scheduler::mAssigned: Set(("c1", "w1")),2285 schedNoPush::scheduler::mBuild: Set(),2286 schedNoPush::scheduler::mDone: Set(),2287 schedNoPush::scheduler::mExpect: Set(),2288 schedNoPush::scheduler::mResult: Set(),2289 schedNoPush::scheduler::mRetry: Set(),2290 schedNoPush::scheduler::mRevoke: Set(),2291 schedNoPush::scheduler::mSchedule: Set(),2292 schedNoPush::scheduler::published: 0,2293 schedNoPush::scheduler::publishedBy: Set(),2294 schedNoPush::scheduler::ws:2295 Map(2296 "w1" ->2297 {2298 attached: Set(),2299 built: false,2300 expecting: false,2301 running: false,2302 session: true,2303 up: true2304 },2305 "w2" ->2306 {2307 attached: Set(),2308 built: false,2309 expecting: false,2310 running: false,2311 session: true,2312 up: true2313 }2314 )2315}23162317[State 3]2318{2319 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2320 schedNoPush::scheduler::crashes: 0,2321 schedNoPush::scheduler::entry:2322 [{ followers: Set("c1"), leased: true, worker: "w1" }],2323 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2324 schedNoPush::scheduler::mAssigned: Set(),2325 schedNoPush::scheduler::mBuild: Set(("c1", "w1")),2326 schedNoPush::scheduler::mDone: Set(),2327 schedNoPush::scheduler::mExpect: Set(),2328 schedNoPush::scheduler::mResult: Set(),2329 schedNoPush::scheduler::mRetry: Set(),2330 schedNoPush::scheduler::mRevoke: Set(),2331 schedNoPush::scheduler::mSchedule: Set(),2332 schedNoPush::scheduler::published: 0,2333 schedNoPush::scheduler::publishedBy: Set(),2334 schedNoPush::scheduler::ws:2335 Map(2336 "w1" ->2337 {2338 attached: Set(),2339 built: false,2340 expecting: false,2341 running: false,2342 session: true,2343 up: true2344 },2345 "w2" ->2346 {2347 attached: Set(),2348 built: false,2349 expecting: false,2350 running: false,2351 session: true,2352 up: true2353 }2354 )2355}23562357[State 4]2358{2359 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2360 schedNoPush::scheduler::crashes: 1,2361 schedNoPush::scheduler::entry:2362 [{ followers: Set("c1"), leased: true, worker: "w1" }],2363 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2364 schedNoPush::scheduler::mAssigned: Set(),2365 schedNoPush::scheduler::mBuild: Set(("c1", "w1")),2366 schedNoPush::scheduler::mDone: Set(),2367 schedNoPush::scheduler::mExpect: Set(),2368 schedNoPush::scheduler::mResult: Set(),2369 schedNoPush::scheduler::mRetry: Set(),2370 schedNoPush::scheduler::mRevoke: Set(),2371 schedNoPush::scheduler::mSchedule: Set(),2372 schedNoPush::scheduler::published: 0,2373 schedNoPush::scheduler::publishedBy: Set(),2374 schedNoPush::scheduler::ws:2375 Map(2376 "w1" ->2377 {2378 attached: Set(),2379 built: false,2380 expecting: false,2381 running: false,2382 session: false,2383 up: false2384 },2385 "w2" ->2386 {2387 attached: Set(),2388 built: false,2389 expecting: false,2390 running: false,2391 session: true,2392 up: true2393 }2394 )2395}23962397[State 5]2398{2399 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2400 schedNoPush::scheduler::crashes: 1,2401 schedNoPush::scheduler::entry: [],2402 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2403 schedNoPush::scheduler::mAssigned: Set(),2404 schedNoPush::scheduler::mBuild: Set(("c1", "w1")),2405 schedNoPush::scheduler::mDone: Set(),2406 schedNoPush::scheduler::mExpect: Set(),2407 schedNoPush::scheduler::mResult: Set(),2408 schedNoPush::scheduler::mRetry: Set("c1"),2409 schedNoPush::scheduler::mRevoke: Set(),2410 schedNoPush::scheduler::mSchedule: Set(),2411 schedNoPush::scheduler::published: 0,2412 schedNoPush::scheduler::publishedBy: Set(),2413 schedNoPush::scheduler::ws:2414 Map(2415 "w1" ->2416 {2417 attached: Set(),2418 built: false,2419 expecting: false,2420 running: false,2421 session: true,2422 up: true2423 },2424 "w2" ->2425 {2426 attached: Set(),2427 built: false,2428 expecting: false,2429 running: false,2430 session: true,2431 up: true2432 }2433 )2434}24352436[State 6]2437{2438 schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),2439 schedNoPush::scheduler::crashes: 1,2440 schedNoPush::scheduler::entry: [],2441 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2442 schedNoPush::scheduler::mAssigned: Set(),2443 schedNoPush::scheduler::mBuild: Set(),2444 schedNoPush::scheduler::mDone: Set(),2445 schedNoPush::scheduler::mExpect: Set(),2446 schedNoPush::scheduler::mResult: Set(),2447 schedNoPush::scheduler::mRetry: Set("c1"),2448 schedNoPush::scheduler::mRevoke: Set(),2449 schedNoPush::scheduler::mSchedule: Set(),2450 schedNoPush::scheduler::published: 0,2451 schedNoPush::scheduler::publishedBy: Set(),2452 schedNoPush::scheduler::ws:2453 Map(2454 "w1" ->2455 {2456 attached: Set("c1"),2457 built: false,2458 expecting: true,2459 running: true,2460 session: true,2461 up: true2462 },2463 "w2" ->2464 {2465 attached: Set(),2466 built: false,2467 expecting: false,2468 running: false,2469 session: true,2470 up: true2471 }2472 )2473}24742475[violation] Found an issue (455ms at 24943 traces/second).2476Use --verbosity=3 to show executions.2477Use --seed=0x94f935d2d8f14f5b --backend=rust to reproduce.2478error: Invariant violated2479An example execution:24802481[State 0]2482{2483 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2484 schedNoReport::scheduler::crashes: 0,2485 schedNoReport::scheduler::entry: [],2486 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2487 schedNoReport::scheduler::mAssigned: Set(),2488 schedNoReport::scheduler::mBuild: Set(),2489 schedNoReport::scheduler::mDone: Set(),2490 schedNoReport::scheduler::mExpect: Set(),2491 schedNoReport::scheduler::mResult: Set(),2492 schedNoReport::scheduler::mRetry: Set(),2493 schedNoReport::scheduler::mRevoke: Set(),2494 schedNoReport::scheduler::mSchedule: Set(),2495 schedNoReport::scheduler::published: 0,2496 schedNoReport::scheduler::publishedBy: Set(),2497 schedNoReport::scheduler::ws:2498 Map(2499 "w1" ->2500 {2501 attached: Set(),2502 built: false,2503 expecting: false,2504 running: false,2505 session: true,2506 up: true2507 },2508 "w2" ->2509 {2510 attached: Set(),2511 built: false,2512 expecting: false,2513 running: false,2514 session: true,2515 up: true2516 }2517 )2518}25192520[State 1]2521{2522 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2523 schedNoReport::scheduler::crashes: 0,2524 schedNoReport::scheduler::entry: [],2525 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2526 schedNoReport::scheduler::mAssigned: Set(),2527 schedNoReport::scheduler::mBuild: Set(),2528 schedNoReport::scheduler::mDone: Set(),2529 schedNoReport::scheduler::mExpect: Set(),2530 schedNoReport::scheduler::mResult: Set(),2531 schedNoReport::scheduler::mRetry: Set(),2532 schedNoReport::scheduler::mRevoke: Set(),2533 schedNoReport::scheduler::mSchedule: Set("c2"),2534 schedNoReport::scheduler::published: 0,2535 schedNoReport::scheduler::publishedBy: Set(),2536 schedNoReport::scheduler::ws:2537 Map(2538 "w1" ->2539 {2540 attached: Set(),2541 built: false,2542 expecting: false,2543 running: false,2544 session: true,2545 up: true2546 },2547 "w2" ->2548 {2549 attached: Set(),2550 built: false,2551 expecting: false,2552 running: false,2553 session: true,2554 up: true2555 }2556 )2557}25582559[State 2]2560{2561 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2562 schedNoReport::scheduler::crashes: 0,2563 schedNoReport::scheduler::entry:2564 [{ followers: Set("c2"), leased: true, worker: "w1" }],2565 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2566 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2567 schedNoReport::scheduler::mBuild: Set(),2568 schedNoReport::scheduler::mDone: Set(),2569 schedNoReport::scheduler::mExpect: Set("w1"),2570 schedNoReport::scheduler::mResult: Set(),2571 schedNoReport::scheduler::mRetry: Set(),2572 schedNoReport::scheduler::mRevoke: Set(),2573 schedNoReport::scheduler::mSchedule: Set(),2574 schedNoReport::scheduler::published: 0,2575 schedNoReport::scheduler::publishedBy: Set(),2576 schedNoReport::scheduler::ws:2577 Map(2578 "w1" ->2579 {2580 attached: Set(),2581 built: false,2582 expecting: false,2583 running: false,2584 session: true,2585 up: true2586 },2587 "w2" ->2588 {2589 attached: Set(),2590 built: false,2591 expecting: false,2592 running: false,2593 session: true,2594 up: true2595 }2596 )2597}25982599[State 3]2600{2601 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2602 schedNoReport::scheduler::crashes: 0,2603 schedNoReport::scheduler::entry:2604 [{ followers: Set("c2"), leased: true, worker: "w1" }],2605 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2606 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2607 schedNoReport::scheduler::mBuild: Set(),2608 schedNoReport::scheduler::mDone: Set(),2609 schedNoReport::scheduler::mExpect: Set(),2610 schedNoReport::scheduler::mResult: Set(),2611 schedNoReport::scheduler::mRetry: Set(),2612 schedNoReport::scheduler::mRevoke: Set(),2613 schedNoReport::scheduler::mSchedule: Set(),2614 schedNoReport::scheduler::published: 0,2615 schedNoReport::scheduler::publishedBy: Set(),2616 schedNoReport::scheduler::ws:2617 Map(2618 "w1" ->2619 {2620 attached: Set(),2621 built: false,2622 expecting: true,2623 running: true,2624 session: true,2625 up: true2626 },2627 "w2" ->2628 {2629 attached: Set(),2630 built: false,2631 expecting: false,2632 running: false,2633 session: true,2634 up: true2635 }2636 )2637}26382639[State 4]2640{2641 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2642 schedNoReport::scheduler::crashes: 1,2643 schedNoReport::scheduler::entry: [],2644 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2645 schedNoReport::scheduler::mAssigned: Set(),2646 schedNoReport::scheduler::mBuild: Set(),2647 schedNoReport::scheduler::mDone: Set(),2648 schedNoReport::scheduler::mExpect: Set(),2649 schedNoReport::scheduler::mResult: Set(),2650 schedNoReport::scheduler::mRetry: Set("c2"),2651 schedNoReport::scheduler::mRevoke: Set(),2652 schedNoReport::scheduler::mSchedule: Set(),2653 schedNoReport::scheduler::published: 0,2654 schedNoReport::scheduler::publishedBy: Set(),2655 schedNoReport::scheduler::ws:2656 Map(2657 "w1" ->2658 {2659 attached: Set(),2660 built: false,2661 expecting: true,2662 running: true,2663 session: false,2664 up: true2665 },2666 "w2" ->2667 {2668 attached: Set(),2669 built: false,2670 expecting: false,2671 running: false,2672 session: false,2673 up: true2674 }2675 )2676}26772678[State 5]2679{2680 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2681 schedNoReport::scheduler::crashes: 2,2682 schedNoReport::scheduler::entry: [],2683 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2684 schedNoReport::scheduler::mAssigned: Set(),2685 schedNoReport::scheduler::mBuild: Set(),2686 schedNoReport::scheduler::mDone: Set(),2687 schedNoReport::scheduler::mExpect: Set(),2688 schedNoReport::scheduler::mResult: Set(),2689 schedNoReport::scheduler::mRetry: Set("c2"),2690 schedNoReport::scheduler::mRevoke: Set(),2691 schedNoReport::scheduler::mSchedule: Set(),2692 schedNoReport::scheduler::published: 0,2693 schedNoReport::scheduler::publishedBy: Set(),2694 schedNoReport::scheduler::ws:2695 Map(2696 "w1" ->2697 {2698 attached: Set(),2699 built: false,2700 expecting: true,2701 running: true,2702 session: false,2703 up: true2704 },2705 "w2" ->2706 {2707 attached: Set(),2708 built: false,2709 expecting: false,2710 running: false,2711 session: false,2712 up: true2713 }2714 )2715}27162717[State 6]2718{2719 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2720 schedNoReport::scheduler::crashes: 2,2721 schedNoReport::scheduler::entry: [],2722 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2723 schedNoReport::scheduler::mAssigned: Set(),2724 schedNoReport::scheduler::mBuild: Set(),2725 schedNoReport::scheduler::mDone: Set(),2726 schedNoReport::scheduler::mExpect: Set(),2727 schedNoReport::scheduler::mResult: Set(),2728 schedNoReport::scheduler::mRetry: Set("c2"),2729 schedNoReport::scheduler::mRevoke: Set(),2730 schedNoReport::scheduler::mSchedule: Set("c1"),2731 schedNoReport::scheduler::published: 0,2732 schedNoReport::scheduler::publishedBy: Set(),2733 schedNoReport::scheduler::ws:2734 Map(2735 "w1" ->2736 {2737 attached: Set(),2738 built: false,2739 expecting: true,2740 running: true,2741 session: false,2742 up: true2743 },2744 "w2" ->2745 {2746 attached: Set(),2747 built: false,2748 expecting: false,2749 running: false,2750 session: false,2751 up: true2752 }2753 )2754}27552756[State 7]2757{2758 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2759 schedNoReport::scheduler::crashes: 2,2760 schedNoReport::scheduler::entry: [],2761 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2762 schedNoReport::scheduler::mAssigned: Set(),2763 schedNoReport::scheduler::mBuild: Set(),2764 schedNoReport::scheduler::mDone: Set(),2765 schedNoReport::scheduler::mExpect: Set(),2766 schedNoReport::scheduler::mResult: Set(),2767 schedNoReport::scheduler::mRetry: Set(),2768 schedNoReport::scheduler::mRevoke: Set(),2769 schedNoReport::scheduler::mSchedule: Set("c1", "c2"),2770 schedNoReport::scheduler::published: 0,2771 schedNoReport::scheduler::publishedBy: Set(),2772 schedNoReport::scheduler::ws:2773 Map(2774 "w1" ->2775 {2776 attached: Set(),2777 built: false,2778 expecting: true,2779 running: true,2780 session: false,2781 up: true2782 },2783 "w2" ->2784 {2785 attached: Set(),2786 built: false,2787 expecting: false,2788 running: false,2789 session: false,2790 up: true2791 }2792 )2793}27942795[State 8]2796{2797 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2798 schedNoReport::scheduler::crashes: 2,2799 schedNoReport::scheduler::entry: [],2800 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2801 schedNoReport::scheduler::mAssigned: Set(),2802 schedNoReport::scheduler::mBuild: Set(),2803 schedNoReport::scheduler::mDone: Set(),2804 schedNoReport::scheduler::mExpect: Set(),2805 schedNoReport::scheduler::mResult: Set(),2806 schedNoReport::scheduler::mRetry: Set(),2807 schedNoReport::scheduler::mRevoke: Set(),2808 schedNoReport::scheduler::mSchedule: Set("c1", "c2"),2809 schedNoReport::scheduler::published: 0,2810 schedNoReport::scheduler::publishedBy: Set(),2811 schedNoReport::scheduler::ws:2812 Map(2813 "w1" ->2814 {2815 attached: Set(),2816 built: false,2817 expecting: true,2818 running: true,2819 session: false,2820 up: true2821 },2822 "w2" ->2823 {2824 attached: Set(),2825 built: false,2826 expecting: false,2827 running: false,2828 session: true,2829 up: true2830 }2831 )2832}28332834[State 9]2835{2836 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2837 schedNoReport::scheduler::crashes: 2,2838 schedNoReport::scheduler::entry:2839 [{ followers: Set("c2"), leased: true, worker: "w2" }],2840 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2841 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2842 schedNoReport::scheduler::mBuild: Set(),2843 schedNoReport::scheduler::mDone: Set(),2844 schedNoReport::scheduler::mExpect: Set("w2"),2845 schedNoReport::scheduler::mResult: Set(),2846 schedNoReport::scheduler::mRetry: Set(),2847 schedNoReport::scheduler::mRevoke: Set(),2848 schedNoReport::scheduler::mSchedule: Set("c1"),2849 schedNoReport::scheduler::published: 0,2850 schedNoReport::scheduler::publishedBy: Set(),2851 schedNoReport::scheduler::ws:2852 Map(2853 "w1" ->2854 {2855 attached: Set(),2856 built: false,2857 expecting: true,2858 running: true,2859 session: false,2860 up: true2861 },2862 "w2" ->2863 {2864 attached: Set(),2865 built: false,2866 expecting: false,2867 running: false,2868 session: true,2869 up: true2870 }2871 )2872}28732874[State 10]2875{2876 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2877 schedNoReport::scheduler::crashes: 2,2878 schedNoReport::scheduler::entry:2879 [{ followers: Set("c2"), leased: true, worker: "w2" }],2880 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2881 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2882 schedNoReport::scheduler::mBuild: Set(),2883 schedNoReport::scheduler::mDone: Set(),2884 schedNoReport::scheduler::mExpect: Set(),2885 schedNoReport::scheduler::mResult: Set(),2886 schedNoReport::scheduler::mRetry: Set(),2887 schedNoReport::scheduler::mRevoke: Set(),2888 schedNoReport::scheduler::mSchedule: Set("c1"),2889 schedNoReport::scheduler::published: 0,2890 schedNoReport::scheduler::publishedBy: Set(),2891 schedNoReport::scheduler::ws:2892 Map(2893 "w1" ->2894 {2895 attached: Set(),2896 built: false,2897 expecting: true,2898 running: true,2899 session: false,2900 up: true2901 },2902 "w2" ->2903 {2904 attached: Set(),2905 built: false,2906 expecting: true,2907 running: true,2908 session: true,2909 up: true2910 }2911 )2912}29132914[State 11]2915{2916 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2917 schedNoReport::scheduler::crashes: 2,2918 schedNoReport::scheduler::entry:2919 [{ followers: Set("c2"), leased: true, worker: "w2" }],2920 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2921 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2922 schedNoReport::scheduler::mBuild: Set(),2923 schedNoReport::scheduler::mDone: Set(),2924 schedNoReport::scheduler::mExpect: Set(),2925 schedNoReport::scheduler::mResult: Set(),2926 schedNoReport::scheduler::mRetry: Set(),2927 schedNoReport::scheduler::mRevoke: Set(),2928 schedNoReport::scheduler::mSchedule: Set("c1"),2929 schedNoReport::scheduler::published: 0,2930 schedNoReport::scheduler::publishedBy: Set(),2931 schedNoReport::scheduler::ws:2932 Map(2933 "w1" ->2934 {2935 attached: Set(),2936 built: false,2937 expecting: true,2938 running: true,2939 session: true,2940 up: true2941 },2942 "w2" ->2943 {2944 attached: Set(),2945 built: false,2946 expecting: true,2947 running: true,2948 session: true,2949 up: true2950 }2951 )2952}29532954[violation] Found an issue (396ms at 56237 traces/second).2955Use --verbosity=3 to show executions.2956Use --seed=0xbc9fc12202d7bc3c --backend=rust to reproduce.2957error: Invariant violated2958An example execution:29592960[State 0]2961{2962 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2963 schedTerminal::scheduler::crashes: 0,2964 schedTerminal::scheduler::entry: [],2965 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2966 schedTerminal::scheduler::mAssigned: Set(),2967 schedTerminal::scheduler::mBuild: Set(),2968 schedTerminal::scheduler::mDone: Set(),2969 schedTerminal::scheduler::mExpect: Set(),2970 schedTerminal::scheduler::mResult: Set(),2971 schedTerminal::scheduler::mRetry: Set(),2972 schedTerminal::scheduler::mRevoke: Set(),2973 schedTerminal::scheduler::mSchedule: Set(),2974 schedTerminal::scheduler::published: 0,2975 schedTerminal::scheduler::publishedBy: Set(),2976 schedTerminal::scheduler::ws:2977 Map(2978 "w1" ->2979 {2980 attached: Set(),2981 built: false,2982 expecting: false,2983 running: false,2984 session: true,2985 up: true2986 },2987 "w2" ->2988 {2989 attached: Set(),2990 built: false,2991 expecting: false,2992 running: false,2993 session: true,2994 up: true2995 }2996 )2997}29982999[State 1]3000{3001 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3002 schedTerminal::scheduler::crashes: 1,3003 schedTerminal::scheduler::entry: [],3004 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3005 schedTerminal::scheduler::mAssigned: Set(),3006 schedTerminal::scheduler::mBuild: Set(),3007 schedTerminal::scheduler::mDone: Set(),3008 schedTerminal::scheduler::mExpect: Set(),3009 schedTerminal::scheduler::mResult: Set(),3010 schedTerminal::scheduler::mRetry: Set(),3011 schedTerminal::scheduler::mRevoke: Set(),3012 schedTerminal::scheduler::mSchedule: Set(),3013 schedTerminal::scheduler::published: 0,3014 schedTerminal::scheduler::publishedBy: Set(),3015 schedTerminal::scheduler::ws:3016 Map(3017 "w1" ->3018 {3019 attached: Set(),3020 built: false,3021 expecting: false,3022 running: false,3023 session: false,3024 up: true3025 },3026 "w2" ->3027 {3028 attached: Set(),3029 built: false,3030 expecting: false,3031 running: false,3032 session: false,3033 up: true3034 }3035 )3036}30373038[State 2]3039{3040 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3041 schedTerminal::scheduler::crashes: 1,3042 schedTerminal::scheduler::entry: [],3043 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3044 schedTerminal::scheduler::mAssigned: Set(),3045 schedTerminal::scheduler::mBuild: Set(),3046 schedTerminal::scheduler::mDone: Set(),3047 schedTerminal::scheduler::mExpect: Set(),3048 schedTerminal::scheduler::mResult: Set(),3049 schedTerminal::scheduler::mRetry: Set(),3050 schedTerminal::scheduler::mRevoke: Set(),3051 schedTerminal::scheduler::mSchedule: Set("c2"),3052 schedTerminal::scheduler::published: 0,3053 schedTerminal::scheduler::publishedBy: Set(),3054 schedTerminal::scheduler::ws:3055 Map(3056 "w1" ->3057 {3058 attached: Set(),3059 built: false,3060 expecting: false,3061 running: false,3062 session: false,3063 up: true3064 },3065 "w2" ->3066 {3067 attached: Set(),3068 built: false,3069 expecting: false,3070 running: false,3071 session: false,3072 up: true3073 }3074 )3075}30763077[State 3]3078{3079 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3080 schedTerminal::scheduler::crashes: 1,3081 schedTerminal::scheduler::entry: [],3082 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3083 schedTerminal::scheduler::mAssigned: Set(),3084 schedTerminal::scheduler::mBuild: Set(),3085 schedTerminal::scheduler::mDone: Set(),3086 schedTerminal::scheduler::mExpect: Set(),3087 schedTerminal::scheduler::mResult: Set(),3088 schedTerminal::scheduler::mRetry: Set(),3089 schedTerminal::scheduler::mRevoke: Set(),3090 schedTerminal::scheduler::mSchedule: Set(),3091 schedTerminal::scheduler::published: 0,3092 schedTerminal::scheduler::publishedBy: Set(),3093 schedTerminal::scheduler::ws:3094 Map(3095 "w1" ->3096 {3097 attached: Set(),3098 built: false,3099 expecting: false,3100 running: false,3101 session: false,3102 up: true3103 },3104 "w2" ->3105 {3106 attached: Set(),3107 built: false,3108 expecting: false,3109 running: false,3110 session: false,3111 up: true3112 }3113 )3114}31153116[violation] Found an issue (188ms at 5085 traces/second).3117Use --verbosity=3 to show executions.3118Use --seed=0x17c54e5fc14acece --backend=rust to reproduce.3119error: Invariant violated3120An example execution:31213122[State 0]3123{3124 pushFixed::push::byPath: Map(),3125 pushFixed::push::inflight: Set(),3126 pushFixed::push::left: Map(),3127 pushFixed::push::sent: Map()3128}31293130[State 1]3131{3132 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3133 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3134 pushFixed::push::left: Map(1 -> 2),3135 pushFixed::push::sent: Map(1 -> Set("a", "b"))3136}31373138[State 2]3139{3140 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3141 pushFixed::push::inflight: Set((1, "a")),3142 pushFixed::push::left: Map(1 -> 1),3143 pushFixed::push::sent: Map(1 -> Set("a", "b"))3144}31453146[State 3]3147{3148 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3149 pushFixed::push::inflight: Set((1, "a"), (3, "a"), (3, "b")),3150 pushFixed::push::left: Map(1 -> 1, 3 -> 2),3151 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3152}31533154[State 4]3155{3156 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3157 pushFixed::push::inflight:3158 Set((1, "a"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),3159 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 2),3160 pushFixed::push::sent:3161 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3162}31633164[State 5]3165{3166 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3167 pushFixed::push::inflight: Set((1, "a"), (2, "a"), (3, "a"), (3, "b")),3168 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 2),3169 pushFixed::push::sent:3170 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3171}31723173[State 6]3174{3175 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3176 pushFixed::push::inflight: Set((1, "a"), (2, "a"), (3, "b")),3177 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 1),3178 pushFixed::push::sent:3179 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3180}31813182[State 7]3183{3184 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3185 pushFixed::push::inflight: Set((2, "a"), (3, "b")),3186 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 1),3187 pushFixed::push::sent:3188 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3189}31903191[State 8]3192{3193 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3194 pushFixed::push::inflight: Set((2, "a")),3195 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 0),3196 pushFixed::push::sent:3197 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3198}31993200[State 9]3201{3202 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3203 pushFixed::push::inflight: Set(),3204 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3205 pushFixed::push::sent:3206 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3207}32083209[ok] No violation found (87ms at 229885 traces/second).3210Trace length statistics: max=10, min=7, average=8.073211You may increase --max-samples and --max-steps.3212Use --verbosity to produce more (or less) output.3213Use --seed=0x6eb63c8d5034dfb --backend=rust to reproduce.