nix-grpc-store-spec
checks.x86_64-linux.spec
· build #847
· raw
1tribuchet: building on jamie2An 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" -> CQueued),46 schedFixed::scheduler::crashes: 0,47 schedFixed::scheduler::entry: [],48 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),49 schedFixed::scheduler::mAssigned: Set(),50 schedFixed::scheduler::mBuild: Set(),51 schedFixed::scheduler::mDone: Set(),52 schedFixed::scheduler::mExpect: Set(),53 schedFixed::scheduler::mResult: Set(),54 schedFixed::scheduler::mRetry: Set(),55 schedFixed::scheduler::mRevoke: Set(),56 schedFixed::scheduler::mSchedule: Set("c2"),57 schedFixed::scheduler::published: 0,58 schedFixed::scheduler::publishedBy: Set(),59 schedFixed::scheduler::ws:60 Map(61 "w1" ->62 {63 attached: Set(),64 built: false,65 expecting: false,66 running: false,67 session: true,68 up: true69 },70 "w2" ->71 {72 attached: Set(),73 built: false,74 expecting: false,75 running: false,76 session: true,77 up: true78 }79 )80}8182[State 2]83{84 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),85 schedFixed::scheduler::crashes: 0,86 schedFixed::scheduler::entry:87 [{ followers: Set("c2"), leased: true, worker: "w1" }],88 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),89 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),90 schedFixed::scheduler::mBuild: Set(),91 schedFixed::scheduler::mDone: Set(),92 schedFixed::scheduler::mExpect: Set("w1"),93 schedFixed::scheduler::mResult: Set(),94 schedFixed::scheduler::mRetry: Set(),95 schedFixed::scheduler::mRevoke: Set(),96 schedFixed::scheduler::mSchedule: Set(),97 schedFixed::scheduler::published: 0,98 schedFixed::scheduler::publishedBy: Set(),99 schedFixed::scheduler::ws:100 Map(101 "w1" ->102 {103 attached: Set(),104 built: false,105 expecting: false,106 running: false,107 session: true,108 up: true109 },110 "w2" ->111 {112 attached: Set(),113 built: false,114 expecting: false,115 running: false,116 session: true,117 up: true118 }119 )120}121122[State 3]123{124 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),125 schedFixed::scheduler::crashes: 1,126 schedFixed::scheduler::entry:127 [{ followers: Set("c2"), leased: true, worker: "w1" }],128 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),129 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),130 schedFixed::scheduler::mBuild: Set(),131 schedFixed::scheduler::mDone: Set(),132 schedFixed::scheduler::mExpect: Set("w1"),133 schedFixed::scheduler::mResult: Set(),134 schedFixed::scheduler::mRetry: Set(),135 schedFixed::scheduler::mRevoke: Set(),136 schedFixed::scheduler::mSchedule: Set(),137 schedFixed::scheduler::published: 0,138 schedFixed::scheduler::publishedBy: Set(),139 schedFixed::scheduler::ws:140 Map(141 "w1" ->142 {143 attached: Set(),144 built: false,145 expecting: false,146 running: false,147 session: true,148 up: true149 },150 "w2" ->151 {152 attached: Set(),153 built: false,154 expecting: false,155 running: false,156 session: false,157 up: false158 }159 )160}161162[State 4]163{164 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),165 schedFixed::scheduler::crashes: 1,166 schedFixed::scheduler::entry:167 [{ followers: Set("c2"), leased: true, worker: "w1" }],168 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),169 schedFixed::scheduler::mAssigned: Set(),170 schedFixed::scheduler::mBuild: Set(("c2", "w1")),171 schedFixed::scheduler::mDone: Set(),172 schedFixed::scheduler::mExpect: Set("w1"),173 schedFixed::scheduler::mResult: Set(),174 schedFixed::scheduler::mRetry: Set(),175 schedFixed::scheduler::mRevoke: Set(),176 schedFixed::scheduler::mSchedule: Set(),177 schedFixed::scheduler::published: 0,178 schedFixed::scheduler::publishedBy: Set(),179 schedFixed::scheduler::ws:180 Map(181 "w1" ->182 {183 attached: Set(),184 built: false,185 expecting: false,186 running: false,187 session: true,188 up: true189 },190 "w2" ->191 {192 attached: Set(),193 built: false,194 expecting: false,195 running: false,196 session: false,197 up: false198 }199 )200}201202[State 5]203{204 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),205 schedFixed::scheduler::crashes: 2,206 schedFixed::scheduler::entry:207 [{ followers: Set("c2"), leased: true, worker: "w1" }],208 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),209 schedFixed::scheduler::mAssigned: Set(),210 schedFixed::scheduler::mBuild: Set(("c2", "w1")),211 schedFixed::scheduler::mDone: Set(),212 schedFixed::scheduler::mExpect: Set(),213 schedFixed::scheduler::mResult: Set(),214 schedFixed::scheduler::mRetry: Set(),215 schedFixed::scheduler::mRevoke: Set(),216 schedFixed::scheduler::mSchedule: Set(),217 schedFixed::scheduler::published: 0,218 schedFixed::scheduler::publishedBy: Set(),219 schedFixed::scheduler::ws:220 Map(221 "w1" ->222 {223 attached: Set(),224 built: false,225 expecting: false,226 running: false,227 session: false,228 up: false229 },230 "w2" ->231 {232 attached: Set(),233 built: false,234 expecting: false,235 running: false,236 session: false,237 up: false238 }239 )240}241242[State 6]243{244 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),245 schedFixed::scheduler::crashes: 2,246 schedFixed::scheduler::entry: [],247 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),248 schedFixed::scheduler::mAssigned: Set(),249 schedFixed::scheduler::mBuild: Set(("c2", "w1")),250 schedFixed::scheduler::mDone: Set(),251 schedFixed::scheduler::mExpect: Set(),252 schedFixed::scheduler::mResult: Set(),253 schedFixed::scheduler::mRetry: Set("c2"),254 schedFixed::scheduler::mRevoke: Set(),255 schedFixed::scheduler::mSchedule: Set(),256 schedFixed::scheduler::published: 0,257 schedFixed::scheduler::publishedBy: Set(),258 schedFixed::scheduler::ws:259 Map(260 "w1" ->261 {262 attached: Set(),263 built: false,264 expecting: false,265 running: false,266 session: false,267 up: false268 },269 "w2" ->270 {271 attached: Set(),272 built: false,273 expecting: false,274 running: false,275 session: false,276 up: false277 }278 )279}280281[State 7]282{283 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),284 schedFixed::scheduler::crashes: 2,285 schedFixed::scheduler::entry: [],286 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),287 schedFixed::scheduler::mAssigned: Set(),288 schedFixed::scheduler::mBuild: Set(("c2", "w1")),289 schedFixed::scheduler::mDone: Set(),290 schedFixed::scheduler::mExpect: Set(),291 schedFixed::scheduler::mResult: Set(),292 schedFixed::scheduler::mRetry: Set("c2"),293 schedFixed::scheduler::mRevoke: Set(),294 schedFixed::scheduler::mSchedule: Set(),295 schedFixed::scheduler::published: 0,296 schedFixed::scheduler::publishedBy: Set(),297 schedFixed::scheduler::ws:298 Map(299 "w1" ->300 {301 attached: Set(),302 built: false,303 expecting: false,304 running: false,305 session: true,306 up: true307 },308 "w2" ->309 {310 attached: Set(),311 built: false,312 expecting: false,313 running: false,314 session: false,315 up: false316 }317 )318}319320[State 8]321{322 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),323 schedFixed::scheduler::crashes: 2,324 schedFixed::scheduler::entry: [],325 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),326 schedFixed::scheduler::mAssigned: Set(),327 schedFixed::scheduler::mBuild: Set(("c2", "w1")),328 schedFixed::scheduler::mDone: Set(),329 schedFixed::scheduler::mExpect: Set(),330 schedFixed::scheduler::mResult: Set(),331 schedFixed::scheduler::mRetry: Set("c2"),332 schedFixed::scheduler::mRevoke: Set(),333 schedFixed::scheduler::mSchedule: Set("c1"),334 schedFixed::scheduler::published: 0,335 schedFixed::scheduler::publishedBy: Set(),336 schedFixed::scheduler::ws:337 Map(338 "w1" ->339 {340 attached: Set(),341 built: false,342 expecting: false,343 running: false,344 session: true,345 up: true346 },347 "w2" ->348 {349 attached: Set(),350 built: false,351 expecting: false,352 running: false,353 session: false,354 up: false355 }356 )357}358359[State 9]360{361 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),362 schedFixed::scheduler::crashes: 2,363 schedFixed::scheduler::entry: [],364 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),365 schedFixed::scheduler::mAssigned: Set(),366 schedFixed::scheduler::mBuild: Set(("c2", "w1")),367 schedFixed::scheduler::mDone: Set(),368 schedFixed::scheduler::mExpect: Set(),369 schedFixed::scheduler::mResult: Set(),370 schedFixed::scheduler::mRetry: Set("c2"),371 schedFixed::scheduler::mRevoke: Set(),372 schedFixed::scheduler::mSchedule: Set("c1"),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" -> CSent("w1")),401 schedFixed::scheduler::crashes: 2,402 schedFixed::scheduler::entry:403 [{ followers: Set("c1"), leased: true, worker: "w1" }],404 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),405 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),406 schedFixed::scheduler::mBuild: Set(("c2", "w1")),407 schedFixed::scheduler::mDone: Set(),408 schedFixed::scheduler::mExpect: Set("w1"),409 schedFixed::scheduler::mResult: Set(),410 schedFixed::scheduler::mRetry: Set("c2"),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"), leased: true, worker: "w1" }],444 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),445 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),446 schedFixed::scheduler::mBuild: Set(("c2", "w1")),447 schedFixed::scheduler::mDone: Set(),448 schedFixed::scheduler::mExpect: Set("w1"),449 schedFixed::scheduler::mResult: Set(),450 schedFixed::scheduler::mRetry: Set(),451 schedFixed::scheduler::mRevoke: Set(),452 schedFixed::scheduler::mSchedule: Set("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" -> CSent("w1"), "c2" -> CQueued),481 schedFixed::scheduler::crashes: 2,482 schedFixed::scheduler::entry:483 [{ followers: Set("c1"), leased: true, worker: "w1" }],484 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),485 schedFixed::scheduler::mAssigned: Set(),486 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),487 schedFixed::scheduler::mDone: Set(),488 schedFixed::scheduler::mExpect: Set("w1"),489 schedFixed::scheduler::mResult: Set(),490 schedFixed::scheduler::mRetry: Set(),491 schedFixed::scheduler::mRevoke: Set(),492 schedFixed::scheduler::mSchedule: Set("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("w1"), "c2" -> CQueued),521 schedFixed::scheduler::crashes: 2,522 schedFixed::scheduler::entry:523 [{ followers: Set("c1"), leased: true, worker: "w1" }],524 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),525 schedFixed::scheduler::mAssigned: Set(),526 schedFixed::scheduler::mBuild: Set(("c2", "w1")),527 schedFixed::scheduler::mDone: Set(),528 schedFixed::scheduler::mExpect: Set("w1"),529 schedFixed::scheduler::mResult: Set(),530 schedFixed::scheduler::mRetry: Set("c1"),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("w1"), "c2" -> CQueued),561 schedFixed::scheduler::crashes: 2,562 schedFixed::scheduler::entry:563 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],564 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),565 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),566 schedFixed::scheduler::mBuild: Set(("c2", "w1")),567 schedFixed::scheduler::mDone: Set(),568 schedFixed::scheduler::mExpect: Set("w1"),569 schedFixed::scheduler::mResult: Set(),570 schedFixed::scheduler::mRetry: Set("c1"),571 schedFixed::scheduler::mRevoke: Set(),572 schedFixed::scheduler::mSchedule: Set(),573 schedFixed::scheduler::published: 0,574 schedFixed::scheduler::publishedBy: Set(),575 schedFixed::scheduler::ws:576 Map(577 "w1" ->578 {579 attached: Set(),580 built: false,581 expecting: false,582 running: false,583 session: true,584 up: true585 },586 "w2" ->587 {588 attached: Set(),589 built: false,590 expecting: false,591 running: false,592 session: true,593 up: true594 }595 )596}597598[State 15]599{600 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),601 schedFixed::scheduler::crashes: 2,602 schedFixed::scheduler::entry:603 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],604 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),605 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),606 schedFixed::scheduler::mBuild: Set(),607 schedFixed::scheduler::mDone: Set(),608 schedFixed::scheduler::mExpect: Set("w1"),609 schedFixed::scheduler::mResult: Set(),610 schedFixed::scheduler::mRetry: Set("c1", "c2"),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" -> CQueued, "c2" -> CQueued),641 schedFixed::scheduler::crashes: 2,642 schedFixed::scheduler::entry:643 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],644 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),645 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),646 schedFixed::scheduler::mBuild: Set(),647 schedFixed::scheduler::mDone: Set(),648 schedFixed::scheduler::mExpect: Set("w1"),649 schedFixed::scheduler::mResult: Set(),650 schedFixed::scheduler::mRetry: Set("c2"),651 schedFixed::scheduler::mRevoke: Set(),652 schedFixed::scheduler::mSchedule: Set("c1"),653 schedFixed::scheduler::published: 0,654 schedFixed::scheduler::publishedBy: Set(),655 schedFixed::scheduler::ws:656 Map(657 "w1" ->658 {659 attached: Set(),660 built: false,661 expecting: false,662 running: false,663 session: true,664 up: true665 },666 "w2" ->667 {668 attached: Set(),669 built: false,670 expecting: false,671 running: false,672 session: true,673 up: true674 }675 )676}677678[State 17]679{680 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),681 schedFixed::scheduler::crashes: 2,682 schedFixed::scheduler::entry:683 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],684 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),685 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),686 schedFixed::scheduler::mBuild: Set(),687 schedFixed::scheduler::mDone: Set(),688 schedFixed::scheduler::mExpect: Set("w1"),689 schedFixed::scheduler::mResult: Set(),690 schedFixed::scheduler::mRetry: Set("c2"),691 schedFixed::scheduler::mRevoke: Set(),692 schedFixed::scheduler::mSchedule: Set(),693 schedFixed::scheduler::published: 0,694 schedFixed::scheduler::publishedBy: Set(),695 schedFixed::scheduler::ws:696 Map(697 "w1" ->698 {699 attached: Set(),700 built: false,701 expecting: false,702 running: false,703 session: true,704 up: true705 },706 "w2" ->707 {708 attached: Set(),709 built: false,710 expecting: false,711 running: false,712 session: true,713 up: true714 }715 )716}717718[State 18]719{720 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),721 schedFixed::scheduler::crashes: 2,722 schedFixed::scheduler::entry:723 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],724 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),725 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),726 schedFixed::scheduler::mBuild: Set(("c2", "w1")),727 schedFixed::scheduler::mDone: Set(),728 schedFixed::scheduler::mExpect: Set("w1"),729 schedFixed::scheduler::mResult: Set(),730 schedFixed::scheduler::mRetry: Set("c2"),731 schedFixed::scheduler::mRevoke: Set(),732 schedFixed::scheduler::mSchedule: Set(),733 schedFixed::scheduler::published: 0,734 schedFixed::scheduler::publishedBy: Set(),735 schedFixed::scheduler::ws:736 Map(737 "w1" ->738 {739 attached: Set(),740 built: false,741 expecting: false,742 running: false,743 session: true,744 up: true745 },746 "w2" ->747 {748 attached: Set(),749 built: false,750 expecting: false,751 running: false,752 session: true,753 up: true754 }755 )756}757758[State 19]759{760 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),761 schedFixed::scheduler::crashes: 2,762 schedFixed::scheduler::entry:763 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],764 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),765 schedFixed::scheduler::mAssigned: Set(),766 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),767 schedFixed::scheduler::mDone: Set(),768 schedFixed::scheduler::mExpect: Set("w1"),769 schedFixed::scheduler::mResult: Set(),770 schedFixed::scheduler::mRetry: Set("c2"),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("w1"), "c2" -> CQueued),801 schedFixed::scheduler::crashes: 2,802 schedFixed::scheduler::entry:803 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],804 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),805 schedFixed::scheduler::mAssigned: Set(),806 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),807 schedFixed::scheduler::mDone: Set(),808 schedFixed::scheduler::mExpect: Set("w1"),809 schedFixed::scheduler::mResult: Set(),810 schedFixed::scheduler::mRetry: Set(),811 schedFixed::scheduler::mRevoke: Set(),812 schedFixed::scheduler::mSchedule: Set("c2"),813 schedFixed::scheduler::published: 0,814 schedFixed::scheduler::publishedBy: Set(),815 schedFixed::scheduler::ws:816 Map(817 "w1" ->818 {819 attached: Set(),820 built: false,821 expecting: false,822 running: false,823 session: true,824 up: true825 },826 "w2" ->827 {828 attached: Set(),829 built: false,830 expecting: false,831 running: false,832 session: true,833 up: true834 }835 )836}837838[State 21]839{840 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),841 schedFixed::scheduler::crashes: 2,842 schedFixed::scheduler::entry:843 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],844 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),845 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),846 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),847 schedFixed::scheduler::mDone: Set(),848 schedFixed::scheduler::mExpect: Set("w1"),849 schedFixed::scheduler::mResult: Set(),850 schedFixed::scheduler::mRetry: Set(),851 schedFixed::scheduler::mRevoke: Set(),852 schedFixed::scheduler::mSchedule: Set(),853 schedFixed::scheduler::published: 0,854 schedFixed::scheduler::publishedBy: Set(),855 schedFixed::scheduler::ws:856 Map(857 "w1" ->858 {859 attached: Set(),860 built: false,861 expecting: false,862 running: false,863 session: true,864 up: true865 },866 "w2" ->867 {868 attached: Set(),869 built: false,870 expecting: false,871 running: false,872 session: true,873 up: true874 }875 )876}877878[State 22]879{880 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),881 schedFixed::scheduler::crashes: 2,882 schedFixed::scheduler::entry:883 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],884 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),885 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),886 schedFixed::scheduler::mBuild: Set(("c2", "w1")),887 schedFixed::scheduler::mDone: Set(),888 schedFixed::scheduler::mExpect: Set("w1"),889 schedFixed::scheduler::mResult: Set(),890 schedFixed::scheduler::mRetry: Set("c1"),891 schedFixed::scheduler::mRevoke: Set(),892 schedFixed::scheduler::mSchedule: Set(),893 schedFixed::scheduler::published: 0,894 schedFixed::scheduler::publishedBy: Set(),895 schedFixed::scheduler::ws:896 Map(897 "w1" ->898 {899 attached: Set(),900 built: false,901 expecting: false,902 running: false,903 session: true,904 up: true905 },906 "w2" ->907 {908 attached: Set(),909 built: false,910 expecting: false,911 running: false,912 session: true,913 up: true914 }915 )916}917918[State 23]919{920 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),921 schedFixed::scheduler::crashes: 2,922 schedFixed::scheduler::entry:923 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],924 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),925 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),926 schedFixed::scheduler::mBuild: Set(("c2", "w1")),927 schedFixed::scheduler::mDone: Set(),928 schedFixed::scheduler::mExpect: Set("w1"),929 schedFixed::scheduler::mResult: Set(),930 schedFixed::scheduler::mRetry: Set(),931 schedFixed::scheduler::mRevoke: Set(),932 schedFixed::scheduler::mSchedule: Set("c1"),933 schedFixed::scheduler::published: 0,934 schedFixed::scheduler::publishedBy: Set(),935 schedFixed::scheduler::ws:936 Map(937 "w1" ->938 {939 attached: Set(),940 built: false,941 expecting: false,942 running: false,943 session: true,944 up: true945 },946 "w2" ->947 {948 attached: Set(),949 built: false,950 expecting: false,951 running: false,952 session: true,953 up: true954 }955 )956}957958[State 24]959{960 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),961 schedFixed::scheduler::crashes: 2,962 schedFixed::scheduler::entry:963 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],964 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),965 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),966 schedFixed::scheduler::mBuild: Set(("c2", "w1")),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: true,982 running: true,983 session: true,984 up: true985 },986 "w2" ->987 {988 attached: Set(),989 built: false,990 expecting: false,991 running: false,992 session: true,993 up: true994 }995 )996}997998[State 25]999{1000 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1001 schedFixed::scheduler::crashes: 2,1002 schedFixed::scheduler::entry:1003 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1004 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1005 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),1006 schedFixed::scheduler::mBuild: Set(("c2", "w1")),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: true,1022 running: true,1023 session: true,1024 up: true1025 },1026 "w2" ->1027 {1028 attached: Set(),1029 built: false,1030 expecting: false,1031 running: false,1032 session: true,1033 up: true1034 }1035 )1036}10371038[State 26]1039{1040 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),1041 schedFixed::scheduler::crashes: 2,1042 schedFixed::scheduler::entry:1043 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1044 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1045 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1046 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),1047 schedFixed::scheduler::mDone: Set(),1048 schedFixed::scheduler::mExpect: Set(),1049 schedFixed::scheduler::mResult: Set(),1050 schedFixed::scheduler::mRetry: Set(),1051 schedFixed::scheduler::mRevoke: Set(),1052 schedFixed::scheduler::mSchedule: Set(),1053 schedFixed::scheduler::published: 0,1054 schedFixed::scheduler::publishedBy: Set(),1055 schedFixed::scheduler::ws:1056 Map(1057 "w1" ->1058 {1059 attached: Set(),1060 built: false,1061 expecting: true,1062 running: true,1063 session: true,1064 up: true1065 },1066 "w2" ->1067 {1068 attached: Set(),1069 built: false,1070 expecting: false,1071 running: false,1072 session: true,1073 up: true1074 }1075 )1076}10771078[State 27]1079{1080 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1081 schedFixed::scheduler::crashes: 2,1082 schedFixed::scheduler::entry:1083 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1084 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1085 schedFixed::scheduler::mAssigned: Set(),1086 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),1087 schedFixed::scheduler::mDone: Set(),1088 schedFixed::scheduler::mExpect: Set(),1089 schedFixed::scheduler::mResult: Set(),1090 schedFixed::scheduler::mRetry: Set(),1091 schedFixed::scheduler::mRevoke: Set(),1092 schedFixed::scheduler::mSchedule: Set(),1093 schedFixed::scheduler::published: 0,1094 schedFixed::scheduler::publishedBy: Set(),1095 schedFixed::scheduler::ws:1096 Map(1097 "w1" ->1098 {1099 attached: Set(),1100 built: false,1101 expecting: true,1102 running: true,1103 session: true,1104 up: true1105 },1106 "w2" ->1107 {1108 attached: Set(),1109 built: false,1110 expecting: false,1111 running: false,1112 session: true,1113 up: true1114 }1115 )1116}11171118[State 28]1119{1120 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1121 schedFixed::scheduler::crashes: 2,1122 schedFixed::scheduler::entry:1123 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1124 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1125 schedFixed::scheduler::mAssigned: Set(),1126 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),1127 schedFixed::scheduler::mDone: Set("w1"),1128 schedFixed::scheduler::mExpect: Set(),1129 schedFixed::scheduler::mResult: Set(),1130 schedFixed::scheduler::mRetry: Set(),1131 schedFixed::scheduler::mRevoke: Set(),1132 schedFixed::scheduler::mSchedule: Set(),1133 schedFixed::scheduler::published: 1,1134 schedFixed::scheduler::publishedBy: Set("w1"),1135 schedFixed::scheduler::ws:1136 Map(1137 "w1" ->1138 {1139 attached: Set(),1140 built: true,1141 expecting: false,1142 running: false,1143 session: true,1144 up: true1145 },1146 "w2" ->1147 {1148 attached: Set(),1149 built: false,1150 expecting: false,1151 running: false,1152 session: true,1153 up: true1154 }1155 )1156}11571158[State 29]1159{1160 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1161 schedFixed::scheduler::crashes: 2,1162 schedFixed::scheduler::entry:1163 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1164 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1165 schedFixed::scheduler::mAssigned: Set(),1166 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1167 schedFixed::scheduler::mDone: Set("w1"),1168 schedFixed::scheduler::mExpect: Set(),1169 schedFixed::scheduler::mResult: Set("c1"),1170 schedFixed::scheduler::mRetry: Set(),1171 schedFixed::scheduler::mRevoke: Set(),1172 schedFixed::scheduler::mSchedule: Set(),1173 schedFixed::scheduler::published: 1,1174 schedFixed::scheduler::publishedBy: Set("w1"),1175 schedFixed::scheduler::ws:1176 Map(1177 "w1" ->1178 {1179 attached: Set(),1180 built: true,1181 expecting: false,1182 running: false,1183 session: true,1184 up: true1185 },1186 "w2" ->1187 {1188 attached: Set(),1189 built: false,1190 expecting: false,1191 running: false,1192 session: true,1193 up: true1194 }1195 )1196}11971198[State 30]1199{1200 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1201 schedFixed::scheduler::crashes: 2,1202 schedFixed::scheduler::entry: [],1203 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1204 schedFixed::scheduler::mAssigned: Set(),1205 schedFixed::scheduler::mBuild: Set(("c2", "w1")),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("w1"),1214 schedFixed::scheduler::ws:1215 Map(1216 "w1" ->1217 {1218 attached: Set(),1219 built: true,1220 expecting: false,1221 running: false,1222 session: true,1223 up: true1224 },1225 "w2" ->1226 {1227 attached: Set(),1228 built: false,1229 expecting: false,1230 running: false,1231 session: true,1232 up: true1233 }1234 )1235}12361237[ok] No violation found (517ms at 58027 traces/second).1238Trace length statistics: max=28, min=15, average=18.961239You may increase --max-samples and --max-steps.1240Use --verbosity to produce more (or less) output.1241Use --seed=0x6f53884ca97d77c --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: 1,1326 schedNoRevoke::scheduler::entry: [],1327 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1328 schedNoRevoke::scheduler::mAssigned: Set(),1329 schedNoRevoke::scheduler::mBuild: Set(),1330 schedNoRevoke::scheduler::mDone: Set(),1331 schedNoRevoke::scheduler::mExpect: Set(),1332 schedNoRevoke::scheduler::mResult: Set(),1333 schedNoRevoke::scheduler::mRetry: Set(),1334 schedNoRevoke::scheduler::mRevoke: Set(),1335 schedNoRevoke::scheduler::mSchedule: Set("c1"),1336 schedNoRevoke::scheduler::published: 0,1337 schedNoRevoke::scheduler::publishedBy: Set(),1338 schedNoRevoke::scheduler::ws:1339 Map(1340 "w1" ->1341 {1342 attached: Set(),1343 built: false,1344 expecting: false,1345 running: false,1346 session: true,1347 up: true1348 },1349 "w2" ->1350 {1351 attached: Set(),1352 built: false,1353 expecting: false,1354 running: false,1355 session: false,1356 up: false1357 }1358 )1359}13601361[State 3]1362{1363 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1364 schedNoRevoke::scheduler::crashes: 1,1365 schedNoRevoke::scheduler::entry:1366 [{ followers: Set("c1"), leased: true, worker: "w1" }],1367 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1368 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1369 schedNoRevoke::scheduler::mBuild: Set(),1370 schedNoRevoke::scheduler::mDone: Set(),1371 schedNoRevoke::scheduler::mExpect: Set("w1"),1372 schedNoRevoke::scheduler::mResult: Set(),1373 schedNoRevoke::scheduler::mRetry: Set(),1374 schedNoRevoke::scheduler::mRevoke: Set(),1375 schedNoRevoke::scheduler::mSchedule: Set(),1376 schedNoRevoke::scheduler::published: 0,1377 schedNoRevoke::scheduler::publishedBy: Set(),1378 schedNoRevoke::scheduler::ws:1379 Map(1380 "w1" ->1381 {1382 attached: Set(),1383 built: false,1384 expecting: false,1385 running: false,1386 session: true,1387 up: true1388 },1389 "w2" ->1390 {1391 attached: Set(),1392 built: false,1393 expecting: false,1394 running: false,1395 session: false,1396 up: false1397 }1398 )1399}14001401[State 4]1402{1403 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1404 schedNoRevoke::scheduler::crashes: 1,1405 schedNoRevoke::scheduler::entry:1406 [{ followers: Set("c1"), leased: true, worker: "w1" }],1407 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1408 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),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(),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: true,1425 running: true,1426 session: true,1427 up: true1428 },1429 "w2" ->1430 {1431 attached: Set(),1432 built: false,1433 expecting: false,1434 running: false,1435 session: false,1436 up: false1437 }1438 )1439}14401441[State 5]1442{1443 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1444 schedNoRevoke::scheduler::crashes: 2,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: true,1464 running: true,1465 session: false,1466 up: true1467 },1468 "w2" ->1469 {1470 attached: Set(),1471 built: false,1472 expecting: false,1473 running: false,1474 session: false,1475 up: false1476 }1477 )1478}14791480[State 6]1481{1482 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1483 schedNoRevoke::scheduler::crashes: 2,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("c1"),1492 schedNoRevoke::scheduler::mRevoke: Set(),1493 schedNoRevoke::scheduler::mSchedule: Set(),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: true,1503 running: true,1504 session: false,1505 up: true1506 },1507 "w2" ->1508 {1509 attached: Set(),1510 built: false,1511 expecting: false,1512 running: false,1513 session: true,1514 up: true1515 }1516 )1517}15181519[State 7]1520{1521 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1522 schedNoRevoke::scheduler::crashes: 2,1523 schedNoRevoke::scheduler::entry: [],1524 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1525 schedNoRevoke::scheduler::mAssigned: Set(),1526 schedNoRevoke::scheduler::mBuild: Set(),1527 schedNoRevoke::scheduler::mDone: Set(),1528 schedNoRevoke::scheduler::mExpect: Set(),1529 schedNoRevoke::scheduler::mResult: Set(),1530 schedNoRevoke::scheduler::mRetry: Set(),1531 schedNoRevoke::scheduler::mRevoke: Set(),1532 schedNoRevoke::scheduler::mSchedule: Set("c1"),1533 schedNoRevoke::scheduler::published: 0,1534 schedNoRevoke::scheduler::publishedBy: Set(),1535 schedNoRevoke::scheduler::ws:1536 Map(1537 "w1" ->1538 {1539 attached: Set(),1540 built: false,1541 expecting: true,1542 running: true,1543 session: false,1544 up: true1545 },1546 "w2" ->1547 {1548 attached: Set(),1549 built: false,1550 expecting: false,1551 running: false,1552 session: true,1553 up: true1554 }1555 )1556}15571558[State 8]1559{1560 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1561 schedNoRevoke::scheduler::crashes: 2,1562 schedNoRevoke::scheduler::entry:1563 [{ followers: Set("c1"), leased: true, worker: "w2" }],1564 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1565 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1566 schedNoRevoke::scheduler::mBuild: Set(),1567 schedNoRevoke::scheduler::mDone: Set(),1568 schedNoRevoke::scheduler::mExpect: Set("w2"),1569 schedNoRevoke::scheduler::mResult: Set(),1570 schedNoRevoke::scheduler::mRetry: Set(),1571 schedNoRevoke::scheduler::mRevoke: Set(),1572 schedNoRevoke::scheduler::mSchedule: Set(),1573 schedNoRevoke::scheduler::published: 0,1574 schedNoRevoke::scheduler::publishedBy: Set(),1575 schedNoRevoke::scheduler::ws:1576 Map(1577 "w1" ->1578 {1579 attached: Set(),1580 built: false,1581 expecting: true,1582 running: true,1583 session: false,1584 up: true1585 },1586 "w2" ->1587 {1588 attached: Set(),1589 built: false,1590 expecting: false,1591 running: false,1592 session: true,1593 up: true1594 }1595 )1596}15971598[State 9]1599{1600 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1601 schedNoRevoke::scheduler::crashes: 2,1602 schedNoRevoke::scheduler::entry:1603 [{ followers: Set("c1"), leased: true, worker: "w2" }],1604 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1605 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1606 schedNoRevoke::scheduler::mBuild: Set(),1607 schedNoRevoke::scheduler::mDone: Set(),1608 schedNoRevoke::scheduler::mExpect: Set(),1609 schedNoRevoke::scheduler::mResult: Set(),1610 schedNoRevoke::scheduler::mRetry: Set(),1611 schedNoRevoke::scheduler::mRevoke: Set(),1612 schedNoRevoke::scheduler::mSchedule: Set(),1613 schedNoRevoke::scheduler::published: 0,1614 schedNoRevoke::scheduler::publishedBy: Set(),1615 schedNoRevoke::scheduler::ws:1616 Map(1617 "w1" ->1618 {1619 attached: Set(),1620 built: false,1621 expecting: true,1622 running: true,1623 session: false,1624 up: true1625 },1626 "w2" ->1627 {1628 attached: Set(),1629 built: false,1630 expecting: true,1631 running: true,1632 session: true,1633 up: true1634 }1635 )1636}16371638[State 10]1639{1640 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1641 schedNoRevoke::scheduler::crashes: 2,1642 schedNoRevoke::scheduler::entry:1643 [{ followers: Set("c1"), leased: true, worker: "w2" }],1644 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1645 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1646 schedNoRevoke::scheduler::mBuild: Set(),1647 schedNoRevoke::scheduler::mDone: Set(),1648 schedNoRevoke::scheduler::mExpect: Set(),1649 schedNoRevoke::scheduler::mResult: Set(),1650 schedNoRevoke::scheduler::mRetry: Set(),1651 schedNoRevoke::scheduler::mRevoke: Set(),1652 schedNoRevoke::scheduler::mSchedule: Set(),1653 schedNoRevoke::scheduler::published: 0,1654 schedNoRevoke::scheduler::publishedBy: Set(),1655 schedNoRevoke::scheduler::ws:1656 Map(1657 "w1" ->1658 {1659 attached: Set(),1660 built: false,1661 expecting: true,1662 running: true,1663 session: true,1664 up: true1665 },1666 "w2" ->1667 {1668 attached: Set(),1669 built: false,1670 expecting: true,1671 running: true,1672 session: true,1673 up: true1674 }1675 )1676}16771678[violation] Found an issue (484ms at 60366 traces/second).1679Use --verbosity=3 to show executions.1680Use --seed=0x2feaa86216218f10 --backend=rust to reproduce.1681error: Invariant violated1682An example execution:16831684[State 0]1685{1686 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1687 schedNoFence::scheduler::crashes: 0,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: true,1709 up: true1710 },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 1]1724{1725 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1726 schedNoFence::scheduler::crashes: 0,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: true,1748 up: true1749 },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 2]1763{1764 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1765 schedNoFence::scheduler::crashes: 0,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: true,1788 up: true1789 },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 3]1803{1804 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1805 schedNoFence::scheduler::crashes: 0,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("w2"),1813 schedNoFence::scheduler::mResult: Set(),1814 schedNoFence::scheduler::mRetry: Set(),1815 schedNoFence::scheduler::mRevoke: Set(),1816 schedNoFence::scheduler::mSchedule: Set("c2"),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: true,1828 up: true1829 },1830 "w2" ->1831 {1832 attached: Set(),1833 built: false,1834 expecting: false,1835 running: false,1836 session: true,1837 up: true1838 }1839 )1840}18411842[State 4]1843{1844 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1845 schedNoFence::scheduler::crashes: 0,1846 schedNoFence::scheduler::entry:1847 [{ followers: Set("c1"), leased: true, worker: "w2" }],1848 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1849 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),1850 schedNoFence::scheduler::mBuild: Set(),1851 schedNoFence::scheduler::mDone: Set(),1852 schedNoFence::scheduler::mExpect: Set(),1853 schedNoFence::scheduler::mResult: Set(),1854 schedNoFence::scheduler::mRetry: Set(),1855 schedNoFence::scheduler::mRevoke: Set(),1856 schedNoFence::scheduler::mSchedule: Set("c2"),1857 schedNoFence::scheduler::published: 0,1858 schedNoFence::scheduler::publishedBy: Set(),1859 schedNoFence::scheduler::ws:1860 Map(1861 "w1" ->1862 {1863 attached: Set(),1864 built: false,1865 expecting: false,1866 running: false,1867 session: true,1868 up: true1869 },1870 "w2" ->1871 {1872 attached: Set(),1873 built: false,1874 expecting: true,1875 running: true,1876 session: true,1877 up: true1878 }1879 )1880}18811882[State 5]1883{1884 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1885 schedNoFence::scheduler::crashes: 1,1886 schedNoFence::scheduler::entry: [],1887 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1888 schedNoFence::scheduler::mAssigned: Set(),1889 schedNoFence::scheduler::mBuild: Set(),1890 schedNoFence::scheduler::mDone: Set(),1891 schedNoFence::scheduler::mExpect: Set(),1892 schedNoFence::scheduler::mResult: Set(),1893 schedNoFence::scheduler::mRetry: Set("c1", "c2"),1894 schedNoFence::scheduler::mRevoke: Set(),1895 schedNoFence::scheduler::mSchedule: Set(),1896 schedNoFence::scheduler::published: 0,1897 schedNoFence::scheduler::publishedBy: Set(),1898 schedNoFence::scheduler::ws:1899 Map(1900 "w1" ->1901 {1902 attached: Set(),1903 built: false,1904 expecting: false,1905 running: false,1906 session: false,1907 up: true1908 },1909 "w2" ->1910 {1911 attached: Set(),1912 built: false,1913 expecting: true,1914 running: true,1915 session: false,1916 up: true1917 }1918 )1919}19201921[State 6]1922{1923 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1924 schedNoFence::scheduler::crashes: 2,1925 schedNoFence::scheduler::entry: [],1926 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1927 schedNoFence::scheduler::mAssigned: Set(),1928 schedNoFence::scheduler::mBuild: Set(),1929 schedNoFence::scheduler::mDone: Set(),1930 schedNoFence::scheduler::mExpect: Set(),1931 schedNoFence::scheduler::mResult: Set(),1932 schedNoFence::scheduler::mRetry: Set("c1", "c2"),1933 schedNoFence::scheduler::mRevoke: Set(),1934 schedNoFence::scheduler::mSchedule: Set(),1935 schedNoFence::scheduler::published: 0,1936 schedNoFence::scheduler::publishedBy: Set(),1937 schedNoFence::scheduler::ws:1938 Map(1939 "w1" ->1940 {1941 attached: Set(),1942 built: false,1943 expecting: false,1944 running: false,1945 session: false,1946 up: true1947 },1948 "w2" ->1949 {1950 attached: Set(),1951 built: false,1952 expecting: true,1953 running: true,1954 session: false,1955 up: true1956 }1957 )1958}19591960[State 7]1961{1962 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1963 schedNoFence::scheduler::crashes: 2,1964 schedNoFence::scheduler::entry: [],1965 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1966 schedNoFence::scheduler::mAssigned: Set(),1967 schedNoFence::scheduler::mBuild: Set(),1968 schedNoFence::scheduler::mDone: Set(),1969 schedNoFence::scheduler::mExpect: Set(),1970 schedNoFence::scheduler::mResult: Set(),1971 schedNoFence::scheduler::mRetry: Set("c1", "c2"),1972 schedNoFence::scheduler::mRevoke: Set(),1973 schedNoFence::scheduler::mSchedule: Set(),1974 schedNoFence::scheduler::published: 0,1975 schedNoFence::scheduler::publishedBy: Set(),1976 schedNoFence::scheduler::ws:1977 Map(1978 "w1" ->1979 {1980 attached: Set(),1981 built: false,1982 expecting: false,1983 running: false,1984 session: true,1985 up: true1986 },1987 "w2" ->1988 {1989 attached: Set(),1990 built: false,1991 expecting: true,1992 running: true,1993 session: false,1994 up: true1995 }1996 )1997}19981999[State 8]2000{2001 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2002 schedNoFence::scheduler::crashes: 2,2003 schedNoFence::scheduler::entry: [],2004 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),2005 schedNoFence::scheduler::mAssigned: Set(),2006 schedNoFence::scheduler::mBuild: Set(),2007 schedNoFence::scheduler::mDone: Set(),2008 schedNoFence::scheduler::mExpect: Set(),2009 schedNoFence::scheduler::mResult: Set(),2010 schedNoFence::scheduler::mRetry: Set("c2"),2011 schedNoFence::scheduler::mRevoke: Set(),2012 schedNoFence::scheduler::mSchedule: Set("c1"),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 9]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("w1"),2049 schedNoFence::scheduler::mResult: Set(),2050 schedNoFence::scheduler::mRetry: Set("c2"),2051 schedNoFence::scheduler::mRevoke: Set(),2052 schedNoFence::scheduler::mSchedule: Set(),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: false,2062 running: false,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 10]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("c2"),2091 schedNoFence::scheduler::mRevoke: Set(),2092 schedNoFence::scheduler::mSchedule: Set(),2093 schedNoFence::scheduler::published: 0,2094 schedNoFence::scheduler::publishedBy: Set(),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: false,2110 expecting: true,2111 running: true,2112 session: false,2113 up: true2114 }2115 )2116}21172118[State 11]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(),2130 schedNoFence::scheduler::mRetry: Set("c2"),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 12]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(),2170 schedNoFence::scheduler::mRetry: Set("c2"),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 (591ms at 45971 traces/second).2199Use --verbosity=3 to show executions.2200Use --seed=0xaf1541fad088ae93 --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" -> CIdle),2285 schedNoPush::scheduler::crashes: 0,2286 schedNoPush::scheduler::entry:2287 [{ followers: Set("c1"), leased: true, worker: "w2" }],2288 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2289 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2290 schedNoPush::scheduler::mBuild: Set(),2291 schedNoPush::scheduler::mDone: Set(),2292 schedNoPush::scheduler::mExpect: Set(),2293 schedNoPush::scheduler::mResult: Set(),2294 schedNoPush::scheduler::mRetry: Set(),2295 schedNoPush::scheduler::mRevoke: Set(),2296 schedNoPush::scheduler::mSchedule: Set(),2297 schedNoPush::scheduler::published: 0,2298 schedNoPush::scheduler::publishedBy: Set(),2299 schedNoPush::scheduler::ws:2300 Map(2301 "w1" ->2302 {2303 attached: Set(),2304 built: false,2305 expecting: false,2306 running: false,2307 session: true,2308 up: true2309 },2310 "w2" ->2311 {2312 attached: Set(),2313 built: false,2314 expecting: false,2315 running: false,2316 session: true,2317 up: true2318 }2319 )2320}23212322[State 3]2323{2324 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2325 schedNoPush::scheduler::crashes: 0,2326 schedNoPush::scheduler::entry:2327 [{ followers: Set("c1"), leased: true, worker: "w2" }],2328 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2329 schedNoPush::scheduler::mAssigned: Set(),2330 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2331 schedNoPush::scheduler::mDone: Set(),2332 schedNoPush::scheduler::mExpect: Set(),2333 schedNoPush::scheduler::mResult: Set(),2334 schedNoPush::scheduler::mRetry: Set(),2335 schedNoPush::scheduler::mRevoke: Set(),2336 schedNoPush::scheduler::mSchedule: Set(),2337 schedNoPush::scheduler::published: 0,2338 schedNoPush::scheduler::publishedBy: Set(),2339 schedNoPush::scheduler::ws:2340 Map(2341 "w1" ->2342 {2343 attached: Set(),2344 built: false,2345 expecting: false,2346 running: false,2347 session: true,2348 up: true2349 },2350 "w2" ->2351 {2352 attached: Set(),2353 built: false,2354 expecting: false,2355 running: false,2356 session: true,2357 up: true2358 }2359 )2360}23612362[State 4]2363{2364 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2365 schedNoPush::scheduler::crashes: 1,2366 schedNoPush::scheduler::entry: [],2367 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2368 schedNoPush::scheduler::mAssigned: Set(),2369 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),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: false,2387 up: true2388 },2389 "w2" ->2390 {2391 attached: Set(),2392 built: false,2393 expecting: false,2394 running: false,2395 session: false,2396 up: true2397 }2398 )2399}24002401[State 5]2402{2403 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),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(("c1", "w2")),2409 schedNoPush::scheduler::mDone: Set(),2410 schedNoPush::scheduler::mExpect: Set(),2411 schedNoPush::scheduler::mResult: Set(),2412 schedNoPush::scheduler::mRetry: Set(),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: true,2435 up: true2436 }2437 )2438}24392440[State 6]2441{2442 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),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(),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(),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("c1"),2470 built: false,2471 expecting: true,2472 running: true,2473 session: true,2474 up: true2475 }2476 )2477}24782479[violation] Found an issue (510ms at 36959 traces/second).2480Use --verbosity=3 to show executions.2481Use --seed=0x29b2e1e31cf88209 --backend=rust to reproduce.2482error: Invariant violated2483An example execution:24842485[State 0]2486{2487 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2488 schedNoReport::scheduler::crashes: 0,2489 schedNoReport::scheduler::entry: [],2490 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2491 schedNoReport::scheduler::mAssigned: Set(),2492 schedNoReport::scheduler::mBuild: Set(),2493 schedNoReport::scheduler::mDone: Set(),2494 schedNoReport::scheduler::mExpect: Set(),2495 schedNoReport::scheduler::mResult: Set(),2496 schedNoReport::scheduler::mRetry: Set(),2497 schedNoReport::scheduler::mRevoke: Set(),2498 schedNoReport::scheduler::mSchedule: Set(),2499 schedNoReport::scheduler::published: 0,2500 schedNoReport::scheduler::publishedBy: Set(),2501 schedNoReport::scheduler::ws:2502 Map(2503 "w1" ->2504 {2505 attached: Set(),2506 built: false,2507 expecting: false,2508 running: false,2509 session: true,2510 up: true2511 },2512 "w2" ->2513 {2514 attached: Set(),2515 built: false,2516 expecting: false,2517 running: false,2518 session: true,2519 up: true2520 }2521 )2522}25232524[State 1]2525{2526 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2527 schedNoReport::scheduler::crashes: 0,2528 schedNoReport::scheduler::entry: [],2529 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2530 schedNoReport::scheduler::mAssigned: Set(),2531 schedNoReport::scheduler::mBuild: Set(),2532 schedNoReport::scheduler::mDone: Set(),2533 schedNoReport::scheduler::mExpect: Set(),2534 schedNoReport::scheduler::mResult: Set(),2535 schedNoReport::scheduler::mRetry: Set(),2536 schedNoReport::scheduler::mRevoke: Set(),2537 schedNoReport::scheduler::mSchedule: Set("c2"),2538 schedNoReport::scheduler::published: 0,2539 schedNoReport::scheduler::publishedBy: Set(),2540 schedNoReport::scheduler::ws:2541 Map(2542 "w1" ->2543 {2544 attached: Set(),2545 built: false,2546 expecting: false,2547 running: false,2548 session: true,2549 up: true2550 },2551 "w2" ->2552 {2553 attached: Set(),2554 built: false,2555 expecting: false,2556 running: false,2557 session: true,2558 up: true2559 }2560 )2561}25622563[State 2]2564{2565 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2566 schedNoReport::scheduler::crashes: 0,2567 schedNoReport::scheduler::entry:2568 [{ followers: Set("c2"), leased: true, worker: "w2" }],2569 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2570 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2571 schedNoReport::scheduler::mBuild: Set(),2572 schedNoReport::scheduler::mDone: Set(),2573 schedNoReport::scheduler::mExpect: Set("w2"),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 3]2604{2605 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2606 schedNoReport::scheduler::crashes: 1,2607 schedNoReport::scheduler::entry:2608 [{ followers: Set("c2"), leased: true, worker: "w2" }],2609 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2610 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2611 schedNoReport::scheduler::mBuild: Set(),2612 schedNoReport::scheduler::mDone: Set(),2613 schedNoReport::scheduler::mExpect: Set("w2"),2614 schedNoReport::scheduler::mResult: Set(),2615 schedNoReport::scheduler::mRetry: Set(),2616 schedNoReport::scheduler::mRevoke: Set(),2617 schedNoReport::scheduler::mSchedule: Set(),2618 schedNoReport::scheduler::published: 0,2619 schedNoReport::scheduler::publishedBy: Set(),2620 schedNoReport::scheduler::ws:2621 Map(2622 "w1" ->2623 {2624 attached: Set(),2625 built: false,2626 expecting: false,2627 running: false,2628 session: false,2629 up: false2630 },2631 "w2" ->2632 {2633 attached: Set(),2634 built: false,2635 expecting: false,2636 running: false,2637 session: true,2638 up: true2639 }2640 )2641}26422643[State 4]2644{2645 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2646 schedNoReport::scheduler::crashes: 1,2647 schedNoReport::scheduler::entry:2648 [{ followers: Set("c2"), leased: true, worker: "w2" }],2649 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2650 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2651 schedNoReport::scheduler::mBuild: Set(),2652 schedNoReport::scheduler::mDone: Set(),2653 schedNoReport::scheduler::mExpect: Set(),2654 schedNoReport::scheduler::mResult: Set(),2655 schedNoReport::scheduler::mRetry: Set(),2656 schedNoReport::scheduler::mRevoke: Set(),2657 schedNoReport::scheduler::mSchedule: Set(),2658 schedNoReport::scheduler::published: 0,2659 schedNoReport::scheduler::publishedBy: Set(),2660 schedNoReport::scheduler::ws:2661 Map(2662 "w1" ->2663 {2664 attached: Set(),2665 built: false,2666 expecting: false,2667 running: false,2668 session: false,2669 up: false2670 },2671 "w2" ->2672 {2673 attached: Set(),2674 built: false,2675 expecting: true,2676 running: true,2677 session: true,2678 up: true2679 }2680 )2681}26822683[State 5]2684{2685 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2686 schedNoReport::scheduler::crashes: 2,2687 schedNoReport::scheduler::entry: [],2688 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2689 schedNoReport::scheduler::mAssigned: Set(),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("c2"),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: false,2706 running: false,2707 session: false,2708 up: false2709 },2710 "w2" ->2711 {2712 attached: Set(),2713 built: false,2714 expecting: true,2715 running: true,2716 session: false,2717 up: true2718 }2719 )2720}27212722[State 6]2723{2724 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2725 schedNoReport::scheduler::crashes: 2,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("c1"),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: false,2745 running: false,2746 session: false,2747 up: false2748 },2749 "w2" ->2750 {2751 attached: Set(),2752 built: false,2753 expecting: true,2754 running: true,2755 session: false,2756 up: true2757 }2758 )2759}27602761[State 7]2762{2763 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "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("c1"),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: false,2784 running: false,2785 session: true,2786 up: true2787 },2788 "w2" ->2789 {2790 attached: Set(),2791 built: false,2792 expecting: true,2793 running: true,2794 session: false,2795 up: true2796 }2797 )2798}27992800[State 8]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(),2812 schedNoReport::scheduler::mRevoke: Set(),2813 schedNoReport::scheduler::mSchedule: Set("c1", "c2"),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: false,2823 running: false,2824 session: true,2825 up: true2826 },2827 "w2" ->2828 {2829 attached: Set(),2830 built: false,2831 expecting: true,2832 running: true,2833 session: false,2834 up: true2835 }2836 )2837}28382839[State 9]2840{2841 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2842 schedNoReport::scheduler::crashes: 2,2843 schedNoReport::scheduler::entry:2844 [{ followers: Set("c2"), leased: true, worker: "w1" }],2845 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2846 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2847 schedNoReport::scheduler::mBuild: Set(),2848 schedNoReport::scheduler::mDone: Set(),2849 schedNoReport::scheduler::mExpect: Set("w1"),2850 schedNoReport::scheduler::mResult: Set(),2851 schedNoReport::scheduler::mRetry: Set(),2852 schedNoReport::scheduler::mRevoke: Set(),2853 schedNoReport::scheduler::mSchedule: Set("c1"),2854 schedNoReport::scheduler::published: 0,2855 schedNoReport::scheduler::publishedBy: Set(),2856 schedNoReport::scheduler::ws:2857 Map(2858 "w1" ->2859 {2860 attached: Set(),2861 built: false,2862 expecting: false,2863 running: false,2864 session: true,2865 up: true2866 },2867 "w2" ->2868 {2869 attached: Set(),2870 built: false,2871 expecting: true,2872 running: true,2873 session: false,2874 up: true2875 }2876 )2877}28782879[State 10]2880{2881 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2882 schedNoReport::scheduler::crashes: 2,2883 schedNoReport::scheduler::entry:2884 [{ followers: Set("c2"), leased: true, worker: "w1" }],2885 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2886 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2887 schedNoReport::scheduler::mBuild: Set(),2888 schedNoReport::scheduler::mDone: Set(),2889 schedNoReport::scheduler::mExpect: Set("w1"),2890 schedNoReport::scheduler::mResult: Set(),2891 schedNoReport::scheduler::mRetry: Set(),2892 schedNoReport::scheduler::mRevoke: Set(),2893 schedNoReport::scheduler::mSchedule: Set("c1"),2894 schedNoReport::scheduler::published: 0,2895 schedNoReport::scheduler::publishedBy: Set(),2896 schedNoReport::scheduler::ws:2897 Map(2898 "w1" ->2899 {2900 attached: Set(),2901 built: false,2902 expecting: false,2903 running: false,2904 session: true,2905 up: true2906 },2907 "w2" ->2908 {2909 attached: Set(),2910 built: false,2911 expecting: true,2912 running: true,2913 session: true,2914 up: true2915 }2916 )2917}29182919[State 11]2920{2921 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2922 schedNoReport::scheduler::crashes: 2,2923 schedNoReport::scheduler::entry:2924 [{ followers: Set("c2"), leased: true, worker: "w1" }],2925 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2926 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2927 schedNoReport::scheduler::mBuild: Set(),2928 schedNoReport::scheduler::mDone: Set(),2929 schedNoReport::scheduler::mExpect: Set(),2930 schedNoReport::scheduler::mResult: Set(),2931 schedNoReport::scheduler::mRetry: Set(),2932 schedNoReport::scheduler::mRevoke: Set(),2933 schedNoReport::scheduler::mSchedule: Set("c1"),2934 schedNoReport::scheduler::published: 0,2935 schedNoReport::scheduler::publishedBy: Set(),2936 schedNoReport::scheduler::ws:2937 Map(2938 "w1" ->2939 {2940 attached: Set(),2941 built: false,2942 expecting: true,2943 running: true,2944 session: true,2945 up: true2946 },2947 "w2" ->2948 {2949 attached: Set(),2950 built: false,2951 expecting: true,2952 running: true,2953 session: true,2954 up: true2955 }2956 )2957}29582959[violation] Found an issue (508ms at 52467 traces/second).2960Use --verbosity=3 to show executions.2961Use --seed=0x5fa6c349411c8310 --backend=rust to reproduce.2962error: Invariant violated2963An example execution:29642965[State 0]2966{2967 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2968 schedTerminal::scheduler::crashes: 0,2969 schedTerminal::scheduler::entry: [],2970 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2971 schedTerminal::scheduler::mAssigned: Set(),2972 schedTerminal::scheduler::mBuild: Set(),2973 schedTerminal::scheduler::mDone: Set(),2974 schedTerminal::scheduler::mExpect: Set(),2975 schedTerminal::scheduler::mResult: Set(),2976 schedTerminal::scheduler::mRetry: Set(),2977 schedTerminal::scheduler::mRevoke: Set(),2978 schedTerminal::scheduler::mSchedule: Set(),2979 schedTerminal::scheduler::published: 0,2980 schedTerminal::scheduler::publishedBy: Set(),2981 schedTerminal::scheduler::ws:2982 Map(2983 "w1" ->2984 {2985 attached: Set(),2986 built: false,2987 expecting: false,2988 running: false,2989 session: true,2990 up: true2991 },2992 "w2" ->2993 {2994 attached: Set(),2995 built: false,2996 expecting: false,2997 running: false,2998 session: true,2999 up: true3000 }3001 )3002}30033004[State 1]3005{3006 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3007 schedTerminal::scheduler::crashes: 1,3008 schedTerminal::scheduler::entry: [],3009 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3010 schedTerminal::scheduler::mAssigned: Set(),3011 schedTerminal::scheduler::mBuild: Set(),3012 schedTerminal::scheduler::mDone: Set(),3013 schedTerminal::scheduler::mExpect: Set(),3014 schedTerminal::scheduler::mResult: Set(),3015 schedTerminal::scheduler::mRetry: Set(),3016 schedTerminal::scheduler::mRevoke: Set(),3017 schedTerminal::scheduler::mSchedule: Set(),3018 schedTerminal::scheduler::published: 0,3019 schedTerminal::scheduler::publishedBy: Set(),3020 schedTerminal::scheduler::ws:3021 Map(3022 "w1" ->3023 {3024 attached: Set(),3025 built: false,3026 expecting: false,3027 running: false,3028 session: false,3029 up: true3030 },3031 "w2" ->3032 {3033 attached: Set(),3034 built: false,3035 expecting: false,3036 running: false,3037 session: false,3038 up: true3039 }3040 )3041}30423043[State 2]3044{3045 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3046 schedTerminal::scheduler::crashes: 1,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("c2"),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: false,3068 up: true3069 },3070 "w2" ->3071 {3072 attached: Set(),3073 built: false,3074 expecting: false,3075 running: false,3076 session: false,3077 up: true3078 }3079 )3080}30813082[State 3]3083{3084 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),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[violation] Found an issue (499ms at 3826 traces/second).3122Use --verbosity=3 to show executions.3123Use --seed=0xbaeda148b737b63c --backend=rust to reproduce.3124error: Invariant violated3125An example execution:31263127[State 0]3128{3129 pushFixed::push::byPath: Map(),3130 pushFixed::push::inflight: Set(),3131 pushFixed::push::left: Map(),3132 pushFixed::push::sent: Map()3133}31343135[State 1]3136{3137 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3138 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3139 pushFixed::push::left: Map(1 -> 2),3140 pushFixed::push::sent: Map(1 -> Set("a", "b"))3141}31423143[State 2]3144{3145 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3146 pushFixed::push::inflight: Set((1, "b")),3147 pushFixed::push::left: Map(1 -> 1),3148 pushFixed::push::sent: Map(1 -> Set("a", "b"))3149}31503151[State 3]3152{3153 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3154 pushFixed::push::inflight: Set(),3155 pushFixed::push::left: Map(1 -> 0),3156 pushFixed::push::sent: Map(1 -> Set("a", "b"))3157}31583159[State 4]3160{3161 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3162 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3163 pushFixed::push::left: Map(1 -> 0, 3 -> 2),3164 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3165}31663167[State 5]3168{3169 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3170 pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "a"), (3, "b")),3171 pushFixed::push::left: Map(1 -> 0, 2 -> 2, 3 -> 2),3172 pushFixed::push::sent:3173 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3174}31753176[State 6]3177{3178 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3179 pushFixed::push::inflight: Set((2, "a"), (3, "a"), (3, "b")),3180 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 2),3181 pushFixed::push::sent:3182 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3183}31843185[State 7]3186{3187 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3188 pushFixed::push::inflight: Set((2, "a"), (3, "a")),3189 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 1),3190 pushFixed::push::sent:3191 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3192}31933194[State 8]3195{3196 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3197 pushFixed::push::inflight: Set((2, "a")),3198 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 0),3199 pushFixed::push::sent:3200 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3201}32023203[State 9]3204{3205 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3206 pushFixed::push::inflight: Set(),3207 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3208 pushFixed::push::sent:3209 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3210}32113212[ok] No violation found (149ms at 134228 traces/second).3213Trace length statistics: max=9, min=7, average=8.103214You may increase --max-samples and --max-steps.3215Use --verbosity to produce more (or less) output.3216Use --seed=0x3a3d887ab60fb075 --backend=rust to reproduce.