nix-grpc-store-spec
checks.aarch64-linux.spec
· build #847
· raw
1tribuchet: building on eliza2An example execution:34[State 0]5{6 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),7 schedFixed::scheduler::crashes: 0,8 schedFixed::scheduler::entry: [],9 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),10 schedFixed::scheduler::mAssigned: Set(),11 schedFixed::scheduler::mBuild: Set(),12 schedFixed::scheduler::mDone: Set(),13 schedFixed::scheduler::mExpect: Set(),14 schedFixed::scheduler::mResult: Set(),15 schedFixed::scheduler::mRetry: Set(),16 schedFixed::scheduler::mRevoke: Set(),17 schedFixed::scheduler::mSchedule: Set(),18 schedFixed::scheduler::published: 0,19 schedFixed::scheduler::publishedBy: Set(),20 schedFixed::scheduler::ws:21 Map(22 "w1" ->23 {24 attached: Set(),25 built: false,26 expecting: false,27 running: false,28 session: true,29 up: true30 },31 "w2" ->32 {33 attached: Set(),34 built: false,35 expecting: false,36 running: false,37 session: true,38 up: true39 }40 )41}4243[State 1]44{45 schedFixed::scheduler::cl: Map("c1" -> 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" -> CQueued, "c2" -> CIdle),85 schedFixed::scheduler::crashes: 1,86 schedFixed::scheduler::entry: [],87 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),88 schedFixed::scheduler::mAssigned: Set(),89 schedFixed::scheduler::mBuild: Set(),90 schedFixed::scheduler::mDone: Set(),91 schedFixed::scheduler::mExpect: Set(),92 schedFixed::scheduler::mResult: Set(),93 schedFixed::scheduler::mRetry: Set(),94 schedFixed::scheduler::mRevoke: Set(),95 schedFixed::scheduler::mSchedule: Set("c1"),96 schedFixed::scheduler::published: 0,97 schedFixed::scheduler::publishedBy: Set(),98 schedFixed::scheduler::ws:99 Map(100 "w1" ->101 {102 attached: Set(),103 built: false,104 expecting: false,105 running: false,106 session: false,107 up: true108 },109 "w2" ->110 {111 attached: Set(),112 built: false,113 expecting: false,114 running: false,115 session: false,116 up: true117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),124 schedFixed::scheduler::crashes: 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("c1"),133 schedFixed::scheduler::mRevoke: Set(),134 schedFixed::scheduler::mSchedule: Set(),135 schedFixed::scheduler::published: 0,136 schedFixed::scheduler::publishedBy: Set(),137 schedFixed::scheduler::ws:138 Map(139 "w1" ->140 {141 attached: Set(),142 built: false,143 expecting: false,144 running: false,145 session: false,146 up: true147 },148 "w2" ->149 {150 attached: Set(),151 built: false,152 expecting: false,153 running: false,154 session: false,155 up: true156 }157 )158}159160[State 4]161{162 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),163 schedFixed::scheduler::crashes: 2,164 schedFixed::scheduler::entry: [],165 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),166 schedFixed::scheduler::mAssigned: Set(),167 schedFixed::scheduler::mBuild: Set(),168 schedFixed::scheduler::mDone: Set(),169 schedFixed::scheduler::mExpect: Set(),170 schedFixed::scheduler::mResult: Set(),171 schedFixed::scheduler::mRetry: Set(),172 schedFixed::scheduler::mRevoke: Set(),173 schedFixed::scheduler::mSchedule: Set("c1"),174 schedFixed::scheduler::published: 0,175 schedFixed::scheduler::publishedBy: Set(),176 schedFixed::scheduler::ws:177 Map(178 "w1" ->179 {180 attached: Set(),181 built: false,182 expecting: false,183 running: false,184 session: false,185 up: true186 },187 "w2" ->188 {189 attached: Set(),190 built: false,191 expecting: false,192 running: false,193 session: false,194 up: true195 }196 )197}198199[State 5]200{201 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),202 schedFixed::scheduler::crashes: 2,203 schedFixed::scheduler::entry: [],204 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),205 schedFixed::scheduler::mAssigned: Set(),206 schedFixed::scheduler::mBuild: Set(),207 schedFixed::scheduler::mDone: Set(),208 schedFixed::scheduler::mExpect: Set(),209 schedFixed::scheduler::mResult: Set(),210 schedFixed::scheduler::mRetry: Set(),211 schedFixed::scheduler::mRevoke: Set(),212 schedFixed::scheduler::mSchedule: Set("c1"),213 schedFixed::scheduler::published: 0,214 schedFixed::scheduler::publishedBy: Set(),215 schedFixed::scheduler::ws:216 Map(217 "w1" ->218 {219 attached: Set(),220 built: false,221 expecting: false,222 running: false,223 session: false,224 up: true225 },226 "w2" ->227 {228 attached: Set(),229 built: false,230 expecting: false,231 running: false,232 session: true,233 up: true234 }235 )236}237238[State 6]239{240 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),241 schedFixed::scheduler::crashes: 2,242 schedFixed::scheduler::entry:243 [{ 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(),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: true265 },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" -> CIdle),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(),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: true305 },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" -> CIdle),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(("c1", "w2")),327 schedFixed::scheduler::mDone: Set(),328 schedFixed::scheduler::mExpect: Set("w2"),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: true,353 up: true354 }355 )356}357358[State 9]359{360 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),361 schedFixed::scheduler::crashes: 2,362 schedFixed::scheduler::entry:363 [{ followers: Set("c1"), leased: true, worker: "w2" }],364 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),365 schedFixed::scheduler::mAssigned: Set(),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: 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" -> CQueued, "c2" -> CIdle),401 schedFixed::scheduler::crashes: 2,402 schedFixed::scheduler::entry:403 [{ followers: Set("c1"), leased: true, worker: "w2" }],404 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),405 schedFixed::scheduler::mAssigned: Set(),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(),411 schedFixed::scheduler::mRevoke: Set(),412 schedFixed::scheduler::mSchedule: Set("c1"),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"), leased: true, worker: "w2" }],444 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),445 schedFixed::scheduler::mAssigned: Set(),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", "c2"),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"), leased: true, worker: "w2" }],484 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),485 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),486 schedFixed::scheduler::mBuild: Set(),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("c2"),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("w2"), "c2" -> CQueued),521 schedFixed::scheduler::crashes: 2,522 schedFixed::scheduler::entry:523 [{ followers: Set("c1"), leased: true, worker: "w2" }],524 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),525 schedFixed::scheduler::mAssigned: Set(),526 schedFixed::scheduler::mBuild: Set(("c1", "w2")),527 schedFixed::scheduler::mDone: Set(),528 schedFixed::scheduler::mExpect: Set("w2"),529 schedFixed::scheduler::mResult: Set(),530 schedFixed::scheduler::mRetry: Set(),531 schedFixed::scheduler::mRevoke: Set(),532 schedFixed::scheduler::mSchedule: Set("c2"),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("w2"), "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(("c2", "w2")),566 schedFixed::scheduler::mBuild: Set(("c1", "w2")),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(),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("w2"), "c2" -> CSent("w2")),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(),606 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w2")),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(),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" -> CSent("w2")),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("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" -> 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(("c1", "w2")),687 schedFixed::scheduler::mDone: Set(),688 schedFixed::scheduler::mExpect: Set("w2"),689 schedFixed::scheduler::mResult: Set(),690 schedFixed::scheduler::mRetry: Set(),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(("c1", "w2")),727 schedFixed::scheduler::mDone: Set(),728 schedFixed::scheduler::mExpect: Set("w2"),729 schedFixed::scheduler::mResult: Set(),730 schedFixed::scheduler::mRetry: Set(),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(("c1", "w2"), ("c2", "w2")),767 schedFixed::scheduler::mDone: Set(),768 schedFixed::scheduler::mExpect: Set("w2"),769 schedFixed::scheduler::mResult: Set(),770 schedFixed::scheduler::mRetry: Set(),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(("c2", "w2")),807 schedFixed::scheduler::mDone: Set(),808 schedFixed::scheduler::mExpect: Set("w2"),809 schedFixed::scheduler::mResult: Set(),810 schedFixed::scheduler::mRetry: Set("c1"),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(("c2", "w2")),847 schedFixed::scheduler::mDone: Set(),848 schedFixed::scheduler::mExpect: Set(),849 schedFixed::scheduler::mResult: Set(),850 schedFixed::scheduler::mRetry: Set("c1"),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(("c2", "w2")),887 schedFixed::scheduler::mDone: Set(),888 schedFixed::scheduler::mExpect: Set(),889 schedFixed::scheduler::mResult: Set(),890 schedFixed::scheduler::mRetry: Set(),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" -> CSent("w2")),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(("c1", "w2")),926 schedFixed::scheduler::mBuild: Set(("c2", "w2")),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(),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" -> CSent("w2")),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(("c1", "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(),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("c2"),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" -> CSent("w2"), "c2" -> CSent("w2")),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(),1006 schedFixed::scheduler::mBuild: Set(("c1", "w2")),1007 schedFixed::scheduler::mDone: Set(),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(),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("c2"),1029 built: false,1030 expecting: true,1031 running: true,1032 session: true,1033 up: true1034 }1035 )1036}10371038[State 26]1039{1040 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),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(),1046 schedFixed::scheduler::mBuild: Set(("c1", "w2")),1047 schedFixed::scheduler::mDone: Set("w2"),1048 schedFixed::scheduler::mExpect: Set(),1049 schedFixed::scheduler::mResult: Set("c2"),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" -> CSent("w2"), "c2" -> CDone),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(("c1", "w2")),1087 schedFixed::scheduler::mDone: Set("w2"),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: 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" -> CSent("w2"), "c2" -> CDone),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"),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" -> CSent("w2"), "c2" -> CDone),1161 schedFixed::scheduler::crashes: 2,1162 schedFixed::scheduler::entry: [],1163 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1164 schedFixed::scheduler::mAssigned: Set(),1165 schedFixed::scheduler::mBuild: Set(),1166 schedFixed::scheduler::mDone: Set(),1167 schedFixed::scheduler::mExpect: Set(),1168 schedFixed::scheduler::mResult: Set("c1"),1169 schedFixed::scheduler::mRetry: Set(),1170 schedFixed::scheduler::mRevoke: Set(),1171 schedFixed::scheduler::mSchedule: Set(),1172 schedFixed::scheduler::published: 1,1173 schedFixed::scheduler::publishedBy: Set("w2"),1174 schedFixed::scheduler::ws:1175 Map(1176 "w1" ->1177 {1178 attached: Set(),1179 built: false,1180 expecting: false,1181 running: false,1182 session: true,1183 up: true1184 },1185 "w2" ->1186 {1187 attached: Set(),1188 built: true,1189 expecting: false,1190 running: false,1191 session: true,1192 up: true1193 }1194 )1195}11961197[State 30]1198{1199 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),1200 schedFixed::scheduler::crashes: 2,1201 schedFixed::scheduler::entry: [],1202 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1203 schedFixed::scheduler::mAssigned: Set(),1204 schedFixed::scheduler::mBuild: Set(),1205 schedFixed::scheduler::mDone: Set(),1206 schedFixed::scheduler::mExpect: Set(),1207 schedFixed::scheduler::mResult: Set(),1208 schedFixed::scheduler::mRetry: Set(),1209 schedFixed::scheduler::mRevoke: Set(),1210 schedFixed::scheduler::mSchedule: Set(),1211 schedFixed::scheduler::published: 1,1212 schedFixed::scheduler::publishedBy: Set("w2"),1213 schedFixed::scheduler::ws:1214 Map(1215 "w1" ->1216 {1217 attached: Set(),1218 built: false,1219 expecting: false,1220 running: false,1221 session: true,1222 up: true1223 },1224 "w2" ->1225 {1226 attached: Set(),1227 built: true,1228 expecting: false,1229 running: false,1230 session: true,1231 up: true1232 }1233 )1234}12351236[ok] No violation found (610ms at 49180 traces/second).1237Trace length statistics: max=29, min=15, average=19.021238You may increase --max-samples and --max-steps.1239Use --verbosity to produce more (or less) output.1240Use --seed=0xb4c2f795ebff3671 --backend=rust to reproduce.1241An example execution:12421243[State 0]1244{1245 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1246 schedNoRevoke::scheduler::crashes: 0,1247 schedNoRevoke::scheduler::entry: [],1248 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1249 schedNoRevoke::scheduler::mAssigned: Set(),1250 schedNoRevoke::scheduler::mBuild: Set(),1251 schedNoRevoke::scheduler::mDone: Set(),1252 schedNoRevoke::scheduler::mExpect: Set(),1253 schedNoRevoke::scheduler::mResult: Set(),1254 schedNoRevoke::scheduler::mRetry: Set(),1255 schedNoRevoke::scheduler::mRevoke: Set(),1256 schedNoRevoke::scheduler::mSchedule: Set(),1257 schedNoRevoke::scheduler::published: 0,1258 schedNoRevoke::scheduler::publishedBy: Set(),1259 schedNoRevoke::scheduler::ws:1260 Map(1261 "w1" ->1262 {1263 attached: Set(),1264 built: false,1265 expecting: false,1266 running: false,1267 session: true,1268 up: true1269 },1270 "w2" ->1271 {1272 attached: Set(),1273 built: false,1274 expecting: false,1275 running: false,1276 session: true,1277 up: true1278 }1279 )1280}12811282[State 1]1283{1284 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1285 schedNoRevoke::scheduler::crashes: 0,1286 schedNoRevoke::scheduler::entry: [],1287 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1288 schedNoRevoke::scheduler::mAssigned: Set(),1289 schedNoRevoke::scheduler::mBuild: Set(),1290 schedNoRevoke::scheduler::mDone: Set(),1291 schedNoRevoke::scheduler::mExpect: Set(),1292 schedNoRevoke::scheduler::mResult: Set(),1293 schedNoRevoke::scheduler::mRetry: Set(),1294 schedNoRevoke::scheduler::mRevoke: Set(),1295 schedNoRevoke::scheduler::mSchedule: Set("c1"),1296 schedNoRevoke::scheduler::published: 0,1297 schedNoRevoke::scheduler::publishedBy: Set(),1298 schedNoRevoke::scheduler::ws:1299 Map(1300 "w1" ->1301 {1302 attached: Set(),1303 built: false,1304 expecting: false,1305 running: false,1306 session: true,1307 up: true1308 },1309 "w2" ->1310 {1311 attached: Set(),1312 built: false,1313 expecting: false,1314 running: false,1315 session: true,1316 up: true1317 }1318 )1319}13201321[State 2]1322{1323 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1324 schedNoRevoke::scheduler::crashes: 1,1325 schedNoRevoke::scheduler::entry: [],1326 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1327 schedNoRevoke::scheduler::mAssigned: Set(),1328 schedNoRevoke::scheduler::mBuild: Set(),1329 schedNoRevoke::scheduler::mDone: Set(),1330 schedNoRevoke::scheduler::mExpect: Set(),1331 schedNoRevoke::scheduler::mResult: Set(),1332 schedNoRevoke::scheduler::mRetry: Set(),1333 schedNoRevoke::scheduler::mRevoke: Set(),1334 schedNoRevoke::scheduler::mSchedule: Set("c1"),1335 schedNoRevoke::scheduler::published: 0,1336 schedNoRevoke::scheduler::publishedBy: Set(),1337 schedNoRevoke::scheduler::ws:1338 Map(1339 "w1" ->1340 {1341 attached: Set(),1342 built: false,1343 expecting: false,1344 running: false,1345 session: true,1346 up: true1347 },1348 "w2" ->1349 {1350 attached: Set(),1351 built: false,1352 expecting: false,1353 running: false,1354 session: false,1355 up: false1356 }1357 )1358}13591360[State 3]1361{1362 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1363 schedNoRevoke::scheduler::crashes: 1,1364 schedNoRevoke::scheduler::entry:1365 [{ followers: Set("c1"), leased: true, worker: "w1" }],1366 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1367 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1368 schedNoRevoke::scheduler::mBuild: Set(),1369 schedNoRevoke::scheduler::mDone: Set(),1370 schedNoRevoke::scheduler::mExpect: Set("w1"),1371 schedNoRevoke::scheduler::mResult: Set(),1372 schedNoRevoke::scheduler::mRetry: Set(),1373 schedNoRevoke::scheduler::mRevoke: Set(),1374 schedNoRevoke::scheduler::mSchedule: Set(),1375 schedNoRevoke::scheduler::published: 0,1376 schedNoRevoke::scheduler::publishedBy: Set(),1377 schedNoRevoke::scheduler::ws:1378 Map(1379 "w1" ->1380 {1381 attached: Set(),1382 built: false,1383 expecting: false,1384 running: false,1385 session: true,1386 up: true1387 },1388 "w2" ->1389 {1390 attached: Set(),1391 built: false,1392 expecting: false,1393 running: false,1394 session: false,1395 up: false1396 }1397 )1398}13991400[State 4]1401{1402 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1403 schedNoRevoke::scheduler::crashes: 1,1404 schedNoRevoke::scheduler::entry:1405 [{ followers: Set("c1"), leased: true, worker: "w1" }],1406 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1407 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1408 schedNoRevoke::scheduler::mBuild: Set(),1409 schedNoRevoke::scheduler::mDone: Set(),1410 schedNoRevoke::scheduler::mExpect: Set(),1411 schedNoRevoke::scheduler::mResult: Set(),1412 schedNoRevoke::scheduler::mRetry: Set(),1413 schedNoRevoke::scheduler::mRevoke: Set(),1414 schedNoRevoke::scheduler::mSchedule: Set(),1415 schedNoRevoke::scheduler::published: 0,1416 schedNoRevoke::scheduler::publishedBy: Set(),1417 schedNoRevoke::scheduler::ws:1418 Map(1419 "w1" ->1420 {1421 attached: Set(),1422 built: false,1423 expecting: true,1424 running: true,1425 session: true,1426 up: true1427 },1428 "w2" ->1429 {1430 attached: Set(),1431 built: false,1432 expecting: false,1433 running: false,1434 session: false,1435 up: false1436 }1437 )1438}14391440[State 5]1441{1442 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1443 schedNoRevoke::scheduler::crashes: 2,1444 schedNoRevoke::scheduler::entry: [],1445 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1446 schedNoRevoke::scheduler::mAssigned: Set(),1447 schedNoRevoke::scheduler::mBuild: Set(),1448 schedNoRevoke::scheduler::mDone: Set(),1449 schedNoRevoke::scheduler::mExpect: Set(),1450 schedNoRevoke::scheduler::mResult: Set(),1451 schedNoRevoke::scheduler::mRetry: Set("c1"),1452 schedNoRevoke::scheduler::mRevoke: Set(),1453 schedNoRevoke::scheduler::mSchedule: Set(),1454 schedNoRevoke::scheduler::published: 0,1455 schedNoRevoke::scheduler::publishedBy: Set(),1456 schedNoRevoke::scheduler::ws:1457 Map(1458 "w1" ->1459 {1460 attached: Set(),1461 built: false,1462 expecting: true,1463 running: true,1464 session: false,1465 up: true1466 },1467 "w2" ->1468 {1469 attached: Set(),1470 built: false,1471 expecting: false,1472 running: false,1473 session: false,1474 up: false1475 }1476 )1477}14781479[State 6]1480{1481 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1482 schedNoRevoke::scheduler::crashes: 2,1483 schedNoRevoke::scheduler::entry: [],1484 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1485 schedNoRevoke::scheduler::mAssigned: Set(),1486 schedNoRevoke::scheduler::mBuild: Set(),1487 schedNoRevoke::scheduler::mDone: Set(),1488 schedNoRevoke::scheduler::mExpect: Set(),1489 schedNoRevoke::scheduler::mResult: Set(),1490 schedNoRevoke::scheduler::mRetry: Set("c1"),1491 schedNoRevoke::scheduler::mRevoke: Set(),1492 schedNoRevoke::scheduler::mSchedule: Set(),1493 schedNoRevoke::scheduler::published: 0,1494 schedNoRevoke::scheduler::publishedBy: Set(),1495 schedNoRevoke::scheduler::ws:1496 Map(1497 "w1" ->1498 {1499 attached: Set(),1500 built: false,1501 expecting: true,1502 running: true,1503 session: false,1504 up: true1505 },1506 "w2" ->1507 {1508 attached: Set(),1509 built: false,1510 expecting: false,1511 running: false,1512 session: true,1513 up: true1514 }1515 )1516}15171518[State 7]1519{1520 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1521 schedNoRevoke::scheduler::crashes: 2,1522 schedNoRevoke::scheduler::entry: [],1523 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1524 schedNoRevoke::scheduler::mAssigned: Set(),1525 schedNoRevoke::scheduler::mBuild: Set(),1526 schedNoRevoke::scheduler::mDone: Set(),1527 schedNoRevoke::scheduler::mExpect: Set(),1528 schedNoRevoke::scheduler::mResult: Set(),1529 schedNoRevoke::scheduler::mRetry: Set("c1"),1530 schedNoRevoke::scheduler::mRevoke: Set(),1531 schedNoRevoke::scheduler::mSchedule: Set("c2"),1532 schedNoRevoke::scheduler::published: 0,1533 schedNoRevoke::scheduler::publishedBy: Set(),1534 schedNoRevoke::scheduler::ws:1535 Map(1536 "w1" ->1537 {1538 attached: Set(),1539 built: false,1540 expecting: true,1541 running: true,1542 session: false,1543 up: true1544 },1545 "w2" ->1546 {1547 attached: Set(),1548 built: false,1549 expecting: false,1550 running: false,1551 session: true,1552 up: true1553 }1554 )1555}15561557[State 8]1558{1559 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1560 schedNoRevoke::scheduler::crashes: 2,1561 schedNoRevoke::scheduler::entry:1562 [{ followers: Set("c2"), leased: true, worker: "w2" }],1563 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1564 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1565 schedNoRevoke::scheduler::mBuild: Set(),1566 schedNoRevoke::scheduler::mDone: Set(),1567 schedNoRevoke::scheduler::mExpect: Set("w2"),1568 schedNoRevoke::scheduler::mResult: Set(),1569 schedNoRevoke::scheduler::mRetry: Set("c1"),1570 schedNoRevoke::scheduler::mRevoke: Set(),1571 schedNoRevoke::scheduler::mSchedule: Set(),1572 schedNoRevoke::scheduler::published: 0,1573 schedNoRevoke::scheduler::publishedBy: Set(),1574 schedNoRevoke::scheduler::ws:1575 Map(1576 "w1" ->1577 {1578 attached: Set(),1579 built: false,1580 expecting: true,1581 running: true,1582 session: false,1583 up: true1584 },1585 "w2" ->1586 {1587 attached: Set(),1588 built: false,1589 expecting: false,1590 running: false,1591 session: true,1592 up: true1593 }1594 )1595}15961597[State 9]1598{1599 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1600 schedNoRevoke::scheduler::crashes: 2,1601 schedNoRevoke::scheduler::entry:1602 [{ followers: Set("c2"), leased: true, worker: "w2" }],1603 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1604 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1605 schedNoRevoke::scheduler::mBuild: Set(),1606 schedNoRevoke::scheduler::mDone: Set(),1607 schedNoRevoke::scheduler::mExpect: Set(),1608 schedNoRevoke::scheduler::mResult: Set(),1609 schedNoRevoke::scheduler::mRetry: Set("c1"),1610 schedNoRevoke::scheduler::mRevoke: Set(),1611 schedNoRevoke::scheduler::mSchedule: Set(),1612 schedNoRevoke::scheduler::published: 0,1613 schedNoRevoke::scheduler::publishedBy: Set(),1614 schedNoRevoke::scheduler::ws:1615 Map(1616 "w1" ->1617 {1618 attached: Set(),1619 built: false,1620 expecting: true,1621 running: true,1622 session: false,1623 up: true1624 },1625 "w2" ->1626 {1627 attached: Set(),1628 built: false,1629 expecting: true,1630 running: true,1631 session: true,1632 up: true1633 }1634 )1635}16361637[State 10]1638{1639 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1640 schedNoRevoke::scheduler::crashes: 2,1641 schedNoRevoke::scheduler::entry:1642 [{ followers: Set("c2"), leased: true, worker: "w2" }],1643 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1644 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1645 schedNoRevoke::scheduler::mBuild: Set(),1646 schedNoRevoke::scheduler::mDone: Set(),1647 schedNoRevoke::scheduler::mExpect: Set(),1648 schedNoRevoke::scheduler::mResult: Set(),1649 schedNoRevoke::scheduler::mRetry: Set("c1"),1650 schedNoRevoke::scheduler::mRevoke: Set(),1651 schedNoRevoke::scheduler::mSchedule: Set(),1652 schedNoRevoke::scheduler::published: 0,1653 schedNoRevoke::scheduler::publishedBy: Set(),1654 schedNoRevoke::scheduler::ws:1655 Map(1656 "w1" ->1657 {1658 attached: Set(),1659 built: false,1660 expecting: true,1661 running: true,1662 session: true,1663 up: true1664 },1665 "w2" ->1666 {1667 attached: Set(),1668 built: false,1669 expecting: true,1670 running: true,1671 session: true,1672 up: true1673 }1674 )1675}16761677[violation] Found an issue (580ms at 49238 traces/second).1678Use --verbosity=3 to show executions.1679Use --seed=0x3ab2a1fbae0c2e53 --backend=rust to reproduce.1680error: Invariant violated1681An example execution:16821683[State 0]1684{1685 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1686 schedNoFence::scheduler::crashes: 0,1687 schedNoFence::scheduler::entry: [],1688 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1689 schedNoFence::scheduler::mAssigned: Set(),1690 schedNoFence::scheduler::mBuild: Set(),1691 schedNoFence::scheduler::mDone: Set(),1692 schedNoFence::scheduler::mExpect: Set(),1693 schedNoFence::scheduler::mResult: Set(),1694 schedNoFence::scheduler::mRetry: Set(),1695 schedNoFence::scheduler::mRevoke: Set(),1696 schedNoFence::scheduler::mSchedule: Set(),1697 schedNoFence::scheduler::published: 0,1698 schedNoFence::scheduler::publishedBy: Set(),1699 schedNoFence::scheduler::ws:1700 Map(1701 "w1" ->1702 {1703 attached: Set(),1704 built: false,1705 expecting: false,1706 running: false,1707 session: true,1708 up: true1709 },1710 "w2" ->1711 {1712 attached: Set(),1713 built: false,1714 expecting: false,1715 running: false,1716 session: true,1717 up: true1718 }1719 )1720}17211722[State 1]1723{1724 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1725 schedNoFence::scheduler::crashes: 0,1726 schedNoFence::scheduler::entry: [],1727 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1728 schedNoFence::scheduler::mAssigned: Set(),1729 schedNoFence::scheduler::mBuild: Set(),1730 schedNoFence::scheduler::mDone: Set(),1731 schedNoFence::scheduler::mExpect: Set(),1732 schedNoFence::scheduler::mResult: Set(),1733 schedNoFence::scheduler::mRetry: Set(),1734 schedNoFence::scheduler::mRevoke: Set(),1735 schedNoFence::scheduler::mSchedule: Set("c2"),1736 schedNoFence::scheduler::published: 0,1737 schedNoFence::scheduler::publishedBy: Set(),1738 schedNoFence::scheduler::ws:1739 Map(1740 "w1" ->1741 {1742 attached: Set(),1743 built: false,1744 expecting: false,1745 running: false,1746 session: true,1747 up: true1748 },1749 "w2" ->1750 {1751 attached: Set(),1752 built: false,1753 expecting: false,1754 running: false,1755 session: true,1756 up: true1757 }1758 )1759}17601761[State 2]1762{1763 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1764 schedNoFence::scheduler::crashes: 0,1765 schedNoFence::scheduler::entry:1766 [{ followers: Set("c2"), leased: true, worker: "w1" }],1767 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1768 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1769 schedNoFence::scheduler::mBuild: Set(),1770 schedNoFence::scheduler::mDone: Set(),1771 schedNoFence::scheduler::mExpect: Set("w1"),1772 schedNoFence::scheduler::mResult: Set(),1773 schedNoFence::scheduler::mRetry: Set(),1774 schedNoFence::scheduler::mRevoke: Set(),1775 schedNoFence::scheduler::mSchedule: Set(),1776 schedNoFence::scheduler::published: 0,1777 schedNoFence::scheduler::publishedBy: Set(),1778 schedNoFence::scheduler::ws:1779 Map(1780 "w1" ->1781 {1782 attached: Set(),1783 built: false,1784 expecting: false,1785 running: false,1786 session: true,1787 up: true1788 },1789 "w2" ->1790 {1791 attached: Set(),1792 built: false,1793 expecting: false,1794 running: false,1795 session: true,1796 up: true1797 }1798 )1799}18001801[State 3]1802{1803 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1804 schedNoFence::scheduler::crashes: 0,1805 schedNoFence::scheduler::entry:1806 [{ followers: Set("c2"), leased: true, worker: "w1" }],1807 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1808 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1809 schedNoFence::scheduler::mBuild: Set(),1810 schedNoFence::scheduler::mDone: Set(),1811 schedNoFence::scheduler::mExpect: Set(),1812 schedNoFence::scheduler::mResult: Set(),1813 schedNoFence::scheduler::mRetry: Set(),1814 schedNoFence::scheduler::mRevoke: Set(),1815 schedNoFence::scheduler::mSchedule: Set(),1816 schedNoFence::scheduler::published: 0,1817 schedNoFence::scheduler::publishedBy: Set(),1818 schedNoFence::scheduler::ws:1819 Map(1820 "w1" ->1821 {1822 attached: Set(),1823 built: false,1824 expecting: true,1825 running: true,1826 session: true,1827 up: true1828 },1829 "w2" ->1830 {1831 attached: Set(),1832 built: false,1833 expecting: false,1834 running: false,1835 session: true,1836 up: true1837 }1838 )1839}18401841[State 4]1842{1843 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1844 schedNoFence::scheduler::crashes: 1,1845 schedNoFence::scheduler::entry: [],1846 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1847 schedNoFence::scheduler::mAssigned: Set(),1848 schedNoFence::scheduler::mBuild: Set(),1849 schedNoFence::scheduler::mDone: Set(),1850 schedNoFence::scheduler::mExpect: Set(),1851 schedNoFence::scheduler::mResult: Set(),1852 schedNoFence::scheduler::mRetry: Set("c2"),1853 schedNoFence::scheduler::mRevoke: Set(),1854 schedNoFence::scheduler::mSchedule: Set(),1855 schedNoFence::scheduler::published: 0,1856 schedNoFence::scheduler::publishedBy: Set(),1857 schedNoFence::scheduler::ws:1858 Map(1859 "w1" ->1860 {1861 attached: Set(),1862 built: false,1863 expecting: true,1864 running: true,1865 session: false,1866 up: true1867 },1868 "w2" ->1869 {1870 attached: Set(),1871 built: false,1872 expecting: false,1873 running: false,1874 session: false,1875 up: true1876 }1877 )1878}18791880[State 5]1881{1882 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1883 schedNoFence::scheduler::crashes: 1,1884 schedNoFence::scheduler::entry: [],1885 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1886 schedNoFence::scheduler::mAssigned: Set(),1887 schedNoFence::scheduler::mBuild: Set(),1888 schedNoFence::scheduler::mDone: Set(),1889 schedNoFence::scheduler::mExpect: Set(),1890 schedNoFence::scheduler::mResult: Set(),1891 schedNoFence::scheduler::mRetry: Set("c2"),1892 schedNoFence::scheduler::mRevoke: Set(),1893 schedNoFence::scheduler::mSchedule: Set("c1"),1894 schedNoFence::scheduler::published: 0,1895 schedNoFence::scheduler::publishedBy: Set(),1896 schedNoFence::scheduler::ws:1897 Map(1898 "w1" ->1899 {1900 attached: Set(),1901 built: false,1902 expecting: true,1903 running: true,1904 session: false,1905 up: true1906 },1907 "w2" ->1908 {1909 attached: Set(),1910 built: false,1911 expecting: false,1912 running: false,1913 session: false,1914 up: true1915 }1916 )1917}19181919[State 6]1920{1921 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1922 schedNoFence::scheduler::crashes: 2,1923 schedNoFence::scheduler::entry: [],1924 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1925 schedNoFence::scheduler::mAssigned: Set(),1926 schedNoFence::scheduler::mBuild: Set(),1927 schedNoFence::scheduler::mDone: Set(),1928 schedNoFence::scheduler::mExpect: Set(),1929 schedNoFence::scheduler::mResult: Set(),1930 schedNoFence::scheduler::mRetry: Set("c2"),1931 schedNoFence::scheduler::mRevoke: Set(),1932 schedNoFence::scheduler::mSchedule: Set("c1"),1933 schedNoFence::scheduler::published: 0,1934 schedNoFence::scheduler::publishedBy: Set(),1935 schedNoFence::scheduler::ws:1936 Map(1937 "w1" ->1938 {1939 attached: Set(),1940 built: false,1941 expecting: true,1942 running: true,1943 session: false,1944 up: true1945 },1946 "w2" ->1947 {1948 attached: Set(),1949 built: false,1950 expecting: false,1951 running: false,1952 session: false,1953 up: false1954 }1955 )1956}19571958[State 7]1959{1960 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1961 schedNoFence::scheduler::crashes: 2,1962 schedNoFence::scheduler::entry: [],1963 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1964 schedNoFence::scheduler::mAssigned: Set(),1965 schedNoFence::scheduler::mBuild: Set(),1966 schedNoFence::scheduler::mDone: Set(),1967 schedNoFence::scheduler::mExpect: Set(),1968 schedNoFence::scheduler::mResult: Set(),1969 schedNoFence::scheduler::mRetry: Set("c2"),1970 schedNoFence::scheduler::mRevoke: Set(),1971 schedNoFence::scheduler::mSchedule: Set("c1"),1972 schedNoFence::scheduler::published: 0,1973 schedNoFence::scheduler::publishedBy: Set(),1974 schedNoFence::scheduler::ws:1975 Map(1976 "w1" ->1977 {1978 attached: Set(),1979 built: false,1980 expecting: true,1981 running: true,1982 session: false,1983 up: true1984 },1985 "w2" ->1986 {1987 attached: Set(),1988 built: false,1989 expecting: false,1990 running: false,1991 session: true,1992 up: true1993 }1994 )1995}19961997[State 8]1998{1999 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2000 schedNoFence::scheduler::crashes: 2,2001 schedNoFence::scheduler::entry:2002 [{ followers: Set("c1"), leased: true, worker: "w2" }],2003 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2004 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2005 schedNoFence::scheduler::mBuild: Set(),2006 schedNoFence::scheduler::mDone: Set(),2007 schedNoFence::scheduler::mExpect: Set("w2"),2008 schedNoFence::scheduler::mResult: Set(),2009 schedNoFence::scheduler::mRetry: Set("c2"),2010 schedNoFence::scheduler::mRevoke: Set(),2011 schedNoFence::scheduler::mSchedule: Set(),2012 schedNoFence::scheduler::published: 0,2013 schedNoFence::scheduler::publishedBy: Set(),2014 schedNoFence::scheduler::ws:2015 Map(2016 "w1" ->2017 {2018 attached: Set(),2019 built: false,2020 expecting: true,2021 running: true,2022 session: false,2023 up: true2024 },2025 "w2" ->2026 {2027 attached: Set(),2028 built: false,2029 expecting: false,2030 running: false,2031 session: true,2032 up: true2033 }2034 )2035}20362037[State 9]2038{2039 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2040 schedNoFence::scheduler::crashes: 2,2041 schedNoFence::scheduler::entry:2042 [{ followers: Set("c1"), leased: true, worker: "w2" }],2043 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2044 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2045 schedNoFence::scheduler::mBuild: Set(),2046 schedNoFence::scheduler::mDone: Set(),2047 schedNoFence::scheduler::mExpect: Set("w2"),2048 schedNoFence::scheduler::mResult: Set(),2049 schedNoFence::scheduler::mRetry: Set("c2"),2050 schedNoFence::scheduler::mRevoke: Set(),2051 schedNoFence::scheduler::mSchedule: Set(),2052 schedNoFence::scheduler::published: 1,2053 schedNoFence::scheduler::publishedBy: Set("w1"),2054 schedNoFence::scheduler::ws:2055 Map(2056 "w1" ->2057 {2058 attached: Set(),2059 built: true,2060 expecting: false,2061 running: false,2062 session: false,2063 up: true2064 },2065 "w2" ->2066 {2067 attached: Set(),2068 built: false,2069 expecting: false,2070 running: false,2071 session: true,2072 up: true2073 }2074 )2075}20762077[State 10]2078{2079 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2080 schedNoFence::scheduler::crashes: 2,2081 schedNoFence::scheduler::entry:2082 [{ followers: Set("c1"), leased: true, worker: "w2" }],2083 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2084 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2085 schedNoFence::scheduler::mBuild: Set(),2086 schedNoFence::scheduler::mDone: Set(),2087 schedNoFence::scheduler::mExpect: Set("w2"),2088 schedNoFence::scheduler::mResult: Set(),2089 schedNoFence::scheduler::mRetry: Set(),2090 schedNoFence::scheduler::mRevoke: Set(),2091 schedNoFence::scheduler::mSchedule: Set("c2"),2092 schedNoFence::scheduler::published: 1,2093 schedNoFence::scheduler::publishedBy: Set("w1"),2094 schedNoFence::scheduler::ws:2095 Map(2096 "w1" ->2097 {2098 attached: Set(),2099 built: true,2100 expecting: false,2101 running: false,2102 session: false,2103 up: true2104 },2105 "w2" ->2106 {2107 attached: Set(),2108 built: false,2109 expecting: false,2110 running: false,2111 session: true,2112 up: true2113 }2114 )2115}21162117[State 11]2118{2119 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2120 schedNoFence::scheduler::crashes: 2,2121 schedNoFence::scheduler::entry:2122 [{ followers: Set("c1"), leased: true, worker: "w2" }],2123 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2124 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2125 schedNoFence::scheduler::mBuild: Set(),2126 schedNoFence::scheduler::mDone: Set(),2127 schedNoFence::scheduler::mExpect: Set(),2128 schedNoFence::scheduler::mResult: Set(),2129 schedNoFence::scheduler::mRetry: Set(),2130 schedNoFence::scheduler::mRevoke: Set(),2131 schedNoFence::scheduler::mSchedule: Set("c2"),2132 schedNoFence::scheduler::published: 1,2133 schedNoFence::scheduler::publishedBy: Set("w1"),2134 schedNoFence::scheduler::ws:2135 Map(2136 "w1" ->2137 {2138 attached: Set(),2139 built: true,2140 expecting: false,2141 running: false,2142 session: false,2143 up: true2144 },2145 "w2" ->2146 {2147 attached: Set(),2148 built: false,2149 expecting: true,2150 running: true,2151 session: true,2152 up: true2153 }2154 )2155}21562157[State 12]2158{2159 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2160 schedNoFence::scheduler::crashes: 2,2161 schedNoFence::scheduler::entry:2162 [{ followers: Set("c1"), leased: true, worker: "w2" }],2163 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2164 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2165 schedNoFence::scheduler::mBuild: Set(),2166 schedNoFence::scheduler::mDone: Set(),2167 schedNoFence::scheduler::mExpect: Set(),2168 schedNoFence::scheduler::mResult: Set(),2169 schedNoFence::scheduler::mRetry: Set(),2170 schedNoFence::scheduler::mRevoke: Set(),2171 schedNoFence::scheduler::mSchedule: Set("c2"),2172 schedNoFence::scheduler::published: 1,2173 schedNoFence::scheduler::publishedBy: Set("w1"),2174 schedNoFence::scheduler::ws:2175 Map(2176 "w1" ->2177 {2178 attached: Set(),2179 built: true,2180 expecting: false,2181 running: false,2182 session: true,2183 up: true2184 },2185 "w2" ->2186 {2187 attached: Set(),2188 built: false,2189 expecting: true,2190 running: true,2191 session: true,2192 up: true2193 }2194 )2195}21962197[State 13]2198{2199 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2200 schedNoFence::scheduler::crashes: 2,2201 schedNoFence::scheduler::entry:2202 [{ followers: Set("c1"), leased: true, worker: "w2" }],2203 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2204 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2205 schedNoFence::scheduler::mBuild: Set(),2206 schedNoFence::scheduler::mDone: Set("w2"),2207 schedNoFence::scheduler::mExpect: Set(),2208 schedNoFence::scheduler::mResult: Set(),2209 schedNoFence::scheduler::mRetry: Set(),2210 schedNoFence::scheduler::mRevoke: Set(),2211 schedNoFence::scheduler::mSchedule: Set("c2"),2212 schedNoFence::scheduler::published: 2,2213 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2214 schedNoFence::scheduler::ws:2215 Map(2216 "w1" ->2217 {2218 attached: Set(),2219 built: true,2220 expecting: false,2221 running: false,2222 session: true,2223 up: true2224 },2225 "w2" ->2226 {2227 attached: Set(),2228 built: true,2229 expecting: false,2230 running: false,2231 session: true,2232 up: true2233 }2234 )2235}22362237[violation] Found an issue (514ms at 50909 traces/second).2238Use --verbosity=3 to show executions.2239Use --seed=0xd638daee1708ab79 --backend=rust to reproduce.2240error: Invariant violated2241An example execution:22422243[State 0]2244{2245 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "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(),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 1]2283{2284 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "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("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 2]2322{2323 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2324 schedNoPush::scheduler::crashes: 0,2325 schedNoPush::scheduler::entry:2326 [{ followers: Set("c2"), leased: true, worker: "w2" }],2327 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2328 schedNoPush::scheduler::mAssigned: Set(("c2", "w2")),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(),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 3]2362{2363 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2364 schedNoPush::scheduler::crashes: 1,2365 schedNoPush::scheduler::entry:2366 [{ followers: Set("c2"), leased: true, worker: "w2" }],2367 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2368 schedNoPush::scheduler::mAssigned: Set(("c2", "w2")),2369 schedNoPush::scheduler::mBuild: Set(),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(),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: false,2396 up: false2397 }2398 )2399}24002401[State 4]2402{2403 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2404 schedNoPush::scheduler::crashes: 1,2405 schedNoPush::scheduler::entry:2406 [{ followers: Set("c2"), leased: true, worker: "w2" }],2407 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2408 schedNoPush::scheduler::mAssigned: Set(),2409 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2410 schedNoPush::scheduler::mDone: Set(),2411 schedNoPush::scheduler::mExpect: Set(),2412 schedNoPush::scheduler::mResult: Set(),2413 schedNoPush::scheduler::mRetry: Set(),2414 schedNoPush::scheduler::mRevoke: Set(),2415 schedNoPush::scheduler::mSchedule: Set(),2416 schedNoPush::scheduler::published: 0,2417 schedNoPush::scheduler::publishedBy: Set(),2418 schedNoPush::scheduler::ws:2419 Map(2420 "w1" ->2421 {2422 attached: Set(),2423 built: false,2424 expecting: false,2425 running: false,2426 session: true,2427 up: true2428 },2429 "w2" ->2430 {2431 attached: Set(),2432 built: false,2433 expecting: false,2434 running: false,2435 session: false,2436 up: false2437 }2438 )2439}24402441[State 5]2442{2443 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2444 schedNoPush::scheduler::crashes: 2,2445 schedNoPush::scheduler::entry: [],2446 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2447 schedNoPush::scheduler::mAssigned: Set(),2448 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2449 schedNoPush::scheduler::mDone: Set(),2450 schedNoPush::scheduler::mExpect: Set(),2451 schedNoPush::scheduler::mResult: Set(),2452 schedNoPush::scheduler::mRetry: Set(),2453 schedNoPush::scheduler::mRevoke: Set(),2454 schedNoPush::scheduler::mSchedule: Set(),2455 schedNoPush::scheduler::published: 0,2456 schedNoPush::scheduler::publishedBy: Set(),2457 schedNoPush::scheduler::ws:2458 Map(2459 "w1" ->2460 {2461 attached: Set(),2462 built: false,2463 expecting: false,2464 running: false,2465 session: false,2466 up: true2467 },2468 "w2" ->2469 {2470 attached: Set(),2471 built: false,2472 expecting: false,2473 running: false,2474 session: false,2475 up: false2476 }2477 )2478}24792480[State 6]2481{2482 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2483 schedNoPush::scheduler::crashes: 2,2484 schedNoPush::scheduler::entry: [],2485 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2486 schedNoPush::scheduler::mAssigned: Set(),2487 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2488 schedNoPush::scheduler::mDone: Set(),2489 schedNoPush::scheduler::mExpect: Set(),2490 schedNoPush::scheduler::mResult: Set(),2491 schedNoPush::scheduler::mRetry: Set(),2492 schedNoPush::scheduler::mRevoke: Set(),2493 schedNoPush::scheduler::mSchedule: Set(),2494 schedNoPush::scheduler::published: 0,2495 schedNoPush::scheduler::publishedBy: Set(),2496 schedNoPush::scheduler::ws:2497 Map(2498 "w1" ->2499 {2500 attached: Set(),2501 built: false,2502 expecting: false,2503 running: false,2504 session: false,2505 up: true2506 },2507 "w2" ->2508 {2509 attached: Set(),2510 built: false,2511 expecting: false,2512 running: false,2513 session: true,2514 up: true2515 }2516 )2517}25182519[State 7]2520{2521 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2522 schedNoPush::scheduler::crashes: 2,2523 schedNoPush::scheduler::entry: [],2524 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2525 schedNoPush::scheduler::mAssigned: Set(),2526 schedNoPush::scheduler::mBuild: Set(),2527 schedNoPush::scheduler::mDone: Set(),2528 schedNoPush::scheduler::mExpect: Set(),2529 schedNoPush::scheduler::mResult: Set(),2530 schedNoPush::scheduler::mRetry: Set(),2531 schedNoPush::scheduler::mRevoke: Set(),2532 schedNoPush::scheduler::mSchedule: Set(),2533 schedNoPush::scheduler::published: 0,2534 schedNoPush::scheduler::publishedBy: Set(),2535 schedNoPush::scheduler::ws:2536 Map(2537 "w1" ->2538 {2539 attached: Set(),2540 built: false,2541 expecting: false,2542 running: false,2543 session: false,2544 up: true2545 },2546 "w2" ->2547 {2548 attached: Set("c2"),2549 built: false,2550 expecting: true,2551 running: true,2552 session: true,2553 up: true2554 }2555 )2556}25572558[violation] Found an issue (415ms at 32147 traces/second).2559Use --verbosity=3 to show executions.2560Use --seed=0x4507038d08c4d5b2 --backend=rust to reproduce.2561error: Invariant violated2562An example execution:25632564[State 0]2565{2566 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2567 schedNoReport::scheduler::crashes: 0,2568 schedNoReport::scheduler::entry: [],2569 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2570 schedNoReport::scheduler::mAssigned: Set(),2571 schedNoReport::scheduler::mBuild: Set(),2572 schedNoReport::scheduler::mDone: Set(),2573 schedNoReport::scheduler::mExpect: Set(),2574 schedNoReport::scheduler::mResult: Set(),2575 schedNoReport::scheduler::mRetry: Set(),2576 schedNoReport::scheduler::mRevoke: Set(),2577 schedNoReport::scheduler::mSchedule: Set(),2578 schedNoReport::scheduler::published: 0,2579 schedNoReport::scheduler::publishedBy: Set(),2580 schedNoReport::scheduler::ws:2581 Map(2582 "w1" ->2583 {2584 attached: Set(),2585 built: false,2586 expecting: false,2587 running: false,2588 session: true,2589 up: true2590 },2591 "w2" ->2592 {2593 attached: Set(),2594 built: false,2595 expecting: false,2596 running: false,2597 session: true,2598 up: true2599 }2600 )2601}26022603[State 1]2604{2605 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2606 schedNoReport::scheduler::crashes: 0,2607 schedNoReport::scheduler::entry: [],2608 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2609 schedNoReport::scheduler::mAssigned: Set(),2610 schedNoReport::scheduler::mBuild: Set(),2611 schedNoReport::scheduler::mDone: Set(),2612 schedNoReport::scheduler::mExpect: Set(),2613 schedNoReport::scheduler::mResult: Set(),2614 schedNoReport::scheduler::mRetry: Set(),2615 schedNoReport::scheduler::mRevoke: Set(),2616 schedNoReport::scheduler::mSchedule: Set("c2"),2617 schedNoReport::scheduler::published: 0,2618 schedNoReport::scheduler::publishedBy: Set(),2619 schedNoReport::scheduler::ws:2620 Map(2621 "w1" ->2622 {2623 attached: Set(),2624 built: false,2625 expecting: false,2626 running: false,2627 session: true,2628 up: true2629 },2630 "w2" ->2631 {2632 attached: Set(),2633 built: false,2634 expecting: false,2635 running: false,2636 session: true,2637 up: true2638 }2639 )2640}26412642[State 2]2643{2644 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2645 schedNoReport::scheduler::crashes: 0,2646 schedNoReport::scheduler::entry:2647 [{ followers: Set("c2"), leased: true, worker: "w1" }],2648 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2649 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2650 schedNoReport::scheduler::mBuild: Set(),2651 schedNoReport::scheduler::mDone: Set(),2652 schedNoReport::scheduler::mExpect: Set("w1"),2653 schedNoReport::scheduler::mResult: Set(),2654 schedNoReport::scheduler::mRetry: Set(),2655 schedNoReport::scheduler::mRevoke: Set(),2656 schedNoReport::scheduler::mSchedule: Set(),2657 schedNoReport::scheduler::published: 0,2658 schedNoReport::scheduler::publishedBy: Set(),2659 schedNoReport::scheduler::ws:2660 Map(2661 "w1" ->2662 {2663 attached: Set(),2664 built: false,2665 expecting: false,2666 running: false,2667 session: true,2668 up: true2669 },2670 "w2" ->2671 {2672 attached: Set(),2673 built: false,2674 expecting: false,2675 running: false,2676 session: true,2677 up: true2678 }2679 )2680}26812682[State 3]2683{2684 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2685 schedNoReport::scheduler::crashes: 0,2686 schedNoReport::scheduler::entry:2687 [{ followers: Set("c2"), leased: true, worker: "w1" }],2688 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2689 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2690 schedNoReport::scheduler::mBuild: Set(),2691 schedNoReport::scheduler::mDone: Set(),2692 schedNoReport::scheduler::mExpect: Set(),2693 schedNoReport::scheduler::mResult: Set(),2694 schedNoReport::scheduler::mRetry: Set(),2695 schedNoReport::scheduler::mRevoke: Set(),2696 schedNoReport::scheduler::mSchedule: Set(),2697 schedNoReport::scheduler::published: 0,2698 schedNoReport::scheduler::publishedBy: Set(),2699 schedNoReport::scheduler::ws:2700 Map(2701 "w1" ->2702 {2703 attached: Set(),2704 built: false,2705 expecting: true,2706 running: true,2707 session: true,2708 up: true2709 },2710 "w2" ->2711 {2712 attached: Set(),2713 built: false,2714 expecting: false,2715 running: false,2716 session: true,2717 up: true2718 }2719 )2720}27212722[State 4]2723{2724 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2725 schedNoReport::scheduler::crashes: 1,2726 schedNoReport::scheduler::entry: [],2727 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2728 schedNoReport::scheduler::mAssigned: Set(),2729 schedNoReport::scheduler::mBuild: Set(),2730 schedNoReport::scheduler::mDone: Set(),2731 schedNoReport::scheduler::mExpect: Set(),2732 schedNoReport::scheduler::mResult: Set(),2733 schedNoReport::scheduler::mRetry: Set("c2"),2734 schedNoReport::scheduler::mRevoke: Set(),2735 schedNoReport::scheduler::mSchedule: Set(),2736 schedNoReport::scheduler::published: 0,2737 schedNoReport::scheduler::publishedBy: Set(),2738 schedNoReport::scheduler::ws:2739 Map(2740 "w1" ->2741 {2742 attached: Set(),2743 built: false,2744 expecting: true,2745 running: true,2746 session: false,2747 up: true2748 },2749 "w2" ->2750 {2751 attached: Set(),2752 built: false,2753 expecting: false,2754 running: false,2755 session: false,2756 up: true2757 }2758 )2759}27602761[State 5]2762{2763 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2764 schedNoReport::scheduler::crashes: 2,2765 schedNoReport::scheduler::entry: [],2766 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2767 schedNoReport::scheduler::mAssigned: Set(),2768 schedNoReport::scheduler::mBuild: Set(),2769 schedNoReport::scheduler::mDone: Set(),2770 schedNoReport::scheduler::mExpect: Set(),2771 schedNoReport::scheduler::mResult: Set(),2772 schedNoReport::scheduler::mRetry: Set("c2"),2773 schedNoReport::scheduler::mRevoke: Set(),2774 schedNoReport::scheduler::mSchedule: Set(),2775 schedNoReport::scheduler::published: 0,2776 schedNoReport::scheduler::publishedBy: Set(),2777 schedNoReport::scheduler::ws:2778 Map(2779 "w1" ->2780 {2781 attached: Set(),2782 built: false,2783 expecting: true,2784 running: true,2785 session: false,2786 up: true2787 },2788 "w2" ->2789 {2790 attached: Set(),2791 built: false,2792 expecting: false,2793 running: false,2794 session: false,2795 up: true2796 }2797 )2798}27992800[State 6]2801{2802 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2803 schedNoReport::scheduler::crashes: 2,2804 schedNoReport::scheduler::entry: [],2805 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2806 schedNoReport::scheduler::mAssigned: Set(),2807 schedNoReport::scheduler::mBuild: Set(),2808 schedNoReport::scheduler::mDone: Set(),2809 schedNoReport::scheduler::mExpect: Set(),2810 schedNoReport::scheduler::mResult: Set(),2811 schedNoReport::scheduler::mRetry: Set("c2"),2812 schedNoReport::scheduler::mRevoke: Set(),2813 schedNoReport::scheduler::mSchedule: Set("c1"),2814 schedNoReport::scheduler::published: 0,2815 schedNoReport::scheduler::publishedBy: Set(),2816 schedNoReport::scheduler::ws:2817 Map(2818 "w1" ->2819 {2820 attached: Set(),2821 built: false,2822 expecting: true,2823 running: true,2824 session: false,2825 up: true2826 },2827 "w2" ->2828 {2829 attached: Set(),2830 built: false,2831 expecting: false,2832 running: false,2833 session: false,2834 up: true2835 }2836 )2837}28382839[State 7]2840{2841 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2842 schedNoReport::scheduler::crashes: 2,2843 schedNoReport::scheduler::entry: [],2844 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2845 schedNoReport::scheduler::mAssigned: Set(),2846 schedNoReport::scheduler::mBuild: Set(),2847 schedNoReport::scheduler::mDone: Set(),2848 schedNoReport::scheduler::mExpect: Set(),2849 schedNoReport::scheduler::mResult: Set(),2850 schedNoReport::scheduler::mRetry: Set(),2851 schedNoReport::scheduler::mRevoke: Set(),2852 schedNoReport::scheduler::mSchedule: Set("c1", "c2"),2853 schedNoReport::scheduler::published: 0,2854 schedNoReport::scheduler::publishedBy: Set(),2855 schedNoReport::scheduler::ws:2856 Map(2857 "w1" ->2858 {2859 attached: Set(),2860 built: false,2861 expecting: true,2862 running: true,2863 session: false,2864 up: true2865 },2866 "w2" ->2867 {2868 attached: Set(),2869 built: false,2870 expecting: false,2871 running: false,2872 session: false,2873 up: true2874 }2875 )2876}28772878[State 8]2879{2880 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2881 schedNoReport::scheduler::crashes: 2,2882 schedNoReport::scheduler::entry: [],2883 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2884 schedNoReport::scheduler::mAssigned: Set(),2885 schedNoReport::scheduler::mBuild: Set(),2886 schedNoReport::scheduler::mDone: Set(),2887 schedNoReport::scheduler::mExpect: Set(),2888 schedNoReport::scheduler::mResult: Set(),2889 schedNoReport::scheduler::mRetry: Set(),2890 schedNoReport::scheduler::mRevoke: Set(),2891 schedNoReport::scheduler::mSchedule: Set("c1", "c2"),2892 schedNoReport::scheduler::published: 0,2893 schedNoReport::scheduler::publishedBy: Set(),2894 schedNoReport::scheduler::ws:2895 Map(2896 "w1" ->2897 {2898 attached: Set(),2899 built: false,2900 expecting: true,2901 running: true,2902 session: false,2903 up: true2904 },2905 "w2" ->2906 {2907 attached: Set(),2908 built: false,2909 expecting: false,2910 running: false,2911 session: true,2912 up: true2913 }2914 )2915}29162917[State 9]2918{2919 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2920 schedNoReport::scheduler::crashes: 2,2921 schedNoReport::scheduler::entry:2922 [{ followers: Set("c2"), leased: true, worker: "w2" }],2923 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2924 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2925 schedNoReport::scheduler::mBuild: Set(),2926 schedNoReport::scheduler::mDone: Set(),2927 schedNoReport::scheduler::mExpect: Set("w2"),2928 schedNoReport::scheduler::mResult: Set(),2929 schedNoReport::scheduler::mRetry: Set(),2930 schedNoReport::scheduler::mRevoke: Set(),2931 schedNoReport::scheduler::mSchedule: Set("c1"),2932 schedNoReport::scheduler::published: 0,2933 schedNoReport::scheduler::publishedBy: Set(),2934 schedNoReport::scheduler::ws:2935 Map(2936 "w1" ->2937 {2938 attached: Set(),2939 built: false,2940 expecting: true,2941 running: true,2942 session: false,2943 up: true2944 },2945 "w2" ->2946 {2947 attached: Set(),2948 built: false,2949 expecting: false,2950 running: false,2951 session: true,2952 up: true2953 }2954 )2955}29562957[State 10]2958{2959 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2960 schedNoReport::scheduler::crashes: 2,2961 schedNoReport::scheduler::entry:2962 [{ followers: Set("c2"), leased: true, worker: "w2" }],2963 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2964 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2965 schedNoReport::scheduler::mBuild: Set(),2966 schedNoReport::scheduler::mDone: Set(),2967 schedNoReport::scheduler::mExpect: Set(),2968 schedNoReport::scheduler::mResult: Set(),2969 schedNoReport::scheduler::mRetry: Set(),2970 schedNoReport::scheduler::mRevoke: Set(),2971 schedNoReport::scheduler::mSchedule: Set("c1"),2972 schedNoReport::scheduler::published: 0,2973 schedNoReport::scheduler::publishedBy: Set(),2974 schedNoReport::scheduler::ws:2975 Map(2976 "w1" ->2977 {2978 attached: Set(),2979 built: false,2980 expecting: true,2981 running: true,2982 session: false,2983 up: true2984 },2985 "w2" ->2986 {2987 attached: Set(),2988 built: false,2989 expecting: true,2990 running: true,2991 session: true,2992 up: true2993 }2994 )2995}29962997[State 11]2998{2999 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),3000 schedNoReport::scheduler::crashes: 2,3001 schedNoReport::scheduler::entry:3002 [{ followers: Set("c2"), leased: true, worker: "w2" }],3003 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),3004 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),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"),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: true,3030 running: true,3031 session: true,3032 up: true3033 }3034 )3035}30363037[violation] Found an issue (429ms at 53436 traces/second).3038Use --verbosity=3 to show executions.3039Use --seed=0xd7a60c4b8ef2b696 --backend=rust to reproduce.3040error: Invariant violated3041An example execution:30423043[State 0]3044{3045 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3046 schedTerminal::scheduler::crashes: 0,3047 schedTerminal::scheduler::entry: [],3048 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3049 schedTerminal::scheduler::mAssigned: Set(),3050 schedTerminal::scheduler::mBuild: Set(),3051 schedTerminal::scheduler::mDone: Set(),3052 schedTerminal::scheduler::mExpect: Set(),3053 schedTerminal::scheduler::mResult: Set(),3054 schedTerminal::scheduler::mRetry: Set(),3055 schedTerminal::scheduler::mRevoke: Set(),3056 schedTerminal::scheduler::mSchedule: Set(),3057 schedTerminal::scheduler::published: 0,3058 schedTerminal::scheduler::publishedBy: Set(),3059 schedTerminal::scheduler::ws:3060 Map(3061 "w1" ->3062 {3063 attached: Set(),3064 built: false,3065 expecting: false,3066 running: false,3067 session: true,3068 up: true3069 },3070 "w2" ->3071 {3072 attached: Set(),3073 built: false,3074 expecting: false,3075 running: false,3076 session: true,3077 up: true3078 }3079 )3080}30813082[State 1]3083{3084 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3085 schedTerminal::scheduler::crashes: 1,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: false,3107 up: true3108 },3109 "w2" ->3110 {3111 attached: Set(),3112 built: false,3113 expecting: false,3114 running: false,3115 session: false,3116 up: true3117 }3118 )3119}31203121[State 2]3122{3123 schedTerminal::scheduler::cl: Map("c1" -> CQueued, "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("c1"),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 3]3161{3162 schedTerminal::scheduler::cl: Map("c1" -> CFailed, "c2" -> CIdle),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(),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[violation] Found an issue (143ms at 6853 traces/second).3200Use --verbosity=3 to show executions.3201Use --seed=0x667c2a27241297e1 --backend=rust to reproduce.3202error: Invariant violated3203An example execution:32043205[State 0]3206{3207 pushFixed::push::byPath: Map(),3208 pushFixed::push::inflight: Set(),3209 pushFixed::push::left: Map(),3210 pushFixed::push::sent: Map()3211}32123213[State 1]3214{3215 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3216 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3217 pushFixed::push::left: Map(1 -> 2),3218 pushFixed::push::sent: Map(1 -> Set("a", "b"))3219}32203221[State 2]3222{3223 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3224 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),3225 pushFixed::push::left: Map(1 -> 2, 2 -> 2),3226 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3227}32283229[State 3]3230{3231 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3232 pushFixed::push::inflight:3233 Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),3234 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 2),3235 pushFixed::push::sent:3236 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3237}32383239[State 4]3240{3241 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3242 pushFixed::push::inflight:3243 Set((1, "a"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),3244 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 2),3245 pushFixed::push::sent:3246 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3247}32483249[State 5]3250{3251 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3252 pushFixed::push::inflight: Set((1, "a"), (2, "b"), (3, "a"), (3, "b")),3253 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 2),3254 pushFixed::push::sent:3255 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3256}32573258[State 6]3259{3260 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3261 pushFixed::push::inflight: Set((1, "a"), (2, "b"), (3, "a")),3262 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 1),3263 pushFixed::push::sent:3264 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3265}32663267[State 7]3268{3269 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3270 pushFixed::push::inflight: Set((1, "a"), (2, "b")),3271 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 0),3272 pushFixed::push::sent:3273 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3274}32753276[State 8]3277{3278 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3279 pushFixed::push::inflight: Set((1, "a")),3280 pushFixed::push::left: Map(1 -> 1, 2 -> 0, 3 -> 0),3281 pushFixed::push::sent:3282 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3283}32843285[State 9]3286{3287 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3288 pushFixed::push::inflight: Set(),3289 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3290 pushFixed::push::sent:3291 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3292}32933294[ok] No violation found (81ms at 246914 traces/second).3295Trace length statistics: max=10, min=7, average=7.933296You may increase --max-samples and --max-steps.3297Use --verbosity to produce more (or less) output.3298Use --seed=0xd73d44346fc040fa --backend=rust to reproduce.