nixbot

builds

succeeded nix-grpc-store-spec checks.aarch64-darwin.spec · build #803 · 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: false,68 up: true69 },70 "w2" ->71 {72 attached: Set(),73 built: false,74 expecting: false,75 running: false,76 session: false,77 up: true78 }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: true117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),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("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: false147 },148 "w2" ->149 {150 attached: Set(),151 built: false,152 expecting: false,153 running: false,154 session: false,155 up: true156 }157 )158}159160[State 4]161{162 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),163 schedFixed::scheduler::crashes: 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("c1", "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: false,185 up: false186 },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: 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: false,224 up: false225 },226 "w2" ->227 {228 attached: Set(),229 built: false,230 expecting: false,231 running: false,232 session: true,233 up: true234 }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("c1"), leased: true, worker: "w2" }],244 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),245 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),246 schedFixed::scheduler::mBuild: Set(),247 schedFixed::scheduler::mDone: Set(),248 schedFixed::scheduler::mExpect: Set("w2"),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: false,264 up: false265 },266 "w2" ->267 {268 attached: Set(),269 built: false,270 expecting: false,271 running: false,272 session: true,273 up: true274 }275 )276}277278[State 7]279{280 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),281 schedFixed::scheduler::crashes: 2,282 schedFixed::scheduler::entry:283 [{ followers: Set("c1"), leased: true, worker: "w2" }],284 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),285 schedFixed::scheduler::mAssigned: Set(),286 schedFixed::scheduler::mBuild: Set(("c1", "w2")),287 schedFixed::scheduler::mDone: Set(),288 schedFixed::scheduler::mExpect: Set("w2"),289 schedFixed::scheduler::mResult: Set(),290 schedFixed::scheduler::mRetry: Set(),291 schedFixed::scheduler::mRevoke: Set(),292 schedFixed::scheduler::mSchedule: Set("c2"),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: false,304 up: false305 },306 "w2" ->307 {308 attached: Set(),309 built: false,310 expecting: false,311 running: false,312 session: true,313 up: true314 }315 )316}317318[State 8]319{320 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),321 schedFixed::scheduler::crashes: 2,322 schedFixed::scheduler::entry:323 [{ followers: Set("c1"), leased: true, worker: "w2" }],324 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),325 schedFixed::scheduler::mAssigned: Set(),326 schedFixed::scheduler::mBuild: Set(),327 schedFixed::scheduler::mDone: Set(),328 schedFixed::scheduler::mExpect: Set("w2"),329 schedFixed::scheduler::mResult: Set(),330 schedFixed::scheduler::mRetry: Set("c1"),331 schedFixed::scheduler::mRevoke: Set(),332 schedFixed::scheduler::mSchedule: Set("c2"),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: false,344 up: false345 },346 "w2" ->347 {348 attached: Set(),349 built: false,350 expecting: false,351 running: false,352 session: true,353 up: true354 }355 )356}357358[State 9]359{360 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),361 schedFixed::scheduler::crashes: 2,362 schedFixed::scheduler::entry:363 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],364 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),365 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),366 schedFixed::scheduler::mBuild: Set(),367 schedFixed::scheduler::mDone: Set(),368 schedFixed::scheduler::mExpect: Set("w2"),369 schedFixed::scheduler::mResult: Set(),370 schedFixed::scheduler::mRetry: Set("c1"),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: true,393 up: true394 }395 )396}397398[State 10]399{400 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),401 schedFixed::scheduler::crashes: 2,402 schedFixed::scheduler::entry:403 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],404 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),405 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),406 schedFixed::scheduler::mBuild: Set(),407 schedFixed::scheduler::mDone: Set(),408 schedFixed::scheduler::mExpect: Set("w2"),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: "w2" }],444 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),445 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),446 schedFixed::scheduler::mBuild: Set(),447 schedFixed::scheduler::mDone: Set(),448 schedFixed::scheduler::mExpect: Set("w2"),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" -> CSent("w2")),481 schedFixed::scheduler::crashes: 2,482 schedFixed::scheduler::entry:483 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],484 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),485 schedFixed::scheduler::mAssigned: Set(),486 schedFixed::scheduler::mBuild: Set(("c2", "w2")),487 schedFixed::scheduler::mDone: Set(),488 schedFixed::scheduler::mExpect: Set("w2"),489 schedFixed::scheduler::mResult: Set(),490 schedFixed::scheduler::mRetry: Set(),491 schedFixed::scheduler::mRevoke: Set(),492 schedFixed::scheduler::mSchedule: Set("c1"),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" -> CQueued, "c2" -> CSent("w2")),521 schedFixed::scheduler::crashes: 2,522 schedFixed::scheduler::entry:523 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],524 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),525 schedFixed::scheduler::mAssigned: Set(),526 schedFixed::scheduler::mBuild: Set(),527 schedFixed::scheduler::mDone: Set(),528 schedFixed::scheduler::mExpect: Set("w2"),529 schedFixed::scheduler::mResult: Set(),530 schedFixed::scheduler::mRetry: Set("c2"),531 schedFixed::scheduler::mRevoke: Set(),532 schedFixed::scheduler::mSchedule: Set("c1"),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" -> CQueued, "c2" -> CQueued),561 schedFixed::scheduler::crashes: 2,562 schedFixed::scheduler::entry:563 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],564 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),565 schedFixed::scheduler::mAssigned: Set(),566 schedFixed::scheduler::mBuild: Set(),567 schedFixed::scheduler::mDone: Set(),568 schedFixed::scheduler::mExpect: Set("w2"),569 schedFixed::scheduler::mResult: Set(),570 schedFixed::scheduler::mRetry: Set(),571 schedFixed::scheduler::mRevoke: Set(),572 schedFixed::scheduler::mSchedule: Set("c1", "c2"),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" -> CQueued, "c2" -> CQueued),601 schedFixed::scheduler::crashes: 2,602 schedFixed::scheduler::entry:603 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],604 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),605 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),606 schedFixed::scheduler::mBuild: Set(),607 schedFixed::scheduler::mDone: Set(),608 schedFixed::scheduler::mExpect: Set("w2"),609 schedFixed::scheduler::mResult: Set(),610 schedFixed::scheduler::mRetry: Set(),611 schedFixed::scheduler::mRevoke: Set(),612 schedFixed::scheduler::mSchedule: Set("c2"),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("w2"), "c2" -> CQueued),641 schedFixed::scheduler::crashes: 2,642 schedFixed::scheduler::entry:643 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],644 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),645 schedFixed::scheduler::mAssigned: Set(),646 schedFixed::scheduler::mBuild: Set(("c1", "w2")),647 schedFixed::scheduler::mDone: Set(),648 schedFixed::scheduler::mExpect: Set("w2"),649 schedFixed::scheduler::mResult: Set(),650 schedFixed::scheduler::mRetry: Set(),651 schedFixed::scheduler::mRevoke: Set(),652 schedFixed::scheduler::mSchedule: Set("c2"),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" -> CSent("w2"), "c2" -> CQueued),681 schedFixed::scheduler::crashes: 2,682 schedFixed::scheduler::entry:683 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],684 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),685 schedFixed::scheduler::mAssigned: Set(),686 schedFixed::scheduler::mBuild: Set(),687 schedFixed::scheduler::mDone: Set(),688 schedFixed::scheduler::mExpect: Set("w2"),689 schedFixed::scheduler::mResult: Set(),690 schedFixed::scheduler::mRetry: Set("c1"),691 schedFixed::scheduler::mRevoke: Set(),692 schedFixed::scheduler::mSchedule: Set("c2"),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" -> CSent("w2"), "c2" -> CQueued),721 schedFixed::scheduler::crashes: 2,722 schedFixed::scheduler::entry:723 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],724 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),725 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),726 schedFixed::scheduler::mBuild: Set(),727 schedFixed::scheduler::mDone: Set(),728 schedFixed::scheduler::mExpect: Set("w2"),729 schedFixed::scheduler::mResult: Set(),730 schedFixed::scheduler::mRetry: Set("c1"),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" -> CSent("w2"), "c2" -> CSent("w2")),761 schedFixed::scheduler::crashes: 2,762 schedFixed::scheduler::entry:763 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],764 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),765 schedFixed::scheduler::mAssigned: Set(),766 schedFixed::scheduler::mBuild: Set(("c2", "w2")),767 schedFixed::scheduler::mDone: Set(),768 schedFixed::scheduler::mExpect: Set("w2"),769 schedFixed::scheduler::mResult: Set(),770 schedFixed::scheduler::mRetry: Set("c1"),771 schedFixed::scheduler::mRevoke: Set(),772 schedFixed::scheduler::mSchedule: Set(),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" -> CSent("w2"), "c2" -> CSent("w2")),801 schedFixed::scheduler::crashes: 2,802 schedFixed::scheduler::entry:803 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],804 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),805 schedFixed::scheduler::mAssigned: Set(),806 schedFixed::scheduler::mBuild: Set(),807 schedFixed::scheduler::mDone: Set(),808 schedFixed::scheduler::mExpect: Set("w2"),809 schedFixed::scheduler::mResult: Set(),810 schedFixed::scheduler::mRetry: Set("c1", "c2"),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("w2"), "c2" -> CSent("w2")),841 schedFixed::scheduler::crashes: 2,842 schedFixed::scheduler::entry:843 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],844 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),845 schedFixed::scheduler::mAssigned: Set(),846 schedFixed::scheduler::mBuild: Set(),847 schedFixed::scheduler::mDone: Set(),848 schedFixed::scheduler::mExpect: Set(),849 schedFixed::scheduler::mResult: Set(),850 schedFixed::scheduler::mRetry: Set("c1", "c2"),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: true,871 running: true,872 session: true,873 up: true874 }875 )876}877878[State 22]879{880 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),881 schedFixed::scheduler::crashes: 2,882 schedFixed::scheduler::entry:883 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],884 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),885 schedFixed::scheduler::mAssigned: Set(),886 schedFixed::scheduler::mBuild: Set(),887 schedFixed::scheduler::mDone: Set(),888 schedFixed::scheduler::mExpect: Set(),889 schedFixed::scheduler::mResult: Set(),890 schedFixed::scheduler::mRetry: Set("c2"),891 schedFixed::scheduler::mRevoke: Set(),892 schedFixed::scheduler::mSchedule: Set("c1"),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: true,911 running: true,912 session: true,913 up: true914 }915 )916}917918[State 23]919{920 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),921 schedFixed::scheduler::crashes: 2,922 schedFixed::scheduler::entry:923 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],924 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),925 schedFixed::scheduler::mAssigned: Set(),926 schedFixed::scheduler::mBuild: Set(),927 schedFixed::scheduler::mDone: Set(),928 schedFixed::scheduler::mExpect: Set(),929 schedFixed::scheduler::mResult: Set(),930 schedFixed::scheduler::mRetry: Set(),931 schedFixed::scheduler::mRevoke: Set(),932 schedFixed::scheduler::mSchedule: Set("c1", "c2"),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: true,951 running: true,952 session: true,953 up: true954 }955 )956}957958[State 24]959{960 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),961 schedFixed::scheduler::crashes: 2,962 schedFixed::scheduler::entry:963 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],964 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),965 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),966 schedFixed::scheduler::mBuild: Set(),967 schedFixed::scheduler::mDone: Set(),968 schedFixed::scheduler::mExpect: Set(),969 schedFixed::scheduler::mResult: Set(),970 schedFixed::scheduler::mRetry: Set(),971 schedFixed::scheduler::mRevoke: Set(),972 schedFixed::scheduler::mSchedule: Set("c1"),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: true,991 running: true,992 session: true,993 up: true994 }995 )996}997998[State 25]999{1000 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1001 schedFixed::scheduler::crashes: 2,1002 schedFixed::scheduler::entry:1003 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1004 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1005 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1006 schedFixed::scheduler::mBuild: Set(),1007 schedFixed::scheduler::mDone: Set("w2"),1008 schedFixed::scheduler::mExpect: Set(),1009 schedFixed::scheduler::mResult: Set(),1010 schedFixed::scheduler::mRetry: Set(),1011 schedFixed::scheduler::mRevoke: Set(),1012 schedFixed::scheduler::mSchedule: Set("c1"),1013 schedFixed::scheduler::published: 1,1014 schedFixed::scheduler::publishedBy: Set("w2"),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: true,1030 expecting: false,1031 running: false,1032 session: true,1033 up: true1034 }1035 )1036}10371038[State 26]1039{1040 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1041 schedFixed::scheduler::crashes: 2,1042 schedFixed::scheduler::entry:1043 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1044 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1045 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),1046 schedFixed::scheduler::mBuild: Set(),1047 schedFixed::scheduler::mDone: Set("w2"),1048 schedFixed::scheduler::mExpect: Set(),1049 schedFixed::scheduler::mResult: Set("c1"),1050 schedFixed::scheduler::mRetry: Set(),1051 schedFixed::scheduler::mRevoke: Set(),1052 schedFixed::scheduler::mSchedule: Set(),1053 schedFixed::scheduler::published: 1,1054 schedFixed::scheduler::publishedBy: Set("w2"),1055 schedFixed::scheduler::ws:1056 Map(1057 "w1" ->1058 {1059 attached: Set(),1060 built: false,1061 expecting: false,1062 running: false,1063 session: true,1064 up: true1065 },1066 "w2" ->1067 {1068 attached: Set(),1069 built: true,1070 expecting: false,1071 running: false,1072 session: true,1073 up: true1074 }1075 )1076}10771078[State 27]1079{1080 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),1081 schedFixed::scheduler::crashes: 2,1082 schedFixed::scheduler::entry:1083 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1084 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1085 schedFixed::scheduler::mAssigned: Set(),1086 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1087 schedFixed::scheduler::mDone: Set("w2"),1088 schedFixed::scheduler::mExpect: Set(),1089 schedFixed::scheduler::mResult: Set("c1"),1090 schedFixed::scheduler::mRetry: Set(),1091 schedFixed::scheduler::mRevoke: Set(),1092 schedFixed::scheduler::mSchedule: Set(),1093 schedFixed::scheduler::published: 1,1094 schedFixed::scheduler::publishedBy: Set("w2"),1095 schedFixed::scheduler::ws:1096 Map(1097 "w1" ->1098 {1099 attached: Set(),1100 built: false,1101 expecting: false,1102 running: false,1103 session: true,1104 up: true1105 },1106 "w2" ->1107 {1108 attached: Set(),1109 built: true,1110 expecting: false,1111 running: false,1112 session: true,1113 up: true1114 }1115 )1116}11171118[State 28]1119{1120 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),1121 schedFixed::scheduler::crashes: 2,1122 schedFixed::scheduler::entry:1123 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1124 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1125 schedFixed::scheduler::mAssigned: Set(),1126 schedFixed::scheduler::mBuild: Set(),1127 schedFixed::scheduler::mDone: Set("w2"),1128 schedFixed::scheduler::mExpect: Set(),1129 schedFixed::scheduler::mResult: Set("c1", "c2"),1130 schedFixed::scheduler::mRetry: Set(),1131 schedFixed::scheduler::mRevoke: Set(),1132 schedFixed::scheduler::mSchedule: Set(),1133 schedFixed::scheduler::published: 1,1134 schedFixed::scheduler::publishedBy: Set("w2"),1135 schedFixed::scheduler::ws:1136 Map(1137 "w1" ->1138 {1139 attached: Set(),1140 built: false,1141 expecting: false,1142 running: false,1143 session: true,1144 up: true1145 },1146 "w2" ->1147 {1148 attached: Set(),1149 built: true,1150 expecting: false,1151 running: false,1152 session: true,1153 up: true1154 }1155 )1156}11571158[State 29]1159{1160 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CDone),1161 schedFixed::scheduler::crashes: 2,1162 schedFixed::scheduler::entry:1163 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1164 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1165 schedFixed::scheduler::mAssigned: Set(),1166 schedFixed::scheduler::mBuild: Set(),1167 schedFixed::scheduler::mDone: Set("w2"),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("w2"),1175 schedFixed::scheduler::ws:1176 Map(1177 "w1" ->1178 {1179 attached: Set(),1180 built: false,1181 expecting: false,1182 running: false,1183 session: true,1184 up: true1185 },1186 "w2" ->1187 {1188 attached: Set(),1189 built: true,1190 expecting: false,1191 running: false,1192 session: true,1193 up: true1194 }1195 )1196}11971198[State 30]1199{1200 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CDone),1201 schedFixed::scheduler::crashes: 2,1202 schedFixed::scheduler::entry: [],1203 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1204 schedFixed::scheduler::mAssigned: Set(),1205 schedFixed::scheduler::mBuild: Set(),1206 schedFixed::scheduler::mDone: Set(),1207 schedFixed::scheduler::mExpect: Set(),1208 schedFixed::scheduler::mResult: Set("c1"),1209 schedFixed::scheduler::mRetry: Set(),1210 schedFixed::scheduler::mRevoke: Set(),1211 schedFixed::scheduler::mSchedule: Set(),1212 schedFixed::scheduler::published: 1,1213 schedFixed::scheduler::publishedBy: Set("w2"),1214 schedFixed::scheduler::ws:1215 Map(1216 "w1" ->1217 {1218 attached: Set(),1219 built: false,1220 expecting: false,1221 running: false,1222 session: true,1223 up: true1224 },1225 "w2" ->1226 {1227 attached: Set(),1228 built: true,1229 expecting: false,1230 running: false,1231 session: true,1232 up: true1233 }1234 )1235}12361237[ok] No violation found (8463ms at 3545 traces/second).1238Trace length statistics: max=31, min=15, average=18.801239You may increase --max-samples and --max-steps.1240Use --verbosity to produce more (or less) output.1241Use --seed=0xe00fb603e8516389 --backend=rust to reproduce.1242An example execution:12431244[State 0]1245{1246 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1247 schedNoRevoke::scheduler::crashes: 0,1248 schedNoRevoke::scheduler::entry: [],1249 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1250 schedNoRevoke::scheduler::mAssigned: Set(),1251 schedNoRevoke::scheduler::mBuild: Set(),1252 schedNoRevoke::scheduler::mDone: Set(),1253 schedNoRevoke::scheduler::mExpect: Set(),1254 schedNoRevoke::scheduler::mResult: Set(),1255 schedNoRevoke::scheduler::mRetry: Set(),1256 schedNoRevoke::scheduler::mRevoke: Set(),1257 schedNoRevoke::scheduler::mSchedule: Set(),1258 schedNoRevoke::scheduler::published: 0,1259 schedNoRevoke::scheduler::publishedBy: Set(),1260 schedNoRevoke::scheduler::ws:1261 Map(1262 "w1" ->1263 {1264 attached: Set(),1265 built: false,1266 expecting: false,1267 running: false,1268 session: true,1269 up: true1270 },1271 "w2" ->1272 {1273 attached: Set(),1274 built: false,1275 expecting: false,1276 running: false,1277 session: true,1278 up: true1279 }1280 )1281}12821283[State 1]1284{1285 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1286 schedNoRevoke::scheduler::crashes: 0,1287 schedNoRevoke::scheduler::entry: [],1288 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1289 schedNoRevoke::scheduler::mAssigned: Set(),1290 schedNoRevoke::scheduler::mBuild: Set(),1291 schedNoRevoke::scheduler::mDone: Set(),1292 schedNoRevoke::scheduler::mExpect: Set(),1293 schedNoRevoke::scheduler::mResult: Set(),1294 schedNoRevoke::scheduler::mRetry: Set(),1295 schedNoRevoke::scheduler::mRevoke: Set(),1296 schedNoRevoke::scheduler::mSchedule: Set("c1"),1297 schedNoRevoke::scheduler::published: 0,1298 schedNoRevoke::scheduler::publishedBy: Set(),1299 schedNoRevoke::scheduler::ws:1300 Map(1301 "w1" ->1302 {1303 attached: Set(),1304 built: false,1305 expecting: false,1306 running: false,1307 session: true,1308 up: true1309 },1310 "w2" ->1311 {1312 attached: Set(),1313 built: false,1314 expecting: false,1315 running: false,1316 session: true,1317 up: true1318 }1319 )1320}13211322[State 2]1323{1324 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1325 schedNoRevoke::scheduler::crashes: 0,1326 schedNoRevoke::scheduler::entry:1327 [{ followers: Set("c1"), leased: true, worker: "w2" }],1328 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1329 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1330 schedNoRevoke::scheduler::mBuild: Set(),1331 schedNoRevoke::scheduler::mDone: Set(),1332 schedNoRevoke::scheduler::mExpect: Set("w2"),1333 schedNoRevoke::scheduler::mResult: Set(),1334 schedNoRevoke::scheduler::mRetry: Set(),1335 schedNoRevoke::scheduler::mRevoke: Set(),1336 schedNoRevoke::scheduler::mSchedule: Set(),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: true,1348 up: true1349 },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" -> CQueued, "c2" -> CIdle),1365 schedNoRevoke::scheduler::crashes: 0,1366 schedNoRevoke::scheduler::entry:1367 [{ followers: Set("c1"), leased: true, worker: "w2" }],1368 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1369 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1370 schedNoRevoke::scheduler::mBuild: Set(),1371 schedNoRevoke::scheduler::mDone: Set(),1372 schedNoRevoke::scheduler::mExpect: Set(),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: true,1388 up: true1389 },1390 "w2" ->1391 {1392 attached: Set(),1393 built: false,1394 expecting: true,1395 running: true,1396 session: true,1397 up: true1398 }1399 )1400}14011402[State 4]1403{1404 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1405 schedNoRevoke::scheduler::crashes: 1,1406 schedNoRevoke::scheduler::entry: [],1407 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1408 schedNoRevoke::scheduler::mAssigned: Set(),1409 schedNoRevoke::scheduler::mBuild: Set(),1410 schedNoRevoke::scheduler::mDone: Set(),1411 schedNoRevoke::scheduler::mExpect: Set(),1412 schedNoRevoke::scheduler::mResult: Set(),1413 schedNoRevoke::scheduler::mRetry: Set("c1"),1414 schedNoRevoke::scheduler::mRevoke: Set(),1415 schedNoRevoke::scheduler::mSchedule: Set(),1416 schedNoRevoke::scheduler::published: 0,1417 schedNoRevoke::scheduler::publishedBy: Set(),1418 schedNoRevoke::scheduler::ws:1419 Map(1420 "w1" ->1421 {1422 attached: Set(),1423 built: false,1424 expecting: false,1425 running: false,1426 session: false,1427 up: true1428 },1429 "w2" ->1430 {1431 attached: Set(),1432 built: false,1433 expecting: true,1434 running: true,1435 session: false,1436 up: true1437 }1438 )1439}14401441[State 5]1442{1443 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1444 schedNoRevoke::scheduler::crashes: 1,1445 schedNoRevoke::scheduler::entry: [],1446 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1447 schedNoRevoke::scheduler::mAssigned: Set(),1448 schedNoRevoke::scheduler::mBuild: Set(),1449 schedNoRevoke::scheduler::mDone: Set(),1450 schedNoRevoke::scheduler::mExpect: Set(),1451 schedNoRevoke::scheduler::mResult: Set(),1452 schedNoRevoke::scheduler::mRetry: Set("c1"),1453 schedNoRevoke::scheduler::mRevoke: Set(),1454 schedNoRevoke::scheduler::mSchedule: Set(),1455 schedNoRevoke::scheduler::published: 0,1456 schedNoRevoke::scheduler::publishedBy: Set(),1457 schedNoRevoke::scheduler::ws:1458 Map(1459 "w1" ->1460 {1461 attached: Set(),1462 built: false,1463 expecting: false,1464 running: false,1465 session: true,1466 up: true1467 },1468 "w2" ->1469 {1470 attached: Set(),1471 built: false,1472 expecting: true,1473 running: true,1474 session: false,1475 up: true1476 }1477 )1478}14791480[State 6]1481{1482 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1483 schedNoRevoke::scheduler::crashes: 1,1484 schedNoRevoke::scheduler::entry: [],1485 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1486 schedNoRevoke::scheduler::mAssigned: Set(),1487 schedNoRevoke::scheduler::mBuild: Set(),1488 schedNoRevoke::scheduler::mDone: Set(),1489 schedNoRevoke::scheduler::mExpect: Set(),1490 schedNoRevoke::scheduler::mResult: Set(),1491 schedNoRevoke::scheduler::mRetry: Set(),1492 schedNoRevoke::scheduler::mRevoke: Set(),1493 schedNoRevoke::scheduler::mSchedule: Set("c1"),1494 schedNoRevoke::scheduler::published: 0,1495 schedNoRevoke::scheduler::publishedBy: Set(),1496 schedNoRevoke::scheduler::ws:1497 Map(1498 "w1" ->1499 {1500 attached: Set(),1501 built: false,1502 expecting: false,1503 running: false,1504 session: true,1505 up: true1506 },1507 "w2" ->1508 {1509 attached: Set(),1510 built: false,1511 expecting: true,1512 running: true,1513 session: false,1514 up: true1515 }1516 )1517}15181519[State 7]1520{1521 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1522 schedNoRevoke::scheduler::crashes: 1,1523 schedNoRevoke::scheduler::entry:1524 [{ followers: Set("c1"), leased: true, worker: "w1" }],1525 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1526 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1527 schedNoRevoke::scheduler::mBuild: Set(),1528 schedNoRevoke::scheduler::mDone: Set(),1529 schedNoRevoke::scheduler::mExpect: Set("w1"),1530 schedNoRevoke::scheduler::mResult: Set(),1531 schedNoRevoke::scheduler::mRetry: Set(),1532 schedNoRevoke::scheduler::mRevoke: Set(),1533 schedNoRevoke::scheduler::mSchedule: Set(),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" -> CQueued, "c2" -> CIdle),1562 schedNoRevoke::scheduler::crashes: 1,1563 schedNoRevoke::scheduler::entry:1564 [{ followers: Set("c1"), leased: true, worker: "w1" }],1565 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1566 schedNoRevoke::scheduler::mAssigned: Set(("c1", "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: true,1594 up: true1595 }1596 )1597}15981599[State 9]1600{1601 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1602 schedNoRevoke::scheduler::crashes: 1,1603 schedNoRevoke::scheduler::entry:1604 [{ followers: Set("c1"), leased: true, worker: "w1" }],1605 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1606 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1607 schedNoRevoke::scheduler::mBuild: Set(),1608 schedNoRevoke::scheduler::mDone: Set(),1609 schedNoRevoke::scheduler::mExpect: Set(),1610 schedNoRevoke::scheduler::mResult: Set(),1611 schedNoRevoke::scheduler::mRetry: Set(),1612 schedNoRevoke::scheduler::mRevoke: Set(),1613 schedNoRevoke::scheduler::mSchedule: Set(),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: true,1623 running: true,1624 session: true,1625 up: true1626 },1627 "w2" ->1628 {1629 attached: Set(),1630 built: false,1631 expecting: true,1632 running: true,1633 session: true,1634 up: true1635 }1636 )1637}16381639[violation] Found an issue (4299ms at 3145 traces/second).1640Use --verbosity=3 to show executions.1641Use --seed=0x3d016c054002bc04 --backend=rust to reproduce.1642error: Invariant violated1643An example execution:16441645[State 0]1646{1647 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1648 schedNoFence::scheduler::crashes: 0,1649 schedNoFence::scheduler::entry: [],1650 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1651 schedNoFence::scheduler::mAssigned: Set(),1652 schedNoFence::scheduler::mBuild: Set(),1653 schedNoFence::scheduler::mDone: Set(),1654 schedNoFence::scheduler::mExpect: Set(),1655 schedNoFence::scheduler::mResult: Set(),1656 schedNoFence::scheduler::mRetry: Set(),1657 schedNoFence::scheduler::mRevoke: Set(),1658 schedNoFence::scheduler::mSchedule: Set(),1659 schedNoFence::scheduler::published: 0,1660 schedNoFence::scheduler::publishedBy: Set(),1661 schedNoFence::scheduler::ws:1662 Map(1663 "w1" ->1664 {1665 attached: Set(),1666 built: false,1667 expecting: false,1668 running: false,1669 session: true,1670 up: true1671 },1672 "w2" ->1673 {1674 attached: Set(),1675 built: false,1676 expecting: false,1677 running: false,1678 session: true,1679 up: true1680 }1681 )1682}16831684[State 1]1685{1686 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1687 schedNoFence::scheduler::crashes: 1,1688 schedNoFence::scheduler::entry: [],1689 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1690 schedNoFence::scheduler::mAssigned: Set(),1691 schedNoFence::scheduler::mBuild: Set(),1692 schedNoFence::scheduler::mDone: Set(),1693 schedNoFence::scheduler::mExpect: Set(),1694 schedNoFence::scheduler::mResult: Set(),1695 schedNoFence::scheduler::mRetry: Set(),1696 schedNoFence::scheduler::mRevoke: Set(),1697 schedNoFence::scheduler::mSchedule: Set(),1698 schedNoFence::scheduler::published: 0,1699 schedNoFence::scheduler::publishedBy: Set(),1700 schedNoFence::scheduler::ws:1701 Map(1702 "w1" ->1703 {1704 attached: Set(),1705 built: false,1706 expecting: false,1707 running: false,1708 session: false,1709 up: false1710 },1711 "w2" ->1712 {1713 attached: Set(),1714 built: false,1715 expecting: false,1716 running: false,1717 session: true,1718 up: true1719 }1720 )1721}17221723[State 2]1724{1725 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1726 schedNoFence::scheduler::crashes: 1,1727 schedNoFence::scheduler::entry: [],1728 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1729 schedNoFence::scheduler::mAssigned: Set(),1730 schedNoFence::scheduler::mBuild: Set(),1731 schedNoFence::scheduler::mDone: Set(),1732 schedNoFence::scheduler::mExpect: Set(),1733 schedNoFence::scheduler::mResult: Set(),1734 schedNoFence::scheduler::mRetry: Set(),1735 schedNoFence::scheduler::mRevoke: Set(),1736 schedNoFence::scheduler::mSchedule: Set("c1"),1737 schedNoFence::scheduler::published: 0,1738 schedNoFence::scheduler::publishedBy: Set(),1739 schedNoFence::scheduler::ws:1740 Map(1741 "w1" ->1742 {1743 attached: Set(),1744 built: false,1745 expecting: false,1746 running: false,1747 session: false,1748 up: false1749 },1750 "w2" ->1751 {1752 attached: Set(),1753 built: false,1754 expecting: false,1755 running: false,1756 session: true,1757 up: true1758 }1759 )1760}17611762[State 3]1763{1764 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1765 schedNoFence::scheduler::crashes: 1,1766 schedNoFence::scheduler::entry:1767 [{ followers: Set("c1"), leased: true, worker: "w2" }],1768 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1769 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),1770 schedNoFence::scheduler::mBuild: Set(),1771 schedNoFence::scheduler::mDone: Set(),1772 schedNoFence::scheduler::mExpect: Set("w2"),1773 schedNoFence::scheduler::mResult: Set(),1774 schedNoFence::scheduler::mRetry: Set(),1775 schedNoFence::scheduler::mRevoke: Set(),1776 schedNoFence::scheduler::mSchedule: Set(),1777 schedNoFence::scheduler::published: 0,1778 schedNoFence::scheduler::publishedBy: Set(),1779 schedNoFence::scheduler::ws:1780 Map(1781 "w1" ->1782 {1783 attached: Set(),1784 built: false,1785 expecting: false,1786 running: false,1787 session: false,1788 up: false1789 },1790 "w2" ->1791 {1792 attached: Set(),1793 built: false,1794 expecting: false,1795 running: false,1796 session: true,1797 up: true1798 }1799 )1800}18011802[State 4]1803{1804 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1805 schedNoFence::scheduler::crashes: 1,1806 schedNoFence::scheduler::entry:1807 [{ followers: Set("c1"), leased: true, worker: "w2" }],1808 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1809 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),1810 schedNoFence::scheduler::mBuild: Set(),1811 schedNoFence::scheduler::mDone: Set(),1812 schedNoFence::scheduler::mExpect: Set(),1813 schedNoFence::scheduler::mResult: Set(),1814 schedNoFence::scheduler::mRetry: Set(),1815 schedNoFence::scheduler::mRevoke: Set(),1816 schedNoFence::scheduler::mSchedule: Set(),1817 schedNoFence::scheduler::published: 0,1818 schedNoFence::scheduler::publishedBy: Set(),1819 schedNoFence::scheduler::ws:1820 Map(1821 "w1" ->1822 {1823 attached: Set(),1824 built: false,1825 expecting: false,1826 running: false,1827 session: false,1828 up: false1829 },1830 "w2" ->1831 {1832 attached: Set(),1833 built: false,1834 expecting: true,1835 running: true,1836 session: true,1837 up: true1838 }1839 )1840}18411842[State 5]1843{1844 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1845 schedNoFence::scheduler::crashes: 2,1846 schedNoFence::scheduler::entry: [],1847 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1848 schedNoFence::scheduler::mAssigned: Set(),1849 schedNoFence::scheduler::mBuild: Set(),1850 schedNoFence::scheduler::mDone: Set(),1851 schedNoFence::scheduler::mExpect: Set(),1852 schedNoFence::scheduler::mResult: Set(),1853 schedNoFence::scheduler::mRetry: Set("c1"),1854 schedNoFence::scheduler::mRevoke: Set(),1855 schedNoFence::scheduler::mSchedule: Set(),1856 schedNoFence::scheduler::published: 0,1857 schedNoFence::scheduler::publishedBy: Set(),1858 schedNoFence::scheduler::ws:1859 Map(1860 "w1" ->1861 {1862 attached: Set(),1863 built: false,1864 expecting: false,1865 running: false,1866 session: false,1867 up: false1868 },1869 "w2" ->1870 {1871 attached: Set(),1872 built: false,1873 expecting: true,1874 running: true,1875 session: false,1876 up: true1877 }1878 )1879}18801881[State 6]1882{1883 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1884 schedNoFence::scheduler::crashes: 2,1885 schedNoFence::scheduler::entry: [],1886 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1887 schedNoFence::scheduler::mAssigned: Set(),1888 schedNoFence::scheduler::mBuild: Set(),1889 schedNoFence::scheduler::mDone: Set(),1890 schedNoFence::scheduler::mExpect: Set(),1891 schedNoFence::scheduler::mResult: Set(),1892 schedNoFence::scheduler::mRetry: Set("c1"),1893 schedNoFence::scheduler::mRevoke: Set(),1894 schedNoFence::scheduler::mSchedule: Set(),1895 schedNoFence::scheduler::published: 0,1896 schedNoFence::scheduler::publishedBy: Set(),1897 schedNoFence::scheduler::ws:1898 Map(1899 "w1" ->1900 {1901 attached: Set(),1902 built: false,1903 expecting: false,1904 running: false,1905 session: true,1906 up: true1907 },1908 "w2" ->1909 {1910 attached: Set(),1911 built: false,1912 expecting: true,1913 running: true,1914 session: false,1915 up: true1916 }1917 )1918}19191920[State 7]1921{1922 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1923 schedNoFence::scheduler::crashes: 2,1924 schedNoFence::scheduler::entry: [],1925 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1926 schedNoFence::scheduler::mAssigned: Set(),1927 schedNoFence::scheduler::mBuild: Set(),1928 schedNoFence::scheduler::mDone: Set(),1929 schedNoFence::scheduler::mExpect: Set(),1930 schedNoFence::scheduler::mResult: Set(),1931 schedNoFence::scheduler::mRetry: Set(),1932 schedNoFence::scheduler::mRevoke: Set(),1933 schedNoFence::scheduler::mSchedule: Set("c1"),1934 schedNoFence::scheduler::published: 0,1935 schedNoFence::scheduler::publishedBy: Set(),1936 schedNoFence::scheduler::ws:1937 Map(1938 "w1" ->1939 {1940 attached: Set(),1941 built: false,1942 expecting: false,1943 running: false,1944 session: true,1945 up: true1946 },1947 "w2" ->1948 {1949 attached: Set(),1950 built: false,1951 expecting: true,1952 running: true,1953 session: false,1954 up: true1955 }1956 )1957}19581959[State 8]1960{1961 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1962 schedNoFence::scheduler::crashes: 2,1963 schedNoFence::scheduler::entry: [],1964 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1965 schedNoFence::scheduler::mAssigned: Set(),1966 schedNoFence::scheduler::mBuild: Set(),1967 schedNoFence::scheduler::mDone: Set(),1968 schedNoFence::scheduler::mExpect: Set(),1969 schedNoFence::scheduler::mResult: Set(),1970 schedNoFence::scheduler::mRetry: Set(),1971 schedNoFence::scheduler::mRevoke: Set(),1972 schedNoFence::scheduler::mSchedule: Set("c1", "c2"),1973 schedNoFence::scheduler::published: 0,1974 schedNoFence::scheduler::publishedBy: Set(),1975 schedNoFence::scheduler::ws:1976 Map(1977 "w1" ->1978 {1979 attached: Set(),1980 built: false,1981 expecting: false,1982 running: false,1983 session: true,1984 up: true1985 },1986 "w2" ->1987 {1988 attached: Set(),1989 built: false,1990 expecting: true,1991 running: true,1992 session: false,1993 up: true1994 }1995 )1996}19971998[State 9]1999{2000 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2001 schedNoFence::scheduler::crashes: 2,2002 schedNoFence::scheduler::entry:2003 [{ followers: Set("c1"), leased: true, worker: "w1" }],2004 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2005 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2006 schedNoFence::scheduler::mBuild: Set(),2007 schedNoFence::scheduler::mDone: Set(),2008 schedNoFence::scheduler::mExpect: Set("w1"),2009 schedNoFence::scheduler::mResult: Set(),2010 schedNoFence::scheduler::mRetry: Set(),2011 schedNoFence::scheduler::mRevoke: Set(),2012 schedNoFence::scheduler::mSchedule: Set("c2"),2013 schedNoFence::scheduler::published: 0,2014 schedNoFence::scheduler::publishedBy: Set(),2015 schedNoFence::scheduler::ws:2016 Map(2017 "w1" ->2018 {2019 attached: Set(),2020 built: false,2021 expecting: false,2022 running: false,2023 session: true,2024 up: true2025 },2026 "w2" ->2027 {2028 attached: Set(),2029 built: false,2030 expecting: true,2031 running: true,2032 session: false,2033 up: true2034 }2035 )2036}20372038[State 10]2039{2040 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2041 schedNoFence::scheduler::crashes: 2,2042 schedNoFence::scheduler::entry:2043 [{ followers: Set("c1"), leased: true, worker: "w1" }],2044 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2045 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2046 schedNoFence::scheduler::mBuild: Set(),2047 schedNoFence::scheduler::mDone: Set(),2048 schedNoFence::scheduler::mExpect: Set(),2049 schedNoFence::scheduler::mResult: Set(),2050 schedNoFence::scheduler::mRetry: Set(),2051 schedNoFence::scheduler::mRevoke: Set(),2052 schedNoFence::scheduler::mSchedule: Set("c2"),2053 schedNoFence::scheduler::published: 0,2054 schedNoFence::scheduler::publishedBy: Set(),2055 schedNoFence::scheduler::ws:2056 Map(2057 "w1" ->2058 {2059 attached: Set(),2060 built: false,2061 expecting: true,2062 running: true,2063 session: true,2064 up: true2065 },2066 "w2" ->2067 {2068 attached: Set(),2069 built: false,2070 expecting: true,2071 running: true,2072 session: false,2073 up: true2074 }2075 )2076}20772078[State 11]2079{2080 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2081 schedNoFence::scheduler::crashes: 2,2082 schedNoFence::scheduler::entry:2083 [{ followers: Set("c1"), leased: true, worker: "w1" }],2084 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2085 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2086 schedNoFence::scheduler::mBuild: Set(),2087 schedNoFence::scheduler::mDone: Set(),2088 schedNoFence::scheduler::mExpect: Set(),2089 schedNoFence::scheduler::mResult: Set(),2090 schedNoFence::scheduler::mRetry: Set(),2091 schedNoFence::scheduler::mRevoke: Set(),2092 schedNoFence::scheduler::mSchedule: Set("c2"),2093 schedNoFence::scheduler::published: 1,2094 schedNoFence::scheduler::publishedBy: Set("w2"),2095 schedNoFence::scheduler::ws:2096 Map(2097 "w1" ->2098 {2099 attached: Set(),2100 built: false,2101 expecting: true,2102 running: true,2103 session: true,2104 up: true2105 },2106 "w2" ->2107 {2108 attached: Set(),2109 built: true,2110 expecting: false,2111 running: false,2112 session: false,2113 up: true2114 }2115 )2116}21172118[State 12]2119{2120 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2121 schedNoFence::scheduler::crashes: 2,2122 schedNoFence::scheduler::entry:2123 [{ followers: Set("c1"), leased: true, worker: "w1" }],2124 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2125 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2126 schedNoFence::scheduler::mBuild: Set(),2127 schedNoFence::scheduler::mDone: Set(),2128 schedNoFence::scheduler::mExpect: Set(),2129 schedNoFence::scheduler::mResult: Set("c2"),2130 schedNoFence::scheduler::mRetry: Set(),2131 schedNoFence::scheduler::mRevoke: Set(),2132 schedNoFence::scheduler::mSchedule: Set(),2133 schedNoFence::scheduler::published: 1,2134 schedNoFence::scheduler::publishedBy: Set("w2"),2135 schedNoFence::scheduler::ws:2136 Map(2137 "w1" ->2138 {2139 attached: Set(),2140 built: false,2141 expecting: true,2142 running: true,2143 session: true,2144 up: true2145 },2146 "w2" ->2147 {2148 attached: Set(),2149 built: true,2150 expecting: false,2151 running: false,2152 session: false,2153 up: true2154 }2155 )2156}21572158[State 13]2159{2160 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2161 schedNoFence::scheduler::crashes: 2,2162 schedNoFence::scheduler::entry:2163 [{ followers: Set("c1"), leased: true, worker: "w1" }],2164 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2165 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),2166 schedNoFence::scheduler::mBuild: Set(),2167 schedNoFence::scheduler::mDone: Set("w1"),2168 schedNoFence::scheduler::mExpect: Set(),2169 schedNoFence::scheduler::mResult: Set("c2"),2170 schedNoFence::scheduler::mRetry: Set(),2171 schedNoFence::scheduler::mRevoke: Set(),2172 schedNoFence::scheduler::mSchedule: Set(),2173 schedNoFence::scheduler::published: 2,2174 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2175 schedNoFence::scheduler::ws:2176 Map(2177 "w1" ->2178 {2179 attached: Set(),2180 built: true,2181 expecting: false,2182 running: false,2183 session: true,2184 up: true2185 },2186 "w2" ->2187 {2188 attached: Set(),2189 built: true,2190 expecting: false,2191 running: false,2192 session: false,2193 up: true2194 }2195 )2196}21972198[violation] Found an issue (845ms at 2922 traces/second).2199Use --verbosity=3 to show executions.2200Use --seed=0x1970360e2570f990 --backend=rust to reproduce.2201error: Invariant violated2202An example execution:22032204[State 0]2205{2206 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2207 schedNoPush::scheduler::crashes: 0,2208 schedNoPush::scheduler::entry: [],2209 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2210 schedNoPush::scheduler::mAssigned: Set(),2211 schedNoPush::scheduler::mBuild: Set(),2212 schedNoPush::scheduler::mDone: Set(),2213 schedNoPush::scheduler::mExpect: Set(),2214 schedNoPush::scheduler::mResult: Set(),2215 schedNoPush::scheduler::mRetry: Set(),2216 schedNoPush::scheduler::mRevoke: Set(),2217 schedNoPush::scheduler::mSchedule: Set(),2218 schedNoPush::scheduler::published: 0,2219 schedNoPush::scheduler::publishedBy: Set(),2220 schedNoPush::scheduler::ws:2221 Map(2222 "w1" ->2223 {2224 attached: Set(),2225 built: false,2226 expecting: false,2227 running: false,2228 session: true,2229 up: true2230 },2231 "w2" ->2232 {2233 attached: Set(),2234 built: false,2235 expecting: false,2236 running: false,2237 session: true,2238 up: true2239 }2240 )2241}22422243[State 1]2244{2245 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2246 schedNoPush::scheduler::crashes: 0,2247 schedNoPush::scheduler::entry: [],2248 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2249 schedNoPush::scheduler::mAssigned: Set(),2250 schedNoPush::scheduler::mBuild: Set(),2251 schedNoPush::scheduler::mDone: Set(),2252 schedNoPush::scheduler::mExpect: Set(),2253 schedNoPush::scheduler::mResult: Set(),2254 schedNoPush::scheduler::mRetry: Set(),2255 schedNoPush::scheduler::mRevoke: Set(),2256 schedNoPush::scheduler::mSchedule: Set("c1"),2257 schedNoPush::scheduler::published: 0,2258 schedNoPush::scheduler::publishedBy: Set(),2259 schedNoPush::scheduler::ws:2260 Map(2261 "w1" ->2262 {2263 attached: Set(),2264 built: false,2265 expecting: false,2266 running: false,2267 session: true,2268 up: true2269 },2270 "w2" ->2271 {2272 attached: Set(),2273 built: false,2274 expecting: false,2275 running: false,2276 session: true,2277 up: true2278 }2279 )2280}22812282[State 2]2283{2284 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2285 schedNoPush::scheduler::crashes: 0,2286 schedNoPush::scheduler::entry: [],2287 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2288 schedNoPush::scheduler::mAssigned: Set(),2289 schedNoPush::scheduler::mBuild: Set(),2290 schedNoPush::scheduler::mDone: Set(),2291 schedNoPush::scheduler::mExpect: Set(),2292 schedNoPush::scheduler::mResult: Set(),2293 schedNoPush::scheduler::mRetry: Set(),2294 schedNoPush::scheduler::mRevoke: Set(),2295 schedNoPush::scheduler::mSchedule: Set("c1", "c2"),2296 schedNoPush::scheduler::published: 0,2297 schedNoPush::scheduler::publishedBy: Set(),2298 schedNoPush::scheduler::ws:2299 Map(2300 "w1" ->2301 {2302 attached: Set(),2303 built: false,2304 expecting: false,2305 running: false,2306 session: true,2307 up: true2308 },2309 "w2" ->2310 {2311 attached: Set(),2312 built: false,2313 expecting: false,2314 running: false,2315 session: true,2316 up: true2317 }2318 )2319}23202321[State 3]2322{2323 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2324 schedNoPush::scheduler::crashes: 0,2325 schedNoPush::scheduler::entry:2326 [{ followers: Set("c2"), leased: true, worker: "w1" }],2327 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2328 schedNoPush::scheduler::mAssigned: Set(("c2", "w1")),2329 schedNoPush::scheduler::mBuild: Set(),2330 schedNoPush::scheduler::mDone: Set(),2331 schedNoPush::scheduler::mExpect: Set(),2332 schedNoPush::scheduler::mResult: Set(),2333 schedNoPush::scheduler::mRetry: Set(),2334 schedNoPush::scheduler::mRevoke: Set(),2335 schedNoPush::scheduler::mSchedule: Set("c1"),2336 schedNoPush::scheduler::published: 0,2337 schedNoPush::scheduler::publishedBy: Set(),2338 schedNoPush::scheduler::ws:2339 Map(2340 "w1" ->2341 {2342 attached: Set(),2343 built: false,2344 expecting: false,2345 running: false,2346 session: true,2347 up: true2348 },2349 "w2" ->2350 {2351 attached: Set(),2352 built: false,2353 expecting: false,2354 running: false,2355 session: true,2356 up: true2357 }2358 )2359}23602361[State 4]2362{2363 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2364 schedNoPush::scheduler::crashes: 0,2365 schedNoPush::scheduler::entry:2366 [{ followers: Set("c2"), leased: true, worker: "w1" }],2367 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2368 schedNoPush::scheduler::mAssigned: Set(),2369 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2370 schedNoPush::scheduler::mDone: Set(),2371 schedNoPush::scheduler::mExpect: Set(),2372 schedNoPush::scheduler::mResult: Set(),2373 schedNoPush::scheduler::mRetry: Set(),2374 schedNoPush::scheduler::mRevoke: Set(),2375 schedNoPush::scheduler::mSchedule: Set("c1"),2376 schedNoPush::scheduler::published: 0,2377 schedNoPush::scheduler::publishedBy: Set(),2378 schedNoPush::scheduler::ws:2379 Map(2380 "w1" ->2381 {2382 attached: Set(),2383 built: false,2384 expecting: false,2385 running: false,2386 session: true,2387 up: true2388 },2389 "w2" ->2390 {2391 attached: Set(),2392 built: false,2393 expecting: false,2394 running: false,2395 session: true,2396 up: true2397 }2398 )2399}24002401[State 5]2402{2403 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2404 schedNoPush::scheduler::crashes: 1,2405 schedNoPush::scheduler::entry: [],2406 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2407 schedNoPush::scheduler::mAssigned: Set(),2408 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2409 schedNoPush::scheduler::mDone: Set(),2410 schedNoPush::scheduler::mExpect: Set(),2411 schedNoPush::scheduler::mResult: Set(),2412 schedNoPush::scheduler::mRetry: Set("c1"),2413 schedNoPush::scheduler::mRevoke: Set(),2414 schedNoPush::scheduler::mSchedule: Set(),2415 schedNoPush::scheduler::published: 0,2416 schedNoPush::scheduler::publishedBy: Set(),2417 schedNoPush::scheduler::ws:2418 Map(2419 "w1" ->2420 {2421 attached: Set(),2422 built: false,2423 expecting: false,2424 running: false,2425 session: false,2426 up: true2427 },2428 "w2" ->2429 {2430 attached: Set(),2431 built: false,2432 expecting: false,2433 running: false,2434 session: false,2435 up: true2436 }2437 )2438}24392440[State 6]2441{2442 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2443 schedNoPush::scheduler::crashes: 1,2444 schedNoPush::scheduler::entry: [],2445 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2446 schedNoPush::scheduler::mAssigned: Set(),2447 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2448 schedNoPush::scheduler::mDone: Set(),2449 schedNoPush::scheduler::mExpect: Set(),2450 schedNoPush::scheduler::mResult: Set(),2451 schedNoPush::scheduler::mRetry: Set(),2452 schedNoPush::scheduler::mRevoke: Set(),2453 schedNoPush::scheduler::mSchedule: Set("c1"),2454 schedNoPush::scheduler::published: 0,2455 schedNoPush::scheduler::publishedBy: Set(),2456 schedNoPush::scheduler::ws:2457 Map(2458 "w1" ->2459 {2460 attached: Set(),2461 built: false,2462 expecting: false,2463 running: false,2464 session: false,2465 up: true2466 },2467 "w2" ->2468 {2469 attached: Set(),2470 built: false,2471 expecting: false,2472 running: false,2473 session: false,2474 up: true2475 }2476 )2477}24782479[State 7]2480{2481 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2482 schedNoPush::scheduler::crashes: 2,2483 schedNoPush::scheduler::entry: [],2484 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2485 schedNoPush::scheduler::mAssigned: Set(),2486 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2487 schedNoPush::scheduler::mDone: Set(),2488 schedNoPush::scheduler::mExpect: Set(),2489 schedNoPush::scheduler::mResult: Set(),2490 schedNoPush::scheduler::mRetry: Set(),2491 schedNoPush::scheduler::mRevoke: Set(),2492 schedNoPush::scheduler::mSchedule: Set("c1"),2493 schedNoPush::scheduler::published: 0,2494 schedNoPush::scheduler::publishedBy: Set(),2495 schedNoPush::scheduler::ws:2496 Map(2497 "w1" ->2498 {2499 attached: Set(),2500 built: false,2501 expecting: false,2502 running: false,2503 session: false,2504 up: false2505 },2506 "w2" ->2507 {2508 attached: Set(),2509 built: false,2510 expecting: false,2511 running: false,2512 session: false,2513 up: true2514 }2515 )2516}25172518[State 8]2519{2520 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2521 schedNoPush::scheduler::crashes: 2,2522 schedNoPush::scheduler::entry: [],2523 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2524 schedNoPush::scheduler::mAssigned: Set(),2525 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2526 schedNoPush::scheduler::mDone: Set(),2527 schedNoPush::scheduler::mExpect: Set(),2528 schedNoPush::scheduler::mResult: Set(),2529 schedNoPush::scheduler::mRetry: Set(),2530 schedNoPush::scheduler::mRevoke: Set(),2531 schedNoPush::scheduler::mSchedule: Set("c1"),2532 schedNoPush::scheduler::published: 0,2533 schedNoPush::scheduler::publishedBy: Set(),2534 schedNoPush::scheduler::ws:2535 Map(2536 "w1" ->2537 {2538 attached: Set(),2539 built: false,2540 expecting: false,2541 running: false,2542 session: true,2543 up: true2544 },2545 "w2" ->2546 {2547 attached: Set(),2548 built: false,2549 expecting: false,2550 running: false,2551 session: false,2552 up: true2553 }2554 )2555}25562557[State 9]2558{2559 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2560 schedNoPush::scheduler::crashes: 2,2561 schedNoPush::scheduler::entry: [],2562 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2563 schedNoPush::scheduler::mAssigned: Set(),2564 schedNoPush::scheduler::mBuild: Set(),2565 schedNoPush::scheduler::mDone: Set(),2566 schedNoPush::scheduler::mExpect: Set(),2567 schedNoPush::scheduler::mResult: Set(),2568 schedNoPush::scheduler::mRetry: Set(),2569 schedNoPush::scheduler::mRevoke: Set(),2570 schedNoPush::scheduler::mSchedule: Set("c1"),2571 schedNoPush::scheduler::published: 0,2572 schedNoPush::scheduler::publishedBy: Set(),2573 schedNoPush::scheduler::ws:2574 Map(2575 "w1" ->2576 {2577 attached: Set("c2"),2578 built: false,2579 expecting: true,2580 running: true,2581 session: true,2582 up: true2583 },2584 "w2" ->2585 {2586 attached: Set(),2587 built: false,2588 expecting: false,2589 running: false,2590 session: false,2591 up: true2592 }2593 )2594}25952596[violation] Found an issue (277ms at 2256 traces/second).2597Use --verbosity=3 to show executions.2598Use --seed=0x8840f5ba9c16a657 --backend=rust to reproduce.2599error: Invariant violated2600An example execution:26012602[State 0]2603{2604 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2605 schedNoReport::scheduler::crashes: 0,2606 schedNoReport::scheduler::entry: [],2607 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2608 schedNoReport::scheduler::mAssigned: Set(),2609 schedNoReport::scheduler::mBuild: Set(),2610 schedNoReport::scheduler::mDone: Set(),2611 schedNoReport::scheduler::mExpect: Set(),2612 schedNoReport::scheduler::mResult: Set(),2613 schedNoReport::scheduler::mRetry: Set(),2614 schedNoReport::scheduler::mRevoke: Set(),2615 schedNoReport::scheduler::mSchedule: Set(),2616 schedNoReport::scheduler::published: 0,2617 schedNoReport::scheduler::publishedBy: Set(),2618 schedNoReport::scheduler::ws:2619 Map(2620 "w1" ->2621 {2622 attached: Set(),2623 built: false,2624 expecting: false,2625 running: false,2626 session: true,2627 up: true2628 },2629 "w2" ->2630 {2631 attached: Set(),2632 built: false,2633 expecting: false,2634 running: false,2635 session: true,2636 up: true2637 }2638 )2639}26402641[State 1]2642{2643 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2644 schedNoReport::scheduler::crashes: 0,2645 schedNoReport::scheduler::entry: [],2646 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2647 schedNoReport::scheduler::mAssigned: Set(),2648 schedNoReport::scheduler::mBuild: Set(),2649 schedNoReport::scheduler::mDone: Set(),2650 schedNoReport::scheduler::mExpect: Set(),2651 schedNoReport::scheduler::mResult: Set(),2652 schedNoReport::scheduler::mRetry: Set(),2653 schedNoReport::scheduler::mRevoke: Set(),2654 schedNoReport::scheduler::mSchedule: Set("c1"),2655 schedNoReport::scheduler::published: 0,2656 schedNoReport::scheduler::publishedBy: Set(),2657 schedNoReport::scheduler::ws:2658 Map(2659 "w1" ->2660 {2661 attached: Set(),2662 built: false,2663 expecting: false,2664 running: false,2665 session: true,2666 up: true2667 },2668 "w2" ->2669 {2670 attached: Set(),2671 built: false,2672 expecting: false,2673 running: false,2674 session: true,2675 up: true2676 }2677 )2678}26792680[State 2]2681{2682 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2683 schedNoReport::scheduler::crashes: 0,2684 schedNoReport::scheduler::entry:2685 [{ followers: Set("c1"), leased: true, worker: "w2" }],2686 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2687 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2688 schedNoReport::scheduler::mBuild: Set(),2689 schedNoReport::scheduler::mDone: Set(),2690 schedNoReport::scheduler::mExpect: Set("w2"),2691 schedNoReport::scheduler::mResult: Set(),2692 schedNoReport::scheduler::mRetry: Set(),2693 schedNoReport::scheduler::mRevoke: Set(),2694 schedNoReport::scheduler::mSchedule: Set(),2695 schedNoReport::scheduler::published: 0,2696 schedNoReport::scheduler::publishedBy: Set(),2697 schedNoReport::scheduler::ws:2698 Map(2699 "w1" ->2700 {2701 attached: Set(),2702 built: false,2703 expecting: false,2704 running: false,2705 session: true,2706 up: true2707 },2708 "w2" ->2709 {2710 attached: Set(),2711 built: false,2712 expecting: false,2713 running: false,2714 session: true,2715 up: true2716 }2717 )2718}27192720[State 3]2721{2722 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2723 schedNoReport::scheduler::crashes: 0,2724 schedNoReport::scheduler::entry:2725 [{ followers: Set("c1"), leased: true, worker: "w2" }],2726 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2727 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2728 schedNoReport::scheduler::mBuild: Set(),2729 schedNoReport::scheduler::mDone: Set(),2730 schedNoReport::scheduler::mExpect: Set(),2731 schedNoReport::scheduler::mResult: Set(),2732 schedNoReport::scheduler::mRetry: Set(),2733 schedNoReport::scheduler::mRevoke: Set(),2734 schedNoReport::scheduler::mSchedule: Set(),2735 schedNoReport::scheduler::published: 0,2736 schedNoReport::scheduler::publishedBy: Set(),2737 schedNoReport::scheduler::ws:2738 Map(2739 "w1" ->2740 {2741 attached: Set(),2742 built: false,2743 expecting: false,2744 running: false,2745 session: true,2746 up: true2747 },2748 "w2" ->2749 {2750 attached: Set(),2751 built: false,2752 expecting: true,2753 running: true,2754 session: true,2755 up: true2756 }2757 )2758}27592760[State 4]2761{2762 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2763 schedNoReport::scheduler::crashes: 1,2764 schedNoReport::scheduler::entry: [],2765 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2766 schedNoReport::scheduler::mAssigned: Set(),2767 schedNoReport::scheduler::mBuild: Set(),2768 schedNoReport::scheduler::mDone: Set(),2769 schedNoReport::scheduler::mExpect: Set(),2770 schedNoReport::scheduler::mResult: Set(),2771 schedNoReport::scheduler::mRetry: Set("c1"),2772 schedNoReport::scheduler::mRevoke: Set(),2773 schedNoReport::scheduler::mSchedule: Set(),2774 schedNoReport::scheduler::published: 0,2775 schedNoReport::scheduler::publishedBy: Set(),2776 schedNoReport::scheduler::ws:2777 Map(2778 "w1" ->2779 {2780 attached: Set(),2781 built: false,2782 expecting: false,2783 running: false,2784 session: false,2785 up: true2786 },2787 "w2" ->2788 {2789 attached: Set(),2790 built: false,2791 expecting: true,2792 running: true,2793 session: false,2794 up: true2795 }2796 )2797}27982799[State 5]2800{2801 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2802 schedNoReport::scheduler::crashes: 2,2803 schedNoReport::scheduler::entry: [],2804 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2805 schedNoReport::scheduler::mAssigned: Set(),2806 schedNoReport::scheduler::mBuild: Set(),2807 schedNoReport::scheduler::mDone: Set(),2808 schedNoReport::scheduler::mExpect: Set(),2809 schedNoReport::scheduler::mResult: Set(),2810 schedNoReport::scheduler::mRetry: Set("c1"),2811 schedNoReport::scheduler::mRevoke: Set(),2812 schedNoReport::scheduler::mSchedule: Set(),2813 schedNoReport::scheduler::published: 0,2814 schedNoReport::scheduler::publishedBy: Set(),2815 schedNoReport::scheduler::ws:2816 Map(2817 "w1" ->2818 {2819 attached: Set(),2820 built: false,2821 expecting: false,2822 running: false,2823 session: false,2824 up: true2825 },2826 "w2" ->2827 {2828 attached: Set(),2829 built: false,2830 expecting: true,2831 running: true,2832 session: false,2833 up: true2834 }2835 )2836}28372838[State 6]2839{2840 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2841 schedNoReport::scheduler::crashes: 2,2842 schedNoReport::scheduler::entry: [],2843 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2844 schedNoReport::scheduler::mAssigned: Set(),2845 schedNoReport::scheduler::mBuild: Set(),2846 schedNoReport::scheduler::mDone: Set(),2847 schedNoReport::scheduler::mExpect: Set(),2848 schedNoReport::scheduler::mResult: Set(),2849 schedNoReport::scheduler::mRetry: Set("c1"),2850 schedNoReport::scheduler::mRevoke: Set(),2851 schedNoReport::scheduler::mSchedule: Set(),2852 schedNoReport::scheduler::published: 0,2853 schedNoReport::scheduler::publishedBy: Set(),2854 schedNoReport::scheduler::ws:2855 Map(2856 "w1" ->2857 {2858 attached: Set(),2859 built: false,2860 expecting: false,2861 running: false,2862 session: true,2863 up: true2864 },2865 "w2" ->2866 {2867 attached: Set(),2868 built: false,2869 expecting: true,2870 running: true,2871 session: false,2872 up: true2873 }2874 )2875}28762877[State 7]2878{2879 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2880 schedNoReport::scheduler::crashes: 2,2881 schedNoReport::scheduler::entry: [],2882 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2883 schedNoReport::scheduler::mAssigned: Set(),2884 schedNoReport::scheduler::mBuild: Set(),2885 schedNoReport::scheduler::mDone: Set(),2886 schedNoReport::scheduler::mExpect: Set(),2887 schedNoReport::scheduler::mResult: Set(),2888 schedNoReport::scheduler::mRetry: Set("c1"),2889 schedNoReport::scheduler::mRevoke: Set(),2890 schedNoReport::scheduler::mSchedule: Set("c2"),2891 schedNoReport::scheduler::published: 0,2892 schedNoReport::scheduler::publishedBy: Set(),2893 schedNoReport::scheduler::ws:2894 Map(2895 "w1" ->2896 {2897 attached: Set(),2898 built: false,2899 expecting: false,2900 running: false,2901 session: true,2902 up: true2903 },2904 "w2" ->2905 {2906 attached: Set(),2907 built: false,2908 expecting: true,2909 running: true,2910 session: false,2911 up: true2912 }2913 )2914}29152916[State 8]2917{2918 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2919 schedNoReport::scheduler::crashes: 2,2920 schedNoReport::scheduler::entry:2921 [{ followers: Set("c2"), leased: true, worker: "w1" }],2922 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2923 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2924 schedNoReport::scheduler::mBuild: Set(),2925 schedNoReport::scheduler::mDone: Set(),2926 schedNoReport::scheduler::mExpect: Set("w1"),2927 schedNoReport::scheduler::mResult: Set(),2928 schedNoReport::scheduler::mRetry: Set("c1"),2929 schedNoReport::scheduler::mRevoke: Set(),2930 schedNoReport::scheduler::mSchedule: Set(),2931 schedNoReport::scheduler::published: 0,2932 schedNoReport::scheduler::publishedBy: Set(),2933 schedNoReport::scheduler::ws:2934 Map(2935 "w1" ->2936 {2937 attached: Set(),2938 built: false,2939 expecting: false,2940 running: false,2941 session: true,2942 up: true2943 },2944 "w2" ->2945 {2946 attached: Set(),2947 built: false,2948 expecting: true,2949 running: true,2950 session: false,2951 up: true2952 }2953 )2954}29552956[State 9]2957{2958 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2959 schedNoReport::scheduler::crashes: 2,2960 schedNoReport::scheduler::entry:2961 [{ followers: Set("c2"), leased: true, worker: "w1" }],2962 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2963 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2964 schedNoReport::scheduler::mBuild: Set(),2965 schedNoReport::scheduler::mDone: Set(),2966 schedNoReport::scheduler::mExpect: Set("w1"),2967 schedNoReport::scheduler::mResult: Set(),2968 schedNoReport::scheduler::mRetry: Set(),2969 schedNoReport::scheduler::mRevoke: Set(),2970 schedNoReport::scheduler::mSchedule: Set("c1"),2971 schedNoReport::scheduler::published: 0,2972 schedNoReport::scheduler::publishedBy: Set(),2973 schedNoReport::scheduler::ws:2974 Map(2975 "w1" ->2976 {2977 attached: Set(),2978 built: false,2979 expecting: false,2980 running: false,2981 session: true,2982 up: true2983 },2984 "w2" ->2985 {2986 attached: Set(),2987 built: false,2988 expecting: true,2989 running: true,2990 session: false,2991 up: true2992 }2993 )2994}29952996[State 10]2997{2998 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2999 schedNoReport::scheduler::crashes: 2,3000 schedNoReport::scheduler::entry:3001 [{ followers: Set("c2"), leased: true, worker: "w1" }],3002 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),3003 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),3004 schedNoReport::scheduler::mBuild: Set(),3005 schedNoReport::scheduler::mDone: Set(),3006 schedNoReport::scheduler::mExpect: Set("w1"),3007 schedNoReport::scheduler::mResult: Set(),3008 schedNoReport::scheduler::mRetry: Set(),3009 schedNoReport::scheduler::mRevoke: Set(),3010 schedNoReport::scheduler::mSchedule: Set("c1"),3011 schedNoReport::scheduler::published: 0,3012 schedNoReport::scheduler::publishedBy: Set(),3013 schedNoReport::scheduler::ws:3014 Map(3015 "w1" ->3016 {3017 attached: Set(),3018 built: false,3019 expecting: false,3020 running: false,3021 session: true,3022 up: true3023 },3024 "w2" ->3025 {3026 attached: Set(),3027 built: false,3028 expecting: true,3029 running: true,3030 session: true,3031 up: true3032 }3033 )3034}30353036[State 11]3037{3038 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),3039 schedNoReport::scheduler::crashes: 2,3040 schedNoReport::scheduler::entry:3041 [{ followers: Set("c2"), leased: true, worker: "w1" }],3042 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),3043 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),3044 schedNoReport::scheduler::mBuild: Set(),3045 schedNoReport::scheduler::mDone: Set(),3046 schedNoReport::scheduler::mExpect: Set(),3047 schedNoReport::scheduler::mResult: Set(),3048 schedNoReport::scheduler::mRetry: Set(),3049 schedNoReport::scheduler::mRevoke: Set(),3050 schedNoReport::scheduler::mSchedule: Set("c1"),3051 schedNoReport::scheduler::published: 0,3052 schedNoReport::scheduler::publishedBy: Set(),3053 schedNoReport::scheduler::ws:3054 Map(3055 "w1" ->3056 {3057 attached: Set(),3058 built: false,3059 expecting: true,3060 running: true,3061 session: true,3062 up: true3063 },3064 "w2" ->3065 {3066 attached: Set(),3067 built: false,3068 expecting: true,3069 running: true,3070 session: true,3071 up: true3072 }3073 )3074}30753076[violation] Found an issue (1065ms at 2600 traces/second).3077Use --verbosity=3 to show executions.3078Use --seed=0x558aed1f90017d93 --backend=rust to reproduce.3079error: Invariant violated3080An example execution:30813082[State 0]3083{3084 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3085 schedTerminal::scheduler::crashes: 0,3086 schedTerminal::scheduler::entry: [],3087 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3088 schedTerminal::scheduler::mAssigned: Set(),3089 schedTerminal::scheduler::mBuild: Set(),3090 schedTerminal::scheduler::mDone: Set(),3091 schedTerminal::scheduler::mExpect: Set(),3092 schedTerminal::scheduler::mResult: Set(),3093 schedTerminal::scheduler::mRetry: Set(),3094 schedTerminal::scheduler::mRevoke: Set(),3095 schedTerminal::scheduler::mSchedule: Set(),3096 schedTerminal::scheduler::published: 0,3097 schedTerminal::scheduler::publishedBy: Set(),3098 schedTerminal::scheduler::ws:3099 Map(3100 "w1" ->3101 {3102 attached: Set(),3103 built: false,3104 expecting: false,3105 running: false,3106 session: true,3107 up: true3108 },3109 "w2" ->3110 {3111 attached: Set(),3112 built: false,3113 expecting: false,3114 running: false,3115 session: true,3116 up: true3117 }3118 )3119}31203121[State 1]3122{3123 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3124 schedTerminal::scheduler::crashes: 1,3125 schedTerminal::scheduler::entry: [],3126 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3127 schedTerminal::scheduler::mAssigned: Set(),3128 schedTerminal::scheduler::mBuild: Set(),3129 schedTerminal::scheduler::mDone: Set(),3130 schedTerminal::scheduler::mExpect: Set(),3131 schedTerminal::scheduler::mResult: Set(),3132 schedTerminal::scheduler::mRetry: Set(),3133 schedTerminal::scheduler::mRevoke: Set(),3134 schedTerminal::scheduler::mSchedule: Set(),3135 schedTerminal::scheduler::published: 0,3136 schedTerminal::scheduler::publishedBy: Set(),3137 schedTerminal::scheduler::ws:3138 Map(3139 "w1" ->3140 {3141 attached: Set(),3142 built: false,3143 expecting: false,3144 running: false,3145 session: false,3146 up: true3147 },3148 "w2" ->3149 {3150 attached: Set(),3151 built: false,3152 expecting: false,3153 running: false,3154 session: false,3155 up: true3156 }3157 )3158}31593160[State 2]3161{3162 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3163 schedTerminal::scheduler::crashes: 1,3164 schedTerminal::scheduler::entry: [],3165 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3166 schedTerminal::scheduler::mAssigned: Set(),3167 schedTerminal::scheduler::mBuild: Set(),3168 schedTerminal::scheduler::mDone: Set(),3169 schedTerminal::scheduler::mExpect: Set(),3170 schedTerminal::scheduler::mResult: Set(),3171 schedTerminal::scheduler::mRetry: Set(),3172 schedTerminal::scheduler::mRevoke: Set(),3173 schedTerminal::scheduler::mSchedule: Set("c2"),3174 schedTerminal::scheduler::published: 0,3175 schedTerminal::scheduler::publishedBy: Set(),3176 schedTerminal::scheduler::ws:3177 Map(3178 "w1" ->3179 {3180 attached: Set(),3181 built: false,3182 expecting: false,3183 running: false,3184 session: false,3185 up: true3186 },3187 "w2" ->3188 {3189 attached: Set(),3190 built: false,3191 expecting: false,3192 running: false,3193 session: false,3194 up: true3195 }3196 )3197}31983199[State 3]3200{3201 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3202 schedTerminal::scheduler::crashes: 1,3203 schedTerminal::scheduler::entry: [],3204 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3205 schedTerminal::scheduler::mAssigned: Set(),3206 schedTerminal::scheduler::mBuild: Set(),3207 schedTerminal::scheduler::mDone: Set(),3208 schedTerminal::scheduler::mExpect: Set(),3209 schedTerminal::scheduler::mResult: Set(),3210 schedTerminal::scheduler::mRetry: Set(),3211 schedTerminal::scheduler::mRevoke: Set(),3212 schedTerminal::scheduler::mSchedule: Set(),3213 schedTerminal::scheduler::published: 0,3214 schedTerminal::scheduler::publishedBy: Set(),3215 schedTerminal::scheduler::ws:3216 Map(3217 "w1" ->3218 {3219 attached: Set(),3220 built: false,3221 expecting: false,3222 running: false,3223 session: false,3224 up: true3225 },3226 "w2" ->3227 {3228 attached: Set(),3229 built: false,3230 expecting: false,3231 running: false,3232 session: false,3233 up: true3234 }3235 )3236}32373238[violation] Found an issue (88ms at 659 traces/second).3239Use --verbosity=3 to show executions.3240Use --seed=0x111c0f4fe1eba0d2 --backend=rust to reproduce.3241error: Invariant violated3242An example execution:32433244[State 0]3245{3246 pushFixed::push::byPath: Map(),3247 pushFixed::push::inflight: Set(),3248 pushFixed::push::left: Map(),3249 pushFixed::push::sent: Map()3250}32513252[State 1]3253{3254 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3255 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3256 pushFixed::push::left: Map(2 -> 2),3257 pushFixed::push::sent: Map(2 -> Set("a", "b"))3258}32593260[State 2]3261{3262 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3263 pushFixed::push::inflight: Set((2, "b")),3264 pushFixed::push::left: Map(2 -> 1),3265 pushFixed::push::sent: Map(2 -> Set("a", "b"))3266}32673268[State 3]3269{3270 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3271 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "b")),3272 pushFixed::push::left: Map(1 -> 2, 2 -> 1),3273 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3274}32753276[State 4]3277{3278 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3279 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3280 pushFixed::push::left: Map(1 -> 2, 2 -> 0),3281 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3282}32833284[State 5]3285{3286 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3287 pushFixed::push::inflight: Set((1, "a")),3288 pushFixed::push::left: Map(1 -> 1, 2 -> 0),3289 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3290}32913292[State 6]3293{3294 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3295 pushFixed::push::inflight: Set(),3296 pushFixed::push::left: Map(1 -> 0, 2 -> 0),3297 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3298}32993300[State 7]3301{3302 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3303 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3304 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 2),3305 pushFixed::push::sent:3306 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3307}33083309[State 8]3310{3311 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3312 pushFixed::push::inflight: Set((3, "b")),3313 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 1),3314 pushFixed::push::sent:3315 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3316}33173318[State 9]3319{3320 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3321 pushFixed::push::inflight: Set(),3322 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3323 pushFixed::push::sent:3324 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3325}33263327[ok] No violation found (465ms at 43011 traces/second).3328Trace length statistics: max=10, min=7, average=8.033329You may increase --max-samples and --max-steps.3330Use --verbosity to produce more (or less) output.3331Use --seed=0x281acaa350d1ac7 --backend=rust to reproduce.