nix-grpc-store-spec
checks.aarch64-darwin.spec
· build #663
· raw
1tribuchet: building on mac022An 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(),133 schedFixed::scheduler::mRevoke: Set(),134 schedFixed::scheduler::mSchedule: Set("c1"),135 schedFixed::scheduler::published: 0,136 schedFixed::scheduler::publishedBy: Set(),137 schedFixed::scheduler::ws:138 Map(139 "w1" ->140 {141 attached: Set(),142 built: false,143 expecting: false,144 running: false,145 session: false,146 up: true147 },148 "w2" ->149 {150 attached: Set(),151 built: false,152 expecting: false,153 running: false,154 session: false,155 up: true156 }157 )158}159160[State 4]161{162 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),163 schedFixed::scheduler::crashes: 1,164 schedFixed::scheduler::entry: [],165 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),166 schedFixed::scheduler::mAssigned: Set(),167 schedFixed::scheduler::mBuild: Set(),168 schedFixed::scheduler::mDone: Set(),169 schedFixed::scheduler::mExpect: Set(),170 schedFixed::scheduler::mResult: Set(),171 schedFixed::scheduler::mRetry: Set(),172 schedFixed::scheduler::mRevoke: Set(),173 schedFixed::scheduler::mSchedule: Set("c1"),174 schedFixed::scheduler::published: 0,175 schedFixed::scheduler::publishedBy: Set(),176 schedFixed::scheduler::ws:177 Map(178 "w1" ->179 {180 attached: Set(),181 built: false,182 expecting: false,183 running: false,184 session: true,185 up: true186 },187 "w2" ->188 {189 attached: Set(),190 built: false,191 expecting: false,192 running: false,193 session: false,194 up: true195 }196 )197}198199[State 5]200{201 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),202 schedFixed::scheduler::crashes: 1,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", "c2"),213 schedFixed::scheduler::published: 0,214 schedFixed::scheduler::publishedBy: Set(),215 schedFixed::scheduler::ws:216 Map(217 "w1" ->218 {219 attached: Set(),220 built: false,221 expecting: false,222 running: false,223 session: true,224 up: true225 },226 "w2" ->227 {228 attached: Set(),229 built: false,230 expecting: false,231 running: false,232 session: false,233 up: true234 }235 )236}237238[State 6]239{240 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),241 schedFixed::scheduler::crashes: 1,242 schedFixed::scheduler::entry:243 [{ followers: Set("c1"), leased: true, worker: "w1" }],244 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),245 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),246 schedFixed::scheduler::mBuild: Set(),247 schedFixed::scheduler::mDone: Set(),248 schedFixed::scheduler::mExpect: Set("w1"),249 schedFixed::scheduler::mResult: Set(),250 schedFixed::scheduler::mRetry: Set(),251 schedFixed::scheduler::mRevoke: Set(),252 schedFixed::scheduler::mSchedule: Set("c2"),253 schedFixed::scheduler::published: 0,254 schedFixed::scheduler::publishedBy: Set(),255 schedFixed::scheduler::ws:256 Map(257 "w1" ->258 {259 attached: Set(),260 built: false,261 expecting: false,262 running: false,263 session: true,264 up: true265 },266 "w2" ->267 {268 attached: Set(),269 built: false,270 expecting: false,271 running: false,272 session: false,273 up: true274 }275 )276}277278[State 7]279{280 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),281 schedFixed::scheduler::crashes: 1,282 schedFixed::scheduler::entry:283 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],284 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),285 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),286 schedFixed::scheduler::mBuild: Set(),287 schedFixed::scheduler::mDone: Set(),288 schedFixed::scheduler::mExpect: Set("w1"),289 schedFixed::scheduler::mResult: Set(),290 schedFixed::scheduler::mRetry: Set(),291 schedFixed::scheduler::mRevoke: Set(),292 schedFixed::scheduler::mSchedule: Set(),293 schedFixed::scheduler::published: 0,294 schedFixed::scheduler::publishedBy: Set(),295 schedFixed::scheduler::ws:296 Map(297 "w1" ->298 {299 attached: Set(),300 built: false,301 expecting: false,302 running: false,303 session: true,304 up: true305 },306 "w2" ->307 {308 attached: Set(),309 built: false,310 expecting: false,311 running: false,312 session: false,313 up: true314 }315 )316}317318[State 8]319{320 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),321 schedFixed::scheduler::crashes: 1,322 schedFixed::scheduler::entry:323 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],324 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),325 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),326 schedFixed::scheduler::mBuild: Set(("c1", "w1")),327 schedFixed::scheduler::mDone: Set(),328 schedFixed::scheduler::mExpect: Set("w1"),329 schedFixed::scheduler::mResult: Set(),330 schedFixed::scheduler::mRetry: Set(),331 schedFixed::scheduler::mRevoke: Set(),332 schedFixed::scheduler::mSchedule: Set(),333 schedFixed::scheduler::published: 0,334 schedFixed::scheduler::publishedBy: Set(),335 schedFixed::scheduler::ws:336 Map(337 "w1" ->338 {339 attached: Set(),340 built: false,341 expecting: false,342 running: false,343 session: true,344 up: true345 },346 "w2" ->347 {348 attached: Set(),349 built: false,350 expecting: false,351 running: false,352 session: false,353 up: true354 }355 )356}357358[State 9]359{360 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),361 schedFixed::scheduler::crashes: 2,362 schedFixed::scheduler::entry:363 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],364 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),365 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),366 schedFixed::scheduler::mBuild: Set(("c1", "w1")),367 schedFixed::scheduler::mDone: Set(),368 schedFixed::scheduler::mExpect: Set(),369 schedFixed::scheduler::mResult: Set(),370 schedFixed::scheduler::mRetry: Set(),371 schedFixed::scheduler::mRevoke: Set(),372 schedFixed::scheduler::mSchedule: Set(),373 schedFixed::scheduler::published: 0,374 schedFixed::scheduler::publishedBy: Set(),375 schedFixed::scheduler::ws:376 Map(377 "w1" ->378 {379 attached: Set(),380 built: false,381 expecting: false,382 running: false,383 session: false,384 up: false385 },386 "w2" ->387 {388 attached: Set(),389 built: false,390 expecting: false,391 running: false,392 session: false,393 up: true394 }395 )396}397398[State 10]399{400 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),401 schedFixed::scheduler::crashes: 2,402 schedFixed::scheduler::entry:403 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],404 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),405 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),406 schedFixed::scheduler::mBuild: Set(("c1", "w1")),407 schedFixed::scheduler::mDone: Set(),408 schedFixed::scheduler::mExpect: Set(),409 schedFixed::scheduler::mResult: Set(),410 schedFixed::scheduler::mRetry: Set(),411 schedFixed::scheduler::mRevoke: Set(),412 schedFixed::scheduler::mSchedule: Set(),413 schedFixed::scheduler::published: 0,414 schedFixed::scheduler::publishedBy: Set(),415 schedFixed::scheduler::ws:416 Map(417 "w1" ->418 {419 attached: Set(),420 built: false,421 expecting: false,422 running: false,423 session: false,424 up: false425 },426 "w2" ->427 {428 attached: Set(),429 built: false,430 expecting: false,431 running: false,432 session: true,433 up: true434 }435 )436}437438[State 11]439{440 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),441 schedFixed::scheduler::crashes: 2,442 schedFixed::scheduler::entry: [],443 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),444 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),445 schedFixed::scheduler::mBuild: Set(("c1", "w1")),446 schedFixed::scheduler::mDone: Set(),447 schedFixed::scheduler::mExpect: Set(),448 schedFixed::scheduler::mResult: Set(),449 schedFixed::scheduler::mRetry: Set("c1", "c2"),450 schedFixed::scheduler::mRevoke: Set(),451 schedFixed::scheduler::mSchedule: Set(),452 schedFixed::scheduler::published: 0,453 schedFixed::scheduler::publishedBy: Set(),454 schedFixed::scheduler::ws:455 Map(456 "w1" ->457 {458 attached: Set(),459 built: false,460 expecting: false,461 running: false,462 session: false,463 up: false464 },465 "w2" ->466 {467 attached: Set(),468 built: false,469 expecting: false,470 running: false,471 session: true,472 up: true473 }474 )475}476477[State 12]478{479 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),480 schedFixed::scheduler::crashes: 2,481 schedFixed::scheduler::entry: [],482 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),483 schedFixed::scheduler::mAssigned: Set(),484 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),485 schedFixed::scheduler::mDone: Set(),486 schedFixed::scheduler::mExpect: Set(),487 schedFixed::scheduler::mResult: Set(),488 schedFixed::scheduler::mRetry: Set("c1", "c2"),489 schedFixed::scheduler::mRevoke: Set(),490 schedFixed::scheduler::mSchedule: Set(),491 schedFixed::scheduler::published: 0,492 schedFixed::scheduler::publishedBy: Set(),493 schedFixed::scheduler::ws:494 Map(495 "w1" ->496 {497 attached: Set(),498 built: false,499 expecting: false,500 running: false,501 session: false,502 up: false503 },504 "w2" ->505 {506 attached: Set(),507 built: false,508 expecting: false,509 running: false,510 session: true,511 up: true512 }513 )514}515516[State 13]517{518 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),519 schedFixed::scheduler::crashes: 2,520 schedFixed::scheduler::entry: [],521 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),522 schedFixed::scheduler::mAssigned: Set(),523 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),524 schedFixed::scheduler::mDone: Set(),525 schedFixed::scheduler::mExpect: Set(),526 schedFixed::scheduler::mResult: Set(),527 schedFixed::scheduler::mRetry: Set("c2"),528 schedFixed::scheduler::mRevoke: Set(),529 schedFixed::scheduler::mSchedule: Set("c1"),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: false,541 up: false542 },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" -> CSent("w1")),558 schedFixed::scheduler::crashes: 2,559 schedFixed::scheduler::entry: [],560 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),561 schedFixed::scheduler::mAssigned: Set(),562 schedFixed::scheduler::mBuild: Set(("c1", "w1")),563 schedFixed::scheduler::mDone: Set(),564 schedFixed::scheduler::mExpect: Set(),565 schedFixed::scheduler::mResult: Set(),566 schedFixed::scheduler::mRetry: Set("c2"),567 schedFixed::scheduler::mRevoke: Set(),568 schedFixed::scheduler::mSchedule: Set("c1"),569 schedFixed::scheduler::published: 0,570 schedFixed::scheduler::publishedBy: Set(),571 schedFixed::scheduler::ws:572 Map(573 "w1" ->574 {575 attached: Set(),576 built: false,577 expecting: false,578 running: false,579 session: false,580 up: false581 },582 "w2" ->583 {584 attached: Set(),585 built: false,586 expecting: false,587 running: false,588 session: true,589 up: true590 }591 )592}593594[State 15]595{596 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),597 schedFixed::scheduler::crashes: 2,598 schedFixed::scheduler::entry:599 [{ followers: Set("c1"), leased: true, worker: "w2" }],600 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),601 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),602 schedFixed::scheduler::mBuild: Set(("c1", "w1")),603 schedFixed::scheduler::mDone: Set(),604 schedFixed::scheduler::mExpect: Set("w2"),605 schedFixed::scheduler::mResult: Set(),606 schedFixed::scheduler::mRetry: Set("c2"),607 schedFixed::scheduler::mRevoke: Set(),608 schedFixed::scheduler::mSchedule: Set(),609 schedFixed::scheduler::published: 0,610 schedFixed::scheduler::publishedBy: Set(),611 schedFixed::scheduler::ws:612 Map(613 "w1" ->614 {615 attached: Set(),616 built: false,617 expecting: false,618 running: false,619 session: false,620 up: false621 },622 "w2" ->623 {624 attached: Set(),625 built: false,626 expecting: false,627 running: false,628 session: true,629 up: true630 }631 )632}633634[State 16]635{636 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),637 schedFixed::scheduler::crashes: 2,638 schedFixed::scheduler::entry:639 [{ followers: Set("c1"), leased: true, worker: "w2" }],640 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),641 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),642 schedFixed::scheduler::mBuild: Set(),643 schedFixed::scheduler::mDone: Set(),644 schedFixed::scheduler::mExpect: Set("w2"),645 schedFixed::scheduler::mResult: Set(),646 schedFixed::scheduler::mRetry: Set("c1", "c2"),647 schedFixed::scheduler::mRevoke: Set(),648 schedFixed::scheduler::mSchedule: Set(),649 schedFixed::scheduler::published: 0,650 schedFixed::scheduler::publishedBy: Set(),651 schedFixed::scheduler::ws:652 Map(653 "w1" ->654 {655 attached: Set(),656 built: false,657 expecting: false,658 running: false,659 session: false,660 up: false661 },662 "w2" ->663 {664 attached: Set(),665 built: false,666 expecting: false,667 running: false,668 session: true,669 up: true670 }671 )672}673674[State 17]675{676 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),677 schedFixed::scheduler::crashes: 2,678 schedFixed::scheduler::entry:679 [{ followers: Set("c1"), leased: true, worker: "w2" }],680 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),681 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),682 schedFixed::scheduler::mBuild: Set(),683 schedFixed::scheduler::mDone: Set(),684 schedFixed::scheduler::mExpect: Set("w2"),685 schedFixed::scheduler::mResult: Set(),686 schedFixed::scheduler::mRetry: Set("c1", "c2"),687 schedFixed::scheduler::mRevoke: Set(),688 schedFixed::scheduler::mSchedule: Set(),689 schedFixed::scheduler::published: 0,690 schedFixed::scheduler::publishedBy: Set(),691 schedFixed::scheduler::ws:692 Map(693 "w1" ->694 {695 attached: Set(),696 built: false,697 expecting: false,698 running: false,699 session: true,700 up: true701 },702 "w2" ->703 {704 attached: Set(),705 built: false,706 expecting: false,707 running: false,708 session: true,709 up: true710 }711 )712}713714[State 18]715{716 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),717 schedFixed::scheduler::crashes: 2,718 schedFixed::scheduler::entry:719 [{ followers: Set("c1"), leased: true, worker: "w2" }],720 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),721 schedFixed::scheduler::mAssigned: Set(),722 schedFixed::scheduler::mBuild: Set(),723 schedFixed::scheduler::mDone: Set(),724 schedFixed::scheduler::mExpect: Set("w2"),725 schedFixed::scheduler::mResult: Set(),726 schedFixed::scheduler::mRetry: Set("c2"),727 schedFixed::scheduler::mRevoke: Set(),728 schedFixed::scheduler::mSchedule: Set("c1"),729 schedFixed::scheduler::published: 0,730 schedFixed::scheduler::publishedBy: Set(),731 schedFixed::scheduler::ws:732 Map(733 "w1" ->734 {735 attached: Set(),736 built: false,737 expecting: false,738 running: false,739 session: true,740 up: true741 },742 "w2" ->743 {744 attached: Set(),745 built: false,746 expecting: false,747 running: false,748 session: true,749 up: true750 }751 )752}753754[State 19]755{756 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),757 schedFixed::scheduler::crashes: 2,758 schedFixed::scheduler::entry:759 [{ followers: Set("c1"), leased: true, worker: "w2" }],760 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),761 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),762 schedFixed::scheduler::mBuild: Set(),763 schedFixed::scheduler::mDone: Set(),764 schedFixed::scheduler::mExpect: Set("w2"),765 schedFixed::scheduler::mResult: Set(),766 schedFixed::scheduler::mRetry: Set("c2"),767 schedFixed::scheduler::mRevoke: Set(),768 schedFixed::scheduler::mSchedule: Set(),769 schedFixed::scheduler::published: 0,770 schedFixed::scheduler::publishedBy: Set(),771 schedFixed::scheduler::ws:772 Map(773 "w1" ->774 {775 attached: Set(),776 built: false,777 expecting: false,778 running: false,779 session: true,780 up: true781 },782 "w2" ->783 {784 attached: Set(),785 built: false,786 expecting: false,787 running: false,788 session: true,789 up: true790 }791 )792}793794[State 20]795{796 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),797 schedFixed::scheduler::crashes: 2,798 schedFixed::scheduler::entry:799 [{ followers: Set("c1"), leased: true, worker: "w2" }],800 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),801 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),802 schedFixed::scheduler::mBuild: Set(),803 schedFixed::scheduler::mDone: Set(),804 schedFixed::scheduler::mExpect: Set(),805 schedFixed::scheduler::mResult: Set(),806 schedFixed::scheduler::mRetry: Set("c2"),807 schedFixed::scheduler::mRevoke: Set(),808 schedFixed::scheduler::mSchedule: Set(),809 schedFixed::scheduler::published: 0,810 schedFixed::scheduler::publishedBy: Set(),811 schedFixed::scheduler::ws:812 Map(813 "w1" ->814 {815 attached: Set(),816 built: false,817 expecting: false,818 running: false,819 session: true,820 up: true821 },822 "w2" ->823 {824 attached: Set(),825 built: false,826 expecting: true,827 running: true,828 session: true,829 up: true830 }831 )832}833834[State 21]835{836 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),837 schedFixed::scheduler::crashes: 2,838 schedFixed::scheduler::entry:839 [{ followers: Set("c1"), leased: true, worker: "w2" }],840 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),841 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),842 schedFixed::scheduler::mBuild: Set(),843 schedFixed::scheduler::mDone: Set(),844 schedFixed::scheduler::mExpect: Set(),845 schedFixed::scheduler::mResult: Set(),846 schedFixed::scheduler::mRetry: Set(),847 schedFixed::scheduler::mRevoke: Set(),848 schedFixed::scheduler::mSchedule: Set("c2"),849 schedFixed::scheduler::published: 0,850 schedFixed::scheduler::publishedBy: Set(),851 schedFixed::scheduler::ws:852 Map(853 "w1" ->854 {855 attached: Set(),856 built: false,857 expecting: false,858 running: false,859 session: true,860 up: true861 },862 "w2" ->863 {864 attached: Set(),865 built: false,866 expecting: true,867 running: true,868 session: true,869 up: true870 }871 )872}873874[State 22]875{876 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),877 schedFixed::scheduler::crashes: 2,878 schedFixed::scheduler::entry:879 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],880 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),881 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),882 schedFixed::scheduler::mBuild: Set(),883 schedFixed::scheduler::mDone: Set(),884 schedFixed::scheduler::mExpect: Set(),885 schedFixed::scheduler::mResult: Set(),886 schedFixed::scheduler::mRetry: Set(),887 schedFixed::scheduler::mRevoke: Set(),888 schedFixed::scheduler::mSchedule: Set(),889 schedFixed::scheduler::published: 0,890 schedFixed::scheduler::publishedBy: Set(),891 schedFixed::scheduler::ws:892 Map(893 "w1" ->894 {895 attached: Set(),896 built: false,897 expecting: false,898 running: false,899 session: true,900 up: true901 },902 "w2" ->903 {904 attached: Set(),905 built: false,906 expecting: true,907 running: true,908 session: true,909 up: true910 }911 )912}913914[State 23]915{916 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),917 schedFixed::scheduler::crashes: 2,918 schedFixed::scheduler::entry:919 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],920 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),921 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),922 schedFixed::scheduler::mBuild: Set(),923 schedFixed::scheduler::mDone: Set("w2"),924 schedFixed::scheduler::mExpect: Set(),925 schedFixed::scheduler::mResult: Set(),926 schedFixed::scheduler::mRetry: Set(),927 schedFixed::scheduler::mRevoke: Set(),928 schedFixed::scheduler::mSchedule: Set(),929 schedFixed::scheduler::published: 1,930 schedFixed::scheduler::publishedBy: Set("w2"),931 schedFixed::scheduler::ws:932 Map(933 "w1" ->934 {935 attached: Set(),936 built: false,937 expecting: false,938 running: false,939 session: true,940 up: true941 },942 "w2" ->943 {944 attached: Set(),945 built: true,946 expecting: false,947 running: false,948 session: true,949 up: true950 }951 )952}953954[State 24]955{956 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),957 schedFixed::scheduler::crashes: 2,958 schedFixed::scheduler::entry: [],959 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),960 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),961 schedFixed::scheduler::mBuild: Set(),962 schedFixed::scheduler::mDone: Set(),963 schedFixed::scheduler::mExpect: Set(),964 schedFixed::scheduler::mResult: Set(),965 schedFixed::scheduler::mRetry: Set(),966 schedFixed::scheduler::mRevoke: Set(),967 schedFixed::scheduler::mSchedule: Set(),968 schedFixed::scheduler::published: 1,969 schedFixed::scheduler::publishedBy: Set("w2"),970 schedFixed::scheduler::ws:971 Map(972 "w1" ->973 {974 attached: Set(),975 built: false,976 expecting: false,977 running: false,978 session: true,979 up: true980 },981 "w2" ->982 {983 attached: Set(),984 built: true,985 expecting: false,986 running: false,987 session: true,988 up: true989 }990 )991}992993[State 25]994{995 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),996 schedFixed::scheduler::crashes: 2,997 schedFixed::scheduler::entry: [],998 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),999 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),1000 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1001 schedFixed::scheduler::mDone: Set(),1002 schedFixed::scheduler::mExpect: Set(),1003 schedFixed::scheduler::mResult: Set(),1004 schedFixed::scheduler::mRetry: Set(),1005 schedFixed::scheduler::mRevoke: Set(),1006 schedFixed::scheduler::mSchedule: Set(),1007 schedFixed::scheduler::published: 1,1008 schedFixed::scheduler::publishedBy: Set("w2"),1009 schedFixed::scheduler::ws:1010 Map(1011 "w1" ->1012 {1013 attached: Set(),1014 built: false,1015 expecting: false,1016 running: false,1017 session: true,1018 up: true1019 },1020 "w2" ->1021 {1022 attached: Set(),1023 built: true,1024 expecting: false,1025 running: false,1026 session: true,1027 up: true1028 }1029 )1030}10311032[State 26]1033{1034 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),1035 schedFixed::scheduler::crashes: 2,1036 schedFixed::scheduler::entry: [],1037 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1038 schedFixed::scheduler::mAssigned: Set(),1039 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w2")),1040 schedFixed::scheduler::mDone: Set(),1041 schedFixed::scheduler::mExpect: Set(),1042 schedFixed::scheduler::mResult: Set(),1043 schedFixed::scheduler::mRetry: Set(),1044 schedFixed::scheduler::mRevoke: Set(),1045 schedFixed::scheduler::mSchedule: Set(),1046 schedFixed::scheduler::published: 1,1047 schedFixed::scheduler::publishedBy: Set("w2"),1048 schedFixed::scheduler::ws:1049 Map(1050 "w1" ->1051 {1052 attached: Set(),1053 built: false,1054 expecting: false,1055 running: false,1056 session: true,1057 up: true1058 },1059 "w2" ->1060 {1061 attached: Set(),1062 built: true,1063 expecting: false,1064 running: false,1065 session: true,1066 up: true1067 }1068 )1069}10701071[State 27]1072{1073 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),1074 schedFixed::scheduler::crashes: 2,1075 schedFixed::scheduler::entry: [],1076 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1077 schedFixed::scheduler::mAssigned: Set(),1078 schedFixed::scheduler::mBuild: Set(("c1", "w2")),1079 schedFixed::scheduler::mDone: Set(),1080 schedFixed::scheduler::mExpect: Set(),1081 schedFixed::scheduler::mResult: Set("c2"),1082 schedFixed::scheduler::mRetry: Set(),1083 schedFixed::scheduler::mRevoke: Set(),1084 schedFixed::scheduler::mSchedule: Set(),1085 schedFixed::scheduler::published: 1,1086 schedFixed::scheduler::publishedBy: Set("w2"),1087 schedFixed::scheduler::ws:1088 Map(1089 "w1" ->1090 {1091 attached: Set(),1092 built: false,1093 expecting: false,1094 running: false,1095 session: true,1096 up: true1097 },1098 "w2" ->1099 {1100 attached: Set(),1101 built: true,1102 expecting: false,1103 running: false,1104 session: true,1105 up: true1106 }1107 )1108}11091110[State 28]1111{1112 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),1113 schedFixed::scheduler::crashes: 2,1114 schedFixed::scheduler::entry: [],1115 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1116 schedFixed::scheduler::mAssigned: Set(),1117 schedFixed::scheduler::mBuild: Set(),1118 schedFixed::scheduler::mDone: Set(),1119 schedFixed::scheduler::mExpect: Set(),1120 schedFixed::scheduler::mResult: Set("c1", "c2"),1121 schedFixed::scheduler::mRetry: Set(),1122 schedFixed::scheduler::mRevoke: Set(),1123 schedFixed::scheduler::mSchedule: Set(),1124 schedFixed::scheduler::published: 1,1125 schedFixed::scheduler::publishedBy: Set("w2"),1126 schedFixed::scheduler::ws:1127 Map(1128 "w1" ->1129 {1130 attached: Set(),1131 built: false,1132 expecting: false,1133 running: false,1134 session: true,1135 up: true1136 },1137 "w2" ->1138 {1139 attached: Set(),1140 built: true,1141 expecting: false,1142 running: false,1143 session: true,1144 up: true1145 }1146 )1147}11481149[State 29]1150{1151 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w2")),1152 schedFixed::scheduler::crashes: 2,1153 schedFixed::scheduler::entry: [],1154 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1155 schedFixed::scheduler::mAssigned: Set(),1156 schedFixed::scheduler::mBuild: Set(),1157 schedFixed::scheduler::mDone: Set(),1158 schedFixed::scheduler::mExpect: Set(),1159 schedFixed::scheduler::mResult: Set("c2"),1160 schedFixed::scheduler::mRetry: Set(),1161 schedFixed::scheduler::mRevoke: Set(),1162 schedFixed::scheduler::mSchedule: Set(),1163 schedFixed::scheduler::published: 1,1164 schedFixed::scheduler::publishedBy: Set("w2"),1165 schedFixed::scheduler::ws:1166 Map(1167 "w1" ->1168 {1169 attached: Set(),1170 built: false,1171 expecting: false,1172 running: false,1173 session: true,1174 up: true1175 },1176 "w2" ->1177 {1178 attached: Set(),1179 built: true,1180 expecting: false,1181 running: false,1182 session: true,1183 up: true1184 }1185 )1186}11871188[State 30]1189{1190 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),1191 schedFixed::scheduler::crashes: 2,1192 schedFixed::scheduler::entry: [],1193 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1194 schedFixed::scheduler::mAssigned: Set(),1195 schedFixed::scheduler::mBuild: Set(),1196 schedFixed::scheduler::mDone: Set(),1197 schedFixed::scheduler::mExpect: Set(),1198 schedFixed::scheduler::mResult: Set(),1199 schedFixed::scheduler::mRetry: Set(),1200 schedFixed::scheduler::mRevoke: Set(),1201 schedFixed::scheduler::mSchedule: Set(),1202 schedFixed::scheduler::published: 1,1203 schedFixed::scheduler::publishedBy: Set("w2"),1204 schedFixed::scheduler::ws:1205 Map(1206 "w1" ->1207 {1208 attached: Set(),1209 built: false,1210 expecting: false,1211 running: false,1212 session: true,1213 up: true1214 },1215 "w2" ->1216 {1217 attached: Set(),1218 built: true,1219 expecting: false,1220 running: false,1221 session: true,1222 up: true1223 }1224 )1225}12261227[ok] No violation found (16497ms at 1819 traces/second).1228Trace length statistics: max=31, min=15, average=18.861229You may increase --max-samples and --max-steps.1230Use --verbosity to produce more (or less) output.1231Use --seed=0xa8351d890a154969 --backend=rust to reproduce.1232An example execution:12331234[State 0]1235{1236 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1237 schedNoRevoke::scheduler::crashes: 0,1238 schedNoRevoke::scheduler::entry: [],1239 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1240 schedNoRevoke::scheduler::mAssigned: Set(),1241 schedNoRevoke::scheduler::mBuild: Set(),1242 schedNoRevoke::scheduler::mDone: Set(),1243 schedNoRevoke::scheduler::mExpect: Set(),1244 schedNoRevoke::scheduler::mResult: Set(),1245 schedNoRevoke::scheduler::mRetry: Set(),1246 schedNoRevoke::scheduler::mRevoke: Set(),1247 schedNoRevoke::scheduler::mSchedule: Set(),1248 schedNoRevoke::scheduler::published: 0,1249 schedNoRevoke::scheduler::publishedBy: Set(),1250 schedNoRevoke::scheduler::ws:1251 Map(1252 "w1" ->1253 {1254 attached: Set(),1255 built: false,1256 expecting: false,1257 running: false,1258 session: true,1259 up: true1260 },1261 "w2" ->1262 {1263 attached: Set(),1264 built: false,1265 expecting: false,1266 running: false,1267 session: true,1268 up: true1269 }1270 )1271}12721273[State 1]1274{1275 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1276 schedNoRevoke::scheduler::crashes: 0,1277 schedNoRevoke::scheduler::entry: [],1278 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1279 schedNoRevoke::scheduler::mAssigned: Set(),1280 schedNoRevoke::scheduler::mBuild: Set(),1281 schedNoRevoke::scheduler::mDone: Set(),1282 schedNoRevoke::scheduler::mExpect: Set(),1283 schedNoRevoke::scheduler::mResult: Set(),1284 schedNoRevoke::scheduler::mRetry: Set(),1285 schedNoRevoke::scheduler::mRevoke: Set(),1286 schedNoRevoke::scheduler::mSchedule: Set("c2"),1287 schedNoRevoke::scheduler::published: 0,1288 schedNoRevoke::scheduler::publishedBy: Set(),1289 schedNoRevoke::scheduler::ws:1290 Map(1291 "w1" ->1292 {1293 attached: Set(),1294 built: false,1295 expecting: false,1296 running: false,1297 session: true,1298 up: true1299 },1300 "w2" ->1301 {1302 attached: Set(),1303 built: false,1304 expecting: false,1305 running: false,1306 session: true,1307 up: true1308 }1309 )1310}13111312[State 2]1313{1314 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1315 schedNoRevoke::scheduler::crashes: 0,1316 schedNoRevoke::scheduler::entry:1317 [{ followers: Set("c2"), leased: true, worker: "w1" }],1318 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1319 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1320 schedNoRevoke::scheduler::mBuild: Set(),1321 schedNoRevoke::scheduler::mDone: Set(),1322 schedNoRevoke::scheduler::mExpect: Set("w1"),1323 schedNoRevoke::scheduler::mResult: Set(),1324 schedNoRevoke::scheduler::mRetry: Set(),1325 schedNoRevoke::scheduler::mRevoke: Set(),1326 schedNoRevoke::scheduler::mSchedule: Set(),1327 schedNoRevoke::scheduler::published: 0,1328 schedNoRevoke::scheduler::publishedBy: Set(),1329 schedNoRevoke::scheduler::ws:1330 Map(1331 "w1" ->1332 {1333 attached: Set(),1334 built: false,1335 expecting: false,1336 running: false,1337 session: true,1338 up: true1339 },1340 "w2" ->1341 {1342 attached: Set(),1343 built: false,1344 expecting: false,1345 running: false,1346 session: true,1347 up: true1348 }1349 )1350}13511352[State 3]1353{1354 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1355 schedNoRevoke::scheduler::crashes: 1,1356 schedNoRevoke::scheduler::entry:1357 [{ followers: Set("c2"), leased: true, worker: "w1" }],1358 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1359 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1360 schedNoRevoke::scheduler::mBuild: Set(),1361 schedNoRevoke::scheduler::mDone: Set(),1362 schedNoRevoke::scheduler::mExpect: Set("w1"),1363 schedNoRevoke::scheduler::mResult: Set(),1364 schedNoRevoke::scheduler::mRetry: Set(),1365 schedNoRevoke::scheduler::mRevoke: Set(),1366 schedNoRevoke::scheduler::mSchedule: Set(),1367 schedNoRevoke::scheduler::published: 0,1368 schedNoRevoke::scheduler::publishedBy: Set(),1369 schedNoRevoke::scheduler::ws:1370 Map(1371 "w1" ->1372 {1373 attached: Set(),1374 built: false,1375 expecting: false,1376 running: false,1377 session: true,1378 up: true1379 },1380 "w2" ->1381 {1382 attached: Set(),1383 built: false,1384 expecting: false,1385 running: false,1386 session: false,1387 up: false1388 }1389 )1390}13911392[State 4]1393{1394 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1395 schedNoRevoke::scheduler::crashes: 1,1396 schedNoRevoke::scheduler::entry:1397 [{ followers: Set("c2"), leased: true, worker: "w1" }],1398 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1399 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1400 schedNoRevoke::scheduler::mBuild: Set(),1401 schedNoRevoke::scheduler::mDone: Set(),1402 schedNoRevoke::scheduler::mExpect: Set(),1403 schedNoRevoke::scheduler::mResult: Set(),1404 schedNoRevoke::scheduler::mRetry: Set(),1405 schedNoRevoke::scheduler::mRevoke: Set(),1406 schedNoRevoke::scheduler::mSchedule: Set(),1407 schedNoRevoke::scheduler::published: 0,1408 schedNoRevoke::scheduler::publishedBy: Set(),1409 schedNoRevoke::scheduler::ws:1410 Map(1411 "w1" ->1412 {1413 attached: Set(),1414 built: false,1415 expecting: true,1416 running: true,1417 session: true,1418 up: true1419 },1420 "w2" ->1421 {1422 attached: Set(),1423 built: false,1424 expecting: false,1425 running: false,1426 session: false,1427 up: false1428 }1429 )1430}14311432[State 5]1433{1434 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1435 schedNoRevoke::scheduler::crashes: 2,1436 schedNoRevoke::scheduler::entry: [],1437 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1438 schedNoRevoke::scheduler::mAssigned: Set(),1439 schedNoRevoke::scheduler::mBuild: Set(),1440 schedNoRevoke::scheduler::mDone: Set(),1441 schedNoRevoke::scheduler::mExpect: Set(),1442 schedNoRevoke::scheduler::mResult: Set(),1443 schedNoRevoke::scheduler::mRetry: Set("c2"),1444 schedNoRevoke::scheduler::mRevoke: Set(),1445 schedNoRevoke::scheduler::mSchedule: Set(),1446 schedNoRevoke::scheduler::published: 0,1447 schedNoRevoke::scheduler::publishedBy: Set(),1448 schedNoRevoke::scheduler::ws:1449 Map(1450 "w1" ->1451 {1452 attached: Set(),1453 built: false,1454 expecting: true,1455 running: true,1456 session: false,1457 up: true1458 },1459 "w2" ->1460 {1461 attached: Set(),1462 built: false,1463 expecting: false,1464 running: false,1465 session: false,1466 up: false1467 }1468 )1469}14701471[State 6]1472{1473 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1474 schedNoRevoke::scheduler::crashes: 2,1475 schedNoRevoke::scheduler::entry: [],1476 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1477 schedNoRevoke::scheduler::mAssigned: Set(),1478 schedNoRevoke::scheduler::mBuild: Set(),1479 schedNoRevoke::scheduler::mDone: Set(),1480 schedNoRevoke::scheduler::mExpect: Set(),1481 schedNoRevoke::scheduler::mResult: Set(),1482 schedNoRevoke::scheduler::mRetry: Set("c2"),1483 schedNoRevoke::scheduler::mRevoke: Set(),1484 schedNoRevoke::scheduler::mSchedule: Set("c1"),1485 schedNoRevoke::scheduler::published: 0,1486 schedNoRevoke::scheduler::publishedBy: Set(),1487 schedNoRevoke::scheduler::ws:1488 Map(1489 "w1" ->1490 {1491 attached: Set(),1492 built: false,1493 expecting: true,1494 running: true,1495 session: false,1496 up: true1497 },1498 "w2" ->1499 {1500 attached: Set(),1501 built: false,1502 expecting: false,1503 running: false,1504 session: false,1505 up: false1506 }1507 )1508}15091510[State 7]1511{1512 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1513 schedNoRevoke::scheduler::crashes: 2,1514 schedNoRevoke::scheduler::entry: [],1515 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1516 schedNoRevoke::scheduler::mAssigned: Set(),1517 schedNoRevoke::scheduler::mBuild: Set(),1518 schedNoRevoke::scheduler::mDone: Set(),1519 schedNoRevoke::scheduler::mExpect: Set(),1520 schedNoRevoke::scheduler::mResult: Set(),1521 schedNoRevoke::scheduler::mRetry: Set("c2"),1522 schedNoRevoke::scheduler::mRevoke: Set(),1523 schedNoRevoke::scheduler::mSchedule: Set("c1"),1524 schedNoRevoke::scheduler::published: 0,1525 schedNoRevoke::scheduler::publishedBy: Set(),1526 schedNoRevoke::scheduler::ws:1527 Map(1528 "w1" ->1529 {1530 attached: Set(),1531 built: false,1532 expecting: true,1533 running: true,1534 session: false,1535 up: true1536 },1537 "w2" ->1538 {1539 attached: Set(),1540 built: false,1541 expecting: false,1542 running: false,1543 session: true,1544 up: true1545 }1546 )1547}15481549[State 8]1550{1551 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1552 schedNoRevoke::scheduler::crashes: 2,1553 schedNoRevoke::scheduler::entry:1554 [{ followers: Set("c1"), leased: true, worker: "w2" }],1555 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1556 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1557 schedNoRevoke::scheduler::mBuild: Set(),1558 schedNoRevoke::scheduler::mDone: Set(),1559 schedNoRevoke::scheduler::mExpect: Set("w2"),1560 schedNoRevoke::scheduler::mResult: Set(),1561 schedNoRevoke::scheduler::mRetry: Set("c2"),1562 schedNoRevoke::scheduler::mRevoke: Set(),1563 schedNoRevoke::scheduler::mSchedule: Set(),1564 schedNoRevoke::scheduler::published: 0,1565 schedNoRevoke::scheduler::publishedBy: Set(),1566 schedNoRevoke::scheduler::ws:1567 Map(1568 "w1" ->1569 {1570 attached: Set(),1571 built: false,1572 expecting: true,1573 running: true,1574 session: false,1575 up: true1576 },1577 "w2" ->1578 {1579 attached: Set(),1580 built: false,1581 expecting: false,1582 running: false,1583 session: true,1584 up: true1585 }1586 )1587}15881589[State 9]1590{1591 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1592 schedNoRevoke::scheduler::crashes: 2,1593 schedNoRevoke::scheduler::entry:1594 [{ followers: Set("c1"), leased: true, worker: "w2" }],1595 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1596 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1597 schedNoRevoke::scheduler::mBuild: Set(),1598 schedNoRevoke::scheduler::mDone: Set(),1599 schedNoRevoke::scheduler::mExpect: Set("w2"),1600 schedNoRevoke::scheduler::mResult: Set(),1601 schedNoRevoke::scheduler::mRetry: Set("c2"),1602 schedNoRevoke::scheduler::mRevoke: Set(),1603 schedNoRevoke::scheduler::mSchedule: Set(),1604 schedNoRevoke::scheduler::published: 0,1605 schedNoRevoke::scheduler::publishedBy: Set(),1606 schedNoRevoke::scheduler::ws:1607 Map(1608 "w1" ->1609 {1610 attached: Set(),1611 built: false,1612 expecting: true,1613 running: true,1614 session: true,1615 up: true1616 },1617 "w2" ->1618 {1619 attached: Set(),1620 built: false,1621 expecting: false,1622 running: false,1623 session: true,1624 up: true1625 }1626 )1627}16281629[State 10]1630{1631 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1632 schedNoRevoke::scheduler::crashes: 2,1633 schedNoRevoke::scheduler::entry:1634 [{ followers: Set("c1"), leased: true, worker: "w2" }],1635 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1636 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1637 schedNoRevoke::scheduler::mBuild: Set(),1638 schedNoRevoke::scheduler::mDone: Set(),1639 schedNoRevoke::scheduler::mExpect: Set(),1640 schedNoRevoke::scheduler::mResult: Set(),1641 schedNoRevoke::scheduler::mRetry: Set("c2"),1642 schedNoRevoke::scheduler::mRevoke: Set(),1643 schedNoRevoke::scheduler::mSchedule: Set(),1644 schedNoRevoke::scheduler::published: 0,1645 schedNoRevoke::scheduler::publishedBy: Set(),1646 schedNoRevoke::scheduler::ws:1647 Map(1648 "w1" ->1649 {1650 attached: Set(),1651 built: false,1652 expecting: true,1653 running: true,1654 session: true,1655 up: true1656 },1657 "w2" ->1658 {1659 attached: Set(),1660 built: false,1661 expecting: true,1662 running: true,1663 session: true,1664 up: true1665 }1666 )1667}16681669[violation] Found an issue (6890ms at 2176 traces/second).1670Use --verbosity=3 to show executions.1671Use --seed=0xd4a04c0a84f7434a --backend=rust to reproduce.1672error: Invariant violated1673An example execution:16741675[State 0]1676{1677 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1678 schedNoFence::scheduler::crashes: 0,1679 schedNoFence::scheduler::entry: [],1680 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1681 schedNoFence::scheduler::mAssigned: Set(),1682 schedNoFence::scheduler::mBuild: Set(),1683 schedNoFence::scheduler::mDone: Set(),1684 schedNoFence::scheduler::mExpect: Set(),1685 schedNoFence::scheduler::mResult: Set(),1686 schedNoFence::scheduler::mRetry: Set(),1687 schedNoFence::scheduler::mRevoke: Set(),1688 schedNoFence::scheduler::mSchedule: Set(),1689 schedNoFence::scheduler::published: 0,1690 schedNoFence::scheduler::publishedBy: Set(),1691 schedNoFence::scheduler::ws:1692 Map(1693 "w1" ->1694 {1695 attached: Set(),1696 built: false,1697 expecting: false,1698 running: false,1699 session: true,1700 up: true1701 },1702 "w2" ->1703 {1704 attached: Set(),1705 built: false,1706 expecting: false,1707 running: false,1708 session: true,1709 up: true1710 }1711 )1712}17131714[State 1]1715{1716 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1717 schedNoFence::scheduler::crashes: 0,1718 schedNoFence::scheduler::entry: [],1719 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1720 schedNoFence::scheduler::mAssigned: Set(),1721 schedNoFence::scheduler::mBuild: Set(),1722 schedNoFence::scheduler::mDone: Set(),1723 schedNoFence::scheduler::mExpect: Set(),1724 schedNoFence::scheduler::mResult: Set(),1725 schedNoFence::scheduler::mRetry: Set(),1726 schedNoFence::scheduler::mRevoke: Set(),1727 schedNoFence::scheduler::mSchedule: Set("c2"),1728 schedNoFence::scheduler::published: 0,1729 schedNoFence::scheduler::publishedBy: Set(),1730 schedNoFence::scheduler::ws:1731 Map(1732 "w1" ->1733 {1734 attached: Set(),1735 built: false,1736 expecting: false,1737 running: false,1738 session: true,1739 up: true1740 },1741 "w2" ->1742 {1743 attached: Set(),1744 built: false,1745 expecting: false,1746 running: false,1747 session: true,1748 up: true1749 }1750 )1751}17521753[State 2]1754{1755 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1756 schedNoFence::scheduler::crashes: 1,1757 schedNoFence::scheduler::entry: [],1758 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1759 schedNoFence::scheduler::mAssigned: Set(),1760 schedNoFence::scheduler::mBuild: Set(),1761 schedNoFence::scheduler::mDone: Set(),1762 schedNoFence::scheduler::mExpect: Set(),1763 schedNoFence::scheduler::mResult: Set(),1764 schedNoFence::scheduler::mRetry: Set(),1765 schedNoFence::scheduler::mRevoke: Set(),1766 schedNoFence::scheduler::mSchedule: Set("c2"),1767 schedNoFence::scheduler::published: 0,1768 schedNoFence::scheduler::publishedBy: Set(),1769 schedNoFence::scheduler::ws:1770 Map(1771 "w1" ->1772 {1773 attached: Set(),1774 built: false,1775 expecting: false,1776 running: false,1777 session: false,1778 up: false1779 },1780 "w2" ->1781 {1782 attached: Set(),1783 built: false,1784 expecting: false,1785 running: false,1786 session: true,1787 up: true1788 }1789 )1790}17911792[State 3]1793{1794 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1795 schedNoFence::scheduler::crashes: 1,1796 schedNoFence::scheduler::entry:1797 [{ followers: Set("c2"), leased: true, worker: "w2" }],1798 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1799 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1800 schedNoFence::scheduler::mBuild: Set(),1801 schedNoFence::scheduler::mDone: Set(),1802 schedNoFence::scheduler::mExpect: Set("w2"),1803 schedNoFence::scheduler::mResult: Set(),1804 schedNoFence::scheduler::mRetry: Set(),1805 schedNoFence::scheduler::mRevoke: Set(),1806 schedNoFence::scheduler::mSchedule: Set(),1807 schedNoFence::scheduler::published: 0,1808 schedNoFence::scheduler::publishedBy: Set(),1809 schedNoFence::scheduler::ws:1810 Map(1811 "w1" ->1812 {1813 attached: Set(),1814 built: false,1815 expecting: false,1816 running: false,1817 session: false,1818 up: false1819 },1820 "w2" ->1821 {1822 attached: Set(),1823 built: false,1824 expecting: false,1825 running: false,1826 session: true,1827 up: true1828 }1829 )1830}18311832[State 4]1833{1834 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1835 schedNoFence::scheduler::crashes: 1,1836 schedNoFence::scheduler::entry:1837 [{ followers: Set("c2"), leased: true, worker: "w2" }],1838 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1839 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),1840 schedNoFence::scheduler::mBuild: Set(),1841 schedNoFence::scheduler::mDone: Set(),1842 schedNoFence::scheduler::mExpect: Set(),1843 schedNoFence::scheduler::mResult: Set(),1844 schedNoFence::scheduler::mRetry: Set(),1845 schedNoFence::scheduler::mRevoke: Set(),1846 schedNoFence::scheduler::mSchedule: Set(),1847 schedNoFence::scheduler::published: 0,1848 schedNoFence::scheduler::publishedBy: Set(),1849 schedNoFence::scheduler::ws:1850 Map(1851 "w1" ->1852 {1853 attached: Set(),1854 built: false,1855 expecting: false,1856 running: false,1857 session: false,1858 up: false1859 },1860 "w2" ->1861 {1862 attached: Set(),1863 built: false,1864 expecting: true,1865 running: true,1866 session: true,1867 up: true1868 }1869 )1870}18711872[State 5]1873{1874 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1875 schedNoFence::scheduler::crashes: 2,1876 schedNoFence::scheduler::entry: [],1877 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1878 schedNoFence::scheduler::mAssigned: Set(),1879 schedNoFence::scheduler::mBuild: Set(),1880 schedNoFence::scheduler::mDone: Set(),1881 schedNoFence::scheduler::mExpect: Set(),1882 schedNoFence::scheduler::mResult: Set(),1883 schedNoFence::scheduler::mRetry: Set("c2"),1884 schedNoFence::scheduler::mRevoke: Set(),1885 schedNoFence::scheduler::mSchedule: Set(),1886 schedNoFence::scheduler::published: 0,1887 schedNoFence::scheduler::publishedBy: Set(),1888 schedNoFence::scheduler::ws:1889 Map(1890 "w1" ->1891 {1892 attached: Set(),1893 built: false,1894 expecting: false,1895 running: false,1896 session: false,1897 up: false1898 },1899 "w2" ->1900 {1901 attached: Set(),1902 built: false,1903 expecting: true,1904 running: true,1905 session: false,1906 up: true1907 }1908 )1909}19101911[State 6]1912{1913 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1914 schedNoFence::scheduler::crashes: 2,1915 schedNoFence::scheduler::entry: [],1916 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1917 schedNoFence::scheduler::mAssigned: Set(),1918 schedNoFence::scheduler::mBuild: Set(),1919 schedNoFence::scheduler::mDone: Set(),1920 schedNoFence::scheduler::mExpect: Set(),1921 schedNoFence::scheduler::mResult: Set(),1922 schedNoFence::scheduler::mRetry: Set("c2"),1923 schedNoFence::scheduler::mRevoke: Set(),1924 schedNoFence::scheduler::mSchedule: Set(),1925 schedNoFence::scheduler::published: 0,1926 schedNoFence::scheduler::publishedBy: Set(),1927 schedNoFence::scheduler::ws:1928 Map(1929 "w1" ->1930 {1931 attached: Set(),1932 built: false,1933 expecting: false,1934 running: false,1935 session: true,1936 up: true1937 },1938 "w2" ->1939 {1940 attached: Set(),1941 built: false,1942 expecting: true,1943 running: true,1944 session: false,1945 up: true1946 }1947 )1948}19491950[State 7]1951{1952 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1953 schedNoFence::scheduler::crashes: 2,1954 schedNoFence::scheduler::entry: [],1955 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1956 schedNoFence::scheduler::mAssigned: Set(),1957 schedNoFence::scheduler::mBuild: Set(),1958 schedNoFence::scheduler::mDone: Set(),1959 schedNoFence::scheduler::mExpect: Set(),1960 schedNoFence::scheduler::mResult: Set(),1961 schedNoFence::scheduler::mRetry: Set(),1962 schedNoFence::scheduler::mRevoke: Set(),1963 schedNoFence::scheduler::mSchedule: Set("c2"),1964 schedNoFence::scheduler::published: 0,1965 schedNoFence::scheduler::publishedBy: Set(),1966 schedNoFence::scheduler::ws:1967 Map(1968 "w1" ->1969 {1970 attached: Set(),1971 built: false,1972 expecting: false,1973 running: false,1974 session: true,1975 up: true1976 },1977 "w2" ->1978 {1979 attached: Set(),1980 built: false,1981 expecting: true,1982 running: true,1983 session: false,1984 up: true1985 }1986 )1987}19881989[State 8]1990{1991 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1992 schedNoFence::scheduler::crashes: 2,1993 schedNoFence::scheduler::entry:1994 [{ followers: Set("c2"), leased: true, worker: "w1" }],1995 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1996 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1997 schedNoFence::scheduler::mBuild: Set(),1998 schedNoFence::scheduler::mDone: Set(),1999 schedNoFence::scheduler::mExpect: Set("w1"),2000 schedNoFence::scheduler::mResult: Set(),2001 schedNoFence::scheduler::mRetry: Set(),2002 schedNoFence::scheduler::mRevoke: Set(),2003 schedNoFence::scheduler::mSchedule: Set(),2004 schedNoFence::scheduler::published: 0,2005 schedNoFence::scheduler::publishedBy: Set(),2006 schedNoFence::scheduler::ws:2007 Map(2008 "w1" ->2009 {2010 attached: Set(),2011 built: false,2012 expecting: false,2013 running: false,2014 session: true,2015 up: true2016 },2017 "w2" ->2018 {2019 attached: Set(),2020 built: false,2021 expecting: true,2022 running: true,2023 session: false,2024 up: true2025 }2026 )2027}20282029[State 9]2030{2031 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2032 schedNoFence::scheduler::crashes: 2,2033 schedNoFence::scheduler::entry:2034 [{ followers: Set("c2"), leased: true, worker: "w1" }],2035 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2036 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2037 schedNoFence::scheduler::mBuild: Set(),2038 schedNoFence::scheduler::mDone: Set(),2039 schedNoFence::scheduler::mExpect: Set(),2040 schedNoFence::scheduler::mResult: Set(),2041 schedNoFence::scheduler::mRetry: Set(),2042 schedNoFence::scheduler::mRevoke: Set(),2043 schedNoFence::scheduler::mSchedule: Set(),2044 schedNoFence::scheduler::published: 0,2045 schedNoFence::scheduler::publishedBy: Set(),2046 schedNoFence::scheduler::ws:2047 Map(2048 "w1" ->2049 {2050 attached: Set(),2051 built: false,2052 expecting: true,2053 running: true,2054 session: true,2055 up: true2056 },2057 "w2" ->2058 {2059 attached: Set(),2060 built: false,2061 expecting: true,2062 running: true,2063 session: false,2064 up: true2065 }2066 )2067}20682069[State 10]2070{2071 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2072 schedNoFence::scheduler::crashes: 2,2073 schedNoFence::scheduler::entry:2074 [{ followers: Set("c2"), leased: true, worker: "w1" }],2075 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2076 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2077 schedNoFence::scheduler::mBuild: Set(),2078 schedNoFence::scheduler::mDone: Set(),2079 schedNoFence::scheduler::mExpect: Set(),2080 schedNoFence::scheduler::mResult: Set(),2081 schedNoFence::scheduler::mRetry: Set(),2082 schedNoFence::scheduler::mRevoke: Set(),2083 schedNoFence::scheduler::mSchedule: Set(),2084 schedNoFence::scheduler::published: 1,2085 schedNoFence::scheduler::publishedBy: Set("w2"),2086 schedNoFence::scheduler::ws:2087 Map(2088 "w1" ->2089 {2090 attached: Set(),2091 built: false,2092 expecting: true,2093 running: true,2094 session: true,2095 up: true2096 },2097 "w2" ->2098 {2099 attached: Set(),2100 built: true,2101 expecting: false,2102 running: false,2103 session: false,2104 up: true2105 }2106 )2107}21082109[State 11]2110{2111 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2112 schedNoFence::scheduler::crashes: 2,2113 schedNoFence::scheduler::entry:2114 [{ followers: Set("c2"), leased: true, worker: "w1" }],2115 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2116 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2117 schedNoFence::scheduler::mBuild: Set(),2118 schedNoFence::scheduler::mDone: Set(),2119 schedNoFence::scheduler::mExpect: Set(),2120 schedNoFence::scheduler::mResult: Set(),2121 schedNoFence::scheduler::mRetry: Set(),2122 schedNoFence::scheduler::mRevoke: Set(),2123 schedNoFence::scheduler::mSchedule: Set("c1"),2124 schedNoFence::scheduler::published: 1,2125 schedNoFence::scheduler::publishedBy: Set("w2"),2126 schedNoFence::scheduler::ws:2127 Map(2128 "w1" ->2129 {2130 attached: Set(),2131 built: false,2132 expecting: true,2133 running: true,2134 session: true,2135 up: true2136 },2137 "w2" ->2138 {2139 attached: Set(),2140 built: true,2141 expecting: false,2142 running: false,2143 session: false,2144 up: true2145 }2146 )2147}21482149[State 12]2150{2151 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2152 schedNoFence::scheduler::crashes: 2,2153 schedNoFence::scheduler::entry:2154 [{ followers: Set("c2"), leased: true, worker: "w1" }],2155 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2156 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2157 schedNoFence::scheduler::mBuild: Set(),2158 schedNoFence::scheduler::mDone: Set("w1"),2159 schedNoFence::scheduler::mExpect: Set(),2160 schedNoFence::scheduler::mResult: Set(),2161 schedNoFence::scheduler::mRetry: Set(),2162 schedNoFence::scheduler::mRevoke: Set(),2163 schedNoFence::scheduler::mSchedule: Set("c1"),2164 schedNoFence::scheduler::published: 2,2165 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2166 schedNoFence::scheduler::ws:2167 Map(2168 "w1" ->2169 {2170 attached: Set(),2171 built: true,2172 expecting: false,2173 running: false,2174 session: true,2175 up: true2176 },2177 "w2" ->2178 {2179 attached: Set(),2180 built: true,2181 expecting: false,2182 running: false,2183 session: false,2184 up: true2185 }2186 )2187}21882189[violation] Found an issue (4312ms at 1386 traces/second).2190Use --verbosity=3 to show executions.2191Use --seed=0x197a26041cfe8d09 --backend=rust to reproduce.2192error: Invariant violated2193An example execution:21942195[State 0]2196{2197 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2198 schedNoPush::scheduler::crashes: 0,2199 schedNoPush::scheduler::entry: [],2200 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2201 schedNoPush::scheduler::mAssigned: Set(),2202 schedNoPush::scheduler::mBuild: Set(),2203 schedNoPush::scheduler::mDone: Set(),2204 schedNoPush::scheduler::mExpect: Set(),2205 schedNoPush::scheduler::mResult: Set(),2206 schedNoPush::scheduler::mRetry: Set(),2207 schedNoPush::scheduler::mRevoke: Set(),2208 schedNoPush::scheduler::mSchedule: Set(),2209 schedNoPush::scheduler::published: 0,2210 schedNoPush::scheduler::publishedBy: Set(),2211 schedNoPush::scheduler::ws:2212 Map(2213 "w1" ->2214 {2215 attached: Set(),2216 built: false,2217 expecting: false,2218 running: false,2219 session: true,2220 up: true2221 },2222 "w2" ->2223 {2224 attached: Set(),2225 built: false,2226 expecting: false,2227 running: false,2228 session: true,2229 up: true2230 }2231 )2232}22332234[State 1]2235{2236 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2237 schedNoPush::scheduler::crashes: 0,2238 schedNoPush::scheduler::entry: [],2239 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2240 schedNoPush::scheduler::mAssigned: Set(),2241 schedNoPush::scheduler::mBuild: Set(),2242 schedNoPush::scheduler::mDone: Set(),2243 schedNoPush::scheduler::mExpect: Set(),2244 schedNoPush::scheduler::mResult: Set(),2245 schedNoPush::scheduler::mRetry: Set(),2246 schedNoPush::scheduler::mRevoke: Set(),2247 schedNoPush::scheduler::mSchedule: Set("c2"),2248 schedNoPush::scheduler::published: 0,2249 schedNoPush::scheduler::publishedBy: Set(),2250 schedNoPush::scheduler::ws:2251 Map(2252 "w1" ->2253 {2254 attached: Set(),2255 built: false,2256 expecting: false,2257 running: false,2258 session: true,2259 up: true2260 },2261 "w2" ->2262 {2263 attached: Set(),2264 built: false,2265 expecting: false,2266 running: false,2267 session: true,2268 up: true2269 }2270 )2271}22722273[State 2]2274{2275 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2276 schedNoPush::scheduler::crashes: 0,2277 schedNoPush::scheduler::entry:2278 [{ followers: Set("c2"), leased: true, worker: "w1" }],2279 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2280 schedNoPush::scheduler::mAssigned: Set(("c2", "w1")),2281 schedNoPush::scheduler::mBuild: Set(),2282 schedNoPush::scheduler::mDone: Set(),2283 schedNoPush::scheduler::mExpect: Set(),2284 schedNoPush::scheduler::mResult: Set(),2285 schedNoPush::scheduler::mRetry: Set(),2286 schedNoPush::scheduler::mRevoke: Set(),2287 schedNoPush::scheduler::mSchedule: Set(),2288 schedNoPush::scheduler::published: 0,2289 schedNoPush::scheduler::publishedBy: Set(),2290 schedNoPush::scheduler::ws:2291 Map(2292 "w1" ->2293 {2294 attached: Set(),2295 built: false,2296 expecting: false,2297 running: false,2298 session: true,2299 up: true2300 },2301 "w2" ->2302 {2303 attached: Set(),2304 built: false,2305 expecting: false,2306 running: false,2307 session: true,2308 up: true2309 }2310 )2311}23122313[State 3]2314{2315 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),2316 schedNoPush::scheduler::crashes: 0,2317 schedNoPush::scheduler::entry:2318 [{ followers: Set("c2"), leased: true, worker: "w1" }],2319 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2320 schedNoPush::scheduler::mAssigned: Set(),2321 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2322 schedNoPush::scheduler::mDone: Set(),2323 schedNoPush::scheduler::mExpect: Set(),2324 schedNoPush::scheduler::mResult: Set(),2325 schedNoPush::scheduler::mRetry: Set(),2326 schedNoPush::scheduler::mRevoke: Set(),2327 schedNoPush::scheduler::mSchedule: Set(),2328 schedNoPush::scheduler::published: 0,2329 schedNoPush::scheduler::publishedBy: Set(),2330 schedNoPush::scheduler::ws:2331 Map(2332 "w1" ->2333 {2334 attached: Set(),2335 built: false,2336 expecting: false,2337 running: false,2338 session: true,2339 up: true2340 },2341 "w2" ->2342 {2343 attached: Set(),2344 built: false,2345 expecting: false,2346 running: false,2347 session: true,2348 up: true2349 }2350 )2351}23522353[State 4]2354{2355 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),2356 schedNoPush::scheduler::crashes: 1,2357 schedNoPush::scheduler::entry:2358 [{ followers: Set("c2"), leased: true, worker: "w1" }],2359 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2360 schedNoPush::scheduler::mAssigned: Set(),2361 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2362 schedNoPush::scheduler::mDone: Set(),2363 schedNoPush::scheduler::mExpect: Set(),2364 schedNoPush::scheduler::mResult: Set(),2365 schedNoPush::scheduler::mRetry: Set(),2366 schedNoPush::scheduler::mRevoke: Set(),2367 schedNoPush::scheduler::mSchedule: Set(),2368 schedNoPush::scheduler::published: 0,2369 schedNoPush::scheduler::publishedBy: Set(),2370 schedNoPush::scheduler::ws:2371 Map(2372 "w1" ->2373 {2374 attached: Set(),2375 built: false,2376 expecting: false,2377 running: false,2378 session: false,2379 up: false2380 },2381 "w2" ->2382 {2383 attached: Set(),2384 built: false,2385 expecting: false,2386 running: false,2387 session: true,2388 up: true2389 }2390 )2391}23922393[State 5]2394{2395 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),2396 schedNoPush::scheduler::crashes: 2,2397 schedNoPush::scheduler::entry: [],2398 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2399 schedNoPush::scheduler::mAssigned: Set(),2400 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2401 schedNoPush::scheduler::mDone: Set(),2402 schedNoPush::scheduler::mExpect: Set(),2403 schedNoPush::scheduler::mResult: Set(),2404 schedNoPush::scheduler::mRetry: Set(),2405 schedNoPush::scheduler::mRevoke: Set(),2406 schedNoPush::scheduler::mSchedule: Set(),2407 schedNoPush::scheduler::published: 0,2408 schedNoPush::scheduler::publishedBy: Set(),2409 schedNoPush::scheduler::ws:2410 Map(2411 "w1" ->2412 {2413 attached: Set(),2414 built: false,2415 expecting: false,2416 running: false,2417 session: false,2418 up: false2419 },2420 "w2" ->2421 {2422 attached: Set(),2423 built: false,2424 expecting: false,2425 running: false,2426 session: false,2427 up: true2428 }2429 )2430}24312432[State 6]2433{2434 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),2435 schedNoPush::scheduler::crashes: 2,2436 schedNoPush::scheduler::entry: [],2437 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2438 schedNoPush::scheduler::mAssigned: Set(),2439 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2440 schedNoPush::scheduler::mDone: Set(),2441 schedNoPush::scheduler::mExpect: Set(),2442 schedNoPush::scheduler::mResult: Set(),2443 schedNoPush::scheduler::mRetry: Set(),2444 schedNoPush::scheduler::mRevoke: Set(),2445 schedNoPush::scheduler::mSchedule: Set(),2446 schedNoPush::scheduler::published: 0,2447 schedNoPush::scheduler::publishedBy: Set(),2448 schedNoPush::scheduler::ws:2449 Map(2450 "w1" ->2451 {2452 attached: Set(),2453 built: false,2454 expecting: false,2455 running: false,2456 session: true,2457 up: true2458 },2459 "w2" ->2460 {2461 attached: Set(),2462 built: false,2463 expecting: false,2464 running: false,2465 session: false,2466 up: true2467 }2468 )2469}24702471[State 7]2472{2473 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),2474 schedNoPush::scheduler::crashes: 2,2475 schedNoPush::scheduler::entry: [],2476 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2477 schedNoPush::scheduler::mAssigned: Set(),2478 schedNoPush::scheduler::mBuild: Set(),2479 schedNoPush::scheduler::mDone: Set(),2480 schedNoPush::scheduler::mExpect: Set(),2481 schedNoPush::scheduler::mResult: Set(),2482 schedNoPush::scheduler::mRetry: Set(),2483 schedNoPush::scheduler::mRevoke: Set(),2484 schedNoPush::scheduler::mSchedule: Set(),2485 schedNoPush::scheduler::published: 0,2486 schedNoPush::scheduler::publishedBy: Set(),2487 schedNoPush::scheduler::ws:2488 Map(2489 "w1" ->2490 {2491 attached: Set("c2"),2492 built: false,2493 expecting: true,2494 running: true,2495 session: true,2496 up: true2497 },2498 "w2" ->2499 {2500 attached: Set(),2501 built: false,2502 expecting: false,2503 running: false,2504 session: false,2505 up: true2506 }2507 )2508}25092510[violation] Found an issue (799ms at 1339 traces/second).2511Use --verbosity=3 to show executions.2512Use --seed=0xda5e4ae4a638021 --backend=rust to reproduce.2513error: Invariant violated2514An example execution:25152516[State 0]2517{2518 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2519 schedNoReport::scheduler::crashes: 0,2520 schedNoReport::scheduler::entry: [],2521 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2522 schedNoReport::scheduler::mAssigned: Set(),2523 schedNoReport::scheduler::mBuild: Set(),2524 schedNoReport::scheduler::mDone: Set(),2525 schedNoReport::scheduler::mExpect: Set(),2526 schedNoReport::scheduler::mResult: Set(),2527 schedNoReport::scheduler::mRetry: Set(),2528 schedNoReport::scheduler::mRevoke: Set(),2529 schedNoReport::scheduler::mSchedule: Set(),2530 schedNoReport::scheduler::published: 0,2531 schedNoReport::scheduler::publishedBy: Set(),2532 schedNoReport::scheduler::ws:2533 Map(2534 "w1" ->2535 {2536 attached: Set(),2537 built: false,2538 expecting: false,2539 running: false,2540 session: true,2541 up: true2542 },2543 "w2" ->2544 {2545 attached: Set(),2546 built: false,2547 expecting: false,2548 running: false,2549 session: true,2550 up: true2551 }2552 )2553}25542555[State 1]2556{2557 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2558 schedNoReport::scheduler::crashes: 1,2559 schedNoReport::scheduler::entry: [],2560 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2561 schedNoReport::scheduler::mAssigned: Set(),2562 schedNoReport::scheduler::mBuild: Set(),2563 schedNoReport::scheduler::mDone: Set(),2564 schedNoReport::scheduler::mExpect: Set(),2565 schedNoReport::scheduler::mResult: Set(),2566 schedNoReport::scheduler::mRetry: Set(),2567 schedNoReport::scheduler::mRevoke: Set(),2568 schedNoReport::scheduler::mSchedule: Set(),2569 schedNoReport::scheduler::published: 0,2570 schedNoReport::scheduler::publishedBy: Set(),2571 schedNoReport::scheduler::ws:2572 Map(2573 "w1" ->2574 {2575 attached: Set(),2576 built: false,2577 expecting: false,2578 running: false,2579 session: true,2580 up: true2581 },2582 "w2" ->2583 {2584 attached: Set(),2585 built: false,2586 expecting: false,2587 running: false,2588 session: false,2589 up: false2590 }2591 )2592}25932594[State 2]2595{2596 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2597 schedNoReport::scheduler::crashes: 1,2598 schedNoReport::scheduler::entry: [],2599 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2600 schedNoReport::scheduler::mAssigned: Set(),2601 schedNoReport::scheduler::mBuild: Set(),2602 schedNoReport::scheduler::mDone: Set(),2603 schedNoReport::scheduler::mExpect: Set(),2604 schedNoReport::scheduler::mResult: Set(),2605 schedNoReport::scheduler::mRetry: Set(),2606 schedNoReport::scheduler::mRevoke: Set(),2607 schedNoReport::scheduler::mSchedule: Set("c2"),2608 schedNoReport::scheduler::published: 0,2609 schedNoReport::scheduler::publishedBy: Set(),2610 schedNoReport::scheduler::ws:2611 Map(2612 "w1" ->2613 {2614 attached: Set(),2615 built: false,2616 expecting: false,2617 running: false,2618 session: true,2619 up: true2620 },2621 "w2" ->2622 {2623 attached: Set(),2624 built: false,2625 expecting: false,2626 running: false,2627 session: false,2628 up: false2629 }2630 )2631}26322633[State 3]2634{2635 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2636 schedNoReport::scheduler::crashes: 1,2637 schedNoReport::scheduler::entry:2638 [{ followers: Set("c2"), leased: true, worker: "w1" }],2639 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2640 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2641 schedNoReport::scheduler::mBuild: Set(),2642 schedNoReport::scheduler::mDone: Set(),2643 schedNoReport::scheduler::mExpect: Set("w1"),2644 schedNoReport::scheduler::mResult: Set(),2645 schedNoReport::scheduler::mRetry: Set(),2646 schedNoReport::scheduler::mRevoke: Set(),2647 schedNoReport::scheduler::mSchedule: Set(),2648 schedNoReport::scheduler::published: 0,2649 schedNoReport::scheduler::publishedBy: Set(),2650 schedNoReport::scheduler::ws:2651 Map(2652 "w1" ->2653 {2654 attached: Set(),2655 built: false,2656 expecting: false,2657 running: false,2658 session: true,2659 up: true2660 },2661 "w2" ->2662 {2663 attached: Set(),2664 built: false,2665 expecting: false,2666 running: false,2667 session: false,2668 up: false2669 }2670 )2671}26722673[State 4]2674{2675 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2676 schedNoReport::scheduler::crashes: 1,2677 schedNoReport::scheduler::entry:2678 [{ followers: Set("c2"), leased: true, worker: "w1" }],2679 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2680 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2681 schedNoReport::scheduler::mBuild: Set(),2682 schedNoReport::scheduler::mDone: Set(),2683 schedNoReport::scheduler::mExpect: Set("w1"),2684 schedNoReport::scheduler::mResult: Set(),2685 schedNoReport::scheduler::mRetry: Set(),2686 schedNoReport::scheduler::mRevoke: Set(),2687 schedNoReport::scheduler::mSchedule: Set(),2688 schedNoReport::scheduler::published: 0,2689 schedNoReport::scheduler::publishedBy: Set(),2690 schedNoReport::scheduler::ws:2691 Map(2692 "w1" ->2693 {2694 attached: Set(),2695 built: false,2696 expecting: false,2697 running: false,2698 session: true,2699 up: true2700 },2701 "w2" ->2702 {2703 attached: Set(),2704 built: false,2705 expecting: false,2706 running: false,2707 session: true,2708 up: true2709 }2710 )2711}27122713[State 5]2714{2715 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2716 schedNoReport::scheduler::crashes: 1,2717 schedNoReport::scheduler::entry:2718 [{ followers: Set("c2"), leased: true, worker: "w1" }],2719 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2720 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2721 schedNoReport::scheduler::mBuild: Set(),2722 schedNoReport::scheduler::mDone: Set(),2723 schedNoReport::scheduler::mExpect: Set(),2724 schedNoReport::scheduler::mResult: Set(),2725 schedNoReport::scheduler::mRetry: Set(),2726 schedNoReport::scheduler::mRevoke: Set(),2727 schedNoReport::scheduler::mSchedule: Set(),2728 schedNoReport::scheduler::published: 0,2729 schedNoReport::scheduler::publishedBy: Set(),2730 schedNoReport::scheduler::ws:2731 Map(2732 "w1" ->2733 {2734 attached: Set(),2735 built: false,2736 expecting: true,2737 running: true,2738 session: true,2739 up: true2740 },2741 "w2" ->2742 {2743 attached: Set(),2744 built: false,2745 expecting: false,2746 running: false,2747 session: true,2748 up: true2749 }2750 )2751}27522753[State 6]2754{2755 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2756 schedNoReport::scheduler::crashes: 2,2757 schedNoReport::scheduler::entry: [],2758 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2759 schedNoReport::scheduler::mAssigned: Set(),2760 schedNoReport::scheduler::mBuild: Set(),2761 schedNoReport::scheduler::mDone: Set(),2762 schedNoReport::scheduler::mExpect: Set(),2763 schedNoReport::scheduler::mResult: Set(),2764 schedNoReport::scheduler::mRetry: Set("c2"),2765 schedNoReport::scheduler::mRevoke: Set(),2766 schedNoReport::scheduler::mSchedule: Set(),2767 schedNoReport::scheduler::published: 0,2768 schedNoReport::scheduler::publishedBy: Set(),2769 schedNoReport::scheduler::ws:2770 Map(2771 "w1" ->2772 {2773 attached: Set(),2774 built: false,2775 expecting: true,2776 running: true,2777 session: false,2778 up: true2779 },2780 "w2" ->2781 {2782 attached: Set(),2783 built: false,2784 expecting: false,2785 running: false,2786 session: false,2787 up: true2788 }2789 )2790}27912792[State 7]2793{2794 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2795 schedNoReport::scheduler::crashes: 2,2796 schedNoReport::scheduler::entry: [],2797 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2798 schedNoReport::scheduler::mAssigned: Set(),2799 schedNoReport::scheduler::mBuild: Set(),2800 schedNoReport::scheduler::mDone: Set(),2801 schedNoReport::scheduler::mExpect: Set(),2802 schedNoReport::scheduler::mResult: Set(),2803 schedNoReport::scheduler::mRetry: Set("c2"),2804 schedNoReport::scheduler::mRevoke: Set(),2805 schedNoReport::scheduler::mSchedule: Set("c1"),2806 schedNoReport::scheduler::published: 0,2807 schedNoReport::scheduler::publishedBy: Set(),2808 schedNoReport::scheduler::ws:2809 Map(2810 "w1" ->2811 {2812 attached: Set(),2813 built: false,2814 expecting: true,2815 running: true,2816 session: false,2817 up: true2818 },2819 "w2" ->2820 {2821 attached: Set(),2822 built: false,2823 expecting: false,2824 running: false,2825 session: false,2826 up: true2827 }2828 )2829}28302831[State 8]2832{2833 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2834 schedNoReport::scheduler::crashes: 2,2835 schedNoReport::scheduler::entry: [],2836 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2837 schedNoReport::scheduler::mAssigned: Set(),2838 schedNoReport::scheduler::mBuild: Set(),2839 schedNoReport::scheduler::mDone: Set(),2840 schedNoReport::scheduler::mExpect: Set(),2841 schedNoReport::scheduler::mResult: Set(),2842 schedNoReport::scheduler::mRetry: Set("c2"),2843 schedNoReport::scheduler::mRevoke: Set(),2844 schedNoReport::scheduler::mSchedule: Set("c1"),2845 schedNoReport::scheduler::published: 0,2846 schedNoReport::scheduler::publishedBy: Set(),2847 schedNoReport::scheduler::ws:2848 Map(2849 "w1" ->2850 {2851 attached: Set(),2852 built: false,2853 expecting: true,2854 running: true,2855 session: false,2856 up: true2857 },2858 "w2" ->2859 {2860 attached: Set(),2861 built: false,2862 expecting: false,2863 running: false,2864 session: true,2865 up: true2866 }2867 )2868}28692870[State 9]2871{2872 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2873 schedNoReport::scheduler::crashes: 2,2874 schedNoReport::scheduler::entry:2875 [{ followers: Set("c1"), leased: true, worker: "w2" }],2876 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2877 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2878 schedNoReport::scheduler::mBuild: Set(),2879 schedNoReport::scheduler::mDone: Set(),2880 schedNoReport::scheduler::mExpect: Set("w2"),2881 schedNoReport::scheduler::mResult: Set(),2882 schedNoReport::scheduler::mRetry: Set("c2"),2883 schedNoReport::scheduler::mRevoke: Set(),2884 schedNoReport::scheduler::mSchedule: Set(),2885 schedNoReport::scheduler::published: 0,2886 schedNoReport::scheduler::publishedBy: Set(),2887 schedNoReport::scheduler::ws:2888 Map(2889 "w1" ->2890 {2891 attached: Set(),2892 built: false,2893 expecting: true,2894 running: true,2895 session: false,2896 up: true2897 },2898 "w2" ->2899 {2900 attached: Set(),2901 built: false,2902 expecting: false,2903 running: false,2904 session: true,2905 up: true2906 }2907 )2908}29092910[State 10]2911{2912 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2913 schedNoReport::scheduler::crashes: 2,2914 schedNoReport::scheduler::entry:2915 [{ followers: Set("c1"), leased: true, worker: "w2" }],2916 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2917 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2918 schedNoReport::scheduler::mBuild: Set(),2919 schedNoReport::scheduler::mDone: Set(),2920 schedNoReport::scheduler::mExpect: Set(),2921 schedNoReport::scheduler::mResult: Set(),2922 schedNoReport::scheduler::mRetry: Set("c2"),2923 schedNoReport::scheduler::mRevoke: Set(),2924 schedNoReport::scheduler::mSchedule: Set(),2925 schedNoReport::scheduler::published: 0,2926 schedNoReport::scheduler::publishedBy: Set(),2927 schedNoReport::scheduler::ws:2928 Map(2929 "w1" ->2930 {2931 attached: Set(),2932 built: false,2933 expecting: true,2934 running: true,2935 session: false,2936 up: true2937 },2938 "w2" ->2939 {2940 attached: Set(),2941 built: false,2942 expecting: true,2943 running: true,2944 session: true,2945 up: true2946 }2947 )2948}29492950[State 11]2951{2952 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2953 schedNoReport::scheduler::crashes: 2,2954 schedNoReport::scheduler::entry:2955 [{ followers: Set("c1"), leased: true, worker: "w2" }],2956 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2957 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2958 schedNoReport::scheduler::mBuild: Set(),2959 schedNoReport::scheduler::mDone: Set(),2960 schedNoReport::scheduler::mExpect: Set(),2961 schedNoReport::scheduler::mResult: Set(),2962 schedNoReport::scheduler::mRetry: Set("c2"),2963 schedNoReport::scheduler::mRevoke: Set(),2964 schedNoReport::scheduler::mSchedule: Set(),2965 schedNoReport::scheduler::published: 0,2966 schedNoReport::scheduler::publishedBy: Set(),2967 schedNoReport::scheduler::ws:2968 Map(2969 "w1" ->2970 {2971 attached: Set(),2972 built: false,2973 expecting: true,2974 running: true,2975 session: true,2976 up: true2977 },2978 "w2" ->2979 {2980 attached: Set(),2981 built: false,2982 expecting: true,2983 running: true,2984 session: true,2985 up: true2986 }2987 )2988}29892990[violation] Found an issue (1462ms at 2092 traces/second).2991Use --verbosity=3 to show executions.2992Use --seed=0x1bea9633c2e680b4 --backend=rust to reproduce.2993error: Invariant violated2994An example execution:29952996[State 0]2997{2998 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2999 schedTerminal::scheduler::crashes: 0,3000 schedTerminal::scheduler::entry: [],3001 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3002 schedTerminal::scheduler::mAssigned: Set(),3003 schedTerminal::scheduler::mBuild: Set(),3004 schedTerminal::scheduler::mDone: Set(),3005 schedTerminal::scheduler::mExpect: Set(),3006 schedTerminal::scheduler::mResult: Set(),3007 schedTerminal::scheduler::mRetry: Set(),3008 schedTerminal::scheduler::mRevoke: Set(),3009 schedTerminal::scheduler::mSchedule: Set(),3010 schedTerminal::scheduler::published: 0,3011 schedTerminal::scheduler::publishedBy: Set(),3012 schedTerminal::scheduler::ws:3013 Map(3014 "w1" ->3015 {3016 attached: Set(),3017 built: false,3018 expecting: false,3019 running: false,3020 session: true,3021 up: true3022 },3023 "w2" ->3024 {3025 attached: Set(),3026 built: false,3027 expecting: false,3028 running: false,3029 session: true,3030 up: true3031 }3032 )3033}30343035[State 1]3036{3037 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3038 schedTerminal::scheduler::crashes: 1,3039 schedTerminal::scheduler::entry: [],3040 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3041 schedTerminal::scheduler::mAssigned: Set(),3042 schedTerminal::scheduler::mBuild: Set(),3043 schedTerminal::scheduler::mDone: Set(),3044 schedTerminal::scheduler::mExpect: Set(),3045 schedTerminal::scheduler::mResult: Set(),3046 schedTerminal::scheduler::mRetry: Set(),3047 schedTerminal::scheduler::mRevoke: Set(),3048 schedTerminal::scheduler::mSchedule: Set(),3049 schedTerminal::scheduler::published: 0,3050 schedTerminal::scheduler::publishedBy: Set(),3051 schedTerminal::scheduler::ws:3052 Map(3053 "w1" ->3054 {3055 attached: Set(),3056 built: false,3057 expecting: false,3058 running: false,3059 session: true,3060 up: true3061 },3062 "w2" ->3063 {3064 attached: Set(),3065 built: false,3066 expecting: false,3067 running: false,3068 session: false,3069 up: false3070 }3071 )3072}30733074[State 2]3075{3076 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3077 schedTerminal::scheduler::crashes: 2,3078 schedTerminal::scheduler::entry: [],3079 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3080 schedTerminal::scheduler::mAssigned: Set(),3081 schedTerminal::scheduler::mBuild: Set(),3082 schedTerminal::scheduler::mDone: Set(),3083 schedTerminal::scheduler::mExpect: Set(),3084 schedTerminal::scheduler::mResult: Set(),3085 schedTerminal::scheduler::mRetry: Set(),3086 schedTerminal::scheduler::mRevoke: Set(),3087 schedTerminal::scheduler::mSchedule: Set(),3088 schedTerminal::scheduler::published: 0,3089 schedTerminal::scheduler::publishedBy: Set(),3090 schedTerminal::scheduler::ws:3091 Map(3092 "w1" ->3093 {3094 attached: Set(),3095 built: false,3096 expecting: false,3097 running: false,3098 session: false,3099 up: true3100 },3101 "w2" ->3102 {3103 attached: Set(),3104 built: false,3105 expecting: false,3106 running: false,3107 session: false,3108 up: false3109 }3110 )3111}31123113[State 3]3114{3115 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3116 schedTerminal::scheduler::crashes: 2,3117 schedTerminal::scheduler::entry: [],3118 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3119 schedTerminal::scheduler::mAssigned: Set(),3120 schedTerminal::scheduler::mBuild: Set(),3121 schedTerminal::scheduler::mDone: Set(),3122 schedTerminal::scheduler::mExpect: Set(),3123 schedTerminal::scheduler::mResult: Set(),3124 schedTerminal::scheduler::mRetry: Set(),3125 schedTerminal::scheduler::mRevoke: Set(),3126 schedTerminal::scheduler::mSchedule: Set("c2"),3127 schedTerminal::scheduler::published: 0,3128 schedTerminal::scheduler::publishedBy: Set(),3129 schedTerminal::scheduler::ws:3130 Map(3131 "w1" ->3132 {3133 attached: Set(),3134 built: false,3135 expecting: false,3136 running: false,3137 session: false,3138 up: true3139 },3140 "w2" ->3141 {3142 attached: Set(),3143 built: false,3144 expecting: false,3145 running: false,3146 session: false,3147 up: false3148 }3149 )3150}31513152[State 4]3153{3154 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3155 schedTerminal::scheduler::crashes: 2,3156 schedTerminal::scheduler::entry: [],3157 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3158 schedTerminal::scheduler::mAssigned: Set(),3159 schedTerminal::scheduler::mBuild: Set(),3160 schedTerminal::scheduler::mDone: Set(),3161 schedTerminal::scheduler::mExpect: Set(),3162 schedTerminal::scheduler::mResult: Set(),3163 schedTerminal::scheduler::mRetry: Set(),3164 schedTerminal::scheduler::mRevoke: Set(),3165 schedTerminal::scheduler::mSchedule: Set(),3166 schedTerminal::scheduler::published: 0,3167 schedTerminal::scheduler::publishedBy: Set(),3168 schedTerminal::scheduler::ws:3169 Map(3170 "w1" ->3171 {3172 attached: Set(),3173 built: false,3174 expecting: false,3175 running: false,3176 session: false,3177 up: true3178 },3179 "w2" ->3180 {3181 attached: Set(),3182 built: false,3183 expecting: false,3184 running: false,3185 session: false,3186 up: false3187 }3188 )3189}31903191[violation] Found an issue (102ms at 451 traces/second).3192Use --verbosity=3 to show executions.3193Use --seed=0xe4d9fbccd653435d --backend=rust to reproduce.3194error: Invariant violated3195An example execution:31963197[State 0]3198{3199 pushFixed::push::byPath: Map(),3200 pushFixed::push::inflight: Set(),3201 pushFixed::push::left: Map(),3202 pushFixed::push::sent: Map()3203}32043205[State 1]3206{3207 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3208 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3209 pushFixed::push::left: Map(3 -> 2),3210 pushFixed::push::sent: Map(3 -> Set("a", "b"))3211}32123213[State 2]3214{3215 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3216 pushFixed::push::inflight: Set((3, "b")),3217 pushFixed::push::left: Map(3 -> 1),3218 pushFixed::push::sent: Map(3 -> Set("a", "b"))3219}32203221[State 3]3222{3223 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3224 pushFixed::push::inflight: Set(),3225 pushFixed::push::left: Map(3 -> 0),3226 pushFixed::push::sent: Map(3 -> Set("a", "b"))3227}32283229[State 4]3230{3231 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3232 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3233 pushFixed::push::left: Map(1 -> 2, 3 -> 0),3234 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3235}32363237[State 5]3238{3239 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3240 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),3241 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 0),3242 pushFixed::push::sent:3243 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3244}32453246[State 6]3247{3248 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3249 pushFixed::push::inflight: Set((1, "a"), (2, "a"), (2, "b")),3250 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 0),3251 pushFixed::push::sent:3252 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3253}32543255[State 7]3256{3257 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3258 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3259 pushFixed::push::left: Map(1 -> 0, 2 -> 2, 3 -> 0),3260 pushFixed::push::sent:3261 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3262}32633264[State 8]3265{3266 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3267 pushFixed::push::inflight: Set((2, "a")),3268 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 0),3269 pushFixed::push::sent:3270 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3271}32723273[State 9]3274{3275 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3276 pushFixed::push::inflight: Set(),3277 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3278 pushFixed::push::sent:3279 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3280}32813282[ok] No violation found (947ms at 21119 traces/second).3283Trace length statistics: max=10, min=7, average=8.003284You may increase --max-samples and --max-steps.3285Use --verbosity to produce more (or less) output.3286Use --seed=0xefabd6e731466efb --backend=rust to reproduce.