nix-grpc-store-spec
checks.aarch64-linux.spec
· build #385
· 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: true,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" -> 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: true195 }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: true234 }235 )236}237238[State 6]239{240 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),241 schedFixed::scheduler::crashes: 2,242 schedFixed::scheduler::entry: [],243 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),244 schedFixed::scheduler::mAssigned: Set(),245 schedFixed::scheduler::mBuild: Set(),246 schedFixed::scheduler::mDone: Set(),247 schedFixed::scheduler::mExpect: Set(),248 schedFixed::scheduler::mResult: Set(),249 schedFixed::scheduler::mRetry: Set(),250 schedFixed::scheduler::mRevoke: Set(),251 schedFixed::scheduler::mSchedule: Set("c1"),252 schedFixed::scheduler::published: 0,253 schedFixed::scheduler::publishedBy: Set(),254 schedFixed::scheduler::ws:255 Map(256 "w1" ->257 {258 attached: Set(),259 built: false,260 expecting: false,261 running: false,262 session: 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("c2"), leased: true, worker: "w1" }],361 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),362 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),363 schedFixed::scheduler::mBuild: Set(),364 schedFixed::scheduler::mDone: Set(),365 schedFixed::scheduler::mExpect: Set("w1"),366 schedFixed::scheduler::mResult: Set(),367 schedFixed::scheduler::mRetry: Set(),368 schedFixed::scheduler::mRevoke: Set(),369 schedFixed::scheduler::mSchedule: Set("c1"),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" -> CQueued, "c2" -> CQueued),398 schedFixed::scheduler::crashes: 2,399 schedFixed::scheduler::entry:400 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],401 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),402 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),403 schedFixed::scheduler::mBuild: Set(),404 schedFixed::scheduler::mDone: Set(),405 schedFixed::scheduler::mExpect: Set("w1"),406 schedFixed::scheduler::mResult: Set(),407 schedFixed::scheduler::mRetry: Set(),408 schedFixed::scheduler::mRevoke: Set(),409 schedFixed::scheduler::mSchedule: Set(),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" -> CQueued, "c2" -> CSent("w1")),438 schedFixed::scheduler::crashes: 2,439 schedFixed::scheduler::entry:440 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],441 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),442 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),443 schedFixed::scheduler::mBuild: Set(("c2", "w1")),444 schedFixed::scheduler::mDone: Set(),445 schedFixed::scheduler::mExpect: Set("w1"),446 schedFixed::scheduler::mResult: Set(),447 schedFixed::scheduler::mRetry: Set(),448 schedFixed::scheduler::mRevoke: Set(),449 schedFixed::scheduler::mSchedule: Set(),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" -> CSent("w1")),478 schedFixed::scheduler::crashes: 2,479 schedFixed::scheduler::entry:480 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],481 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),482 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),483 schedFixed::scheduler::mBuild: Set(),484 schedFixed::scheduler::mDone: Set(),485 schedFixed::scheduler::mExpect: Set("w1"),486 schedFixed::scheduler::mResult: Set(),487 schedFixed::scheduler::mRetry: Set("c2"),488 schedFixed::scheduler::mRevoke: Set(),489 schedFixed::scheduler::mSchedule: Set(),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("w1"), "c2" -> CSent("w1")),518 schedFixed::scheduler::crashes: 2,519 schedFixed::scheduler::entry:520 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],521 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),522 schedFixed::scheduler::mAssigned: Set(),523 schedFixed::scheduler::mBuild: Set(("c1", "w1")),524 schedFixed::scheduler::mDone: Set(),525 schedFixed::scheduler::mExpect: Set("w1"),526 schedFixed::scheduler::mResult: Set(),527 schedFixed::scheduler::mRetry: Set("c2"),528 schedFixed::scheduler::mRevoke: Set(),529 schedFixed::scheduler::mSchedule: Set(),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" -> CSent("w1"), "c2" -> CSent("w1")),558 schedFixed::scheduler::crashes: 2,559 schedFixed::scheduler::entry:560 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],561 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),562 schedFixed::scheduler::mAssigned: Set(),563 schedFixed::scheduler::mBuild: Set(),564 schedFixed::scheduler::mDone: Set(),565 schedFixed::scheduler::mExpect: Set("w1"),566 schedFixed::scheduler::mResult: Set(),567 schedFixed::scheduler::mRetry: Set("c1", "c2"),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("w1")),598 schedFixed::scheduler::crashes: 2,599 schedFixed::scheduler::entry:600 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],601 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),602 schedFixed::scheduler::mAssigned: Set(),603 schedFixed::scheduler::mBuild: Set(),604 schedFixed::scheduler::mDone: Set(),605 schedFixed::scheduler::mExpect: Set("w1"),606 schedFixed::scheduler::mResult: Set(),607 schedFixed::scheduler::mRetry: Set("c2"),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("w1")),638 schedFixed::scheduler::crashes: 2,639 schedFixed::scheduler::entry:640 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],641 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),642 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),643 schedFixed::scheduler::mBuild: Set(),644 schedFixed::scheduler::mDone: Set(),645 schedFixed::scheduler::mExpect: Set("w1"),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: "w1" }],681 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),682 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),683 schedFixed::scheduler::mBuild: Set(),684 schedFixed::scheduler::mDone: Set(),685 schedFixed::scheduler::mExpect: Set("w1"),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: "w1" }],721 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),722 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),723 schedFixed::scheduler::mBuild: Set(),724 schedFixed::scheduler::mDone: Set(),725 schedFixed::scheduler::mExpect: Set("w1"),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("w1"), "c2" -> CQueued),758 schedFixed::scheduler::crashes: 2,759 schedFixed::scheduler::entry:760 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],761 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),762 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),763 schedFixed::scheduler::mBuild: Set(("c1", "w1")),764 schedFixed::scheduler::mDone: Set(),765 schedFixed::scheduler::mExpect: Set("w1"),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("w1"), "c2" -> CSent("w1")),798 schedFixed::scheduler::crashes: 2,799 schedFixed::scheduler::entry:800 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],801 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),802 schedFixed::scheduler::mAssigned: Set(),803 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),804 schedFixed::scheduler::mDone: Set(),805 schedFixed::scheduler::mExpect: Set("w1"),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("w1"), "c2" -> CSent("w1")),838 schedFixed::scheduler::crashes: 2,839 schedFixed::scheduler::entry:840 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],841 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),842 schedFixed::scheduler::mAssigned: Set(),843 schedFixed::scheduler::mBuild: Set(("c2", "w1")),844 schedFixed::scheduler::mDone: Set(),845 schedFixed::scheduler::mExpect: Set("w1"),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("w1")),878 schedFixed::scheduler::crashes: 2,879 schedFixed::scheduler::entry:880 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],881 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),882 schedFixed::scheduler::mAssigned: Set(),883 schedFixed::scheduler::mBuild: Set(("c2", "w1")),884 schedFixed::scheduler::mDone: Set(),885 schedFixed::scheduler::mExpect: Set("w1"),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("w1")),918 schedFixed::scheduler::crashes: 2,919 schedFixed::scheduler::entry:920 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],921 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),922 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),923 schedFixed::scheduler::mBuild: Set(("c2", "w1")),924 schedFixed::scheduler::mDone: Set(),925 schedFixed::scheduler::mExpect: Set("w1"),926 schedFixed::scheduler::mResult: Set(),927 schedFixed::scheduler::mRetry: Set(),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("w1"), "c2" -> CSent("w1")),958 schedFixed::scheduler::crashes: 2,959 schedFixed::scheduler::entry:960 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],961 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),962 schedFixed::scheduler::mAssigned: Set(),963 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),964 schedFixed::scheduler::mDone: Set(),965 schedFixed::scheduler::mExpect: Set("w1"),966 schedFixed::scheduler::mResult: Set(),967 schedFixed::scheduler::mRetry: Set(),968 schedFixed::scheduler::mRevoke: Set(),969 schedFixed::scheduler::mSchedule: Set(),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("w1"), "c2" -> CSent("w1")),998 schedFixed::scheduler::crashes: 2,999 schedFixed::scheduler::entry:1000 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1001 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1002 schedFixed::scheduler::mAssigned: Set(),1003 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),1004 schedFixed::scheduler::mDone: Set(),1005 schedFixed::scheduler::mExpect: Set(),1006 schedFixed::scheduler::mResult: Set(),1007 schedFixed::scheduler::mRetry: Set(),1008 schedFixed::scheduler::mRevoke: Set(),1009 schedFixed::scheduler::mSchedule: Set(),1010 schedFixed::scheduler::published: 0,1011 schedFixed::scheduler::publishedBy: Set(),1012 schedFixed::scheduler::ws:1013 Map(1014 "w1" ->1015 {1016 attached: Set(),1017 built: false,1018 expecting: true,1019 running: true,1020 session: true,1021 up: true1022 },1023 "w2" ->1024 {1025 attached: Set(),1026 built: false,1027 expecting: false,1028 running: false,1029 session: true,1030 up: true1031 }1032 )1033}10341035[State 26]1036{1037 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1038 schedFixed::scheduler::crashes: 2,1039 schedFixed::scheduler::entry:1040 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1041 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1042 schedFixed::scheduler::mAssigned: Set(),1043 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),1044 schedFixed::scheduler::mDone: Set("w1"),1045 schedFixed::scheduler::mExpect: Set(),1046 schedFixed::scheduler::mResult: Set(),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("w1"),1052 schedFixed::scheduler::ws:1053 Map(1054 "w1" ->1055 {1056 attached: Set(),1057 built: true,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" -> CSent("w1"), "c2" -> CSent("w1")),1078 schedFixed::scheduler::crashes: 2,1079 schedFixed::scheduler::entry: [],1080 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1081 schedFixed::scheduler::mAssigned: Set(),1082 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),1083 schedFixed::scheduler::mDone: Set(),1084 schedFixed::scheduler::mExpect: Set(),1085 schedFixed::scheduler::mResult: Set(),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("w1"),1091 schedFixed::scheduler::ws:1092 Map(1093 "w1" ->1094 {1095 attached: Set(),1096 built: true,1097 expecting: false,1098 running: false,1099 session: true,1100 up: true1101 },1102 "w2" ->1103 {1104 attached: Set(),1105 built: false,1106 expecting: false,1107 running: false,1108 session: true,1109 up: true1110 }1111 )1112}11131114[State 28]1115{1116 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1117 schedFixed::scheduler::crashes: 2,1118 schedFixed::scheduler::entry: [],1119 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1120 schedFixed::scheduler::mAssigned: Set(),1121 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1122 schedFixed::scheduler::mDone: Set(),1123 schedFixed::scheduler::mExpect: Set(),1124 schedFixed::scheduler::mResult: Set("c1"),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("w1"),1130 schedFixed::scheduler::ws:1131 Map(1132 "w1" ->1133 {1134 attached: Set(),1135 built: true,1136 expecting: false,1137 running: false,1138 session: true,1139 up: true1140 },1141 "w2" ->1142 {1143 attached: Set(),1144 built: false,1145 expecting: false,1146 running: false,1147 session: true,1148 up: true1149 }1150 )1151}11521153[State 29]1154{1155 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w1")),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(("c2", "w1")),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("w1"),1169 schedFixed::scheduler::ws:1170 Map(1171 "w1" ->1172 {1173 attached: Set(),1174 built: true,1175 expecting: false,1176 running: false,1177 session: true,1178 up: true1179 },1180 "w2" ->1181 {1182 attached: Set(),1183 built: false,1184 expecting: false,1185 running: false,1186 session: true,1187 up: true1188 }1189 )1190}11911192[State 30]1193{1194 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w1")),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("c2"),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("w1"),1208 schedFixed::scheduler::ws:1209 Map(1210 "w1" ->1211 {1212 attached: Set(),1213 built: true,1214 expecting: false,1215 running: false,1216 session: true,1217 up: true1218 },1219 "w2" ->1220 {1221 attached: Set(),1222 built: false,1223 expecting: false,1224 running: false,1225 session: true,1226 up: true1227 }1228 )1229}12301231[ok] No violation found (581ms at 51635 traces/second).1232Trace length statistics: max=28, min=16, average=19.021233You may increase --max-samples and --max-steps.1234Use --verbosity to produce more (or less) output.1235Use --seed=0x137d3d961114d28d --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" -> CQueued, "c2" -> CIdle),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("c1"),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" -> CQueued, "c2" -> CIdle),1319 schedNoRevoke::scheduler::crashes: 0,1320 schedNoRevoke::scheduler::entry:1321 [{ followers: Set("c1"), leased: true, worker: "w2" }],1322 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1323 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1324 schedNoRevoke::scheduler::mBuild: Set(),1325 schedNoRevoke::scheduler::mDone: Set(),1326 schedNoRevoke::scheduler::mExpect: Set("w2"),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" -> CQueued, "c2" -> CIdle),1359 schedNoRevoke::scheduler::crashes: 1,1360 schedNoRevoke::scheduler::entry:1361 [{ followers: Set("c1"), leased: true, worker: "w2" }],1362 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1363 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1364 schedNoRevoke::scheduler::mBuild: Set(),1365 schedNoRevoke::scheduler::mDone: Set(),1366 schedNoRevoke::scheduler::mExpect: Set("w2"),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: false,1380 running: false,1381 session: false,1382 up: false1383 },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" -> CQueued, "c2" -> CIdle),1399 schedNoRevoke::scheduler::crashes: 1,1400 schedNoRevoke::scheduler::entry:1401 [{ followers: Set("c1"), leased: true, worker: "w2" }],1402 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1403 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1404 schedNoRevoke::scheduler::mBuild: Set(),1405 schedNoRevoke::scheduler::mDone: Set(),1406 schedNoRevoke::scheduler::mExpect: Set(),1407 schedNoRevoke::scheduler::mResult: Set(),1408 schedNoRevoke::scheduler::mRetry: Set(),1409 schedNoRevoke::scheduler::mRevoke: Set(),1410 schedNoRevoke::scheduler::mSchedule: Set(),1411 schedNoRevoke::scheduler::published: 0,1412 schedNoRevoke::scheduler::publishedBy: Set(),1413 schedNoRevoke::scheduler::ws:1414 Map(1415 "w1" ->1416 {1417 attached: Set(),1418 built: false,1419 expecting: false,1420 running: false,1421 session: false,1422 up: false1423 },1424 "w2" ->1425 {1426 attached: Set(),1427 built: false,1428 expecting: true,1429 running: true,1430 session: true,1431 up: true1432 }1433 )1434}14351436[State 5]1437{1438 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1439 schedNoRevoke::scheduler::crashes: 2,1440 schedNoRevoke::scheduler::entry: [],1441 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1442 schedNoRevoke::scheduler::mAssigned: Set(),1443 schedNoRevoke::scheduler::mBuild: Set(),1444 schedNoRevoke::scheduler::mDone: Set(),1445 schedNoRevoke::scheduler::mExpect: Set(),1446 schedNoRevoke::scheduler::mResult: Set(),1447 schedNoRevoke::scheduler::mRetry: Set("c1"),1448 schedNoRevoke::scheduler::mRevoke: Set(),1449 schedNoRevoke::scheduler::mSchedule: Set(),1450 schedNoRevoke::scheduler::published: 0,1451 schedNoRevoke::scheduler::publishedBy: Set(),1452 schedNoRevoke::scheduler::ws:1453 Map(1454 "w1" ->1455 {1456 attached: Set(),1457 built: false,1458 expecting: false,1459 running: false,1460 session: false,1461 up: false1462 },1463 "w2" ->1464 {1465 attached: Set(),1466 built: false,1467 expecting: true,1468 running: true,1469 session: false,1470 up: true1471 }1472 )1473}14741475[State 6]1476{1477 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1478 schedNoRevoke::scheduler::crashes: 2,1479 schedNoRevoke::scheduler::entry: [],1480 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1481 schedNoRevoke::scheduler::mAssigned: Set(),1482 schedNoRevoke::scheduler::mBuild: Set(),1483 schedNoRevoke::scheduler::mDone: Set(),1484 schedNoRevoke::scheduler::mExpect: Set(),1485 schedNoRevoke::scheduler::mResult: Set(),1486 schedNoRevoke::scheduler::mRetry: Set("c1"),1487 schedNoRevoke::scheduler::mRevoke: Set(),1488 schedNoRevoke::scheduler::mSchedule: Set(),1489 schedNoRevoke::scheduler::published: 0,1490 schedNoRevoke::scheduler::publishedBy: Set(),1491 schedNoRevoke::scheduler::ws:1492 Map(1493 "w1" ->1494 {1495 attached: Set(),1496 built: false,1497 expecting: false,1498 running: false,1499 session: true,1500 up: true1501 },1502 "w2" ->1503 {1504 attached: Set(),1505 built: false,1506 expecting: true,1507 running: true,1508 session: false,1509 up: true1510 }1511 )1512}15131514[State 7]1515{1516 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1517 schedNoRevoke::scheduler::crashes: 2,1518 schedNoRevoke::scheduler::entry: [],1519 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1520 schedNoRevoke::scheduler::mAssigned: Set(),1521 schedNoRevoke::scheduler::mBuild: Set(),1522 schedNoRevoke::scheduler::mDone: Set(),1523 schedNoRevoke::scheduler::mExpect: Set(),1524 schedNoRevoke::scheduler::mResult: Set(),1525 schedNoRevoke::scheduler::mRetry: Set(),1526 schedNoRevoke::scheduler::mRevoke: Set(),1527 schedNoRevoke::scheduler::mSchedule: Set("c1"),1528 schedNoRevoke::scheduler::published: 0,1529 schedNoRevoke::scheduler::publishedBy: Set(),1530 schedNoRevoke::scheduler::ws:1531 Map(1532 "w1" ->1533 {1534 attached: Set(),1535 built: false,1536 expecting: false,1537 running: false,1538 session: true,1539 up: true1540 },1541 "w2" ->1542 {1543 attached: Set(),1544 built: false,1545 expecting: true,1546 running: true,1547 session: false,1548 up: true1549 }1550 )1551}15521553[State 8]1554{1555 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1556 schedNoRevoke::scheduler::crashes: 2,1557 schedNoRevoke::scheduler::entry:1558 [{ followers: Set("c1"), leased: true, worker: "w1" }],1559 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1560 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1561 schedNoRevoke::scheduler::mBuild: Set(),1562 schedNoRevoke::scheduler::mDone: Set(),1563 schedNoRevoke::scheduler::mExpect: Set("w1"),1564 schedNoRevoke::scheduler::mResult: Set(),1565 schedNoRevoke::scheduler::mRetry: Set(),1566 schedNoRevoke::scheduler::mRevoke: Set(),1567 schedNoRevoke::scheduler::mSchedule: Set(),1568 schedNoRevoke::scheduler::published: 0,1569 schedNoRevoke::scheduler::publishedBy: Set(),1570 schedNoRevoke::scheduler::ws:1571 Map(1572 "w1" ->1573 {1574 attached: Set(),1575 built: false,1576 expecting: false,1577 running: false,1578 session: true,1579 up: true1580 },1581 "w2" ->1582 {1583 attached: Set(),1584 built: false,1585 expecting: true,1586 running: true,1587 session: false,1588 up: true1589 }1590 )1591}15921593[State 9]1594{1595 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1596 schedNoRevoke::scheduler::crashes: 2,1597 schedNoRevoke::scheduler::entry:1598 [{ followers: Set("c1"), leased: true, worker: "w1" }],1599 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1600 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1601 schedNoRevoke::scheduler::mBuild: Set(),1602 schedNoRevoke::scheduler::mDone: Set(),1603 schedNoRevoke::scheduler::mExpect: Set("w1"),1604 schedNoRevoke::scheduler::mResult: Set(),1605 schedNoRevoke::scheduler::mRetry: Set(),1606 schedNoRevoke::scheduler::mRevoke: Set(),1607 schedNoRevoke::scheduler::mSchedule: Set(),1608 schedNoRevoke::scheduler::published: 0,1609 schedNoRevoke::scheduler::publishedBy: Set(),1610 schedNoRevoke::scheduler::ws:1611 Map(1612 "w1" ->1613 {1614 attached: Set(),1615 built: false,1616 expecting: false,1617 running: false,1618 session: true,1619 up: true1620 },1621 "w2" ->1622 {1623 attached: Set(),1624 built: false,1625 expecting: true,1626 running: true,1627 session: true,1628 up: true1629 }1630 )1631}16321633[State 10]1634{1635 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1636 schedNoRevoke::scheduler::crashes: 2,1637 schedNoRevoke::scheduler::entry:1638 [{ followers: Set("c1"), leased: true, worker: "w1" }],1639 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1640 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1641 schedNoRevoke::scheduler::mBuild: Set(),1642 schedNoRevoke::scheduler::mDone: Set(),1643 schedNoRevoke::scheduler::mExpect: Set(),1644 schedNoRevoke::scheduler::mResult: Set(),1645 schedNoRevoke::scheduler::mRetry: Set(),1646 schedNoRevoke::scheduler::mRevoke: Set(),1647 schedNoRevoke::scheduler::mSchedule: Set(),1648 schedNoRevoke::scheduler::published: 0,1649 schedNoRevoke::scheduler::publishedBy: Set(),1650 schedNoRevoke::scheduler::ws:1651 Map(1652 "w1" ->1653 {1654 attached: Set(),1655 built: false,1656 expecting: true,1657 running: true,1658 session: true,1659 up: true1660 },1661 "w2" ->1662 {1663 attached: Set(),1664 built: false,1665 expecting: true,1666 running: true,1667 session: true,1668 up: true1669 }1670 )1671}16721673[violation] Found an issue (520ms at 54842 traces/second).1674Use --verbosity=3 to show executions.1675Use --seed=0xf2b72cdfa5557d77 --backend=rust to reproduce.1676error: Invariant violated1677An example execution:16781679[State 0]1680{1681 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1682 schedNoFence::scheduler::crashes: 0,1683 schedNoFence::scheduler::entry: [],1684 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1685 schedNoFence::scheduler::mAssigned: Set(),1686 schedNoFence::scheduler::mBuild: Set(),1687 schedNoFence::scheduler::mDone: Set(),1688 schedNoFence::scheduler::mExpect: Set(),1689 schedNoFence::scheduler::mResult: Set(),1690 schedNoFence::scheduler::mRetry: Set(),1691 schedNoFence::scheduler::mRevoke: Set(),1692 schedNoFence::scheduler::mSchedule: Set(),1693 schedNoFence::scheduler::published: 0,1694 schedNoFence::scheduler::publishedBy: Set(),1695 schedNoFence::scheduler::ws:1696 Map(1697 "w1" ->1698 {1699 attached: Set(),1700 built: false,1701 expecting: false,1702 running: false,1703 session: true,1704 up: true1705 },1706 "w2" ->1707 {1708 attached: Set(),1709 built: false,1710 expecting: false,1711 running: false,1712 session: true,1713 up: true1714 }1715 )1716}17171718[State 1]1719{1720 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1721 schedNoFence::scheduler::crashes: 0,1722 schedNoFence::scheduler::entry: [],1723 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1724 schedNoFence::scheduler::mAssigned: Set(),1725 schedNoFence::scheduler::mBuild: Set(),1726 schedNoFence::scheduler::mDone: Set(),1727 schedNoFence::scheduler::mExpect: Set(),1728 schedNoFence::scheduler::mResult: Set(),1729 schedNoFence::scheduler::mRetry: Set(),1730 schedNoFence::scheduler::mRevoke: Set(),1731 schedNoFence::scheduler::mSchedule: Set("c1"),1732 schedNoFence::scheduler::published: 0,1733 schedNoFence::scheduler::publishedBy: Set(),1734 schedNoFence::scheduler::ws:1735 Map(1736 "w1" ->1737 {1738 attached: Set(),1739 built: false,1740 expecting: false,1741 running: false,1742 session: true,1743 up: true1744 },1745 "w2" ->1746 {1747 attached: Set(),1748 built: false,1749 expecting: false,1750 running: false,1751 session: true,1752 up: true1753 }1754 )1755}17561757[State 2]1758{1759 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1760 schedNoFence::scheduler::crashes: 0,1761 schedNoFence::scheduler::entry:1762 [{ followers: Set("c1"), leased: true, worker: "w1" }],1763 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1764 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1765 schedNoFence::scheduler::mBuild: Set(),1766 schedNoFence::scheduler::mDone: Set(),1767 schedNoFence::scheduler::mExpect: Set("w1"),1768 schedNoFence::scheduler::mResult: Set(),1769 schedNoFence::scheduler::mRetry: Set(),1770 schedNoFence::scheduler::mRevoke: Set(),1771 schedNoFence::scheduler::mSchedule: Set(),1772 schedNoFence::scheduler::published: 0,1773 schedNoFence::scheduler::publishedBy: Set(),1774 schedNoFence::scheduler::ws:1775 Map(1776 "w1" ->1777 {1778 attached: Set(),1779 built: false,1780 expecting: false,1781 running: false,1782 session: true,1783 up: true1784 },1785 "w2" ->1786 {1787 attached: Set(),1788 built: false,1789 expecting: false,1790 running: false,1791 session: true,1792 up: true1793 }1794 )1795}17961797[State 3]1798{1799 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1800 schedNoFence::scheduler::crashes: 0,1801 schedNoFence::scheduler::entry:1802 [{ followers: Set("c1"), leased: true, worker: "w1" }],1803 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1804 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1805 schedNoFence::scheduler::mBuild: Set(),1806 schedNoFence::scheduler::mDone: Set(),1807 schedNoFence::scheduler::mExpect: Set(),1808 schedNoFence::scheduler::mResult: Set(),1809 schedNoFence::scheduler::mRetry: Set(),1810 schedNoFence::scheduler::mRevoke: Set(),1811 schedNoFence::scheduler::mSchedule: Set(),1812 schedNoFence::scheduler::published: 0,1813 schedNoFence::scheduler::publishedBy: Set(),1814 schedNoFence::scheduler::ws:1815 Map(1816 "w1" ->1817 {1818 attached: Set(),1819 built: false,1820 expecting: true,1821 running: true,1822 session: true,1823 up: true1824 },1825 "w2" ->1826 {1827 attached: Set(),1828 built: false,1829 expecting: false,1830 running: false,1831 session: true,1832 up: true1833 }1834 )1835}18361837[State 4]1838{1839 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1840 schedNoFence::scheduler::crashes: 1,1841 schedNoFence::scheduler::entry: [],1842 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1843 schedNoFence::scheduler::mAssigned: Set(),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("c1"),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: false,1862 up: true1863 },1864 "w2" ->1865 {1866 attached: Set(),1867 built: false,1868 expecting: false,1869 running: false,1870 session: false,1871 up: true1872 }1873 )1874}18751876[State 5]1877{1878 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),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("c1"),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" -> CIdle),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("c1"),1927 schedNoFence::scheduler::mRevoke: Set(),1928 schedNoFence::scheduler::mSchedule: Set(),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: true,1949 up: true1950 }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("c1"),1966 schedNoFence::scheduler::mRevoke: Set(),1967 schedNoFence::scheduler::mSchedule: Set("c2"),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("c2"), leased: true, worker: "w2" }],1999 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2000 schedNoFence::scheduler::mAssigned: Set(("c2", "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("c1"),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("c2"), leased: true, worker: "w2" }],2039 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2040 schedNoFence::scheduler::mAssigned: Set(("c2", "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("c1"),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("c2"), leased: true, worker: "w2" }],2079 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2080 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2081 schedNoFence::scheduler::mBuild: Set(),2082 schedNoFence::scheduler::mDone: Set(),2083 schedNoFence::scheduler::mExpect: Set(),2084 schedNoFence::scheduler::mResult: Set(),2085 schedNoFence::scheduler::mRetry: Set("c1"),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: false,2099 up: true2100 },2101 "w2" ->2102 {2103 attached: Set(),2104 built: false,2105 expecting: true,2106 running: true,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("c2"), leased: true, worker: "w2" }],2119 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2120 schedNoFence::scheduler::mAssigned: Set(("c2", "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("c1"),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("c2"), leased: true, worker: "w2" }],2159 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2160 schedNoFence::scheduler::mAssigned: Set(("c2", "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("c1"),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 (482ms at 51390 traces/second).2194Use --verbosity=3 to show executions.2195Use --seed=0xf4bc73b50a2571fb --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: "w2" }],2283 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2284 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),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" -> CQueued, "c2" -> CIdle),2320 schedNoPush::scheduler::crashes: 1,2321 schedNoPush::scheduler::entry:2322 [{ followers: Set("c1"), leased: true, worker: "w2" }],2323 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2324 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2325 schedNoPush::scheduler::mBuild: Set(),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: false,2343 up: false2344 },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("w2"), "c2" -> CIdle),2360 schedNoPush::scheduler::crashes: 1,2361 schedNoPush::scheduler::entry:2362 [{ followers: Set("c1"), leased: true, worker: "w2" }],2363 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2364 schedNoPush::scheduler::mAssigned: Set(),2365 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),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("w2"), "c2" -> CIdle),2400 schedNoPush::scheduler::crashes: 2,2401 schedNoPush::scheduler::entry: [],2402 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2403 schedNoPush::scheduler::mAssigned: Set(),2404 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2405 schedNoPush::scheduler::mDone: Set(),2406 schedNoPush::scheduler::mExpect: Set(),2407 schedNoPush::scheduler::mResult: Set(),2408 schedNoPush::scheduler::mRetry: Set(),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: false,2422 up: false2423 },2424 "w2" ->2425 {2426 attached: Set(),2427 built: false,2428 expecting: false,2429 running: false,2430 session: false,2431 up: true2432 }2433 )2434}24352436[State 6]2437{2438 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2439 schedNoPush::scheduler::crashes: 2,2440 schedNoPush::scheduler::entry: [],2441 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2442 schedNoPush::scheduler::mAssigned: Set(),2443 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2444 schedNoPush::scheduler::mDone: Set(),2445 schedNoPush::scheduler::mExpect: Set(),2446 schedNoPush::scheduler::mResult: Set(),2447 schedNoPush::scheduler::mRetry: Set(),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(),2457 built: false,2458 expecting: false,2459 running: false,2460 session: false,2461 up: false2462 },2463 "w2" ->2464 {2465 attached: Set(),2466 built: false,2467 expecting: false,2468 running: false,2469 session: true,2470 up: true2471 }2472 )2473}24742475[State 7]2476{2477 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2478 schedNoPush::scheduler::crashes: 2,2479 schedNoPush::scheduler::entry: [],2480 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2481 schedNoPush::scheduler::mAssigned: Set(),2482 schedNoPush::scheduler::mBuild: Set(),2483 schedNoPush::scheduler::mDone: Set(),2484 schedNoPush::scheduler::mExpect: Set(),2485 schedNoPush::scheduler::mResult: Set(),2486 schedNoPush::scheduler::mRetry: Set(),2487 schedNoPush::scheduler::mRevoke: Set(),2488 schedNoPush::scheduler::mSchedule: Set(),2489 schedNoPush::scheduler::published: 0,2490 schedNoPush::scheduler::publishedBy: Set(),2491 schedNoPush::scheduler::ws:2492 Map(2493 "w1" ->2494 {2495 attached: Set(),2496 built: false,2497 expecting: false,2498 running: false,2499 session: false,2500 up: false2501 },2502 "w2" ->2503 {2504 attached: Set("c1"),2505 built: false,2506 expecting: true,2507 running: true,2508 session: true,2509 up: true2510 }2511 )2512}25132514[violation] Found an issue (494ms at 22265 traces/second).2515Use --verbosity=3 to show executions.2516Use --seed=0xfaddbd7275338d74 --backend=rust to reproduce.2517error: Invariant violated2518An example execution:25192520[State 0]2521{2522 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),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(),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 1]2560{2561 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2562 schedNoReport::scheduler::crashes: 0,2563 schedNoReport::scheduler::entry: [],2564 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2565 schedNoReport::scheduler::mAssigned: Set(),2566 schedNoReport::scheduler::mBuild: Set(),2567 schedNoReport::scheduler::mDone: Set(),2568 schedNoReport::scheduler::mExpect: Set(),2569 schedNoReport::scheduler::mResult: Set(),2570 schedNoReport::scheduler::mRetry: Set(),2571 schedNoReport::scheduler::mRevoke: Set(),2572 schedNoReport::scheduler::mSchedule: Set("c2"),2573 schedNoReport::scheduler::published: 0,2574 schedNoReport::scheduler::publishedBy: Set(),2575 schedNoReport::scheduler::ws:2576 Map(2577 "w1" ->2578 {2579 attached: Set(),2580 built: false,2581 expecting: false,2582 running: false,2583 session: true,2584 up: true2585 },2586 "w2" ->2587 {2588 attached: Set(),2589 built: false,2590 expecting: false,2591 running: false,2592 session: true,2593 up: true2594 }2595 )2596}25972598[State 2]2599{2600 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2601 schedNoReport::scheduler::crashes: 1,2602 schedNoReport::scheduler::entry: [],2603 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2604 schedNoReport::scheduler::mAssigned: Set(),2605 schedNoReport::scheduler::mBuild: Set(),2606 schedNoReport::scheduler::mDone: Set(),2607 schedNoReport::scheduler::mExpect: Set(),2608 schedNoReport::scheduler::mResult: Set(),2609 schedNoReport::scheduler::mRetry: Set(),2610 schedNoReport::scheduler::mRevoke: Set(),2611 schedNoReport::scheduler::mSchedule: Set("c2"),2612 schedNoReport::scheduler::published: 0,2613 schedNoReport::scheduler::publishedBy: Set(),2614 schedNoReport::scheduler::ws:2615 Map(2616 "w1" ->2617 {2618 attached: Set(),2619 built: false,2620 expecting: false,2621 running: false,2622 session: true,2623 up: true2624 },2625 "w2" ->2626 {2627 attached: Set(),2628 built: false,2629 expecting: false,2630 running: false,2631 session: false,2632 up: false2633 }2634 )2635}26362637[State 3]2638{2639 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2640 schedNoReport::scheduler::crashes: 1,2641 schedNoReport::scheduler::entry:2642 [{ followers: Set("c2"), leased: true, worker: "w1" }],2643 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2644 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2645 schedNoReport::scheduler::mBuild: Set(),2646 schedNoReport::scheduler::mDone: Set(),2647 schedNoReport::scheduler::mExpect: Set("w1"),2648 schedNoReport::scheduler::mResult: Set(),2649 schedNoReport::scheduler::mRetry: Set(),2650 schedNoReport::scheduler::mRevoke: Set(),2651 schedNoReport::scheduler::mSchedule: Set(),2652 schedNoReport::scheduler::published: 0,2653 schedNoReport::scheduler::publishedBy: Set(),2654 schedNoReport::scheduler::ws:2655 Map(2656 "w1" ->2657 {2658 attached: Set(),2659 built: false,2660 expecting: false,2661 running: false,2662 session: true,2663 up: true2664 },2665 "w2" ->2666 {2667 attached: Set(),2668 built: false,2669 expecting: false,2670 running: false,2671 session: false,2672 up: false2673 }2674 )2675}26762677[State 4]2678{2679 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2680 schedNoReport::scheduler::crashes: 1,2681 schedNoReport::scheduler::entry:2682 [{ followers: Set("c2"), leased: true, worker: "w1" }],2683 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2684 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),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(),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: true,2703 up: true2704 },2705 "w2" ->2706 {2707 attached: Set(),2708 built: false,2709 expecting: false,2710 running: false,2711 session: false,2712 up: false2713 }2714 )2715}27162717[State 5]2718{2719 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "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(),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: false2752 }2753 )2754}27552756[State 6]2757{2758 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "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("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: false2791 }2792 )2793}27942795[State 7]2796{2797 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "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("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 8]2835{2836 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2837 schedNoReport::scheduler::crashes: 2,2838 schedNoReport::scheduler::entry: [],2839 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2840 schedNoReport::scheduler::mAssigned: Set(),2841 schedNoReport::scheduler::mBuild: Set(),2842 schedNoReport::scheduler::mDone: Set(),2843 schedNoReport::scheduler::mExpect: Set(),2844 schedNoReport::scheduler::mResult: Set(),2845 schedNoReport::scheduler::mRetry: Set(),2846 schedNoReport::scheduler::mRevoke: Set(),2847 schedNoReport::scheduler::mSchedule: Set("c2"),2848 schedNoReport::scheduler::published: 0,2849 schedNoReport::scheduler::publishedBy: Set(),2850 schedNoReport::scheduler::ws:2851 Map(2852 "w1" ->2853 {2854 attached: Set(),2855 built: false,2856 expecting: true,2857 running: true,2858 session: true,2859 up: true2860 },2861 "w2" ->2862 {2863 attached: Set(),2864 built: false,2865 expecting: false,2866 running: false,2867 session: true,2868 up: true2869 }2870 )2871}28722873[State 9]2874{2875 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2876 schedNoReport::scheduler::crashes: 2,2877 schedNoReport::scheduler::entry:2878 [{ followers: Set("c2"), leased: true, worker: "w2" }],2879 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2880 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2881 schedNoReport::scheduler::mBuild: Set(),2882 schedNoReport::scheduler::mDone: Set(),2883 schedNoReport::scheduler::mExpect: Set("w2"),2884 schedNoReport::scheduler::mResult: Set(),2885 schedNoReport::scheduler::mRetry: Set(),2886 schedNoReport::scheduler::mRevoke: Set(),2887 schedNoReport::scheduler::mSchedule: Set(),2888 schedNoReport::scheduler::published: 0,2889 schedNoReport::scheduler::publishedBy: Set(),2890 schedNoReport::scheduler::ws:2891 Map(2892 "w1" ->2893 {2894 attached: Set(),2895 built: false,2896 expecting: true,2897 running: true,2898 session: true,2899 up: true2900 },2901 "w2" ->2902 {2903 attached: Set(),2904 built: false,2905 expecting: false,2906 running: false,2907 session: true,2908 up: true2909 }2910 )2911}29122913[State 10]2914{2915 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2916 schedNoReport::scheduler::crashes: 2,2917 schedNoReport::scheduler::entry:2918 [{ followers: Set("c2"), leased: true, worker: "w2" }],2919 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2920 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2921 schedNoReport::scheduler::mBuild: Set(),2922 schedNoReport::scheduler::mDone: Set(),2923 schedNoReport::scheduler::mExpect: Set(),2924 schedNoReport::scheduler::mResult: Set(),2925 schedNoReport::scheduler::mRetry: Set(),2926 schedNoReport::scheduler::mRevoke: Set(),2927 schedNoReport::scheduler::mSchedule: Set(),2928 schedNoReport::scheduler::published: 0,2929 schedNoReport::scheduler::publishedBy: Set(),2930 schedNoReport::scheduler::ws:2931 Map(2932 "w1" ->2933 {2934 attached: Set(),2935 built: false,2936 expecting: true,2937 running: true,2938 session: true,2939 up: true2940 },2941 "w2" ->2942 {2943 attached: Set(),2944 built: false,2945 expecting: true,2946 running: true,2947 session: true,2948 up: true2949 }2950 )2951}29522953[violation] Found an issue (561ms at 40916 traces/second).2954Use --verbosity=3 to show executions.2955Use --seed=0x424dab5f0b6bce7e --backend=rust to reproduce.2956error: Invariant violated2957An example execution:29582959[State 0]2960{2961 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2962 schedTerminal::scheduler::crashes: 0,2963 schedTerminal::scheduler::entry: [],2964 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2965 schedTerminal::scheduler::mAssigned: Set(),2966 schedTerminal::scheduler::mBuild: Set(),2967 schedTerminal::scheduler::mDone: Set(),2968 schedTerminal::scheduler::mExpect: Set(),2969 schedTerminal::scheduler::mResult: Set(),2970 schedTerminal::scheduler::mRetry: Set(),2971 schedTerminal::scheduler::mRevoke: Set(),2972 schedTerminal::scheduler::mSchedule: Set(),2973 schedTerminal::scheduler::published: 0,2974 schedTerminal::scheduler::publishedBy: Set(),2975 schedTerminal::scheduler::ws:2976 Map(2977 "w1" ->2978 {2979 attached: Set(),2980 built: false,2981 expecting: false,2982 running: false,2983 session: true,2984 up: true2985 },2986 "w2" ->2987 {2988 attached: Set(),2989 built: false,2990 expecting: false,2991 running: false,2992 session: true,2993 up: true2994 }2995 )2996}29972998[State 1]2999{3000 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3001 schedTerminal::scheduler::crashes: 1,3002 schedTerminal::scheduler::entry: [],3003 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3004 schedTerminal::scheduler::mAssigned: Set(),3005 schedTerminal::scheduler::mBuild: Set(),3006 schedTerminal::scheduler::mDone: Set(),3007 schedTerminal::scheduler::mExpect: Set(),3008 schedTerminal::scheduler::mResult: Set(),3009 schedTerminal::scheduler::mRetry: Set(),3010 schedTerminal::scheduler::mRevoke: Set(),3011 schedTerminal::scheduler::mSchedule: Set(),3012 schedTerminal::scheduler::published: 0,3013 schedTerminal::scheduler::publishedBy: Set(),3014 schedTerminal::scheduler::ws:3015 Map(3016 "w1" ->3017 {3018 attached: Set(),3019 built: false,3020 expecting: false,3021 running: false,3022 session: false,3023 up: true3024 },3025 "w2" ->3026 {3027 attached: Set(),3028 built: false,3029 expecting: false,3030 running: false,3031 session: false,3032 up: true3033 }3034 )3035}30363037[State 2]3038{3039 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3040 schedTerminal::scheduler::crashes: 1,3041 schedTerminal::scheduler::entry: [],3042 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3043 schedTerminal::scheduler::mAssigned: Set(),3044 schedTerminal::scheduler::mBuild: Set(),3045 schedTerminal::scheduler::mDone: Set(),3046 schedTerminal::scheduler::mExpect: Set(),3047 schedTerminal::scheduler::mResult: Set(),3048 schedTerminal::scheduler::mRetry: Set(),3049 schedTerminal::scheduler::mRevoke: Set(),3050 schedTerminal::scheduler::mSchedule: Set("c2"),3051 schedTerminal::scheduler::published: 0,3052 schedTerminal::scheduler::publishedBy: Set(),3053 schedTerminal::scheduler::ws:3054 Map(3055 "w1" ->3056 {3057 attached: Set(),3058 built: false,3059 expecting: false,3060 running: false,3061 session: false,3062 up: true3063 },3064 "w2" ->3065 {3066 attached: Set(),3067 built: false,3068 expecting: false,3069 running: false,3070 session: false,3071 up: true3072 }3073 )3074}30753076[State 3]3077{3078 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3079 schedTerminal::scheduler::crashes: 1,3080 schedTerminal::scheduler::entry: [],3081 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3082 schedTerminal::scheduler::mAssigned: Set(),3083 schedTerminal::scheduler::mBuild: Set(),3084 schedTerminal::scheduler::mDone: Set(),3085 schedTerminal::scheduler::mExpect: Set(),3086 schedTerminal::scheduler::mResult: Set(),3087 schedTerminal::scheduler::mRetry: Set(),3088 schedTerminal::scheduler::mRevoke: Set(),3089 schedTerminal::scheduler::mSchedule: Set(),3090 schedTerminal::scheduler::published: 0,3091 schedTerminal::scheduler::publishedBy: Set(),3092 schedTerminal::scheduler::ws:3093 Map(3094 "w1" ->3095 {3096 attached: Set(),3097 built: false,3098 expecting: false,3099 running: false,3100 session: false,3101 up: true3102 },3103 "w2" ->3104 {3105 attached: Set(),3106 built: false,3107 expecting: false,3108 running: false,3109 session: false,3110 up: true3111 }3112 )3113}31143115[violation] Found an issue (173ms at 5566 traces/second).3116Use --verbosity=3 to show executions.3117Use --seed=0x13161ebd5019e4d2 --backend=rust to reproduce.3118error: Invariant violated3119An example execution:31203121[State 0]3122{3123 pushFixed::push::byPath: Map(),3124 pushFixed::push::inflight: Set(),3125 pushFixed::push::left: Map(),3126 pushFixed::push::sent: Map()3127}31283129[State 1]3130{3131 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3132 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3133 pushFixed::push::left: Map(1 -> 2),3134 pushFixed::push::sent: Map(1 -> Set("a", "b"))3135}31363137[State 2]3138{3139 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3140 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (3, "a"), (3, "b")),3141 pushFixed::push::left: Map(1 -> 2, 3 -> 2),3142 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3143}31443145[State 3]3146{3147 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3148 pushFixed::push::inflight:3149 Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),3150 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 2),3151 pushFixed::push::sent:3152 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3153}31543155[State 4]3156{3157 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3158 pushFixed::push::inflight:3159 Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a")),3160 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 1),3161 pushFixed::push::sent:3162 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3163}31643165[State 5]3166{3167 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3168 pushFixed::push::inflight: Set((1, "a"), (2, "a"), (2, "b"), (3, "a")),3169 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 1),3170 pushFixed::push::sent:3171 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3172}31733174[State 6]3175{3176 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3177 pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "a")),3178 pushFixed::push::left: Map(1 -> 0, 2 -> 2, 3 -> 1),3179 pushFixed::push::sent:3180 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3181}31823183[State 7]3184{3185 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3186 pushFixed::push::inflight: Set((2, "a"), (3, "a")),3187 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 1),3188 pushFixed::push::sent:3189 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3190}31913192[State 8]3193{3194 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3195 pushFixed::push::inflight: Set((3, "a")),3196 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 1),3197 pushFixed::push::sent:3198 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3199}32003201[State 9]3202{3203 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3204 pushFixed::push::inflight: Set(),3205 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3206 pushFixed::push::sent:3207 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3208}32093210[ok] No violation found (136ms at 147059 traces/second).3211Trace length statistics: max=10, min=7, average=8.043212You may increase --max-samples and --max-steps.3213Use --verbosity to produce more (or less) output.3214Use --seed=0x29fc2ac1131c035f --backend=rust to reproduce.