nixbot

builds

succeeded nix-grpc-store-spec checks.aarch64-darwin.spec · build #689 · 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" -> CIdle, "c2" -> CIdle),46 schedFixed::scheduler::crashes: 1,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(),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: false,77 up: false78 }79 )80}8182[State 2]83{84 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),85 schedFixed::scheduler::crashes: 2,86 schedFixed::scheduler::entry: [],87 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),88 schedFixed::scheduler::mAssigned: Set(),89 schedFixed::scheduler::mBuild: Set(),90 schedFixed::scheduler::mDone: Set(),91 schedFixed::scheduler::mExpect: Set(),92 schedFixed::scheduler::mResult: Set(),93 schedFixed::scheduler::mRetry: Set(),94 schedFixed::scheduler::mRevoke: Set(),95 schedFixed::scheduler::mSchedule: Set(),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: false108 },109 "w2" ->110 {111 attached: Set(),112 built: false,113 expecting: false,114 running: false,115 session: false,116 up: false117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),124 schedFixed::scheduler::crashes: 2,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("c2"),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: false147 },148 "w2" ->149 {150 attached: Set(),151 built: false,152 expecting: false,153 running: false,154 session: false,155 up: false156 }157 )158}159160[State 4]161{162 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),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(),172 schedFixed::scheduler::mRevoke: Set(),173 schedFixed::scheduler::mSchedule: Set("c2"),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: false195 }196 )197}198199[State 5]200{201 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),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", "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: false234 }235 )236}237238[State 6]239{240 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),241 schedFixed::scheduler::crashes: 2,242 schedFixed::scheduler::entry:243 [{ followers: Set("c2"), leased: true, worker: "w1" }],244 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),245 schedFixed::scheduler::mAssigned: Set(("c2", "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("c1"),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: false274 }275 )276}277278[State 7]279{280 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),281 schedFixed::scheduler::crashes: 2,282 schedFixed::scheduler::entry:283 [{ 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: false314 }315 )316}317318[State 8]319{320 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),321 schedFixed::scheduler::crashes: 2,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: false354 }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("w1"),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: true,384 up: true385 },386 "w2" ->387 {388 attached: Set(),389 built: false,390 expecting: false,391 running: false,392 session: true,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(),407 schedFixed::scheduler::mDone: Set(),408 schedFixed::scheduler::mExpect: Set("w1"),409 schedFixed::scheduler::mResult: Set(),410 schedFixed::scheduler::mRetry: Set("c1"),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: true,424 up: true425 },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" -> CQueued, "c2" -> CQueued),441 schedFixed::scheduler::crashes: 2,442 schedFixed::scheduler::entry:443 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],444 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),445 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),446 schedFixed::scheduler::mBuild: Set(),447 schedFixed::scheduler::mDone: Set(),448 schedFixed::scheduler::mExpect: Set("w1"),449 schedFixed::scheduler::mResult: Set(),450 schedFixed::scheduler::mRetry: Set(),451 schedFixed::scheduler::mRevoke: Set(),452 schedFixed::scheduler::mSchedule: Set("c1"),453 schedFixed::scheduler::published: 0,454 schedFixed::scheduler::publishedBy: Set(),455 schedFixed::scheduler::ws:456 Map(457 "w1" ->458 {459 attached: Set(),460 built: false,461 expecting: false,462 running: false,463 session: true,464 up: true465 },466 "w2" ->467 {468 attached: Set(),469 built: false,470 expecting: false,471 running: false,472 session: true,473 up: true474 }475 )476}477478[State 12]479{480 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),481 schedFixed::scheduler::crashes: 2,482 schedFixed::scheduler::entry:483 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],484 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),485 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),486 schedFixed::scheduler::mBuild: Set(),487 schedFixed::scheduler::mDone: Set(),488 schedFixed::scheduler::mExpect: Set("w1"),489 schedFixed::scheduler::mResult: Set(),490 schedFixed::scheduler::mRetry: Set(),491 schedFixed::scheduler::mRevoke: Set(),492 schedFixed::scheduler::mSchedule: Set(),493 schedFixed::scheduler::published: 0,494 schedFixed::scheduler::publishedBy: Set(),495 schedFixed::scheduler::ws:496 Map(497 "w1" ->498 {499 attached: Set(),500 built: false,501 expecting: false,502 running: false,503 session: true,504 up: true505 },506 "w2" ->507 {508 attached: Set(),509 built: false,510 expecting: false,511 running: false,512 session: true,513 up: true514 }515 )516}517518[State 13]519{520 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),521 schedFixed::scheduler::crashes: 2,522 schedFixed::scheduler::entry:523 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],524 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),525 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),526 schedFixed::scheduler::mBuild: Set(("c1", "w1")),527 schedFixed::scheduler::mDone: Set(),528 schedFixed::scheduler::mExpect: Set("w1"),529 schedFixed::scheduler::mResult: Set(),530 schedFixed::scheduler::mRetry: Set(),531 schedFixed::scheduler::mRevoke: Set(),532 schedFixed::scheduler::mSchedule: Set(),533 schedFixed::scheduler::published: 0,534 schedFixed::scheduler::publishedBy: Set(),535 schedFixed::scheduler::ws:536 Map(537 "w1" ->538 {539 attached: Set(),540 built: false,541 expecting: false,542 running: false,543 session: true,544 up: true545 },546 "w2" ->547 {548 attached: Set(),549 built: false,550 expecting: false,551 running: false,552 session: true,553 up: true554 }555 )556}557558[State 14]559{560 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),561 schedFixed::scheduler::crashes: 2,562 schedFixed::scheduler::entry:563 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],564 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),565 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),566 schedFixed::scheduler::mBuild: Set(),567 schedFixed::scheduler::mDone: Set(),568 schedFixed::scheduler::mExpect: Set("w1"),569 schedFixed::scheduler::mResult: Set(),570 schedFixed::scheduler::mRetry: Set("c1"),571 schedFixed::scheduler::mRevoke: Set(),572 schedFixed::scheduler::mSchedule: Set(),573 schedFixed::scheduler::published: 0,574 schedFixed::scheduler::publishedBy: Set(),575 schedFixed::scheduler::ws:576 Map(577 "w1" ->578 {579 attached: Set(),580 built: false,581 expecting: false,582 running: false,583 session: true,584 up: true585 },586 "w2" ->587 {588 attached: Set(),589 built: false,590 expecting: false,591 running: false,592 session: true,593 up: true594 }595 )596}597598[State 15]599{600 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),601 schedFixed::scheduler::crashes: 2,602 schedFixed::scheduler::entry:603 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],604 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),605 schedFixed::scheduler::mAssigned: Set(),606 schedFixed::scheduler::mBuild: Set(("c2", "w1")),607 schedFixed::scheduler::mDone: Set(),608 schedFixed::scheduler::mExpect: Set("w1"),609 schedFixed::scheduler::mResult: Set(),610 schedFixed::scheduler::mRetry: Set("c1"),611 schedFixed::scheduler::mRevoke: Set(),612 schedFixed::scheduler::mSchedule: Set(),613 schedFixed::scheduler::published: 0,614 schedFixed::scheduler::publishedBy: Set(),615 schedFixed::scheduler::ws:616 Map(617 "w1" ->618 {619 attached: Set(),620 built: false,621 expecting: false,622 running: false,623 session: true,624 up: true625 },626 "w2" ->627 {628 attached: Set(),629 built: false,630 expecting: false,631 running: false,632 session: true,633 up: true634 }635 )636}637638[State 16]639{640 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),641 schedFixed::scheduler::crashes: 2,642 schedFixed::scheduler::entry:643 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],644 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),645 schedFixed::scheduler::mAssigned: Set(),646 schedFixed::scheduler::mBuild: Set(),647 schedFixed::scheduler::mDone: Set(),648 schedFixed::scheduler::mExpect: Set("w1"),649 schedFixed::scheduler::mResult: Set(),650 schedFixed::scheduler::mRetry: Set("c1", "c2"),651 schedFixed::scheduler::mRevoke: Set(),652 schedFixed::scheduler::mSchedule: Set(),653 schedFixed::scheduler::published: 0,654 schedFixed::scheduler::publishedBy: Set(),655 schedFixed::scheduler::ws:656 Map(657 "w1" ->658 {659 attached: Set(),660 built: false,661 expecting: false,662 running: false,663 session: true,664 up: true665 },666 "w2" ->667 {668 attached: Set(),669 built: false,670 expecting: false,671 running: false,672 session: true,673 up: true674 }675 )676}677678[State 17]679{680 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),681 schedFixed::scheduler::crashes: 2,682 schedFixed::scheduler::entry:683 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],684 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),685 schedFixed::scheduler::mAssigned: Set(),686 schedFixed::scheduler::mBuild: Set(),687 schedFixed::scheduler::mDone: Set(),688 schedFixed::scheduler::mExpect: Set("w1"),689 schedFixed::scheduler::mResult: Set(),690 schedFixed::scheduler::mRetry: Set("c2"),691 schedFixed::scheduler::mRevoke: Set(),692 schedFixed::scheduler::mSchedule: Set("c1"),693 schedFixed::scheduler::published: 0,694 schedFixed::scheduler::publishedBy: Set(),695 schedFixed::scheduler::ws:696 Map(697 "w1" ->698 {699 attached: Set(),700 built: false,701 expecting: false,702 running: false,703 session: true,704 up: true705 },706 "w2" ->707 {708 attached: Set(),709 built: false,710 expecting: false,711 running: false,712 session: true,713 up: true714 }715 )716}717718[State 18]719{720 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),721 schedFixed::scheduler::crashes: 2,722 schedFixed::scheduler::entry:723 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],724 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),725 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),726 schedFixed::scheduler::mBuild: Set(),727 schedFixed::scheduler::mDone: Set(),728 schedFixed::scheduler::mExpect: Set("w1"),729 schedFixed::scheduler::mResult: Set(),730 schedFixed::scheduler::mRetry: Set("c2"),731 schedFixed::scheduler::mRevoke: Set(),732 schedFixed::scheduler::mSchedule: Set(),733 schedFixed::scheduler::published: 0,734 schedFixed::scheduler::publishedBy: Set(),735 schedFixed::scheduler::ws:736 Map(737 "w1" ->738 {739 attached: Set(),740 built: false,741 expecting: false,742 running: false,743 session: true,744 up: true745 },746 "w2" ->747 {748 attached: Set(),749 built: false,750 expecting: false,751 running: false,752 session: true,753 up: true754 }755 )756}757758[State 19]759{760 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),761 schedFixed::scheduler::crashes: 2,762 schedFixed::scheduler::entry:763 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],764 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),765 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),766 schedFixed::scheduler::mBuild: Set(),767 schedFixed::scheduler::mDone: Set(),768 schedFixed::scheduler::mExpect: Set("w1"),769 schedFixed::scheduler::mResult: Set(),770 schedFixed::scheduler::mRetry: Set(),771 schedFixed::scheduler::mRevoke: Set(),772 schedFixed::scheduler::mSchedule: Set("c2"),773 schedFixed::scheduler::published: 0,774 schedFixed::scheduler::publishedBy: Set(),775 schedFixed::scheduler::ws:776 Map(777 "w1" ->778 {779 attached: Set(),780 built: false,781 expecting: false,782 running: false,783 session: true,784 up: true785 },786 "w2" ->787 {788 attached: Set(),789 built: false,790 expecting: false,791 running: false,792 session: true,793 up: true794 }795 )796}797798[State 20]799{800 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),801 schedFixed::scheduler::crashes: 2,802 schedFixed::scheduler::entry:803 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],804 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),805 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),806 schedFixed::scheduler::mBuild: Set(),807 schedFixed::scheduler::mDone: Set(),808 schedFixed::scheduler::mExpect: Set("w1"),809 schedFixed::scheduler::mResult: Set(),810 schedFixed::scheduler::mRetry: Set(),811 schedFixed::scheduler::mRevoke: Set(),812 schedFixed::scheduler::mSchedule: Set(),813 schedFixed::scheduler::published: 0,814 schedFixed::scheduler::publishedBy: Set(),815 schedFixed::scheduler::ws:816 Map(817 "w1" ->818 {819 attached: Set(),820 built: false,821 expecting: false,822 running: false,823 session: true,824 up: true825 },826 "w2" ->827 {828 attached: Set(),829 built: false,830 expecting: false,831 running: false,832 session: true,833 up: true834 }835 )836}837838[State 21]839{840 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),841 schedFixed::scheduler::crashes: 2,842 schedFixed::scheduler::entry:843 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],844 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),845 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),846 schedFixed::scheduler::mBuild: Set(("c1", "w1")),847 schedFixed::scheduler::mDone: Set(),848 schedFixed::scheduler::mExpect: Set("w1"),849 schedFixed::scheduler::mResult: Set(),850 schedFixed::scheduler::mRetry: Set(),851 schedFixed::scheduler::mRevoke: Set(),852 schedFixed::scheduler::mSchedule: Set(),853 schedFixed::scheduler::published: 0,854 schedFixed::scheduler::publishedBy: Set(),855 schedFixed::scheduler::ws:856 Map(857 "w1" ->858 {859 attached: Set(),860 built: false,861 expecting: false,862 running: false,863 session: true,864 up: true865 },866 "w2" ->867 {868 attached: Set(),869 built: false,870 expecting: false,871 running: false,872 session: true,873 up: true874 }875 )876}877878[State 22]879{880 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),881 schedFixed::scheduler::crashes: 2,882 schedFixed::scheduler::entry:883 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],884 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),885 schedFixed::scheduler::mAssigned: Set(),886 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),887 schedFixed::scheduler::mDone: Set(),888 schedFixed::scheduler::mExpect: Set("w1"),889 schedFixed::scheduler::mResult: Set(),890 schedFixed::scheduler::mRetry: Set(),891 schedFixed::scheduler::mRevoke: Set(),892 schedFixed::scheduler::mSchedule: Set(),893 schedFixed::scheduler::published: 0,894 schedFixed::scheduler::publishedBy: Set(),895 schedFixed::scheduler::ws:896 Map(897 "w1" ->898 {899 attached: Set(),900 built: false,901 expecting: false,902 running: false,903 session: true,904 up: true905 },906 "w2" ->907 {908 attached: Set(),909 built: false,910 expecting: false,911 running: false,912 session: true,913 up: true914 }915 )916}917918[State 23]919{920 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),921 schedFixed::scheduler::crashes: 2,922 schedFixed::scheduler::entry:923 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],924 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),925 schedFixed::scheduler::mAssigned: Set(),926 schedFixed::scheduler::mBuild: Set(("c1", "w1")),927 schedFixed::scheduler::mDone: Set(),928 schedFixed::scheduler::mExpect: Set("w1"),929 schedFixed::scheduler::mResult: Set(),930 schedFixed::scheduler::mRetry: Set("c2"),931 schedFixed::scheduler::mRevoke: Set(),932 schedFixed::scheduler::mSchedule: Set(),933 schedFixed::scheduler::published: 0,934 schedFixed::scheduler::publishedBy: Set(),935 schedFixed::scheduler::ws:936 Map(937 "w1" ->938 {939 attached: Set(),940 built: false,941 expecting: false,942 running: false,943 session: true,944 up: true945 },946 "w2" ->947 {948 attached: Set(),949 built: false,950 expecting: false,951 running: false,952 session: true,953 up: true954 }955 )956}957958[State 24]959{960 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),961 schedFixed::scheduler::crashes: 2,962 schedFixed::scheduler::entry:963 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],964 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),965 schedFixed::scheduler::mAssigned: Set(),966 schedFixed::scheduler::mBuild: Set(("c1", "w1")),967 schedFixed::scheduler::mDone: Set(),968 schedFixed::scheduler::mExpect: Set("w1"),969 schedFixed::scheduler::mResult: Set(),970 schedFixed::scheduler::mRetry: Set(),971 schedFixed::scheduler::mRevoke: Set(),972 schedFixed::scheduler::mSchedule: Set("c2"),973 schedFixed::scheduler::published: 0,974 schedFixed::scheduler::publishedBy: Set(),975 schedFixed::scheduler::ws:976 Map(977 "w1" ->978 {979 attached: Set(),980 built: false,981 expecting: false,982 running: false,983 session: true,984 up: true985 },986 "w2" ->987 {988 attached: Set(),989 built: false,990 expecting: false,991 running: false,992 session: true,993 up: true994 }995 )996}997998[State 25]999{1000 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),1001 schedFixed::scheduler::crashes: 2,1002 schedFixed::scheduler::entry:1003 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1004 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1005 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1006 schedFixed::scheduler::mBuild: Set(("c1", "w1")),1007 schedFixed::scheduler::mDone: Set(),1008 schedFixed::scheduler::mExpect: Set("w1"),1009 schedFixed::scheduler::mResult: Set(),1010 schedFixed::scheduler::mRetry: Set(),1011 schedFixed::scheduler::mRevoke: Set(),1012 schedFixed::scheduler::mSchedule: Set(),1013 schedFixed::scheduler::published: 0,1014 schedFixed::scheduler::publishedBy: Set(),1015 schedFixed::scheduler::ws:1016 Map(1017 "w1" ->1018 {1019 attached: Set(),1020 built: false,1021 expecting: false,1022 running: false,1023 session: true,1024 up: true1025 },1026 "w2" ->1027 {1028 attached: Set(),1029 built: false,1030 expecting: false,1031 running: false,1032 session: true,1033 up: true1034 }1035 )1036}10371038[State 26]1039{1040 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),1041 schedFixed::scheduler::crashes: 2,1042 schedFixed::scheduler::entry:1043 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1044 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1045 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1046 schedFixed::scheduler::mBuild: Set(("c1", "w1")),1047 schedFixed::scheduler::mDone: Set(),1048 schedFixed::scheduler::mExpect: Set(),1049 schedFixed::scheduler::mResult: Set(),1050 schedFixed::scheduler::mRetry: Set(),1051 schedFixed::scheduler::mRevoke: Set(),1052 schedFixed::scheduler::mSchedule: Set(),1053 schedFixed::scheduler::published: 0,1054 schedFixed::scheduler::publishedBy: Set(),1055 schedFixed::scheduler::ws:1056 Map(1057 "w1" ->1058 {1059 attached: Set(),1060 built: false,1061 expecting: true,1062 running: true,1063 session: true,1064 up: true1065 },1066 "w2" ->1067 {1068 attached: Set(),1069 built: false,1070 expecting: false,1071 running: false,1072 session: true,1073 up: true1074 }1075 )1076}10771078[State 27]1079{1080 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),1081 schedFixed::scheduler::crashes: 2,1082 schedFixed::scheduler::entry:1083 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1084 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1085 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1086 schedFixed::scheduler::mBuild: Set(),1087 schedFixed::scheduler::mDone: Set(),1088 schedFixed::scheduler::mExpect: Set(),1089 schedFixed::scheduler::mResult: Set(),1090 schedFixed::scheduler::mRetry: Set(),1091 schedFixed::scheduler::mRevoke: Set(),1092 schedFixed::scheduler::mSchedule: Set(),1093 schedFixed::scheduler::published: 0,1094 schedFixed::scheduler::publishedBy: Set(),1095 schedFixed::scheduler::ws:1096 Map(1097 "w1" ->1098 {1099 attached: Set("c1"),1100 built: false,1101 expecting: true,1102 running: true,1103 session: true,1104 up: true1105 },1106 "w2" ->1107 {1108 attached: Set(),1109 built: false,1110 expecting: false,1111 running: false,1112 session: true,1113 up: true1114 }1115 )1116}11171118[State 28]1119{1120 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1121 schedFixed::scheduler::crashes: 2,1122 schedFixed::scheduler::entry:1123 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1124 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1125 schedFixed::scheduler::mAssigned: Set(),1126 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1127 schedFixed::scheduler::mDone: Set(),1128 schedFixed::scheduler::mExpect: Set(),1129 schedFixed::scheduler::mResult: Set(),1130 schedFixed::scheduler::mRetry: Set(),1131 schedFixed::scheduler::mRevoke: Set(),1132 schedFixed::scheduler::mSchedule: Set(),1133 schedFixed::scheduler::published: 0,1134 schedFixed::scheduler::publishedBy: Set(),1135 schedFixed::scheduler::ws:1136 Map(1137 "w1" ->1138 {1139 attached: Set("c1"),1140 built: false,1141 expecting: true,1142 running: true,1143 session: true,1144 up: true1145 },1146 "w2" ->1147 {1148 attached: Set(),1149 built: false,1150 expecting: false,1151 running: false,1152 session: true,1153 up: true1154 }1155 )1156}11571158[State 29]1159{1160 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1161 schedFixed::scheduler::crashes: 2,1162 schedFixed::scheduler::entry:1163 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1164 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1165 schedFixed::scheduler::mAssigned: Set(),1166 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1167 schedFixed::scheduler::mDone: Set("w1"),1168 schedFixed::scheduler::mExpect: Set(),1169 schedFixed::scheduler::mResult: Set("c1"),1170 schedFixed::scheduler::mRetry: Set(),1171 schedFixed::scheduler::mRevoke: Set(),1172 schedFixed::scheduler::mSchedule: Set(),1173 schedFixed::scheduler::published: 1,1174 schedFixed::scheduler::publishedBy: Set("w1"),1175 schedFixed::scheduler::ws:1176 Map(1177 "w1" ->1178 {1179 attached: Set(),1180 built: true,1181 expecting: false,1182 running: false,1183 session: true,1184 up: true1185 },1186 "w2" ->1187 {1188 attached: Set(),1189 built: false,1190 expecting: false,1191 running: false,1192 session: true,1193 up: true1194 }1195 )1196}11971198[State 30]1199{1200 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1201 schedFixed::scheduler::crashes: 2,1202 schedFixed::scheduler::entry:1203 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1204 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1205 schedFixed::scheduler::mAssigned: Set(),1206 schedFixed::scheduler::mBuild: Set(),1207 schedFixed::scheduler::mDone: Set("w1"),1208 schedFixed::scheduler::mExpect: Set(),1209 schedFixed::scheduler::mResult: Set("c1", "c2"),1210 schedFixed::scheduler::mRetry: Set(),1211 schedFixed::scheduler::mRevoke: Set(),1212 schedFixed::scheduler::mSchedule: Set(),1213 schedFixed::scheduler::published: 1,1214 schedFixed::scheduler::publishedBy: Set("w1"),1215 schedFixed::scheduler::ws:1216 Map(1217 "w1" ->1218 {1219 attached: Set(),1220 built: true,1221 expecting: false,1222 running: false,1223 session: true,1224 up: true1225 },1226 "w2" ->1227 {1228 attached: Set(),1229 built: false,1230 expecting: false,1231 running: false,1232 session: true,1233 up: true1234 }1235 )1236}12371238[ok] No violation found (13504ms at 2222 traces/second).1239Trace length statistics: max=31, min=15, average=18.841240You may increase --max-samples and --max-steps.1241Use --verbosity to produce more (or less) output.1242Use --seed=0xc169b276ba11cf8e --backend=rust to reproduce.1243An example execution:12441245[State 0]1246{1247 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1248 schedNoRevoke::scheduler::crashes: 0,1249 schedNoRevoke::scheduler::entry: [],1250 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1251 schedNoRevoke::scheduler::mAssigned: Set(),1252 schedNoRevoke::scheduler::mBuild: Set(),1253 schedNoRevoke::scheduler::mDone: Set(),1254 schedNoRevoke::scheduler::mExpect: Set(),1255 schedNoRevoke::scheduler::mResult: Set(),1256 schedNoRevoke::scheduler::mRetry: Set(),1257 schedNoRevoke::scheduler::mRevoke: Set(),1258 schedNoRevoke::scheduler::mSchedule: Set(),1259 schedNoRevoke::scheduler::published: 0,1260 schedNoRevoke::scheduler::publishedBy: Set(),1261 schedNoRevoke::scheduler::ws:1262 Map(1263 "w1" ->1264 {1265 attached: Set(),1266 built: false,1267 expecting: false,1268 running: false,1269 session: true,1270 up: true1271 },1272 "w2" ->1273 {1274 attached: Set(),1275 built: false,1276 expecting: false,1277 running: false,1278 session: true,1279 up: true1280 }1281 )1282}12831284[State 1]1285{1286 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1287 schedNoRevoke::scheduler::crashes: 1,1288 schedNoRevoke::scheduler::entry: [],1289 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1290 schedNoRevoke::scheduler::mAssigned: Set(),1291 schedNoRevoke::scheduler::mBuild: Set(),1292 schedNoRevoke::scheduler::mDone: Set(),1293 schedNoRevoke::scheduler::mExpect: Set(),1294 schedNoRevoke::scheduler::mResult: Set(),1295 schedNoRevoke::scheduler::mRetry: Set(),1296 schedNoRevoke::scheduler::mRevoke: Set(),1297 schedNoRevoke::scheduler::mSchedule: Set(),1298 schedNoRevoke::scheduler::published: 0,1299 schedNoRevoke::scheduler::publishedBy: Set(),1300 schedNoRevoke::scheduler::ws:1301 Map(1302 "w1" ->1303 {1304 attached: Set(),1305 built: false,1306 expecting: false,1307 running: false,1308 session: false,1309 up: false1310 },1311 "w2" ->1312 {1313 attached: Set(),1314 built: false,1315 expecting: false,1316 running: false,1317 session: true,1318 up: true1319 }1320 )1321}13221323[State 2]1324{1325 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1326 schedNoRevoke::scheduler::crashes: 1,1327 schedNoRevoke::scheduler::entry: [],1328 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1329 schedNoRevoke::scheduler::mAssigned: Set(),1330 schedNoRevoke::scheduler::mBuild: Set(),1331 schedNoRevoke::scheduler::mDone: Set(),1332 schedNoRevoke::scheduler::mExpect: Set(),1333 schedNoRevoke::scheduler::mResult: Set(),1334 schedNoRevoke::scheduler::mRetry: Set(),1335 schedNoRevoke::scheduler::mRevoke: Set(),1336 schedNoRevoke::scheduler::mSchedule: Set("c2"),1337 schedNoRevoke::scheduler::published: 0,1338 schedNoRevoke::scheduler::publishedBy: Set(),1339 schedNoRevoke::scheduler::ws:1340 Map(1341 "w1" ->1342 {1343 attached: Set(),1344 built: false,1345 expecting: false,1346 running: false,1347 session: false,1348 up: false1349 },1350 "w2" ->1351 {1352 attached: Set(),1353 built: false,1354 expecting: false,1355 running: false,1356 session: true,1357 up: true1358 }1359 )1360}13611362[State 3]1363{1364 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1365 schedNoRevoke::scheduler::crashes: 1,1366 schedNoRevoke::scheduler::entry:1367 [{ followers: Set("c2"), leased: true, worker: "w2" }],1368 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1369 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1370 schedNoRevoke::scheduler::mBuild: Set(),1371 schedNoRevoke::scheduler::mDone: Set(),1372 schedNoRevoke::scheduler::mExpect: Set("w2"),1373 schedNoRevoke::scheduler::mResult: Set(),1374 schedNoRevoke::scheduler::mRetry: Set(),1375 schedNoRevoke::scheduler::mRevoke: Set(),1376 schedNoRevoke::scheduler::mSchedule: Set(),1377 schedNoRevoke::scheduler::published: 0,1378 schedNoRevoke::scheduler::publishedBy: Set(),1379 schedNoRevoke::scheduler::ws:1380 Map(1381 "w1" ->1382 {1383 attached: Set(),1384 built: false,1385 expecting: false,1386 running: false,1387 session: false,1388 up: false1389 },1390 "w2" ->1391 {1392 attached: Set(),1393 built: false,1394 expecting: false,1395 running: false,1396 session: true,1397 up: true1398 }1399 )1400}14011402[State 4]1403{1404 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1405 schedNoRevoke::scheduler::crashes: 1,1406 schedNoRevoke::scheduler::entry:1407 [{ followers: Set("c2"), leased: true, worker: "w2" }],1408 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1409 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1410 schedNoRevoke::scheduler::mBuild: Set(),1411 schedNoRevoke::scheduler::mDone: Set(),1412 schedNoRevoke::scheduler::mExpect: Set(),1413 schedNoRevoke::scheduler::mResult: Set(),1414 schedNoRevoke::scheduler::mRetry: Set(),1415 schedNoRevoke::scheduler::mRevoke: Set(),1416 schedNoRevoke::scheduler::mSchedule: Set(),1417 schedNoRevoke::scheduler::published: 0,1418 schedNoRevoke::scheduler::publishedBy: Set(),1419 schedNoRevoke::scheduler::ws:1420 Map(1421 "w1" ->1422 {1423 attached: Set(),1424 built: false,1425 expecting: false,1426 running: false,1427 session: false,1428 up: false1429 },1430 "w2" ->1431 {1432 attached: Set(),1433 built: false,1434 expecting: true,1435 running: true,1436 session: true,1437 up: true1438 }1439 )1440}14411442[State 5]1443{1444 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1445 schedNoRevoke::scheduler::crashes: 2,1446 schedNoRevoke::scheduler::entry: [],1447 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1448 schedNoRevoke::scheduler::mAssigned: Set(),1449 schedNoRevoke::scheduler::mBuild: Set(),1450 schedNoRevoke::scheduler::mDone: Set(),1451 schedNoRevoke::scheduler::mExpect: Set(),1452 schedNoRevoke::scheduler::mResult: Set(),1453 schedNoRevoke::scheduler::mRetry: Set("c2"),1454 schedNoRevoke::scheduler::mRevoke: Set(),1455 schedNoRevoke::scheduler::mSchedule: Set(),1456 schedNoRevoke::scheduler::published: 0,1457 schedNoRevoke::scheduler::publishedBy: Set(),1458 schedNoRevoke::scheduler::ws:1459 Map(1460 "w1" ->1461 {1462 attached: Set(),1463 built: false,1464 expecting: false,1465 running: false,1466 session: false,1467 up: false1468 },1469 "w2" ->1470 {1471 attached: Set(),1472 built: false,1473 expecting: true,1474 running: true,1475 session: false,1476 up: true1477 }1478 )1479}14801481[State 6]1482{1483 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1484 schedNoRevoke::scheduler::crashes: 2,1485 schedNoRevoke::scheduler::entry: [],1486 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1487 schedNoRevoke::scheduler::mAssigned: Set(),1488 schedNoRevoke::scheduler::mBuild: Set(),1489 schedNoRevoke::scheduler::mDone: Set(),1490 schedNoRevoke::scheduler::mExpect: Set(),1491 schedNoRevoke::scheduler::mResult: Set(),1492 schedNoRevoke::scheduler::mRetry: Set("c2"),1493 schedNoRevoke::scheduler::mRevoke: Set(),1494 schedNoRevoke::scheduler::mSchedule: Set(),1495 schedNoRevoke::scheduler::published: 0,1496 schedNoRevoke::scheduler::publishedBy: Set(),1497 schedNoRevoke::scheduler::ws:1498 Map(1499 "w1" ->1500 {1501 attached: Set(),1502 built: false,1503 expecting: false,1504 running: false,1505 session: true,1506 up: true1507 },1508 "w2" ->1509 {1510 attached: Set(),1511 built: false,1512 expecting: true,1513 running: true,1514 session: false,1515 up: true1516 }1517 )1518}15191520[State 7]1521{1522 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1523 schedNoRevoke::scheduler::crashes: 2,1524 schedNoRevoke::scheduler::entry: [],1525 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1526 schedNoRevoke::scheduler::mAssigned: Set(),1527 schedNoRevoke::scheduler::mBuild: Set(),1528 schedNoRevoke::scheduler::mDone: Set(),1529 schedNoRevoke::scheduler::mExpect: Set(),1530 schedNoRevoke::scheduler::mResult: Set(),1531 schedNoRevoke::scheduler::mRetry: Set(),1532 schedNoRevoke::scheduler::mRevoke: Set(),1533 schedNoRevoke::scheduler::mSchedule: Set("c2"),1534 schedNoRevoke::scheduler::published: 0,1535 schedNoRevoke::scheduler::publishedBy: Set(),1536 schedNoRevoke::scheduler::ws:1537 Map(1538 "w1" ->1539 {1540 attached: Set(),1541 built: false,1542 expecting: false,1543 running: false,1544 session: true,1545 up: true1546 },1547 "w2" ->1548 {1549 attached: Set(),1550 built: false,1551 expecting: true,1552 running: true,1553 session: false,1554 up: true1555 }1556 )1557}15581559[State 8]1560{1561 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1562 schedNoRevoke::scheduler::crashes: 2,1563 schedNoRevoke::scheduler::entry:1564 [{ followers: Set("c2"), leased: true, worker: "w1" }],1565 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1566 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1567 schedNoRevoke::scheduler::mBuild: Set(),1568 schedNoRevoke::scheduler::mDone: Set(),1569 schedNoRevoke::scheduler::mExpect: Set("w1"),1570 schedNoRevoke::scheduler::mResult: Set(),1571 schedNoRevoke::scheduler::mRetry: Set(),1572 schedNoRevoke::scheduler::mRevoke: Set(),1573 schedNoRevoke::scheduler::mSchedule: Set(),1574 schedNoRevoke::scheduler::published: 0,1575 schedNoRevoke::scheduler::publishedBy: Set(),1576 schedNoRevoke::scheduler::ws:1577 Map(1578 "w1" ->1579 {1580 attached: Set(),1581 built: false,1582 expecting: false,1583 running: false,1584 session: true,1585 up: true1586 },1587 "w2" ->1588 {1589 attached: Set(),1590 built: false,1591 expecting: true,1592 running: true,1593 session: false,1594 up: true1595 }1596 )1597}15981599[State 9]1600{1601 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1602 schedNoRevoke::scheduler::crashes: 2,1603 schedNoRevoke::scheduler::entry:1604 [{ followers: Set("c2"), leased: true, worker: "w1" }],1605 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1606 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1607 schedNoRevoke::scheduler::mBuild: Set(),1608 schedNoRevoke::scheduler::mDone: Set(),1609 schedNoRevoke::scheduler::mExpect: Set("w1"),1610 schedNoRevoke::scheduler::mResult: Set(),1611 schedNoRevoke::scheduler::mRetry: Set(),1612 schedNoRevoke::scheduler::mRevoke: Set(),1613 schedNoRevoke::scheduler::mSchedule: Set("c1"),1614 schedNoRevoke::scheduler::published: 0,1615 schedNoRevoke::scheduler::publishedBy: Set(),1616 schedNoRevoke::scheduler::ws:1617 Map(1618 "w1" ->1619 {1620 attached: Set(),1621 built: false,1622 expecting: false,1623 running: false,1624 session: true,1625 up: true1626 },1627 "w2" ->1628 {1629 attached: Set(),1630 built: false,1631 expecting: true,1632 running: true,1633 session: false,1634 up: true1635 }1636 )1637}16381639[State 10]1640{1641 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1642 schedNoRevoke::scheduler::crashes: 2,1643 schedNoRevoke::scheduler::entry:1644 [{ followers: Set("c2"), leased: true, worker: "w1" }],1645 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1646 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1647 schedNoRevoke::scheduler::mBuild: Set(),1648 schedNoRevoke::scheduler::mDone: Set(),1649 schedNoRevoke::scheduler::mExpect: Set(),1650 schedNoRevoke::scheduler::mResult: Set(),1651 schedNoRevoke::scheduler::mRetry: Set(),1652 schedNoRevoke::scheduler::mRevoke: Set(),1653 schedNoRevoke::scheduler::mSchedule: Set("c1"),1654 schedNoRevoke::scheduler::published: 0,1655 schedNoRevoke::scheduler::publishedBy: Set(),1656 schedNoRevoke::scheduler::ws:1657 Map(1658 "w1" ->1659 {1660 attached: Set(),1661 built: false,1662 expecting: true,1663 running: true,1664 session: true,1665 up: true1666 },1667 "w2" ->1668 {1669 attached: Set(),1670 built: false,1671 expecting: true,1672 running: true,1673 session: false,1674 up: true1675 }1676 )1677}16781679[State 11]1680{1681 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1682 schedNoRevoke::scheduler::crashes: 2,1683 schedNoRevoke::scheduler::entry:1684 [{ followers: Set("c2"), leased: true, worker: "w1" }],1685 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1686 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1687 schedNoRevoke::scheduler::mBuild: Set(),1688 schedNoRevoke::scheduler::mDone: Set(),1689 schedNoRevoke::scheduler::mExpect: Set(),1690 schedNoRevoke::scheduler::mResult: Set(),1691 schedNoRevoke::scheduler::mRetry: Set(),1692 schedNoRevoke::scheduler::mRevoke: Set(),1693 schedNoRevoke::scheduler::mSchedule: Set("c1"),1694 schedNoRevoke::scheduler::published: 0,1695 schedNoRevoke::scheduler::publishedBy: Set(),1696 schedNoRevoke::scheduler::ws:1697 Map(1698 "w1" ->1699 {1700 attached: Set(),1701 built: false,1702 expecting: true,1703 running: true,1704 session: true,1705 up: true1706 },1707 "w2" ->1708 {1709 attached: Set(),1710 built: false,1711 expecting: true,1712 running: true,1713 session: true,1714 up: true1715 }1716 )1717}17181719[violation] Found an issue (6787ms at 1737 traces/second).1720Use --verbosity=3 to show executions.1721Use --seed=0xc8284d88118d6d38 --backend=rust to reproduce.1722error: Invariant violated1723An example execution:17241725[State 0]1726{1727 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1728 schedNoFence::scheduler::crashes: 0,1729 schedNoFence::scheduler::entry: [],1730 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1731 schedNoFence::scheduler::mAssigned: Set(),1732 schedNoFence::scheduler::mBuild: Set(),1733 schedNoFence::scheduler::mDone: Set(),1734 schedNoFence::scheduler::mExpect: Set(),1735 schedNoFence::scheduler::mResult: Set(),1736 schedNoFence::scheduler::mRetry: Set(),1737 schedNoFence::scheduler::mRevoke: Set(),1738 schedNoFence::scheduler::mSchedule: Set(),1739 schedNoFence::scheduler::published: 0,1740 schedNoFence::scheduler::publishedBy: Set(),1741 schedNoFence::scheduler::ws:1742 Map(1743 "w1" ->1744 {1745 attached: Set(),1746 built: false,1747 expecting: false,1748 running: false,1749 session: true,1750 up: true1751 },1752 "w2" ->1753 {1754 attached: Set(),1755 built: false,1756 expecting: false,1757 running: false,1758 session: true,1759 up: true1760 }1761 )1762}17631764[State 1]1765{1766 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1767 schedNoFence::scheduler::crashes: 0,1768 schedNoFence::scheduler::entry: [],1769 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1770 schedNoFence::scheduler::mAssigned: Set(),1771 schedNoFence::scheduler::mBuild: Set(),1772 schedNoFence::scheduler::mDone: Set(),1773 schedNoFence::scheduler::mExpect: Set(),1774 schedNoFence::scheduler::mResult: Set(),1775 schedNoFence::scheduler::mRetry: Set(),1776 schedNoFence::scheduler::mRevoke: Set(),1777 schedNoFence::scheduler::mSchedule: Set("c1"),1778 schedNoFence::scheduler::published: 0,1779 schedNoFence::scheduler::publishedBy: Set(),1780 schedNoFence::scheduler::ws:1781 Map(1782 "w1" ->1783 {1784 attached: Set(),1785 built: false,1786 expecting: false,1787 running: false,1788 session: true,1789 up: true1790 },1791 "w2" ->1792 {1793 attached: Set(),1794 built: false,1795 expecting: false,1796 running: false,1797 session: true,1798 up: true1799 }1800 )1801}18021803[State 2]1804{1805 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1806 schedNoFence::scheduler::crashes: 0,1807 schedNoFence::scheduler::entry:1808 [{ followers: Set("c1"), leased: true, worker: "w1" }],1809 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1810 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1811 schedNoFence::scheduler::mBuild: Set(),1812 schedNoFence::scheduler::mDone: Set(),1813 schedNoFence::scheduler::mExpect: Set("w1"),1814 schedNoFence::scheduler::mResult: Set(),1815 schedNoFence::scheduler::mRetry: Set(),1816 schedNoFence::scheduler::mRevoke: Set(),1817 schedNoFence::scheduler::mSchedule: Set(),1818 schedNoFence::scheduler::published: 0,1819 schedNoFence::scheduler::publishedBy: Set(),1820 schedNoFence::scheduler::ws:1821 Map(1822 "w1" ->1823 {1824 attached: Set(),1825 built: false,1826 expecting: false,1827 running: false,1828 session: true,1829 up: true1830 },1831 "w2" ->1832 {1833 attached: Set(),1834 built: false,1835 expecting: false,1836 running: false,1837 session: true,1838 up: true1839 }1840 )1841}18421843[State 3]1844{1845 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1846 schedNoFence::scheduler::crashes: 0,1847 schedNoFence::scheduler::entry:1848 [{ followers: Set("c1"), leased: true, worker: "w1" }],1849 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1850 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1851 schedNoFence::scheduler::mBuild: Set(),1852 schedNoFence::scheduler::mDone: Set(),1853 schedNoFence::scheduler::mExpect: Set(),1854 schedNoFence::scheduler::mResult: Set(),1855 schedNoFence::scheduler::mRetry: Set(),1856 schedNoFence::scheduler::mRevoke: Set(),1857 schedNoFence::scheduler::mSchedule: Set(),1858 schedNoFence::scheduler::published: 0,1859 schedNoFence::scheduler::publishedBy: Set(),1860 schedNoFence::scheduler::ws:1861 Map(1862 "w1" ->1863 {1864 attached: Set(),1865 built: false,1866 expecting: true,1867 running: true,1868 session: true,1869 up: true1870 },1871 "w2" ->1872 {1873 attached: Set(),1874 built: false,1875 expecting: false,1876 running: false,1877 session: true,1878 up: true1879 }1880 )1881}18821883[State 4]1884{1885 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1886 schedNoFence::scheduler::crashes: 0,1887 schedNoFence::scheduler::entry:1888 [{ followers: Set("c1"), leased: true, worker: "w1" }],1889 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1890 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1891 schedNoFence::scheduler::mBuild: Set(),1892 schedNoFence::scheduler::mDone: Set(),1893 schedNoFence::scheduler::mExpect: Set(),1894 schedNoFence::scheduler::mResult: Set(),1895 schedNoFence::scheduler::mRetry: Set(),1896 schedNoFence::scheduler::mRevoke: Set(),1897 schedNoFence::scheduler::mSchedule: Set("c2"),1898 schedNoFence::scheduler::published: 0,1899 schedNoFence::scheduler::publishedBy: Set(),1900 schedNoFence::scheduler::ws:1901 Map(1902 "w1" ->1903 {1904 attached: Set(),1905 built: false,1906 expecting: true,1907 running: true,1908 session: true,1909 up: true1910 },1911 "w2" ->1912 {1913 attached: Set(),1914 built: false,1915 expecting: false,1916 running: false,1917 session: true,1918 up: true1919 }1920 )1921}19221923[State 5]1924{1925 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1926 schedNoFence::scheduler::crashes: 1,1927 schedNoFence::scheduler::entry: [],1928 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1929 schedNoFence::scheduler::mAssigned: Set(),1930 schedNoFence::scheduler::mBuild: Set(),1931 schedNoFence::scheduler::mDone: Set(),1932 schedNoFence::scheduler::mExpect: Set(),1933 schedNoFence::scheduler::mResult: Set(),1934 schedNoFence::scheduler::mRetry: Set("c1", "c2"),1935 schedNoFence::scheduler::mRevoke: Set(),1936 schedNoFence::scheduler::mSchedule: Set(),1937 schedNoFence::scheduler::published: 0,1938 schedNoFence::scheduler::publishedBy: Set(),1939 schedNoFence::scheduler::ws:1940 Map(1941 "w1" ->1942 {1943 attached: Set(),1944 built: false,1945 expecting: true,1946 running: true,1947 session: false,1948 up: true1949 },1950 "w2" ->1951 {1952 attached: Set(),1953 built: false,1954 expecting: false,1955 running: false,1956 session: false,1957 up: true1958 }1959 )1960}19611962[State 6]1963{1964 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1965 schedNoFence::scheduler::crashes: 2,1966 schedNoFence::scheduler::entry: [],1967 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1968 schedNoFence::scheduler::mAssigned: Set(),1969 schedNoFence::scheduler::mBuild: Set(),1970 schedNoFence::scheduler::mDone: Set(),1971 schedNoFence::scheduler::mExpect: Set(),1972 schedNoFence::scheduler::mResult: Set(),1973 schedNoFence::scheduler::mRetry: Set("c1", "c2"),1974 schedNoFence::scheduler::mRevoke: Set(),1975 schedNoFence::scheduler::mSchedule: Set(),1976 schedNoFence::scheduler::published: 0,1977 schedNoFence::scheduler::publishedBy: Set(),1978 schedNoFence::scheduler::ws:1979 Map(1980 "w1" ->1981 {1982 attached: Set(),1983 built: false,1984 expecting: true,1985 running: true,1986 session: false,1987 up: true1988 },1989 "w2" ->1990 {1991 attached: Set(),1992 built: false,1993 expecting: false,1994 running: false,1995 session: false,1996 up: true1997 }1998 )1999}20002001[State 7]2002{2003 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2004 schedNoFence::scheduler::crashes: 2,2005 schedNoFence::scheduler::entry: [],2006 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),2007 schedNoFence::scheduler::mAssigned: Set(),2008 schedNoFence::scheduler::mBuild: Set(),2009 schedNoFence::scheduler::mDone: Set(),2010 schedNoFence::scheduler::mExpect: Set(),2011 schedNoFence::scheduler::mResult: Set(),2012 schedNoFence::scheduler::mRetry: Set("c1"),2013 schedNoFence::scheduler::mRevoke: Set(),2014 schedNoFence::scheduler::mSchedule: Set("c2"),2015 schedNoFence::scheduler::published: 0,2016 schedNoFence::scheduler::publishedBy: Set(),2017 schedNoFence::scheduler::ws:2018 Map(2019 "w1" ->2020 {2021 attached: Set(),2022 built: false,2023 expecting: true,2024 running: true,2025 session: false,2026 up: true2027 },2028 "w2" ->2029 {2030 attached: Set(),2031 built: false,2032 expecting: false,2033 running: false,2034 session: false,2035 up: true2036 }2037 )2038}20392040[State 8]2041{2042 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2043 schedNoFence::scheduler::crashes: 2,2044 schedNoFence::scheduler::entry: [],2045 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),2046 schedNoFence::scheduler::mAssigned: Set(),2047 schedNoFence::scheduler::mBuild: Set(),2048 schedNoFence::scheduler::mDone: Set(),2049 schedNoFence::scheduler::mExpect: Set(),2050 schedNoFence::scheduler::mResult: Set(),2051 schedNoFence::scheduler::mRetry: Set("c1"),2052 schedNoFence::scheduler::mRevoke: Set(),2053 schedNoFence::scheduler::mSchedule: Set("c2"),2054 schedNoFence::scheduler::published: 0,2055 schedNoFence::scheduler::publishedBy: Set(),2056 schedNoFence::scheduler::ws:2057 Map(2058 "w1" ->2059 {2060 attached: Set(),2061 built: false,2062 expecting: true,2063 running: true,2064 session: false,2065 up: true2066 },2067 "w2" ->2068 {2069 attached: Set(),2070 built: false,2071 expecting: false,2072 running: false,2073 session: true,2074 up: true2075 }2076 )2077}20782079[State 9]2080{2081 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2082 schedNoFence::scheduler::crashes: 2,2083 schedNoFence::scheduler::entry:2084 [{ followers: Set("c2"), leased: true, worker: "w2" }],2085 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2086 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2087 schedNoFence::scheduler::mBuild: Set(),2088 schedNoFence::scheduler::mDone: Set(),2089 schedNoFence::scheduler::mExpect: Set("w2"),2090 schedNoFence::scheduler::mResult: Set(),2091 schedNoFence::scheduler::mRetry: Set("c1"),2092 schedNoFence::scheduler::mRevoke: Set(),2093 schedNoFence::scheduler::mSchedule: Set(),2094 schedNoFence::scheduler::published: 0,2095 schedNoFence::scheduler::publishedBy: Set(),2096 schedNoFence::scheduler::ws:2097 Map(2098 "w1" ->2099 {2100 attached: Set(),2101 built: false,2102 expecting: true,2103 running: true,2104 session: false,2105 up: true2106 },2107 "w2" ->2108 {2109 attached: Set(),2110 built: false,2111 expecting: false,2112 running: false,2113 session: true,2114 up: true2115 }2116 )2117}21182119[State 10]2120{2121 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2122 schedNoFence::scheduler::crashes: 2,2123 schedNoFence::scheduler::entry:2124 [{ followers: Set("c2"), leased: true, worker: "w2" }],2125 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2126 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2127 schedNoFence::scheduler::mBuild: Set(),2128 schedNoFence::scheduler::mDone: Set(),2129 schedNoFence::scheduler::mExpect: Set("w2"),2130 schedNoFence::scheduler::mResult: Set(),2131 schedNoFence::scheduler::mRetry: Set("c1"),2132 schedNoFence::scheduler::mRevoke: Set(),2133 schedNoFence::scheduler::mSchedule: Set(),2134 schedNoFence::scheduler::published: 1,2135 schedNoFence::scheduler::publishedBy: Set("w1"),2136 schedNoFence::scheduler::ws:2137 Map(2138 "w1" ->2139 {2140 attached: Set(),2141 built: true,2142 expecting: false,2143 running: false,2144 session: false,2145 up: true2146 },2147 "w2" ->2148 {2149 attached: Set(),2150 built: false,2151 expecting: false,2152 running: false,2153 session: true,2154 up: true2155 }2156 )2157}21582159[State 11]2160{2161 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2162 schedNoFence::scheduler::crashes: 2,2163 schedNoFence::scheduler::entry:2164 [{ followers: Set("c2"), leased: true, worker: "w2" }],2165 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2166 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2167 schedNoFence::scheduler::mBuild: Set(),2168 schedNoFence::scheduler::mDone: Set(),2169 schedNoFence::scheduler::mExpect: Set("w2"),2170 schedNoFence::scheduler::mResult: Set(),2171 schedNoFence::scheduler::mRetry: Set(),2172 schedNoFence::scheduler::mRevoke: Set(),2173 schedNoFence::scheduler::mSchedule: Set("c1"),2174 schedNoFence::scheduler::published: 1,2175 schedNoFence::scheduler::publishedBy: Set("w1"),2176 schedNoFence::scheduler::ws:2177 Map(2178 "w1" ->2179 {2180 attached: Set(),2181 built: true,2182 expecting: false,2183 running: false,2184 session: false,2185 up: true2186 },2187 "w2" ->2188 {2189 attached: Set(),2190 built: false,2191 expecting: false,2192 running: false,2193 session: true,2194 up: true2195 }2196 )2197}21982199[State 12]2200{2201 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2202 schedNoFence::scheduler::crashes: 2,2203 schedNoFence::scheduler::entry:2204 [{ followers: Set("c2"), leased: true, worker: "w2" }],2205 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2206 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2207 schedNoFence::scheduler::mBuild: Set(),2208 schedNoFence::scheduler::mDone: Set(),2209 schedNoFence::scheduler::mExpect: Set(),2210 schedNoFence::scheduler::mResult: Set(),2211 schedNoFence::scheduler::mRetry: Set(),2212 schedNoFence::scheduler::mRevoke: Set(),2213 schedNoFence::scheduler::mSchedule: Set("c1"),2214 schedNoFence::scheduler::published: 1,2215 schedNoFence::scheduler::publishedBy: Set("w1"),2216 schedNoFence::scheduler::ws:2217 Map(2218 "w1" ->2219 {2220 attached: Set(),2221 built: true,2222 expecting: false,2223 running: false,2224 session: false,2225 up: true2226 },2227 "w2" ->2228 {2229 attached: Set(),2230 built: false,2231 expecting: true,2232 running: true,2233 session: true,2234 up: true2235 }2236 )2237}22382239[State 13]2240{2241 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2242 schedNoFence::scheduler::crashes: 2,2243 schedNoFence::scheduler::entry:2244 [{ followers: Set("c2"), leased: true, worker: "w2" }],2245 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2246 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2247 schedNoFence::scheduler::mBuild: Set(),2248 schedNoFence::scheduler::mDone: Set("w2"),2249 schedNoFence::scheduler::mExpect: Set(),2250 schedNoFence::scheduler::mResult: Set(),2251 schedNoFence::scheduler::mRetry: Set(),2252 schedNoFence::scheduler::mRevoke: Set(),2253 schedNoFence::scheduler::mSchedule: Set("c1"),2254 schedNoFence::scheduler::published: 2,2255 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2256 schedNoFence::scheduler::ws:2257 Map(2258 "w1" ->2259 {2260 attached: Set(),2261 built: true,2262 expecting: false,2263 running: false,2264 session: false,2265 up: true2266 },2267 "w2" ->2268 {2269 attached: Set(),2270 built: true,2271 expecting: false,2272 running: false,2273 session: true,2274 up: true2275 }2276 )2277}22782279[violation] Found an issue (2759ms at 1900 traces/second).2280Use --verbosity=3 to show executions.2281Use --seed=0xcc51f9f31a2ed667 --backend=rust to reproduce.2282error: Invariant violated2283An example execution:22842285[State 0]2286{2287 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2288 schedNoPush::scheduler::crashes: 0,2289 schedNoPush::scheduler::entry: [],2290 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2291 schedNoPush::scheduler::mAssigned: Set(),2292 schedNoPush::scheduler::mBuild: Set(),2293 schedNoPush::scheduler::mDone: Set(),2294 schedNoPush::scheduler::mExpect: Set(),2295 schedNoPush::scheduler::mResult: Set(),2296 schedNoPush::scheduler::mRetry: Set(),2297 schedNoPush::scheduler::mRevoke: Set(),2298 schedNoPush::scheduler::mSchedule: Set(),2299 schedNoPush::scheduler::published: 0,2300 schedNoPush::scheduler::publishedBy: Set(),2301 schedNoPush::scheduler::ws:2302 Map(2303 "w1" ->2304 {2305 attached: Set(),2306 built: false,2307 expecting: false,2308 running: false,2309 session: true,2310 up: true2311 },2312 "w2" ->2313 {2314 attached: Set(),2315 built: false,2316 expecting: false,2317 running: false,2318 session: true,2319 up: true2320 }2321 )2322}23232324[State 1]2325{2326 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2327 schedNoPush::scheduler::crashes: 0,2328 schedNoPush::scheduler::entry: [],2329 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2330 schedNoPush::scheduler::mAssigned: Set(),2331 schedNoPush::scheduler::mBuild: Set(),2332 schedNoPush::scheduler::mDone: Set(),2333 schedNoPush::scheduler::mExpect: Set(),2334 schedNoPush::scheduler::mResult: Set(),2335 schedNoPush::scheduler::mRetry: Set(),2336 schedNoPush::scheduler::mRevoke: Set(),2337 schedNoPush::scheduler::mSchedule: Set("c2"),2338 schedNoPush::scheduler::published: 0,2339 schedNoPush::scheduler::publishedBy: Set(),2340 schedNoPush::scheduler::ws:2341 Map(2342 "w1" ->2343 {2344 attached: Set(),2345 built: false,2346 expecting: false,2347 running: false,2348 session: true,2349 up: true2350 },2351 "w2" ->2352 {2353 attached: Set(),2354 built: false,2355 expecting: false,2356 running: false,2357 session: true,2358 up: true2359 }2360 )2361}23622363[State 2]2364{2365 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2366 schedNoPush::scheduler::crashes: 1,2367 schedNoPush::scheduler::entry: [],2368 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2369 schedNoPush::scheduler::mAssigned: Set(),2370 schedNoPush::scheduler::mBuild: Set(),2371 schedNoPush::scheduler::mDone: Set(),2372 schedNoPush::scheduler::mExpect: Set(),2373 schedNoPush::scheduler::mResult: Set(),2374 schedNoPush::scheduler::mRetry: Set(),2375 schedNoPush::scheduler::mRevoke: Set(),2376 schedNoPush::scheduler::mSchedule: Set("c2"),2377 schedNoPush::scheduler::published: 0,2378 schedNoPush::scheduler::publishedBy: Set(),2379 schedNoPush::scheduler::ws:2380 Map(2381 "w1" ->2382 {2383 attached: Set(),2384 built: false,2385 expecting: false,2386 running: false,2387 session: false,2388 up: false2389 },2390 "w2" ->2391 {2392 attached: Set(),2393 built: false,2394 expecting: false,2395 running: false,2396 session: true,2397 up: true2398 }2399 )2400}24012402[State 3]2403{2404 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2405 schedNoPush::scheduler::crashes: 1,2406 schedNoPush::scheduler::entry:2407 [{ followers: Set("c2"), leased: true, worker: "w2" }],2408 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2409 schedNoPush::scheduler::mAssigned: Set(("c2", "w2")),2410 schedNoPush::scheduler::mBuild: Set(),2411 schedNoPush::scheduler::mDone: Set(),2412 schedNoPush::scheduler::mExpect: Set(),2413 schedNoPush::scheduler::mResult: Set(),2414 schedNoPush::scheduler::mRetry: Set(),2415 schedNoPush::scheduler::mRevoke: Set(),2416 schedNoPush::scheduler::mSchedule: Set(),2417 schedNoPush::scheduler::published: 0,2418 schedNoPush::scheduler::publishedBy: Set(),2419 schedNoPush::scheduler::ws:2420 Map(2421 "w1" ->2422 {2423 attached: Set(),2424 built: false,2425 expecting: false,2426 running: false,2427 session: false,2428 up: false2429 },2430 "w2" ->2431 {2432 attached: Set(),2433 built: false,2434 expecting: false,2435 running: false,2436 session: true,2437 up: true2438 }2439 )2440}24412442[State 4]2443{2444 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2445 schedNoPush::scheduler::crashes: 1,2446 schedNoPush::scheduler::entry:2447 [{ followers: Set("c2"), leased: true, worker: "w2" }],2448 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2449 schedNoPush::scheduler::mAssigned: Set(),2450 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2451 schedNoPush::scheduler::mDone: Set(),2452 schedNoPush::scheduler::mExpect: Set(),2453 schedNoPush::scheduler::mResult: Set(),2454 schedNoPush::scheduler::mRetry: Set(),2455 schedNoPush::scheduler::mRevoke: Set(),2456 schedNoPush::scheduler::mSchedule: Set(),2457 schedNoPush::scheduler::published: 0,2458 schedNoPush::scheduler::publishedBy: Set(),2459 schedNoPush::scheduler::ws:2460 Map(2461 "w1" ->2462 {2463 attached: Set(),2464 built: false,2465 expecting: false,2466 running: false,2467 session: false,2468 up: false2469 },2470 "w2" ->2471 {2472 attached: Set(),2473 built: false,2474 expecting: false,2475 running: false,2476 session: true,2477 up: true2478 }2479 )2480}24812482[State 5]2483{2484 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2485 schedNoPush::scheduler::crashes: 2,2486 schedNoPush::scheduler::entry: [],2487 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2488 schedNoPush::scheduler::mAssigned: Set(),2489 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2490 schedNoPush::scheduler::mDone: Set(),2491 schedNoPush::scheduler::mExpect: Set(),2492 schedNoPush::scheduler::mResult: Set(),2493 schedNoPush::scheduler::mRetry: Set(),2494 schedNoPush::scheduler::mRevoke: Set(),2495 schedNoPush::scheduler::mSchedule: Set(),2496 schedNoPush::scheduler::published: 0,2497 schedNoPush::scheduler::publishedBy: Set(),2498 schedNoPush::scheduler::ws:2499 Map(2500 "w1" ->2501 {2502 attached: Set(),2503 built: false,2504 expecting: false,2505 running: false,2506 session: false,2507 up: false2508 },2509 "w2" ->2510 {2511 attached: Set(),2512 built: false,2513 expecting: false,2514 running: false,2515 session: false,2516 up: true2517 }2518 )2519}25202521[State 6]2522{2523 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2524 schedNoPush::scheduler::crashes: 2,2525 schedNoPush::scheduler::entry: [],2526 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2527 schedNoPush::scheduler::mAssigned: Set(),2528 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2529 schedNoPush::scheduler::mDone: Set(),2530 schedNoPush::scheduler::mExpect: Set(),2531 schedNoPush::scheduler::mResult: Set(),2532 schedNoPush::scheduler::mRetry: Set(),2533 schedNoPush::scheduler::mRevoke: Set(),2534 schedNoPush::scheduler::mSchedule: Set(),2535 schedNoPush::scheduler::published: 0,2536 schedNoPush::scheduler::publishedBy: Set(),2537 schedNoPush::scheduler::ws:2538 Map(2539 "w1" ->2540 {2541 attached: Set(),2542 built: false,2543 expecting: false,2544 running: false,2545 session: false,2546 up: false2547 },2548 "w2" ->2549 {2550 attached: Set(),2551 built: false,2552 expecting: false,2553 running: false,2554 session: true,2555 up: true2556 }2557 )2558}25592560[State 7]2561{2562 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2563 schedNoPush::scheduler::crashes: 2,2564 schedNoPush::scheduler::entry: [],2565 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2566 schedNoPush::scheduler::mAssigned: Set(),2567 schedNoPush::scheduler::mBuild: Set(),2568 schedNoPush::scheduler::mDone: Set(),2569 schedNoPush::scheduler::mExpect: Set(),2570 schedNoPush::scheduler::mResult: Set(),2571 schedNoPush::scheduler::mRetry: Set(),2572 schedNoPush::scheduler::mRevoke: Set(),2573 schedNoPush::scheduler::mSchedule: Set(),2574 schedNoPush::scheduler::published: 0,2575 schedNoPush::scheduler::publishedBy: Set(),2576 schedNoPush::scheduler::ws:2577 Map(2578 "w1" ->2579 {2580 attached: Set(),2581 built: false,2582 expecting: false,2583 running: false,2584 session: false,2585 up: false2586 },2587 "w2" ->2588 {2589 attached: Set("c2"),2590 built: false,2591 expecting: true,2592 running: true,2593 session: true,2594 up: true2595 }2596 )2597}25982599[violation] Found an issue (580ms at 1541 traces/second).2600Use --verbosity=3 to show executions.2601Use --seed=0x1debce2376e217b7 --backend=rust to reproduce.2602error: Invariant violated2603An example execution:26042605[State 0]2606{2607 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2608 schedNoReport::scheduler::crashes: 0,2609 schedNoReport::scheduler::entry: [],2610 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2611 schedNoReport::scheduler::mAssigned: Set(),2612 schedNoReport::scheduler::mBuild: Set(),2613 schedNoReport::scheduler::mDone: Set(),2614 schedNoReport::scheduler::mExpect: Set(),2615 schedNoReport::scheduler::mResult: Set(),2616 schedNoReport::scheduler::mRetry: Set(),2617 schedNoReport::scheduler::mRevoke: Set(),2618 schedNoReport::scheduler::mSchedule: Set(),2619 schedNoReport::scheduler::published: 0,2620 schedNoReport::scheduler::publishedBy: Set(),2621 schedNoReport::scheduler::ws:2622 Map(2623 "w1" ->2624 {2625 attached: Set(),2626 built: false,2627 expecting: false,2628 running: false,2629 session: true,2630 up: true2631 },2632 "w2" ->2633 {2634 attached: Set(),2635 built: false,2636 expecting: false,2637 running: false,2638 session: true,2639 up: true2640 }2641 )2642}26432644[State 1]2645{2646 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2647 schedNoReport::scheduler::crashes: 0,2648 schedNoReport::scheduler::entry: [],2649 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2650 schedNoReport::scheduler::mAssigned: Set(),2651 schedNoReport::scheduler::mBuild: Set(),2652 schedNoReport::scheduler::mDone: Set(),2653 schedNoReport::scheduler::mExpect: Set(),2654 schedNoReport::scheduler::mResult: Set(),2655 schedNoReport::scheduler::mRetry: Set(),2656 schedNoReport::scheduler::mRevoke: Set(),2657 schedNoReport::scheduler::mSchedule: Set("c2"),2658 schedNoReport::scheduler::published: 0,2659 schedNoReport::scheduler::publishedBy: Set(),2660 schedNoReport::scheduler::ws:2661 Map(2662 "w1" ->2663 {2664 attached: Set(),2665 built: false,2666 expecting: false,2667 running: false,2668 session: true,2669 up: true2670 },2671 "w2" ->2672 {2673 attached: Set(),2674 built: false,2675 expecting: false,2676 running: false,2677 session: true,2678 up: true2679 }2680 )2681}26822683[State 2]2684{2685 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2686 schedNoReport::scheduler::crashes: 0,2687 schedNoReport::scheduler::entry:2688 [{ followers: Set("c2"), leased: true, worker: "w1" }],2689 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2690 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2691 schedNoReport::scheduler::mBuild: Set(),2692 schedNoReport::scheduler::mDone: Set(),2693 schedNoReport::scheduler::mExpect: Set("w1"),2694 schedNoReport::scheduler::mResult: Set(),2695 schedNoReport::scheduler::mRetry: Set(),2696 schedNoReport::scheduler::mRevoke: Set(),2697 schedNoReport::scheduler::mSchedule: Set(),2698 schedNoReport::scheduler::published: 0,2699 schedNoReport::scheduler::publishedBy: Set(),2700 schedNoReport::scheduler::ws:2701 Map(2702 "w1" ->2703 {2704 attached: Set(),2705 built: false,2706 expecting: false,2707 running: false,2708 session: true,2709 up: true2710 },2711 "w2" ->2712 {2713 attached: Set(),2714 built: false,2715 expecting: false,2716 running: false,2717 session: true,2718 up: true2719 }2720 )2721}27222723[State 3]2724{2725 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2726 schedNoReport::scheduler::crashes: 0,2727 schedNoReport::scheduler::entry:2728 [{ followers: Set("c2"), leased: true, worker: "w1" }],2729 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2730 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2731 schedNoReport::scheduler::mBuild: Set(),2732 schedNoReport::scheduler::mDone: Set(),2733 schedNoReport::scheduler::mExpect: Set(),2734 schedNoReport::scheduler::mResult: Set(),2735 schedNoReport::scheduler::mRetry: Set(),2736 schedNoReport::scheduler::mRevoke: Set(),2737 schedNoReport::scheduler::mSchedule: Set(),2738 schedNoReport::scheduler::published: 0,2739 schedNoReport::scheduler::publishedBy: Set(),2740 schedNoReport::scheduler::ws:2741 Map(2742 "w1" ->2743 {2744 attached: Set(),2745 built: false,2746 expecting: true,2747 running: true,2748 session: true,2749 up: true2750 },2751 "w2" ->2752 {2753 attached: Set(),2754 built: false,2755 expecting: false,2756 running: false,2757 session: true,2758 up: true2759 }2760 )2761}27622763[State 4]2764{2765 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2766 schedNoReport::scheduler::crashes: 0,2767 schedNoReport::scheduler::entry:2768 [{ followers: Set("c2"), leased: true, worker: "w1" }],2769 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2770 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2771 schedNoReport::scheduler::mBuild: Set(),2772 schedNoReport::scheduler::mDone: Set(),2773 schedNoReport::scheduler::mExpect: Set(),2774 schedNoReport::scheduler::mResult: Set(),2775 schedNoReport::scheduler::mRetry: Set(),2776 schedNoReport::scheduler::mRevoke: Set(),2777 schedNoReport::scheduler::mSchedule: Set("c1"),2778 schedNoReport::scheduler::published: 0,2779 schedNoReport::scheduler::publishedBy: Set(),2780 schedNoReport::scheduler::ws:2781 Map(2782 "w1" ->2783 {2784 attached: Set(),2785 built: false,2786 expecting: true,2787 running: true,2788 session: true,2789 up: true2790 },2791 "w2" ->2792 {2793 attached: Set(),2794 built: false,2795 expecting: false,2796 running: false,2797 session: true,2798 up: true2799 }2800 )2801}28022803[State 5]2804{2805 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2806 schedNoReport::scheduler::crashes: 1,2807 schedNoReport::scheduler::entry: [],2808 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2809 schedNoReport::scheduler::mAssigned: Set(),2810 schedNoReport::scheduler::mBuild: Set(),2811 schedNoReport::scheduler::mDone: Set(),2812 schedNoReport::scheduler::mExpect: Set(),2813 schedNoReport::scheduler::mResult: Set(),2814 schedNoReport::scheduler::mRetry: Set("c1", "c2"),2815 schedNoReport::scheduler::mRevoke: Set(),2816 schedNoReport::scheduler::mSchedule: Set(),2817 schedNoReport::scheduler::published: 0,2818 schedNoReport::scheduler::publishedBy: Set(),2819 schedNoReport::scheduler::ws:2820 Map(2821 "w1" ->2822 {2823 attached: Set(),2824 built: false,2825 expecting: true,2826 running: true,2827 session: false,2828 up: true2829 },2830 "w2" ->2831 {2832 attached: Set(),2833 built: false,2834 expecting: false,2835 running: false,2836 session: false,2837 up: true2838 }2839 )2840}28412842[State 6]2843{2844 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2845 schedNoReport::scheduler::crashes: 2,2846 schedNoReport::scheduler::entry: [],2847 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2848 schedNoReport::scheduler::mAssigned: Set(),2849 schedNoReport::scheduler::mBuild: Set(),2850 schedNoReport::scheduler::mDone: Set(),2851 schedNoReport::scheduler::mExpect: Set(),2852 schedNoReport::scheduler::mResult: Set(),2853 schedNoReport::scheduler::mRetry: Set("c1", "c2"),2854 schedNoReport::scheduler::mRevoke: Set(),2855 schedNoReport::scheduler::mSchedule: Set(),2856 schedNoReport::scheduler::published: 0,2857 schedNoReport::scheduler::publishedBy: Set(),2858 schedNoReport::scheduler::ws:2859 Map(2860 "w1" ->2861 {2862 attached: Set(),2863 built: false,2864 expecting: true,2865 running: true,2866 session: false,2867 up: true2868 },2869 "w2" ->2870 {2871 attached: Set(),2872 built: false,2873 expecting: false,2874 running: false,2875 session: false,2876 up: true2877 }2878 )2879}28802881[State 7]2882{2883 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2884 schedNoReport::scheduler::crashes: 2,2885 schedNoReport::scheduler::entry: [],2886 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2887 schedNoReport::scheduler::mAssigned: Set(),2888 schedNoReport::scheduler::mBuild: Set(),2889 schedNoReport::scheduler::mDone: Set(),2890 schedNoReport::scheduler::mExpect: Set(),2891 schedNoReport::scheduler::mResult: Set(),2892 schedNoReport::scheduler::mRetry: Set("c1", "c2"),2893 schedNoReport::scheduler::mRevoke: Set(),2894 schedNoReport::scheduler::mSchedule: Set(),2895 schedNoReport::scheduler::published: 0,2896 schedNoReport::scheduler::publishedBy: Set(),2897 schedNoReport::scheduler::ws:2898 Map(2899 "w1" ->2900 {2901 attached: Set(),2902 built: false,2903 expecting: true,2904 running: true,2905 session: false,2906 up: true2907 },2908 "w2" ->2909 {2910 attached: Set(),2911 built: false,2912 expecting: false,2913 running: false,2914 session: true,2915 up: true2916 }2917 )2918}29192920[State 8]2921{2922 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2923 schedNoReport::scheduler::crashes: 2,2924 schedNoReport::scheduler::entry: [],2925 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2926 schedNoReport::scheduler::mAssigned: Set(),2927 schedNoReport::scheduler::mBuild: Set(),2928 schedNoReport::scheduler::mDone: Set(),2929 schedNoReport::scheduler::mExpect: Set(),2930 schedNoReport::scheduler::mResult: Set(),2931 schedNoReport::scheduler::mRetry: Set("c1", "c2"),2932 schedNoReport::scheduler::mRevoke: Set(),2933 schedNoReport::scheduler::mSchedule: Set(),2934 schedNoReport::scheduler::published: 0,2935 schedNoReport::scheduler::publishedBy: Set(),2936 schedNoReport::scheduler::ws:2937 Map(2938 "w1" ->2939 {2940 attached: Set(),2941 built: false,2942 expecting: true,2943 running: true,2944 session: true,2945 up: true2946 },2947 "w2" ->2948 {2949 attached: Set(),2950 built: false,2951 expecting: false,2952 running: false,2953 session: true,2954 up: true2955 }2956 )2957}29582959[State 9]2960{2961 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2962 schedNoReport::scheduler::crashes: 2,2963 schedNoReport::scheduler::entry: [],2964 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2965 schedNoReport::scheduler::mAssigned: Set(),2966 schedNoReport::scheduler::mBuild: Set(),2967 schedNoReport::scheduler::mDone: Set(),2968 schedNoReport::scheduler::mExpect: Set(),2969 schedNoReport::scheduler::mResult: Set(),2970 schedNoReport::scheduler::mRetry: Set("c1"),2971 schedNoReport::scheduler::mRevoke: Set(),2972 schedNoReport::scheduler::mSchedule: Set("c2"),2973 schedNoReport::scheduler::published: 0,2974 schedNoReport::scheduler::publishedBy: Set(),2975 schedNoReport::scheduler::ws:2976 Map(2977 "w1" ->2978 {2979 attached: Set(),2980 built: false,2981 expecting: true,2982 running: true,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 10]2999{3000 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),3001 schedNoReport::scheduler::crashes: 2,3002 schedNoReport::scheduler::entry: [],3003 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),3004 schedNoReport::scheduler::mAssigned: Set(),3005 schedNoReport::scheduler::mBuild: Set(),3006 schedNoReport::scheduler::mDone: Set(),3007 schedNoReport::scheduler::mExpect: Set(),3008 schedNoReport::scheduler::mResult: Set(),3009 schedNoReport::scheduler::mRetry: Set(),3010 schedNoReport::scheduler::mRevoke: Set(),3011 schedNoReport::scheduler::mSchedule: Set("c1", "c2"),3012 schedNoReport::scheduler::published: 0,3013 schedNoReport::scheduler::publishedBy: Set(),3014 schedNoReport::scheduler::ws:3015 Map(3016 "w1" ->3017 {3018 attached: Set(),3019 built: false,3020 expecting: true,3021 running: true,3022 session: true,3023 up: true3024 },3025 "w2" ->3026 {3027 attached: Set(),3028 built: false,3029 expecting: false,3030 running: false,3031 session: true,3032 up: true3033 }3034 )3035}30363037[State 11]3038{3039 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),3040 schedNoReport::scheduler::crashes: 2,3041 schedNoReport::scheduler::entry:3042 [{ followers: Set("c2"), leased: true, worker: "w2" }],3043 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),3044 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),3045 schedNoReport::scheduler::mBuild: Set(),3046 schedNoReport::scheduler::mDone: Set(),3047 schedNoReport::scheduler::mExpect: Set("w2"),3048 schedNoReport::scheduler::mResult: Set(),3049 schedNoReport::scheduler::mRetry: Set(),3050 schedNoReport::scheduler::mRevoke: Set(),3051 schedNoReport::scheduler::mSchedule: Set("c1"),3052 schedNoReport::scheduler::published: 0,3053 schedNoReport::scheduler::publishedBy: Set(),3054 schedNoReport::scheduler::ws:3055 Map(3056 "w1" ->3057 {3058 attached: Set(),3059 built: false,3060 expecting: true,3061 running: true,3062 session: true,3063 up: true3064 },3065 "w2" ->3066 {3067 attached: Set(),3068 built: false,3069 expecting: false,3070 running: false,3071 session: true,3072 up: true3073 }3074 )3075}30763077[State 12]3078{3079 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),3080 schedNoReport::scheduler::crashes: 2,3081 schedNoReport::scheduler::entry:3082 [{ followers: Set("c2"), leased: true, worker: "w2" }],3083 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),3084 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),3085 schedNoReport::scheduler::mBuild: Set(),3086 schedNoReport::scheduler::mDone: Set(),3087 schedNoReport::scheduler::mExpect: Set(),3088 schedNoReport::scheduler::mResult: Set(),3089 schedNoReport::scheduler::mRetry: Set(),3090 schedNoReport::scheduler::mRevoke: Set(),3091 schedNoReport::scheduler::mSchedule: Set("c1"),3092 schedNoReport::scheduler::published: 0,3093 schedNoReport::scheduler::publishedBy: Set(),3094 schedNoReport::scheduler::ws:3095 Map(3096 "w1" ->3097 {3098 attached: Set(),3099 built: false,3100 expecting: true,3101 running: true,3102 session: true,3103 up: true3104 },3105 "w2" ->3106 {3107 attached: Set(),3108 built: false,3109 expecting: true,3110 running: true,3111 session: true,3112 up: true3113 }3114 )3115}31163117[violation] Found an issue (938ms at 2023 traces/second).3118Use --verbosity=3 to show executions.3119Use --seed=0xdb152a716aa7260b --backend=rust to reproduce.3120error: Invariant violated3121An example execution:31223123[State 0]3124{3125 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3126 schedTerminal::scheduler::crashes: 0,3127 schedTerminal::scheduler::entry: [],3128 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3129 schedTerminal::scheduler::mAssigned: Set(),3130 schedTerminal::scheduler::mBuild: Set(),3131 schedTerminal::scheduler::mDone: Set(),3132 schedTerminal::scheduler::mExpect: Set(),3133 schedTerminal::scheduler::mResult: Set(),3134 schedTerminal::scheduler::mRetry: Set(),3135 schedTerminal::scheduler::mRevoke: Set(),3136 schedTerminal::scheduler::mSchedule: Set(),3137 schedTerminal::scheduler::published: 0,3138 schedTerminal::scheduler::publishedBy: Set(),3139 schedTerminal::scheduler::ws:3140 Map(3141 "w1" ->3142 {3143 attached: Set(),3144 built: false,3145 expecting: false,3146 running: false,3147 session: true,3148 up: true3149 },3150 "w2" ->3151 {3152 attached: Set(),3153 built: false,3154 expecting: false,3155 running: false,3156 session: true,3157 up: true3158 }3159 )3160}31613162[State 1]3163{3164 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3165 schedTerminal::scheduler::crashes: 1,3166 schedTerminal::scheduler::entry: [],3167 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3168 schedTerminal::scheduler::mAssigned: Set(),3169 schedTerminal::scheduler::mBuild: Set(),3170 schedTerminal::scheduler::mDone: Set(),3171 schedTerminal::scheduler::mExpect: Set(),3172 schedTerminal::scheduler::mResult: Set(),3173 schedTerminal::scheduler::mRetry: Set(),3174 schedTerminal::scheduler::mRevoke: Set(),3175 schedTerminal::scheduler::mSchedule: Set(),3176 schedTerminal::scheduler::published: 0,3177 schedTerminal::scheduler::publishedBy: Set(),3178 schedTerminal::scheduler::ws:3179 Map(3180 "w1" ->3181 {3182 attached: Set(),3183 built: false,3184 expecting: false,3185 running: false,3186 session: false,3187 up: true3188 },3189 "w2" ->3190 {3191 attached: Set(),3192 built: false,3193 expecting: false,3194 running: false,3195 session: false,3196 up: true3197 }3198 )3199}32003201[State 2]3202{3203 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3204 schedTerminal::scheduler::crashes: 1,3205 schedTerminal::scheduler::entry: [],3206 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3207 schedTerminal::scheduler::mAssigned: Set(),3208 schedTerminal::scheduler::mBuild: Set(),3209 schedTerminal::scheduler::mDone: Set(),3210 schedTerminal::scheduler::mExpect: Set(),3211 schedTerminal::scheduler::mResult: Set(),3212 schedTerminal::scheduler::mRetry: Set(),3213 schedTerminal::scheduler::mRevoke: Set(),3214 schedTerminal::scheduler::mSchedule: Set("c2"),3215 schedTerminal::scheduler::published: 0,3216 schedTerminal::scheduler::publishedBy: Set(),3217 schedTerminal::scheduler::ws:3218 Map(3219 "w1" ->3220 {3221 attached: Set(),3222 built: false,3223 expecting: false,3224 running: false,3225 session: false,3226 up: true3227 },3228 "w2" ->3229 {3230 attached: Set(),3231 built: false,3232 expecting: false,3233 running: false,3234 session: false,3235 up: true3236 }3237 )3238}32393240[State 3]3241{3242 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3243 schedTerminal::scheduler::crashes: 1,3244 schedTerminal::scheduler::entry: [],3245 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3246 schedTerminal::scheduler::mAssigned: Set(),3247 schedTerminal::scheduler::mBuild: Set(),3248 schedTerminal::scheduler::mDone: Set(),3249 schedTerminal::scheduler::mExpect: Set(),3250 schedTerminal::scheduler::mResult: Set(),3251 schedTerminal::scheduler::mRetry: Set(),3252 schedTerminal::scheduler::mRevoke: Set(),3253 schedTerminal::scheduler::mSchedule: Set(),3254 schedTerminal::scheduler::published: 0,3255 schedTerminal::scheduler::publishedBy: Set(),3256 schedTerminal::scheduler::ws:3257 Map(3258 "w1" ->3259 {3260 attached: Set(),3261 built: false,3262 expecting: false,3263 running: false,3264 session: false,3265 up: true3266 },3267 "w2" ->3268 {3269 attached: Set(),3270 built: false,3271 expecting: false,3272 running: false,3273 session: false,3274 up: true3275 }3276 )3277}32783279[violation] Found an issue (131ms at 389 traces/second).3280Use --verbosity=3 to show executions.3281Use --seed=0xa82d8887343d3e7d --backend=rust to reproduce.3282error: Invariant violated3283An example execution:32843285[State 0]3286{3287 pushFixed::push::byPath: Map(),3288 pushFixed::push::inflight: Set(),3289 pushFixed::push::left: Map(),3290 pushFixed::push::sent: Map()3291}32923293[State 1]3294{3295 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3296 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3297 pushFixed::push::left: Map(3 -> 2),3298 pushFixed::push::sent: Map(3 -> Set("a", "b"))3299}33003301[State 2]3302{3303 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3304 pushFixed::push::inflight: Set((3, "b")),3305 pushFixed::push::left: Map(3 -> 1),3306 pushFixed::push::sent: Map(3 -> Set("a", "b"))3307}33083309[State 3]3310{3311 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3312 pushFixed::push::inflight: Set(),3313 pushFixed::push::left: Map(3 -> 0),3314 pushFixed::push::sent: Map(3 -> Set("a", "b"))3315}33163317[State 4]3318{3319 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3320 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3321 pushFixed::push::left: Map(2 -> 2, 3 -> 0),3322 pushFixed::push::sent: Map(2 -> Set("a", "b"), 3 -> Set("a", "b"))3323}33243325[State 5]3326{3327 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3328 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),3329 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 0),3330 pushFixed::push::sent:3331 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3332}33333334[State 6]3335{3336 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3337 pushFixed::push::inflight: Set((1, "b"), (2, "a"), (2, "b")),3338 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 0),3339 pushFixed::push::sent:3340 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3341}33423343[State 7]3344{3345 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3346 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3347 pushFixed::push::left: Map(1 -> 0, 2 -> 2, 3 -> 0),3348 pushFixed::push::sent:3349 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3350}33513352[State 8]3353{3354 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3355 pushFixed::push::inflight: Set((2, "a")),3356 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 0),3357 pushFixed::push::sent:3358 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3359}33603361[State 9]3362{3363 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3364 pushFixed::push::inflight: Set(),3365 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3366 pushFixed::push::sent:3367 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3368}33693370[ok] No violation found (741ms at 26991 traces/second).3371Trace length statistics: max=10, min=7, average=8.003372You may increase --max-samples and --max-steps.3373Use --verbosity to produce more (or less) output.3374Use --seed=0xfd7e63ee8162e7c7 --backend=rust to reproduce.